FV-frontier (b): Real-valued probability-monad quantitative bound (Pr[forge] ≤ ε)

The log-domain / bit-security half is DONE (Crypto/Quantitative.lean, mathlib-free, decide, axiom-free: cited bounds + multi-term floor min(143,112,96)=96 bits at the 2¹⁶ cap, cap proven load-bearing).

Remaining EasyCrypt-class piece: the actual Pr[forge] ≤ ε over a probability monad + a formal +C grinding treatment — needs mathlib (PMF/NNReal); do it in a SEPARATE mathlib-importing project so lean/ stays mathlib-free and fast.

Scope honesty (Tier-3 evaluation 2026-07-02): fully mechanized C10 EUF-CMA (extending the Barbosa'24 EasyCrypt SPHINCS+ development to the +C variant) is person-years and declared OUT OF SCOPE — the qualitative reduction stays cited-TCB. Keep this item scoped to the probability-monad bound, not the full EUF-CMA mechanization.

Migrated from docs/work-todo.md section FV-frontier follow-ups (surfaced 2026-06-16 — TxFlow repair + a/b/c session) (file retired 2026-07-19; original archived at docs/archive/work-todo-retired-2026-07-19.md).

PR #716 landed on master at d947c047 and supplies a checked intermediate probability result: for independently uniform digest draws, p = 22169393903687611906220091621190388 / 2^129, bounded exhaustion is (1-p)^B, and successful-event mass retains (1-(1-p)^B) times the conditioned event probability, with B=10000000. The actual consumer predicate/target bridge is proved.

This does not instantiate the deterministic SHA-256 counter search, establish shared-oracle/adaptive-history coupling, or produce the final deployed Pr[forge] ≤ ε bound. This issue remains open. Full certification and scope receipt; #100 owns the corresponding refinement work.

The bounded WOTS game probability bridge is now on master at 8f739990 through PR #718.

C10BoundedGame.bounded_win_le_total proves that the guarded bounded game's winning probability is at most the existing total WOTS game's for the same admissible, terminating adversary, including adaptive signing/hash-oracle requests. Failure is absorbing. This comparison has no IID or universal-search-success premise. C10BoundedReduction.bounded_interactive_D1 composes the existing conditional WOTS bound and explicitly retains N2 and its original collection-tweak well-formedness premise.

The fresh full pinned-image gate is GREEN: 68 files under both drivers, 67 controls, 1,339 pins, 1,208 statements, unchanged assumption census; Rust correspondence tests pass. Astra and Opus return GO with no findings, within the 15-minute bound. The Docker-interrupted run is retained as incomplete evidence. Exact source identities, raw gate and review receipts.

Keep this issue open. The next research boundary is an abort-restricted/member-aware reduction that removes N2 and composes through the hypertree, followed by shared-hash/adaptive-history/FORS truncated-R and numerical resource accounting. This batch establishes neither whole-scheme SPHINCS+C security nor real SHA-256 probability bounds. #509 remains deferred. Known broad CI baseline failures remain tracked separately in #660/#711/#717.

Landed the bounded member-aware WOTS batch via PR #726 on master at 044b3d200194687cb61b6d59984739169d451f67 (reviewed proof source 532c4b7a2b945566ce4e3b3247a9f50224883788).

C10BoundedMA.bounded_interactive_D1_MA bounds BoundedGame(A) wins by the existing WOTS-TW and member-aware S-TCR challenge probabilities, with no universal counter-reachability (N2) premise and no charged grind-failure summand. Accepted signing records witness reachability; the good-transcript event survives the coupling and collision split. Target cap, address separation, encoder bridge, member-aware collection separation and explicit adversary termination remain.

Evidence: 69 files pass direct compilation and CLI replay from cold inputs; all 70 controls pass. 57 roots / 1,347 declaration pins / 1,216 statements; assumption census unchanged. Astra and Opus returned GO within the single bounded wave; Kimi omitted under owner instruction. Input identity c8559f353fcd973902a9f5ad466b6f58 remained unchanged. Receipt.

This issue remains open. Next bounded slice: a failure-rejecting hypertree game/coupling and the reduction-specific collection/termination facts. Shared-hash/adaptive-history, FORS truncated-R accounting, useful reduction runtime and numerical challenge bounds remain research. This does not remove N2 from the old total games or close whole-scheme security. #509 stays deferred; unrelated baseline CI failures remain tracked in #660/#711/#717.

Landed bounded hypertree / actual leaf-reduction interfaces in master bd9b8a889da225238a52ca896b8fa1735262b9b4 via #727. Full cold pinned replay passes all 71 files through direct compilation and CLI iteration, with all 75 controls (exit 0). Opus GO; Astra found no issues and its sole pending-replay GAP is discharged on the unchanged reviewed source. Existing unrelated hosted CI baseline failures are documented in the receipt.

Closed in this batch: an option-valued NPRF hypertree signer with losslessness, successful-output agreement, d-layer output and exhaustion rejection; its failure-rejecting nonadaptive game and bounded ≤ total probability comparison; choose/forge termination and member-separation composition for the actual XmssmtCC_All leaf wrapper, instantiating the N2-free WOTS bound. No new project axiom or admit.

Remaining: these are two separate inequalities, not a whole-hypertree N2-free theorem. Prove a common failure-aware experiment through the precomputed signature cube and collision branches, accounting explicitly for which cube entries are covered by the signing paths. Then address real shared-hash/adaptive-history, FORS truncated-R, useful reduction resources and numerical challenge bounds. The model is manually linked and sampled-key, not a Rust extraction.

Banked review note: BoundedHypertreeGame.bad is local, so no observable exhaustion probability or reverse total-to-bounded inequality is exported. If a later result needs either, introduce an instrumented observable experiment with explicit privacy/coupling proof. This does not block the current bounded operational inequality. #509 remains the deferred owner-triggered combined assurance pass.

Exact source, proof logs, controls and review receipt.

Landed the remaining-research batch in PR #731, source 8d388d66123068b995827f76840b129d4491f4a9 and receipt commit d3e6dd0303888010ef1425355031b1e4c06fd058. Proof/review evidence and exact boundaries. All 78 proof files pass both drivers, all 90 controls meet their expected outcomes, and Astra/Opus returned GO. No new project axioms or admits; no production-security claim.

The checked conservative search theorem gives exhaustion at most 2^-305 when at least 9,994,240 of the 10,000,000 candidate inputs are fresh in the classical model. The adaptive R collision theorem assumes a cap on draws over the whole experiment, not per signature or per key. These are search/randomizer results, not a numerical forgery bound.

This issue stays open for explicit hash-query, signing-query and resource accounting in the actual reductions, a worst-case whole-experiment draw budget derived from per-key usage, and quantitative ITSR/EUF-CMA bounds. The current pure hash operators have no cost semantics. Expected rejection counts cannot justify a worst-case signing allowance. The illustrative arithmetic in the receipt is separate from the mechanized conservative bound and supplies no QROM or deployed SHA-256 claim.

Charge-free composition and the common stateful shared-hash simulation remain tracked in #100. No new mathlib dependency was added to the existing Lean tree.

#732 landed the accepted-history hypertree milestone and persistent raw-oracle foundations (master 1be79a0a), with a green corrected cold EasyCrypt gate and bounded Astra/Opus review. This removes the bounded theorem's grind-failure summand; it does not establish a numerical forgery advantage.

This issue remains OPEN. External, not-yet-enrolled research now checks keygen followed by adaptive R/H_msg grinding under one shared oracle/secret, with explicit physical-call and availability bounds. Availability is not EUF-CMA. The legacy uncosted ITSR game still admits a probability-one countermodel; a meaningful forgery bound needs actual costed reduction composition. No numerical security level is upgraded by this milestone.

#734 is merged at master 1abfc31. The EasyCrypt track now includes a manually transcribed adaptive complete-byte C10 experiment with persistent oracle history, explicit query budgets, fail-stop semantics, and a same-client secret-prefix hop.

The unchanged-source cold gate passed 163 direct and 163 default-CLI targets plus 113 controls; Astra ultra and Opus xhigh returned GO under the owner's standing reviewer substitutions. Full source-bound receipts are in docs/security/adversarial-review/findings/easycrypt-shared-byte-session-2026-09-23.

This does not close this issue's probability bound: the independent-game forgery probability remains on the right-hand side. The existing Lean arithmetic margin remains separate from an instantiated end-to-end EasyCrypt forgery theorem. Next work connects the actual byte game to component reductions and handles adaptive opening coverage. New fixed-prior-set and memoized-grind probability lemmas are checked external research only, outside the merged receipt.

PR #736 is merged to master at 38976ea50b0f79e083759feb33f43876504d2738. It adds accepted-output probability laws for the actual memoized complete signer and exact-coordinate replay accounting. The unchanged-source cold gate passes 184 direct targets, 184 default-CLI targets and 122 controls; bounded Astra/Opus review returned GO. The merge receipt is in docs/security/adversarial-review/findings/easycrypt-quantitative-foundations-2026-09-23/.

The accumulated adaptive opening argument and complete byte-model component reduction remain open; the residual forgery probability is still unbounded. Entry freshness/history and cached-query charges remain explicit. The next selected batch addresses live-session history and repeated contexts. No numerical end-to-end EUF, extraction, concrete SHA-256, QROM or production claim follows. Hosted CI has the separately tracked baseline failures #660/#711/#717; owner-triggered playbook pass #509 remains deferred.

Complete-session history and repeat accounting landed in PR #738, master b89a1b6. The unchanged-input cold replay passed 203 direct targets, 203 default-CLI targets and 133 controls; Astra and Opus returned GO. The source merge receipt records the remaining baseline hosted-CI failures separately.

Verifier-side raw authentication-path correspondence is now draft PR #744: ten modules and eleven new controls pass focused checks; both bounded reviewers returned GO, with the complete cold replay still required. This does not close accumulated adaptive opening coverage or the complete byte-model component reduction. Honest-tree construction is separate unfinished research. #509 stays owner-triggered and deferred.

Raw authentication-path correspondence landed in PR #744, master 78c6ad3. The unchanged-input cold replay passed 213 direct targets, 213 default-CLI targets and 144 controls; Astra and Opus returned GO. Hosted-CI baseline failures are recorded separately in the merge receipt.

The next construction batch is frozen at dd99b60: 53 modules supply actual builder/reference paths, FORS leaf/private provenance and signing/recovery equality to the internally computed root. All 106 focused checks and 24 new controls passed; the full replay and bounded review remain required. Later WOTS, forest and layer correctness checkpoints are checked but not yet enrolled or reviewed. Whole-signer composition and accumulated adaptive opening coverage remain open. #509 stays owner-triggered and deferred.

The construction, complete honest-signing, and probability-charge milestones are now merged through #745, #746 and #747. This issue remains open.

The manual C10 model now connects separate key generation to actual WOTS, forest, layers, signing, exact byte encoding/decoding and later verification. In the independent-oracle model, a returned honest signature is 4008 valid bytes and verifies against its earlier root; bounded signing failure remains explicit. The shared-oracle honest-error transfer supplies the checked 30520798 * 2^-256 upper bound for malformed or non-verifying returned encodings, excluding None.

Under the proved query-budget and module-scope premises, the same actual byte game now has checked public-node collision Q(Q-1)/2 * 2^-128, public zero-node Q * 2^-128, and secret-prefix Q * 2^-256 charges. Cached public calls remain charged. Invalid-sum WOTS recovery matching a reference leaf implies the public zero-node event. The remaining collision-free, zero-free successful-forgery probability is still explicit; this is not a closed numerical EUF bound.

Master is faa06863f908adf14c3f96150dc0fb5e16c6c290; reviewed source is a25c9122ac294bea966ac9ac7b909dc3dfb39514. The unchanged-input cold replay passed 371 direct targets, 371 interactive targets and 263 controls, exit 0 in 8996.59 seconds. Fresh bounded Astra and Opus reviews returned GO under the standing owner substitutions. Exact proof/review receipt. An initial review finding corrected the negative-control evidence description: rejected exact theorem applications do not establish that altered statements are false or that bound terms are necessary. Both rejected and valid proofs of a true weaker bound are retained in the receipt.

Next mathematical boundary: extract WOTS/FORS failure or exposed-opening events from arbitrary successful new-message byte forgeries; account for openings accumulated through later adaptive signing requests; charge the resulting private-preimage/guess/encoding events; compose them in one common initialized game. Manual-model/Rust extraction, concrete SHA-256 and QROM remain separate. No numerical deployed security or production authority is claimed. #509 remains deferred, and hosted CI remains red on the unchanged baseline failures #660/#711/#717.

The reverse WOTS/layer recovery milestone is landed in PR #748 (master ef9102f8e5c21c14558035306d8dc839420b786c; reviewed source 444c1d4aca22d7b676a0b64b4be1fc13881c813d).

Actual WOTS recovery matching a retained key now yields its reference-chain opening outside the already charged public-node collision/zero-node events. The proof records the real counter, 43 suffixes and compression input, including empty digit-7 suffixes. The verifier predicate uses the full u32 count domain and has a forward replay theorem; it does not impose the signer's ten-million search budget.

Actual Merkle-layer recovery composes that result. Actual key-generation leaf and Merkle-builder comparison harnesses supply the reference keys and paths, with probability-one termination statements. This removes an assumed WOTS opening in those component comparisons; the harnesses are not the complete byte-session forgery game.

Evidence: 384 direct and 384 interactive targets, 285 controls in the fresh full cold replay; 26 focused checks and 22 new controls. Astra and Opus returned GO within the bounded wave; Kimi remains omitted under the owner's standing instruction. No new project axiom/admit/clone assumption. The first replay was interrupted by the host crash and is not passing evidence; completed review artifact hashes were checked after reboot. Hosted CI retains the unrelated baseline failures tracked by #660/#711/#717.

Still open: arbitrary successful byte-game forgery to component reference openings; accumulation through adaptive signing; private preimage/guess and encoding-event charges; one initialized game and a nontrivial numerical bound. This component milestone does not close #100 or #295. Classical manual-oracle model only; Rust extraction, SHA-256 and QROM remain separate. #509 stays deferred.

Proof boundary · Source-matched replay/review receipt.

Batch BL is closed on master df4879e6e2540d377f86102cf50161ab0c6f85ab via PR #966. Keep #100 and #295 OPEN.

The manually transcribed FORS tree/sign/recovery and complete shuffled forest now compile into the separate shared-cache PMF interpreter. Compiler equalities retain exact private/public bytes, actual stack merges, authentication overwrites, ordered recovery, full-digest sub-seed derivation, four blocks and the computed twelve-position shuffle. The forest actually recovers each signed tree and stores by natural index. The thirteenth root is transmitted as the final secret and separately hashed for its compression slot. The full output and memo table survive every stage, for arbitrary initial history. Array lengths/bounds and independent bytes/query-order/cache/last-role witnesses include complete cached executions.

Executed geometry proves 2048 leaves and 2047 merges: tree/sign use 6143/6144 total and 4095 public calls; recovery uses twelve calls. Full forest signing has at most 80022 total / 53386 public calls, including cached calls and shuffle branches; recovery uses 146. Prefix event error is 4095/2^256 per tree/sign and 53386/2^256 for forest signing, with an independent uniform hidden secret and empty initial tables. Conservative empty-cache selected-collision-or-raw-zero charges are 18871296/2^128 for a tree, 18877440/2^128 for tree signing, 3201800253/2^128 for forest signing and 10731/2^128 for recovery. Arbitrary-history compiler equalities do not discharge those probability premises or make repeats fresh.

Validation: 156 new / 1017 total theorem closures; 511 typed cases / 1533 compiler jobs (448 semantic rejections, 63 equivalents), closure canaries, seven local gate groups, exact source scan, actual PR/push checkout-tree checks and postpush audit. All 861 old statements, 440 fixture objects, old proof-module bytes and 30 old bindings are preserved. RawForest.ec and hypertree.rs bring the binding total to 32, with push/PR enforcement. The 71 new cases passed 213 focused jobs, and all 67 semantic rejection diagnostics match the fresh final replay. Opus returned GO. Astra returned GAP for the then-pending full control suite, combined audit and exact PR/push CI, with no source blocker. The coordinator checked the disclosed source-coverage limits and authenticated the completed local suite/audits and exact PR CI before landing. Actual postpush evidence is required separately. Raw verdicts and coverage limits are retained; no additional model wave was used.

The local full gate and current PR/push probability workflows ran freshly on the final corrected snapshot. One original tag-control diagnostic did not reduce a string conversion: that diagnostic is uncredited, the literal-byte consumer now proves the mutant false, and a tested classifier guard rejects non-reducing diagnostics. The obsolete initial control run was deliberately stopped, not counted as a complete gate. The scanner correction permits only the exact public ForestAccess source checksum at its exact field/path; all 32 scanner controls and the full source scan pass. Earlier EasyCrypt 2931-job and main/extracted correspondence evidence is reused only under exact identities, retaining the BC wrapper-source exception and its regeneration/native/kernel receipts. No pending or cancelled workflow is called successful.

Remaining: full hypertree/C10 keygen/sign/verify client, WOTS outer sub-seed preparation, session/node-cost/output/forgery composition; reverse-chain/FORS probability components; repeated-grinder freshness; concrete backend and cross-language correspondence. No new universal tree/forest build/recover correctness, axiom, native evaluator or imported EasyCrypt theorem. Runtime panic/retry, callbacks/erasure, concrete SHA, QROM, physical execution and shipment remain outside this result. Main lean/ remains mathlib-free; #509/#789 remain deferred.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-fors-forest-20261017/closure. Probability result SHA256 e93ad2a0df7cb33fc81736ab851763d0e6031a37b8bd5d09c456b24656f70441; review manifest bbc1b519938303fcb3a85c5aa8ea66fce60f56bbbfe740cf7fad5c8ca75dc3fc; postpush audit fa62c16348d8a0422f5a3d8e2f386a5388b409253e9dc8bbec58c96c3fbd90ee.

Batch BM plan — complete C10/hypertree PMF clients, following closed BL PR #966. Baseline df4879e6e2540d377f86102cf50161ab0c6f85ab / tree 3ed4b88edb86efc5e5692980c5f8f3bb199eaf90. BL postpush workflows, published receipts and all216 preserved canonical file hashes were independently verified.

Five related slices: (BM1) shared-label WOTS recovery, exact layer labels/coordinates/signature fields; (BM2) actual subtree-build/sub-seed/WOTS-sign/reconstruction layer and failure; (BM3) actual two-layer finish, R-grind signing, keygen at layer1/tree0, and H_msg/forced-zero/full recovery verification; (BM4) derived raw/public/selected budgets, physical relabelling, explicit probability premises and independent byte/order/failure/cache witnesses; (BM5) typed controls/inventory/bindings, mandatory combined gates, single fresh Astra ultra/Opus5.5 xhigh wave, exact CI and guarded normal landing/postpush/publication audit.

Preserve1017old statements,511fixtures,32bindings and old module bytes. Counts include cache hits and every branch; no fresh/independent-call or build-root-equals-recovered-root assumption. Terminal zero bytes in wots-0/wots-1 labels, bit143/18-bit hypertree extraction, both 9-bit coordinate shifts, full32-byte count input and retained exhaustion cache are load-bearing. All future probability transfers keep their independent-hidden-secret and empty-table/domain premises. One physical oracle is retained through all continuations.

Scope is the separate mathlib project and necessary gate/owner updates. No production Rust/EC/main/extracted source changes. Structured signature clients do not claim the4008-byte parser/serializer bridge, universal honest correctness, adaptive session/output/forgery composition, repeated-grinder freshness, concrete hashes/backends/cross-kernel/Rust execution, callbacks/erasure, QROM or hardware. #100/#295 stay OPEN; #509/#789 stay deferred. Review after the combined five-slice candidate; no per-slice review or extra agents.

Plan and source/evidence identities: /home/nicola/.local/state/pqsigner-research/easycrypt-hypertree-client-20261017/plan.json and development/owner-inputs.json. Existing authorization covers research and normal guarded publication; no irreversible action.

Batch BM is closed on master d31d3cfadea46538da4fb6b7df051c49357a772d via PR #967. Keep #100 and #295 OPEN.

The manually transcribed complete structured C10 keygen, signer and verifier now compile into the shared-cache PMF interpreter. Layer signing builds the authentication path, derives the actual seven-byte-label WOTS sub-seed, signs, and reconstructs the root. The complete signer runs the two-query R/H_msg grinder, forest and exactly two ordered layers; it preserves all returned fields and accumulated cache on success or exhaustion. Keygen builds layer1/tree0 using the high128-bit public digest. Verification recomputes H_msg, checks the forced-zero field, recovers the forest and both layers, and compares the entire padded root. Natural counters use full32-byte encoding; returned counters are proved below the supplied u32 cap. Signature list lengths and coordinate/read bounds, finite byte/order examples, constant-cache success/rejection and actual conditional first/second-layer failure equations are kernel checked.

Executed signing budgets are 2m+2n+435044 total, m+2n+364290 public and m+435042 selected calls. Verification has at most361 total/358selected calls; keygen has177151total/155135public. Caps m,n are at most2^32, with10,000,000 deployed. Prefix event error is the public budget/2^256 under independent uniform hidden secret and empty tables. Empty-cache node-event charges are (choose(m + 435042, 2) + 2*m + 2*n + 435044) / 2^128 for signing, 64264 / 2^128 for verification and (choose(177151, 2) + 177151) / 2^128 for keygen. Costs count cached calls; they do not imply independence, fresh repeated trials, honest correctness or a forgery bound.

Validation:143new/1160total theorem closures;609typed cases/1827compiler jobs (540semantic negatives,69equivalents), closure canaries, seven local gate groups, full source scan and actual PR/push checkout-tree/postpush audits. All1017old statements,511fixture objects,old proof-module bytes and32old bindings are preserved. RawLayer.ec,RawSigner.ec,KeygenExhaustion.ec andRoleGrind.ec bring bindings to36 with push/PR enforcement. All294focused jobs and their92semantic rejection diagnostics match the complete fresh replay. Astra ultra and Opus5.5xhigh both returned GO with no source findings in one simultaneous bounded wave. Astra retained the exact PR/push CI requirement. Opus did not independently replay the compiler suite; the coordinator authenticated the completed local proof/control evidence and exact scanner-only reuse. Exact PR CI is required before landing and actual postpush evidence separately afterward. Raw reports and their limits are retained.

The local full proof replay executed on the initial frozen proof/control snapshot and was reused only across a scanner-only correction after exact Git/proof-input equality. Current PR/push probability workflows ran freshly. Four scanner exceptions permit only authenticated public source-file hashes at exact fields/path;48controls prove exact acceptance and changed path/field/value rejection. A reproduced stuck-typeclass control diagnostic is uncredited; the corrected consumer fails semantically and the strengthened classifier rejects that invalid diagnostic. Earlier EasyCrypt2931-job and main/extracted correspondence evidence is reused under authenticated unchanged identities, retaining the BC wrapper-source exception and regeneration/native/kernel receipts. No pending or cancelled workflow is counted successful.

Remaining: adaptive full C10 session, session node cost and successful-output/forgery partition; a final forgery PMF bound and reverse-chain/FORS probability reductions; universal honest sign/verify correctness in this manual PMF model; repeated-grinder freshness;4008-byte codec composition, concrete backend and cross-language correspondence. Constant-populated-cache witnesses permit inconsistent nodes and are not honest correctness or fresh probability proofs. No added axiom, native evaluator or imported EasyCrypt theorem. Runtime panic/retry, callbacks/erasure, concrete SHA, QROM, physical execution and shipment remain outside this result. Main lean/ remains mathlib-free; #509/#789 remain deferred.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-hypertree-client-20261017/closure. Probability result SHA256 9c150da6a890011b6658d563ba0053cd8bc09bbfcaa4037dc1e68ce73e1cb9fa; review manifest 5cedfbedd5998f18bef8b37aa4c03e132c468040506342dff4b437096a7edf15; postpush audit f3186ed93277caf29bd88a5d0d6ce84d41d0e18d4f919217905f35dd6d018796.

Next bounded research batch BN: adaptive structured C10 session in the separate mathlib PMF project, based on master d31d3cfadea46538da4fb6b7df051c49357a772d (BM/PR #967 fully closed).

Five related slices: (1) finite reply-dependent hash/sign client and exact admission/cache semantics; (2) remaining-cap raw/public/selected budgets and state invariants; (3) guarded fresh-message verification and initialized keygen/game event transfer; (4) branch/exhaustion/ledger/cache witnesses; (5) typed controls, preserved census/bindings, mandatory gates and one combined review/landing boundary.

Keep existing 1160 theorem statements,609 controls and36 bindings. Hash calls remain available after signing failure; refused calls consume neither cap nor oracle, admitted exhaustion consumes one signing cap, and only successful signatures enter the message ledger. Physical R queries remain in the selected-node budget.

This is a manually transcribed finite structured session over an ideal memo oracle. The successful-output/forgery partition, full forgery bound,4008-byte codec,unbounded adversary correspondence,backend/Rust equivalence and hardware claims remain open. No production or EasyCrypt source changes.

Authorized Phase C under the existing interface/authority contract. Phase D: combined fresh PMF gate and unchanged-input audits, exactly one simultaneous fresh Astra ultra + Opus5.5 xhigh review (owner override;900s/800words/16MiB each;no Kimi), exact CI, guarded normal master push and actual publication/root audit. Deferred #509/#789 remain deferred. Local plan: easycrypt-adaptive-session-20261017/plan.json.

Batch BN is closed on master 079d5acffa5845dcb5e26b840e67ea7fa0727aee via PR #968. Keep #100 and #295 OPEN.

The finite adaptive structured C10 session now compiles into the full shared-cache PMF interpreter. Hash/sign admission uses actual remaining caps, separately from attempted-interaction fuel. Refused requests touch neither cache nor caps. Every admitted signing attempt consumes one cap, including exhaustion; exhaustion prevents later signing but leaves raw queries available. Successful signatures append the message without erasing previous entries. Final verification checks nonfailure, 32-byte message, structured signature shape/u32 counters and ledger freshness. Keygen supplies the actual public seed/root and retains its cache through the adaptive session and final verifier. The compiler-only key-width guard is proved redundant on actual keygen support.

Initialized budgets are T = qr + qs*(2*m+2*n+435044) + 177512, P = qr + qs*(m+2*n+364290) + 155496 and N = qr + qs*(m+435042) + 177509 for total, public and selected physical calls. R inputs remain selected. The physical node-event charge from an empty cache is (choose(N,2)+T)/2^128. For an independent public-seed/adversary sampler, uniform hidden secret and empty tables, real returned-event error between the initialized shared and independent-interface games is at most P/2^256. The forgery-transfer inequality retains the independent game's forgery probability as an unresolved term.

Validation: 64 new/1224 total kernel-only theorem closures; 669 typed cases / 2007 compiler jobs (596 semantic negatives, 73 equivalents); closure canaries; seven local gate groups; full source scan; actual PR/push checkout-tree and postpush audits. All 1160 old statements, 609 fixture objects, old proof-module bytes and 36 old bindings are preserved. FullSession.ec and RawSignature.ec bring bindings to 38 with push/PR enforcement. The 180 focused jobs, including 56 semantic rejections and 4 equivalents, match the fresh replay. Astra ultra and Opus 5.5 xhigh returned GO with no findings in one simultaneous bounded wave. Astra retained the exact PR/push CI requirement. Opus did not independently replay Lean or inspect every rejection diagnostic; the coordinator authenticated the fresh complete gate and all new semantic diagnostic matches. Actual PR CI is required before landing and actual push evidence afterward. Raw reports and their limits are retained.

The full PMF replay and current PR/push probability workflows ran freshly on this exact candidate. The unchanged scanner configuration, 48 controls and earlier 2931-job EC/main/extraction evidence are authenticated through exact source/toolchain receipts, retaining the BC wrapper-source exception and regeneration/native/kernel receipts. Initial fixture extraction, ambiguous typeclass diagnostics and unsuccessful equivalence checks are uncredited; corrected final fixtures pass their intended checks. No pending or cancelled workflow is counted successful.

Remaining: successful-output/forgery partition, final forgery bound, arbitrary lossless/unbounded-adversary representation, universal honest correctness, 4008-byte PMF codec, repeated-grinder freshness, concrete backend and Rust/cross-kernel correspondence. Populated constant-cache witnesses are not fresh-oracle probability or correctness claims. No new axiom, native evaluator or imported EasyCrypt theorem. Runtime panic/retry, callbacks/erasure, QROM, physical execution and shipment remain outside this result. Main lean/ remains mathlib-free; #509/#789 remain deferred.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-adaptive-session-20261017/closure. Probability result SHA256: f347549bf1e915a94318cccfac73f0f215829fd6291061095d48af3d93a06c5f; review manifest: 094a8a5a27a22be943f7873b5efcd2bc6fe26d69f5b9839f1ec492766ac7cd56; postpush audit: 242d38f5e321b75ee8bd0e3e960d1d1473f6afff5bcb97c7091f7c9d9eaa0103.

Batch BO plan — observed adaptive-session and successful-output witnesses, based on master 079d5acffa5845dcb5e26b840e67ea7fa0727aee. Batch BN / PR #968 is fully closed: actual PR and push CI, publication audit and coordinator checkout observation passed. #100 and #295 remain open.

The current PMF game keeps a Boolean and the successful-message ledger. The next forgery partition needs the actual returned signatures, forwarded client queries and final forgery tied to the same final memo history. This batch will add a passive observed interpreter and prove exact erasure to the existing session and initialized game; no observation may alter admission, replies, caps or final verification.

Five bounded slices:

Lookup-only replay of an executed query program in its final cache, with persistence, determinism and composition.
Actual successful signing exposures and admitted client hash inputs, preserving duplicates and proving ledger/cap/width accounting.
Observed final verification and initialized keygen, with exact output/cache erasure and initialized event equality.
Same-final-cache signing/keygen/verifier support and successful H_msg/root-reconstruction witnesses for the actual forgery, with finite branch and cached examples.
Typed semantic/equivalent controls, claims/source bindings and CI coverage, mandatory combined validation, review and publication closure.

Preserve all 1224 prior theorem statements, 669 fixtures, 38 bindings and old proof-module bytes. Use independent pinned dependency/cache copies. Keep production Rust, EasyCrypt implementations, main mathlib-free Lean and extracted sources unchanged. The complete six-case forgery partition, final numerical bound, universal honest correctness, repeated-grinder freshness, unbounded-adversary representation and codec/backend/Rust correspondence remain explicitly open.

The combined candidate is the next Phase-D review boundary: one fresh simultaneous Astra ultra and Opus 5.5 xhigh CLI wave under the existing 900-second/800-word/16-MiB bounds; no Kimi or added reviewers. Require exact PR CI before a guarded normal master push, actual push CI and published/root closure afterward. #509/#789 stay deferred. Plan and evidence: /home/nicola/.local/state/pqsigner-research/easycrypt-session-witnesses-20261017.

Batch BO is closed on master 7793ff5725e93c58eba10603ac588b69c629dd72 via PR #969. Keep #100 and #295 OPEN.

The passive observed interpreter retains actual successful signing request/signature exposures, admitted client hash inputs and the final forgery, preserving chronology and duplicates. Refusals are not logged; admitted exhaustion consumes its cap without creating a successful exposure. Exact session/game erasure preserves outputs and complete caches. Lookup-only replay is derived from executed support and persists under cache extension. Winning observed outputs jointly retain actual keygen/root, signing exposures, query replies, ledger/cap accounting, message freshness and verification in the same final cache. H_msg, forest and ordered layer reconstruction preserve rejected WOTS zero branches and signature defaults.

Initialized returned-Boolean erasure inherits the existing shared/independent error bound under its independent uniform secret and empty-table premises. No cache-visible event comparison is asserted; the independent forgery probability remains unresolved. These witnesses supply the history dependency for the remaining six-case cryptographic partition and final numerical bound.

Validation: 81 new / 1305 total kernel-only closures; 725 typed cases / 2175 compiler jobs (648 semantic negatives, 77 equivalents); closure canaries; seven local gate groups; source scan; actual PR/push checkout-tree and postpush audits. All 1224 old statements, 669 fixture objects, 38 bindings and old proof-module bytes are preserved. Six added exposure/client-query source bindings bring the total to 44 with push/PR enforcement. All 168 new development control jobs match the fresh replay. Astra and Opus both returned GO with no findings. Opus did not independently rerun compilation or controls; the fresh exact-candidate gate and diagnostic audit cover that execution gap. Astra required actual PR/push CI, enforced at the prelanding and postpush boundaries.

Local and actual PR/push probability replays ran freshly. Unchanged scanner configuration/48 controls and earlier 2931-job EC/main/extraction evidence are authenticated by exact source/toolchain receipts, retaining the BC wrapper-source exception and regeneration/native/kernel receipts. Failed exploratory compiles and two replaced control baselines are uncredited. No pending or cancelled workflow is called successful.

Remaining: full cryptographic forgery partition and numerical bound; arbitrary lossless/unbounded-adversary representation; universal honest correctness; 4008-byte PMF codec; repeated-grinder freshness; concrete backend and Rust/cross-kernel correspondence. Populated-cache examples establish no empty-cache success probability. No new axiom, native evaluator or imported EasyCrypt theorem. Runtime, QROM, physical execution and shipment remain outside this result. Main lean/ stays mathlib-free; #509/#789 remain deferred.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-session-witnesses-20261017/closure. Probability result SHA256: c608b7903a8de4678a2e38bac712126e2db54f9733727aea2b57ea9bdc00bf94; review manifest: 963700b1a64459cfe0672df297c26cc2f9a9cd065719d70ef3062eb7fc795408; postpush audit: 6430e22b24da9601a35bf86262f209a6bf1aa10a9585e88e436dfacf89f8f939.

Batch BP plan — actual tree-reference and recovery binding

Baseline 7793ff5725e93c58eba10603ac588b69c629dd72 / tree 35765f71b09281197eb13057bce83bead2081ce2; BO postpush and publication/root audits passed.

Derive reference leaves and authentication paths from the actual memoized tree builders, then bind successful recovery at the same coordinate to those references or an explicit node collision. Apply that fact to the actual keygen root and winning verifier output. Retire the missing tree-reference/path-binding dependency of the forgery partition.

BP1: Generic tree replay certificates derived from the actual indexed merge/tree loops, retaining leaf execution and pair lookups in one final cache.
BP2: Reference paths for complete Merkle/FORS trees, with proved coordinate/height ordering and cache-extension persistence; instantiate actual builders and keygen.
BP3: Input child injectivity and reverse recovery binding for actual Merkle/FORS paths, including defaults, fixed coordinates and selected public-node collisions.
BP4: Actual winning-output top-layer binding to the keygen reference leaf; explicit collision/zero alternatives and finite counterexamples demonstrating required premises.
BP5: Typed controls, complete claims/inventory, relevant source bindings and enforcement, mandatory combined gates, exact review and actual landing/publication/root audit.

Preserve all 1305 prior statements, 725 cases and 44 bindings. Certificates must come from executed builders; cache and coordinate identity, defaults, collision alternatives and WOTS zero branches remain explicit. No production changes or new axioms. Full forgery partition/bound and implementation correspondence remain open.

One combined review boundary after per-slice evidence: mandatory fresh gates, owner-authorized Astra ultra / Opus 5.5 xhigh wave, actual PR/push CI and publication/root audit. #509/#789 stay deferred. Detailed plan: /home/nicola/.local/state/pqsigner-research/easycrypt-tree-binding-20261017/plan.json.

Batch BP is closed on master 7aad6c998306b36ff6cb1e9b2ba12475680c68bb via PR #972. Keep #100 and #295 OPEN.

Actual indexed merge/tree programs now supply recorded Merkle/FORS root certificates, retaining leaf replay and ordered parent lookups. Every later valid coordinate has a derived reference leaf and path in the same final cache. The actual Merkle and FORS recovery programs preserve sibling defaults and truncation; fixed-width child/secret input injectivity binds recovery to an actual WOTS leaf or private FORS derivation unless the selected public cache has a node collision.

Winning initialized independent-game outputs now yield selected-node collision, public zero, or a jointly linked top-tree opening. H_msg, forest/lower/top recovery, actual keygen WOTS leaf, count digest and padded-root equality remain linked. WOTS count acceptance follows only after zero exclusion. This is a structural dependency, not yet a new-message WOTS attack or its numerical charge.

Validation: 76 new / 1381 total kernel-only closures; 783 typed cases / 2349 compiler jobs (702 semantic negatives, 81 equivalents); closure canaries; seven local gate groups; source scan; actual PR/push checkout-tree and postpush audits. All 1305 old statements, 725 fixture objects, 44 bindings and old proof-module bytes are preserved. Eight new source bindings bring the total to 52 with push/PR enforcement. All 174 new development control jobs match the full replay. Astra and Opus both returned GO on the corrected snapshot, with no findings. The reference-deletion control now consumes the jointly linked reference leaf. Both reviewers explicitly left full local/CI execution to the mandatory gate receipts; their GO is source-stage only.

The local probability replay ran freshly on the exact corrected snapshot, including the strengthened reference-deletion consumer; no local probability replay is reused for this correction. Actual PR/push probability replays ran freshly. All 52 scanner controls ran freshly; the earlier 2931-job EasyCrypt replay plus main/extraction evidence are authenticated by exact source/toolchain receipts, retaining the BC wrapper-source exception and regeneration/native/kernel receipts. Failed exploratory compiles and control fixtures remain uncredited. The CI envelope is 60 minutes; all checks and compiler limits are preserved. No pending or cancelled workflow is called successful.

Remaining: WOTS chain openings/new-component distinctions, lower-layer/FORS descent, adaptive coverage/private-opening charges and the full six-case partition/final numerical bound; arbitrary lossless/unbounded-adversary representation; universal honest correctness; 4008-byte PMF codec; repeated-grinder freshness; concrete backend and Rust/cross-kernel correspondence. Populated-cache examples establish no empty-cache success probability. No new axiom, native evaluator or imported EasyCrypt theorem. Runtime, QROM, physical execution and shipment remain outside this result. Main lean/ stays mathlib-free; #509/#789 remain deferred. Legacy statement-pin boundary issue #970 is banked separately; BP's new pins remain within their declarations.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-tree-binding-20261017/remediation-closure. Probability result SHA256: 58e969cf226d0ab13627620ac6c3631d4966a0554ea17f0333802f3dcec66633; review manifest: b65437877746abfc627cdf50de801aa00f6f7a2f2ffc04d6687b367da697c654; postpush audit: 3ceb7c1ef9c6951749239a9493b9aa392135f377b240ab6a9cce981275c93eb3.

The reference-deletion regression now consumes the opening and projects its linked H_msg/recovered-WOTS/keygen-reference leaf, addressing #971. Counts and all theorem statements remain unchanged.

The first post-push CI attempt was cancelled by the master-branch concurrency rule after an unrelated hardware-document push. That single CI workflow was rerun successfully at the same landed commit after other master CI finished; the probability replay and other workflows were preserved. The cancelled attempt and successful rerun remain separately recorded.

The WOTS chain-binding batch is landed in 4c2d33f9932aeb54a14deb08b568aa1794b4b9d2 via PR #973.

Accepted top-tree recovery now binds all 43 submitted WOTS values to actual private-seeded prefixes in the final cache. Successful signing exposures retain joint randomizer, forest and ordered two-layer witnesses, including their actual accepted counts and chain values. At a common address, accepted words give equal values or an earlier position with a suffix to the signed value.

Validation: 17 new modules, 67 theorems and 21 finite examples; fresh full local replay and actual PR/push CI pass with 1,448 theorem closures and 830 typed cases / 2,490 compiler jobs. The 47 new cases include 43 semantic rejections and four equivalent controls. All prior 1,381 statements, 783 fixtures, old proof-module bytes and 52 manual source bindings are preserved. Fresh simultaneous Astra (gpt-6-astra ultra) and Opus (claude-opus-5-5 xhigh) reviews returned GO with no source findings. Their explicit execution-evidence gaps are retained and require the separate gate/CI receipts.

The existing EasyCrypt replay and main/extraction evidence were reused only after exact dependency/toolchain/source authentication, preserving the documented BC wrapper-source exception. This batch makes no EasyCrypt-to-Lean or Rust correctness theorem. Scanner, freshness, source pins, workflow enforcement and workflow linters passed for the candidate.

Still open: minimum exposure across repeated addresses; lower-layer/FORS descent; adaptive coverage/private-opening charges; the complete six-case PMF partition and final bound. An earlier position need not be undisclosed, and equal words need not mean equal messages or full digests. Universal honest correctness, arbitrary lossless/unbounded-adversary representation, the 4008-byte PMF codec, repeated-grinder freshness, concrete backend/cross-kernel/QROM and physical claims remain outside this result. #100 and #295 remain open. #509/#789/#970 remain deferred.

Local receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-wots-chain-binding-20261017/closure. Full PMF result SHA-256 d14a22baf43e52f8eaa2d24609f430353d4742170155c652113f8a810e124fd8; review manifest 429ccfae9e0a3faf62b75f2258de2b27509ede48446535f19588fb94a295cedb; actual postpush audit 1b85a262d68de5bdd4e20b11530c3ab23833644510ca37dcf017707acb62f131. The root audit separately verifies publication readback and preservation of the unrelated canonical checkout.

Batch BR landed in PR #977, commit f2461dd060b77afe3110516119e1e1efc2a5cf06. The separate Lean PMF project now derives correctness of the actual returned Merkle/FORS authentication arrays from their stack-loop collection, then connects them to actual recovery and cache extension. The FORS signing result also ties the returned secret and path to that execution's root. Forward correctness uses functional cache consistency, with no collision-exclusion or assumed reference-path premise.

Evidence: 57 new theorem closures (including 10 finite examples); 1,505 total closures; 870 typed cases / 2,610 compiler jobs, including 40 new cases (36 negatives, four equivalents). The full local replay passed and was reused across integration only after exact PMF-input/toolchain equality; actual PR and push probability CI also passed. Existing statements, fixtures and all 52 bindings were preserved. All applicable current CI workflows passed, including extraction; all six other local gate groups, 92 scanner controls and the final source scan passed. The upstream fi.rs pin update followed fresh wrapper regeneration, native/lifted corpus and nine Lean module checks; generated Lean remained unchanged. Three stale bundles were regenerated from integrated source.

Raw review verdicts: Astra GAP (exact CI and component authentication unverified by the reviewer), Opus GO; neither found a source blocker. The coordinator preserves both raw verdicts and discharges execution gaps only with completed exact receipts.

Hosted-runner interruption: post-push extraction run 39076349442 lost runner communication on attempt 1; GitHub supplied no job log, so the underlying cause remains unknown. The failed attempt and annotations were preserved. One deliberate retry on the unchanged commit passed on attempt 2; the other successful workflows were not rerun. See postpush-retry-audit.json and postpush-extraction-failure-20261018/ in the completed receipts.

Completed receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-auth-paths-20261017/night-closure. PMF result SHA-256 00827223be451b70aa9e6b2c390ac16d8c9de5d1a1f2cb2d86d58828a437dc04; review manifest cdc3438d4c583b9a698199f35caa2307f6080adfd5a913100a4fe0e3d2967568; postpush audit e1cf512d75ced86b9de45b522f69e80643a2d92c80d1a0864983d3d2d9ed1739. Issue/PR publication readback and canonical-worktree preservation are the final closure checks.

#100 and #295 remain open. The PMF frontier still includes whole C10 honest-signature correctness, lower/FORS forgery descent, minimum repeated-address exposure, adaptive coverage/private-opening charges and the final bound. Unbounded adversaries, the 4,008-byte PMF codec/session connection, freshness, concrete hash/Rust interpretation, cross-kernel correspondence, QROM and physical claims remain outside this component. This is source-stage research evidence, not shipment or hardware approval.

The structured PMF honest-correctness batch is landed on master in #978 at 6d4c2a3aad516d1f88904a49326df81eaec37102 (tree 17bdb3804647ed248ab46034ddd90f7ddf60c3b4).

Every successful bounded structured C10 signature under the actual generated key now verifies in its resulting cache and every consistent later cache. The proof derives accepted WOTS count/R/H_msg lookups, private-seeded prefixes, actual returned authentication paths, shuffled forest positions, the special final leaf/compression, both layers and equality with the actual top keygen root. The composed PMF keeps signing failure as none and assigns zero mass to some false.

Evidence: 40 new theorem closures in 11 modules, including 11 finite examples; fresh full gate passed all 1,545 kernel closures and 917 typed cases / 2,751 compiler jobs in 23.3 minutes. All 1,505 prior statements, 870 prior fixtures, old proof-module bytes and 52 bindings are preserved. The 47 new controls include 40 negatives and seven equivalents. The three corrected control groups execute complete consuming proofs; mathematical b && true and root ++ [] equivalents pass. Six local supporting groups and the exact source scan passed. Unchanged EasyCrypt/extraction evidence was authenticated; extraction was outside this diff's trigger.

Review: Opus GO; Astra GAP for then-pending execution evidence, now discharged by the audited full replay and actual applicable CI. Neither reported source findings. All 6 actual PR workflows and 4 actual push workflows succeeded; the main/probability checkout trees match this candidate. Publication and final preservation readback are recorded separately.

This closes the honest structured-signature component only. It does not prove guaranteed signing success, a byte-codec/Rust/EasyCrypt/cross-kernel relation, concrete hashing or hardware assurance. Minimum repeated-address exposure, lower/FORS forgery descent, adaptive coverage/private-opening charges, the final six-case PMF forgery partition/bound, unbounded adversaries and repeated-grinder freshness remain open. #100 and #295 remain open; combined assurance #509, optimization #789 and parser work #970 remain deferred.

The complete repeated-address WOTS exposure batch is landed on master in #979 at 359509a474bc14f1c2dbe6ac08fe643f7a3b1422 (tree c4688a07cf336925b828739225a98732d88a71eb).

Functional tree/forest uniqueness and actual count replay now derive stable signed messages and accepted words at repeated logical C10 WOTS addresses. The complete chronological signing history retains both layers, every successful exposure and duplicate calls. For an actual winning top-chain opening, the proof derives either a prior identical word and all returned prefix values, or a position below the exact minimum of every prior returned position at that address, with an actual private-seeded prefix and suffix to every matching prior value. Original collision/public-zero alternatives remain.

Evidence: 60 new theorem closures in 13 modules, including 15 finite examples; fresh full gate passed all 1,605 kernel closures and 963 typed cases / 2,889 compiler jobs in 22.8 minutes. All 1,545 prior statements, 917 prior fixtures, old proof-module bytes and 52 bindings are preserved. The 46 new controls include 40 negatives and six mathematical equivalents, using complete consuming proofs or asymmetric kernel computations. A mixed accepted-word counterexample demonstrates why same-address uniformity must be derived. Six local supporting groups and the exact source scan passed. Unchanged EasyCrypt/extraction evidence was authenticated; extraction was outside this diff's trigger.

Review: Opus GO; Astra GAP solely for then-pending full replay and mandatory CI evidence. Neither reported source findings. Full execution evidence remains a mandatory landing gate. Mandatory execution evidence is now discharged by the audited full replay and all actual applicable CI. All 6 actual PR workflows and 4 actual push workflows succeeded; the main/probability checkout trees match this candidate. Publication and final preservation readback are recorded separately.

This closes the positional repeated-address comparison only. Earlier than every returned position does not establish secrecy, absence from raw queries or a private-opening probability charge. Equal words do not imply equal full digests. Lower/FORS forgery descent, adaptive coverage/private-opening charges, the final six-case PMF forgery partition/bound, unbounded adversaries, the byte codec, repeated-grinder freshness and concrete hash/Rust/EasyCrypt/cross-kernel/QROM/runtime/hardware claims remain open. #100 and #295 remain open; combined assurance #509, optimization #789 and parser work #970 remain deferred.

The lower-layer WOTS descent batch is landed on master in #980 at 0f3ad9dd54df12977bee9cba4277477114f842c9 (tree a6f2dd10274c909f923d681784dc0a0bfccb12de).

Actual selected count lookups now turn a repeated upper WOTS word into either a concrete distinct-input accepted-word collision or equality with a prior signature's actual lower root. Its builder certificate supplies the submitted lower leaf even at a different selected leaf. Reverse binding derives the accepted lower count and every private-seeded prefix; complete lower-history comparison retains both coordinates, duplicates, exact minimum and actual suffixes to all matching prior values. The observed/initialized winning endpoints preserve the actual top opening, prior upper occurrence/root and original collision/zero/top-earlier alternatives.

Evidence: 24 new lemmas in six modules including seven finite examples. Fresh full validation passed 1,629 kernel closures and 995 typed cases / 2,985 compiler jobs in 23.5 minutes. All 1,605 prior statements, 963 fixtures, old proof modules and 52 bindings are preserved. The 32 new proof-sensitivity controls comprise 27 negatives and five equivalents. Six local supporting groups and exact source scan passed. The initial local attempt stopped on filesystem ENOSPC and is not credited; its logs were retained and a fresh project replay passed after inactive cache reclamation. Unchanged EasyCrypt and extracted-proof evidence was authenticated against exact relevant inputs across concurrent firmware changes; current main CI was required separately.

The concurrent baseline's #711 curation receipt and three generated research bundles were repaired using the existing printers/generators. The five curation metadata files change only the shared input receipt and dependent hash metadata; all 534 authority artifacts, roots, descriptors, known/refused sets, Bloom and signing eligibility remain identical. Full xtask tests, descriptor repeat gate, actual production quarantine and bundle repeat gate passed. No production provenance was promoted.

Review: Opus returned GO with no findings; Astra returned GAP with no findings, solely because the mandatory full replay and exact CI were pending. The raw reports are preserved. The coordinator must discharge those execution requirements before landing. Mandatory execution evidence is now discharged by the audited full replay and all actual applicable CI. All 6 actual PR workflows and 4 actual push workflows succeeded; actual main/probability checkout trees match. Publication and final preservation readback are recorded separately.

This closes lower-layer structural descent only. Earlier-than-all positions do not prove secrecy, absence from raw queries or private-opening probability. Repeated lower words still need FORS descent; coverage/private-opening charges and the final six-case PMF forgery partition/bound remain open. Existing unbounded-adversary, byte-codec, repeated-freshness, concrete hash/Rust/EasyCrypt/cross-kernel/QROM/runtime/hardware limits remain. #100/#295 remain open; #509, #789 and #970 remain deferred.

The FORS descent batch is landed on master in #983 at 1331efd73d4e02300dae9864e189e73d51cd8380 (tree 4e275b4343a8f00595d2465b961c01e6c71a0300).

Actual lower count lookups retain accepted-word collisions or bind the forest public key and complete hypertree address. Actual shuffled signing and ordered recovery executions provide all twelve ordinary tree certificates, ordered thirteen-root compression, and the separate last transmitted root/leaf hash. Selected-node collision exclusion then derives every submitted ordinary private-value lookup from the actual certificates and recovery paths. The thirteenth transmitted value remains a built root, not an ordinary private-leaf exposure.

The complete duplicate-preserving successful-signing history yields coverage of every ordinary hypertree/tree/leaf coordinate with equality to an actual returned secret, or a coordinate absent from every matching signing record with its actual private lookup retained. Different trees may match different prior signatures. Observed/support/initialized winning endpoints preserve the complete history, signing cap, prior upper/lower occurrences, both earlier-chain alternatives and all original collision/zero branches.

Evidence: 34 new lemmas in nine modules including eight finite examples. Fresh full validation passed 1,663 kernel closures and 1,040 typed cases / 3,120 compiler jobs in 26.3 minutes. All 1,629 prior statements, 995 fixtures, old proof-module bytes and 52 source bindings are preserved. The 45 new complete-consuming-proof controls comprise 38 negatives and seven equivalents. Six local supporting groups and exact source scan passed. Unchanged EasyCrypt and extracted-proof evidence was authenticated against actual relevant inputs, including all 29 registered extraction sources and 583 workflow inputs across concurrent firmware changes; current main CI was separately required. Two inherited stale research bundles were refreshed by their unchanged generator and passed the repeat gate. No runtime or generator change is included.

Review: Opus returned GO with no findings; Astra returned GAP with no findings, solely because the mandatory full replay and exact CI were pending. Raw reports are preserved; those execution requirements must be discharged before landing. Mandatory execution evidence is now discharged by the audited full replay and all actual applicable CI. All 6 actual PR workflows and 4 actual push workflows succeeded; actual main/probability checkout trees match. Publication and final preservation readback are recorded separately.

This closes structural repeated-lower-word FORS descent only. Unmatched in signing history does not mean absent from raw queries, undisclosed, fresh or probabilistically bounded. Adaptive coverage/private-opening charges and the final six-case PMF forgery partition/bound remain open. Existing unbounded-adversary, byte-codec, repeated-grinder freshness, concrete hash/Rust/EasyCrypt/cross-kernel/QROM/runtime/hardware limits remain. #100/#295 remain open; #509, #789 and #970 remain deferred.

Navigation Menu

Repository navigation

FV-frontier (b): Real-valued probability-monad quantitative bound (`Pr[forge] ≤ ε`) #295

96 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

FV-frontier (b): Real-valued probability-monad quantitative bound (Pr[forge] ≤ ε) #295

Description

Activity

Nicola-Ceornea commented on Sep 21, 2026

Nicola-Ceornea commented on Sep 22, 2026

Nicola-Ceornea commented on Sep 22, 2026

Nicola-Ceornea commented on Sep 22, 2026

Nicola-Ceornea commented on Sep 22, 2026

Nicola-Ceornea commented on Sep 23, 2026

Nicola-Ceornea commented on Sep 23, 2026

Nicola-Ceornea commented on Sep 23, 2026

Nicola-Ceornea commented on Sep 23, 2026

Nicola-Ceornea commented on Sep 23, 2026

Nicola-Ceornea commented on Sep 24, 2026

Nicola-Ceornea commented on Sep 24, 2026

96 remaining items

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 17, 2026

Nicola-Ceornea commented on Oct 18, 2026

Nicola-Ceornea commented on Oct 18, 2026

Nicola-Ceornea commented on Oct 18, 2026

Nicola-Ceornea commented on Oct 18, 2026

Nicola-Ceornea commented on Oct 18, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

FV-frontier (b): Real-valued probability-monad quantitative bound (`Pr[forge] ≤ ε`) #295