Sphincs FV in ROM - #19
Open
TomWambsgans wants to merge 945 commits into
Open
Conversation
Connect the canonical boundary to the original retained verifier and combine the eight-unit private-witness bound with the five-unit ordinary-failure bound. Close the unchanged security statement through the grouped terminal endpoint and replace both native_decide calls with kernel-checked proofs. Validation: lake build passes. The final theorem depends only on propext, Classical.choice, and Quot.sound. The two new proof modules compiled in 1.7 and 1.9 seconds on this host.
Close the 125-bit classical random-oracle SUF bound for the existing scheme and game. Retain root and non-root selection probabilities in a common execution, combine diagnostic and residual bounds, and tighten the forest and structural collision accounting. Expose sphincs_has_125_bits_of_classical_security alongside the original 120-bit theorem. Document whole-experiment query accounting and the independent-secret model, which does not cover seed derivation or concrete BLAKE2s. Validation: lake build passed all 3162 jobs. The public theorem depends only on propext, Classical.choice and Quot.sound, with no sorryAx or custom security axioms. The statement audit confirms unchanged algorithms, parameters and game definitions.
Extend supporting probability bounds to the 2^126 query range and add conditional 126-bit assembly, refined query reserves, native execution couplings, and adaptive hidden-root sampling bounds. Retain the original public security statement and the proved 125-bit theorem. Separate roots copied into native state from auxiliary-only roots. Prove local materialization preservation and an encoding-root occurrence charge invariant under preloading, so early sampling cannot create an occurrence charge by itself. The 126-bit theorem is not complete. The local root-risk experiment still needs transport to original root production, the complete execution invariant must be established, and the residual forgery event must be covered within the shared reserve. Validation: lake build passed (3432 jobs); audited public theorems, conditional assembly, root-risk and materialization lemmas depend only on propext, Classical.choice and Quot.sound. No sorry, admit, custom axiom, native_decide or skipKernelTC occurs in the proof sources. git diff --check passed.
Prove root materialization throughout the original chronological native game and its query histories, including key generation, the signer, adversarial hash queries and verification. Equate the preload-invariant encoding-root occurrence charge with the existing charge and retain its joint reserve bound. Accumulate native root guesses in an observer with terminal root resolution. Prove resolution-order neutrality, identify the observer with the existing native trace, and derive the explicit uniform-preload equality for an initially fresh ensured target in a valid completable context. Retain completion guards, earlier guesses and pending-hit failures. The public theorem remains 125 bits. The 126-bit proof still needs specialization to the charged matching-guess event, connection to the local record-risk bound, and coverage of the residual forgery event. Validation: lake build passed (3439 jobs), all proof modules are in the public import closure, and git diff --check passed. Axiom audits of the public theorems and new materialization, reserve and sampling endpoints use only propext, Classical.choice and Quot.sound.
Preserve charged candidate selection through terminal root resolution and transfer hit and occurrence probabilities from compatible stored-root records. Bound terminal-filtered occurrence by the original native trace occurrence. Validated with a full lake build and standard-axiom audit of 25 declarations. Public security remains 125 bits; global occurrence accounting and residual forgery coverage for 126 bits remain open.
Prove that initialized key generation preserves freshness of non-top layer roots and leaves no pending or cached encoding guesses. Apply the charged cut risk bound to the actual retained continuation and average over key-generation outcomes. Validated with a full lake build and standard-axiom audit of 32 declarations. Public security remains 125 bits; global occurrence accounting and residual forgery coverage remain open.
The expected-growth bounds charged a full uniform view even when the signer selected a cached digest or exhausted its digest search. Keep the actual fresh-selection probability in admissible-cache growth, raw-index moments, new-target envelopes, transformed target costs and successful-signature input weights. Factor the common expectation argument once and retain the previous interfaces as corollaries. These proofs retain cache entries produced before a later Option signing failure. The final 127-bit allocation remains open. Validation: full lake build (4360 jobs) and an axiom audit including private and generated declarations, allowing only propext, Classical.choice and Quot.sound.
Propagate the actual probability of selecting a fresh digest through signer weights, index moments and the logged signing transition. Preserve the existing unweighted bounds as corollaries. Prove an exact nonfresh signing gap for future envelopes and retain it alongside the query commutation gap for the actual changing signer cache. This is an intermediate improvement; the full 127-bit SUF inequality remains open. Validation: lake build passed all 4361 jobs. The extended axiom audit checked 4336 declarations, including private and generated declarations, and found only propext, Classical.choice and Quot.sound. The public 120-, 125- and 126-bit theorem axiom checks also passed.
Retain the nonfresh selection and query commutation gaps in the capped remaining-budget signing envelope. Preserve the reduction when accounting for new targets, encoding pairs and signing execution refunds, and transport it through arbitrary adaptive computations with the existing query bound. Prove that the sampled signing gap fits inside the additional complete coverage refund. The cancellation uses a proved finite bound on the shared terminal potential and encoding charges. Derive an explicit global forgery bound retaining the gap alongside the net coverage refund, terminal retirement, double-parent credit and structural overlap. The final numerical inequality for 127-bit SUF remains open. Validation: lake build passed all 4364 jobs. The extended axiom audit checked 4374 declarations, including private and generated declarations, and found only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorem axiom checks passed. No proof holes, custom axioms, native_decide, unsafe declarations or option overrides were added.
Prove exact cached-selection probabilities from the expected number of reached digest attempts, and retain digest-search exhaustion in the normalization. Carry the exact coefficient into successful signer input weights and prove it is bounded by the existing query-budget coefficient. Preserve the old signer interfaces. Full lake build passed (4369 jobs). The extended axiom audit passed, including the new lemmas and public 120-, 125- and 126-bit theorems, with only propext, Classical.choice and Quot.sound. The full 127-bit SUF bound remains open.
Generalize the signer moment bounds to accept a proved reuse coefficient and specialize them to the actual digest-selection coefficient. Retain both the missing fresh-selection contribution and the excess of the old reuse coefficient in the remaining-budget signing gap, including its adaptive and sampled global refund bounds. Prove a quantitative lower bound using the actual admissible-cache count and retain exhaustion explicitly. Full lake build passed (4371 jobs). The extended axiom audit checked 4444 declarations with only propext, Classical.choice and Quot.sound, including the public 120-, 125- and 126-bit theorems. The full 127-bit SUF allocation remains open.
Relate reached digest attempts to actual fresh-selection probability, retaining cached stopping and exhaustion. Bound the nonfresh probability below by A/(A+2^118), where A counts admissible cached inputs for the current message. Carry the resulting whole-increment signing refund through adaptive execution and sampling into the combined forgery inequality. Full lake build passed (4374 jobs). The extended axiom audit checked 4480 declarations with only propext, Classical.choice and Quot.sound, including the public 120-, 125- and 126-bit theorems. The full 127-bit numerical allocation remains open.
Split cached signer weight into inputs matching the requested key, root and message, and their complement. Retain exact digest reuse weight times that complement through weighted moments and the raw-index signing envelope. Include the additional nonnegative gap in the existing remaining-signing refund, so the adaptive and sampled global bounds preserve it alongside the nonfresh, reuse and commutation gaps. Adjust the cached-selection lower bound for the enlarged refund. The concrete algorithms, SUF game and whole-experiment query bound are unchanged. The final 127-bit numerical allocation remains open. Validation: full lake build passed (4377 jobs). Extended axiom audit passed for 4495 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No proof holes, custom axioms or resource-option increases were added.
Bound the combined signing gaps below by A/(A+C) times the full signing increment envelope plus R_other/(A+C), where A counts admissible cached inputs for the requested key, root and message, C=2^118, and R_other is the envelope of unmatched cached weight. Carry this stronger credit through the existing adaptive and sampled cached-selection bounds into the global SUF inequality. Prove that A=0 forces all cached signer weight to be unmatched and that the exact reuse and unmatched gaps then recover the full coarse reuse contribution. The scalar mixture argument retains finite-loop selection probabilities and actual failures; it does not restrict the security game. The final 127-bit numerical allocation remains open. Validation: full lake build passed (4378 jobs). Extended axiom audit passed for 4508 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No new axioms, proof holes or resource/transparency options.
Prove the exact randomizer cache-hit probability from all cached inputs matching the requested key, root and message. Bound fresh digest selection by exact reuse weight times S=(1-C_all/2^128)*2^118, retaining the actual finite retry loop and failures. Replace the coarse 2^118 denominator in the cached selection and unmatched reuse refunds by S. Prove its positivity in the existing cache-budget range, inverse domination by the coarse reuse weight, and comparison with the previous refund. The stronger credit propagates through the existing adaptive and sampled bounds to the global SUF inequality. The scheme and query accounting are unchanged; the final 127-bit numerical allocation remains open. Validation: full lake build passed (4380 jobs). Extended axiom audit passed for 4535 declarations including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No new proof holes, axioms or resource/transparency options.
Bound the exact digest reuse coefficient by D / (1 + A * D) using the finite signing-loop selection mass. Combine it with the unmatched-cache credit and carry the stronger refund through the SUF bound. Prove that it dominates the previous refund and recovers the full coarse reuse contribution when the message has no admissible cached digest. Validation: lake build completed successfully (4381 jobs). Audited 4554 declarations, including generated and private declarations, with only propext, Classical.choice and Quot.sound dependencies. The public 120-bit, 125-bit and 126-bit theorems pass explicit axiom checks. The full 127-bit bound remains open.
Use the shared probability mass of fresh selection and cached reuse to lower-bound their combined envelope gap. Take the stronger of this joint credit and the existing normalized credit, and carry it through the adaptive SUF bound without adding it independently to the underlying refund. Preserve the exact full-reuse refund when the requested message has no admissible cached digest. Validation: lake build succeeded (4382 jobs). Audited 4563 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound dependencies. Explicit axiom checks passed for the public 120-bit, 125-bit and 126-bit theorems. The full 127-bit numerical allocation remains open.
Bound the fresh digest hazard by the cache entries for the requested root and message plus the remaining attempts. Normalize with the admissible count and carry the stronger reuse credit through the existing adaptive SUF bound. Prove exact cache-count updates, a closed reciprocal formula, and a near-uniform reuse bound conditional on a bounded admissible-count deficit. Validation: lake build completed successfully (4386 jobs). Audited 4609 declarations, including generated and private declarations, with only propext, Classical.choice and Quot.sound dependencies. Public 120-bit, 125-bit and 126-bit theorem axiom checks passed. The deficit probability and full 127-bit numerical allocation remain open.
Prove a budget-dependent potential bound for the existing exception monitor, then derive a q/2^223 bound from second- and fourth-moment growth conditions. The monitor retains the first exceptional query even if later cache entries remove the deficit. Prove the positive-part moment inequalities for increments +1 and -1023 with admissibility probability 1/1024. These are auxiliary results. The cache-moment hypotheses and integration into the 127-bit SUF bound remain open. The concrete scheme, game, and public security statements are unchanged. Validation: full lake build and an axiom audit covering the new modules plus the existing audited reduction; only propext, Classical.choice, and Quot.sound.
Prove second- and fourth-moment growth for the actual message cache counts. Each fresh query changes at most one message bucket, with the concrete admissibility probability. Bound the probability of ever exceeding the admissible-count deficit threshold by q/2^223 under the original whole-experiment hash query bound. Carry the bound through key generation and secret sampling. Prove that the monitored experiment projects to the original SUF game, and derive the tighter digest-reuse bound on monitored prefixes without an exception. The full 127-bit inequality remains open; the scheme and public security statements are unchanged. Validation: full lake build (4396 jobs); audit of 4697 declarations, including private/generated declarations and explicit public120/125/126 checks, with only propext, Classical.choice, and Quot.sound. No proof holes or resource-option changes in the new modules.
Bound raw index moments on executions that have not triggered a message-deficit exception. Parameterize the envelope by the reuse weight and debit the original syntactic hash-query budget across adaptive hash and signing requests. Instantiate the reuse weight with the proved clean-cache estimate, retain the signing cap and failure flags, and reduce the initial envelope to the existing index-moment calculation. Generalize the cache exception invariant to any monitor that detects the exceptional cache condition, preserving its existing interfaces. The public algorithms, SUF game and security statements are unchanged. The full 127-bit SUF theorem remains open; the new coverage calculation still needs to be combined with the forgery reduction and its query credits. Validation: full lake build; expanded axiom-dependency audit including private and generated declarations and the public 120-, 125- and 126-bit endpoints; source and whitespace checks. Only propext, Classical.choice and Quot.sound are permitted by the audit.
The clean-cache digest reuse estimate now bounds the actual cached-target coverage event across adaptive signing and hash requests. Parameterize the target moments and envelopes by reuse, retain exclusion of the target's own input, and carry the tighter estimate through the original remaining-query budget. Preserve unused-query credits, budget and signing execution gaps, terminal reserves, and potential discarded on exceptions or failures. Specialize the adaptive bound to the union of an existing exception and the message-deficit exception. Express the initial charge through initialNearUniformRawIndexRate for the next numerical bound and reduction step. Factor out a fixed-budget raw signing lemma while preserving its previous interface. Public algorithms, the SUF game, and the 120-, 125- and 126-bit statements are unchanged. Full 127-bit SUF remains open: the new numerical rate and its integration with the final forgery inequality still need proof. Validation: full lake build passed 4411 jobs; expanded axiom audit passed 4817 declarations, including private and generated declarations, plus explicit public and new endpoints. Dependencies were limited to propext, Classical.choice and Quot.sound. Source and whitespace checks passed with no new proof options or warnings.
Bound initialNearUniformRawIndexRate by 3/(16*2^128) using the proved near-uniform digest reuse weight. Carry the mixed-moment domination through a finite factorial envelope and discharge the common-denominator integer certificate with kernel decide. Apply the numerical bound to adaptive cached-target coverage while retaining the unused-budget and discard credits. Prove an adaptive union bound for exception monitors and project the exception flag of runWithFailure back to the original expanded oracle execution. Adding the message-deficit exception increases its probability by at most q/2^223, without assuming that the internal couplings for the two exceptions coincide. The public scheme, SUF game, and 120-, 125- and 126-bit statements are unchanged. Full 127-bit SUF remains open: parent-record lemmas that require every exception to be a parent settlement need an appropriate extension, and the final query-credit inequality still needs proof. Validation: full lake build passed 4418 jobs; expanded audit passed 4863 declarations including private and generated declarations, plus explicit public and new endpoints. Axiom dependencies were limited to propext, Classical.choice and Quot.sound. Source and whitespace checks passed with no added proof options or new warnings.
Adding the digest-deficit exception invalidates the old premise that every first exception settles a structural parent. Prove that a nonmessage first record of the combined monitor, starting from a clean cache, is supported by the original parent monitor with the same record and final result. Carry the OTS record bound into the combined run's shared failure probability without equating the two runs' internal frames or failure flags. Extend the stopped potential argument with its clean-cache invariant. The collision structural potential retains its pre-exception charge under the combined monitor, and the shared-failure step adds only an explicit first-message-record probability. Bound that selected record event by the original deficit monitor and its q/2^223 concentration bound. Full lake build passed (4425 jobs). Expanded axiom audit checked 4895 declarations, including private and generated declarations, using only propext, Classical.choice and Quot.sound. New modules have no proof holes, custom axioms, native_decide, unsafe code or resource-option increases. Public algorithms, game and proved 120/125/126 endpoints are unchanged. Full 127-bit SUF remains open: adaptive accumulation of the selected deficit charge and the final query-credit inequality remain to be proved.
Prove an exact bind identity for the first selected exception. Use the original monitor marginal of each joint step to carry the digest-deficit term through the full adaptive run as one first-record probability, then bound it by q/2^223 under the original expanded hash-query budget. Initialize the deficit detector with the actual generated root. Prove that the resulting joint run projects to the original retained game, derive its structural-failure bound, and decompose the original game's success probability into shared failure, structural charge, the existing live nonsecret residual and the single deficit term. The public algorithms, game and proved 120/125/126 endpoints are unchanged. Full lake build passed (4429 jobs). The final expanded axiom audit checked 4930 declarations, including private and generated declarations, using only propext, Classical.choice and Quot.sound. New modules have no proof holes, custom axioms, native_decide, unsafe code or resource-option increases. Full 127-bit SUF remains open: sampled shared-failure and coverage/refund integration and the final query-credit inequality remain to be proved.
Bound future cache growth using generic binomial factorial moments, then give the remaining signing operator a stochastic interpretation under its reachable rate bound. Instantiate the comparison with the existing reuse rate and compare it with a uniformly sampled proposal suffix appended to a consumed prefix. The endpoint uses the original raw envelope, signing cap, and explicit cache and proposal prefix hypotheses. The adaptive original-game coupling and certificate charging remain open. The scheme and public security statements are unchanged. Validation: lake build passed (4435 jobs). The new boundary endpoint and public 120-, 125-, and 126-bit theorems have only propext, Classical.choice, and Quot.sound in their printed axiom dependencies.
Construct normalized geometric rejected words and prove that the bridge retains the original record marginal. Prove its exact density and equality to a kernel that accepts a record or emits a rejection and continues. The proposal marginal equals the prescribed base law. Show that adaptive record transitions preserve every finite independent proposal-word distribution. Instantiate the acceptance probability and index cap from the 127-bit paper route and identify the result with the existing uniform-word sampler. The original signing-history instantiation, stopping estimates, and coverage certificate charging remain open. The scheme and public security statements are unchanged. Validation: lake build passed (4438 jobs). Printed axiom dependencies of the new bridge, adaptive word, previous raw-envelope endpoint, and public 126-bit theorem contain only propext, Classical.choice, and Quot.sound.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
126 bits security proven, now working for 127