Skip to content

5. Proof certificates

"The assertion holds" is intrepid's word. When the word is not enough (a certification, a reviewer, a customer), a property proved can come with its proof certificate: a script that any SMT solver checks, without intrepid and without trusting it.

Getting the proofs

In the panel's Verify tab, tick proof certificates, and press ✔ Verify. Each property that holds, and each target proved unreachable, comes with its proof: its row says proof. intrepid checks every proof before giving it.

Proof certificates: the right-click menu of a property proved Proof certificates: the right-click menu of a property proved

Right-click the row of ack_silences, and Export proof…: it saves the proof as an SMT-LIB 2 script, and offers to check it with an SMT solver found on your machine (z3, cvc5, bitwuzla, yices), another one than intrepid uses if there is one.

What is in a proof

The script says what it proves and how, in comments, then states it in SMT-LIB 2, the standard language of SMT solvers. For ack_silences:

; A proof certificate from intrepid: no target of the circuit is reachable.
; Engine: br. Kind: inductive invariant.
;
; Any path from an initial state, the assumptions true at each step,
; is in Inv at each step (initiation, then consecution), and Inv
; excludes the targets (safety): no target is reachable.
; Inv is over the latches.
;
; Each check-sat below must answer unsat: run the script with any SMT-LIB 2
; solver (z3 FILE, cvc5 FILE, ...) to check the proof.

then the circuit's initial states (Init), its assumptions (Assume: here speed ≥ 0), its steps (Trans), the states where the assertion fails (Bad), the invariant Inv, and three questions to the solver, each of which must answer unsat:

  • initiation: is there an initial state outside Inv?
  • consecution: can a step lead from inside Inv to outside?
  • safety: is there a state in Inv where the assertion fails?

Three times no is the proof: every run stays in Inv, and in Inv the assertion holds. Check it yourself:

$ z3 ack_silences.smt2
unsat
unsat
unsat

The kind of proof depends on the engine that found it: backward reachability (br) and PDR prove with an inductive invariant, as here; k-induction with its base cases and its step. The script says which.

Next: the tests that show the logic is exercised.