diff --git a/research/selected-bootstrap-stock-audit/README.md b/research/selected-bootstrap-stock-audit/README.md new file mode 100644 index 0000000000..bba25c7fec --- /dev/null +++ b/research/selected-bootstrap-stock-audit/README.md @@ -0,0 +1,170 @@ +# Selected bootstrap stock: independent audit and a factor-16 fit extension + +This package independently corroborates the fourteen selected bootstrap cutoffs +and stock headrooms from [Josie Elliston's PR1965](https://github.com/CrocSwap/integer-mult-bounds/pull/1965), +then proves a small extension of its **conditional stock-fit bound**. Under the +same stock-envelope hypothesis, every recorded cutoff supports a coefficient +16 times the coefficient admitted by that proof's sufficient guard. The actual +selected coefficients remain unknown. There is no new κ, supplier adoption, +frontier change, or proof of the full multiplication theorem. + +The subject is the seven native and seven conservative stages in +`research/community-frontier1094-audit/ASSEMBLY.json`, bound by +`certificates/selected-result.json` on main commit +`4d3248d6d52f8ddfe612e8508b74a36acb67fbe3`. PR1965 is pinned at +`c9819a94f9c630f8b42ff5c3027965c4ba451653`; its README and result are retained +byte for byte under `sources/pr1965/`. Its checker is neither imported nor run. + +## Exact arithmetic scope + +For each branch, reconstruct the selected producer's seven-step chain: + +``` +beta = 1/10^24 +s = min(bit_lower, (1-beta)*complex_lower) - 1/10^27 +a_0 = 384599/10^10 +a_j = (1-s)*s + s*a_(j-1) +delta_j = min(s-a_j, 1-a_j-s, 1-a_j-s*(1-a_(j-1)), 1-s) +L_j = max(ceil(36/delta_j^2), ceil(1032/delta_j)) +H_j = floor(L_j*delta_j/2) - 4 +``` + +Use `conservative_complex_lower` for the conservative branch. The formula is +read from frozen PR1087's `code/assemble.py`, lines 205–211, inside the pinned +`upstream1087.tar.gz`; source is inspected, not executed. Integer rational +pairs, Euclidean reduction and cross multiplication reconstruct every stage. +The tests use a separately implemented `Fraction` oracle. Neither arithmetic +path calls the retained assembler or PR1965's functions. The inequalities +`2(H_j+4) <= L_j*delta_j < 2(H_j+5)` certify that H is the **largest integer +log bound admitted by this guard**. They do not characterize all possible fit +proofs. + +Both branches have `H_1 = 6,562,783`. Their original guard coefficient cap is +`2^6,562,780`; the extension below admits `2^6,562,784`. At stage seven, H is +`296674203132883528250615` (native) and `296674207198239164557594` +(conservative). `RESULT.json` retains all fourteen exact values and symbolic +coefficient exponents; it never materializes these enormous powers of two. + +## Conditional factor-16 fit lemma + +Let `0=3`, `L*delta^2>=36`, and +`H=floor(L*delta/2)-4`. For every width `e>=2^L`, set +`t=log2(e)`, `w=ceil(e^s)` and `k=ceil(log_q S(e,w))`, where `q>1`. +Assume, uniformly at those widths, + +``` +log_q S(e,w) <= sigma*w*(1+log2 e), 0 < sigma <= 2^(H+1). +``` + +Then `k=L`, we have +`H+4<=delta*t/2` and `3*sqrt(t)<=delta*t/2`. The elementary inequality +`log2(1+t)<=3*sqrt(t)` for `t>=1` therefore gives + +``` +8*sigma_0*(1+t)*2^(-delta*t) <= 1/16. +``` + +For completeness, `ln(2)>=1/2` follows by integrating `1/x` on `[1,2]`. +Also `sqrt(t)-ln(1+t)` is positive at one and nondecreasing for `t>=1`, +because `1+t>=2*sqrt(t)`. Thus the stronger inequality +`log2(1+t)<=2*sqrt(t)` suffices for the displayed elementary bound. +Since `w<=2*e^s`, `s+delta<=1`, and `sigma<=16*sigma_0`, + +``` +k <= sigma*w*(1+t)+1 + <= 16*e^(s+delta)/64+1 + <= e/4+1 < e/2 (e>=8). +``` + +All fourteen selected cutoffs meet the lemma's arithmetic premises. This proof +changes only a sufficient fit coefficient and leaves the recorded L values +fixed. It does not measure or derive sigma. + +At `sigma=2^(H+1)`, `log2(8*sigma)=H+4` exceeds the original guard's maximum +H. Nevertheless the displayed proof still establishes fit under the envelope +hypothesis. Consequently PR1965's phrase "valid exactly when" should be read +as passing that particular sufficient guard, rather than as a necessary +condition for `k **Absorption bound.** For `δ > 0` and all `t ≥ 0`, +> `(1+t)·2^(−δt) ≤ M(δ) := max(2, 2/(ℯ·ln2·δ))`, where ℯ = exp(1) (e is reserved for the width). +> +> *Proof.* If t ≤ 1, the left side is at most 2. If t ≥ 1, then `1+t ≤ 2t`, and `exp(y) ≥ ℯ·y` gives +> `2^(δt) ≥ ℯ·ln2·δt`. Hence the left side is at most `2/(ℯ·ln2·δ)`. + +## Restated lemma + +*Retained hypotheses, which are not re-proved here.* (H1) `A_(j−1)` is a completed ordinary algorithm at every +width `e ≥ 1`, with `T_(j−1)(e) ≤ C_(j−1)·V·e^(1−a)`. (H2) Whenever `k(e) < e/2`, the stopped construction is a +completed ordinary algorithm at width e with + + T(e)/V ≤ K·[e^(1−s) + e^(1−a') + e^s(1+log2 e) + w^(1−a)]. + +Here K is finite and does not depend on e or on the cutoff. K is built from fresh coefficients (multiplicities, +the weighted-induction factor `1+1/(1−μ_1)+1/(1−μ_τ)`, scalar/wrapper/padding counts, the stock coefficient +inside the high-part exchange) and from `C_(j−1)`, which enters through the ordinary leaves, the remainder, the +routing and the high-part exchange. This is the retained stopped-leaf estimate of PR387 with its O-constant +written as K. The sources state it asymptotically ("for large e", `k = o(e)`). Its quantifier "whenever +`k < e/2`" and the independence of K from the cutoff are a reading of those sources, not a quotation. +(H3) `log_q S(e,w) ≤ σ·w·(1+log2 e)`, where σ is a *stock* coefficient. It is built from the +per-level row stock, the depth factor and the old algorithm's logarithmic row-reserve coefficient. It contains +no time constant. + +**Lemma (repair (b)).** Let `ℓ ≥ log2(8σ)` and `L ≥ max(2, 36/δ², 2(4+ℓ)/δ)`, and set `e0 = 2^L`. Let `A_j` +run the stopped construction for `e ≥ e0` and `A_(j−1)` below e0. Then: + +1. `A_j` is defined (the stock fits) for every `e ≥ e0`. +2. `T_j(e) ≤ C_j·V·e^(1−a')` for all `e ≥ 1`, where + `C_j = max(K·(4+M(δ)), C_(j−1)·2^(L·(a'−a)))`. +3. L depends only on δ and σ. The time constants `C_(j−1)`, K and `C_j` never enter it. + +*Proof.* (1) Put `t = log2 e ≥ L`. As in the original lemma, `log2(1+t) ≤ 3√t ≤ δt/2` and +`log2(8σ)+4 ≤ δt/2`, so `8σ(1+t)e^(−δ) ≤ 1/16`. Since `δ ≤ 1−s` and `w ≤ 2e^s`, +`k ≤ 2σe^s(1+t)+1 ≤ (e/4)·8σ(1+t)e^(−(1−s)) + 1 ≤ e/64 + 1 < e/2` for `e ≥ 4`. +(2) For `e ≥ e0`, apply (H2) term by term. `e^(1−s) ≤ e^(1−a')` because `s > a'`. +`e^s(1+t) = e^(1−a')·(1+t)2^(−(1−a'−s)t) ≤ M(δ)·e^(1−a')` by the absorption bound, since `1−a'−s ≥ δ` and M is +decreasing. `w^(1−a) ≤ 2e^(s(1−a)) ≤ 2e^(1−a')` because of the remainder gap. For `1 ≤ e < e0`, +`T_(j−1)(e) ≤ C_(j−1)e^(1−a)·e^(a'−a) ≤ C_(j−1)2^(L(a'−a))·e^(1−a')`. (3) follows from the definition of L. ∎ + +The original lemma's next constant `C_large + C_old·2^(L(a_(j+1)−a_j))` dominates this `C_j`, with +`C_large = K(4+M(δ))`. The induction stays sequential: `σ → L → C_j → (σ_(j+1), next stage)`. + +**Consequence for the selected receipt.** Read with C = 8σ (a space constant) instead of a constant that +dominates the previous time constant, the receipt's formula `max(⌈36/δ²⌉, ⌈2(4+512)/δ⌉)` is an instance of +the restated lemma whenever `8σ_j ≤ 2^512`, that is, whenever `σ_j ≤ 2^509`. In fact each recorded cutoff supports much more. The verifier +computes the exact largest `ℓ` each one admits (`stock_headroom_log2`). It is 6,562,783 bits at stage 1 and +grows by about 1/s per stage, to about 3·10^23 bits at stage 7. Every one of the 14 recorded cutoffs is +therefore a valid fit cutoff for any stock coefficient `σ_j ≤ 2^(H_j−3)`, where `H_j` is that stage's headroom. +At stage 1 this means `σ_1 ≤ 2^6,562,780`. The carried time constant stays +finite and does not feed back into L. Under the receipt's own assumption that fresh time constants are below +2^512, the verifier's explicit chain bounds `log2 C_7` by a 27-digit integer. That chain also assumes +`K_j ≤ 2^512 + 2^512·C_(j−1)`, which is a modeling assumption stronger than (H2)'s finite K. It only illustrates +finiteness and plays no role in the cutoffs. On the other side, the carried +factor alone gives `log2 C_(j−1) ≥ L_(j−1)·Δa_(j−1)`, which already exceeds the stage-j headroom for every +j = 2..7. This reproduces PR #1956's finding from the other side: the lemma *as written* fails exactly at +stages 2–7. + +So, under (H1)–(H3), the recorded cutoff numbers are valid exactly when every `σ_j ≤ 2^(H_j−3)`. If that holds, +only the proof text needs to change. The condition is plausible by a wide margin, but it is not verified here. + +## Remaining obligations (not discharged here) + +- **(H3) and the stock coefficient.** The stock coefficient must contain no time constant. Each `σ_j` must + satisfy `log2(8σ_j) ≤ stock_headroom_log2[j]`, which is a margin of millions of bits or more. This rests on + the retained complete-row contract: the old supplier's row reserve is logarithmic, and that bound has the same + shape at every stage, so the below-cutoff branch does not multiply it by `2^(LΔa)`. This package does not + re-derive that contract or compute the actual σ_j. +- **(H2) form.** The retained stopped-leaf estimate is taken with its O-constant K independent of the cutoff, as + PR387 and the weighted induction of FINITE_BIT_ACCOUNTING state it. If any other "sufficiently large e" + condition hides in the inherited primitives (PR185 lineage), it is a further fit condition. It needs its own + coefficient checked against the headroom, and it may not contain a time constant. +- Other lineages (T37's 1024-bit receipts, open PRs #1424, #1586 and #1724) use the same formula. The argument + applies to them verbatim, but their headrooms are not computed here. +- Every other inherited all-size, precision, hosting and analytic obligation of the selected record. + +## Reproduce + +```sh +python3 -B research/bootstrap-cutoff-time-space-split/verify.py +python3 scripts/research_package.py --package research/bootstrap-cutoff-time-space-split --check-only +python3.12 scripts/research_package.py --package research/bootstrap-cutoff-time-space-split +``` + +Expected: `PASS_BOOTSTRAP_TIME_SPACE_SPLIT recorded=14 fit_only_valid=14 written_rule_fails=12 +time_constant_finite=2 controls_rejected=7`, in well under a second, using the standard library only. + +The verifier checks every input against [SOURCES.json](SOURCES.json). It binds the lemma text, the fit statement +in `three-stage-cover-rows.tex` and the assembler formula in the pinned `upstream1087.tar.gz`. It then checks the +following in exact rational arithmetic: + +- the 14 cutoffs reproduce from the receipt's chain; +- δ never exceeds the stock gap; +- each cutoff satisfies the fit-only rule with the exact headroom (`ℓ` passes and `ℓ+1` fails); +- certified rational lower bounds `ln2 > 693/1000` and `ℯ > 2718/1000`, from series partial sums with tail + bounds; +- the `3√t` step, from `9(ln2)²/2 ≥ 1`; +- the explicit time-constant chain. + +The `ℯ` bound needs only a positive partial sum. The quartered-M control (control 3 below) uses the same +floating-point check. A floating-point check at the true maximizer `t* = 1/(δ ln2) − 1` and on a grid confirms that `M(δ)` dominates +the actual supremum. It is a sanity check, not a certificate. The verifier compares its summary with +[RESULT.json](RESULT.json). + +Seven controls must be rejected: + +1. a recorded cutoff minus one; +2. a stock coefficient one bit above the headroom; +3. `M(δ)/4` in place of `M(δ)`; +4. the false lower bound `ln2 > 0.6932`; +5. the false lower bound `ℯ > 2.719`; +6. the carried time constant put into the fit rule (the lemma as written, at stage 2); +7. a tampered gap. + +## Open next questions + +1. **Compute σ_j for the selected lineage.** Is `log2(8σ_j)` below the recorded headroom at every stage? We + expect it to be far below. *First step:* collect the per-level row stock (`14400w+1`, depth factor, the + `57,604` new contribution in FINITE_BIT_ACCOUNTING) and the old-leaf reserve coefficient from the PR185/#384 + complete-row contract. *Blocked by:* the reserve coefficient is stated only as "logarithmic" in the retained + sources. +2. **Adopt the wording.** If maintainers accept the restated lemma, the proof texts (PR387 PROOF, + FINITE_BIT_ACCOUNTING and their successors) could say "C dominates the stage's stock/fit constants" + instead of "previous ordinary constants". PR #1956's corrected chain would then be needed only by readers who + keep the original wording. *Blocked by:* maintainer decision. Frozen packages are not edited here. + +## Credit + +The cutoff lemma, its 1/16 inequality chain and the next-constant rule are from rohanarun's PR387 PROOF and +eumemic's five-stage bank proof. The borrowing/fit construction is from the retained +`three-stage-cover-rows.tex`. The chain and the 512 allowance are from the frozen PR1087 assembler (Jeremy +Kothe's package and its credited lineage) and Rohan Arun's PR1094 selected receipt. The receipt binding and the +question come from PR #1956 (`bootstrap-cutoff-carry`, same author). Prepared by Josie Elliston with Claude Code +(Claude Opus 5.5) assistance. Apache-2.0. diff --git a/research/selected-bootstrap-stock-audit/sources/pr1965/RESULT.json b/research/selected-bootstrap-stock-audit/sources/pr1965/RESULT.json new file mode 100644 index 0000000000..b4cf2572cc --- /dev/null +++ b/research/selected-bootstrap-stock-audit/sources/pr1965/RESULT.json @@ -0,0 +1,109 @@ +{ + "bootstrap": { + "cutoff_digits": [ + 13, + 19, + 24, + 30, + 35, + 41, + 46 + ], + "stock_headroom_log2": [ + 6562783, + 3917000013, + 2337861697120, + 1395352895343721, + 832816459989422004, + 497066554520932088547, + 296674203132883528250615 + ], + "m_bar_log2_ceil": [ + 19, + 28, + 38, + 47, + 56, + 65, + 74 + ], + "time_log2C_digits": [ + 3, + 10, + 13, + 16, + 19, + 21, + 24, + 27 + ], + "time_log2C_final_sha256": "4ab13a5ce9894525117996ad288c630b28f2938c234e0755046aa4a692cd18cf", + "written_rule_holds": [ + true, + false, + false, + false, + false, + false, + false + ] + }, + "conservative_bootstrap": { + "cutoff_digits": [ + 13, + 19, + 24, + 30, + 35, + 41, + 46 + ], + "stock_headroom_log2": [ + 6562783, + 3917000033, + 2337861713185, + 1395352907315128, + 832816468556900243, + 497066560483357858654, + 296674207198239164557594 + ], + "m_bar_log2_ceil": [ + 19, + 28, + 38, + 47, + 56, + 65, + 74 + ], + "time_log2C_digits": [ + 3, + 10, + 13, + 16, + 19, + 21, + 24, + 27 + ], + "time_log2C_final_sha256": "4714d46e06668e81d1a0028a780e99e9c3901872170d5b77e50cd0243645518c", + "written_rule_holds": [ + true, + false, + false, + false, + false, + false, + false + ] + }, + "controls_rejected": [ + "recorded_cutoff_minus_one", + "stock_coefficient_above_headroom", + "absorption_constant_quartered", + "ln2_lower_bound_too_high", + "e_lower_bound_too_high", + "carried_time_constant_in_fit", + "tampered_gap" + ] +} diff --git a/research/selected-bootstrap-stock-audit/test_verify.py b/research/selected-bootstrap-stock-audit/test_verify.py new file mode 100644 index 0000000000..e9af04c084 --- /dev/null +++ b/research/selected-bootstrap-stock-audit/test_verify.py @@ -0,0 +1,173 @@ +#!/usr/bin/env python3 +"""Separate Fraction oracle and bounded file/claim controls for the stock audit.""" +import copy +from fractions import Fraction as F +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location('stock_audit', HERE/'verify.py') +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +def oracle_branch(record, branch, endpoint): + """Use independent Fraction arithmetic and the closed saving formula.""" + saving = min(F(record['bit_lower']), (1-F(1, 10**24))*F(record[endpoint]))-F(1, 10**27) + start = F(384599, 10**10) + rows = [] + for index, item in enumerate(record[branch], 1): + old = saving-saving**(index-1)*(saving-start) + new = saving-saving**index*(saving-start) + gaps = {'atom': saving-new, 'borrowing': 1-new-saving, + 'remainder': 1-new-saving*(1-old), 'stock': 1-saving} + delta = min(gaps.values()) + qterm, linear = F(36)/delta**2, F(1032)/delta + ceil = lambda a: -(-a.numerator//a.denominator) + L = max(ceil(qterm), ceil(linear)) + value = F(L)*delta/2 + H = value.numerator//value.denominator-4 + rows.append({'old': str(old), 'exponent': str(new), 'gaps': {k: str(v) for k, v in gaps.items()}, 'gap': str(delta), 'cutoff_log2': str(L), 'stock_headroom_log2': H}) + return saving, rows + + +class StockAuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.record = json.loads((ROOT/audit.ASSEMBLY).read_bytes()) + + def test_independent_closed_form_oracle_all_fourteen(self): + actual = audit.analyze(self.record) + for branch, endpoint in audit.BRANCHES: + saving, rows = oracle_branch(self.record, branch, endpoint) + self.assertEqual(str(saving), actual[branch]['common_saving']) + self.assertEqual(7, len(rows)) + for expected, observed in zip(rows, actual[branch]['stages']): + self.assertEqual(expected, {k: observed[k] for k in expected}) + self.assertEqual(observed['original_guard_cap_exp']+4, observed['relaxed_fit_cap_exp']) + + def test_adjacent_integer_headroom_and_active_cutoff(self): + self.assertFalse(audit.fit_guard(40, '-1', -100)) + self.assertFalse(audit.fit_guard(40, '0', -100)) + for branch, endpoint in audit.BRANCHES: + _, rows = oracle_branch(self.record, branch, endpoint) + for row in rows: + delta, L, H = F(row['gap']), int(row['cutoff_log2']), row['stock_headroom_log2'] + self.assertGreaterEqual(L*delta/2, H+4) + self.assertLess(L*delta/2, H+5) + self.assertTrue(audit.fit_guard(L, row['gap'], H)) + self.assertFalse(audit.fit_guard(L, row['gap'], H+1)) + self.assertFalse(audit.fit_guard(L, row['gap'], H+4)) + self.assertTrue((L-1)*delta**2 < 36 or (L-1)*delta < 1032) + + def test_factor_sixteen_strict_fit_and_domain(self): + # The source proof gives k <= factor*e/64 + 1. No huge 2^L is formed. + for e in (8, 9, 16, 128, 1024): + self.assertLess(F(16*e, 64)+1, F(e, 2)) + self.assertEqual(F(16*4, 64)+1, F(4, 2)) + self.assertGreater(F(32*8, 64)+1, F(8, 2)) + + def test_arithmetic_mutations(self): + for branch, _ in audit.BRANCHES: + for field in ('gap', 'exponent', 'cutoff_log2'): + changed = copy.deepcopy(self.record) + value = changed[branch][3][field] + changed[branch][3][field] = str(int(value)-1) if field == 'cutoff_log2' else str(F(value)+F(1, 10**100)) + with self.assertRaises(audit.AuditError): + audit.analyze(changed) + + def test_source_boundary_and_unproved_claim_mutations(self): + result = audit.compute() + boundary = result['source_boundary'] + self.assertEqual('NOT_ESTABLISHED', boundary['status']) + self.assertEqual((120, 73), (boundary['historical_candidate']['m'], boundary['selected_candidate']['m'])) + self.assertEqual(0, boundary['completed_inner_leaf_external_extra_stock']) + self.assertFalse(boundary['external_252_is_actual_internal_reserve']) + mutations = ( + lambda q: q['source_boundary'].__setitem__('selected_additive_57604_recurrence', 'ESTABLISHED'), + lambda q: q['source_boundary'].__setitem__('actual_stage_stock_coefficients', [57604]*7), + lambda q: q['source_boundary'].__setitem__('inherited_old_leaf_reserve_coefficient', 252), + lambda q: q['branches']['bootstrap']['stages'][0].__setitem__('actual_stock_coefficient', 0), + ) + for mutate in mutations: + changed = copy.deepcopy(result) + mutate(changed) + with self.assertRaises(audit.AuditError): + audit.validate_claim(changed) + + def test_exact_json_and_rational_domain(self): + self.assertNotEqual(audit.typed(True), audit.typed(1)) + for raw in ('{"x":1,"x":2}', '{"x":1.0}', '{"x":NaN}'): + with self.assertRaises(audit.AuditError): + audit.load_json(raw) + with self.assertRaises(audit.AuditError): + audit.R(True) + + def make_relocation(self, where): + target = where/'repo' + package = target/'research'/HERE.name + shutil.copytree(HERE, package) + manifest = json.loads((HERE/'SOURCES.json').read_bytes()) + for f in manifest['files']: + src, dst = ROOT/f['path'], target/f['path'] + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(src, dst) + return target, package + + def run_relocated(self, package, *args): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(package/'verify.py'), *map(str, args)], cwd=package, text=True, capture_output=True) + + def test_relocated_optimized_receipt_source_and_manifest_controls(self): + with tempfile.TemporaryDirectory(prefix='selected-stock-test-') as directory: + base = Path(directory) + target, package = self.make_relocation(base) + replay = self.run_relocated(package) + self.assertEqual(0, replay.returncode, replay.stderr) + catalogue = target/'docs/research/agent-task-catalog.json' + catalogue.write_text('changed working catalogue priority data') + self.assertEqual(0, self.run_relocated(package).returncode) + manifest_path = package/'SOURCES.json' + original_manifest = manifest_path.read_bytes() + manifest = json.loads(original_manifest) + for mutate in ( + lambda q: q.__setitem__('base_commit', '0'*40), + lambda q: q['pending_sources'][0].__setitem__('head', '0'*40), + lambda q: next(f for f in q['files'] if f['usage'] == 'input').__setitem__('git_blob', '0'*40), + lambda q: q['files'].append(copy.deepcopy(q['files'][0])), + ): + changed = copy.deepcopy(manifest) + mutate(changed) + manifest_path.write_text(json.dumps(changed)) + bad = self.run_relocated(package) + self.assertNotEqual(0, bad.returncode) + manifest_path.write_bytes(original_manifest) + source = target/audit.ROWS + old_source = source.read_bytes() + source.write_bytes(old_source+b'\nchanged source\n') + self.assertNotEqual(0, self.run_relocated(package).returncode) + source.write_bytes(old_source) + receipt = package/'RESULT.json' + old_receipt = receipt.read_bytes() + false_receipt = json.loads(old_receipt) + false_receipt['source_boundary']['actual_stage_stock_coefficients'] = [0]*7 + receipt.write_text(json.dumps(false_receipt)) + self.assertNotEqual(0, self.run_relocated(package).returncode) + receipt.write_bytes(old_receipt) + existing = base/'existing.json' + existing.write_text('retain me') + self.assertNotEqual(0, self.run_relocated(package, '--write-result', existing).returncode) + self.assertEqual('retain me', existing.read_text()) + internal = package/'must-not-be-written.json' + self.assertNotEqual(0, self.run_relocated(package, '--write-result', internal).returncode) + self.assertFalse(internal.exists()) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/selected-bootstrap-stock-audit/verify.py b/research/selected-bootstrap-stock-audit/verify.py new file mode 100644 index 0000000000..3593b2761b --- /dev/null +++ b/research/selected-bootstrap-stock-audit/verify.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Independent integer-pair audit of selected bootstrap stock thresholds. + +No predecessor checker, Fraction, numerical log/exp, or float is used. +The stock coefficient itself is unknown; thresholds are sufficient conditions. +ToikY with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import hashlib +import io +import json +import math +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE_COMMIT = '4d3248d6d52f8ddfe612e8508b74a36acb67fbe3' +PENDING_HEAD = 'c9819a94f9c630f8b42ff5c3027965c4ba451653' +SELECTED = 'certificates/selected-result.json' +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +FBA = 'research/five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md' +ROWS = 'research/five-stage-source527-banks/proof/three-stage-cover-rows.tex' +PR387 = 'research/bootstrap-depth-audit/sources/pr387/PROOF.md' +PR185 = 'research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md' +TARBALL = 'research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz' +BRANCHES = (('bootstrap', 'complex_lower'), ('conservative_bootstrap', 'conservative_complex_lower')) + + +class AuditError(ValueError): + pass + + +def require(condition, message): + if not condition: + raise AuditError(message) + + +class R: + """Reduced integer rational; comparisons use integer cross products.""" + __slots__ = ('p', 'q') + + def __init__(self, p, q=1): + require(type(p) is int and type(q) is int and q != 0, 'rational integer domain') + if q < 0: + p, q = -p, -q + g = math.gcd(p, q) + self.p, self.q = p // g, q // g + + @staticmethod + def of(x): + if isinstance(x, R): + return x + if type(x) is int: + return R(x) + require(type(x) is str, 'rational string domain') + fields = x.split('/') + require(len(fields) in (1, 2), 'rational serialization') + return R(*(int(a) for a in fields)) + + def __add__(self, x): + x = R.of(x) + return R(self.p*x.q+x.p*self.q, self.q*x.q) + + __radd__ = __add__ + + def __neg__(self): + return R(-self.p, self.q) + + def __sub__(self, x): + return self + -R.of(x) + + def __rsub__(self, x): + return R.of(x) - self + + def __mul__(self, x): + x = R.of(x) + return R(self.p*x.p, self.q*x.q) + + __rmul__ = __mul__ + + def __truediv__(self, x): + x = R.of(x) + require(x.p != 0, 'nonzero rational divisor') + return R(self.p*x.q, self.q*x.p) + + def __lt__(self, x): + x = R.of(x) + return self.p*x.q < x.p*self.q + + def __le__(self, x): + x = R.of(x) + return self.p*x.q <= x.p*self.q + + def __eq__(self, x): + if not isinstance(x, R) and type(x) not in (int, str): + return False + x = R.of(x) + return self.p == x.p and self.q == x.q + + def __str__(self): + return str(self.p) if self.q == 1 else f'{self.p}/{self.q}' + + def floor(self): + return self.p // self.q + + def ceil(self): + return -(-self.p // self.q) + + +def fit_guard(L, delta, ell): + require(type(L) is int and type(ell) is int, 'integer cutoff and headroom') + delta = R.of(delta) + return R(0) < delta and L >= 2 and R(36) <= L*delta*delta and R(2*(4+ell)) <= L*delta + + +def analyze_branch(record, name, side): + s = min(R.of(record['bit_lower']), (1-R(1, 10**24))*R.of(record[side])) - R(1, 10**27) + require(R(0) < s < R(1, 2), 'positive common saving below one half') + old = R(384599, 10**10) + require(type(record[name]) is list and len(record[name]) == 7, 'seven bootstrap stages') + result = [] + for j, item in enumerate(record[name], 1): + new = (1-s)*s+s*old + gaps = dict(atom=s-new, borrowing=1-new-s, remainder=1-new-s*(1-old), stock=1-s) + require(all(R(0) < g for g in gaps.values()), 'positive four gaps') + delta = min(gaps.values()) + require(R.of(item['exponent']) == new, 'recorded stage exponent') + require(R.of(item['gap']) == delta, 'recorded minimum gap') + require(type(item['cutoff_log2']) is str and item['cutoff_log2'].isdigit(), 'recorded integer cutoff') + L = int(item['cutoff_log2']) + expected_L = max((R(36)/(delta*delta)).ceil(), (R(1032)/delta).ceil()) + require(L == expected_L, 'recorded fixed-512 cutoff') + require(fit_guard(L, delta, 512), 'fixed-512 sufficient guard') + H = (L*delta/R(2)).floor()-4 + require(fit_guard(L, delta, H) and not fit_guard(L, delta, H+1), 'maximal integer guard headroom') + require(delta <= gaps['stock'], 'gap covers stock exponent') + require(L >= 3, 'relaxed fit domain e at least eight') + require(not fit_guard(L, delta, H+4), 'relaxed fit cap must not pass old guard') + result.append(dict(stage=j, old=str(old), exponent=str(new), gaps={k: str(v) for k, v in gaps.items()}, gap=str(delta), cutoff_log2=str(L), stock_headroom_log2=H, original_guard_cap_exp=H-3, relaxed_fit_cap_exp=H+1, relaxed_fit_factor=16, fit_requires_e_ge=8, actual_stock_coefficient=None)) + old = new + return dict(common_saving=str(s), stages=result) + + +def analyze(record): + return {name: analyze_branch(record, name, side) for name, side in BRANCHES} + + +def typed(value): + """Comparison key distinguishes booleans, integers, strings and null.""" + if type(value) is dict: + return ('dict', tuple((k, typed(v)) for k, v in sorted(value.items()))) + if type(value) is list: + return ('list', tuple(typed(v) for v in value)) + require(type(value) in (str, int, bool, type(None)), 'JSON exact types') + return type(value).__name__, value + + +def load_json(raw): + def pairs(items): + out = {} + for k, v in items: + require(k not in out, 'duplicate JSON key') + out[k] = v + return out + obj = json.loads(raw, object_pairs_hook=pairs) + typed(obj) + return obj + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def blob_sha(raw): + return hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + + +def load_sources(): + manifest = load_json((HERE/'SOURCES.json').read_bytes()) + require(type(manifest['schema_version']) is int and manifest['schema_version'] == 1 and manifest['base_commit'] == BASE_COMMIT, 'fixed source schema and base') + raw = {} + paths = set() + for f in manifest['files']: + require(f['path'] not in paths, 'unique repository source path') + paths.add(f['path']) + if f['path'] == 'docs/research/agent-task-catalog.json': + require(f['usage'] == 'provenance', 'catalogue is historical provenance only') + continue + require(f['usage'] == 'input', 'consumed source usage') + path = (ROOT/f['path']).resolve() + require(path.is_relative_to(ROOT), 'repository source path') + data = path.read_bytes() + require(sha(data) == f['sha256'] and blob_sha(data) == f['git_blob'], 'source SHA256/Git blob: '+f['path']) + raw[f['path']] = data + require({SELECTED, ASSEMBLY, FBA, ROWS, PR387, PR185, TARBALL} == set(raw), 'complete consumed source set') + require(set(raw) | {'docs/research/agent-task-catalog.json'} == paths, 'complete source inventory') + pending = manifest['pending_sources'] + require(len(pending) == 1 and type(pending[0]['pr']) is int and pending[0]['pr'] == 1965 and pending[0]['repository'] == 'CrocSwap/integer-mult-bounds' and pending[0]['head'] == PENDING_HEAD, 'fixed unique pending PR1965 identity') + vendor = {} + paths = set() + for f in pending[0]['files']: + require(f['path'] not in paths, 'unique pending source path') + paths.add(f['path']) + path = (HERE/f['path']).resolve() + require(path.is_relative_to(HERE), 'pending source path') + data = path.read_bytes() + require(sha(data) == f['sha256'] and blob_sha(data) == f['git_blob'], 'pending source SHA256/Git blob: '+f['path']) + vendor[path.name] = data + require(paths == {'sources/pr1965/README.md', 'sources/pr1965/RESULT.json'}, 'PR1965 text and receipt paths') + return raw, vendor, pending[0]['head'] + + +def source_boundary(raw): + fba, rows, pr387 = (raw[p].decode() for p in (FBA, ROWS, PR387)) + for needle in ('m=120, W=23,683', 'four levels halve', '14400w+1', '57,604w*ceil(log2(max(2,n)))', 'Add the\ninherited old-leaf reserve'): + require(needle in fba, 'historical stock source anchor: '+needle) + for needle in (r'\log_qS(e,w)=O(w\log e)', 'logarithmic reserve', 'original width $e$', 'Small widths use the retained supplier directly'): + require(needle in rows, 'row contract source anchor: '+needle) + require('previous ordinary constants' in pr387 and 'previous ordinary constants' in fba, 'inherited cutoff wording') + reviewed = raw[PR185].decode() + for needle in ('new ordinary leaves need no *external* extra stock', '252 is not asserted to be the new leaf\'s actual internal reserve', 'additional externally supplied stock is zero'): + require(needle in reviewed, 'completed leaf source anchor: '+needle) + with tarfile.open(fileobj=io.BytesIO(raw[TARBALL])) as archive: + producer = archive.extractfile('code/assemble.py').read().decode() + require(sha(producer.encode()) == '15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a', 'selected producer member SHA256') + for needle in ('chain=[Q(384599,10**10)]', 'for _ in range(7)', 'cut=max(ceil(36/gap**2),ceil(2*(4+512)/gap))', "check_moment('complex',H,73"): + require(needle in producer, 'selected producer source anchor: '+needle) + return dict(status='NOT_ESTABLISHED', historical_candidate=dict(m=120, halving_levels=4, new_stock_coefficient=57604), selected_candidate=dict(m=73), selected_additive_57604_recurrence='NOT_ESTABLISHED', actual_stage_stock_coefficients=None, inherited_old_leaf_reserve_coefficient=None, completed_inner_leaf_external_extra_stock=0, external_252_is_actual_internal_reserve=False, guard_necessity='NOT_ESTABLISHED', established_scope='Exact sufficient fit thresholds under PR1965 H3; no actual selected stock or quantitative reserve recurrence.') + + +def validate_claim(result): + boundary = result['source_boundary'] + require(boundary['status'] == 'NOT_ESTABLISHED' and boundary['selected_additive_57604_recurrence'] == 'NOT_ESTABLISHED', 'selected stock recurrence remains unproved') + require(boundary['actual_stage_stock_coefficients'] is None and boundary['inherited_old_leaf_reserve_coefficient'] is None, 'actual stock coefficients remain unknown') + require(all(s['actual_stock_coefficient'] is None for b in result['branches'].values() for s in b['stages']), 'no unproved numerical stage stock') + + +def semantic_controls(record, branches, boundary): + import copy + controls = [] + for name, field in (('wrong gap', 'gap'), ('wrong exponent', 'exponent'), ('cutoff minus one', 'cutoff_log2')): + changed = copy.deepcopy(record) + old = changed['bootstrap'][0][field] + changed['bootstrap'][0][field] = str(R.of(old)+R(1, 10**100)) if field != 'cutoff_log2' else str(int(old)-1) + try: + analyze(changed) + except AuditError as error: + controls.append(dict(name=name, rejected=True, predicate=str(error))) + else: + raise AuditError('semantic mutation was accepted: '+name) + st = branches['bootstrap']['stages'][1] + prev = branches['bootstrap']['stages'][0] + carried = R.of(prev['cutoff_log2'])*(R.of(prev['exponent'])-R.of(prev['old'])) + require(not fit_guard(int(st['cutoff_log2']), st['gap'], carried.ceil()), 'time constant exceeds fit guard headroom') + controls.append(dict(name='time-space confusion arithmetic guard', rejected=True, predicate='carried time lower bound fails fit guard; it is not an actual stock coefficient', stage=2, carried_log2_lower=str(carried))) + require(not fit_guard(int(st['cutoff_log2']), st['gap'], st['stock_headroom_log2']+4), 'false relaxed-cap guard acceptance') + controls.append(dict(name='relaxed fit cap declared old-guard accepted', rejected=True, predicate='H+4 fails maximal old guard', stage=2)) + for name, field, value in (('blanket selected 57604 recurrence', 'selected_additive_57604_recurrence', 'ESTABLISHED'), ('unproved actual stock coefficient', 'actual_stage_stock_coefficients', [57604]*7)): + changed = dict(source_boundary=copy.deepcopy(boundary), branches=branches) + changed['source_boundary'][field] = value + try: + validate_claim(changed) + except AuditError as error: + controls.append(dict(name=name, rejected=True, predicate=str(error))) + else: + raise AuditError('unproved stock claim was accepted: '+name) + return controls + + +def compute(): + raw, vendor, head = load_sources() + selected, record = load_json(raw[SELECTED]), load_json(raw[ASSEMBLY]) + require(selected['certificate'] == ASSEMBLY and selected['certificate_sha256'] == sha(raw[ASSEMBLY]), 'selected assembly binding') + require(selected['kappa'] == record['kappa'], 'unchanged selected kappa') + branches = analyze(record) + predecessor = load_json(vendor['RESULT.json']) + for name, _ in BRANCHES: + require(typed([r['stock_headroom_log2'] for r in branches[name]['stages']]) == typed(predecessor[name]['stock_headroom_log2']), 'independent PR1965 headroom corroboration') + text = vendor['README.md'].decode() + require('valid exactly when every' in text and 'σ_j ≤ 2^(H_j−3)' in text, 'pinned overstrong necessity wording') + require('not computed here' in text, 'predecessor actual-stock limitation') + boundary = source_boundary(raw) + result = dict(status='PASS_SELECTED_BOOTSTRAP_STOCK_AUDIT', selected_kappa=record['kappa'], cutoff_count=14, predecessor_pr=1965, predecessor_head=head, branches=branches, source_boundary=boundary, relaxed_fit=dict(factor=16, cap='sigma_j <= 2^(H_j+1)', fit_requires_e_ge=8, still_conditional_on_H3=True, sharp_maximum_claim=False), controls=semantic_controls(record, branches, boundary), scope='Independent exact selected threshold audit and sufficient factor16 fit extension; actual stock, H1/H2/H3 and physical compiler are not discharged.') + validate_claim(result) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path) + args = parser.parse_args() + if args.write_result is not None: + require(not args.write_result.exists(), 'fresh result output only') + require(not args.write_result.resolve().is_relative_to(ROOT), 'fresh result output must be external') + result = compute() + if args.write_result is None: + require(typed(load_json((HERE/'RESULT.json').read_bytes())) == typed(result), 'committed RESULT equality') + else: + with args.write_result.open('x') as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True)+'\n') + print(result['status'], 'cutoffs=14', 'factor16_fit=14', 'actual_stock=NOT_ESTABLISHED') + + +if __name__ == '__main__': + main()