Accelerating all-path reachability proofs with one-path reachability proofs

[Stevengre]

All-path reachability proofs (APRProof) are slow: at every step the symbolic engine must search for applicable rules and branch over them through the SMT solver.

This proposal splits the work into two independently useful pieces:

1. Proof Checker — a trusted component that, given an APRProof, force-applies the rule on each edge (no search, no branching) and checks coverage.
   It needs no exploration and already accelerates re-validating an existing proof (e.g. a cached proof after a semantics change).
2. Concolic Explorer — a new component that builds such proofs: run a concrete seed on the LLVM backend, take its rule trace as a one-path certificate, and let the Checker validate it while computing remainders; each remainder yields a new seed down a different path, until none is left.

Concrete execution is an untrusted, pluggable oracle that only decides which rule to apply; all soundness lives in the Checker.

[ehildenb]

I'm not sure how much faster this will be if you actually are checking at each step which rules could apply. Have you profiled the backend to understand where the slowdowns are?

We could have it blindly apply the rules in the rule list, and not check if other rules could apply, which would be a good sanity check. But it's not a fully sound check, because if a rule is added that could apply, then the all-path reachability proof wouldn't apply anymore.

Maybe there would be a way to check for new rules: does it intersect with any other rules on the LHS? If the answer is "no", then the checker is sound. If the answer is "yes", then only check those extra rules on cases where the new/changed rule could apply because it overlaps with the next rule.

[Stevengre]

I won't check every step to find which rules could apply.

Most rules are applied blindly, except for those with a requires clause. For those, we need to evaluate wether remainder exist or not by C ∧ ¬ requires. If SAT, the model provides a concrete seed the uncovered case for LLVM backend to explore the missing paths.

I've run concrete programs under both the Haskell and LLVM backends and observed a significant performance gap. That said, I can profile the backend during an APR proof to pinpoint where the slowdown actually is.

[palinatolmach]

@Stevengre can you share the examples you've used?

[Stevengre]

It's a rust example using mir-semantics. I cannot find the pr, but it's something like

x = 1
while (x < 1000):
  x = x + 1