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: every obligation Lean-proved AND all bindings implemented
  • L4: every obligation Lean-proved — strict per-obligation coverage, proved + not_applicable >= proof_obligations.len() with proved > 0 (partial coverage is NOT L4; see [is_lean_proved])
  • L3: has Kani harnesses AND falsification tests cover obligations
  • L2: falsification tests count >= obligations count
  • L1: contract exists with equations