FV15-F6 — EasyCrypt C10 representability stop/go (research-only)

Stage-1 shipped with F5; this is the stage-2 stop/go. Before adaptive/capstone work, determine whether a concrete checksum-free WOTS theory can cover w=8, log_w=3, l=43, target sum 205 and whether the conditioned fresh-R bounded grinder refines production. Preserve and stop if either requires a foundational rewrite that retires no named assumption; otherwise proceed milestone-by-milestone through concrete WOTS, FORS, trees, and one common-adversary scheme theorem. No release credit meanwhile.

Migrated from docs/work-todo.md section Formal-verification full-stack review 2026-07-15 — open follow-ups (file retired 2026-07-19; original archived at docs/archive/work-todo-retired-2026-07-19.md).

Canonical finding record: docs/security/adversarial-review/findings/fv-full-stack-2026-07-15-coordinator.md F6 (status 🔲 OPEN — CONFIRMED gap · OPEN RESEARCH; V8/V9/V11/G5 · MED while honestly research-only, HIGH if promoted as concrete C10 evidence): imported EasyCrypt WOTS results cannot instantiate shipped C10 (MM45 restricts log2_w to {2,4,8} with standard checksum; C10 uses w=8, log2_w=3, 43 checksum-free target-sum chains); capstone remains conditional. Anchors MM45 WOTS_TW_ES.ec, C10 params.rs. Includes the staged EasyCrypt stop/go decision (do not resume abstract capstone work before a C10 representability result). This issue tracks the same item; the frozen evidence and cross-adjudication live in the report.

Current frontier checked on 2026-09-17 against master ab9e9049a5a8c8d088966d02b7ff9a5714ae678a (the same EasyCrypt sources are preserved in integration candidate 6bc23f2223aa820595be3bd6b04391bd7e5b6121). Keep this issue OPEN.

The original July MM45-only explanation is now partly historical. base-c10-split/WOTS_TW_ES.ec:55 admits log2_w=3; cdrafts-split/C10DeployedInstance.ec defines the deployed constants and proves the split theory's numerical admissibility/width obligations. The 16-byte chain / 32-byte message-digest split removes that representability obstacle. This is not a concrete firmware instantiation. The former false WOTS injectivity admit was replaced by an explicit encoding-collision term; the remaining extract_op admit is outside all six registered headline environments and is explicitly not the owner's recommended next unit.

A bounded Phase-A experiment succeeded: an EasyCrypt integer search with an explicit cap proves termination, first valid counter, and exhaustion exactly when [0, cap) contains no hit. It introduces no new axiom, admit, or finite-enumeration clone. Additional lemmas prove u32 increment safety at 10M and show that a valid full-domain counter need not lie in the signing budget. Both drivers pass (CLI: 29 prompts, no diagnostics), plain require passes, and a control that skips counters fails the intended proof. Pinned image: ghcr.io/easycrypt/ec-test-box@sha256:bf1a13e73d7fe18fccdcc91d1532c1a5a17cfc3a6a2a34619248c4f2710d0bb3.

Artifacts are preserved locally, on branch research/c10-budgeted-grind-20260917, under docs/verification/research/budgeted-grind-2026-09-17/ (prototype, negative control, assessment, logs and hash receipt). They are not added to the certified cone or PR #689. The existing Grind.ec already proves finite-enumeration search; this experiment's contribution is an explicit integer budget/exhaustion model, not a first termination proof or retirement of assumptions from a headline theorem.

The next useful refinement must preserve both domains: production WOTS signing tries 0..10_000_000u32 and panics on exhaustion, while verification accepts any u32 counter. It must also pin right-zero-padding of the 16-byte message, the big-endian counter in a 32-byte slot, one SHA-256 evaluation, and low-129-bit base-8 extraction. The model's two digest halves are correlated outputs of that same hash, not independent hashes. The separate FORS fresh-R budget, optional randomizer and conditioned distribution remain open.

Encoder/cardinality correspondence, grind-reachability, and quantitative ITSRC10/T_COLL_RES_ENUM bounds remain research obligations. The structural c=262656 is not a signing-query budget. Decision: the explicit-budget refinement slice is tractable; broader C10 production-refinement/security claims remain conditional. No release credit or numerical security improvement is claimed. The owner-triggered combined assurance pass in #509 stays deferred.

Phase-A research update, 2026-09-21, checked against current master 2d4ba31d3ff7a745dc338c5ec349ba943ce380b5. Keep #100 OPEN, but two previously separate modelling questions now have constructive, checked research results.

Concrete u32 counter realization: U32Grind.ec clones the actual current Grind.Grind, proves its inherited CntrFT.enum_spec, and proves exact cardinality 2^32, rank equal to numeric counter, and agreement between a successful 10M-prefix search and the existing full-domain grinder. Verification retains the entire u32 domain. This proves the obligation in the research instance; it has not been wired into the current headline.
Exact finite-budget conditioning: BoundedIID.ec proves that independent draws from a lossless distribution with acceptance mass p exhaust with probability (1-p)^B. For p>0, every successful-output event has probability (1-(1-p)^B) * mu(dcond d P, E). The stronger mixture theorem includes exhaustion explicitly. Repeated sample values are allowed. The firmware's deterministic nonce/hash transcript is not automatically an instance of these independent draws, and its actual acceptance mass has not been bounded.

There are 12 new named lemmas plus the two realized clone obligations. Direct compile, CLI inspection and plain-require consumers pass in the existing pinned r2026.02 image. Four deliberate false variants (cardinality, rank, exhaustion outcome, unconditional success mass) fail at the intended proof obligations, without syntax/import failures or timeouts. No new project axiom or admit was introduced; the counter subtype uses the standard library's four explicit construction axioms, and the normal library/prover trusted base remains.

Proofs, inputs, negative controls, logs, hashes and the updated assessment are preserved locally, in commit acef3b99 on the existing branch research/c10-budgeted-grind-20260917, under docs/verification/research/budgeted-grind-2026-09-17/2026-09-21/. The existing parent README contains the dated assessment. Nothing was added to the certified cone or pushed to master.

The current split theory already resolves the original numerical-parameter admissibility obstacle. These two new results support proceeding with a bounded integration batch: concrete counter/encoder wiring; actual serialization and bounded operational-loop correspondence; then the fresh-R sampling/game bridge with explicit abort semantics. The SHA-256 digest halves must remain correlated. The isolated extract_op admit remains outside the six headline environments and is not the recommended next unit.

The SPHINCS+C paper, Appendix C calculates geometric failure and then assumes suitable-counter existence for its analysis; that does not close our production correspondence. Quantitative ITSRC10, unbounded collision-game and primitive bounds still need explicit cryptographic assumptions and query/resource limits. The integer digit-surface count is not yet a firmware distribution bound, and c=262656 is not a signing-query budget. #295 remains open; #509 stays deferred. No release or numerical-security credit is claimed from these research results.

Landed the concrete counter / serialization / bounded-search batch in #710, now on master at 19ddfc401ac3ba6c473f628d7552a4f8bc45ddef.

Resolved within the stated manual-model boundary:

The actual WOTS/STCRC consumer uses the full-u32 counter domain and ascending enumeration; its enum obligation is realized, with numeric rank and cardinality proved.
The actual compact encoder is fixed. Width, injectivity and equality to the named encoder are proved without additional premises; the legacy headline binders remain for compatibility.
The physical byte adapter has proved padding/order/round-trip properties. Source identities and 210 cases against real Rust helpers bind the manual correspondence.
Bounded search proves first-hit correctness and explicit exhaustion, with conditional agreement with the actual grindC consumer on success.

The integration preserves master's separate surface-count promotion. The combined full replay is GREEN: 60 files through both drivers, zero disagreements, all 58 controls and census/containment checks pass. Rust tests, 10 split regressions, 22 gate-enforcement regression groups and the final fast gate also pass. Exact review, replay and editorial identities, raw reports and logs.

Owner review decision, 2026-09-21: leave Kimi out for now while access is unavailable. Astra and Opus both returned GO on the integration; an earlier additional independent Astra review was capped at eight minutes and finished GO in 145 seconds. This adds an independent reading, not a third provider family. Conservative documentation findings were corrected with formal-code equality checked.

Keep #100 open. Full Rust/hash/predicate refinement, abort-aware signing-game composition and fresh-R oracle coupling remain. Four standard-library Subtype construction obligations remain trusted. This does not supply a numerical security bound (#295). The combined owner-triggered playbook pass stays deferred under #509. Broader unrelated CI failures remain tracked in #660/#661/#711; the dedicated FV/G1/workflow/census checks passed on the final source candidate.

Literature/source reassessment, 2026-09-21, against master 19ddfc401ac3ba6c473f628d7552a4f8bc45ddef. Keep #100 and #295 open.

The next useful batch is smaller than a fresh implementation-verification project: this tree already contains WotsDigits.lean::extract_digits_spec (all 43 exact bit windows) and HashSpecs/WotsDigest.lean::hash.wots_digest_spec (the hash transcript). Selected Rust/generated-Lean pins for both extraction entries match. This was a source-identity check, not fresh extraction or proof replay.

Recommended order:

Realize the actual EasyCrypt digit encoder and target 205, including least-significant-first chain assignment, and connect it to the gated count.
Compose bounded failure into the signing games, retaining abort/no-signature semantics and success conditioning.
Prove shared-oracle/fresh-R correspondence and query accounting before attempting numerical ITSRC10/T_COLL_RES_ENUM bounds.

Useful recent sources:

libshrincs has explicit bounded-search failure and a security-game connection. Its different parameters, known-message game and symbolic hash bounds prevent direct transfer to C10.
Ho et al., September 14, 2026 provide newer Aeneas/Rust verification methods.
Completing the Chain connects Jasmin XMSS implementations to EasyCrypt security; it is a related methodology, not C10 closure.

Two independent host arithmetic methods reproduce the surface count. Under IID uniform digests it implies about 30,698 WOTS trials on average and 10M-trial exhaustion near 2^-470. These are conditional calculations, not firmware probabilities or security bits. Repeated truncated R and adaptive oracle history still require explicit treatment.

Detailed sources, limitations and acceptance criteria are preserved locally in commit c0243d497a3db169c1e9f2f060a8d90d6974f36c, branch research/easycrypt-literature-20260921, amending the existing feasibility note. The branch is not pushed. No new proof replay, production change, numerical-security credit or #509 activation.

The next encoder/abort batch is implemented in draft PR #716 (commit 031158745e5939885f2886fd6040747ce441557b).

The actual C10 consumer now has a concrete LSB-first digit encoder and target-205 witness. Its uniform-input acceptance theorem consumes the checked count 22169393903687611906220091621190388 / 2^129. The option-valued bounded signer preserves full signature agreement on a successful prefix; the bounded oracle preserves successful replies/state and makes failure absorbing. A guarded game rejects flagged runs. The separate IID companion retains exhaustion and the successful-event factor explicitly.

Astra and Opus returned GO with no blocking findings. Fast integrity, Rust correspondence, targeted Lean digit proof/axiom dump and gate regressions pass. The mandatory 66-file dual-driver/64-control replay is still running; no master landing yet.

Still open: failure-aware end-to-end reduction to the capstones, real shared-oracle/adaptive-history and FORS truncated-R coupling, and resource-accounted numerical bounds (#295). The IID sampler is not a refinement of the real SHA-256 counter process. #509 remains deferred.

Banked non-blocking editorial note from review: BadEncCountermodel.ec still describes the encoder as free. Its generic theory retains abstract geometry and explicit collision hypotheses; the new concrete identification is proved for the deployed SPHINCS_PLUS consumer. Update those historical comments in the next owner-triggered touch without broadening the current closure phase.

PR #716 is now at 47c9bb1e. The first full replay found a CLI disagreement at the existing WOTS_C_Multi loop-exit proof. The correction makes the same list-length argument explicit; the theorem, invariants, premises and prover budgets remain unchanged. Focused compile and CLI pass (172 commands, zero diagnostics), the fast integrity gate passes at identity 946053f3a3915a95a5556a0a08a93fb7, and fresh Astra/Opus reviews both returned GO. The corrected full replay is still running; no master landing yet.

Additional non-blocking editorial debt from review: WOTS_C_Real.ec's historical predC_tgts comment still calls the witness declared and target 205 unpinned. Group this with the previously banked BadEncCountermodel comment cleanup. The new C10Encoding lemmas and current owner documents carry the precise boundary; this conservative historical wording does not add an assumption or change a theorem.

The active batch does not close #100/#295's real shared-hash/adaptive-history/FORS truncated-R coupling or numerical EUF-CMA work. #509 remains deferred.

Landed on master as d947c04780a156853160bef32882b158518c90b7 via PR #716.

Closed in this batch: actual consumer digit encoding and target-205 witness; consumer predicate to exact CountDS uniform-input acceptance; option-valued bounded signing with no-signature exhaustion and successful reply/state agreement; separate IID exhaustion/success-mass law instantiated with the consumer predicate. No new project axiom or admit.

The corrected full gate is GREEN, exit 0: all 66 files under both drivers, 1,332 declaration pins, 1,201 statements, all 64 controls, zero driver disagreements, input identity 946053f3a3915a95a5556a0a08a93fb7 unchanged. Fresh Astra/Opus GO reports and Rust/Lean correspondence receipts are published here. The first full replay's loop-exit proof disagreement and its correction are preserved in the receipt.

Keep this issue open for failure-aware end-to-end reduction, real shared-SHA-256/adaptive-history coupling (including FORS truncated R), and numerical EUF-CMA bounds. Finite Rust tests, a manual EasyCrypt model and the targeted Lean proof remain distinct evidence. Historical conservative comment cleanup remains banked; #509 remains the deferred combined playbook pass. Broad baseline CI failures remain tracked in #660/#661/#711/#717 and do not acquire a green claim from this batch.

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.

New checked progress: deployed all-leaf paths cover the complete hypertree cube; the actual bounded hypertree has an N2-free five-term bound with its failure charge retained; C10's concrete counter-input search has a classical memoizing-history bound; physical hash domains, high-half R truncation, budgeted randomizer collisions, and the existing FORS consumer's bounded/conditioned mixture are now explicit.

This issue stays open for the actual event-preserving accepted-history composition that removes the whole-hypertree failure charge, plus a common stateful hash simulation covering H_msg, WOTS/tree calls and secret-keyed R derivation. Index coverage alone does not establish those game equivalences. Repeated R values must replay the same hash answer. The broader legacy tree-port admit remains outside the isolated headline claims.

The costed-game work and a justified link from whole-experiment R draws to per-key usage remain coordinated with #295. The combined playbook pass in #509 stays deferred until owner-triggered.

FORS secret-generation correspondence landed via PR #822 (e96aec7f). The corrected reference helper and all reference signer/round-trip callers now bind the hypertree-position field already present in Rust. The actual extracted helper is proved equivalent on its complete 48-byte preimage and 16-byte result for every seed and all three full-width indices. The existing SHA helper preserves Rust's five ordered updates; concrete backend correctness remains explicit.

Evidence: 123 audited headline closures with the same 27 environment axioms; nine complete extraction regenerations; 131 independent cases across four software/extraction/host-adapter configurations; 262 value, 131 width and five malformed-input controls; two positive baselines and 13 typed semantic mutations; copied-definition and six CI-path deletion controls; 61 Rust regressions. The combined local proof/differential gates passed. ARM crate evidence: code +120 bytes, unchanged static data, sign_inner compiler frame -8 bytes; not whole-program stack or silicon evidence.

Fresh EasyCrypt replay: all 1,998 judgments GREEN in 4,143.2 active seconds, identity 27015a144ca3e10d6a96b4375c3e29e8; all 1,960 EC files and 626 source bindings match the landed candidate. All eight exact-commit CI workflows passed (21 passing checks; existing nonblocking dependency-review availability failure). Astra and Opus both GO; Kimi remains omitted by owner instruction.

#820 is closed. A pre-existing reference signer final-slot mismatch is now banked as #823: Rust serializes the full final FORS tree root where the reference currently uses the leaf-0 secret. It remains outside this secret-helper theorem and belongs with tree/signer refinement. Tree construction/membership, shuffled signing, concrete backends, randomness and full signer/session refinement remain open. Deferred #509/#789/#809/#812 stay deferred.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-fors-secret-20261009.

FORS tree-root construction and final-slot correspondence landed through PR #824 (415b81d9). The complete actual stack/carry algorithm is proved total and equal to the faithful recursive height-11 root for every seed and full-width hypertree/tree index. The reference signer now puts that full root in the final FORS slot, matching Rust; its honest roundtrip remains proved. #823 is closed. Production Rust is unchanged.

Evidence: 128 audited headline closures with the same 27 environment axioms; complete extraction regeneration and freshness; 21 independent recursive root cases plus two actual signer cases; all three positive baselines and 19 typed semantic controls; fidelity and ten CI-path deletion controls. All mandatory local gates and eight exact-candidate CI workflows passed (21 passing checks; existing dependency-review advisory remains unavailable). Astra and Opus both GO under the standing reviewer overrides; Kimi omitted. The completed 1,998-check EasyCrypt replay is reused after exact equality of 1,960 files and all 626 source bindings.

Optional merge-address mutation coverage is banked as #825. Authentication-path generation, hypertree key-generation trees, shuffled signing, concrete backends, randomness, and full signer/session refinement remain open. The next bounded batch will address FORS authentication-path generation. Deferred #509/#789/#809/#812 stay deferred. Master push workflows have started without a failure observed; post-push monitoring continues.

Receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-fors-tree-20261009. No hardware or shipment claim.

Landed PR #826 (5ab861449ec8ff3ebac99a51df4db6af5e9a0571): actual C10 FORS authentication-path generation now has a total extraction proof and faithful reference bridge for the secret and all eleven siblings, for every seed, full-width hypertree/tree index and valid leaf below 2,048. The audited headline count is 133 with the same 27 environment axioms; production Rust is unchanged.

Evidence: complete local proof/differential suite, independent recursive Rust oracle across all 2,048 leaves and 22,528 siblings plus 23 boundary cases, actual/pure/reference Lean comparisons, regeneration, semantic/fidelity controls, and exact-candidate CI. Two reproduced evidence-classification findings were corrected: proof controls reject abnormal/resource exits; fidelity controls reject incomplete reports and error-stream diagnostics. Their affected gates were rerun, with 34 and 44 invalid-result regressions respectively; unchanged proof/corpus evidence was explicitly reused by exact Git diffs. Both bounded Astra and Opus reviews returned GO on the final commit. Opus's independent 100-second differential attempt was inconclusive; it is not treated as execution evidence.

All eight exact-commit CI workflows passed, with 21 passing checks and only the existing non-blocking dependency-review failure because GitHub Dependency Graph is unavailable. The completed 1,998-check EasyCrypt replay is reused after exact equality of all 1,960 proof inputs and 626 source bindings.

Remaining: whole-signer/forest composition, hypertree key-generation trees, shuffled signing/randomness, concrete backends, and the full Rust/EasyCrypt session relation. No hardware or shipment closure. The older sibling control-classifier follow-up remains tracked in #827; deferred broader assurance remains with #509.

Landed PR #828 (922254c90587cf9bf11498a904b213bd52651fa4): the actual C10 FORS signing helper, private recovery helper and root builder now compose for every pair of seeds, full-width hypertree/tree index and valid leaf below 2,048. The generated secret and all eleven siblings recover exactly the constructed root and the faithful reference root. The actual-call headlines have no desired-output premise.

Three added audited headlines bring the total to 136 with the same 27 environment axioms. Production Rust and extraction registration are unchanged. Rust checks all 2,048 leaves, 22,528 changed siblings and six full-width positions in both normal and extraction configurations. The 23-case Lean corpus compares actual sign/recover/root results to independent recursive roots; 552 altered secret/path recoveries and 23 wrong-leaf recoveries differ as expected. These finite corpus inequalities are not a universal collision-freedom theorem. Seven typed fold mutations and both new-path CI deletion controls pass.

All frozen local gates and exact-candidate CI passed. Both bounded Astra and Opus reviews returned GO with no findings. Opus performed source inspection; Astra's separate full-corpus attempt exceeded its 180-second cap after two boundary cases passed. Coordinator execution evidence includes the completed 357-second focused corpus and the full frozen differential; reviewer timeouts are not counted as passing evidence. The same completed 1,998-check EasyCrypt replay is reused after exact comparison of 1,960 proof inputs, 626 source bindings and 28 auxiliary EC files. The only advisory CI exception is the existing unsupported GitHub Dependency Graph check.

This closes per-tree membership and the actual sign/recover/root connection. Remaining: actual complete forest/signer control flow, serialization, shuffling, special final-slot composition, hypertree key-generation trees, concrete backends, randomness and the complete Rust/EasyCrypt signer/session relation. No hardware or shipment closure; #509 and other deferred assurance remain deferred.

Landed PR #830 on master at 21056afcf9c4bd46f530f83e25ce69ff42d254cf.

The actual 512-leaf XMSS stack builder and public-root wrapper now have totality and faithful reference-tree proofs. Six new audited headlines bring the total to 142, with the same 27 environment axioms. Production Rust is unchanged. The batch also fixes complete extraction-registry enrollment, the affected Merkle fixture marker, and a reproduced false pass for proof errors accompanied by MemoryError.

All mandatory frozen local gates passed; the full differential took 39m48s. All eight exact-candidate PR workflows passed (21 passing checks; the unchanged unsupported Dependency graph check is explicitly advisory). The bounded review wave found no concrete defect: Opus GO; Astra GAP for then-pending gate results, resolved by the completed coordinator evidence without changing source. The completed 1,998-check EasyCrypt replay was reused only after 2,614 exact proof/source-file comparisons. Post-push workflows are being observed separately and are not yet claimed complete.

Next: XMSS authentication-path generation and its connection to actual root recovery. Full signer/forest/serialization/session composition, concrete backends, randomness and callback effects remain explicit boundaries. Deferred #509/#789/#809/#812/#825/#827/#829 remain separate; this is no hardware or shipment claim.

Landed XMSS authentication-path construction and membership in #833, master 5d74e068f4f89b408d42f088171cec5d4e943cb1 (tree d062df98b2ef6f82b727571b67a31f6000299bd9). The actual builder terminates for every valid leaf below 512, returns the faithful nine siblings and height-nine root, and composes with actual WOTS public-key generation, path recovery and independent root construction, including full-width addresses.

Evidence: 149 exact headline closures with the unchanged 27-entry environment; independent Rust/Lean oracle corpora; 37 typed authentication mutations plus fidelity/deletion and gate controls. Four actual-builder headlines explicitly carry the existing Aeneas Formatter : Type dependency through the unreachable debug-panic branch; three new headlines are kernel-only. Production signing Rust is unchanged by this proof diff.

The complete local differential passed in 41m22s. After integrating master’s unrelated UI commits without conflicts, all verification inputs were checked unchanged and that completed local proof evidence was reused explicitly; fresh fast gates and exact integrated CI passed. All eight workflows succeeded (21 passing checks; the pre-existing unsupported Dependency graph advisory failure remains separate). The integrated extracted CI run completed its differential in 85m15s under the 120-minute budget. The earlier 90-minute cancellation and reboot-interrupted attempts remain recorded as incomplete/failed evidence.

The fresh bounded review on the landed commit found no source blocker: Astra ultra (281.5s) reported only pending CI, now resolved by the exact successful run; Opus 5.5 xhigh (285.5s) returned GO. No Kimi. Completed 1,998-check EasyCrypt replay was reused only after exact proof/source identity checks.

Remaining boundaries stay open: full WOTS signing, shuffled forest/signer/session and serialization correspondence, concrete backend/randomness/QROM assumptions, and hardware assurance. This does not claim a new full-scheme security theorem. Deferred combined assurance remains #509. Post-push master workflows are being observed; the next proof slice will follow the remaining component frontier.

Landed #836 on master at efece4d0a6e2dc3e63ec90b50478f5e985c98b61 (tree b79fa09579f2193fb7e63cbd25364f538d916e02). The actual shuffled WOTS signer now proves first accepted count or bounded exhaustion, all 43 positional chains, shuffle-seed independence, recovery to the actual generated public key, and agreement with the faithful reference primitives. Fisher–Yates totality/prefix permutation holds for every supported length. No desired output is a headline premise.

The audit now covers 156 headlines with the same 27 environment axioms; 31 extraction entries include 30 fresh and the existing tx-merkle waiver. Independent Rust/Lean corpora and 20 typed mutation controls pass. Review identified a spec-preserving mutation that only broke a proof tactic; it was replaced with an out-of-range mutation and an executed counterexample. The required emulator tail gate now actually verifies every changed successful output and fails on verifier errors: 16,306 such outputs were rejected across 90,045 sampled trials. This is a fixed-input mirror check, not production or physical fault-resistance evidence.

Full EasyCrypt replay passed in 82m27s: 662 direct + 662 CLI + 674 controls, all 1,998 judged, identity 01b6d821baae24efe8b63a52ded33d9a. Two parallel CLI load failures passed prescribed isolated rechecks. Complete local differential passed with exact unchanged-input binding and a fresh corrected-control run. Exact-candidate CI independently reran the full differential successfully in 90m40s: run. All eight workflows succeeded; the existing unsupported Dependency Graph check remains explicitly advisory.

Fresh bounded Astra/Opus reviews found no remaining source findings. Their only pending condition was mandatory execution evidence; the coordinator closed it after the above results without changing the reviewed source. All six exact-master post-push workflows subsequently passed, including the fresh extracted differential run.

Next component: shuffled FORS forest construction and recovery composition. Whole signer/serialization/session correspondence, concrete backends, callback effects, randomness/QROM and physical assurance remain open. This is no full-scheme security or shipment claim. #295's exclusion of full C10 EUF-CMA mechanization and deferred #509/#789/#809/#812/#825/#827/#829 remain unchanged.

FORS forest correspondence checkpoint — PR #837, commit 137c2ae82dd5f3d49d763f9508a57338b2794c1c, tree cbd33ee315935c7267b3e4bae26a5b79af005531.

The actual Rust sign_inner FORS phase now has positional totality for all twelve shuffled trees, the special final root/compression relationship, verifier recovery and reference equivalence, shuffle independence, and an unconditional caller-prefix equality preserving failure and the unchanged suffix. Production Rust is unchanged. Six new audited headlines bring the default set to 162 (148 kernel-only, five retaining the existing Formatter type, and nine retaining existing backend axioms); the environment remains at 27 axioms. The extraction registry has 32 entries, 31 fresh plus the existing tx-merkle waiver.

Validation: exact regeneration, Rust/Lean differential corpora, 290 changed-value recoveries, 15 typed semantic mutations, the full local differential gate (46m19s), static/audit/freshness/gate-enrollment checks, and both bounded reviewers (Astra GO, Opus GO). All eight exact-candidate PR workflows passed, including the fresh complete differential gate in 92m38s; the existing unsupported Dependency Graph advisory is recorded separately. Landed on master; all six post-push workflows now pass, including the complete differential replay. EasyCrypt evidence is explicitly reused from the completed base replay (1,998 judged jobs, zero unjudged), after exact equality of 1,971 relevant inputs and a fresh binding/identity gate; no new EasyCrypt replay is claimed.

Remaining: signature serialization and hypertree suffix correspondence, complete signer/session relation, concrete backend/entropy/callback/erasure and physical assurance. Full C10 EUF-CMA remains outside #295's scope. The combined assurance pass stays deferred under #509; this source-level merge grants no production or hardware authority.

Banked nonblocking editorial follow-up: extracted/axiom_closure_manifest.txt:28–29 still has the historical 156-headline explanatory comment; the enforced records correctly contain 162. Update the comment with the next proof batch, without reopening this reviewed candidate.

Serialization correspondence landed on master through PR #838: commit 8bab34f, tree b7bd1a58527f072bb8271f92070133eec1d30b08. Thirteen new audited headlines (175 total; environment axioms unchanged), exact byte/frame and supplied-field decoder correspondence, eight independent Rust/Lean cases, nine positive and twelve typed semantic controls. All nine local mandatory gates and all eight exact-candidate PR workflows pass; the full differential took 94m03s. Astra (121s) and Opus (183s) returned GO with no blockers. Exact unchanged EasyCrypt input equality plus a fresh binding gate authorize reuse of the 1,998-judged/zero-unjudged full replay; no fresh replay is claimed. All six post-push workflows now pass too; the post-push full differential took 5426s.

The next bounded proof slice is actual two-layer signer composition: bind layer ℓ to offset 2336+836·ℓ, replace its writer fragment with pure serializedLayer values, and connect its cryptographic outputs while preserving grinder failures. Full Rust/EasyCrypt signer/session, concrete backend, callback, entropy, erasure and physical boundaries remain open. #295's full C10 EUF-CMA exclusion and deferred #509 remain unchanged.

Two-layer signer landed: PR #839 (f95aa28, tree 9942995889bb36e21e05278a9599736973c847b0). Both actual extracted layer iterations now equal a pure first-count/canonical-chain/path construction, preserving bounded failure, full index arithmetic and exact wire positions. Success preserves the nonce/FORS prefix and yields the top tree root; the actual post-FORS caller is connected through the final root check.

All nine local mandatory gates pass, with 184 audited headlines and the unchanged 27-axiom environment. Two independent full-byte Rust cases pass in normal/extraction configurations; the full-u32 actual Lean loop passes; five positive proof baselines and fourteen typed semantic mutations pass. The prior 1,998-judgment EasyCrypt replay is reused after fresh equality of all 1,971 relevant inputs and a passing binding/identity gate. Astra GO (195.749s) and Opus GO (376.88s), no blockers; all eight exact-candidate PR workflows passed (full differential 6234s). Pushed normally to master; all six post-push workflows now pass too (post-push full differential 4662s).

The executable vectors currently share leaf 511 across layers; the arbitrary-index theorem covers the general arithmetic. Record a mixed-leaf runtime vector for the next caller/header corpus. Nonce/header and whole signer/session composition, the actual Rust/EasyCrypt relation, concrete backends/callbacks/entropy/erasure/physical evidence, and existing research-reduction limits remain open. Deferred #509/#789/#809/#812/#825/#827/#829 are unchanged.

Whole signer landed: PR #840 (003d5d3, tree 143c3281e3de90ef1d1b1a552fbdd3879edd4814). The actual extracted nonce/header and whole signer now have unconditional Result composition through the canonical forest, serialization, both layers and final root check. First accepted nonce, bounded failure, exact header fields/bytes and shuffle independence are explicit. A successful extracted-model signature retains the first nonce bytes and matches the constructed top key-generation root.

Important build boundary: the final offset/root checks are debug assertions retained by extraction and omitted in normal release Rust. The root-mismatch and success-root claims are model-level facts; release caller/verification correspondence remains open. The exact unchanged Rust tail was replayed with debug assertions on/off to confirm this limitation, and both status documents and proof comments disclose it.

All nine mandatory local gates pass on this commit. The default audit has 196 headlines (169 kernel-only, 18 existing Formatter, 4 SHA, 1 SHA/HMAC, 4 Keccak), with the unchanged 27-axiom environment. Both OptRand header fixtures pass normal/extraction Rust and actual Lean, with zero/nonzero first nonce and full-byte/digest comparisons. Three two-layer Rust cases and the actual full-u32 mixed-leaf Lean case pass. Four proof baselines and twelve typed semantic mutations pass. The prior 1,998-judgment EasyCrypt replay is reused after equality of all 1,971 relevant inputs and a fresh binding check. Astra GO (215.597s), Opus GO (256.275s), no remaining findings. All eight exact-candidate PR workflows passed (full differential 6376s). Pushed normally to master; five post-push workflows passed. GitHub concurrency cancelled extracted push run 38043717021; the same-commit scheduled replacement 38045958053 passed every gate (full differential 6425s). This bounded batch is complete.

This closes the bounded functional nonce/header and whole-signer composition slice, not the entire issue. Complete Rust/EasyCrypt simulation/session correspondence, release caller correspondence, backend/callback/entropy/erasure/physical evidence and existing research-reduction limits remain open. Deferred #509/#789/#809/#812/#825/#827/#829 remain deferred.

Release caller landed: PR #841 (#841), commit fd4fa32938f5bbf8482ea413f8700b36fa87e78e.

The separately generated assertion-off caller now has an unconditional Result relation, an exact checked/release relation for arbitrary roots, and equality when the extracted key-generation call supplies the root. Fourteen new audited headlines bring the total to 210 (170 kernel-only, 31 existing Formatter, four SHA-256, one SHA-256/HMAC, four Keccak); no new axioms. All nine local gates pass. Four positive proof baselines and eight typed semantic mutations pass. Four real Rust build configurations agree on all 4,008 signature bytes in both OptRand modes and distinguish checked root-mismatch panic from release output rejected by verification. Complete release extraction regeneration passes. The prior EasyCrypt replay is reused after a complete 1,972-file unchanged-input check.

Astra and Opus independently returned GO. All eight exact-candidate PR workflows passed (full differential 6504s). Pushed normally to master; all six post-push workflows passed (full differential 6413s). This bounded batch is complete.

Remaining scoped work: release-compiled opaque helper/backend correspondence; secure double-sign/compare/verify/CFI release effects; full Rust/EasyCrypt session simulation. This batch proves the caller under existing component models and does not close those boundaries. Follow-ups retained on this owner tracker: root Cargo.toml/Cargo.lock workflow trigger coverage for profile checks; per-body comparison for common dependency declarations currently protected by complete raw-output pins; independent bridge-statement controls. No current candidate defect was found in these areas. Deferred broader sweeps and replay optimization remain deferred.

Release helper landed: PR #842 — #842

Frozen candidate 8ed15f318e64dc9d2f08e6388644712a5a9a3696, tree b4af47223d634fdc758b28e51d7e74a1aa59378d, based on fd4fa32938f5bbf8482ea413f8700b36fa87e78e.

All twenty registered C10 component extractions now explicitly use release assertions-off/overflow-on settings; the assertion-on signer caller remains a comparison configuration. Fresh Charon/Aeneas generation changed six bodies and reproduced the complete outputs of the other fourteen. Root/frontier, authentication capture/copy and verifier loop proofs were adapted while retaining the headline all-input functional specifications and failure behavior. No production Rust behavior changed.

Evidence: 22 complete extraction regenerations; the full 24-suite enrolled proof-control matrix, including 24 release-helper baselines and 136 mutations; 102 invalid-result classifier checks; four-profile Rust full-byte checks; all nine mandatory local gates; all 210 exact headline closures (201 kernel-only, nine existing hash-dependent), unchanged 27-axiom environment. EasyCrypt's 1,972 relevant inputs are unchanged from the recorded 1,998-judgment replay; fresh binding checks passed. That replay is reused, not claimed as rerun.

Astra returned GO (109.662s) and Opus returned GO (285.695s) on this exact snapshot. Opus used its single permitted mechanical retry after quota reset. Its extraction-replay caveat is covered by 22 actual coordinator regeneration receipts; its pre-existing two-script CI path-filter note is banked under #567. Raw reports are preserved; no mandatory review gap remains.

The complete enrolled classifier set was reconciled after reproducing killed/interrupted/memory-failed outcomes being counted as semantic rejection in older suites. All 24 suites now use the strict shared classifier; H_msg mutations type-check their definitions independently. The release-output-equivalent flag-only mutation is retired. This also addresses the finite legacy classifier scope in #827; the broader owner-triggered assurance pass remains deferred.

All eight exact-candidate PR workflows passed (full differential 6406s). Pushed normally to master; all six post-push workflows passed (full differential 3583s). This bounded batch is complete.

This closes the registered helper assertion-profile mismatch. Concrete SHA/RustCrypto/STM32 implementation correspondence, the modeled shuffle sub-seed, callback/erasure and secure-wrapper effects, and the complete Rust/EasyCrypt session relation remain explicit boundaries. The next bounded batch is secure-wrapper functional effects, followed by the session relation. Hardware/production evidence and full C10 EUF-CMA/QROM research are not claimed. The combined owner-triggered assurance pass stays deferred under #509.

Local immutable receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-release-dependencies-20261010/remediation-4/.

Batch X checkpoint: PR #843, commit 0feea78a1b8bd5ecaa99c3346a5a69480fd13cbc, tree f612a14865a7d114a431cb6fb4d93e07d43db548, based on 8ed15f318e64dc9d2f08e6388644712a5a9a3696.

The ordinary secure-wrapper source slice now has sequential release, required-rate, cleanup and refusal-suffix theorems, plus composition with the extracted release signer and faithful raw verifier. Ten new headlines are kernel-only; the full audit is 220 headlines with the existing 27-axiom environment unchanged. Complete new-target regeneration, 12 typed Lean controls, three 12,232-case native/lifted corpora, five compiled Rust controls and all nine local gates passed. Existing full EasyCrypt replay evidence is reused after exact equality of 1,972 proof inputs and a fresh identity gate.

The source-lifting, SigningKey/backend interpretation and callback non-interference remain explicit translation/model boundaries. Forced receipt validation, physical backends and the full Rust/EasyCrypt session relation are not claimed closed. Initial unconditional guard-deletion probes hit a resource limit and remain inconclusive; they were not counted as semantic rejection. The final verification-result mutation is type-correct and rejected normally.

Landed on master at the exact reviewed commit above, through PR #843. Astra and Opus both returned GO within their 15-minute bounds, and all nine local gates and eight PR workflows passed. The full differential took 4,918 seconds. All six exact-commit post-push workflows passed; the post-push differential took 3882 seconds. The nonblocking upstream sentinel-provenance follow-up is banked as #844. Kimi remains excluded by owner instruction. Batch X is complete. The next bounded batch proves paired digest-field/wire-decoder representation endpoints as a component of the cross-language relation; research owner #295 and deferred combined assurance #509 remain open.

Batch Y landed through PR #845 on master at c2fab9704b54a4b67b807f8b7bb79badf5bf6bec / tree d8a1c7cfc96aba30615a0213e75629341a50df9d: paired Lean/EasyCrypt definitions and endpoint proofs for every 32-byte digest and complete 4,008-byte signature, including both full-width counters. Nine new kernel-only headlines bring the audit to 229. Astra and Opus returned GO on this exact candidate, and all nine local gates pass.

The prior complete-input replay was stopped after ObservedValueOpening failed its mandatory CLI proof even in the isolated recheck; its evidence remains failed, not reused as GREEN. The existing helper now spells out 512 <= 2^256 by power rewrites. Both drivers pass the correction in the exact pinned image at unchanged budgets, with no theorem-statement or assumption change. The fresh complete replay passed in 4,835.47 active seconds (80m35s), with unchanged inputs and a GREEN result. All eight exact-candidate PR workflows passed and the audited normal master push completed at 2026-10-12 12:32:30 UTC. All six exact-commit post-push workflows passed. The post-push differential completed in 4,710 seconds (78m30s), and its job/log audit passed. Batch Y is complete. The shared generator and cross-tool arithmetic/list interpretation remain explicit TCB; hash/caller, stateful session/oracle and wrapper query-cost relations remain open.

Banked nonblocking review cleanup under this owner: redundant /read_node unfolds in C10RepresentationBridge.ec. The proof builds and the tactic has no effect; removing it is optional cleanup, outside this frozen closure. The focused negative-control diagnostics have been checked against their intended lemmas; proof rejection alone is not claimed as a logical-falsity theorem.

Batch Z landed through PR #868 on master at 897c38489bc8fd97666339a888b9d9467a14ecb7 / tree 37c5dac00c8586edd445ae1625c07ca62fd9409b, based on the landed Y commit. Paired common preimages now cover H_msg, one-node/pair/multi-node hashing, WOTS digest inputs and R derivation. Full u32 encoding, the WOTS 32-byte counter slot, field order, node padding and both OptRand modes are retained. Production code is unchanged. The local audit passes all 244 headlines with the same 27-axiom environment; all nine local gates, 21 Lean typed rejections and 43 EasyCrypt control cases pass. Both bounded Astra/Opus source reviews returned GO. The fresh complete pinned EasyCrypt replay passed in 4,852.39 active seconds (80m52s), with unchanged inputs, all 665 proof targets and 719 controls, and a GREEN result. All seven applicable PR workflows passed, including the main CI transcription check; the dedicated transcription workflow was correctly path-filtered because all 13 inputs were unchanged. The audited normal master push completed at 2026-10-12 14:48:43 UTC. All five applicable exact-commit post-push workflows passed. The extracted-code differential completed in 4,978 seconds (82m58s), and the final job/log audit passed. Batch Z is complete.

Two nonblocking reviewer observations remain banked under the caller-composition frontier: (1) the new grinder corollary substitutes the common R preimage while retaining forsGrindDigest for H_msg; the separately proved H_msg endpoint still needs explicit caller composition, and (2) some EasyCrypt endpoints normalize the exact inline preimage expressions without a Hoare theorem at the call site. These are preimage-component results, with shared-generator/list/integer interpretation TCB; address construction, other private derivations, stateful oracle/session and wrapper-cost relations remain open. They do not justify an ideal-oracle or full Rust/session claim. Deferred #509/#789/#844 remain separate.

Batch AA is pending final validation in PR #895 at 271862886e411296f865e8bb37f669ededd31d38 / tree 403a61ee6610c706c3d1097106ec509c2e9c4d2a, based on 0b7ac3f35439d70cf87c790c4f6c9f8b39e7d512. Paired full-width address and WOTS/FORS private inputs add 12 kernel-only headlines (256 total, unchanged 27-axiom environment), nine EC lemmas and 32 typed layout mutations. Both EasyCrypt address-window equalities now compose with the existing field constructor. All nine local gates and all 65 focused EC control cases pass; unchanged Lean inputs retain the passing 32-mutation evidence. Astra and Opus both returned GO on this corrected snapshot within five minutes. Coordinator inspection confirmed the existing extracted chain-loop write-back theorem; no remaining merge-review blocker or mandatory gap is recorded.

The earlier snapshot's missing composition, Astra timeout and incomplete replay remain superseded receipts. The current full pinned replay and exact-candidate PR CI are running; AA is not yet on master. The guarded normal push requires those gates, the already-complete Z post-push audit, exact clean identity and unchanged remote master. Full caller/search/error composition, shuffle/callback interpretation, stateful oracle/session and wrapper query costs remain open; #509/#789/#844 remain deferred.

AA integration checkpoint (2026-10-12 17:17 UTC): the frozen PR's main CI failed the hardware-assumption ledger check on two identifiers in the upstream research reports. Reproduced locally; upstream commit 1a656023 already corrects both. Master has since moved to b87eb660, whose own CI run 38279325298 fails the canonical Safe transaction E2E assertion and detects two stale research bundles. These are integration blockers from the separately landed #846 work. The AA guarded push exited before changing master. The immutable AA full replay remains running in its final isolated checks; all nine local gates and both GO reviews remain valid for 27186288. Current upstream changes intersect none of the pinned EasyCrypt sources, extraction inputs or Lean inputs. A completed replay can be reused only after checking the full proof/toolchain identity of the eventual integrated candidate. No AA production-source edits or proof restart were made.

AA proof replay and integration checkpoint (2026-10-12): the complete pinned replay is GREEN at 271862886e411296f865e8bb37f669ededd31d38 / tree 403a61ee6610c706c3d1097106ec509c2e9c4d2a, taking 4,205.05 active seconds (70m05s), with no suspension and unchanged input identity 8bcd0fdf3d3fc114346da89c45cbd0f8. Its log SHA256 is 5925ad68f01ada67aa8b8ba54c4be256c29f60cee471247da276d718b56b01af.

Upstream corrected the report identifiers and #846 CI regressions. Integrated candidate e8c0c20257dd86f4890ca4c26daa4b3e606cdb02 passed all nine local gates, both bounded Astra/Opus reviews, and all seven exact-candidate PR workflows. The final differential took 6,331 seconds (105m31s). The guarded push stopped before changing master because independently landed commit e4a7a4ea110bbe9e647d325c07569ee3e86e2a0d added the #896 gateway hardware fixtures.

The new integration in PR #895 is 09f90de51415e680f4c852fa6a80b56305e91c16 / tree af6885e75c1216587ce95faedd779190d200c319, based on that latest master. The completed 70m05s EasyCrypt replay is preserved: all 2,709 proof/build/bound-source inputs are identical, and the fresh pinned identity gate passes. The only additional manifest delta is the root Makefile's hardware-only recipes and production denylist entry; the proof command directly loads the unchanged verification-directory Makefile. The explicit delta audit is retained; no full replay was restarted and no hardware command was run. All nine fresh local gates pass. Astra returned GO in 234 seconds and Opus in 206 seconds, with no findings or mandatory gaps. All seven exact-candidate PR workflows passed; the extracted-code differential took 3,949 seconds (65m49s), and the complete job/log audit passed. The guarded normal push landed this exact commit on master at 2026-10-13 09:39:54 UTC; PR #895 is merged. All five applicable exact-commit post-push workflows passed. The differential took 6,576 seconds (109m36s) and finished at 2026-10-13 11:31:03 UTC; the full job/log audit completed at 11:32:42 UTC. Batch AA is complete. Full caller/search/error composition, shuffle/callback interpretation, stateful oracle/session relations and wrapper query costs remain open; #509/#789/#844 remain deferred. AA has landed; both whole research issues remain open. Kimi remains excluded by owner instruction.

Batch AB (2026-10-13), commit f6447cb73011ea29459b727c5a87e20fc56938ec, PR #899: the actual EasyCrypt WOTS count/chain/recovery and nonce-grind procedures now have four common-input equivalences preserving results and arbitrary oracle global state, including full-width counters, zero sentinel and bounded exhaustion. Ten lemmas and 21 focused control outcomes pass; all nine local gates and six fresh host/curation/correspondence gates pass. The full pinned EasyCrypt replay completed before the reboot at 6fa65ad42ae458a667d39735c7c2ee1f8fa3c2c5 in 4291 active seconds (71m31s); its log checksum is c7237c1e899d4bd38cfac6f0fa76c79540e59b29d79e96d36f3cbf86ca00d903. Exact-input checks retain that engine evidence with 2,727 identical proof/build/source files and seven exact non-engine deltas audited. No replay was lost or restarted. The prior candidate passed all seven PR workflows, but its guarded push stopped when master advanced several commits. This snapshot integrates master at 3e2c7b8 and preserves its dependency correction. The two changed Rust inputs (aa/src/userop.rs and proto/src/lib.rs) were actually re-extracted; complete generated Lean outputs are unchanged. Only their two source hashes and the registry binding are refreshed, along with the generated research mirrors. The inherited Kani census is refreshed to 180 harnesses in 30 files and 45 mutation groups, without a new proof-execution claim. The protocol source-tree receipt is also refreshed in the catalogue manifest; production status bytes change only in its 32-byte manifest digest, with databases, roots and admission sets unchanged. All EasyCrypt sources, tools, source bindings and pinned engine identity remain unchanged. Astra and Opus returned GO in 234 and 209 seconds on the integrated proof snapshot f6447cb73011ea29459b727c5a87e20fc56938ec. This fresh wave covers the complete integrated candidate, including the generated Kani census/prose repair. All seven exact-candidate PR workflows and job/log audits passed. The guarded normal master push landed at 2026-10-13T21:59:45.672435+00:00. All five exact-commit postpush workflows and job/log audits passed at 2026-10-13T23:52:30.115352+00:00. Batch AB is complete. No new hash assumption or signing authority is introduced. Other keygen/signing callers, full Rust/session correspondence, concrete backends, callbacks, quantum games and wrapper query costs remain open in #100/#295. Optional fixture trigger symmetry is banked under #100: the broad easycrypt/** workflow already enforces source bindings and regeneration, so no present gate bypass was found. Automating the coordinator’s intended-theorem diagnostic check is also banked under #100; all ten current rejection locations were independently checked against their intended theorem, with source/log hashes revalidated. #509/#789/#844 remain deferred; Kimi remains excluded by owner instruction.

Batch AC — WOTS private-input caller correspondence: #913.

Draft candidate; full replay and exact-candidate CI must pass before landing. Candidate e6a6ea851ce7872a12352f1244e76b003db3dbd3 / tree 63b64571a14863de40c59a8b534a9ac5bb87388a.

The actual EasyCrypt WOTS leaf and signing callers now compose common private/count/chain/compression inputs, preserving results and the entire arbitrary oracle state. This retains full-width fields, count exhaustion, the exact shared shuffle, digit-dependent stops, signature placement and returned count. Nine lemmas, two headlines and eleven typed mutations are enrolled; no production source or cryptographic assumption changes.

Both EasyCrypt entry points, all 23 focused controls (11 typed definitions pass and 11 intended-theorem rejections), and nine frozen local gates passed. Fresh Astra ultra / Opus 5.5 xhigh reviews both returned GO. Their semantic review was source-only; reviewer static executions and coordinator proof executions are recorded separately. Full pinned replay passed in 4051.7 active seconds. Exact-candidate PR CI is pending.

Existing #100 follow-ups also cover this batch: automated intended-theorem diagnostic binding and narrow extraction-workflow fixture-path symmetry. Coordinator checked all eleven exact theorem locations; the blocking Lean FV workflow's broad easycrypt/** trigger enforces fixture fidelity/source binding. No new unguarded path was found, and these notes do not reopen the frozen batch.

Remaining FORS/tree/forest/layer/signer caller composition, cross-language control-flow/error/session relations, backend/callback interpretation and secure-wrapper query costs remain open. The exact shared shuffle is not a cross-language derivation proof. This is neither concrete-SHA idealization nor a deployed EUF-CMA/hardware/release claim. Issues #100 and #295 remain open; #509, #789 and #844 remain deferred.

Navigation Menu

Repository navigation

FV15-F6 — EasyCrypt C10 representability stop/go (research-only) #100

41 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

FV15-F6 — EasyCrypt C10 representability stop/go (research-only) #100

Description

Activity

Nicola-Ceornea commented on Jul 19, 2026

Nicola-Ceornea commented on Sep 17, 2026

Nicola-Ceornea commented on Sep 21, 2026

Nicola-Ceornea commented on Sep 21, 2026

Nicola-Ceornea commented on Sep 21, 2026

Nicola-Ceornea commented on Sep 21, 2026

Nicola-Ceornea commented on Sep 21, 2026

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

41 remaining items

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 9, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 10, 2026

Nicola-Ceornea commented on Oct 11, 2026

Nicola-Ceornea commented on Oct 13, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions