Module formal_verify 

Formal Verification Helpers

This module provides utilities and helpers to support formal verification of cryptographic implementations, including property-based testing, invariant checking, and verification condition generation.

Features

• Property-based testing: Automatic generation of test cases
• Invariant checking: Runtime verification of cryptographic properties
• Pre/post-condition checking: Function contract verification
• State machine verification: Verify state transitions are valid
• Symbolic execution helpers: Support for symbolic analysis
• Proof obligations: Generate verification conditions

Example

use chie_crypto::formal_verify::{Invariant, PropertyChecker, check_invariant};

// Define an invariant
let inv = Invariant::new("key_length", |state: &[u8]| {
    state.len() == 32
});

// Check the invariant
let key = [0u8; 32];
assert!(inv.check(&key));

// Property-based testing
let mut checker = PropertyChecker::new();
checker.add_property("encryption_decryption_roundtrip", |data: &[u8]| {
    // Property: encrypt(decrypt(x)) == x
    true // simplified example
});

Structs

Invariant

Invariant that must hold for a cryptographic operation

PostCondition

Post-condition for a function

PreCondition

Pre-condition for a function

PropertyCheckResult

Result of property checking

PropertyChecker

Property-based test checker

PropertyResult

Result for a single property

StateMachine

State machine verifier

VerificationCondition

Verification condition

Functions

check_invariant

Helper function to check an invariant and panic if it doesn’t hold

check_postcondition

Helper function to check a post-condition

check_precondition

Helper function to check a pre-condition