From 0ac8192bdf6b5217787ffe44c4b1d91732ef6b23 Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 21 Oct 2026 21:43:44 +1100 Subject: [PATCH] Extract optional ordinary B2 bootstrap with canonical pinned inputs --- research/ordinary-b2-bootstrap/B2-PINS.json | 37 ++ research/ordinary-b2-bootstrap/PROOF.md | 391 ++++++++++++++++++ research/ordinary-b2-bootstrap/README.md | 48 +++ .../SOURCE-MANIFEST.json | 385 +++++++++++++++++ research/ordinary-b2-bootstrap/SOURCES.json | 336 +++++++++++++++ research/ordinary-b2-bootstrap/TASK.json | 80 ++++ research/ordinary-b2-bootstrap/VERIFY.json | 87 ++++ .../ordinary-b2-bootstrap/b2_bootstrap.py | 292 +++++++++++++ .../evidence/B2-BOOTSTRAP.json | 105 +++++ .../frozen/interval_engine.py | 377 +++++++++++++++++ 10 files changed, 2138 insertions(+) create mode 100644 research/ordinary-b2-bootstrap/B2-PINS.json create mode 100644 research/ordinary-b2-bootstrap/PROOF.md create mode 100644 research/ordinary-b2-bootstrap/README.md create mode 100644 research/ordinary-b2-bootstrap/SOURCE-MANIFEST.json create mode 100644 research/ordinary-b2-bootstrap/SOURCES.json create mode 100644 research/ordinary-b2-bootstrap/TASK.json create mode 100644 research/ordinary-b2-bootstrap/VERIFY.json create mode 100644 research/ordinary-b2-bootstrap/b2_bootstrap.py create mode 100644 research/ordinary-b2-bootstrap/evidence/B2-BOOTSTRAP.json create mode 100644 research/ordinary-b2-bootstrap/frozen/interval_engine.py diff --git a/research/ordinary-b2-bootstrap/B2-PINS.json b/research/ordinary-b2-bootstrap/B2-PINS.json new file mode 100644 index 0000000000..2b3bb46b12 --- /dev/null +++ b/research/ordinary-b2-bootstrap/B2-PINS.json @@ -0,0 +1,37 @@ +{ + "historical_result": { + "commit": "46965e30a34af44499a1442daeb94cd3b68fa67a", + "mathematical_projection_sha256": "9f2b0b27f20ee0e0f126a33351c39c41e070f801141e761957ad038642084ce6", + "path": "research/complex-pooled-full-admission/evidence/B2-BOOTSTRAP.json", + "projection_omits": [ + "source_pins_sha256", + "local_inputs", + "source_bundle" + ], + "sha256": "f7780281e1920aa7067ffcf68e293f2d975126a9760ca63df08390e055bf7b82" + }, + "local_inputs": { + "frozen/interval_engine.py": "c4740234bee2bab8292aeef7fb561246cff8a060ea6e96f0bc14a7b69c62042c" + }, + "schema_version": 3, + "scientific_base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "scope": "Pins for read-only B2 arithmetic, inspected theorem sources, and complete ordinary backend compatibility; no production source activation.", + "source_bundle": { + "kind": "declared-pinned-repository-inputs", + "manifest": "SOURCE-MANIFEST.json", + "manifest_sha256": "de0120c931050ea9d82758455aec5cb3addf384ebd9eed6ee708c442168ba38f" + }, + "source_inputs": { + "research/bootstrap-depth-audit/sources/pr387/PROOF.md": "15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8", + "research/community-round8-audit/pr185-proof-reviewed.md": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa", + "research/physical-complex-compact/PROOF.md": "ec6395822ae500242f3fe5e2cf40caf9a7f9fa259d475d2c14970d951ff4df48", + "research/retuned-ordinary-coupling/PROOF.md": "3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22", + "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz": "0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c", + "research/retuned-ordinary-coupling/interface.py": "25707c61b9fc6c1f09388c7cc72d269be0f8f8cae4dbc7cd5c2d00ce7fadf839", + "research/selected-bit-fast-primitives/PROOF.md": "c6912c307304b71ab51a5b9647df19a3e2c85efaca5bb3f1b635e918a62b5978", + "research/selected-bit-fast-primitives/compile_routes.py": "1bfef464dfb3e33d9d57f53b657b2d1fe3598bc453be49000a5e782b622e8585", + "research/selected-bit-fast-primitives/inputs/pr2899.tar": "fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531", + "research/selected-bit-fast-primitives/stage.py": "44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647", + "research/selected-bit-fast-primitives/stage_sources.py": "55c6631cce4f76e14b66b6195468c36b544e2374cc6c59702135c664bff10822" + } +} diff --git a/research/ordinary-b2-bootstrap/PROOF.md b/research/ordinary-b2-bootstrap/PROOF.md new file mode 100644 index 0000000000..b723a2fdca --- /dev/null +++ b/research/ordinary-b2-bootstrap/PROOF.md @@ -0,0 +1,391 @@ +# One ordinary bootstrap step that clears the complex rate + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. The construction composes Jose Manuel's completed ordinary and +fast-primitive sources, Rohan Arun's PR185/387 stopped-leaf argument, and the +retained PR589 BIT profile. It does not originate those components or their +bootstrap formula. + +Under the stated source-relative physical contracts, one further ordinary +stage supplies + +``` +a2 = 57697923247/33292900000000 + = 0.001733039874778105842386815206845904..., +T_B2(V,e) <= 4283584 A V e^(1-a2), +``` + +for a finite uniform coefficient `A` specified below. It exceeds the present +complex endpoint `C=0.001730980255989036959962` by the exact positive rational + +``` +a2-C = 342853411912956978405651/166464500000000000000000000000. +``` + +This is an ordinary interchange construction from the **BIT** component. +It invokes no part of the new complex source. It removes an ordinary-rate +obstruction once the completed binary interface is connected to the complex +caller; it does not by itself supply that caller or its outer embedding. + +## 1. Why a bootstrap at the complex rate is insufficient + +The demonstrated preceding ordinary rate is +`a1=169711/100000000=0.00169711`. If one retains the selected convenience +choice `s=(1-10^-24)C-10^-27`, the one-step value is + +``` +a_next = s(1-s)+s*a1 = 0.001730921627244654642552821294... . +``` + +Although this exceeds the requested legacy kappa, the legacy outer margin is + +``` +q=(1-2*10^-24)*a_next, +(1-10^-24)*q/(1+q) = 0.001727930714600372546778004395..., +``` + +which is below `0.001727989140903569` by more than `5.8426*10^-8`. +Comparing an ordinary rate directly with kappa omits a necessary outer loss. + +Instead choose the independent BIT coupling `c=1/577`. The BIT constructor +does not need `c2^80`, positive complete preceding, +intervening and trailing spectator extents, and the selected PR589 BIT +catalogue. The native ordinary interface maps the two complete radix-q +chunks of width `e`, preserves its borrowed input, returns a distinct owned +output, restores every spectator coordinate, and closes its owned work. +The binary wrapper preserves the same completed contract. Successful admitted +execution is the scope; interruption recovery is not asserted. + +The previous `B1` is the actual ordinary construction of +[`selected-bit-recursive-closure`](../selected-bit-recursive-closure/PROOF.md) +and PR2899, with its fixed coupling `17/10000` and saving `a1`. Its sealed +coarse caller uses its elementary `A0` routes and swaps. The successor `C1` +is the physical program in +[`selected-bit-fast-primitives`](../selected-bit-fast-primitives/PROOF.md): +both the reached weighted/remainder swap and the reached complete owner-chart +route use that completed `B1`. Entering `B1` suspends the successor factory +scope and restores both preceding bindings. `B1` completes under those +preceding bindings. Exiting the suspended scope then restores the successor +bindings before the caller acquires its output lease, copies the protected +result and clears that result. The preceding output remains protected until +this copy/clear finishes, before any reuse. + +The complete dependency order is + +``` +new complex caller -> binary B2 -> ordinary B2 -> C1 -> B1 -> C0 -> A0. +``` + +Only the leftmost caller is the new complex construction. Its correctness is +not used to construct anything to its right. Coarse recursive calls decrease +atom count; a call to the preceding ordinary implementation decreases the +fixed stage. `B1` never re-enters `C1` or `B2`. + +The existing factory composition is precise. In the one cold namespace +authenticated by `stage_sources.activate()`, create two distinct `Ordinary` +instances on the same immutable selected BIT binding, topology and programs: + +``` +previous = Ordinary(q, binding, topology, programs, + profile=Profile()) # 17/10000, m=64, rmax=42 +outer = Ordinary(q, binding, topology, programs, + profile=Profile(numerator=1, denominator=577)) +registry, receipt = selected_registry(actual_selected_bit_catalogue) +native_B2 = promote_ordinary(outer, previous, registry) +binary_B2 = Binary(native_B2) +``` + +`selected_registry` must bind all 1,123 actual data/host charts and their +inverse factor words. An identity-only `Registry(64)` is insufficient. +`promote_ordinary` changes the controller view of the fresh outer root +session before it reads numerical input; it reuses that session's actual +physical roles and adds the fixed successor scratch allowance. It does not +copy an active machine or alias its work with `previous`. + +The two predecessor exports are compatible at the source level. All 23 files +in `selected-bit-fast-primitives/inputs/pr2899.tar` are byte-identical to the +corresponding files in the retuned coupling's PR2899 export; the latter adds +twelve frozen dependencies. Their SHA256 values are respectively +`fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531` and +`0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c`. +The independently cold-guarded loaders should not both be invoked into one +already populated namespace. + +This specifies a finite program composition under the retained source +arguments. The present arithmetic audit does not execute a production GL64 +payload or claim a new full physical-machine replay of that composition. +Changing `Profile` on an unpromoted C0-backed `Ordinary` supplies only a +retuned first stage and does not establish this B2 bound. + +## 3. Complete stopped BIT recurrence + +Write `p1=1-a1`. Retain the complete paid BIT histogram and bad-class term: + +``` +H={1:381024,2:400416,3:22752,4:26880, + 5:29376,6:17376,7:26784,42:288}, +m=64, W=28416, epsilon=10^-16, +F=32*64^2*sum(H)=118606528512. +``` + +Every paid request executes its complete low/high fibre; the per-request +bad-class estimate is retained. No average over selectively omitted prefixes +is used. The fast-primitive source's explicit local bill is bounded by + +``` +C_B1 V [252 w^p1 + (1598048/111)(w-1)^p1] + A_q V(n+1) + E_prep. +``` + +At `w=1`, omit the high-route term. The 252 bound is four calls for each +of at most 63 peeled pairs. The other coefficient counts both entrance and +return owner routes, with the actual same-q `B1` interface. It is a time +coefficient, unrelated to the old external row allowance also numbered 252. +`E_prep` includes coefficient/history preparation and is absorbed only in +the canonical root-coupled domain, by the complete target-fibre argument. + +Choose a finite `A>=1` dominating these uniform coefficients, the preceding +`B1` bound, all source access and output disposal, the outer wrapper bill, +and its elementary fallback. It may depend on the fixed prime, source, +compiled registry and fixed machine inventories. It does not depend on +width, payload contents, ancestor, prefix ordinal or external multiplicity. +No empirical bound such as `A<2^512` is asserted. + +For normalized time `T1(n,w)` and `f=floor(n/64)`, the actual stopped tariff is + +``` +T1(n,w) <= A w^p1 (0=64). +``` + +It includes all restoration, routing, selection, copying, marker work, +rewinds and private-work disposal. The preceding ordinary calls are in the +local toll, not additional C1 coarse children or parent row multipliers. + +Define `mu_t=(sum H[r](r/64)^t+epsilon F(1/64)^t)/W`. +The exact full-profile calculation gives + +``` +mu_1 = 2874298095721977/2890625000000000 < 199/200, +mu_(576/577) in + [999998938581682162866772413602, + 999998938581682162866772413603]/10^30 < 999999/1000000. +``` + +The old `9999/10000` power cap is false at this coupling. Use the increased +coefficient, not the predecessor's smaller number. Strong induction against +a monotone majorant, including the fallback maximum, yields + +``` +T1(n,w) <= 200 A n + 1000000 A n^(1-c) w^p1. (1) +``` + +The linear contraction pays `A n`; the strict power gap pays `A w^p1`. +No monotonicity of the machine's measured running time is assumed. + +The interval above was independently rechecked using both the outward +rational series in `frozen/interval_engine.py` and integer-power bisection: at scale +`Q=2^160`, consecutive integers bound each power through +`z^577 64^576 <= r^576 Q^577 < (z+1)^577 64^576`. +Both computations retain the rational fallback weight. + +## 4. Actual stock, wrapper and all-width coefficient + +Use the encoded selector of +[`retuned-ordinary-coupling`](../retuned-ordinary-coupling/PROOF.md), keeping +the original width fixed throughout each coarse root: + +``` +w=ceil(e^c), +D(e)=0 for e<64; D(e)=1+D(42 floor(e/64)) otherwise, +K(w)=269241600 |GL64(F_q)| q^(4096(w-1)), +stock=K(w)^D(e), k=min{j:q^j>=stock}. +``` + +Choose the stock before the body, then set `n=floor((e-k)/w)` and +`ell=e-k-nw`. Use elementary fallback if `2k>=e` or `n<64`. +The retained depth and stock proof gives `k<=16390 e^c log2(e)` for `e>=2`. +Since `17/10000=2^20`, both actual fit predicates hold. The sufficient comparisons +include `17^128>32*16^128` and +`32780*(17/16)*20=696575<2^20`; then `n>e^(1-c)/4-1>64`. +This is a sufficient cutoff, not a claim of the smallest fit threshold. + +The ordinary wrapper executes two completed reversed-body ROOT calls. Each +uses padding below two, so (1) is charged four times. Include the three +ordered body updates, restrictions, residual digits, high exchange, setup, +all scans, copying, rewinds, erasure and output return. Enlarging `A` as above +gives the complete bill + +``` +T_B2(V,e)/V <= A[801n + 4000000 n^(1-c) w^p1 + k+w+1]. (2) +``` + +The wrapper's retained elementary high/remainder operations are sufficient; +they are not silently promoted to a free weighted or reversed operation. + +Now `a2=c(1-c)+c*a1`. Since `c>a1`, + +``` +n^(1-c) w^p1 <= e^(1-c) w^(c-a1) + <= 2^(c-a1) e^(1-a2) + < (17/16) e^(1-a2). +``` + +Also `a21/2`, and `log2(e)<=2 sqrt(e)` for `e>=1`. +Consequently `n<=e^(1-a2)`, `k<=32780 e^(1-a2)`, +`w<=2 e^(1-a2)` and `1<=e^(1-a2)`. Substitution in (2) gives + +``` +801 + 4000000*(17/16) + 32780 + 2 + 1 = 4283584. +``` + +For the finite fallback range `e<2^20`, `e^a2<2^(20/512)<2`, so its +elementary `A V e` bound fits the same coefficient. The source's fixed-degree +logarithmic setup is retained and absorbed into `A`; the retuned proof uses +`(1+log2 V)^4<=512V`. Positive input volumes also absorb fixed compilation +allowances into a further finite coefficient. The binary wrapper pads two +complete fields by a factor below `q^2` and charges its own operations; this +only changes the fixed q-dependent coefficient. + +For comparison with the PR185/387 generic cutoff method, the four exact gaps +are + +| Gap | Value | +| --- | --- | +| `c-a2` | `2076753/33292900000000` | +| `1-a2-c` | `33177502076753/33292900000000` | +| `1-a2-c(1-a1)` | `331776/332929` | +| `1-c` | `576/577` | + +Their minimum is the first. The generic sufficient recipe remains valid: +choose a genuine coefficient bound `A_*<2^h`, then +`L>=max(20,36/delta^2,2(4+h)/delta)` and use the preceding completed algorithm +below `2^L`, enlarging the next constant by its actual fallback cost. +It must carry the preceding constant. The explicit coefficient argument +above avoids needing that enormous time-absorption cutoff: its `2^20` +cutoff is for physical stock fit, while `A` is retained in the time bound. + +## 5. Restoration and finite physical inventories + +Each B1 primitive restores its borrowed source, complete spectators and row +coordinate at its own return, before the successor reuses any output or row. +The parent C1 retains its fixed roles while the preceding complete inventory +is active. The successor adds 128 fixed scratch tapes and its separately +counted fixed-capacity high numerical bank. Distinct B1 and B2 instances have +distinct owned work; immutable source tables may be shared. + +The parent's stock quotient is reused only after each completed child +returns. Neither the two reversed-body calls nor the extra bootstrap stage +multiplies the externally supplied row divisor. B1's internal stock and +binary padding are included in its completed time/space contract. Depth-first +parking and the geometric child-volume sum give the retained +`O_q(V_root)+F_q` occupied/visited space, including blank retained backing +for the fixed roles. This is not per-return deallocation of host memory. + +This is the completed-interface premise of PR185 and PR387, not merely a +final two-call endpoint: two erroneous row changes that cancel at the outer +return would not meet it. The source-bound `StagePool.suspended` and +protected-output copy/clear are the relevant implementation boundaries. + +## 6. Boundary of the optional B2 route + +This package constructs and prices the optional ordinary B2 stage under its +retained source-relative physical contracts. It uses the canonical BIT, +preceding ordinary and fast-primitive sources; it invokes no pooled complex +supplier and has no dependency on PR #4270. + +The B2 rate is strictly above `C`, so it can be weakened to a desired +ordinary rate below `C`. This removes one rate obstruction. It does not +establish a complex or multiplication exponent. A consumer must bind the +completed B2 interface at its actual compact call sites and preserve every +native endpoint, hosting, width, restoration, stopping-rule and outer +analytic obligation at those calls. In particular, changing an ordinary +exponent does not remove exceptional repair, row separation or long-record +costs in the compact binary theorem of +[`physical-complex-compact`](../physical-complex-compact/PROOF.md). + +That theorem's complete tariff includes + +``` +s sum_rows T_B2(v0,nG) + O_m(V+M A_len^6+delta M A_len(R+A_len)), +``` + +with four binary calls for an earlier source/toggle and twelve for a later +source. A candidate complex join must separately establish its global +binding over every actual call and chart, its one-active-node recursion +and parked-parent reserve, common-grid precision, and the stopping/root +contract needed by the outer parameters. A modular fixture or a rate +table cannot supply this global invocation. + +The production B2 factory is specified by the source-relative composition +above, but this package's checker neither constructs nor executes it. +Implementation and caller admission remain open. They are not needed for +the exact conditional rate calculation and written cost derivation here. + +## 7. Exact evidence and proof scope + +Run the bounded check from this package: + +``` +python3 b2_bootstrap.py --output /tmp/b2-normal.json +python3 -O b2_bootstrap.py --output /tmp/b2-optimized.json +cmp /tmp/b2-normal.json /tmp/b2-optimized.json +``` + +The independent arithmetic and backend-source comparison are recorded in +[`evidence/B2-BOOTSTRAP.json`](evidence/B2-BOOTSTRAP.json). Both modes passed +with byte-identical receipts, the fallback retained, overlapping independent +rational moment enclosures, all four strict gaps, the exact `4283584` +coefficient, sufficient `2^20` fit and all 23 equal backend files. The eleven +negative controls reject the direct-rate/outer-loss shortcut, omitted +fallback, wrong power coefficient, profile-only bootstrap, infeasible +coupling, inadequate sufficient stock cutoff, omitted root padding, and +changed or missing authenticated source material. + +[`B2-PINS.json`](B2-PINS.json) authenticates the unchanged 54-file inventory +in [`SOURCE-MANIFEST.json`](SOURCE-MANIFEST.json). Each file is read directly +from its declared canonical repository path at the exact scientific-base +bytes, Git blob and SHA256. `VERIFY.json` declares all 54 inputs, so a +Git-free package export includes their complete bytes. No duplicate +2.2 MB closure archive is needed. `--source-root` selects another root and +requires the same full inventory and hashes, rejecting missing or changed +inputs. The legacy control names `missing_vendored_source` and +`changed_vendored_source` are retained; they now test the authenticated +canonical input map. + +The exact original interval engine is retained as +[`frozen/interval_engine.py`](frozen/interval_engine.py), authenticated before +its bytes are compiled and only its pure moment function is called. +The 23-member backend archives are inspected without extraction or source +execution. No production B2 factory is constructed or invoked. + +The receipt's complete mathematical projection is also checked against the +historical B2 receipt recorded at `46965e30a34af44499a1442daeb94cd3b68fa67a`. +Only `source_pins_sha256`, `local_inputs` and `source_bundle` transport fields +change. `B2-PINS.json` records the original receipt SHA256 and exact +projection digest. All rates, full moments, tariffs, fit, 23 backend member +hashes, eleven rejection controls and scope flags agree. + +The inspected reviewed PR185 proof has SHA256 +`bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa`; +the PR387 proof is +`15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8`. +They are retained in `research/community-round8-audit/pr185-proof-reviewed.md` +and `research/bootstrap-depth-audit/sources/pr387/PROOF.md`. +The actual fast-primitive `stage.py` is +`44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647`. + +These finite checks support the stated source-relative construction and +written all-width cost derivation. They are not a production payload run, +independent human review, proof-assistant verification or a completed +integer-multiplication theorem. diff --git a/research/ordinary-b2-bootstrap/README.md b/research/ordinary-b2-bootstrap/README.md new file mode 100644 index 0000000000..cb66a25db0 --- /dev/null +++ b/research/ordinary-b2-bootstrap/README.md @@ -0,0 +1,48 @@ +# Optional ordinary B2 bootstrap (draft) + +Prepared by Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. Jose Manuel's ordinary and fast-primitive sources, Rohan Arun's +PR185/387 arguments and the retained PR589 BIT profile keep their credit. + +This is the optional B2 result split from PR #4270. It stands on canonical +main `12fa8c5c844be21bfefb38a19503fbd867a11244` and has no dependency on that +PR. Under the explicit source-relative completed-interface contracts in +[PROOF.md](PROOF.md), one ordinary bootstrap at coupling `1/577` gives +saving `57697923247/33292900000000`, with complete wrapper coefficient +`4283584` and sufficient original-width stock fit from `2^20`. + +The draft preserves the written proof and exact mathematical evidence. +Its checker does not construct or execute the production B2 factory, and +this ordinary-rate comparison does not claim a new multiplication exponent. +All arbitrary-input, spectator, restoration, precision and completed-return +premises in the proof remain requirements. + +The same 54 source files and nested backend archives are reused directly +from exact canonical paths, declared in [VERIFY.json](VERIFY.json) and pinned +by [SOURCE-MANIFEST.json](SOURCE-MANIFEST.json). The frozen interval engine +is an exact copy of the earlier `joint_bound.py` (SHA256 +`c4740234bee2bab8292aeef7fb561246cff8a060ea6e96f0bc14a7b69c62042c`); +it is compiled from authenticated bytes and only its pure moment is used. +No duplicate source-closure archive or copied BIT evidence is added. +`B2-PINS.json` binds every mathematical field and all eleven controls to +the historical receipt while identifying the three changed transport fields. + +From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/ordinary-b2-bootstrap +``` + +The registered normal and optimized runs compare the same full deterministic +receipt. A Git-free export includes all 54 declared files; missing or changed +source inputs fail. [PROOF.md](PROOF.md) states the exact mathematical and +execution scope. + +## Open next questions + +- Implement the two-owner production B2 factory at the complete dirty returned + interface, then independently check endpoint/restoration and source access. + The first step is the explicit registry composition in the proof. +- Bind that completed implementation to a concrete complex compact caller, + paying every stopping, hosting, precision and outer cost. Production + implementation and a separate caller-specific admission are prerequisites. diff --git a/research/ordinary-b2-bootstrap/SOURCE-MANIFEST.json b/research/ordinary-b2-bootstrap/SOURCE-MANIFEST.json new file mode 100644 index 0000000000..7f4dd77577 --- /dev/null +++ b/research/ordinary-b2-bootstrap/SOURCE-MANIFEST.json @@ -0,0 +1,385 @@ +{ + "files": [ + { + "bytes": 10725, + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "path": "certificates/selected-result.json", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "provenance" + }, + { + "bytes": 9746, + "git_blob": "ede0d322c477af91d4c2cc33db0fd10958f45eab", + "path": "research/bit2234-stock-threshold/README.md", + "sha256": "1e050c9f963421d751d9208092f9a15321ed77810e03912df8eb5eb56bbb06e7", + "usage": "provenance" + }, + { + "bytes": 5799, + "git_blob": "915d08efd81fa304e1974e26d8212803e03e6623", + "path": "research/bootstrap-depth-audit/sources/pr387/PROOF.md", + "sha256": "15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8", + "usage": "provenance" + }, + { + "bytes": 85147, + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "usage": "provenance" + }, + { + "bytes": 799504, + "git_blob": "9eafb8776cbf78c72124f833534469ddfa5e98ec", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz", + "sha256": "0357b7cfbd7c29b4983982baf153c8a9f1e1e412690cd7fa9fc3d23d7963b20f", + "usage": "provenance" + }, + { + "bytes": 4467, + "git_blob": "1f648db9e63e7bfcaa6d5b1dd9fa6503caac47d2", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json", + "sha256": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819", + "usage": "provenance" + }, + { + "bytes": 5827833, + "git_blob": "44006542202ca6037533a754f0bcd00549d7e088", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json", + "sha256": "0058c491d839142aa99ef86a5ec697ce99857632228531512ea3fa74fb24d734", + "usage": "provenance" + }, + { + "bytes": 6920, + "git_blob": "93a588a73a38050dfa0a383cb44f228aff6f243e", + "path": "research/community-round8-audit/pr185-proof-reviewed.md", + "sha256": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa", + "usage": "provenance" + }, + { + "bytes": 5987, + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "usage": "provenance" + }, + { + "bytes": 42353, + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "usage": "provenance" + }, + { + "bytes": 6405, + "git_blob": "4468a00349b4f68dce103e785a8392099435e1d6", + "path": "research/idle-axis-hosting/PROOF.md", + "sha256": "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542", + "usage": "provenance" + }, + { + "bytes": 18626, + "git_blob": "f65f38123ca0adb02f6ca69351cbfc933506e5cb", + "path": "research/physical-complex-compact/PROOF.md", + "sha256": "ec6395822ae500242f3fe5e2cf40caf9a7f9fa259d475d2c14970d951ff4df48", + "usage": "provenance" + }, + { + "bytes": 12438, + "git_blob": "bbd3f12b9a32b3ad3cba85a2d5a1b3054214fa02", + "path": "research/pr589-five-helper-hosting/PROOF.md", + "sha256": "59cae781bfbe1a01ed9e66a8efeeb5a2b995e5ecdf908586b23ecc39f2b8d647", + "usage": "provenance" + }, + { + "bytes": 21449, + "git_blob": "dbc71f56bb4205ebe378ada1f9f4ea88630d1d39", + "path": "research/pr589-five-helper-hosting/verify.py", + "sha256": "cf90e19ae9991b0698be03d395a8cc29061ecb307eb7fea19adfb2d23c25a367", + "usage": "provenance" + }, + { + "bytes": 15680, + "git_blob": "251f335ebaccc11d69393ee7aeb5a2e84526d0bb", + "path": "research/recursive-parking-boundary/README.md", + "sha256": "491aa208391ee4c2936510b1a5c5c018dd5509d9a0e88687c72ab8406cd77b18", + "usage": "provenance" + }, + { + "bytes": 3138, + "git_blob": "b370d63711733f6eb9685a96d09ca1964f685c51", + "path": "research/retuned-ordinary-coupling/EVIDENCE.md", + "sha256": "3cea6f279f0ae302f3432e1c67955ed009d2a9e569192b690f68627c62c2c3cb", + "usage": "provenance" + }, + { + "bytes": 8312, + "git_blob": "8a0f47a1541a0b8e67866df4f65928de31073651", + "path": "research/retuned-ordinary-coupling/PROOF.md", + "sha256": "3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22", + "usage": "provenance" + }, + { + "bytes": 4091, + "git_blob": "21a248de1d9ea63c88ed596554af307a36360383", + "path": "research/retuned-ordinary-coupling/README.md", + "sha256": "b342b26f131e67cd6e5bc143a41845e40eaec349af19648a6f76bc2c43ec0983", + "usage": "provenance" + }, + { + "bytes": 1479, + "git_blob": "2d346515fb715a1e6d91371e89aa6727ef25d3d9", + "path": "research/retuned-ordinary-coupling/SOURCES.json", + "sha256": "d4208b2d236c6055cc86c1d8ba8ce5cf54263ec5034556b0d70fbab3fbd7796e", + "usage": "provenance" + }, + { + "bytes": 4230, + "git_blob": "dc1ca38c3b0758bde1d7bf0f035014021e1e3c2a", + "path": "research/retuned-ordinary-coupling/TASK.json", + "sha256": "cf0749a2e4c805b28e5284f519fdcb43f203d77c3fd227d8581cb1079454fb1e", + "usage": "provenance" + }, + { + "bytes": 1511, + "git_blob": "7fe1448397d60577fe8445c64f6424cb8bb80422", + "path": "research/retuned-ordinary-coupling/VERIFY.json", + "sha256": "a46e323a04b959c76ceea82e738e66489639f4189b7b2b93f5e8111fb5b85b38", + "usage": "provenance" + }, + { + "bytes": 5458, + "git_blob": "03a5942a7b35e5c22b2f9993589be4167d477759", + "path": "research/retuned-ordinary-coupling/certificate.py", + "sha256": "461aabd741d12e97278968dece22cc5435293e55d744808838865988856b0b2e", + "usage": "provenance" + }, + { + "bytes": 7031, + "git_blob": "dc4a415d78f2de81332a0b7e4256dd9f01fc3c9d", + "path": "research/retuned-ordinary-coupling/check_runtime.py", + "sha256": "82de942e6c609cf46533f8746cfd67ae55714cd39e808af3ebf00eed4f71a16b", + "usage": "provenance" + }, + { + "bytes": 4269, + "git_blob": "3a196ed2ae7030a75f4fadc423e15f0c4fb23193", + "path": "research/retuned-ordinary-coupling/check_setup.py", + "sha256": "5ccea0216b701e3e1adb6bb0890ba3db179b1d7b3d1a6e9913ac1fdc4d56bfca", + "usage": "provenance" + }, + { + "bytes": 8202240, + "git_blob": "5c07cf429005658400d7a64e229162ea845e5bf7", + "path": "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz", + "sha256": "0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c", + "usage": "provenance" + }, + { + "bytes": 858, + "git_blob": "6479a08fe78f7f4fe93d144cec26ac84aebcf9d3", + "path": "research/retuned-ordinary-coupling/interface.py", + "sha256": "25707c61b9fc6c1f09388c7cc72d269be0f8f8cae4dbc7cd5c2d00ce7fadf839", + "usage": "provenance" + }, + { + "bytes": 3336, + "git_blob": "31c08659c843dc114ae84d9c431bd749919c40bc", + "path": "research/retuned-ordinary-coupling/predecessor.py", + "sha256": "4733b33a6a840f73ebc87f0c3f9e9f1aee95438b10eae7f8dbbf20d5b11b2306", + "usage": "provenance" + }, + { + "bytes": 1582, + "git_blob": "d5cf4133d53a8bbbd95561df90b8f21ebcaea1cc", + "path": "research/retuned-ordinary-coupling/test_controls.py", + "sha256": "06f3ee0b77e8c9cf8c031b1f1c7590c6dc7b627ccf7d67fa17b7a79a0ba477b9", + "usage": "provenance" + }, + { + "bytes": 1428, + "git_blob": "9a21f9e08c5264abfd9d50968691f32a8c526484", + "path": "research/retuned-ordinary-coupling/verify.py", + "sha256": "887e878fd78f27b0029de651c94728f4e71314f08e562272dc9e52d66328fcb7", + "usage": "provenance" + }, + { + "bytes": 14768, + "git_blob": "6522e6ec84ed91bce98056456a88698b1cbfe1ad", + "path": "research/selected-bit-fast-primitives/PROOF.md", + "sha256": "c6912c307304b71ab51a5b9647df19a3e2c85efaca5bb3f1b635e918a62b5978", + "usage": "provenance" + }, + { + "bytes": 5381, + "git_blob": "22280ad31392300f4c2934800aa82a1fabf299b7", + "path": "research/selected-bit-fast-primitives/README.md", + "sha256": "46136a36462163003cecf93a78d4a435d170948676e9015bae22620589e9d57e", + "usage": "provenance" + }, + { + "bytes": 643, + "git_blob": "25bd73fd36d150c020a28d8ba3751c2320c2e11f", + "path": "research/selected-bit-fast-primitives/RESULT.json", + "sha256": "2af1012f3e3467588397bd5ba581d419442477caf0407ba48f8ee7e6137d1992", + "usage": "provenance" + }, + { + "bytes": 4857, + "git_blob": "bba64765508e3d293e40243b40409b671a3d0c2c", + "path": "research/selected-bit-fast-primitives/SOURCES.json", + "sha256": "12878f05f1cbc1ff4a0db76d5d39f4f991c1fe3b5d14865340bf75d5df79c6d5", + "usage": "provenance" + }, + { + "bytes": 7622, + "git_blob": "dba96083fefb88573d7388bea80f9c2b87e197d2", + "path": "research/selected-bit-fast-primitives/TASK.json", + "sha256": "b415aee0f8d9bfded525cb47d3aa04ea97680abf16a02a89888ac0dc5ab2ecbd", + "usage": "provenance" + }, + { + "bytes": 2898, + "git_blob": "606bf32c4fc154f9ace0fcd51ec9857a51e1876a", + "path": "research/selected-bit-fast-primitives/VERIFY.json", + "sha256": "fee812dbe7905c31c39bf97920c88deb442b152a2cfb261c86c169fbad4d1edc", + "usage": "provenance" + }, + { + "bytes": 5321, + "git_blob": "c3085e1d648ff2ba8d774d1739854306b84e5798", + "path": "research/selected-bit-fast-primitives/check_caller.py", + "sha256": "75808ef9a1b65d620109717ab4af88598777a39cfc4d4bc2e42d3788233f029b", + "usage": "provenance" + }, + { + "bytes": 3067, + "git_blob": "7368d63e1a7c54c29d622324e35f4115884adc10", + "path": "research/selected-bit-fast-primitives/check_catalogue.py", + "sha256": "f7cc1c7907fd1877e310ba41904110a40e52f091ad38442ab2398c798afd3644", + "usage": "provenance" + }, + { + "bytes": 2216, + "git_blob": "d4db3439979d347a1ab6a96b978c8d3dbfa5cb7e", + "path": "research/selected-bit-fast-primitives/check_complete.py", + "sha256": "0751dd27a129823894cd7ade7ba73fcc84c825ecf5fcdd1fedac11ca08526d9d", + "usage": "provenance" + }, + { + "bytes": 3183, + "git_blob": "bee3f603c989358b8e6169bd7770ebf9280b3a00", + "path": "research/selected-bit-fast-primitives/check_controls.py", + "sha256": "d0b41aec46462f6b351935efdd8b200eb4de72fa2f8784cfa672fe3607711d91", + "usage": "provenance" + }, + { + "bytes": 4539, + "git_blob": "96051d7ca03bd38541d86289cdb6ec5fed98e707", + "path": "research/selected-bit-fast-primitives/check_handoff.py", + "sha256": "be1436e32bfad474330b69905aa6e4bfdb1a3538c295ace0f0ef96f40a34661a", + "usage": "provenance" + }, + { + "bytes": 3933, + "git_blob": "f4525ca47b90151f5461b01ed33ff80d64931ffe", + "path": "research/selected-bit-fast-primitives/check_kernels.py", + "sha256": "dd35d535e6986687bee112cef2003569252fc473acbce98f1a64b66e84083cc2", + "usage": "provenance" + }, + { + "bytes": 1083, + "git_blob": "013b959cc9fc4a37f0c109cda4ffc37d639a5473", + "path": "research/selected-bit-fast-primitives/check_outer.py", + "sha256": "b303f94091b1a09333532c57182808e5e049ad8b00dc77d491c664f5c5351ee3", + "usage": "provenance" + }, + { + "bytes": 5109, + "git_blob": "0b05ab1e4de1e10fe651c72da883887cb44a643d", + "path": "research/selected-bit-fast-primitives/check_routes.py", + "sha256": "28803eb270202e2742c713bf14ead47f44c8b5341a380c156bce7392ebed642d", + "usage": "provenance" + }, + { + "bytes": 5110, + "git_blob": "37263fdc327b4a300ccfaa0b7ad650012ab3d59c", + "path": "research/selected-bit-fast-primitives/compile_routes.py", + "sha256": "1bfef464dfb3e33d9d57f53b657b2d1fe3598bc453be49000a5e782b622e8585", + "usage": "provenance" + }, + { + "bytes": 4056, + "git_blob": "ec7481f890147be7763f4da729fd879a88a87e8e", + "path": "research/selected-bit-fast-primitives/high_route.py", + "sha256": "13d9c706e7bad2fa3b7d2a97d19b58f2c4efac06d2bb76b613b40069c38b1cd2", + "usage": "provenance" + }, + { + "bytes": 71680, + "git_blob": "9504807466071f56519f8663ccb532076a42a273", + "path": "research/selected-bit-fast-primitives/inputs/pr2157.tar", + "sha256": "db202c7b91b5b8b9340f96f870d54e275854f0b73839451c7c15bd7895ac3639", + "usage": "provenance" + }, + { + "bytes": 1382400, + "git_blob": "e85ce82745879141e416ac6d9e3551ff959871aa", + "path": "research/selected-bit-fast-primitives/inputs/pr2899.tar", + "sha256": "fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531", + "usage": "provenance" + }, + { + "bytes": 4506, + "git_blob": "de9fb08c35e92c8354ae622276866385fd07e3d2", + "path": "research/selected-bit-fast-primitives/kernels.py", + "sha256": "c4b91333817f7fcea44b1d32e01095cd71aeb673ed3608d2e25f4c06d56bb420", + "usage": "provenance" + }, + { + "bytes": 6863, + "git_blob": "765ae9e11af3acb9458d7a1444a9e79112b72d96", + "path": "research/selected-bit-fast-primitives/stage.py", + "sha256": "44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647", + "usage": "provenance" + }, + { + "bytes": 2595, + "git_blob": "27383dd1553672f9c82139f80b628b2a094628d8", + "path": "research/selected-bit-fast-primitives/stage_sources.py", + "sha256": "55c6631cce4f76e14b66b6195468c36b544e2374cc6c59702135c664bff10822", + "usage": "provenance" + }, + { + "bytes": 1226, + "git_blob": "a2f602c15cd413638116b4ea9bcffe613e4e3a7d", + "path": "research/selected-bit-fast-primitives/verify.py", + "sha256": "90760db1526f73cfffc34eb8af3f2e5ec83f8f1015a780caa61d156f0d850c68", + "usage": "provenance" + }, + { + "bytes": 16491, + "git_blob": "4330de85dd9862ed15d84ab917887d249753df99", + "path": "research/selected-bit-local-ring-sweeps/PROOF.md", + "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7", + "usage": "provenance" + }, + { + "bytes": 23425, + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "path": "research/selected-bit-recursive-closure/PROOF.md", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344", + "usage": "provenance" + }, + { + "bytes": 11311, + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "path": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "usage": "provenance" + } + ], + "schema_version": 1, + "scientific_base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "scope": "Immutable B2 arithmetic/proof inputs, complete selected fast-primitive and retuned packages, their selected live-source inputs, and nested unchanged backend exports. No source execution is certified." +} diff --git a/research/ordinary-b2-bootstrap/SOURCES.json b/research/ordinary-b2-bootstrap/SOURCES.json new file mode 100644 index 0000000000..32d29abb58 --- /dev/null +++ b/research/ordinary-b2-bootstrap/SOURCES.json @@ -0,0 +1,336 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "path": "certificates/selected-result.json", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "input" + }, + { + "git_blob": "ede0d322c477af91d4c2cc33db0fd10958f45eab", + "path": "research/bit2234-stock-threshold/README.md", + "sha256": "1e050c9f963421d751d9208092f9a15321ed77810e03912df8eb5eb56bbb06e7", + "usage": "input" + }, + { + "git_blob": "915d08efd81fa304e1974e26d8212803e03e6623", + "path": "research/bootstrap-depth-audit/sources/pr387/PROOF.md", + "sha256": "15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8", + "usage": "input" + }, + { + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "usage": "input" + }, + { + "git_blob": "9eafb8776cbf78c72124f833534469ddfa5e98ec", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz", + "sha256": "0357b7cfbd7c29b4983982baf153c8a9f1e1e412690cd7fa9fc3d23d7963b20f", + "usage": "input" + }, + { + "git_blob": "1f648db9e63e7bfcaa6d5b1dd9fa6503caac47d2", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json", + "sha256": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819", + "usage": "input" + }, + { + "git_blob": "44006542202ca6037533a754f0bcd00549d7e088", + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json", + "sha256": "0058c491d839142aa99ef86a5ec697ce99857632228531512ea3fa74fb24d734", + "usage": "input" + }, + { + "git_blob": "93a588a73a38050dfa0a383cb44f228aff6f243e", + "path": "research/community-round8-audit/pr185-proof-reviewed.md", + "sha256": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa", + "usage": "input" + }, + { + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "usage": "input" + }, + { + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "usage": "input" + }, + { + "git_blob": "4468a00349b4f68dce103e785a8392099435e1d6", + "path": "research/idle-axis-hosting/PROOF.md", + "sha256": "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542", + "usage": "input" + }, + { + "git_blob": "f65f38123ca0adb02f6ca69351cbfc933506e5cb", + "path": "research/physical-complex-compact/PROOF.md", + "sha256": "ec6395822ae500242f3fe5e2cf40caf9a7f9fa259d475d2c14970d951ff4df48", + "usage": "input" + }, + { + "git_blob": "bbd3f12b9a32b3ad3cba85a2d5a1b3054214fa02", + "path": "research/pr589-five-helper-hosting/PROOF.md", + "sha256": "59cae781bfbe1a01ed9e66a8efeeb5a2b995e5ecdf908586b23ecc39f2b8d647", + "usage": "input" + }, + { + "git_blob": "dbc71f56bb4205ebe378ada1f9f4ea88630d1d39", + "path": "research/pr589-five-helper-hosting/verify.py", + "sha256": "cf90e19ae9991b0698be03d395a8cc29061ecb307eb7fea19adfb2d23c25a367", + "usage": "input" + }, + { + "git_blob": "251f335ebaccc11d69393ee7aeb5a2e84526d0bb", + "path": "research/recursive-parking-boundary/README.md", + "sha256": "491aa208391ee4c2936510b1a5c5c018dd5509d9a0e88687c72ab8406cd77b18", + "usage": "input" + }, + { + "git_blob": "b370d63711733f6eb9685a96d09ca1964f685c51", + "path": "research/retuned-ordinary-coupling/EVIDENCE.md", + "sha256": "3cea6f279f0ae302f3432e1c67955ed009d2a9e569192b690f68627c62c2c3cb", + "usage": "input" + }, + { + "git_blob": "8a0f47a1541a0b8e67866df4f65928de31073651", + "path": "research/retuned-ordinary-coupling/PROOF.md", + "sha256": "3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22", + "usage": "input" + }, + { + "git_blob": "21a248de1d9ea63c88ed596554af307a36360383", + "path": "research/retuned-ordinary-coupling/README.md", + "sha256": "b342b26f131e67cd6e5bc143a41845e40eaec349af19648a6f76bc2c43ec0983", + "usage": "input" + }, + { + "git_blob": "2d346515fb715a1e6d91371e89aa6727ef25d3d9", + "path": "research/retuned-ordinary-coupling/SOURCES.json", + "sha256": "d4208b2d236c6055cc86c1d8ba8ce5cf54263ec5034556b0d70fbab3fbd7796e", + "usage": "input" + }, + { + "git_blob": "dc1ca38c3b0758bde1d7bf0f035014021e1e3c2a", + "path": "research/retuned-ordinary-coupling/TASK.json", + "sha256": "cf0749a2e4c805b28e5284f519fdcb43f203d77c3fd227d8581cb1079454fb1e", + "usage": "input" + }, + { + "git_blob": "7fe1448397d60577fe8445c64f6424cb8bb80422", + "path": "research/retuned-ordinary-coupling/VERIFY.json", + "sha256": "a46e323a04b959c76ceea82e738e66489639f4189b7b2b93f5e8111fb5b85b38", + "usage": "input" + }, + { + "git_blob": "03a5942a7b35e5c22b2f9993589be4167d477759", + "path": "research/retuned-ordinary-coupling/certificate.py", + "sha256": "461aabd741d12e97278968dece22cc5435293e55d744808838865988856b0b2e", + "usage": "input" + }, + { + "git_blob": "dc4a415d78f2de81332a0b7e4256dd9f01fc3c9d", + "path": "research/retuned-ordinary-coupling/check_runtime.py", + "sha256": "82de942e6c609cf46533f8746cfd67ae55714cd39e808af3ebf00eed4f71a16b", + "usage": "input" + }, + { + "git_blob": "3a196ed2ae7030a75f4fadc423e15f0c4fb23193", + "path": "research/retuned-ordinary-coupling/check_setup.py", + "sha256": "5ccea0216b701e3e1adb6bb0890ba3db179b1d7b3d1a6e9913ac1fdc4d56bfca", + "usage": "input" + }, + { + "git_blob": "5c07cf429005658400d7a64e229162ea845e5bf7", + "path": "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz", + "sha256": "0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c", + "usage": "input" + }, + { + "git_blob": "6479a08fe78f7f4fe93d144cec26ac84aebcf9d3", + "path": "research/retuned-ordinary-coupling/interface.py", + "sha256": "25707c61b9fc6c1f09388c7cc72d269be0f8f8cae4dbc7cd5c2d00ce7fadf839", + "usage": "input" + }, + { + "git_blob": "31c08659c843dc114ae84d9c431bd749919c40bc", + "path": "research/retuned-ordinary-coupling/predecessor.py", + "sha256": "4733b33a6a840f73ebc87f0c3f9e9f1aee95438b10eae7f8dbbf20d5b11b2306", + "usage": "input" + }, + { + "git_blob": "d5cf4133d53a8bbbd95561df90b8f21ebcaea1cc", + "path": "research/retuned-ordinary-coupling/test_controls.py", + "sha256": "06f3ee0b77e8c9cf8c031b1f1c7590c6dc7b627ccf7d67fa17b7a79a0ba477b9", + "usage": "input" + }, + { + "git_blob": "9a21f9e08c5264abfd9d50968691f32a8c526484", + "path": "research/retuned-ordinary-coupling/verify.py", + "sha256": "887e878fd78f27b0029de651c94728f4e71314f08e562272dc9e52d66328fcb7", + "usage": "input" + }, + { + "git_blob": "6522e6ec84ed91bce98056456a88698b1cbfe1ad", + "path": "research/selected-bit-fast-primitives/PROOF.md", + "sha256": "c6912c307304b71ab51a5b9647df19a3e2c85efaca5bb3f1b635e918a62b5978", + "usage": "input" + }, + { + "git_blob": "22280ad31392300f4c2934800aa82a1fabf299b7", + "path": "research/selected-bit-fast-primitives/README.md", + "sha256": "46136a36462163003cecf93a78d4a435d170948676e9015bae22620589e9d57e", + "usage": "input" + }, + { + "git_blob": "25bd73fd36d150c020a28d8ba3751c2320c2e11f", + "path": "research/selected-bit-fast-primitives/RESULT.json", + "sha256": "2af1012f3e3467588397bd5ba581d419442477caf0407ba48f8ee7e6137d1992", + "usage": "input" + }, + { + "git_blob": "bba64765508e3d293e40243b40409b671a3d0c2c", + "path": "research/selected-bit-fast-primitives/SOURCES.json", + "sha256": "12878f05f1cbc1ff4a0db76d5d39f4f991c1fe3b5d14865340bf75d5df79c6d5", + "usage": "input" + }, + { + "git_blob": "dba96083fefb88573d7388bea80f9c2b87e197d2", + "path": "research/selected-bit-fast-primitives/TASK.json", + "sha256": "b415aee0f8d9bfded525cb47d3aa04ea97680abf16a02a89888ac0dc5ab2ecbd", + "usage": "input" + }, + { + "git_blob": "606bf32c4fc154f9ace0fcd51ec9857a51e1876a", + "path": "research/selected-bit-fast-primitives/VERIFY.json", + "sha256": "fee812dbe7905c31c39bf97920c88deb442b152a2cfb261c86c169fbad4d1edc", + "usage": "input" + }, + { + "git_blob": "c3085e1d648ff2ba8d774d1739854306b84e5798", + "path": "research/selected-bit-fast-primitives/check_caller.py", + "sha256": "75808ef9a1b65d620109717ab4af88598777a39cfc4d4bc2e42d3788233f029b", + "usage": "input" + }, + { + "git_blob": "7368d63e1a7c54c29d622324e35f4115884adc10", + "path": "research/selected-bit-fast-primitives/check_catalogue.py", + "sha256": "f7cc1c7907fd1877e310ba41904110a40e52f091ad38442ab2398c798afd3644", + "usage": "input" + }, + { + "git_blob": "d4db3439979d347a1ab6a96b978c8d3dbfa5cb7e", + "path": "research/selected-bit-fast-primitives/check_complete.py", + "sha256": "0751dd27a129823894cd7ade7ba73fcc84c825ecf5fcdd1fedac11ca08526d9d", + "usage": "input" + }, + { + "git_blob": "bee3f603c989358b8e6169bd7770ebf9280b3a00", + "path": "research/selected-bit-fast-primitives/check_controls.py", + "sha256": "d0b41aec46462f6b351935efdd8b200eb4de72fa2f8784cfa672fe3607711d91", + "usage": "input" + }, + { + "git_blob": "96051d7ca03bd38541d86289cdb6ec5fed98e707", + "path": "research/selected-bit-fast-primitives/check_handoff.py", + "sha256": "be1436e32bfad474330b69905aa6e4bfdb1a3538c295ace0f0ef96f40a34661a", + "usage": "input" + }, + { + "git_blob": "f4525ca47b90151f5461b01ed33ff80d64931ffe", + "path": "research/selected-bit-fast-primitives/check_kernels.py", + "sha256": "dd35d535e6986687bee112cef2003569252fc473acbce98f1a64b66e84083cc2", + "usage": "input" + }, + { + "git_blob": "013b959cc9fc4a37f0c109cda4ffc37d639a5473", + "path": "research/selected-bit-fast-primitives/check_outer.py", + "sha256": "b303f94091b1a09333532c57182808e5e049ad8b00dc77d491c664f5c5351ee3", + "usage": "input" + }, + { + "git_blob": "0b05ab1e4de1e10fe651c72da883887cb44a643d", + "path": "research/selected-bit-fast-primitives/check_routes.py", + "sha256": "28803eb270202e2742c713bf14ead47f44c8b5341a380c156bce7392ebed642d", + "usage": "input" + }, + { + "git_blob": "37263fdc327b4a300ccfaa0b7ad650012ab3d59c", + "path": "research/selected-bit-fast-primitives/compile_routes.py", + "sha256": "1bfef464dfb3e33d9d57f53b657b2d1fe3598bc453be49000a5e782b622e8585", + "usage": "input" + }, + { + "git_blob": "ec7481f890147be7763f4da729fd879a88a87e8e", + "path": "research/selected-bit-fast-primitives/high_route.py", + "sha256": "13d9c706e7bad2fa3b7d2a97d19b58f2c4efac06d2bb76b613b40069c38b1cd2", + "usage": "input" + }, + { + "git_blob": "9504807466071f56519f8663ccb532076a42a273", + "path": "research/selected-bit-fast-primitives/inputs/pr2157.tar", + "sha256": "db202c7b91b5b8b9340f96f870d54e275854f0b73839451c7c15bd7895ac3639", + "usage": "input" + }, + { + "git_blob": "e85ce82745879141e416ac6d9e3551ff959871aa", + "path": "research/selected-bit-fast-primitives/inputs/pr2899.tar", + "sha256": "fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531", + "usage": "input" + }, + { + "git_blob": "de9fb08c35e92c8354ae622276866385fd07e3d2", + "path": "research/selected-bit-fast-primitives/kernels.py", + "sha256": "c4b91333817f7fcea44b1d32e01095cd71aeb673ed3608d2e25f4c06d56bb420", + "usage": "input" + }, + { + "git_blob": "765ae9e11af3acb9458d7a1444a9e79112b72d96", + "path": "research/selected-bit-fast-primitives/stage.py", + "sha256": "44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647", + "usage": "input" + }, + { + "git_blob": "27383dd1553672f9c82139f80b628b2a094628d8", + "path": "research/selected-bit-fast-primitives/stage_sources.py", + "sha256": "55c6631cce4f76e14b66b6195468c36b544e2374cc6c59702135c664bff10822", + "usage": "input" + }, + { + "git_blob": "a2f602c15cd413638116b4ea9bcffe613e4e3a7d", + "path": "research/selected-bit-fast-primitives/verify.py", + "sha256": "90760db1526f73cfffc34eb8af3f2e5ec83f8f1015a780caa61d156f0d850c68", + "usage": "input" + }, + { + "git_blob": "4330de85dd9862ed15d84ab917887d249753df99", + "path": "research/selected-bit-local-ring-sweeps/PROOF.md", + "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7", + "usage": "input" + }, + { + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "path": "research/selected-bit-recursive-closure/PROOF.md", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344", + "usage": "input" + }, + { + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "path": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "usage": "input" + }, + { + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "path": "docs/research/agent-task-catalog.json", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/ordinary-b2-bootstrap/TASK.json b/research/ordinary-b2-bootstrap/TASK.json new file mode 100644 index 0000000000..659c63ba0a --- /dev/null +++ b/research/ordinary-b2-bootstrap/TASK.json @@ -0,0 +1,80 @@ +{ + "actual_scope": "Independent draft of the existing conditional ordinary B2 rate and complete tariff, with unchanged exact mathematical evidence and source compatibility.", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review or formal-kernel proof claimed.", + "author": "Ross Richardson", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "bottleneck_link": "A stronger ordinary stage can remove a rate obstruction while complete complex and outer admission remain separate.", + "budget_minutes": 60, + "evidence": "PROOF.md gives the source-relative argument; evidence/B2-BOOTSTRAP.json is compared in full and by historical mathematical projection.", + "open_questions": [ + { + "blocked_by": "The new factory and its caller-specific admission are not included.", + "first_step": "Instantiate the two distinct Ordinary owners and sealed preceding-stage registry described in PROOF.md; test complete dirty endpoints and literal cleanup.", + "question": "Implement and independently audit the source-relative production B2 factory at its complete returned interface.", + "why_it_matters": "The bounded checker certifies rates and source compatibility but does not execute the production composition." + }, + { + "blocked_by": "A completed production B2 interface and a separate complex/outer proof are required.", + "first_step": "Use the complete compact tariff and check the actual root, stopping, hosting and outer domains.", + "question": "Bind B2 to one actual complex compact caller with every restoration and recursive cost.", + "why_it_matters": "An ordinary-rate gain alone does not establish a multiplication exponent." + } + ], + "original_card": { + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "existing_checks": [ + { + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "author-checked" + } + ], + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "id": "uniform-transfer-audit", + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ] + }, + "outcome": "partial", + "priority_revision": 7, + "schema_version": 1, + "scope_change_reason": "Explicit user request extracts the optional B2 result from PR4270 and replaces its duplicate source archive with the same declared canonical inputs; no new scientific claim.", + "scope_status": "changed", + "stop_rule": "Preserve all mathematical fields and eleven controls, authenticate the complete pinned input inventory, and finish normal/optimized and cold-export checks. No production factory or new kappa theorem.", + "task_id": "uniform-transfer-audit" +} diff --git a/research/ordinary-b2-bootstrap/VERIFY.json b/research/ordinary-b2-bootstrap/VERIFY.json new file mode 100644 index 0000000000..80496c14b2 --- /dev/null +++ b/research/ordinary-b2-bootstrap/VERIFY.json @@ -0,0 +1,87 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/b2_bootstrap.py", + "--check", + "{package}/evidence/B2-BOOTSTRAP.json" + ], + "checks": "Authenticate all 54 exact canonical inputs and original interval-engine bytes; independent rational-series/integer-power full BIT moment, complete B2 tariffs/stock fit, 23 backend equalities, historical mathematical projection, and all 11 negative controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/b2_bootstrap.py", + "--check", + "{package}/evidence/B2-BOOTSTRAP.json" + ], + "checks": "Authenticate all 54 exact canonical inputs and original interval-engine bytes; independent rational-series/integer-power full BIT moment, complete B2 tariffs/stock fit, 23 backend equalities, historical mathematical projection, and all 11 negative controls.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "certificates/selected-result.json", + "research/bit2234-stock-threshold/README.md", + "research/bootstrap-depth-audit/sources/pr387/PROOF.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz", + "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json", + "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json", + "research/community-round8-audit/pr185-proof-reviewed.md", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/idle-axis-hosting/PROOF.md", + "research/physical-complex-compact/PROOF.md", + "research/pr589-five-helper-hosting/PROOF.md", + "research/pr589-five-helper-hosting/verify.py", + "research/recursive-parking-boundary/README.md", + "research/retuned-ordinary-coupling/EVIDENCE.md", + "research/retuned-ordinary-coupling/PROOF.md", + "research/retuned-ordinary-coupling/README.md", + "research/retuned-ordinary-coupling/SOURCES.json", + "research/retuned-ordinary-coupling/TASK.json", + "research/retuned-ordinary-coupling/VERIFY.json", + "research/retuned-ordinary-coupling/certificate.py", + "research/retuned-ordinary-coupling/check_runtime.py", + "research/retuned-ordinary-coupling/check_setup.py", + "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz", + "research/retuned-ordinary-coupling/interface.py", + "research/retuned-ordinary-coupling/predecessor.py", + "research/retuned-ordinary-coupling/test_controls.py", + "research/retuned-ordinary-coupling/verify.py", + "research/selected-bit-fast-primitives/PROOF.md", + "research/selected-bit-fast-primitives/README.md", + "research/selected-bit-fast-primitives/RESULT.json", + "research/selected-bit-fast-primitives/SOURCES.json", + "research/selected-bit-fast-primitives/TASK.json", + "research/selected-bit-fast-primitives/VERIFY.json", + "research/selected-bit-fast-primitives/check_caller.py", + "research/selected-bit-fast-primitives/check_catalogue.py", + "research/selected-bit-fast-primitives/check_complete.py", + "research/selected-bit-fast-primitives/check_controls.py", + "research/selected-bit-fast-primitives/check_handoff.py", + "research/selected-bit-fast-primitives/check_kernels.py", + "research/selected-bit-fast-primitives/check_outer.py", + "research/selected-bit-fast-primitives/check_routes.py", + "research/selected-bit-fast-primitives/compile_routes.py", + "research/selected-bit-fast-primitives/high_route.py", + "research/selected-bit-fast-primitives/inputs/pr2157.tar", + "research/selected-bit-fast-primitives/inputs/pr2899.tar", + "research/selected-bit-fast-primitives/kernels.py", + "research/selected-bit-fast-primitives/stage.py", + "research/selected-bit-fast-primitives/stage_sources.py", + "research/selected-bit-fast-primitives/verify.py", + "research/selected-bit-local-ring-sweeps/PROOF.md", + "research/selected-bit-recursive-closure/PROOF.md", + "upstream/build/sections/02-streams.tex" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/ordinary-b2-bootstrap/b2_bootstrap.py b/research/ordinary-b2-bootstrap/b2_bootstrap.py new file mode 100644 index 0000000000..072dc49828 --- /dev/null +++ b/research/ordinary-b2-bootstrap/b2_bootstrap.py @@ -0,0 +1,292 @@ +#!/usr/bin/env python3 +"""Exact B2 pricing and source compatibility; no production machine replay. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. Mathematical dependencies retain their authors and source scope. +""" +import argparse +from fractions import Fraction as Q +from functools import lru_cache +import hashlib +import io +import json +from pathlib import Path, PurePosixPath +import tarfile +import types + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +H = {1: 381024, 2: 400416, 3: 22752, 4: 26880, + 5: 29376, 6: 17376, 7: 26784, 42: 288} +W = 28416 +C = Q("0.001730980255989036959962") +A1 = Q(169711, 10**8) +COUPLING = Q(1, 577) +TARGET = Q("0.001727989140903569") +BIT_LOWER = Q("0.001733427039589844234749") +FALLBACK = Q(32 * 64**2 * sum(H.values()), 10**16) +FAST_ARCHIVE = "research/selected-bit-fast-primitives/inputs/pr2899.tar" +RETUNED_ARCHIVE = "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def digest(body): + return hashlib.sha256(body).hexdigest() + + +def checked_body(path, expected): + need(path.is_file() and not path.is_symlink(), "regular pinned input: " + str(path)) + body = path.read_bytes() + need(digest(body) == expected, "source SHA256: " + str(path)) + return body + + +def complete_members(members, manifest): + expected = {row["path"]: row["sha256"] for row in manifest["files"]} + need(len(expected) == len(manifest["files"]), "unique source-manifest paths") + need(set(members) == set(expected), "complete vendored B2 source inventory") + need(all(digest(members[name]) == sha for name, sha in expected.items()), + "vendored B2 member SHA256") + + +def sources(source_root=None): + pins = json.loads((HERE / "B2-PINS.json").read_bytes()) + need(pins["schema_version"] == 3, "B2 pin schema") + local = {name: checked_body(HERE / name, sha) + for name, sha in pins["local_inputs"].items()} + bundle = pins["source_bundle"] + manifest = json.loads(checked_body(HERE / bundle["manifest"], bundle["manifest_sha256"])) + need(manifest["scientific_base"] == pins["scientific_base"], "B2 source base") + need(bundle["kind"] == "declared-pinned-repository-inputs", "pinned repository transport") + root = REPO if source_root is None else source_root + external = {row["path"]: checked_body(root / row["path"], row["sha256"]) + for row in manifest["files"]} + complete_members(external, manifest) + need(all(digest(external[name]) == sha for name, sha in pins["source_inputs"].items()), + "theorem and backend input SHA256") + # Compile exactly the authenticated bytes, without a bytecode-cache loader. + engine = types.ModuleType("b2_authenticated_joint_engine") + engine.__file__ = str(HERE / "frozen/interval_engine.py") + exec(compile(local["frozen/interval_engine.py"], engine.__file__, "exec"), engine.__dict__) + bit = json.loads(external["research/e8-bit-p111-tuned/tune/EXPECTED.json"])["nine"] + need({int(k): int(v) for k, v in bit["profile"].items()} == H, + "complete selected BIT profile") + need(bit["bit"]["live"] == W and sum(H.values()) == 904896, + "complete selected BIT stock and child count") + need(Q(bit["bit_lower"]) == BIT_LOWER > COUPLING, "coarse BIT headroom") + return pins, external, engine, manifest + + +@lru_cache(maxsize=None) +def root_power(rank, saving=COUPLING): + """Independent integer-only enclosure of (rank/64)^(1-saving).""" + need(0 < rank < 64 and 0 < saving < 1, "power domain") + numerator, denominator = (1-saving).as_integer_ratio() + scale = 1 << 160 + target = rank**numerator * scale**denominator + divisor = 64**numerator + lo, hi = 0, scale + while hi-lo > 1: + middle = (lo+hi)//2 + if middle**denominator * divisor <= target: + lo = middle + else: + hi = middle + need(lo**denominator * divisor <= target < hi**denominator * divisor, + "outward integer-power enclosure") + return Q(lo, scale), Q(hi, scale) + + +def integer_moment(saving=COUPLING, fallback=FALLBACK): + low = high = Q(0) + for rank, count in H.items(): + weight = (Q(count) + (fallback if rank == 1 else 0))/W + lo, hi = root_power(rank, saving) + low += weight*lo + high += weight*hi + return low, high + + +def decimal_enclosure(bounds, digits=30): + low, high = bounds + scale = 10**digits + return [low.numerator*scale//low.denominator, + -(-high.numerator*scale//high.denominator), scale] + + +def archive_members(body): + # No extraction or execution. The entire archive has already been pinned. + with tarfile.open(fileobj=io.BytesIO(body), mode="r:*") as archive: + all_items = archive.getmembers() + need(all((member.isfile() or member.isdir()) + and not PurePosixPath(member.name).is_absolute() + and ".." not in PurePosixPath(member.name).parts + for member in all_items), "safe relative regular archive members") + items = [member for member in all_items if member.isfile()] + need(len({member.name for member in items}) == len(items), + "unique archived regular-file names") + return {member.name: archive.extractfile(member).read() for member in items} + + +def same_backend(fast, retuned): + need(len(fast) == 23 and len(retuned) == 35 and set(fast) <= set(retuned), + "complete ordinary backend inventories") + need(all(fast[name] == retuned[name] for name in fast), + "byte-identical common ordinary backend") + + +def legacy_ceiling(rate): + eta = Q(1, 10**24) + q = (1-2*eta)*rate + return (1-eta)*q/(1+q) + + +def check_power_coefficient(coefficient, moment_upper): + need(coefficient*(1-moment_upper) > 1, "complete power-moment tariff") + + +def check_fit(bits): + need(bits in (19, 20), "fixed sufficient-fit comparison domain") + need(32780*Q(17, 16)*bits < 2**bits, "whole original-width stock fits") + + +def wrapper_coefficient(padded_root_factor=4): + need(padded_root_factor == 4, "two ROOT calls each require below-two volume padding") + return (padded_root_factor*200+1 + + padded_root_factor*10**6*Q(17, 16)+32780+2+1) + + +def reject(name, operation): + try: + operation() + except (ValueError, KeyError): + return name + raise ValueError("control accepted: " + name) + + +def certificate(source_root=None): + pins, external, engine, manifest = sources(source_root) + series = tuple(x+1 for x in engine.moment(H, 64, W, COUPLING, FALLBACK)) + integer = integer_moment() + need(max(integer[0], series[0]) <= min(integer[1], series[1]), + "independent rational moment overlap") + expected = [999998938581682162866772413602, + 999998938581682162866772413603, 10**30] + need(decimal_enclosure(integer) == decimal_enclosure(series) == expected, + "matching independent outward decimal enclosures") + upper = max(integer[1], series[1]) + lower = min(integer[0], series[0]) + check_power_coefficient(10**6, upper) + need(lower > Q(9999, 10000), "old power tariff is unavailable") + mu1 = (sum(Q(r*n, 64) for r, n in H.items())+FALLBACK/64)/W + need(mu1 == Q(2874298095721977, 2890625000000000) < Q(199, 200), + "exact complete linear moment") + a2 = COUPLING*(1-COUPLING)+COUPLING*A1 + need(a2 == Q(57697923247, 33292900000000) > C, "B2 clears complex rate") + gaps = {"atom": COUPLING-a2, "borrowing": 1-a2-COUPLING, + "remainder": 1-a2-COUPLING*(1-A1), "stock": 1-COUPLING} + need(all(x > 0 for x in gaps.values()) and min(gaps.values()) == COUPLING-a2, + "four strict completed-bootstrap gaps") + need(A1 < COUPLING < Q(1, 512) and 1-a2-COUPLING > Q(1, 2), + "full wrapper power absorption") + need(17**128 > 32*16**128, "fixed power-factor bound") + check_fit(20) + coefficient = wrapper_coefficient() + need(coefficient == 4283584 < 4300000, "complete two-root and wrapper coefficient") + eta = Q(1, 10**24) + s = (1-eta)*C-Q(1, 10**27) + inadequate = s*(1-s)+s*A1 + need(inadequate > TARGET > legacy_ceiling(inadequate), + "ordinary rate alone does not pay the legacy outer loss") + baseline = COUPLING*(1-COUPLING) + need(baseline < C, "unpromoted retuned C0 is insufficient") + fast = archive_members(external[FAST_ARCHIVE]) + retuned = archive_members(external[RETUNED_ARCHIVE]) + retuned = {name.removeprefix("research/physical-ordinary-interchange/"): body + for name, body in retuned.items() if not name.startswith(".")} + same_backend(fast, retuned) + changed = dict(fast) + changed["ordinary.py"] += b"\n# changed source\n" + bad_moment = integer_moment(Q(1, 576)) + full_next = engine.moment(H, 64, W, BIT_LOWER+Q(1, 10**24), FALLBACK) + omitted_next = engine.moment(H, 64, W, BIT_LOWER+Q(1, 10**24), Q(0)) + need(full_next[0] > 0 > omitted_next[1], "fallback changes the endpoint decision") + controls = [ + reject("omitted_bit_fallback", lambda: need(omitted_next[0] > 0, "paid endpoint reject sign")), + reject("old_10000_power_coefficient", lambda: check_power_coefficient(10000, upper)), + reject("profile_only_without_C1", lambda: need(baseline > C, "completed C1 required")), + reject("ordinary_rate_substituted_for_kappa", + lambda: need(legacy_ceiling(inadequate) > TARGET, "legacy outer margin")), + reject("coupling_1_over_576", lambda: need(bad_moment[0] < 1, "complete BIT moment")), + reject("stock_cutoff_2_power_19", lambda: check_fit(19)), + reject("missing_two_call_padding", lambda: wrapper_coefficient(2)), + reject("changed_backend_member", lambda: same_backend(changed, retuned)), + reject("changed_stage_source", lambda: need( + digest(external["research/selected-bit-fast-primitives/stage.py"]+b"\n") + == pins["source_inputs"]["research/selected-bit-fast-primitives/stage.py"], + "stage source hash")), + reject("missing_vendored_source", lambda: complete_members( + {name: body for name, body in external.items() if name != FAST_ARCHIVE}, manifest)), + reject("changed_vendored_source", lambda: complete_members( + {**external, FAST_ARCHIVE: external[FAST_ARCHIVE]+b"\n"}, manifest)), + ] + return { + "status": "PASS_B2_EXACT_ARITHMETIC_AND_BACKEND_SOURCE_COMPATIBILITY", + "a1": str(A1), "coupling": str(COUPLING), "B2_saving": str(a2), + "complex_lower": str(C), "B2_minus_complex": str(a2-C), + "strict_gaps": {name: str(value) for name, value in gaps.items()}, + "full_bit_mu1": str(mu1), "full_bit_mu_decimal": expected, + "full_bit_mu_series": list(map(str, series)), + "full_bit_mu_integer_power": list(map(str, integer)), + "fallback_rank_one_count": str(FALLBACK), + "fallback_decisive_endpoint": str(BIT_LOWER+Q(1, 10**24)), + "C1_linear_coefficient": 200, "C1_power_coefficient": 10**6, + "B2_wrapper_coefficient": int(coefficient), "physical_fit_from": 2**20, + "source_backend_equal_files": len(fast), + "backend_common_member_sha256": {name: digest(body) for name, body in sorted(fast.items())}, + "source_pins_sha256": digest((HERE / "B2-PINS.json").read_bytes()), + "source_inputs": pins["source_inputs"], "local_inputs": pins["local_inputs"], + "source_bundle": pins["source_bundle"], "source_bundle_files": len(external), + "complex_coupling_counterexample": { + "a_next": str(inadequate), "legacy_outer_ceiling": str(legacy_ceiling(inadequate)), + "target": str(TARGET), "ceiling_minus_target": str(legacy_ceiling(inadequate)-TARGET)}, + "controls_rejected": controls, + "production_factory_executed": False, "all_size_complex_admission": False, + "scope": "Exact B2 rates, complete tariffs and source compatibility under retained physical/source arguments; no production retuned-C1 execution or new complex/outer admission.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--source-root", type=Path, + help="read the same complete pinned inputs from another source root") + parser.add_argument("--output", type=Path) + parser.add_argument("--check", type=Path, help="compare the complete deterministic receipt") + args = parser.parse_args() + result = certificate(args.source_root.resolve() if args.source_root else None) + historical = json.loads((HERE / "B2-PINS.json").read_bytes())["historical_result"] + need(set(historical["projection_omits"]) + == {"source_pins_sha256", "local_inputs", "source_bundle"}, + "only transport metadata may differ from the historical receipt") + projection = {key: value for key, value in result.items() + if key not in historical["projection_omits"]} + need(digest(json.dumps(projection, sort_keys=True, separators=(",", ":")).encode()) + == historical["mathematical_projection_sha256"], + "complete historical mathematical receipt equality") + if args.check: + need(result == json.loads(args.check.read_bytes()), "complete deterministic B2 receipt") + encoded = json.dumps(result, sort_keys=True, indent=2)+"\n" + if args.output: + args.output.write_text(encoded) + elif not args.check: + print(encoded, end="") + print(result["status"]+" controls="+str(len(result["controls_rejected"]))+ + " production_factory_executed=false all_size_complex_admission=false") + + +if __name__ == "__main__": + main() diff --git a/research/ordinary-b2-bootstrap/evidence/B2-BOOTSTRAP.json b/research/ordinary-b2-bootstrap/evidence/B2-BOOTSTRAP.json new file mode 100644 index 0000000000..3f3c170ac6 --- /dev/null +++ b/research/ordinary-b2-bootstrap/evidence/B2-BOOTSTRAP.json @@ -0,0 +1,105 @@ +{ + "B2_minus_complex": "342853411912956978405651/166464500000000000000000000000", + "B2_saving": "57697923247/33292900000000", + "B2_wrapper_coefficient": 4283584, + "C1_linear_coefficient": 200, + "C1_power_coefficient": 1000000, + "a1": "169711/100000000", + "all_size_complex_admission": false, + "backend_common_member_sha256": { + "PROOF.md": "8a1c2145cd8f080026488a571d95813c09679aa323f19aeaef0ea98030136e1c", + "README.md": "dec1ca108a1dbd2d81df6f18d4e75040ce7538c804ed697478ae360af8f6b86a", + "RESULT.json": "4a99a483aa2ea5323fd8ab172f551232d5e397d797843dc3a3986e260b4c1c3d", + "SOURCES.json": "7a7407f9963b500d2782a9d41867129de3a25601206db8a0245c7677bae45762", + "TASK.json": "28a9024e78ceedd25673115604dce0231906b537feb40af79f97d11654bb73ea", + "VALIDATION.md": "61f060315562a5544ec51014b03e96e4befb4b6c9ca979c82832925a64dc9440", + "VERIFY.json": "1e3bfe986588dafde5b3d7e78fef89752049137554321b93d0d1682b3a721408", + "binary.py": "578fb5bc793fc544dca8111605bf9f6067b8ba7dc7489a3ac243e1df3cd37953", + "check_binary.py": "5eae93f8a6383dc847e906b36ce9de0bc1b5a5ecb19f66d02460eece6d8f6bf1", + "check_controls.py": "fa78e942e0386a098899dc9f454b2f36c7858ba721c483336cb95ea04627381f", + "check_engine.py": "b1610802acb43623973df11af78738a6fab234aa30e04c8f72c75bfbbaeb2296", + "check_join.py": "a93b3e3cf558b64fa53158b5e3cd5cd7928e002ec581c1b5882a899107dab9dc", + "check_root.py": "fb15328ed0c88d53202eb50968fa3714fe1c5ca6be9d589d9e720be99be85c97", + "check_setup.py": "e4a254bfcf42aeb447c8492aba0a33706a170b3b76a3ab10ca4f6905a54f6fa9", + "encoded.py": "10ad2fa5902a48d49cf2b89a30b3f2711d63a6a43b9512a6427affcdf07335a7", + "inputs/pr2808.tar": "2ab59c6d0ad00c001ecbe44090b66871ec3d2c1fdc51daa503109e56f3285cab", + "inputs/pr2809.tar": "ee1d4ec05e3c872d264be3b38f71a8c153acf37427f5d3ba87f8e15440c9ccf0", + "ordinary.py": "7f8338e748bcd42fbef1e7cc47b6c5040dfb3aad216e34759bcb12b8e14f7705", + "physical_words.py": "89ba40442297ec35368e426770f44852b39807ca426710ded2735678651bef61", + "provenance.py": "353745d666b144c7c2e10a587d6b2b1a853607bdde1121cef1b6afe8a958ca61", + "session.py": "45ee809b27a69ca5576361922fd2760f568c9a98864d4c55c4fee3003ee3c9ad", + "source.py": "4bd047a1272374880962d3074f1e50de717518a3a181f11607e820afe50dd4e5", + "verify.py": "7b976ba0aa8f09719a357fee0658c6faabd66ad03e37f39f6f16d1f20ea80714" + }, + "complex_coupling_counterexample": { + "a_next": "432730406811163660638205323612681259789065461849265284832147745034260944727697802281302239639/250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "ceiling_minus_target": "-4107764917760802665186324818749919768565068234093563524220425174671270426209123018453116344060508321882590233872482812351695309998181/70306774398318687159078664923681040886429462152004103890923534016536591029252422273437903473081726711006287320998181000000000000000000000000", + "legacy_outer_ceiling": "121485234927333986703594616906642567742303073339180209882647587074439025148531349903886936490697458584013883094707918273288993712679001819/70306774398318687159078664923681040886429462152004103890923534016536591029252422273437903473081726711006287320998181000000000000000000000000", + "target": "1727989140903569/1000000000000000000" + }, + "complex_lower": "865490127994518479981/500000000000000000000000", + "controls_rejected": [ + "omitted_bit_fallback", + "old_10000_power_coefficient", + "profile_only_without_C1", + "ordinary_rate_substituted_for_kappa", + "coupling_1_over_576", + "stock_cutoff_2_power_19", + "missing_two_call_padding", + "changed_backend_member", + "changed_stage_source", + "missing_vendored_source", + "changed_vendored_source" + ], + "coupling": "1/577", + "fallback_decisive_endpoint": "6933708158359376939/4000000000000000000000", + "fallback_rank_one_count": "1809792/152587890625", + "full_bit_mu1": "2874298095721977/2890625000000000", + "full_bit_mu_decimal": [ + 999998938581682162866772413602, + 999998938581682162866772413603, + 1000000000000000000000000000000 + ], + "full_bit_mu_integer_power": [ + "13202027144641811457560526678499378895046406447411610705697117/13202041157530128899789145217407830011540406272000000000000000", + "66010135723209057287802633392496894475232032238496346985535687/66010205787650644498945726087039150057702031360000000000000000" + ], + "full_bit_mu_series": [ + "113896303269701850359154731245838864711643096177962777219118082258168619281049593084826185221447639696633740583611957873529622045849/113896424161452791472994100289477633655308621328689181774538035621647789495734124423619363393026709274206659034480640000000000000000", + "113896303269701850359154731245838864711643096177962777219118082258168619281049593084826185221447639696633740583612196837152670504417/113896424161452791472994100289477633655308621328689181774538035621647789495734124423619363393026709274206659034480640000000000000000" + ], + "local_inputs": { + "frozen/interval_engine.py": "c4740234bee2bab8292aeef7fb561246cff8a060ea6e96f0bc14a7b69c62042c" + }, + "physical_fit_from": 1048576, + "production_factory_executed": false, + "scope": "Exact B2 rates, complete tariffs and source compatibility under retained physical/source arguments; no production retuned-C1 execution or new complex/outer admission.", + "source_backend_equal_files": 23, + "source_bundle": { + "kind": "declared-pinned-repository-inputs", + "manifest": "SOURCE-MANIFEST.json", + "manifest_sha256": "de0120c931050ea9d82758455aec5cb3addf384ebd9eed6ee708c442168ba38f" + }, + "source_bundle_files": 54, + "source_inputs": { + "research/bootstrap-depth-audit/sources/pr387/PROOF.md": "15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8", + "research/community-round8-audit/pr185-proof-reviewed.md": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa", + "research/physical-complex-compact/PROOF.md": "ec6395822ae500242f3fe5e2cf40caf9a7f9fa259d475d2c14970d951ff4df48", + "research/retuned-ordinary-coupling/PROOF.md": "3e554832c38b4b801f55b20868679f3283bc90cd5a9d8ce1960f828ed2655f22", + "research/retuned-ordinary-coupling/inputs/pr2899-export.tar.gz": "0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c", + "research/retuned-ordinary-coupling/interface.py": "25707c61b9fc6c1f09388c7cc72d269be0f8f8cae4dbc7cd5c2d00ce7fadf839", + "research/selected-bit-fast-primitives/PROOF.md": "c6912c307304b71ab51a5b9647df19a3e2c85efaca5bb3f1b635e918a62b5978", + "research/selected-bit-fast-primitives/compile_routes.py": "1bfef464dfb3e33d9d57f53b657b2d1fe3598bc453be49000a5e782b622e8585", + "research/selected-bit-fast-primitives/inputs/pr2899.tar": "fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531", + "research/selected-bit-fast-primitives/stage.py": "44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647", + "research/selected-bit-fast-primitives/stage_sources.py": "55c6631cce4f76e14b66b6195468c36b544e2374cc6c59702135c664bff10822" + }, + "source_pins_sha256": "43b04b48c9ae0d55adf3fb105bf3ec9674fdddaac26f3817d4e62ed5d948b699", + "status": "PASS_B2_EXACT_ARITHMETIC_AND_BACKEND_SOURCE_COMPATIBILITY", + "strict_gaps": { + "atom": "2076753/33292900000000", + "borrowing": "33177502076753/33292900000000", + "remainder": "331776/332929", + "stock": "576/577" + } +} diff --git a/research/ordinary-b2-bootstrap/frozen/interval_engine.py b/research/ordinary-b2-bootstrap/frozen/interval_engine.py new file mode 100644 index 0000000000..eaa2d59865 --- /dev/null +++ b/research/ordinary-b2-bootstrap/frozen/interval_engine.py @@ -0,0 +1,377 @@ +#!/usr/bin/env python3 +"""Exact joint arithmetic, with an optional binding to completed finite release. + +Prepared for Ross Richardson with OpenAI Codex assistance. Apache-2.0. +The interval implementation is separate from the inherited moment engines. +Finite arithmetic and receipt binding do not prove the all-size interfaces. +""" +import argparse +from collections import Counter +from decimal import Decimal, localcontext +from fractions import Fraction as Q +from functools import lru_cache +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PINS = { + "frozen/pr4181/RESULT.json": "d823509ea38e545db6c287a85c00bc4257825fb2710728dfc776c8801d2becd9", + "frozen/pr4181/owner/MIXED-DISPATCH.json": "ab8c774b614730701435c0f5dc1bfba4a46d980690a1b6bc09225555ff9be6f4", + "frozen/selected/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "frozen/selected/BIT-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", +} +THREE = {1: 2487, 2: 713, 3: 224, 4: 102, 5: 20, 8: 8} +FOUR = {1: 2489, 2: 713, 3: 227, 4: 99, 5: 20, 8: 8} +PREVIOUS = {1: 8060060, 2: 2310120, 3: 751813, 4: 327210, + 5: 66425, 8: 25920, 48: 138492} +PREVIOUS_LOWER = Q("0.001730979115670792472760") +PREVIOUS_UPPER = PREVIOUS_LOWER + Q(1, 10**24) +SCALE = 1 << 384 +LOG_TERMS = 140 +EXP_TERMS = 80 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + return json.loads(path.read_bytes()) + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def hist(x): + return {int(k): int(v) for k, v in x.items() if v} + + +def decimal(x): + with localcontext() as ctx: + ctx.prec = 90 + return str(Decimal(x.numerator) / Decimal(x.denominator)) + + +def ceildiv(a, b): + return -((-a) // b) + + +def down(x): + return (x.numerator * SCALE) // x.denominator + + +def up(x): + return ceildiv(x.numerator * SCALE, x.denominator) + + +def unit_log(x): + """Enclose ln(x), 1<=x<=2, in integer units of 2^-384. + + ln(x)=2 sum z^(2j+1)/(2j+1), z=(x-1)/(x+1)<=1/3. + Every recurrence rounds out; the remaining positive tail is at most + 2*z^(2N+1)/((2N+1)*(1-z*z)). + """ + need(1 <= x <= 2, "unit logarithm domain") + z = (x - 1) / (x + 1) + p, q = z.numerator, z.denominator + lo, hi = down(z), up(z) + sl = sh = 0 + for j in range(LOG_TERMS): + sl += lo // (2*j + 1) + sh += ceildiv(hi, 2*j + 1) + lo = lo * p*p // (q*q) + hi = ceildiv(hi * p*p, q*q) + tail = ceildiv(2 * hi * q*q, (2*LOG_TERMS + 1) * (q*q-p*p)) + return 2*sl, 2*sh + tail + + +@lru_cache(None) +def log_interval(x): + need(x >= 1, "positive logarithm domain") + k = 0 + while x >= 2: + x /= 2 + k += 1 + lo, hi = unit_log(x) + l2, h2 = unit_log(Q(2)) + return lo + k*l2, hi + k*h2 + + +def exp_interval(lo, hi): + """Enclose exp(x), x in [lo,hi]/SCALE, with positive Taylor terms.""" + need(0 <= lo <= hi < SCALE//100, "exponential domain x<0.01") + tl = th = sl = sh = SCALE + for j in range(1, EXP_TERMS): + tl = tl * lo // (SCALE*j) + th = ceildiv(th * hi, SCALE*j) + sl += tl + sh += th + next_upper = ceildiv(th * hi, SCALE*EXP_TERMS) + # Subsequent term ratios are < 1/2, so this geometric tail is valid. + return Q(sl, SCALE), Q(sh + 2*next_upper, SCALE) + + +def moment(profile, m, live, a, fallback=Q(0)): + """Normalized complete moment minus one; fallback is a rank-one count.""" + need(0 <= a < Q(1, 500), "certified arithmetic exponent domain") + terms = {r: Q(n) for r, n in profile.items()} + terms[1] = terms.get(1, Q(0)) + fallback + lo = hi = Q(0) + for rank, count in sorted(terms.items()): + need(0 < rank < m and count >= 0, "positive proper child") + ll, lh = log_interval(Q(m, rank)) + el, eh = exp_interval(down(a * Q(ll, SCALE)), up(a * Q(lh, SCALE))) + weight = Q(count * rank, m*live) + lo += weight * el + hi += weight * eh + return lo-1, hi-1 + + +def bracket(profile, m, live, lower, upper, fallback=Q(0)): + need(upper-lower == Q(1, 10**24), "adjacent root bracket") + at = moment(profile, m, live, lower, fallback) + nxt = moment(profile, m, live, upper, fallback) + need(at[1] < 0 < nxt[0], "strict lower/upper moment signs") + return {"lower_interval": list(map(str, at)), "upper_interval": list(map(str, nxt))} + + +def profile_check(profile, idle): + full = Counter(idle) + full.update({r: 2160*n for r, n in THREE.items()}) + full.update({r: 1080*n for r, n in FOUR.items()}) + need(dict(full) == profile, "all local, restoration and idle children included") + need(sum(r*n for r, n in profile.items()) == 65088*360, "complete rank mass") + need(73*(896*360)-sum(r*n for r, n in profile.items()) == 320*360, "rank deficit") + need(max(profile) == 48 and 73**2 > 2*48**2, "proper contraction and halving guard") + + +def legacy(complex_rate, bit_rate): + """Selected PR1094 convention, independently written in exact rationals.""" + eta = beta = Q(1, 10**24) + s = min(bit_rate, (1-beta)*complex_rate) - Q(1, 10**27) + a = Q(384599, 10**10) + chain = [a] + for _ in range(7): + nxt = s*(1-s) + s*a + need(0 < a < nxt < s < 1-nxt, "strict finite bootstrap") + a = nxt + chain.append(a) + q = (1-2*eta)*a + ceiling = (1-eta)*q/(1+q) + scale = 10**18 + ticks = ceiling*scale + kappa = Q(ceildiv(ticks.numerator, ticks.denominator)-1, scale) + need(kappa < ceiling <= kappa+Q(1, scale), "strict legacy grid") + return {"kappa": kappa, "ceiling": ceiling, "s": s, + "chain": chain, "binding": "bit" if bit_rate <= (1-beta)*complex_rate else "complex"} + + +def modern(complex_rate, bit_rate): + """Exact endpoint-DIG24 parameter algebra; analytic hypotheses are external.""" + r = Q(1, 10**104) + delta = Q(1025, 1024)*r + eps, beta = 1-delta, 1-3*delta + b, q = complex_rate-r, complex_rate-2*r + a = (q+b)/2 + saving = eps*q + need(0 < q < a < b < complex_rate < bit_rate, "joint modern rates") + need(0 < complex_rate-saving < Q(1, 10**70), "modern floor gap") + need((complex_rate*10**70).denominator == 1, "modern endpoint on floor grid") + kappa = Q((saving*10**70).__floor__(), 10**70)-Q(1, 10**46) + need(kappa == complex_rate-Q(1, 10**70)-Q(1, 10**46), "derived modern kappa") + need(1-eps-r > 0 and 1-beta-2*(1-eps) > 0, "gamma and membership costs") + need(1-eps+q*beta-saving == delta*(1-2*q) > 0, "Gaussian cost exceeds main saving") + # An explicit finite ordinary-bootstrap witness can reach the effective a. + # It requires the inherited arbitrary-strict-rate bootstrap lemma, with + # carried constants; the historical twelve-stage receipt alone is not it. + s = complex_rate-r/2 + a0 = Q(384599, 10**10) + aj = s-(s-a0)*s**38 + need(a < aj < s < bit_rate, "38-stage ordinary-rate existence witness") + return {"kappa": kappa, "b": b, "q": q, "a": a, "epsilon": eps, + "beta": beta, "r0": r, "ordinary_bootstrap_steps_sufficient": 38, + "ordinary_bootstrap_s": s, "ordinary_bootstrap_final_above_effective": aj-a} + + +def reject(name, fn): + try: + fn() + except ValueError: + return name + raise ValueError("accepted mutation: " + name) + + +def release_binding(work, profile, idle, complex_rate, bit_rate, modern_kappa, legacy_kappa): + """Cross-bind actual emitted ledgers, without claiming to re-execute them.""" + work = work.resolve() + admission = work / "admission" + paths = { + "result": admission / "RESULT.json", + "release": admission / "release/RELEASE-RECEIPT.json", + "strict_result": admission / "release/verify/RESULT.json", + "assembly": admission / "release/verify/strict/ASSEMBLY.json", + "invoice": admission / "release/verify/strict/global/audit/PREFIX-AND-INVOICE.json", + "outer": admission / "release/outer-tmp/outer/LEDGER.json", + "spec": admission / "package/new/SPEC.json", + "contract": work / "source/new/MIXED-CONTRACT.json", + } + x = {k: read(p) for k, p in paths.items()} + need(x["result"]["status"] == "PASS_REPLICA_ORDER_FILL_DERIVATIVE_COMPLETE_RELEASE", "completed inherited release") + need(x["release"]["status"] == "PASS_RELEASE", "completed release verifier") + need(hist(x["result"]["profile"]) == profile and Q(x["result"]["kappa"]) == modern_kappa, "actual new result") + need(Q(x["release"]["kappa_decimal"]) == modern_kappa, "actual modern release endpoint") + selected = read(HERE / "frozen/pr4181/owner/MIXED-DISPATCH.json") + need(sorted(x["contract"]["dispatch"]) == sorted(selected), "actual pooled selector") + a = x["assembly"] + need(hist(a["complex_profile"]) == profile and Q(a["complex_lower"]) == complex_rate, "actual complete complex profile") + need(Q(a["bit_lower"]) == bit_rate and a["surcharge_model"] == {"complex": False, "bit": True}, "actual surcharge models") + need(Q(a["kappa"]) == legacy_kappa, "actual legacy grid comparison") + need(len(a["outer"]) == 47 and all(Q(v) > 0 for v in a["outer"].values()), "all 47 inherited outer rows") + outer = x["outer"]["rows"]["struct_boundary_radix_union"] + need(Q(outer["kappa"]["rational"]) == modern_kappa, "actual modern outer ledger") + need(len(outer["strict_checks"]) == 63 and all(Q(v["rational"]) > 0 for v in outer["strict_checks"].values()), "all 63 modern outer rows") + s = x["strict_result"] + need(s["status"] == "PASS_T74_EXACT_FILL_COMPLETE_FINITE_ADMISSION", "ordinary strict admission") + expected = x["spec"]["expected"] + need(s["controls"] == {"admission": expected["assembly_controls_rejected"], "bit": 12, + "controller": expected["mutations_rejected"], "independent_owner": 8, + "geometry": 6}, "actual generated mutation coverage") + need(s["controls"]["admission"] > 119 and s["controls"]["controller"] > 25, + "active third provider retains expanded control families") + i = x["invoice"] + need(i["physical"] == 323069 == 896*360+408+8+91+2 and i["live"] == 896*360, "all physical families") + need(i["helpers"] == 408 and i["centres"] == 8 and i["private_zero_buffers"] == 91, "private and helper inventory") + calls = i["selected_calls"] + need(len(calls) == 3240 and len({(c["stage"], c["replica"]) for c in calls}) == 3240, "all literal calls") + dispatch = {(s, r): p for s, r, p in selected} + counts = Counter() + local = Counter() + for c in calls: + pid, orientation = c["provider_id"], c["orientation"] + need(dispatch[c["stage"], c["replica"]] == pid, "invoice follows pooled dispatch") + p = i["providers"][pid] + need(c["program_sha256"] == p["program_hashes"][orientation], "actual program binding") + need(hist(p["paid_profile"]) == (FOUR if pid.endswith("-four") else THREE), "complete local rank bill") + local.update(hist(p["paid_profile"])) + counts[pid] += 1 + z = p["local"][orientation] + need(z["all_exact_columns"] == 632 and z["dirty_helper_columns"] == 408 and z["all_dirty_helper_columns_restored"] and z["private_centres_and_coefficient_work_cleared"], "dirty and private restoration") + for key in ("real_component_primitives", "coefficient_work_primitive_count", "macros", "pre_wrappers", "post_wrappers"): + need(c[key] == z[key], "actual local cost: " + key) + need(dict(counts) == i["provider_counts"] == {"gauge44": 1568, "extra": 592, "extra-four": 1080}, "actual three active provider counts") + need(dict(local) == hist(i["selected_local_paid_profile"]), "local invoice sum") + local.update(idle) + need(dict(local) == profile, "actual local plus idle invoice") + for field, key in (("selected_real_component_primitives", "real_component_primitives"), ("selected_coefficient_work_primitive_count", "coefficient_work_primitive_count"), ("selected_scalar_macros", "macros")): + need(i[field] == sum(c[key] for c in calls), "full invoice sum: " + field) + need(i["wrapper_elementary_factors_charged"] == 144*sum(c["pre_wrappers"]+c["post_wrappers"] for c in calls), "paid wrapper factors") + b = i["blocknorm"] + need(b["local_actual_prefix_bits"] == 95 and b["stock_l2_bits"] == 1323 and b["max_active_depth"] == 18, "actual prefix components") + need(i["global_prefix_bits"] == 95+37+18+1323+1+4 == 1478 and i["charged_prefix_bits"] == 2048, "complete prefix reserve") + f = i["finite"] + need(f["physical_stock_bits"] == 2646 and f["physical_row_coefficient"] == 19549 < f["retained_row_coefficient"] == 20161, "complete stock and row reserve") + need(f["required_C0_bits"] < f["C0_exponent"] == 210000 and all(i["strict_checks"].values()), "precision, tape, router and finite guards") + return {"status": "COMPLETED_FINITE_RELEASE_RECEIPTS_BOUND", + "files": {k: {"path": str(p.relative_to(work)), "sha256": sha(p)} for k, p in paths.items()}, + "provider_counts": dict(counts), "physical": i["physical"], "global_prefix_bits": i["global_prefix_bits"], + "charged_prefix_bits": i["charged_prefix_bits"], "finite": f, + "selected_real_component_primitives": i["selected_real_component_primitives"], + "selected_coefficient_work_primitive_count": i["selected_coefficient_work_primitive_count"], + "selected_scalar_macros": i["selected_scalar_macros"], + "conservative_pervertex_used": i["conservative_pervertex_used"], + "scope": "Cross-binding of the parent driver's actual complete finite release; this check neither reruns the engine nor proves its all-size premises."} + + +def certificate(release_work=None): + for name, digest in PINS.items(): + need(sha(HERE/name) == digest, "frozen source pin: " + name) + source = read(HERE / "frozen/pr4181/RESULT.json") + selected = read(HERE / "frozen/selected/ASSEMBLY.json") + bit = read(HERE / "frozen/selected/BIT-EXPECTED.json")["nine"] + profile, idle = hist(source["profile"]), hist(source["idle"]) + provider_counts = Counter(p for _, _, p in read(HERE / "frozen/pr4181/owner/MIXED-DISPATCH.json")) + need(dict(provider_counts) == {"gauge44": 1568, "extra": 592, "extra-four": 1080}, + "actual pooled dispatch has three active providers") + profile_check(profile, idle) + c, upper = Q(source["root_lower"]), Q(source["root_upper"]) + b = Q(bit["bit_lower"]) + need(b == Q(selected["bit_lower"]) and selected["surcharge_model"] == {"complex": False, "bit": True}, "selected BIT and native-complex models") + candidate_signs = bracket(profile, 73, 896*360, c, upper) + previous_signs = bracket(PREVIOUS, 73, 896*360, PREVIOUS_LOWER, PREVIOUS_UPPER) + bh = hist(bit["profile"]) + fallback = Q(32*64**2*sum(bh.values()), 10**16) + bit_signs = bracket(bh, 64, bit["bit"]["live"], b, b+Q(1, 10**24), fallback) + need(b > upper, "retained BIT strictly above candidate complex root") + old_legacy = legacy(Q(selected["complex_lower"]), b) + need(old_legacy["kappa"] == Q(selected["kappa"]), "reproduce selected normalization") + new_legacy, pred_legacy = legacy(c, b), legacy(PREVIOUS_LOWER, b) + new_modern = modern(c, b) + need(new_modern["kappa"] == Q(source["conditional_kappa"]), "pooled modern claim") + gain = {r: PREVIOUS.get(r, 0)-profile.get(r, 0) for r in set(PREVIOUS)|set(profile)} + gain = {r: n for r, n in gain.items() if n} + need(gain == {1: 20, 3: 25, 4: -30, 5: 5}, "complete signed profile difference") + need(3**15*5**5 < 4**24, "uniform power-gain derivative witness") + controls = [ + reject("missing_idle_children", lambda: profile_check(profile, {})), + reject("root_used_as_legacy_kappa", lambda: need(c < new_legacy["ceiling"], "legacy outer loss omitted")), + reject("unpadded_root_used_as_modern_kappa", lambda: need(c == new_modern["kappa"], "strict modern padding omitted")), + reject("bit_improvement_only_claims_joint_gain", lambda: need(legacy(Q(selected["complex_lower"]), Q("0.001737631818486007553483"))["kappa"] > Q(selected["kappa"]), "unchanged complex side still binds")), + reject("bit_fallback_omitted", lambda: bracket(bh, 64, bit["bit"]["live"], b, b+Q(1, 10**24))), + reject("old_profile_claims_new_root", lambda: bracket(PREVIOUS, 73, 896*360, c, upper)), + ] + out = {"status": "PASS_JOINT_CONDITIONAL_ARITHMETIC_NOT_SUPPLIER_ADMISSION", "source_sha256": PINS, + "profile": profile, "idle": idle, "rank_mass": sum(r*n for r, n in profile.items()), + "active_provider_counts": dict(provider_counts), + "rank_deficit": 320*360, "child_count": sum(profile.values()), + "complex_root_bracket": [str(c), str(upper)], "complex_signs": candidate_signs, + "previous_complex_signs": previous_signs, "bit_endpoint": str(b), "bit_signs": bit_signs, + "bit_fallback_rank_one_count": str(fallback), "bit_slack_above_candidate_upper": str(b-upper), + "legacy": {**new_legacy, "kappa_decimal": decimal(new_legacy["kappa"]), + "gain_over_selected": new_legacy["kappa"]-Q(selected["kappa"]), + "gain_over_previous": new_legacy["kappa"]-pred_legacy["kappa"]}, + "modern": {**new_modern, "kappa_decimal": decimal(new_modern["kappa"]), + "gain_over_previous_upper": new_modern["kappa"]-PREVIOUS_UPPER}, + "uniform_profile_gain": {"previous_minus_new": gain, "covered_domain": "0 < a < 1", + "exact_integer_witness": [3**15*5**5, 4**24], + "argument": "F(p)=4*4^(-p)+5*(3/4)^p+(5/4)^p-6 is strictly convex; F(1)=0 and F'(1)<0. Therefore F(p)>0 for p=1-a<1. See RECURSION.md."}, + "controls": controls, + "release_binding": {"status": "NOT_REQUESTED_ARITHMETIC_ONLY"}, + "all_size_admission": False, "selected_frontier_changed": False, + "scope": "Exact complete-profile and joint-transfer arithmetic. A finite conditional improvement requires the new literal owner/operator and full ordinary/outer release. Uniform source/native generation, whole-call hosting, rounded cleanup, precision, fixed tapes, and the stated analytic transfer remain hypotheses."} + if release_work is not None: + out["release_binding"] = release_binding(release_work, profile, idle, c, b, new_modern["kappa"], new_legacy["kappa"]) + out["status"] = "PASS_JOINT_CONDITIONAL_ARITHMETIC_WITH_FINITE_RELEASE_BINDING" + return out + + +def encode(x): + if isinstance(x, Q): + return str(x) + if isinstance(x, dict): + return {str(k): encode(v) for k, v in x.items()} + if isinstance(x, (list, tuple)): + return [encode(v) for v in x] + return x + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--release-work", type=Path) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + result = encode(certificate(args.release_work)) + if args.output: + with args.output.open("x") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + print(json.dumps(result, sort_keys=True)) + print(result["status"], "legacy_kappa=" + result["legacy"]["kappa_decimal"], + "controls=" + str(len(result["controls"])), "all_size_admission=false") + + +if __name__ == "__main__": + main()