diff --git a/research/selected-bootstrap-reserve-composition/README.md b/research/selected-bootstrap-reserve-composition/README.md new file mode 100644 index 0000000000..4cda661b8a --- /dev/null +++ b/research/selected-bootstrap-reserve-composition/README.md @@ -0,0 +1,204 @@ +# Later selected bootstrap stages do not multiply external leaf stock + +This is an independent conditional composition audit, not a new stock formula. +The retained PR185/PR387 argument and the pending [PR2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084)/[PR2120](https://github.com/CrocSwap/integer-mult-bounds/pull/2120) +stock arguments imply that stages 2 through 7 need no additional external +leaf factor **if each preceding ordinary callee is internally completed at +all widths, with pointwise row and complete-spectator restoration**. +The same conditional parent coefficient, 6748 from PR2120, then suffices for +all fourteen recorded native/conservative fit guards. This does not establish +that an actual selected implementation meets those hypotheses. + +The added evidence is a separately implemented nested-borrowing regression and +an explicit stagewise endpoint/space induction. A fault that negates an outer +row after each of the two body calls passes the whole completed endpoint, +because the negations cancel. In the explicit F3, stage-two, width-four +witness, an initial row value 1 becomes 2 after the first body return and +returns to 1 after the second. It fails the individual child-return contract +required to reuse the parent's stock. Thus checking only the final two-call +endpoint cannot establish this stock induction. This is a countermodel to a +weakened premise, not a bug report against the selected implementation. + +No new exponent, supplier admission, changed cutoff or selected-frontier +change is claimed. The fourteen guard comparisons corroborate predecessor +arithmetic; they are not the contribution's novelty. + +## Exact source and overlap boundary + +Scientific base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +The selected record binds PR1094's assembly and its PR589 BIT receipt. +The ordinary producer is **BIT m=64, maximum child rank 42**, not the separate +complex m=73 supplier that constrains the common atom exponent. +The BIT receipt has 28,416 live and 28,425 physical roles. + +The source-pinned PR1087 assembler is read, not executed. Its seven updates +and both branch inputs reproduce the recorded exponents, gaps and cutoffs. +The retained PR185 proof's sections "Required completed leaf contract" and +"Nested row restoration and fixed tapes" supply the precise completed-leaf +hypothesis. PR387 extends that argument to a fixed number of stages and +explicitly says that the external allowance 252 is not an internal reserve +estimate. Neither 252 nor the historical m=120 increment 57,604 is used here. + +Pending sources are frozen byte-for-byte under `sources/`, with their original +credit and notices retained: + +| Source | Exact head | Used scope | +| --- | --- | --- | +| Adam Gall, PR2084 | `8001a23b003bec5dff5e61edec907b652c475932` | Conditional GL64 packet and completed-leaf stock argument | +| Nick Petalas, PR2120 | `378593574261e0b0915e7e8a83147aa640274fc8` | Conditional coefficient 6748 and ceiling-free depth bound | + +These sources already state the generic fixed-stage reuse argument. This +package independently audits it; it does not claim that argument as new. +[PR2183](https://github.com/CrocSwap/integer-mult-bounds/pull/2183) separates +later-stage completion from first-stage arithmetic. +The replacement-caller work in PR2234, callee-substitution PR2399 at +`14458fda3cac4441c27980d584582ebbbb3e9233`, and spectator-completion PR2457 at +`0362534712dca8639917a733be62840d5ce55978` are complementary proposals, not +admitted implementations of the retained fourteen stages. Their checkers +are not imported, executed or certified here. + +## Conditional endpoint/space closure + +Fix an eligible prime `q>2^80` and a finite bootstrap depth `J<=7` before +choosing input widths. Use one native or conservative branch at a time. +For each stage set `w=ceil(e^s)` using its branch's fixed selected `s`. +Retain the following hypotheses, separately from any time estimate. + +1. `A0` is an ordinary interchange for every required width. It accepts two + complete chunks and arbitrary complete spectators, returns every external + row coordinate pointwise, and obtains its own borrowing internally. Its + additional externally supplied row divisor is one. +2. The same selected full-cover constructor is available at every fixed stage. + For fixed atom width w it has floor-child bound `42*floor(n/64)`, terminates + below 64 atoms, preserves exposed ancestors, and restores each child's row + before the next child uses it. Its complete physical packet divisor is + `W_q(w)=28425*|GL64(F_q)|*q^(4096*(w-1))`. +3. Once the borrowed stock fits, this constructor's ordinary wrapper has its + stated endpoint using only already completed previous-stage ordinary + calls for leaves, routing, remainders and high-part exchange. Padding is + removed only after a completed endpoint preserves the genuine rectangle. + This is a uniform endpoint contract, not merely an eventual asymptotic + statement. All required complete-spectator/radix conversions are included. + +Let `D(n)=0` below 64 and `D(n)=1+D(42*floor(n/64))` otherwise. Choose the +parent's divisible stock from the original width before choosing the borrowed +width or body: + +``` +S(e,w) = W_q(w)^D(e). +``` + +At a node, expose one packet and pass its quotient to a child. Every child +needs at most one lower power. Since that child restores the supplied row, +siblings and successive residuals reuse the same quotient. At an ordinary +leaf the external factor is one by hypothesis 1, or its inductive successor. +Neither the two wrapper calls nor the number of bootstrap stages multiplies +this external divisor. This says nothing about the leaf's internal workspace, +number of tapes, padding/time constants or recursion cost. + +For each `j=1,...,J`, define `Aj` to use the new constructor above its recorded +cutoff and `A(j-1)` below it. Suppose `A(j-1)` is internally completed at all +widths. The packet induction supplies exactly the same `S(e,w)` as at stage +one. The inherited bound from PR2120 is + +``` +log_q S(e,w) <= 6748*w*(1+log2 e). +``` + +The recorded cutoff satisfies the sufficient fit guard with +`ell=ceil(log2(8*6748))=16`. Therefore stock fits above that cutoff. +Hypothesis 3 completes that branch, while `A(j-1)` completes the below-cutoff +branch. Thus `Aj` has the same all-width endpoint/space contract and zero +additional external factor. Induction proves this for every `j<=J`. +Coarse calls strictly decrease n; ordinary calls strictly decrease j. The +construction has no circular dependency on its own completion. + +The numerical checks reconstruct, for each branch, + +``` +a0 = 384599/10^10 +s = min(bit_lower, (1-10^-24)*complex_lower) - 10^-27 +a_j = (1-s)*s + s*a_(j-1) +delta_j = min(s-a_j, 1-a_j-s, 1-a_j-s*(1-a_(j-1)), 1-s) +L_j = max(ceil(36/delta_j^2), ceil(1032/delta_j)). +``` + +They verify the source records and `L_j>=3`, `L_j*delta_j^2>=36`, +`L_j*delta_j>=2*(4+16)`, and `02^80`, avoiding the selected recipe's finite denominator/rank exclusions, before choosing the widths. Let `e,w` be positive integers and let the coarse atom count satisfy `0<=n<=e`; at the native stage of interest `w=ceil(e^s)` and the body has at most `floor(e/w)` atoms. + +The proof uses the following inherited interfaces explicitly: + +1. **Selected full-cover realization.** The selected `m=64` finite physical recipe is realized over `GL_64(Z/q^w Z)`, with one fresh complete physical-role packet per active coarse level. Its role packet has `P=28425` slots, including work roles. A sufficient level divisor is + `W_q(w)=P*|GL_64(F_q)|*q^(4096*(w-1))`. + The selected all-size/compiler and hosting assumptions are still required to identify these packet slots with the physical word. A finite receipt alone does not construct that identification. +2. **Fixed atom width along a coarse call.** An internal child has atom count at most `r*floor(n/64)`, where `r<=42`; the conservative bad-class compiler has children at most `floor(n/64)`. Calls with `n<64`, peeled remainders, routing and high-part exchanges use completed ordinary operations, rather than another same-level coarse call. +3. **Fresh fields and restoration.** A child can use only the unused quotient of its parent's row packet; already exposed ancestor fields remain complete spectators. Every child returns its supplied row coordinate unchanged. Successive residuals, the two-call ordinary wrapper and other sequential calls reuse restored stock. +4. **Completed leaves.** The previous ordinary algorithm handles all required widths and complete spectators, borrows its own high digits internally and restores its row coordinate. It needs **no additional externally supplied row factor**. This is the reviewed PR185 contract retained by PR387, not an estimate of the leaf's internal memory or running time. + +The generic full-cover cardinality and fixed-width recurrence are in `three-stage-cover-bit.tex`, lines 197–218 and 253–264. That file's displayed geometry is historical `m=67`; its numerical parameters are **not** copied. The present proof derives the cardinality identity for general `m`, then instantiates the selected `m=64` recipe under hypothesis 1. The reviewed PR185 proof, paragraphs “Nested row restoration and fixed tapes”, provides hypothesis 4. The original rows note's inherited old-leaf factor must not be retained a second time when its use is replaced by this stronger completed interface. + +## Reserve theorem + +### 1. Charge the entire level divisor + +Reduction modulo `q` maps `GL_m(Z/q^w Z)` onto `GL_m(F_q)`. Every invertible residue matrix has exactly `q^(m^2*(w-1))` lifts; a matrix over this local ring is invertible exactly when its reduction is. Consequently + +\[ +|GL_m(\mathbb Z/q^w\mathbb Z)| +=|GL_m(\mathbb F_q)|q^{m^2(w-1)}=2`, + +\[ +D(n)\le2\lceil\log_2 n\rceil; +\] + +for `n=0,1` it is zero. Thus in all cases with `n<=e`, + +\[ +D(n)\le2\lceil\log_2\max(1,e)\rceil +\le2(1+\log_2 e). \tag{2} +\] + +No unnamed additive `O(1)` is used. One-level halving is false: `n=128` permits the selected rank-42 child `84>64`. + +### 3. Construct divisible stock, not a product over all calls + +For the same fixed `w`, define + +\[ +S(n,w)=W_q(w)^{D(n)}. +\] + +At a coarse node with depth `d>0`, split a complete row index into its role remainder modulo `W_q(w)` and an unused quotient of size `W_q(w)^(d-1)`. Every child has depth at most `d-1`, so that quotient is divisible by its required reserve. Any excess quotient is an additional complete spectator. Because the child restores its row, the quotient can be reused for each later child. The node's complete endpoint restores its own exposed role field. Induction supplies all nested calls and restores the entire row. + +At a leaf there is no external factor: the ordinary operation supplies its own borrowing under hypothesis 4. Consequently the recurrence is multiplication by **one level divisor along an active path**, not multiplication over siblings, residuals, the two wrapper calls, or bootstrap levels. This is also why the previous ordinary **time** constant does not enter the reserve. If a leaf instead needs external factor `B>1`, the base case becomes `S_leaf=B`; the zero-external conclusion no longer follows. That is a genuine hypothesis, not something finite examples can infer. + +Combining (1) and (2), for the parent construction at every integer `e,w>=1`, + +\[ +\log_q S(n,w)<4097wD(n) +\le8194w(1+\log_2 e). +\] + +Use non-strict `<=` to include the zero-depth case. This is PR1965's H3 with **sigma=8194** under the stated interfaces. At fixed completed bootstrap depth the same proof can be reused, but this package binds and checks only the first native stage. It does not claim a new implementation or all fourteen independently admitted stages. + +## First native cutoff + +From the selected assembly, with exact rational arithmetic, + +``` +s = min(bit_lower, (1-10^-24)*complex_lower) - 10^-27 +a0 = 384599/10^10 +a1 = (1-s)*s + s*a0 +delta = min(s-a1, 1-a1-s, 1-a1-s*(1-a0), 1-s) +L = 4785575287428 +``` + +The independently derived coefficient needs only `ell=ceil(log2(8*8194))=17`. The exact checks prove + +``` +L >= 2 +L*delta^2 >= 36 +L*delta >= 2*(4+17) = 42 +0 < delta <= 1-s +``` + +These are PR1965's sufficient fit premises, so `k=ceil(log_q S(e,w))=2^L`, with `w=ceil(e^s)`. The inherited sufficient-headroom value `floor(L*delta/2)-4=6562783` is included only to show the comparison; it is predecessor arithmetic, not the novelty. The powers `2^L` and huge stock sizes are not materialized. + +This closes the *numerical parent-stock coefficient implication* at this stage under the explicit full-cover/completed-leaf assumptions. H2's cutoff-independent stopped time bound, any other primitive fit condition, and all selected all-size/compiler, common-label, mutable-source, hosting, precision/tape, exact-recovery and analytic obligations remain. The selected result and frozen proofs are unchanged. + +## Reproduction and evidence + +From the repository root, using standard-library CPython 3.12: + +```sh +uv run --python 3.12 --no-project python -I -B research/selected-bit-parent-reserve/verify.py +uv run --python 3.12 --no-project python -I -O -B research/selected-bit-parent-reserve/test_verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-bit-parent-reserve +``` + +The verifier authenticates every external input before reading its semantic fields and authenticates the archive member before parsing it. No predecessor Python is imported or executed. It derives the selected parameters, complete level charge, exact halving and cutoff comparison; independently checks the floor-depth recurrence over 20,001 atom counts; and uses small exact local-ring matrices and row permutations as finite controls for the proof's failure modes. Acceptance uses explicit exceptions, not removable `assert` statements. The regenerated `RESULT.json` payload must compare canonically with the committed one. `--write-result PATH` creates an external receipt and refuses overwrite. + +The finite fixtures support the argument but do not prove its all-width quantifiers; those are proved above. Neither a complete selected cold replay nor a formal kernel is run here. See [TASK.json](TASK.json) for scope, provenance and open questions, [SELECTION.json](SELECTION.json) for the unchanged selection, and [SOURCES.json](SOURCES.json) for exact byte pins. + +## Open next questions + +1. **Realize the retained interfaces.** Construct the selected all-size GL64 role-packet/compiler map with fresh descendant fields and complete spectator preservation. Begin with one parent/child split and the common-label/mutable-source mapping. This would replace hypothesis 1's inherited implementation assumption; the finite cardinality proof cannot do so. +2. **Complete the time implication.** Trace every routing, padding, weighted-leaf, descriptor and high-part-exchange toll to prove H2 whenever stock fits with a cutoff-independent constant. The first step is an explicit quantified stopped recurrence. H3 alone cannot adopt PR1965's outer-proof repair. + +## Attribution and limits + +DreamingOfClouds supplied the selected tuned P111 word and parameterized PR589 pipeline, on eumemic's PR555 base and DreamingOfClouds' PR510 nine-stage work, with the credited geometry, whole-call hosting and compiler lineage. The finite-cover/local-ring and reviewed PR185/PR387 completed-leaf sources supply the retained interfaces. Josie Elliston's PR1956 and PR1965 isolate the carried-constant problem and time/space repair; ToikY's PR1990 independently checks the headroom and insists on the missing selected-source coefficient. Rohan Arun supplied the selected PR1094 assembly on Jeremy Kothe's PR1087 predecessor. Their results and numerical receipts are not claimed as new. + +Prepared by Adam Gall with substantial OpenAI Codex assistance. No independent human review or unconditional multiplication theorem is claimed. Apache-2.0, following the repository and retained source notices. diff --git a/research/selected-bootstrap-reserve-composition/sources/pr2120-README.md b/research/selected-bootstrap-reserve-composition/sources/pr2120-README.md new file mode 100644 index 0000000000..fce1792420 --- /dev/null +++ b/research/selected-bootstrap-reserve-composition/sources/pr2120-README.md @@ -0,0 +1,146 @@ +# A ceiling-free parent-stock bound for the selected BIT producer + +Under the same packet and completed-leaf hypotheses as [PR2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084), the selected ordinary BIT producer admits + +``` +log_q S(n,w) <= 6748*w*log2(max(1,n)) + <= 6748*w*(1+log2 e), 0 <= n <= e, e,w integers >= 1. +``` + +This reduces PR2084's sufficient parent-stock coefficient from 8194 to 6748, a ratio of exactly 14/17. It also reduces `ceil(log2(8*sigma))` from 17 to 16. The existing native first-stage cutoff passes the sufficient fit guard with this coefficient. + +This is a conditional stock-bound refinement and independent audit, not a new supplier, changed cutoff, physical reserve implementation or new kappa. The production row coefficient remains 18,355. No selected record or predecessor evidence changes. + +## Scope and overlap + +Scientific base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. The one-time selection is retained in [SELECTION.json](SELECTION.json). The assigned card is `selected-stock-envelope`, refined to the native first-stage ordinary BIT producer and a tighter depth implication. + +The nearest predecessor is Adam Gall's PR2084, read at head `8001a23b003bec5dff5e61edec907b652c475932`. Its packet/restoration proof and coefficient 8194 are credited, not claimed as new. Sricharan Vagvala's concurrent [PR2105](https://github.com/CrocSwap/integer-mult-bounds/pull/2105), head `0aca64e29d43533743bb912ac8b77b434e04b84a`, audits floor-depth thresholds for the **different complex m=73/rank-48 producer**. Its exact-depth method informed the independent inverse-threshold cross-check here. No predecessor verifier is imported or executed, and no pending package is copied into this one. + +The new implication uses the BIT terminal threshold to remove a rounded-depth additive term before bounding stock. It does not reproduce the fourteen known headrooms or solve the retained implementation hypotheses. The ordinary producer is BIT `m=64`, not the complex `m=73` supplier that constrains the shared exponent. + +Coordination: [Discussion 2114](https://github.com/CrocSwap/integer-mult-bounds/discussions/2114). The entry refresh covered 376 open PRs and 769 discussion records with complete pagination and no warnings. Metadata searches do not cover every diff or unpublished result. + +## Source binding + +The selected record binds `research/community-frontier1094-audit/ASSEMBLY.json`. Its BIT citation binds the exact tuned PR589 receipt by Git blob. The retained PR1087 assembler is authenticated as an immutable archive, then its `code/assemble.py` member is authenticated separately and read without execution. Its `BIT_L,BIT_T=9,32` and `BIT_M=1+7*BIT_L` identify dimension 64. + +The cited receipt has maximum child rank 42, 28,416 live roles and 28,425 physical roles. All nine work roles remain in the packet. Its row bill is `2*(64^2+1)+9909+252=18355`; this package changes none of those charged production terms. + +The source `three-stage-cover-bit.tex` supplies the local-ring full-cover formula and floor-child contract in sections "Finite covers, batching, and the strict moment" and "One weighted child on a generic residue class". Its displayed dimension 67 is historical. Instantiating that contract on the selected BIT recipe remains an explicit realization assumption. The reviewed PR185 proof retained by PR387 supplies the internally completed ordinary-leaf interface in "Nested row restoration and fixed tapes". Source hashes, Git blobs and the archive-member hash are in [SOURCES.json](SOURCES.json). + +## Conditional all-width lemma + +Retain these hypotheses. + +- Fix an eligible odd prime `q>2^80`, avoiding the recipe's fixed denominator and rank exclusions, before choosing widths. +- The selected full-cover implementation exposes one complete packet per active coarse level, with divisor + `W_q(w)=28425*|GL_64(F_q)|*q^(4096*(w-1))`. +- Atom width `w` stays fixed along a coarse call. Every child has atom count at most `r*floor(n/64)`, with `r<=42`. Bad-class fallback children have the stronger bound `floor(n/64)`. Below 64 atoms, and for peeled remainders and other ordinary operations, use completed ordinary calls. +- A child uses only its unused row quotient, fixes exposed ancestor fields as complete spectators and restores its supplied row before sequential reuse. The complete node restores its exposed role field. Completed ordinary leaves borrow internally and need no additional external row factor. + +These are inherited interfaces, not conclusions of the finite checks below. + +### Depth without a ceiling + +Let `D(n)` be the maximum-rank depth envelope: zero for `n<64`, and otherwise + +``` +D(n) = 1 + D(42*floor(n/64)). +``` + +Monotonicity makes this an upper bound for every permitted child path, including fallback. It is not a claim that every such path is realized by the physical compiler. + +Set `rho=42/64`. The exact integer certificate + +``` +2^17 * 42^28 < 64^28 +``` + +proves `rho < 2^(-17/28)`. If a path has `d>=1` active nodes, its last active atom count is at least 64 and at most `rho^(d-1)*n`. Thus + +``` +log2 n >= 6 + (d-1)*log2(64/42) + >= 6 + (d-1)*17/28 + >= d*17/28. +``` + +The last step uses the terminal slack `6>=17/28`. Consequently, for every integer `n>=0`, + +``` +D(n) <= (28/17)*log2(max(1,n)). +``` + +This has no ceiling or unnamed additive constant. Removing the terminal threshold invalidates this proof step. Replacing the floor by a ceiling can even prevent termination, since `42*ceil(84/64)=84`. Neither countermodel describes a defect in the selected floor contract. The allowance 28/17 is not claimed optimal. + +### Divisible stock and its complete packet charge + +Reduction modulo q gives exactly `q^(4096*(w-1))` lifts of each invertible low matrix. Therefore + +``` +|GL_64(Z/q^w Z)| < q^(4096*w), +log_q W_q(w) < 4096*w+1 <= 4097*w, +``` + +since `28425= 3, +L*delta^2 >= 36, +L*delta >= 2*(4+16). +``` + +The sufficient fit lemma of Josie Elliston's PR1965 then gives `ceil(log_q S(e,w))=2^L`, with `w=ceil(e^s)`, subject to the retained interfaces. This comparison does not assert that an actual selected implementation meets them, nor that this cutoff is necessary. The known headroom arithmetic is not claimed as new. + +## Replay and controls + +Standard-library Python 3.12, from the repository root: + +``` +python3.12 -I -B research/selected-bit-ceiling-free-stock/verify.py +python3.12 -I -O -B research/selected-bit-ceiling-free-stock/test_verify.py +python3.12 scripts/research_package.py --package research/selected-bit-ceiling-free-stock +``` + +Expected output includes `PASS_SELECTED_BIT_CEILING_FREE_STOCK sigma=6748 predecessor=8194 ratio=14/17 widths=100001 ell=16 no_new_kappa`, ten passing test groups and `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The verifier checks every external byte pin before semantic use, authenticates the archive member, and requires the committed [RESULT.json](RESULT.json). It neither regenerates a missing result nor changes a mismatched one. The exact checks cover every width 0..100,000 using separate forward and all-child dynamic programs, 196 inverse-threshold boundary probes, and 15 power-boundary probes up to 4097-bit atom counts. Literal depth fixtures constrain their shared conventions. + +Tests reject a false contraction, rank-43 substitution, missing terminal slack, capacity excess, wrong producer, omitted largest child, corrupted/nonregular archive member, insufficient cutoff and wrong coefficient. Optimized public-CLI controls mutate every declared live input in isolated copies and test corrupted and missing required results. No frozen file is modified. Python assertions are not acceptance gates. The universal implication rests on the written argument, not the finite fixtures. + +## Verification limits and implementation bounds + +No full selected cold replay, native compiler execution, Lean proof, hosted CI pass or independent human review is claimed. Only the native first-stage comparison is checked. Other stages need their preceding completed ordinary contract. The selected exponent and production row charge are unchanged. + +The new checker has no recursion. The width sweep is bounded at 100,001, rank inventories at 64, source lists at 16, archive scanning at 1024 members, consumed member size at 65,536 bytes and forward paths at 8194 edges. Source files are capped at 8 MiB and authenticated before archive decoding. The selected two-level halving guard bounds paths for the admitted 4097-bit atom counts. + +Power-of-Ten deviations are confined to Python's managed allocation and standard testing machinery. Rules 3 and 9 cannot provide allocation-free arithmetic or static unittest dispatch in this runtime. The fixed input/sweep/bit capacities bound live collections and integer sizes; test subprocesses have 120-second timeouts and temporary copies have scoped cleanup. The single `runpy` target is this package's own fixed verifier path. Follow-up is to reassess these capacities if the sweep or width domain expands, not to generalize this checker into an unbounded search. Syntax compilation, warnings-as-errors and normal/optimized replays are the available diagnostics; no repository-wide analyzer configuration changes are made. + +## Open next questions + +1. Can the selected GL64 packet and completed-row interfaces be realized with a source-bound all-size field-dependency certificate? Begin with one emitted parent/child split and verify that routes fix ancestor spectators and unused descendant stock. Finite scalar and depth checks do not discharge this implementation obligation. PR2097's fresh-fiber theorem is complementary. +2. Can an actual selected ordinary leaf be bound to the internally completed, zero-extra-external-stock interface at every admitted width? Trace its borrowing and restored endpoints while retaining complete outer spectators. The reviewed contract is inherited here; its physical realization, uniform time coefficients and tape obligations still block unconditional adoption. + +## Credit + +Adam Gall supplied PR2084's conditional BIT packet/stock implication. Sricharan Vagvala supplied the concurrent PR2105 complex depth audit. Josie Elliston supplied PR1956/PR1965's cutoff audit and time/space separation; ToikY supplied PR1990's independent stock-fit audit. DreamingOfClouds supplied the selected PR589 BIT word on eumemic's base and its credited compiler/hosting lineage. Rohan Arun supplied the reviewed PR185/PR387 contracts and selected PR1094 assembly on Jeremy Kothe's PR1087 predecessor. Their constructions, interface arguments and existing numerical receipts are not claimed as new. + +Nick Petalas retains authorship and responsibility for this conditional refinement and checker. Apache-2.0, following the repository license. No predecessor files are vendored or modified. diff --git a/research/selected-bootstrap-reserve-composition/test_verify.py b/research/selected-bootstrap-reserve-composition/test_verify.py new file mode 100644 index 0000000000..f0b7343e6a --- /dev/null +++ b/research/selected-bootstrap-reserve-composition/test_verify.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Public-CLI, literal endpoint and contract-failure controls.""" +from __future__ import annotations + +import copy +import json +import runpy +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +V = runpy.run_path(str(PACKAGE / "verify.py")) + + +class CompositionTests(unittest.TestCase): + def test_literal_borrowing_word(self) -> None: + # A nontrivial C reverses the two body coordinates. The full endpoint + # must nevertheless swap only the whole original chunks. + word = V["wrapper_word"](1, 3) + actual = V["evaluate"](word, 3, 3) + self.assertEqual(actual, [ + [0, 0, 0, 1, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 1, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 1, 0, 0, 0], + [1, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 1, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 1, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 1, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 1]]) + + def test_cancelled_row_fault_is_invisible_at_whole_endpoint(self) -> None: + word = V["wrapper_word"](2, 4, "cancelled_row") + endpoint = V["evaluate"](word, 4, 3, False) + self.assertEqual(endpoint, V["expected_swap"](4)) + self.assertEqual(V["cancelled_row_trace"](word, 4, 3), [2, 1]) + with self.assertRaisesRegex(V["Rejected"], "child spectator/row return"): + V["evaluate"](word, 4, 3) + + def test_missing_final_high_exchange(self) -> None: + word = V["wrapper_word"](2, 4, "omit_high") + self.assertNotEqual(V["evaluate"](word, 4, 3), V["expected_swap"](4)) + + def test_nested_stage_fixture_and_capacities(self) -> None: + word = V["wrapper_word"](7, 9) + self.assertEqual(len(word), 2162) + self.assertEqual(V["evaluate"](word, 9, 5), V["expected_swap"](9)) + for level, width in ((8, 9), (7, 10), (True, 3), (0, 0)): + with self.assertRaises(V["Rejected"]): + V["wrapper_word"](level, width) + + def test_all_fourteen_guards_with_inherited_not_measured_coefficient(self) -> None: + assembly, _ = V["authenticated_inputs"]() + records = V["stage_records"](assembly, 6748) + self.assertEqual(len(records), 14) + self.assertEqual(records[0], dict(branch="native", stage=1, previous_stage=0, + cutoff_log2="4785575287428", sigma=6748, + ell=16, external_leaf_factor_hypothesis=1)) + self.assertEqual(records[7]["cutoff_log2"], "4785575320504") + self.assertTrue(all(r["external_leaf_factor_hypothesis"] == 1 for r in records)) + + def test_source_stage_mutations(self) -> None: + assembly, _ = V["authenticated_inputs"]() + for field in ("exponent", "gap", "cutoff_log2"): + bad = copy.deepcopy(assembly) + bad["bootstrap"][1][field] = "1" + with self.assertRaises(V["Rejected"]): + V["stage_records"](bad, 6748) + for sigma in (0, 8195, True): + with self.assertRaises(V["Rejected"]): + V["stage_records"](assembly, sigma) + + def test_source_hash_fails_closed(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / "input" + path.write_bytes(b"source") + with self.assertRaisesRegex(V["Rejected"], "source pin"): + V["source_bytes"](path, "0" * 64) + + def test_public_cli_integrity_under_optimization(self) -> None: + # One isolated copy. Every mutated file is restored before the next + # control, and the actual public CLI is used rather than a mock. + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + for entry in manifest["files"]: + if entry["usage"] == "input": + target = root / entry["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / entry["path"], target) + command = [sys.executable, "-I", "-O", "-Werror", "-B", str(package / "verify.py")] + passed = subprocess.run(command, capture_output=True, text=True, timeout=30) + self.assertEqual(passed.returncode, 0, passed.stderr) + paths = [root / entry["path"] for entry in manifest["files"] if entry["usage"] == "input"] + paths += [package / entry["path"] for entry in manifest["pending_sources"]] + paths += [package / "RESULT.json"] + for path in paths: + original = path.read_bytes() + path.write_bytes(original + b" ") + if path.name == "RESULT.json": + changed = json.loads(original) + changed["actual_packet_implementation_checked"] = True + path.write_text(json.dumps(changed)) + failed = subprocess.run(command, capture_output=True, text=True, timeout=30) + self.assertNotEqual(failed.returncode, 0, str(path)) + self.assertIn("FAIL_SELECTED_RESERVE_COMPOSITION", failed.stderr) + path.write_bytes(original) + source_manifest = package / "SOURCES.json" + original_manifest = source_manifest.read_bytes() + changed_manifest = json.loads(original_manifest) + changed_manifest["archive_members"][0]["sha256"] = "0" * 64 + source_manifest.write_text(json.dumps(changed_manifest)) + failed = subprocess.run(command, capture_output=True, text=True, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertIn("member pin", failed.stderr) + source_manifest.write_bytes(original_manifest) + receipt = package / "RESULT.json" + receipt.unlink() + failed = subprocess.run(command, capture_output=True, text=True, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertFalse(receipt.exists()) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-bootstrap-reserve-composition/verify.py b/research/selected-bootstrap-reserve-composition/verify.py new file mode 100644 index 0000000000..4b5c7c20e2 --- /dev/null +++ b/research/selected-bootstrap-reserve-composition/verify.py @@ -0,0 +1,268 @@ +#!/usr/bin/env python3 +"""Independent conditional reserve-composition audit. No supplier admission.""" +from __future__ import annotations + +import hashlib +import io +import json +import sys +import tarfile +from dataclasses import dataclass +from fractions import Fraction as Q +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MAX_SOURCE = 64 * 1024 * 1024 +MAX_WORD = 50000 +MAX_STAGES = 7 +MAX_WIDTH = 9 + + +class Rejected(ValueError): + """A source, semantic contract or receipt failed.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise Rejected(message) + + +def source_bytes(path: Path, digest: str) -> bytes: + require(path.stat().st_size <= MAX_SOURCE, "source capacity") + data = path.read_bytes() + require(hashlib.sha256(data).hexdigest() == digest, f"source pin: {path}") + return data + + +def authenticated_inputs() -> tuple[dict, dict]: + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + require(len(manifest["files"]) <= 16, "source inventory capacity") + inputs = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + inputs[entry["path"]] = source_bytes(ROOT / entry["path"], entry["sha256"]) + require(len(manifest["pending_sources"]) == 2, "pending source inventory") + for entry in manifest["pending_sources"]: + source_bytes(PACKAGE / entry["path"], entry["sha256"]) + binding = json.loads(inputs["certificates/selected-result.json"]) + assembly_path = "research/community-frontier1094-audit/ASSEMBLY.json" + require(binding["certificate"] == assembly_path, "selected certificate path") + require(hashlib.sha256(inputs[assembly_path]).hexdigest() == + binding["certificate_sha256"], "selected assembly binding") + archive = manifest["archive_members"][0] + with tarfile.open(fileobj=io.BytesIO(inputs[archive["path"]]), mode="r:gz") as bundle: + members = bundle.getmembers() + require(len(members) <= 1024, "archive member capacity") + member = bundle.getmember(archive["member"]) + require(member.isfile() and member.size <= 65536, "assembler member type/size") + stream = bundle.extractfile(member) + require(stream is not None, "assembler absent") + with stream: + code = stream.read() + require(hashlib.sha256(code).hexdigest() == archive["sha256"], "member pin") + for fragment in (b"BIT_L,BIT_T=9,32", b"BIT_M=1+7*BIT_L", b"range(7)"): + require(fragment in code, "selected producer/stage formula") + expected_path = "research/e8-bit-p111-tuned/tune/EXPECTED.json" + expected_data = inputs[expected_path] + blob = hashlib.sha1(b"blob " + str(len(expected_data)).encode() + b"\0" + expected_data) + assembly = json.loads(inputs[assembly_path]) + require(blob.hexdigest() == assembly["bit_supplier"]["git_blob_sha1"], "BIT blob binding") + return assembly, json.loads(expected_data) + + +def ceil_q(value: Q) -> int: + return -(-value.numerator // value.denominator) + + +def stage_records(assembly: dict, sigma: int) -> list[dict]: + require(type(sigma) is int and 1 <= sigma <= 8194, "stock coefficient domain") + ell = (8 * sigma - 1).bit_length() + records = [] + for branch, key, chain in (("native", "complex_lower", "bootstrap"), + ("conservative", "conservative_complex_lower", "conservative_bootstrap")): + stages = assembly[chain] + require(len(stages) == MAX_STAGES, "seven source stages required") + s = min(Q(assembly["bit_lower"]), (1 - Q(1, 10**24)) * Q(assembly[key])) - Q(1, 10**27) + old = Q(384599, 10**10) + for index, source in enumerate(stages, 1): + a = (1 - s) * s + s * old + delta = min(s - a, 1 - a - s, 1 - a - s * (1 - old), 1 - s) + cutoff = max(ceil_q(36 / delta**2), ceil_q(1032 / delta)) + require(old < a < s < 1 - a and 0 < delta <= 1 - s, "stage gaps") + require(Q(source["exponent"]) == a and Q(source["gap"]) == delta, "source recurrence") + require(int(source["cutoff_log2"]) == cutoff, "source cutoff") + require(cutoff >= 3 and cutoff * delta**2 >= 36, "fit quadratic guard") + require(cutoff * delta >= 2 * (4 + ell), "fit stock guard") + records.append(dict(branch=branch, stage=index, previous_stage=index - 1, + cutoff_log2=str(cutoff), sigma=sigma, ell=ell, + external_leaf_factor_hypothesis=1)) + old = a + return records + + +@dataclass(frozen=True) +class Action: + kind: str + h: tuple[int, ...] + d: tuple[int, ...] = () + + +def wrapper_word(level: int, width: int, fault: str = "") -> list[Action]: + """Expand nested borrowed-high-digit wrappers with an explicit bounded stack.""" + require(type(level) is int and 0 <= level <= MAX_STAGES, "level capacity") + require(type(width) is int and 1 <= width <= MAX_WIDTH, "width capacity") + require(fault in ("", "omit_high", "cancelled_row"), "fault alphabet") + h, d = tuple(range(width)), tuple(range(width, 2 * width)) + pending = [("call", level, h, d, True)] + word = [] + for _ in range(MAX_WORD): + if not pending: + return word + kind, j, h, d, root = pending.pop() + if kind != "call": + word.append(Action(kind, h, d)) + continue + body = [("begin", j, h, d, root)] + if j == 0 or len(h) < 3: + body.append(("swap", j, h, d, root)) + else: + hb, db, hh, dh = h[1:], d[1:], h[:1], d[:1] + body.append(("sub", j, hb, db, False)) + for pass_index in range(2): + body.extend([("begin", j, hb, db, False), + ("call", j - 1, hb, db, False), + ("reverse", j, hb, db, False)]) + if root and fault == "cancelled_row": + body.append(("negate", j, (2 * width,), (), False)) + body.append(("end", j, hb, db, False)) + body.append((("add" if pass_index == 0 else "diff"), j, hb, db, False)) + if not (root and fault == "omit_high"): + body.append(("call", j - 1, hh, dh, False)) + body.append(("end", j, h, d, root)) + pending.extend(reversed(body)) + require(len(pending) + len(word) < MAX_WORD, "word capacity") + raise Rejected("word expansion exhausted") + + +def apply_action(state: list[list[int]], action: Action, q: int) -> None: + h, d, kind = action.h, action.d, action.kind + if kind == "negate": + state[h[0]] = [(-x) % q for x in state[h[0]]] + elif kind == "reverse": + for field in (h, d): + values = [state[i] for i in reversed(field)] + for i, value in zip(field, values): + state[i] = value + else: + for left, right in zip(h, d): + x, y = state[left], state[right] + if kind == "swap": + state[left], state[right] = y, x + elif kind == "sub": + state[right] = [(b - a) % q for a, b in zip(x, y)] + elif kind == "add": + state[right] = [(a + b) % q for a, b in zip(x, y)] + elif kind == "diff": + state[right] = [(a - b) % q for a, b in zip(x, y)] + else: + raise Rejected("unknown action") + + +def evaluate(word: list[Action], width: int, q: int, check_calls: bool = True) -> list[list[int]]: + require(len(word) < MAX_WORD and 1 <= width <= MAX_WIDTH, "evaluation capacity") + require(q in (3, 5), "fixture radix") + dimension = 2 * width + 3 + state = [[int(i == j) for j in range(dimension)] for i in range(dimension)] + snapshots = [] + for action in word: + if action.kind == "begin": + targets = set(action.h + action.d) + snapshots.append({i: state[i][:] for i in range(dimension) if i not in targets}) + elif action.kind == "end": + require(bool(snapshots), "unmatched return") + old = snapshots.pop() + if check_calls: + require(all(state[i] == value for i, value in old.items()), "child spectator/row return") + else: + apply_action(state, action, q) + require(not snapshots, "unclosed call") + return state + + +def expected_swap(width: int) -> list[list[int]]: + dimension = 2 * width + 3 + order = list(range(width, 2 * width)) + list(range(width)) + list(range(2 * width, dimension)) + return [[int(j == i) for j in range(dimension)] for i in order] + + +def cancelled_row_trace(word: list[Action], width: int, q: int) -> list[int]: + dimension = 2 * width + 3 + state = [[int(i == j) for j in range(dimension)] for i in range(dimension)] + trace = [] + for action in word: + if action.kind not in ("begin", "end"): + apply_action(state, action, q) + if action.kind == "negate": + trace.append(state[2 * width][2 * width]) + return trace + + +def wrapper_checks() -> dict: + cases, columns, maximum_word = 0, 0, 0 + for level in range(MAX_STAGES + 1): + for width in range(1, MAX_WIDTH + 1): + word = wrapper_word(level, width) + maximum_word = max(maximum_word, len(word)) + for q in (3, 5): + require(evaluate(word, width, q) == expected_swap(width), "nested endpoint") + cases += 1 + columns += 2 * width + 3 + bad = wrapper_word(2, 4, "cancelled_row") + require(evaluate(bad, 4, 3, False) == expected_swap(4), "cancellation control endpoint") + try: + evaluate(bad, 4, 3) + except Rejected as error: + require(str(error) == "child spectator/row return", "cancellation rejection reason") + else: + raise Rejected("endpoint-only completion incorrectly accepted") + row_trace = cancelled_row_trace(bad, 4, 3) + require(row_trace == [2, 1], "literal canceled-row witness") + missing = evaluate(wrapper_word(2, 4, "omit_high"), 4, 3) + require(missing != expected_swap(4), "omitted high exchange control") + return dict(cases=cases, basis_columns=columns, maximum_word=maximum_word, + cancelled_row_endpoint_passes=True, cancelled_row_child_contract_rejected=True, + cancelled_row_witness=dict(q=3, stage=2, width=4, initial_row=1, + after_body_returns=row_trace), + omitted_high_exchange_rejected=True) + + +def result() -> dict: + assembly, expected = authenticated_inputs() + bit = expected["nine"]["bit"] + require((bit["live"], bit["physical"], bit["maxchild"]) == (28416, 28425, 42), "selected BIT producer") + require(max(map(int, expected["nine"]["profile"])) == 42, "maximal child") + require(2**17 * 42**28 < 64**28 and bit["physical"] < 2**80, "packet/depth premises") + sigma = (64**2 + 1) * Q(28, 17) + require(sigma == 6748, "inherited coefficient") + stages = stage_records(assembly, int(sigma)) + return dict(status="CONDITIONAL_RESERVE_COMPOSITION_AUDIT", stages=stages, + wrappers=wrapper_checks(), selected_kappa=assembly["kappa"], + actual_packet_implementation_checked=False, uniform_time_H2_checked=False, + new_supplier_or_exponent=False) + + +def main() -> None: + require(len(sys.argv) == 1, "no regeneration or extra arguments") + observed = result() + recorded = json.loads((PACKAGE / "RESULT.json").read_text()) + require(json.dumps(observed, sort_keys=True) == json.dumps(recorded, sort_keys=True), "required receipt") + print("PASS_SELECTED_RESERVE_COMPOSITION stages=14 sigma=6748 wrappers=144 child_return_control=1 no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (Rejected, OSError, ValueError, KeyError, TypeError, tarfile.TarError) as error: + print(f"FAIL_SELECTED_RESERVE_COMPOSITION: {error}", file=sys.stderr) + raise SystemExit(1)