This repository was archived by the owner on Sep 12, 2026. It is now read-only.
Sphincs FV in ROM - #19
Merged
Merged
Conversation
Identify conditional target-completion sums with the expected number of newly covered targets, and specialize the identity to the concrete cached signer charge. Prove the exact occupancy increment on inserting a signing view and bound the actual signer increment by the uniform-index average plus weighted cached-answer reuse. Validation: full lake build passed (3948 jobs). Audited 425 declarations across 41 recent proof modules, including generated and private declarations, plus the public 120-, 125-, and 126-bit theorems. Only propext, Classical.choice, and Quot.sound occur. Global adaptive charge bounds and 127-bit SUF remain unproved.
Bound eligible-view occupancy by observed optional signing views, preserve those views under cache growth, and derive exact response-append counts. Prove the supported concrete signer update and its expected increment with cached-answer reuse retained. Lift the bound to one logged interpreter step and bound fresh message-query cover charges by the same observed-log occupancy. Validation: full lake build passed (3950 jobs). Audited 461 declarations across 43 recent proof modules, including private and generated declarations, and public 120-, 125-, and 126-bit theorems; only propext, Classical.choice, and Quot.sound occur. Global accumulated-cost bounds and 127-bit SUF remain unproved.
Connect the exact degree-14 binomial expansion and concrete signer recurrence to arbitrary adaptive executions. Retain failed signing attempts, transcript validity, cached-answer reuse, and the public whole-experiment cache budget. Validation: full lake build passed; 515 declarations and the public 120-, 125-, and 126-bit theorems use only propext, Classical.choice, and Quot.sound. The numerical allocation needed for 127-bit SUF remains open.
Prove the binomial completion recurrence and its empty-log value, then lift it through actual signing attempts and adaptive executions. Bound the initial degree-14 contribution by 7 * 2^40, leaving explicit propagated cached-reuse costs in the retained game. Validation: full lake build passed; 578 declarations and public security theorem axiom lists use only propext, Classical.choice, and Quot.sound. Cached-reuse bounds and adaptive security-charge allocation remain open for 127-bit SUF.
Freeze observed signing views at the signature limit and prove pathwise monotonicity through supported executions. Bound fresh world-query cover charges by frozen terminal occupancy, and preserve the same completion and cached-reuse bound without a terminal validity indicator. Validation: full lake build passed; 605 declarations and the public 120-, 125-, and 126-bit theorem axiom lists use only propext, Classical.choice, and Quot.sound. Numerical cached-reuse bounds and adaptive query-charge allocation remain open for 127-bit SUF.
Prove mass preservation and a terminal occupancy bound for accumulated world-query cover costs, following supported signer replies. Split the existing interleaved charge into world and signing parts and derive their budgets from the public experiment through verification. The security inequality now has an explicit 7*q/2^136 term plus accumulated signing and cached-reuse costs. Full lake build passed; 669 declarations and public security theorem axiom lists use only propext, Classical.choice, and Quot.sound. The remaining costs still need bounds to prove 127-bit SUF.
Exclude the target input from actual signer reuse charges and propagate the refined cost through the global cache-capacity inequality. Express reuse as a sum of input pairs, prove the fresh-source column identity, and bound newly covered targets by the occupancy increment. Full lake build passes. Audit of 964 declarations across 88 modules permits only propext, Classical.choice, and Quot.sound. Public 126-bit SUF remains proved; the numerical reuse bound for 127 bits remains open.
Lift the newly covered-target bound through all remaining uniform signing attempts. Split each fresh cache insertion into the new target row and source column, then prove their combined random-oracle expectation bound while retaining the future-coverage reserve. Full lake build passes. Audit of 999 declarations across 94 modules permits only propext, Classical.choice, and Quot.sound. Adaptive message choices, accumulated reuse, and the final 127-bit numerical allocation remain open.
Bound actual signer weights by all cached admissible message sources. Prove the input-based occupancy update and propagate both all-message reuse charges through the global cache-capacity inequality. Establish fresh target and occupancy arrival bounds for these same charges. Full lake build passes. Audit of 1026 declarations across 99 modules permits only propext, Classical.choice, and Quot.sound. Public 126-bit SUF remains proved; accumulated reuse and the 127-bit numerical allocation remain open.
Represent coverage changes as nonnegative expectations and combine reuse arrivals with unused-slot and slot-pair reserves. Prove domination of the existing per-signing reuse charge and nonincrease through actual adaptive world-oracle computations under supported terminal cache bounds. Full lake build passes. Audit of 1079 declarations across 105 modules permits only propext, Classical.choice, and Quot.sound. Signing-log growth, accumulated signing costs, and the final 127-bit numerical allocation remain open.
Prove a linear reserve that dominates the existing signing reuse charge, starts at zero without cached message inputs, and incurs costs only on fresh message queries. Compose the bound through supported adaptive world computations and bound its cost by the expected fresh message count. Express the uniform occupancy increment as a completed binomial polynomial, bound its actual signing update with an explicit reuse polynomial, and prove the empty-log increment is at most 2^21 at the signature limit. Full lake build passes. Audit of 1127 declarations across 111 modules permits only propext, Classical.choice, and Quot.sound. Target reuse through signing-log changes, accumulated signing reuse costs, and the final 127-bit allocation remain open.
Bound the actual signer using message-independent cached binomial moments. Prove exact degree shifts, signing bounds at every polynomial order, and vanishing from order fifteen onward. Derive exact cached polynomial growth through adaptive world computations with a fixed signing log. Identify the existing occupancy reuse charge with the first cached polynomial and the uniform-increment signing reuse term with the second. Full lake build passes; the audit of 1187 declarations across 118 modules permits only propext, Classical.choice, and Quot.sound. Cached polynomials across signing-log changes, target reuse, global accumulation, and the final 127-bit allocation remain open. The public theorem remains at 126 bits.
Prove actual signing bounds for arbitrary fixed index weights and specialize them to powers of cached multiplicities. Signing raises the cache power and derivative order; fresh message queries have exact expansions into lower powers. Decompose the actual terminal-cache signing moment into its frozen-source contribution and an explicit nonnegative growth term evaluated on the final log. The correlated growth term remains unbounded. Full lake build passes. Audit of 1235 declarations across 126 modules permits only propext, Classical.choice, and Quot.sound. The public security theorem remains 126 bits; correlated signing growth, target reuse, accumulation, and 127-bit allocation remain open.
Prove that every signing outcome introduces at most one new admissible message input, whose view is uniformly dominated even if signature assembly fails. Derive its exact cache-weight contribution and bound terminal-cache mixed growth by lower moments. Combine the growth estimate with the frozen-cache bound so the actual signing recurrence refers only to before-signing moments. Full lake build passes; the audit of 1270 declarations across 133 modules permits only propext, Classical.choice, and Quot.sound. The public theorem remains at 126 bits. Adaptive composition of the mixed recurrences, target reuse with input exclusions, and the final 127-bit numerical allocation remain open.
Prove a positive query-before-signing commutation identity and extend it through repeated operations and expectations. Account for fresh queries with unused cache slots and retain the signing-request cap, including Option signing failures. Bound terminal valid occupancy by the initial mixed envelope without an accumulated signing-reuse residual. The numerical envelope and target reuse remain open, so this does not establish 127-bit SUF. Validation: full lake build passed (4045 jobs). Axiom audit passed for 1331 declarations across 138 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Identify the explicit initial moment vector for an empty signing log and a cache with no message inputs. Prove that query and signing increments vanish beyond finite coordinate ranks, then apply the binomial theorem for additive endomorphisms to replace the large iteration counts. Connect the resulting 29-term signing expansion to the adaptive occupancy bound. Numerical certification and target reuse remain open; the public security theorem is still 126 bits. Validation: full lake build passed (4049 jobs). Axiom audit passed for 1388 declarations across 142 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove factorial coefficient bounds, increment monotonicity and scalar compatibility, and a uniform digest reuse-weight bound. Isolate the cache-power leading term exactly and bound lower query terms by a monomial remainder. For powers at most 14, bound the query envelope by 1025/1024 times the natural scale uniformly over q <= 2^127. The signing expression and target reuse remain open, so this is not a 127-bit SUF proof. Validation: full lake build passed (4052 jobs). Axiom audit passed for 1415 declarations across 145 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Dominate the reachable mixed signing coordinates by a scalar order recurrence, retaining the derivative tail and Option signing failures. Scale by the signing budget and apply factorial bounds, then prove the finite integer arithmetic certificate in the Lean kernel. Bound actual adaptive valid terminal occupancy by 29 * 2^43 under the supported terminal cache budget and no initial message-cache entries. Its uniform target scaling is at most (29/64) * 2^-127. Target reuse and the full SUF allocation remain open; this does not prove 127-bit SUF. Validation: full lake build passed (4058 jobs). Axiom audit passed for 1475 declarations across 150 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove exact uniform-target occupancy averages, monotone excluded-input reuse bounds, and fresh-query and actual Option signer recurrences. The adaptive target-reuse closure and full 127-bit SUF theorem remain open. Validation: full lake build passed (4064 jobs). Audited 1594 declarations across 156 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove decreasing tree-subset increments, exact block averages for arbitrary fixed view collections, and cache-product query recurrences retaining same-answer correlations. Normalize disjoint leaf factors to the index-space coefficient and connect the subset weights to the actual Option signer with target-input exclusions. Validation: full lake build passed (4071 jobs). The axiom audit checked 1667 declarations across 163 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem checks passed. Combined cache/signing moment closure, adaptive composition, and 127-bit SUF remain open.
Bound terminal cache and eligible-log products using only prior-state moments. Retain the shared selected source in joint cache/log growth, include failed signature assembly, and preserve target-input exclusions in signing reuse. Adaptive composition, fresh-target accounting, and full 127-bit SUF remain open. Validation: full lake build passed (4076 jobs). Audited 1717 declarations across 168 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed. No resource overrides or new-module warnings.
Preserve nonempty disjoint tree-group shapes, bound their rank by 28, prove query-before-signing domination, and truncate both operator powers to exact 29-term binomial sums. The concrete moment adapter, adaptive execution lift, fresh-target accounting, and full 127-bit SUF remain open. Validation: full lake build passed (4081 jobs). Audited 1811 declarations across 173 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed. No new resource settings or new-module warnings.
Identify the finite slot and group-set formulations of normalized target moments, and transport the actual Option signer and random-oracle bounds to the shape operators. Prove expectation interchange and continuation monotonicity, then compose the capped target envelope through arbitrary adaptive execution using remaining cache capacity and signing attempts. The fixed-target adaptive bound retains the target-input exclusion and supported terminal cache budget. Fresh-target arrival accounting, target-reuse numerics, and the final 127-bit SUF allocation remain open; the public theorem remains 126 bits. Validation: full lake build passed (4089 jobs). Audited 1873 declarations across 181 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove the uniform-target average for disjoint weighted source groups, preserving cache-input and signing-slot multiplicities. Instantiate it with the concrete target moments and use freshness to remove target-input exclusions only where justified. Project the valid shape operators and their iterates to cache-group and remaining-tree counts with exact binomial coefficients. The actual fresh target cache insertion now has an exact continuation average in this index envelope. Accumulated arrival accounting, reuse numerics, and the final 127-bit SUF allocation remain open; the public theorem remains 126 bits. Validation: full lake build passed (4097 jobs). Audited 1957 declarations across 189 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove the ordinary-power signing recurrence for the actual Option signer, including the correlated cache growth from its selected source. Connect the complete signing and query updates to the index operators. Compose the raw index envelope through arbitrary adaptive execution using remaining cache capacity and signing attempts. With an empty log and no cached message hashes, the initial bound is an explicit index envelope with a single nonzero initial coordinate. Its numerical connection to the existing occupancy certificate, accumulated target-arrival accounting, and the final 127-bit SUF allocation remain open. The public theorem remains 126 bits. Validation: full lake build passed (4107 jobs). Audited 2017 declarations across 199 modules, including generated and private declarations, allowing only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit theorem axiom checks passed.
Prove the exact finite-difference transform and reuse the existing numerical certificate. The public 126-bit SUF theorem remains proved; full 127-bit SUF still requires accumulated target accounting and final allocation. Validation: full Lean build passed (4112 jobs); axiom audit checked 2065 declarations across 204 modules, allowing only propext, Classical.choice, and Quot.sound.
Prove that every supported signing result consumes at least 1024 syntactic hash queries, including failures, and preserve the residual continuation budget. Bound the accumulated macro index charges by q times the initial envelope, giving the normalized factor 29/64 at 127 bits. Full 127-bit SUF remains open: newly admitted target rows must be connected to these charges and the final SUF allocation completed. The public 126-bit theorem is unchanged. Validation: full Lean build passed (4118 jobs). Axiom audit checked 2105 declarations across 210 modules, allowing only propext, Classical.choice, and Quot.sound.
…ounds Bound the certificate's original message work by the full original boundary message count, then identify that count with the existing reference allocation. Retained signing and verification work uses exactly the original game-rest cost; the comparison includes the key-generation contribution without needing an extra adversary premise. For q <= 3*2^114, combine the primitive probability and original full-certificate probability within (7/4 + 11/65536)*q/2^128 plus the explicit certificate exception probability. The complete SUF event decomposition, exception transfers and remaining FTS estimates are still open. Validation: full lake build passed (4177 jobs). Audit checked 20719 local declarations using only propext, Classical.choice and Quot.sound. All 1010 local modules are root reachable. Statement and the public 126-bit theorem are unchanged. No placeholders, additional axioms or checker-limit increases.
Freeze the cache weight at one after a recorded exception and telescope its expected increase through the actual adaptive signing and verification execution. The cache projection and message charge remain valid after the certificate monitor stops. Original key generation gives a zero initial weight. The actual certificate monitor's cache-history probability is at most original expected message work times the cache rate, and at most q/2^169 under the unchanged original hash bound. Absorb that charge into the shared message reservation: primitive probability plus original full-certificate probability is at most (7/4 + 11/65536)*q/2^128 plus only the proposal-prefix exception, for q <= 3*2^114. Remove the two superseded wrappers that left the cache exception explicit. The proposal-prefix estimate, FTS comparisons and full original-SUF decomposition remain open. The public security theorem stays at 126 bits. Validation: full lake build passed (4178 jobs). Audit checked 20746 local declarations using only propext, Classical.choice and Quot.sound. All 1011 local modules are root reachable. Statement is unchanged. No placeholders, additional axioms or checker-limit increases.
Prove that the original certificate monitor preserves the exponential prefix weight in expectation. Active signing uses the exact geometric length marginal, ordinary queries and inactive steps preserve the weight, and the supported monitor log stays within the signing cap even when signing fails. Project the result through the proposal and cache monitors and the original key-generation mixture. The actual proposal-prefix exception has probability at most 2^-700. For q <= 3*2^114, the primitive-event probability plus original full-certificate probability is now at most (7/4 + 11/65536)*q/2^128 + 2^-700, with the cache and proposal exceptions discharged. The full original-SUF probability decomposition and remaining FTS estimates are still open; the public theorem remains 126 bits. Validation: full lake build passed (4179 jobs). Audit checked 20760 local declarations using only propext, Classical.choice and Quot.sound. All 1012 local modules are root reachable. Statement is unchanged. No placeholders, additional axioms or checker-limit increases.
Retain the actual forgery, signing log and signing-boundary record in the original reference experiment. Prove exact verdict and full-trace projections to the existing contact and graph-context sources, preserving the primitive-event probability. Factor the verifier classification through an explicit adversary run and use that same retained run for the FTS alternatives, including signing-log validity. Original SUF success is now bounded by the existing primitive union plus the full-certificate, near-certificate/guess and two-guess alternatives on this joint source. The original certificate-cache transfer and the two remaining FTS probability estimates remain open. The full 127-bit theorem is not claimed. Statement.lean, the original game and budget, and the public 126-bit result are unchanged. Validation: full lake build passed (4180 jobs); axiom audit passed for all 20801 local declarations using only propext, Classical.choice and Quot.sound; all 1013 local modules remain root-reachable; focused theorem checks and git diff --check passed. No new axioms, placeholders or checker-limit increases.
Preserve the sampled key, actual forgery, signing log, verification result and message-query record jointly between the reference source and original random-oracle execution. Successful signing entries and verification provide every message row needed by a transcript certificate. Embed those rows in the original final cache and preserve certificate coverage with own-input exclusion intact. For q <= 3 * 2^114, derive original SUF probability at most (7/4 + 11/65536) q/2^128 + 2^-700 plus the retained near-certificate/undisclosed-guess and two-distinct-undisclosed-guesses probability. Those two estimates and final numerical assembly remain open; this does not prove the full 127-bit theorem. Validation: lake build completed all 4184 jobs. The axiom audit passed for 20869 local declarations with only propext, Classical.choice and Quot.sound. All 1017 local modules remain root reachable. Statement.lean and the public 126-bit theorem are unchanged. No proof escapes or checker-limit increases were introduced.
Add an adaptive secret-table interpreter that continues after true guesses and signing disclosures. Prove its exact product posterior and erasure law, preserve nonempty candidate sets, and retire guessed or disclosed coordinates. An active coordinate has at least N-q candidates after at most q probes, so its conditional true-guess probability is at most 1/(N-q). Repeated hits do not increase the distinct-guess count. Identify the original FTS key-generation prior with the interpreter's uniform table. Reproduce the original signing response, failure, selected view and boundary cost trace through its disclosure program, preserving the signing posterior and leaving guess/probe counters unchanged. The full external-query translation, original-budget transfer, forced-law coverage and two remaining FTS probability estimates are still open. This is a prerequisite for the 127-bit proof, not the completed theorem. Validation: lake build completed all 4186 jobs. The audit checked all 21023 local declarations using only propext, Classical.choice and Quot.sound. All 1019 local modules are root reachable. Statement.lean and the public 126-bit theorem remain unchanged. No proof escapes or checker-limit increases were introduced.
Preserve full hash replies, signing responses, signing logs, charged boundary work, and external and verifier traces in a secret-test and disclosure program. Specialize its public signing records to the existing reference experiment using an FTS-independent auxiliary handler and root. The original uniform FTS secret prior gives the same reference adversary output law as the continuing lazy interpreter. The fixed-secret correspondence also retains final verification. Original-budget charging, the connection from forgery witnesses to tracked guesses, and the near-certificate and two-guess probability estimates remain open. The public 127-bit theorem is not proved by this change. Validation: full lake build passed (4190 jobs); the axiom audit checked 21110 local declarations using only propext, Classical.choice, and Quot.sound; all 1023 local modules are root-reachable. The original Statement.lean and public 126-bit theorem are unchanged. No new axioms or checker-limit increases.
Bound every translated secret test by the retained signing and verification work. Each external hash query adds at most one test; signing disclosures add none. This accounting covers adaptive adversaries and the final verifier under both fixed-secret and lazy interpretations. Project the completed verdict and boundary record to the existing reference experiment and use its original HasHashQueryBound theorem. Every supported auxiliary seed and completed original-reference run satisfies 1212415 + retained work <= q and secret tests <= retained work. The fixed debit is the original key-generation cost. No alternate budget or extra security assumption is introduced. The witness-to-guess implications and two remaining FTS probability estimates are still open. Forced-test laws still need support containment and the required message/certificate kernels. Full 127-bit security is not proved by this milestone. Validation: full lake build passed (4192 jobs); the axiom audit checked 21172 local declarations using only propext, Classical.choice, and Quot.sound; all 1025 local modules are root-reachable. Statement.lean and the public 126-bit theorem are unchanged. No axioms, proof placeholders, or checker-limit increases were added.
Track guesses, retirements and successful signing disclosures throughout adaptive external queries and final verification. An uncovered true-secret query becomes a tracked guess. Two witnesses in distinct FTS trees imply at least two distinct guesses; a near-certificate witness preserves its certificate and places the omitted coordinate in the guess set. Discharge the signing-view premise using the original signing-origin theorem, then transfer the witness implications through the exact lazy posterior. The event-level statement retains the actual forgery, signing log, certificate boundary and combined external/verifier trace. Failed signing discloses no secrets. Full 127-bit security remains unfinished. The near-certificate/guess and two-distinct-guesses probability bounds, their retained-source transport and final assembly remain open. The statement, signing cap, hash budget and public 126-bit theorem are unchanged. Validation: lake build passed all 4195 jobs. The axiom audit checked 21248 local declarations against propext, Classical.choice and Quot.sound. All 1028 local modules remain root-reachable. Statement.lean retains blob 5e2627d.
Use a zero/one/two-guess potential for the continuing secret interpreter. Its supported terminal budget bounds the two-guess event by choose(q, 2)/(2^128-q)^2, hence x^2/(2*(1-x)^2) for x=q/2^128 below one. Preserve the joint retained forgery through auxiliary sampling and the exact secret-table posterior. Transfer the witness event to the interpreter's distinct-guess count and insert its probability bound into the original small-budget SUF reduction. The remaining probability term is the valid near-certificate/undisclosed-guess event. Full 127-bit security remains open. Validation: lake build passed all 4201 jobs; the axiom audit passed for 21308 local declarations with only propext, Classical.choice and Quot.sound. All 1034 local modules are root-reachable. Statement.lean is unchanged and the public 126-bit theorem still checks.
Force one eligible active secret test to hit while retaining every earlier test and all other transition kernels. Prove support containment in the original lazy interpreter and transfer the concrete completed reference program's original whole-experiment budget, including key generation and retained signing/verifier work. Carry transition likelihoods through arbitrary adaptive computations and erase the weights back to the forced law. The selected-hit subprobability law has exactly this weighted payoff, with zero weight on unreached or ineligible selected tests. For a position below q, bound every nonnegative terminal payoff by 1/(2^128-q) times its forced-law expectation. This supports the remaining near-certificate comparison without assuming independence. Update the retained proof plan to use single-test forcing. Forced-law message, signing and coverage kernels, the sum over test positions, and the final 127-bit assembly remain open. Validation: lake build passed all 4206 jobs; the axiom audit passed for 21400 local declarations with only propext, Classical.choice and Quot.sound. All 1039 local modules are root-reachable, updated documentation links resolve, and the new modules contain no proof placeholders or checker-limit overrides. Statement.lean is unchanged and the public 126-bit theorem still checks.
Sum the selected-hit subprobability laws over test positions while retaining arbitrary terminal payoffs. Transfer the retained near-guess witness through the exact secret-table posterior to a final valid-log certificate in the completed message record, then average the original sampling law. The original small-budget SUF bound now leaves only the sum of probabilities in forcedNearGame. This uses the original whole-experiment hash budget and adds no coverage hypothesis. Full 127-bit security remains open: each forced game's final certificate probability still needs its coverage bound, including certificates formed after a stopped monitor, followed by the small-budget arithmetic and public theorem assembly. Validation: lake build passed all 4212 jobs. The axiom audit passed for 21471 local declarations using only propext, Classical.choice and Quot.sound. All 1045 local modules are root-reachable; new modules contain no proof placeholders or checker-limit increases. Statement.lean and the public 126-bit theorem are unchanged. Local documentation links and git diff --check pass.
Express the forced secret interpreter and reference signer as adaptive query programs. Prove exact interpretation for every residual seed, then apply deferred table sampling to the completed program while preserving its record and secret-guess state. The actual forcedNearGame equals forcedNearDeferredGame, and supported deferred executions inherit the original whole-experiment hash budget. External message hashes and the signer's residual message path read the same table. A fresh message row receives a uniform full hash reply and is fixed in the table. The quantitative selected-view and cached-input estimates, proposal augmentation, final-certificate comparison including stopped-monitor cases, and public 127-bit assembly remain open. Update the retained proof plan to distinguish these obligations from the completed source and fresh-message transport. Validation: lake build passed all 4217 jobs. The axiom audit passed for 21571 local declarations using only propext, Classical.choice and Quot.sound. All 1050 local modules are root-reachable. The five new modules have no proof placeholders, checker-limit increases or build warnings. Statement.lean is unchanged; local documentation links and git diff --check pass.
The public theorem sphincs_has_127_bits_of_classical_security states HasClassicalSecurityBits scheme 127 for the unchanged scheme, SUF game, signing cap and whole-experiment hash budget. Budgets at least 3 * 2^114 were already covered by security127_of_large_budget; this commit closes every positive budget below that split. The forced FTS near-certificate game of each test position is bounded by monitoring its cached forced run with the certificate monitor of the retained residual chain: the deferred seed table becomes an explicit query cache, the monitor runs beside the cached interpreter with public key fields and the key-generation debit, erasing it recovers the forced run exactly, and the one-step bank potential bounds telescope to expected bank count at most expected creation cost. Each forced law carries its own rejected-proposal word with the proposal invariant preserved, so the creation cost is bounded by the terminal certificate price martingale. Run accounting gives cache rows, cache size, creation mass, spent count, signing log and bank completeness on supported runs, and passive cache and prefix flags bound the stopped-monitor case together with a Chebyshev tail for a short Poisson proposal pool. The resulting per-slot bound is 557 q / 2^128 plus 14 (2^-10 + q r_cache + 2^-700), which the small-budget arithmetic absorbs under q / 2^127 for 1 <= q <= 3 * 2^114. Validation: lake build in formal/sphincs succeeds, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the 127-bit and 126-bit public theorems. Each new module compiles in a few seconds standalone. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The 126-bit, 125-bit and 120-bit statements now follow from the 127-bit theorem, so the independent 126-bit route and every module or declaration unreachable from the public theorem are removed: 408 modules and about 108k lines. Reachability was computed from the proof terms of the public theorems; blocks that reachability cannot see (rfl simp lemmas, instances, names used only in simp lists) were kept by syntactic rules, and two proofs were rewritten to explicit simp only steps after their simp sets changed. Validation: lake build in formal/sphincs succeeds, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorems. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…s with a proof guide The modules under SphincsSecurity/Proof move into Base, Scheme, Hypertree, Ots, Fts, Reference, Residual and Forced, with Security127Completion at the root, so that the one-time signature lives in one directory with a documented interface into the rest of the proof. PROOF.md explains the route, the constants and what to re-prove if the one-time signature changes; README.md maps the layout; PAPER-127.md and the paper-127 notes and check scripts, which planned work that is now proved, are removed and remain in the Git history. Reach.lean is kept as the reachability audit used for pruning. The four remaining linter warnings are fixed. Validation: lake build in formal/sphincs succeeds, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorems. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Each removed import line named a module that another import of the same file already brings in transitively, so the loaded environment of every module is unchanged. Explicit Prelude imports are kept as the conventional anchor. Validation: lake build in formal/sphincs succeeds with no warnings, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorems. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The statement module keeps only what the claim depends on: parameters, types, byte layouts, the three algorithms, the experiment and SphincsSecurityStatement, the 127-bit claim. The legacy 120, 125 and 126 bit claims and securityBits are gone, and the layer, index and path arithmetic that used to be proved inside the statement moves to Proof/Scheme/StatementLemmas.lean next to the sealing lemmas, with the two unused path lemmas dropped. Validation: lake build in formal/sphincs succeeds with no warnings, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorem. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…dit component dependencies Taint.lean records, for every declaration, whether it references the one-time-signature, few-time-signature or hypertree definitions of Statement.lean directly or transitively. By that audit the AdaptiveChain and PartialChain modules never touch the scheme, so they move from Proof/Ots to Proof/Chains, and RawQueryMomentBound, which does, moves from Proof/Base to Proof/Scheme. PROOF.md gains a per-directory table of these dependency classes and the list of modules outside Proof/Ots that mention the one-time signature directly. Validation: lake build in formal/sphincs succeeds with no warnings, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorem. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
A module under thirty lines imported by exactly one other module is folded into that module as a section, kept whole inside its own namespace block so its local attributes and variables keep their scope, when its top level holds only imports, a module doc and complete namespace blocks and no private name clashes. Four small modules whose names are landmarks stay as they are. Validation: lake build in formal/sphincs succeeds with no warnings, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorem. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
PROOF.md now records why both budget routes are needed for the 127-bit target, what each costs in modules and lines, and the four ways to simplify further: accepting 126 bits, precomputing the key as the XMSS proof does, stating the scheme over an abstract one-time signature, and using one proposal model. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The refined route averaged near-certificate prices over a Poisson pool and paid a 2^-10 term for a short pool; it now uses the same uniform word of length fixedProposalLength as the crude route, whose thirteenth binomial moment is bounded by the existing Stirling moment lemma. The Poisson pool, its tail bound and its moment module are removed, the prefix stop rule keeps its own module, and the per-slot bound and the closing arithmetic lose the pool term. Validation: lake build in formal/sphincs succeeds with no warnings, including Audit.lean, which reports only propext, Classical.choice and Quot.sound for the public theorem. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
PROOF.md now names the modules that carry the consequences of the target-sum parameters, the neighbor counts, the derived marker rates, the two-edge rate, the total primitive coefficient and the byte-layout facts, so a parameter change of the one-time signature is a bounded list of re-proofs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
FewTime and Layer each carried one coercion lemma under a module doc describing pruned content, and Game only introduced gameRest for Secrets, so the lemmas move to ExtractFts, ExtractOts and Secrets. The guide's component table and route sizes are recomputed on the current tree: 618 proof modules, crude route 372 modules, refined route 246 more. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The tiny-module merges appended the merged modules' import lists, and a second pass finds thirty-four imports whose closure another import of the same module already provides. The shared prelude stays explicit where it is. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Statement.lean loses the traverseOption helper (sequenceFin in the Option monad does the same), the SignRequest alias, the layerHeight_le theorem (inlined into leafIndexAt and restated in StatementLemmas), and five scattered irreducible attributes, now one line at the end of the namespace; its module docs are shorter and carry no query-count estimates. The spec's security section said the Lean file states 120 bits with nothing proven; it now names the 127-bit theorem and its model, the abstract no longer marks the classical claim as to do, and the signing section says the loop need not compute the discarded top root, which is what the Lean signer does. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The root module now states the theorem and pins its axiom footprint with #guard_msgs, as XmssSecurity.lean does, so the separate Audit target goes away. The reachability and component-taint scripts move under scripts/, leaving the top level with the root module, Statement.lean and the proof directory. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
… docstrings One variable line replaces the monad binder every hashing algorithm repeated, the central definitions say which spec symbol they implement, the index-group type is IndexGroup rather than DigestTree, and the index types and the sampled key say what they contain. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…cstrings One variable line replaces the monad binder every hashing algorithm repeated, the five irreducible attributes are one line at the end of the namespace, the section headers match the SPHINCS statement, and the parameters, types, key, signature and algorithms say which spec symbol they implement. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
127 proven