Repository navigation
Add executable Lean WHIR and checked list-binding composition - #551
Draft
kevaundray wants to merge 30 commits into
Draft
kevaundray wants to merge 30 commits into
kevaundray wants to merge 30 commits into
Conversation
Benchmarks: base against this PR, on one runner8198d0b merged into its base, against the base 392e187: each benchmark run in turns on one runner, base and PR 5 times each. A size is shown when it changed; a time or a peak memory when it moved the same way in every round and its median by at least 1% (the change is the median ratio, with the rounds' range). Threads shows the named configuration; BLAKE2sProver stages
PCS
leanXMSS
Prover stages
Every resultBLAKE2s
Prover stages
Fibonacci
Prover stages
Field and transpose kernels
Flock
PCS
leanSPHINCS
Prover stages
leanXMSS
Prover stages
|
kevaundray
marked this pull request as draft
October 8, 2026 08:07
kevaundray
changed the title
Collaborator
Author
Clarifying what is and is not provedAt The final
Further limits:
The transcript change follows the separate review request in #529 and proposed construction in #552. It should not be interpreted as a demonstrated attack on the older transcript. The concrete Rust bug reported by this formalization is the separate selector-validation issue in #565, not a transcript exploit. The remaining review priorities are to justify the exact DMV instantiation, identify a meaningful permitted adversary class and concrete primitive loss, and assess the implementation correspondence. “No |
…r-lean-strengthen-20261009
…r-security-20261010
Store executable digests and squeeze outputs as data behind csimp equalities, add the observed physical record-capture compiler, literal byte transport and current caller parser coverage, and derive the parser's call order, domain, proof bytes and empty hints from an accepted setup, receive, payload and binding replay (SpongefishCurrentAcceptedJoin).
…full-prefix BCS endpoint
…coverage The full current source program re-walks the opening over the replay events and authenticates every query batch with counted hash programs. A current root policy (cap Q(Q+1)) and the ported physical freeze give opening_cover, and reduction_full proves the reduction to the public good event. The endpoint full_knowledge_bound is conditional only on Refines.
…knowledge bound A per-coin builder reconstructs each opening packet's incoming caller data from the erased table (caller original, first-mention root captures, earlier packet answers, replies parsed from the packet history). On every ideal table where the public good event fires this gives the state path, so current_knowledge bounds native acceptance with public extraction failure by the sum over the four binding shapes of finalBound, and current_knowledge_bits gives 2^-lambda for per-shape budgets up to 2^(49-lambda).
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 13, 2026
…ks, PCS, collisions and the AIR link RecParts splits hrec: the parent's circuit holds a verifier of each child, certified checks reducing input claims to output claims. Where the parent's circuit is satisfied (which hrec now receives, as sat_tree_at's induction has it), a check lets a false input through with true outputs only on its event, and each check's outputs are later checks' inputs or openings of the child's committed witness, true off the PCS event (leanEthereum#551). RecParts.ins_ok: off those events every check's inputs are true; RecParts.least_ok: the least such events satisfy the premises for any claims. RecParts.hrec gives hrec off the checks' events, the PCS event and the collision event from the AIR link, the premise left: a child's AIR claims true on its committed witness give its circuit satisfied at the statement its parent's verifier reads. tree_sound_parts bounds the tree's failures by the sum of those fractions. A sumcheck is such a check: sumcheck_claim_agree (the input claim is bound before the first challenge with the hints as seeds) gives sumcheck_run_sound_at, which drops the premise that the input claim is false and bounds the oracles at which the test passes with a false input and true outputs (sumcheckFalse); sumcheck_part reads it as a check's event. The run's answer theorems take their instance premises at the vectors put in at one oracle.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 13, 2026
… an event and reduce the AIR link The design summaries now hold, per shape, the claims `Design::carried` takes from a statement of labeled words, the statement `Reduced::statement` exposes for labeled reduction outputs, each tier's `Design::fixed_claim` on labeled hints at zero and at differing heights, the edge layout, and once the scalars `bind_state` binds; `checkdesign` compares each with `Rec/DesignClaims.lean` on all 600 shapes, with kernel-checked mutations for every rule, and computes each fixed stack's variables instead of reading them. DesignClaims proves the exposed statement's claims are the reduction's outputs, the fixed stack's placement, that a fresh fixed term reads the child's own column, and the bound state and digest round trips. `Rec/Collision.lean` bounds an adaptive prover's compression collisions and near window collisions under a uniform oracle and derives `HashCRP`, `WindowCRP` and `RomAnswers` from them; `crEvent` bounds `crBad`, and `PcsBound` states leanEthereum#551's bound as the interface for `pcsBad`. `Rec/AirLink.lean` proves the AIR's row, public and bus claims on a committed witness give `Model.Sat`, the bus from its GKR products off a bounded draw event, leaving `ChecksGiveRows`; `Rec/TreeBound.lean` combines the bounds.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 13, 2026
…he AIR's challenges from a run and match leanEthereum#551's bound to pcsBad Run.lean: the run theorems take the honest instance, hints and true children as functions of the oracle fixed before the check's challenges (CommittedBefore, Run.committed_at, Run.sumcheck_committed and the like, draws_not_fixed). AirRun.lean: the bus's and the constraint batch's draws as a run's challenges after the commitment, the prover adaptive (busRun_frac, batchRun_frac), and tree_sound_run with no lens premise. PcsMatch.lean: leanEthereum#551's current_knowledge conclusion in its own form with a fiber-uniform map to its outcomes and pcsBad inside its event gives PcsBound (Pcs551.frac, pcsBound_of_551), and compress_fiber discharges the fiber premise for the ideal compression model read through an injective node encoding.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 13, 2026
…-to-end tree bound and reduce the AIR link to the honest instances A run's cr is now asked between two executions both off their execution's event, which every round theorem has. Run.cr_of_extract derives it from a causal, normalized prover whose rows the prefix binds output words the prefix fixed: a row whose input is first queried after the squeeze is a collision when its output is an earlier answer and otherwise a late hit on a target (Collision.LateHit, at most Q B / |V|^4, Edges.lateEvent_frac), charged per execution beside epsCR in tree_sound_exec. A later query hitting a word the prefix fixed is a collision only when that word is an earlier answer. AirLink.tree_sound_end takes the PCS term from leanEthereum#551 and states the tree's bound per child as D/|E| + leanEthereum#551's finalBound sum + epsCR + epsLate; Edges.tree_bound_deployed evaluates it (below 2^-19 for 2^10 nodes at leanEthereum#551 budgets 2^20, below 2^-7 at 2^32) and Edges.pcs_dominates shows leanEthereum#551's query term dominates. AirLink.ChecksGiveInst states the table sumcheck's input claim as the committed witness's honest sum and the bus GKR's roots as its honest products; checksGiveBatch_of_inst gives ChecksGiveBatch from it.
kevaundray
added a commit
to kevaundray/leanVM
that referenced
this pull request
Oct 14, 2026
…ights and make GKR layers RecParts checks Rec/Tries.lean: an outcome is an oracle per try with the compression oracle shared; an event at most an ε fraction of try i's oracle at every value of the other tries' oracles is at most ε of all outcomes (Bind.frac_fix_le), so whichever try the prover outputs fails on at most the sum of the tries' bounds (frac_pick_le, frac_pick_le_mul), and Edges.tries_bound_deployed folds it into the end-to-end bound: m / 2^7 at leanEthereum#551 budgets 2^32, m / 2^19 at 2^20. Rec/Heights.lean: Circuit::heights transcribed from Table::height_log (circuitHeights), proven to hold the rows (heightsHold_circuit), so checksGiveRows_of_tree drops HeightsHold. Rust tests compare height_log with the transcription and check, on a tree of one tier and one of two, that each circuit Tree::converge returns sits at its tier's heights holding its rows. Rec/GkrParts.lean: a radix-four GKR layer past the top meets RecParts.Ok.test off its sumcheck's event, a line event (at most 2|S| pairs) and a λ event (at most one λ) (Bind.layer_part, lineBad_card, lamBad_card).
This branch has not been deployed
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.
Summary
Adds the executable Lean WHIR model, root-fixed adaptive list binding, supported commitment-anchor mathematics, a real interactive reset extractor with original-statement checking and polynomial resource bounds, an adaptive ideal-compression coupling for the #552 byte duplex, and additive source RBR knowledge with a literal public-state predicate and frozen Merkle-query-log extraction. This is a proof-only draft, not a claim of complete deployed PCS or whole-VM security.
The proof checkout's historical Rust harness remains pinned to 10266a1. The DuplexRefinement, DuplexFraming and WHIRNativeSecurity mode model is pinned separately to the pre-#607 #552 transcript at ff6a275, historically deployed by the merge at f11f84f. It does not currently model the newly deployed #607 session-IV and raw-byte transcript. The historical file and callsite equality audit does not claim that later #599, #555, #607 or Aeneas preparation files remain byte-identical.
#607 at d3c7f9d9 changes more than interfaces. Source inspection confirms the reachable buffered compression core retains its role/counter semantics, while session derivation and initialization, public-instance placement, raw 32-byte roots, proof-of-work challenge/nonce/zero-work steps, final consuming digests and the NARG/hints wire all change. Native and Rows agree on their new session, root and proof-of-work byte encodings by inspection; this is not new runtime or kernel correspondence evidence, and Rows does not constrain exact hint-wire decoding/EOF. New source, framing, schedule and budget adapters are required before the historical native mode theorem, including its conditional 2^-42 endpoint, applies to that deployed transcript.
The new duplex documentation's Q^2/2^257 and protocol prose's choose(Q,2)/2^256 are not the justified whole-view min(1,(2Q^2-Q)/2^256) proved here. Neither smaller coefficient follows from this theorem. That is a proof-claim correspondence gap requiring its own correctly instantiated argument, not a demonstrated attack or a lower bound on #607 security.
Corrected adaptive ideal-compression coupling
The actual finite causal public-compression game now has an internally proved coupling certificate. The joint construction proves both marginals, handles cached and fresh adaptive primitive calls, couples the actual source stream, and bounds disagreement for unrestricted whole-public-view observers. The old external PublicRandomCompressionDMV premise and dmvLoss name are removed, not retained as aliases.
The justified clean-cutover loss is duplexModeLoss(Q) = min(1, (2Q^2 - Q) / 2^256). The earlier birthday-only coefficient was insufficient and has been corrected throughout the downstream observable, source, native, concrete-budget and ROM chains. A birthday subevent can still have a sharper coefficient; it is not substituted for the full adaptive mode loss.
Recomputing the previously capped conditional native endpoint with the corrected coefficient still proves 2^-42, not 2^-43. At Q = 2^60 and its published caller, family and resource caps, the exact recomputed rational is 5712480737351244866976450137972416606804377619 / 50216813883093446110686315385661331328818843555712276103168. This is a mathematical conditional inequality for the modeled unanchored event, not a usable ordinary concrete BLAKE2s security level or an automatically composed anchored Fiat-Shamir result.
Complete interactive reset knowledge endpoint
PCSRewindSource.complete_original_knowledge runs the actual prepare, legal reply collector, Gao decoder, lane reconstruction and original checker. Every returned word explains one common Root0 candidate, all 64 original family slices, every ordinary or strided point claim, and the literal saved commitment-time anchor. It assumes neither an honest-root equality nor a recovery oracle. A nearby malformed commitment can be recovered; withholding, malformed replies and wrong original claims are rejected. A gamma-zero regression demonstrates that a compressed false second-family claim is rejected by the original checker.
This endpoint is labelled interactive only. Its exact joint accepted-and-extraction-failed bound is 1/2^50 + 2^-s. The cutoff is not labelled a security level, and choosing s = 128 does not turn that sum into 128 bit knowledge security. This is not a Fiat-Shamir knowledge result.
Let kappa be the original verifier's acceptance probability, gap = kappa - 1/2^50, N the initial physical block length and d the initial query depth. For positive gap, the actual schedule uses ceil(8N/gap) * (d+2) legal collector rounds per attempt and ceil(8/gap) * s attempts. The checked upper bounds are rounds <= (8N/gap + 1) * (d+2) and attempts <= (8/gap + 1) * s. The executable accepts integer budgets; this analytic choice uses an acceptance-gap bound and does not claim to compute kappa.
PCSRewindSource.complete_original_resource connects the counted executable to the same result and discharges supported profile and redundancy requirements. It includes field operations, inversions under the stated field-operation cost model, unit prover calls, admitted literal reply words, preparation, original point and slice checks, and retained-record work. Physical root rectangularity, occupied-lane limits and the literal response-word admission bound remain explicit. Prover CPU time outside unit calls is not silently bounded.
The coin-free full-Root0 decoder has checked correctness and polynomial counted cost. It recovers a strongly supported word and checks every original family, point and anchor; its compiled example corrects one corrupted physical row. The additive characteristic-two protocol now has a checked literal-public-state RBR certificate: initial state zero, exact incoming-history transition fibers and final accepted extraction failure imply state one. Its predicate contains no hidden future challenge or following prover response, and rectangularity follows from the actual accepting model guard. This is our own additive proof, not an application of the WHIR paper's characteristic-not-two theorem.
Completed PCS-only RBR and extraction components
For prepared immutable original inputs with m <= 2^64 and points.size + 2 <= 2^64, the exact RBR round error is (17/32)^56 + 1/2^78. The round count is 1 + sum_i(folds_i + oodCount_i + 1) + tailCount, including the response-free final full-E draw. The checked unchanged PCS profiles have k <= 40 and maximal raw message length at most 5760 bits. The first raw message is gamma, six maps and lambda together; query messages retain all full E draws before position projection. The minimum raw message entropy is exactly 192 bits, PCS-only. Neither this error nor its query-dependent amplification is labelled a security level.
The public Merkle compression log feeds an actual preimage index and compact Root0 reconstruction. The earlier PCSBCSMerkleSourceRows.rawRoot0_eq_compactBaseOracle and pruned_opened_rows covered only leaf_words=occupied. The completed LeafImages, FullSourceTransport and root-cache transport now authenticate the full zero-prefixed image before dropping leaf_words-occupied scalars, matching production whir/verify.rs:404 and pcs/verifier.rs:51-52,121-123. Missing images stay explicitly unavailable; recovered nonzero padding is available but invalid. Cache identity is CV, height, leaf image width and occupied width. Accepted opened rows agree with their frozen source rows outside the stated primitive opening-bad event; honest availability is not assumed. The compiled real-BLAKE2s regression exercises padded source extraction, an actual opening, invalid padding rejection, unavailable images and cross-shape identity. There is no production change.
The executable public-log extractor captures the first recognized Root0 shape address before that node's answer and invokes the same Gao/original-statement helper on its strictly earlier ordinary records. A source scanner derives the conservative target cap M=Q*(Q+1), accounting for adaptive anchor references as well as opening source paths. Its separate Merkle extraction loss is exactly (Q^3+3Q^2-2Q)/2^256. That term alone is not the current deployed Fiat-Shamir extraction-failure bound, and no Q^2/2^192 hash-chain term is asserted for these source keys.
These component contracts alone do not establish deployed Fiat-Shamir knowledge. The actual duplex's raw history keys retain prover/nonce frames and squeeze counts, not previous verifier-answer values. Arbitrary child-prefix prequeries must remain admitted. Replay of latent ancestor draws and shared-query composition require their own adapter rather than a direct invocation of the book's explicit hash-chain compiler. The following endpoint supplies the historical modeled-source adapter; the current deployed composition remains separate.
The historical PCS-only public-source experiment now has a checked executable observer and straight-line extractor, not merely a recovery-selector existence theorem. PCSBCSPublicExtractor.failureObserver equals the accepted, publicly decoded original-statement extraction-failure event. Its exact random-compression bound is B*((17/32)^56 + 1/2^78) + min(1,(2B^2-B)/2^256) + (B^3+3B^2-2B)/2^256. B charges the complete attacker-plus-verifier ordinary and construction-path work, including rejecting traces; fixed public profile/layout/frame-boundary metadata, finite nonempty coins and the stated supported caps remain explicit. Actual byte recognition, first-root capture, hash-before-projection and all-original checking feed that endpoint. The counted public extractor includes parsing, history scans, getters and actual Gao/original checks. These are historical modeled-source results, not current deployed BLAKE2s knowledge security.
The anchored mixed attacker-prefix wrapper preserves the entire existing source view, freezes the root before its current point answer and handles earlier adversarial mentions and repeated groups. Its exact ambiguity term is remaining/2^124 under the aggregate source Counts cap. Cache-hit observations need not preserve draw-log order; the source join derives the needed set-membership and preimage equality outside the SAME already-paid physical Merkle alarm. PCSBCSPublicExtractorAnchor.extractAt_changed_claims_same_word proves equality of actual returned base-word arrays for arbitrary later claim sets sharing the retained anchor metadata and earliest prefix, under the explicit clean-anchor condition. This is not yet a complete current deployed anchored knowledge composition.
Current #607 hand-port adapters now derive ordinary session work, raw32 record and preanchor-header recognition, actual full-vector point sampling followed by the prover-value read, literal bounded mode output coordinates and earliest full-physical-image root capture. The ordinary primitive compiler observes typed reads, guarded draws and decoded hints, preserving reached rejection and exact query traces. The computable mixed compiler joins observed session derivation and initialization to cached current construction replies, proves real byte-source erasure and all-branch path work, and permits an arbitrary counted attacker prefix. Its initialized current byte-mode coupling loss is min(1,(2Q^2-Q)/2^256), with Q explicitly including prefix, session and construction-path work. Current schedule separation proves nonempty prover absorption between verifier messages and distinct full raw histories across those boundaries, including partially consumed output blocks. Raw hint decoding, poison/error identity, native PCS equations, Rows and Aeneas remain separate obligations.
The accepted current caller path is now joined to the public original list. A physical-mode compiler retains the actual seed, absorb and finalization chaining values beside the cached construction replies; from an accepted setup, prelude, commitment receive, payload and expected-record binding it derives record.context = capture pre.state rather than assuming a record or context equality. SpongefishCurrentAcceptedJoin.accepted_original then proves that the received record is among the raw-decoded candidates of the post-binding construction key, that the deterministic public parser's result equals the physical replay, and that every prepared original is in the public original list. The parser's call order, derived domain, reconstructed proof bytes and empty hints are consequences of the accepted replay: receive and binding are one accepted replay of the caller tape, and a hint-free replay accepted with unread proof bytes makes the same queries on its consumed prefix. Header validity and the received context's one-block pending-buffer bound are derived. accepted_original_next derives the post-binding query when the verifier suffix begins with a positive challenge draw, as the PCS opening does. Native PCS equation, proof-of-work and original-claim acceptance, the distributional source join and the basic full-prefix BCS knowledge endpoint for the deployed #607 transcript are not claimed.
The current native PCS opening after binding now has its acceptance adapter. SpongefishCurrentOpeningAcceptance walks the configured coordinate schedule over the actual byte cursor (query proof of work on a raw32 challenge and UInt64 nonce, grouped verifier draws decoded with the unchanged grouped E codec, the Merkle hint, prover replies in native order) and checks the anchored native equations (a kernel computation shows its call list equals the separately inspected OpeningLayout.schedule for all 56 production profiles at the deployed grinding), which are literally the historical AnchoredPhysicalAnchor.sourceVerify on the record's shape, point and value. accepted_opening_original proves that an accepted caller path followed by an accepted opening is one accepted replay of the caller tape and opening call list, that every ground query level's proof of work cleared on its actual challenge, that the anchored equations hold for the prepared original claims, and that this original is in the public original list of the post-binding key; the first-draw cursor guard is derived. The Merkle hint wire codec is an explicit parameter receiving the query positions and row width, as the native from_hint does; every theorem holds for any such decoder.
SpongefishCurrentSourceJoinProbability.native_ideal_bound composes that join with the initialized byte-mode coupling: for any property of the prepared original and source view, the real probability of whole native acceptance with that property is at most the ideal raw-oracle probability of the public original-list event plus min(1,(2Q^2-Q)/2^256). SpongefishCurrentRoundPackets defines the current basic full-prefix round packets (closed key history with the full absorbed prover prefix and no coin values, coordinate selected by a public frame-count classifier, same grouped decoder), proves they partition the raw keys, and proves the additive RBR hazard rbrError for every caller-data builder.
SpongefishCurrentOpeningProgram.fullProgram is the counted current source program followed by a public opening walk: after an accepted replay it re-walks the opening schedule over the replay's recorded source events (exactly one per call) and authenticates every query batch with the existing WHIRPhysicalVerifier.openRows hash programs, so the opening's Merkle hashes are now observations of the counted program (fullBudget adds a uniform public Merkle budget; the initialized byte-mode coupling applies unchanged). On the real primitive the walk returns exactly the native accepted opening, with every hashed input's compression plan in the primitive log (fullProgram_native). SpongefishCurrentRootPolicy.targets is a current root policy recovering construction coordinates from the public primitive log and collecting Root0 and every announced level root, with growth and the Q(Q+1) cap, and ports the historical physical freeze/admission.
SpongefishCurrentKnowledgeEndpoint.full_knowledge_bound is the basic full-prefix endpoint for the current transcript. Its real event is: the caller tape replays and the record binding verifies on the real primitive, the PCS opening is natively accepted (query proof of work, Merkle authentication of every query batch, anchored native equations), and the public straight-line extractor fails (Root0 frozen at its first-mention key, then the source extractor). Its probability is at most Q*((17/32)^56+2^-78) + min(1,(2Q^2-Q)/2^256) + (Q^3+3Q^2-2Q)/2^256 with Q = fullBudget (attacker work plus the charged verifier replay and Merkle work) and no hash-chain term. The reduction to a public good event or the complete Merkle trace alarm is proved (reduction_full), including opening coverage (opening_cover: an accepted opening that is not quiet against the frozen first-mention log of its root raises the alarm) and collisions (collision_alarm).
SpongefishCurrentKnowledgeFinal.current_knowledge discharges the remaining refinement obligation Refines, so the bound holds in the ideal-compression model with only static public premises (nonempty instance, caller prelude and payload call shapes, and a valid caller shape whose dimension, batch and rate match the profile). For every attacker coin and binding message shape, SpongefishCurrentRefines.builder reconstructs each opening packet's incoming caller data from the table with that packet erased: the caller original from caller-path answers, Root0 and every announced level root from first-mention captures (every packet history mentions them, so erasure does not change them), the tape from earlier packets, and the incoming replies parsed from the packet history with query rows and next-level oracles from the frozen captures. On every ideal table where the good event fires, one packet per schedule coordinate is exposed (every deployed coordinate has positive raw width, by a kernel computation over all 56 profiles), each reconstruction equals the literal incoming data, Merkle quietness against the frozen logs authenticates the opened rows, and the native opening equations with public extraction failure make the terminal state doomed, giving the state path. The bound for every received record is the sum over the four binding message shapes of the three-term bound. At the deployed 17-bit query grinding, current_knowledge_level gives at most B/2^49 when every per-shape budget is at most B <= 2^64, and current_knowledge_bits gives at most 2^-lambda for per-shape budgets up to 2^(49-lambda) (2^29 units: 2^-20; 2^39 units: 2^-10), with the four-shape union included and no grinding credit. Scope: the instance, tag, session IV, caller layout and Merkle hint wire decoder (an arbitrary parameter) are fixed before the attacker runs; caller-side proof of work and caller equations are not part of the event, which only enlarges it; each per-shape budget counts attacker work plus a worst-case charge for verifier replay and Merkle work that is not evaluated for deployed layouts; completeness of the opening model (acceptance of an honest prover) is not proved here. This is a knowledge error in the ideal-compression model, not a concrete BLAKE2s security level.
Executable paths that returned or retained a digest or squeeze output as a closure, recomputing earlier compressions at each use, now store computed values as data; each stored form is selected by csimp with a kernel-checked equality to the unchanged semantic definition.
The pinned primary book source also distinguishes hash-chain BCS from its basic full-prefix variant: the hash-chain query includes the previous verifier randomness, whereas the basic variant includes the whole prover prefix and omits the hash-chain Q^2/2^lambda error term and minimum-entropy condition. Current duplex histories preserve the whole absorbed prover prefix, not previous coin bytes, so the basic variant is the appropriate adapter target. This is a route selection based on the verified
remark:bcs-with-basic-fs, not an application of its knowledge theorem to current deployed code. The native acceptance/original-statement distributional join is now proved, and the basic full-prefix endpoint is proved, with Refines discharged, as SpongefishCurrentKnowledgeFinal.current_knowledge under static public premises only; no whole-system lambda is assumed.Deployed leaf/node shape invariant
Fresh upstream inspection at 3caf021 confirms that leaf/node hashing is untagged, but the deployed verifier fixes each phase's height rather than accepting a proof-selected path length. Native opening folds exactly the configured height and rejects missing or extra siblings and a wrong root at merkle.rs:346-385. Rows uses verifier-generated query-bit length and fixed low/top hashes with a root constraint at rec/verifier/mod.rs:253-282. Production full leaf images are additionally 512 or 384 bytes, versus 64-byte node inputs; omitted zero lanes do not shorten the image and zero-prefix caching is not domain separation. Exact source callsites and configuration lines are documented in the README.
An actual native upstream executable confirmed cross-shape untagged reinterpretation and rejection at the original fixed height. The release Rows node-as-leaf regression passed and its original-depth circuit rejects the shorter-tree interpretation. Future code must retain verifier-fixed height, image width and occupied width and hash/constrain exactly that height. CV-alone equality is not binding across arbitrary shapes or a justification for a digest-only extraction cache. This is not an observed deployed same-shape protocol exploit.
Caller statement-binding precondition
The full original opening statement must be fixed independently of its current batching challenge packet. Values come from earlier absorbed messages or the seeded public statement, coordinates from strictly earlier verifier coins or public constants, and offsets/selectors/shapes from the bound layout. The source-fiber obligation is that updating only the current packet's random-table entry leaves the caller statement and incoming public state unchanged. The record identity frame and anchor do not bind arbitrary external claims.
At historical PR #600 source 12eea88, every production native leaf, aggregation and matching Rows opening was traced. CPU uses cpu/reduce.rs:68-103 and rec/verifier/riscv.rs:63-79; recursion shares rec/proof.rs:217-245 with rec/verifier/recursion.rs:105-125. Terminal bus/table/Flock values are observed before opening, while coordinates are earlier challenges, not reserialized point vectors. Child statements are seeded limb-for-limb. Deferred fixed/program hints are observed in the separate reduction before its batching at tree/reduce/mod.rs:63-78; the final native checks or satisfied aggregation circuit must settle those obligations. No late unbound prover-selectable production claim was found. README gives the detailed source references. This audit does not prove shared-oracle causality, universal caller safety or Fiat-Shamir composition.
Anchor and deployed source boundary
The anchor mathematics fixes a supported candidate list before a fresh uniform point and allows malicious advertised values. Outside its explicit pairwise ambiguity event, at most one candidate satisfies the advertised anchor. The capped 2^-124 ambiguity term is not a whole-protocol security level.
PR #600 separately implements immutable original records and opening identity frames on typed Rust PCS APIs. Its published normal merge 75d4562 incorporates #607 and #608 from upstream d3c7f9d and migrates native and Rows frames to raw 32-byte roots, the original chaining value and normalized byte-buffer context under the session-IV and new codec API. The source versions are LVMP17, LVMT15, rv64im15 and tree12. Its actual public CPU and first/node tree prove/serialize/decode/verify smoke passed with native-to-Rows replay and legacy, foreign-statement, changed-output and truncation rejection. The proof checkout does not universally refine that source: the duplex chain remains explicitly historical pre-#607, and a session-IV/raw-root/PoW/final-digest adapter is needed. Existing physical and fresh-caller models retain explicit historical source and parser premises. Source changes and finite smoke agreement do not discharge Fiat-Shamir knowledge, full acceptance and rejection/error correspondence or compiler/runtime correctness.
The three historical malformed selector acceptances recorded at 10266a1 remain historical known gaps of that range-only guard, not claims about current upstream's stricter #599 typed guards. The independent Aeneas project targets actual verifier code and records unsupported primitives and extern assumptions rather than replacing the verifier with a proof-only clone.
Concrete cryptographic boundary
DuplexModeGame.concretePrimitiveGap_knownAnswer_lower_bound proves that the exact full-public-view ConcretePrimitiveGap is at least 1 - 2^-256 for Q >= 1 whenever Allowed includes the elementary fixed known-answer adversary and distinguisher. Ordinary efficient classes include that pair. Efficiency or collision resistance cannot justify a useful small loss for this replacement game. Arbitrarily excluding the observer is not used to manufacture a security assumption.
The concrete native inequality remains explicitly conditional, not ordinary computational security for deterministic BLAKE2s. This limitation concerns the replacement proof strategy, not a demonstrated cryptanalytic attack on BLAKE2s or the deployed protocol. No unconditional hash theorem, grinding amplification, complete deployed Fiat-Shamir knowledge theorem, whole-system lambda value or proved 128 bit whole-system level is claimed. The 192 bit challenge-entropy terms and 256 bit Merkle and compression-mode terms remain separate.
Verification and remaining hypotheses
Exact pinned tooling, reproduction commands, source drift and exercised checks are recorded in verification/whir/README.md. The final warning-denied library, Main and compiled-model closure passed, including every registered executable. Audit.lean checked 16213 exported Whir theorem declarations, including generated declarations, rejecting project axioms and every transitive axiom except propext, Classical.choice and Quot.sound. With digests stored as data, sixteen compiled scenarios completed within the bounded runtime invocation, including the current real-BLAKE2s adapter, the current record codec, the literal current caller reconstruction (previously stalled by closure recomputation), the captured source executable and the maintained model, reset/counting, source-stream, PCS grouping and real-BLAKE2s Merkle/public-log scenarios. The branch merges upstream 392e187 normally and changes no Rust outside verification/whir.
Actual compiled execution covers the multilevel accepted/rejected model, original reset and counted extraction, source-stream coupling, nontrivial full-root Gao correction, PCS grouped rounds and byte-cache resets, and real-BLAKE2s Merkle-query-log reconstruction with honest, tampered, missing, malformed and lane-order cases. An inconsistent-output record fixture checks collision handling without claiming a BLAKE2s collision. No sorry, admit, native_decide, unsafe proof tricks, mock oracle or new correctness axiom is introduced. The historical 71-group differential and six production query-batch checks remain explicitly historical, not universal refinement or evidence for changed upstream files.
The production-profile public extractor compiled and executed literal-original recovery, fake-prequery rejection, genuine first-root capture and full zero-prefix leaf decoding. Its Gao/original reconstruction did not complete within the bounded invocation after the general shared-nodal and shorter-left multiplication changes. That production-profile run remains explicitly not completed. The compiled smaller valid runForConfig helper from the same reconstruction path recovered eight nontrivial words with one corrupted row, checked fifteen common matches and rejected malformed root/anchor metadata, wrong originals and a changed anchor. This is not substituted production-runtime evidence. Kernel-checked value and polynomial-cost theorems remain the mathematical result; native CPU/allocation costs are not inferred from them.
Finite coins, supported public shapes and caps, first-registration semantics, attacker Counts before execution, reachable verifier budgets and terminal paths, free announcements and the backfill envelope remain explicit experiment hypotheses. The corrected ideal mode coupling no longer has an external unproved DMV certificate. Concrete cryptographic justification, the current Merkle hint wire codec, native CPU/allocation runtime correspondence and complete current Rust-to-Lean correspondence remain separate obligations. The current #607 knowledge bound holds in the ideal-compression model under static public premises; no concrete BLAKE2s, complete Rust-correspondence or whole-system Fiat-Shamir knowledge endpoint is claimed.