proof: #192 phase 3 — proven term-DAG encoder and folding/hashing pass; the solver runs them (TR-061) - #222
Merged
Merged
Conversation
…s; the solver runs them (TR-061)
The lowering from the term DAG to the CNF is now proven end to end over
the Aeneas model of blast_kernel.rs, and it is the code the solver runs.
Kernel (crates/ordeal/src/blast_kernel.rs, Aeneas fragment):
- DagNode: the closed term.rs fragment with operands as node indices;
encode_node / encode walk a topologically ordered DAG calling the
proven rule for every node (Var takes the next w inputs, Const reads a
bit table, the boolean connectives are one push_and / push_or).
- compact / compact_and / hint_matches / map_lit / map_word: the shipped
Aig::and's constant folds and operand normalisation, with gate sharing
driven by hints the pass checks (a wrong hint costs a duplicate gate,
never a value).
Lean (sorry-free, axiom-clean, pinned in AxiomCheck.lean):
- BlasterFrame.lean: structural frame lemmas for every rule that lacked
one, plus the leaf specs of the new helpers.
- BlasterDag.lean: the DAG semantics directly over Lean BitVec (dagSim,
dagWidths, DagWF, dagBool); encode_node_spec (32 arms gluing each
rule's frame to its _bitvec capstone); encode_sound.
- BlasterCompact.lean: compact_sound / compact_sound_lit, for any hints.
- BlasterCapstone.lean: dag_refuted (encode + compact + map_word +
tseitin + an accepted check_steps run ⟹ no input assignment satisfies
the DAG's roots) and dag_refuted_raw, composed with lrat_check_sound.
Solver (crates/ordeal/src/{dag.rs,solver.rs}): the canonicalized
assertions become a hash-consed term DAG (dag.rs, untrusted glue);
lower_with runs blast_kernel::encode, dag::strash_hints (untrusted; the
old HashMap strash's decisions), blast_kernel::compact and
blast_kernel::tseitin. The phase-2 replay bridge (blast/mod.rs) and
cnf.rs / aig.rs leave the production path and serve the per-family
differentials and the gate-identity tests.
Shipped bytes unchanged: ordeal check --format json is byte-identical
(stdout, stderr, exit code) to the v0.25.0 release binary on all 24
fixtures; cnf_gap_digest prints the four phase-2 digests unchanged over
1211 queries (44.6M clauses); dag::tests pin compact + kernel tseitin
against the Aig::and replay + cnf::tseitin node for node and clause for
clause.
Verification: regenerated models (0 axioms); lake build 1724 jobs, 0
sorry; axiom gate; three negative controls (encoder rule swap, dropped
fold, dropped negation — each fails its proof; restored, touched, clean
rebuild); cargo test --workspace debug and release; nextest 255 passed,
71 results mapped, no dead marker; clippy default and
--features oracle,cert-bundle; fmt; Z3 differential 12 passed;
kani_tiers.sh check; wasm32-wasip2 release build;
check_verification_citations.sh; rivet validate. blast+Tseitin time is
1.1–1.55x on the bench queries and 1.85x on the oracle corpus total
(docs/design/query-cnf-gap.md has the table and the reading).
Implements: TR-061
Verifies: VER-061
Refs: #192
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Phase 3 of #192. The solver now lowers every query through a proven term-DAG encoder and a proven folding/hashing pass, and one theorem covers the whole chain from the term DAG to an accepted LRAT certificate.
What changes
blast_kernel.rs(Aeneas fragment) adds:DagNode, covering the closedterm.rsfragment;encode, which calls the proven rules per node;compact, which reproducesAig::and's folding and operand normalisation and shares gates via checked hints.dag.rs(new, untrusted): a hash-consedDagBuilderfrom canonicalised assertions, plusstrash_hints.solver.rsnow runsencode → compact → map_word → tseitin, all kernel code. The phase-2 bridge,cnf.rsandaig.rsare now only used by tests.New theorems
They live in
BlasterFrame,BlasterCompact,BlasterDagandBlasterCapstone, and all four capstones are pinned inAxiomCheck.lean.encode_sound: every root's output literal simulates to the DAG'sBitVec/Boolmeaning, under every assignment.compact_sound: compaction preserves every literal's value, for any hints. A wrong hint can only cost sharing.dag_refuted(anddag_refuted_raw): ifkernel.check_stepsaccepts a proof for the CNF thatencode → compact → map_word → tseitinproduces from a DAG, then no assignment makes all roots true.Output is unchanged
ordeal check --format jsonis byte-identical to the published v0.25.0 binary on all 24 queries. I re-checked this independently.cnf_gap_digestCNF digests match the phase-2 record, on corpora of up to 34 million clauses (agent-reported).Re-verified independently
lake build: 1724 jobs, 0sorry.cargo test --workspaceafter a forced rebuild: 244 passed, debug and release.lower_withwiring; it has exactly the shapedag_refutedcovers.Negative controls (agent-run): each one-line mutation in the kernel, with the model regenerated, fails the Lean build.
Addarm that callsblast_sub;x&!x=0fold;map_litdropping negation.Cost
Lowering is 1.1–1.55× slower on the bench queries, and 1.85× on the oracle corpus total. The reasons: a whole-query raw arena, two extra passes, and the builder's maps. Lowering is a small share of a solve, and mitigations are in
docs/design/query-cnf-gap.md.What is still trusted, stated honestly
dag.rs: the translation from term to DAG.DagWF: an assumed precondition that the builder meets by construction.canon,lowering, the sliver and the SMT-LIB/Verus front ends.Phase 4, v0.27.0, closes the DAG part. The certificate will carry the DAG, and
ordeal-lratwill checkdag_wfand re-encode it (check_query). That is the option (b) end state.rivet: TR-061, VER-061, VE-051, VV-108.
rivet validatepasses with 0 warnings.🤖 Generated with Claude Code
https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1