All-path reachability proof checker

[Stevengre]

check(APRProof) → (ProofStatus, APRProof, [remainder], [undecided_obligation]).

The prover is slow because at every step it searches for applicable rules and calls SMT to decide which branches are feasible; re-establishing a proof (after a semantics change, or to trust one from elsewhere) re-pays all of it, though the finished proof already records which rules fire and where it branches.

The Checker instead treats the KCFG as a certificate and validates every element by its kind: edges are re-applied by the Haskell backend (force-apply the recorded rules, no search), splits and covers are discharged by SMT in pyk.
Because the fired rule is known, there is no rule-search SMT and the taken branch is feasible by its concrete witness; only the irreducible SMT remains — split coverage (parent ∧ ¬⋁cᵢ UNSAT) and cover subsumption (implies) — and even that moves off the critical path, since the rule sequence is fixed: rewrite streams ahead while SMT runs concurrently.
All soundness lives here.

Goal. ≥~2× faster than the prover, or reusing a proof / adding concolic execution is not worth it — measured once a first APRProofChecker exists, not before.

What is checked, and how

• Edge source --[τ]--> target, a rule sequence τ = [r₁, …, rₙ] — Haskell backend.
  guided_execute force-applies τ to source and returns the resulting end state target'; it is agnostic to any previously recorded target.
  If a step branches before τ is exhausted, the edge hides an uncovered case and the check emits a remainder.
• Split parent into branches with conditions c₁, …, cₖ — SMT.
  The branches must be exhaustive and non-vacuous: parent ∧ ¬(c₁ ∨ … ∨ cₖ) is UNSAT (nothing falls through the cracks) and each parent ∧ cᵢ is SAT.
  A satisfiable parent ∧ ¬⋁cᵢ is a coverage hole, and its model is a remainder seed.
• Cover node ⟹ target (or an ancestor, under a substitution) — SMT, implies.
  This closes the final target and loops; a BMC depth bound is the backstop when no cover is found.
• Leaf — it must subsume the target (success) or be a known terminal/bounded node; a stuck leaf that subsumes neither is a Failed counterexample.

Any of these SMT checks may return unknown/timeout → an UndecidedObligation; it never silently passes.

Layers

• Haskell backend — guided_execute(S, τ) (new RPC).
  Force-apply rules from τ to S (no rule search), folding steps into a single Edge; cheap simplification discharges trivial guards.
  At the first step whose guard it cannot cheaply discharge, it solves C ∧ ¬guard in place: UNSAT → fold and continue (no round-trip); SAT → return the Edge (depth, end state S'), the taken branch's guard (the Split condition), and the remainder's model (the ¬guard seed); unknown → return an obligation; the trace end also returns.
  It uses SMT for these remainder checks but never for rule search, and can overlap rewriting along the fixed τ with the remainder solve.
  Checking the taken branch's feasibility is an optional parameter — skip it when a concrete witness already establishes it (explore mode), enable it when re-validating a proof without one.
• pyk — the driver.
  Drive guided_execute and record its Edges, Splits, and remainder seeds; check aggregate split coverage (parent ∧ ¬⋁cᵢ) and cover subsumption via implies; maintain the KCFG and accumulate the result tuple and the monotone ProofStatus.
  Reuses the existing implies, get_model, and simplify RPCs.

Outputs

• ProofStatus — Passed / Pending / Failed.
• updated APRProof — the validated (and, when building, grown) KCFG.
• [remainder] — coverage holes still open.
  Each is remainder = (depth, model, obligation): depth locates the node; model is a concrete seed for the uncovered sub-region (set when the residual is SAT); obligation is set instead when the solver could not decide.
• [undecided_obligation] —

UndecidedObligation:
  source_node_id : int        # node whose check spawned the query (referenced, not owned)
  depth          : int        # rewrite steps from source_node_id to the query
  kind           : edge | split-coverage | cover
  rule_id        : str | None
  query          : Pattern    # the term the solver could not decide
  result         : unknown | timeout

Passed ⟺ remainders == [] and undecided_obligations == [] and every leaf subsumes the target.