Module bmc 

Bounded model checking, k-induction, and vacuity over ProofExpr — pure-Rust, certified, Z3-free, browser-ready.

A transition system is given as three closures over signal@t atoms:

• init — the constraint at t = 0,
• trans(t) — relates state @t to @t+1,
• property(t) — the safety property that must hold at @t.

Every question reduces to one unsatisfiability query discharged by crate::sat::prove_unsat (CDCL + RUP certification):

• BMC (find_counterexample) — is a violating state reachable within k steps? init ∧ ⋀ trans ∧ ¬property(k) satisfiable ⇒ a counterexample trace.
• k-induction (prove_invariant) — base (no violation in the first k steps) + step (property is k-inductive); both certified-UNSAT ⇒ the property holds for ALL reachable states (an unbounded proof, not merely bounded).
• Vacuity (check_vacuity) — can the antecedent ever fire? Unsatisfiable ⇒ a dead trigger and a vacuously-true property.

Enums

BmcOutcome

The verdict of bounded model checking.

InductionOutcome

The verdict of k-induction.

VacuityOutcome

The verdict of a vacuity check.

Functions

check_vacuity

Vacuity: can antecedent ever be satisfied? An unsatisfiable antecedent means the property is never actually exercised (a vacuous pass / dead trigger).

find_counterexample

Bounded model checking: search for a reachable state violating property within max_k transitions, returning the shallowest counterexample (and its trace) if one exists.

find_counterexample_incremental

Bounded model checking, incrementally: the unrolling is clausified ONCE into a single persistent solver, and each depth’s violation ¬property(k) is checked by crate::cdcl::Solver::solve_under_assumptions. Every clause learned while ruling out a shallow depth is reused at the next — the IPASIR amortisation that makes deep BMC fast.

find_counterexample_symmetric

Bounded model checking with temporal symmetry breaking. Interchangeable signals (temporal_symmetry_pairs) give a system automorphism that holds at every frame, so a swap lifted uniformly through the unrolling permutes counterexample trajectories. We order each pair at the initial frame (a@0 ≤ b@0, i.e. ¬a@0 ∨ b@0): a sound partial lex-leader that keeps at least one trajectory per symmetry orbit. Hence a counterexample exists under the ordering iff one exists at all, and the shallowest violating depth is unchanged — the verdict matches find_counterexample, with the symmetric search space pruned.

prove_invariant

k-induction: prove property is an invariant of the transition system.

temporal_symmetry_pairs

The temporal symmetries of a transition system: pairs of base signals interchangeable across all time — a swap that preserves the initial constraint, the transition relation (checked on the generic frame trans(0), hence on every frame by uniformity), and the property. Each surviving pair is a genuine system automorphism when lifted uniformly through the unrolling.