Skip to main content

compute_proof_level

provable_contracts::proof_status

Function compute_proof_level 

Source 
pub fn compute_proof_level(
    contract: &Contract,
    binding_status: Option<(u32, u32)>,
) -> ProofLevel
Expand description

Compute the proof level for a single contract.

Derivation rules (highest matching level wins):

  • L5: all Lean proved AND all bindings implemented
  • L4: all Lean proved (verification_summary.l4_lean_proved == total)
  • L3: has Kani harnesses AND falsification tests cover obligations
  • L2: falsification tests count >= obligations count
  • L1: contract exists with equations