From 0c2873e6ac844b369a5962f06ef0a74ac86cf4a4 Mon Sep 17 00:00:00 2001 From: martinxxx9 Date: Tue, 13 Oct 2026 20:58:35 +0200 Subject: [PATCH 1/2] Add files via upload --- .../CLAIM.json | 59 ++++++ .../README.md | 172 ++++++++++++++++ .../RESULT.json | 160 +++++++++++++++ .../SOURCES.json | 50 +++++ .../VALIDATION.json | 35 ++++ .../test_package.py | 51 +++++ .../verify.py | 169 ++++++++++++++++ .../CLAIM.md | 10 + .../NOTICE.md | 2 + .../PINS.json | 13 ++ .../PROOF.md | 11 + .../README.md | 29 +++ .../RESULT.json | 22 ++ .../test_package.py | 50 +++++ .../verify.py | 191 ++++++++++++++++++ 15 files changed, 1024 insertions(+) create mode 100644 research/compact-boundary-cancellation-seed51/CLAIM.json create mode 100644 research/compact-boundary-cancellation-seed51/README.md create mode 100644 research/compact-boundary-cancellation-seed51/RESULT.json create mode 100644 research/compact-boundary-cancellation-seed51/SOURCES.json create mode 100644 research/compact-boundary-cancellation-seed51/VALIDATION.json create mode 100644 research/compact-boundary-cancellation-seed51/test_package.py create mode 100644 research/compact-boundary-cancellation-seed51/verify.py create mode 100644 research/frontier1042-capsule-closure-seed75/CLAIM.md create mode 100644 research/frontier1042-capsule-closure-seed75/NOTICE.md create mode 100644 research/frontier1042-capsule-closure-seed75/PINS.json create mode 100644 research/frontier1042-capsule-closure-seed75/PROOF.md create mode 100644 research/frontier1042-capsule-closure-seed75/README.md create mode 100644 research/frontier1042-capsule-closure-seed75/RESULT.json create mode 100644 research/frontier1042-capsule-closure-seed75/test_package.py create mode 100644 research/frontier1042-capsule-closure-seed75/verify.py diff --git a/research/compact-boundary-cancellation-seed51/CLAIM.json b/research/compact-boundary-cancellation-seed51/CLAIM.json new file mode 100644 index 0000000000..09329a49da --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/CLAIM.json @@ -0,0 +1,59 @@ +{ + "seed": 51, + "randomness": "System.Security.Cryptography.RandomNumberGenerator.Fill; UInt32 modulo 100", + "track": "Recursive interfaces (50-59)", + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "object": "One-digit earlier-source compact raw forward/return cancellation across recursive boundary", + "method": "Exact parity partition, complete small rectangles, independent retained primitive comparisons", + "deliverable": "Scoped negative result, exact support/order, full inherited recurrence and rejection controls", + "finish": "This session; final quarter reserved for verification and packaging", + "candidates": [ + "T37 restoration deferral (overlap PR1012)", + "Additive echo pool reuse (overlap PR1057)", + "Raw versus repaired compact boundary cancellation (chosen)" + ], + "coordination": "No open issue in earliest 100-item API page; related PRs report no pinned sprint issue. No posting connector/gh available, so claim recorded locally.", + "open_pr_snapshot": { + "count": 763, + "first": 1096, + "last": 1 + }, + "related_prs": [ + { + "number": 1057, + "title": "Research: exact additive echoes with three dirty arrays at any depth (no new kappa)", + "head": "78a062df1dcab2bffea5ff4d8243f3da6e465414" + }, + { + "number": 1012, + "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", + "head": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03" + }, + { + "number": 773, + "title": "Research audit: exact packed-bit repair density via carry states", + "head": "dbd9da3eed9a0045b77de861099e869259f1ad13" + }, + { + "number": 763, + "title": "Research audit: compact interior carries and exact exceptional repair (no new kappa)", + "head": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6" + }, + { + "number": 735, + "title": "Research audit: tighten the packed-bit repair envelope (no new kappa)", + "head": "8d36139e49add1e55795e283b3bfa45e1cfe1bf0" + } + ], + "novelty": "Exact repeated earlier-source one-digit raw pair law, support and order; prior compact audit concerns later-source interior carries.", + "stopping_rule": "Complete all specified rectangles and controls; no optimization search or new frontier", + "result": "Raw pair translates by 2B on saturated z=1 fibre; repaired pair cancels. No new kappa.", + "final_overlap_refresh": { + "open_pr_count": 755, + "newest_pr": 1100, + "query": "compact boundary / compact cancellation / compact involution in full titles and bodies", + "matching_new_prs": [], + "result": "Distinct one-digit earlier-source repetition law; no overlapping PR found." + }, + "completion_time_utc": "2026-10-13T18:11:37.846260+00:00" +} diff --git a/research/compact-boundary-cancellation-seed51/README.md b/research/compact-boundary-cancellation-seed51/README.md new file mode 100644 index 0000000000..3a16ec6f55 --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/README.md @@ -0,0 +1,172 @@ +# Compact boundary cancellation requires completed repair + +**Research note / scoped negative result. No new kappa.** Assignment seed 51 +(Windows OS CSPRNG), recursive interfaces. Analysis base +`abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`; selected conditional kappa +`1661960547713947/10^18` (#942), unchanged. + +The explicit proposed mechanism was to keep a compact parity operation open +across a recursive boundary and replace its return by the same forward word, +using the ideal operation's involution. The raw four-rotation implementation +is not an involution. +This note gives the exact one-digit obstruction, its complete support and +order, and the remaining cost recurrence. It does not identify a defect in the +existing repaired construction. + +## Precise statement and proof + +Use one compact digit (`n=1`, `f=2`, offset `rho=0`). Let `B=2^G`, let +`Q=2^N` be the whole target-slot modulus, and assume `G>=1`, `N>=G+2`. +In the retained physical implementation `N=2K`. A control bit `z` is fixed; +the other source bits and the arbitrary back digit are spectators. The +earlier-source sequence S is, in execution order, + +``` +y <- y + 2*z*t mod Q +t <- t + (y mod 2) mod B +y <- y + z*(1-2*t) mod Q +t <- t - ((y mod 2) XOR z) mod B +``` + +Each temporal update is physically swap/rotate/swap. These swaps restore the +back field exactly. The ideal T is `(y,t) -> (y XOR z,t)`. + +If `z=0`, both y updates vanish and the temporary load/unload cancel. If +`z=1`, write the incoming parity as a. For a=0 there is no temporary load, +and the net target displacement is 1. For a=1 and `t=G+4` with `y=8B+1,t=B-1`: the target guard is safe, +but S^2 shifts y by 2B. It is not a phenomenon restricted to tiny empty +guard intervals. The omitted highest selected bit is zero in these witnesses. + +## What the boundary optimization can actually do + +Let E be the **completed, repaired** earlier-source operation controlled by +the parity of a compact front digit u. It preserves u,t,b and is exactly an +involution. Write L_x for the raw modular compact load from x. A later-source +word has the pattern `E L_x E L_x^-1` in execution order, followed by its +outer exceptional repair and highest-bit operation. Two adjacent E's cancel +only when those E's are actually adjacent in the complete program. Moving +outer repair or a recursive child across that boundary needs a separate +commutation/changed-layout proof. This note supplies neither. + +Even granting those adjacencies, using raw S instead of E leaves the +translation above. For an isolated repeated raw pair, its exact correction +is a translation by -2B on `z=1,t=B-1`. The predicate is invariant under S^2; +the correction therefore restores the identity on every address. The +verifier checks this constructive correction, but does not claim a physical +fixed-tape implementation saving. + +In particular, two later-source blocks concatenate as +`E L_x E L_x^-1 E L_z E L_z^-1`. There are no adjacent E's: the inverse +load intervenes. Equal E labels alone do not permit cancellation. No +commutation with L is assumed. + +Price the favorable boundary mechanism before implementation. One isolated +forward/return pair of earlier-source raw words uses eight compact swaps and +eight rotations. A complete ideal E pair can be deleted entirely if adjacent; +a raw S pair left in place needs the correction above. A literal S inverse +already provides an exact alternative return with the original eight swaps +and eight rotations. With an intervening child H, `S^-1 H S` remains the +appropriate conjugated program (composition notation); replacing the inverse +by S needs additional proof, even for the identity child. This optimistic +fixed number of eliminated pairs changes only a node constant. Repair, +highest-bit operations, source/control arithmetic and tape transport must +still be billed. It is not a supplier invoice or an attained construction. + +For a new isolated raw-pair repair, delta=`1/(2B)` over the full complete +rectangle. Under the retained fixed-tape repair interface, extraction, +inverse address calculation, sorting and reinsertion cost + +``` +O(V + M*A^3 + delta*M*A*(R+A)), V=M*R. +``` + +With `G=4*ceil(log2 p)+6`, `A=O(p)` and superpolynomial record width R, +the extra term is O(V). It cannot be silently deleted, even though it is +asymptotically absorbed. Retain source access, rewinds, parking, clearing, +row splits, reservations and every recursive child. Granting a fixed number +of admissible cancellations changes a node constant, not the recurrence + +``` +F(e) <= (s/W)*F(e/m) + O(G^tau*e^tau + 1), +F(e) = O(e) for e < d^beta. +``` + +The child multiplier s/W, chi and leaf exponent are unchanged. This scoped +mechanism alone establishes no improved conditional kappa. Growing batches, +changed rank profiles, multi-digit repair support and transporting children +in a permuted layout are separate problems. + +## Reproduction and evidence + +From the repository root, Python 3.9+ and standard library only: + +```sh +python3 -B research/compact-boundary-cancellation-seed51/verify.py +``` + +Expected: `PASS_COMPACT_BOUNDARY_CANCELLATION states=40800 production=1176 controls=8 no_new_kappa`. +Exact per-domain counts are in RESULT.json. `python3 -O -B .../verify.py` checks the same obligations +with Python assertions disabled. The checker uses explicit failures. + +Sixteen complete one-digit domains have G=1..4 and N=G+2..G+5; every z,y,t +is checked for the parity formula, bijection, literal inverse, repeated-pair +support, exact exceptional order and constructive pair repair. A separate +retained physical interpreter checks targeted two-slot cases including every +back digit in each fixture. Those comparisons are not exhaustive over the +whole source-slot rectangle. Eight negative controls distinguish restoration, +inversion, pair support, guard admission and repair sign. The universal +statement rests on the written parity proof, not a finite or formal theorem +claim. No search or optimality assertion is made. + +Run `python3 -B research/compact-boundary-cancellation-seed51/test_package.py` +for a clean relocated replay under `-I -O -B` and four deliberately injected +faults: source drift, receipt drift, formula sign and repair sign. Expected: +`PASS_COMPACT_BOUNDARY_PACKAGE relocated_isolated_optimized=PASS faults=4`. +VALIDATION.json records the local environment and affected existing tests. + +SOURCES.json pins the consumed sources and the selected construction/review +chain using Git blob SHA1 and SHA256 of LF-normalized text. CRLF-to-LF is the +only permitted normalization; both hashes are checked. No archives or frozen +supplier payloads are regenerated. CLAIM.json records selection and overlap. + +## Scope and attribution + +Credit Douglas Colkitt's compact-control movement/layout construction and +retained simulator, OpenAI's upstream multiplication framework, and the +selected #942 lineage credited in the maintainer review. John-Michael +Smith's #763 compact-carry audit studies later-source interior digit carries; +Precious Oyetunji's #773 and Aryan Sudhir's #735 study the distinct wide-slot +gadget. Their existing guard/repair conclusions are respected. This note adds +an exact **repeated earlier-source boundary** law, support and order, rather +than reopening their carry searches. #1012 studies hosted T37 restoration +mass; #1057 studies additive echo memory. Neither result is imported here. + +Prepared for the requesting contributor with substantial OpenAI Codex +assistance in derivation, implementation, verification and writing; no human +identity is inferred. New material is Apache-2.0 under the repository license. +All-size/compiler, common-label/mutable-source, hosting, fixed-tape, +precision and analytic obligations remain inherited. No full multiplication +proof, current supplier improvement or hosted CI result is claimed. diff --git a/research/compact-boundary-cancellation-seed51/RESULT.json b/research/compact-boundary-cancellation-seed51/RESULT.json new file mode 100644 index 0000000000..5567712562 --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/RESULT.json @@ -0,0 +1,160 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "controls": [ + "omitting_saturation_test_fails", + "raw_forward_is_not_inverse", + "raw_pair_is_not_identity", + "raw_word_is_not_ideal", + "restored_temporary_does_not_imply_identity", + "safe_target_guard_does_not_replace_digit_guard", + "single_word_half_density_is_not_pair_density", + "wrong_repair_sign_fails" + ], + "domains": [ + { + "G": 1, + "exceptional_word_order": 4, + "pair_support": 8, + "single_support": 4, + "states": 32, + "width": 3 + }, + { + "G": 1, + "exceptional_word_order": 8, + "pair_support": 16, + "single_support": 8, + "states": 64, + "width": 4 + }, + { + "G": 1, + "exceptional_word_order": 16, + "pair_support": 32, + "single_support": 16, + "states": 128, + "width": 5 + }, + { + "G": 1, + "exceptional_word_order": 32, + "pair_support": 64, + "single_support": 32, + "states": 256, + "width": 6 + }, + { + "G": 2, + "exceptional_word_order": 4, + "pair_support": 16, + "single_support": 8, + "states": 128, + "width": 4 + }, + { + "G": 2, + "exceptional_word_order": 8, + "pair_support": 32, + "single_support": 16, + "states": 256, + "width": 5 + }, + { + "G": 2, + "exceptional_word_order": 16, + "pair_support": 64, + "single_support": 32, + "states": 512, + "width": 6 + }, + { + "G": 2, + "exceptional_word_order": 32, + "pair_support": 128, + "single_support": 64, + "states": 1024, + "width": 7 + }, + { + "G": 3, + "exceptional_word_order": 4, + "pair_support": 32, + "single_support": 16, + "states": 512, + "width": 5 + }, + { + "G": 3, + "exceptional_word_order": 8, + "pair_support": 64, + "single_support": 32, + "states": 1024, + "width": 6 + }, + { + "G": 3, + "exceptional_word_order": 16, + "pair_support": 128, + "single_support": 64, + "states": 2048, + "width": 7 + }, + { + "G": 3, + "exceptional_word_order": 32, + "pair_support": 256, + "single_support": 128, + "states": 4096, + "width": 8 + }, + { + "G": 4, + "exceptional_word_order": 4, + "pair_support": 64, + "single_support": 32, + "states": 2048, + "width": 6 + }, + { + "G": 4, + "exceptional_word_order": 8, + "pair_support": 128, + "single_support": 64, + "states": 4096, + "width": 7 + }, + { + "G": 4, + "exceptional_word_order": 16, + "pair_support": 256, + "single_support": 128, + "states": 8192, + "width": 8 + }, + { + "G": 4, + "exceptional_word_order": 32, + "pair_support": 512, + "single_support": 256, + "states": 16384, + "width": 9 + } + ], + "exhaustive_states": 40800, + "production_comparisons": 1176, + "scope": "One compact digit, rho=0. General proof is written, not formally checked. Production comparisons are targeted, not exhaustive.", + "seed": 51, + "status": "SCOPED NEGATIVE RESULT; NO NEW KAPPA", + "universal_pair_support": "1/(2*2^G) over z,y,t; 1/2^G conditional on z=1", + "witness": { + "G": 2, + "K": 6, + "b": 2, + "first_y": 40, + "ideal_pair_y": 33, + "second_y": 41, + "t": 3, + "x": 1, + "y": 33 + } +} diff --git a/research/compact-boundary-cancellation-seed51/SOURCES.json b/research/compact-boundary-cancellation-seed51/SOURCES.json new file mode 100644 index 0000000000..5172eabb46 --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/SOURCES.json @@ -0,0 +1,50 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "normalization": "Text CRLF to LF only; no other normalization", + "files": { + "notes/compact-control-movement.tex": { + "lf_sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357" + }, + "notes/compact-control-layout.tex": { + "lf_sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87", + "git_blob": "16f4d233471a7d189163ae7e7902becadecbba64" + }, + "scripts/audit_compact_controls.py": { + "lf_sha256": "c3513cd6b41a20bc33b392d66c1536f0a5fcaa76088848361a3aef64074fa989", + "git_blob": "22da5574cb160fafab359a0a41bfe86db5a3bc34" + }, + "scripts/certify.py": { + "lf_sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", + "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a" + }, + "scripts/prepare_layers.py": { + "lf_sha256": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947", + "git_blob": "8e17b52f9573135426d7ba6865c8c9bc8da8639a" + }, + "scripts/search_network.py": { + "lf_sha256": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a", + "git_blob": "f03d5c1b2c81afd6c2f1d3ba9e17d4e7bcd31b9b" + }, + "certificates/selected-result.json": { + "lf_sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3", + "git_blob": "3d7529d77a5f22d8c6f64f98bd5a0e71b8eee892" + }, + "research/community-frontier942-audit/SELECTED-SOURCE.json": { + "lf_sha256": "1cd8dfde15919d1c3df9796b262e67898143d9793d2b86ee7b0a47fc903654c9", + "git_blob": "7bb22cec9e1150f81c2d695c73d9f5fe4c847f84" + }, + "research/community-frontier942-audit/ASSEMBLY.json": { + "lf_sha256": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a", + "git_blob": "9e71e9c1a1c1cbd1979f0c7bac87495322cbfad0" + }, + "research/complex-t37-owners/PROOF.md": { + "lf_sha256": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "git_blob": "04bdeda39111678e27e2c4baa3ce5c6e0ac6f64b" + }, + "docs/research/community-batch952-review.md": { + "lf_sha256": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "git_blob": "512ce9f18b32007bea71452eb5f3eb85c4d577ad" + } + } +} diff --git a/research/compact-boundary-cancellation-seed51/VALIDATION.json b/research/compact-boundary-cancellation-seed51/VALIDATION.json new file mode 100644 index 0000000000..b3b21ee6bf --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/VALIDATION.json @@ -0,0 +1,35 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "python": "3.12.14 (main, Aug 25 2026, 14:01:42) [MSC v.1944 64 bit (AMD64)]", + "platform": "win32", + "standalone": "PASS states=40800 production=1176 controls=8", + "optimized_standalone": "PASS identical receipt", + "relocated_package": "PASS under -I -O -B; four corruption controls rejected", + "existing_tests": [ + { + "pattern": "test_compact_controls.py", + "passed": 5 + }, + { + "pattern": "test_compact_control_layer.py", + "passed": 7 + }, + { + "pattern": "test_compact_control_patch.py", + "passed": 5 + }, + { + "pattern": "test_selected_result.py", + "passed": 5 + } + ], + "omitted": [ + "Full make verify", + "Selected supplier cold replay", + "Hosted CI", + "Formal theorem proof" + ], + "source_integrity": "All pinned canonical LF SHA256 and Git blob hashes checked; selected assembly digest bound", + "publication": "Local patch only: gh/connector unavailable and no GH_TOKEN/GITHUB_TOKEN in environment", + "patch_checks": "git diff --cached --check; clean base temporary-index git apply --cached --check; reverse application check: PASS" +} diff --git a/research/compact-boundary-cancellation-seed51/test_package.py b/research/compact-boundary-cancellation-seed51/test_package.py new file mode 100644 index 0000000000..3a3c5ada22 --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/test_package.py @@ -0,0 +1,51 @@ +"""Relocated replay and four independently injected package faults.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REL = HERE.relative_to(ROOT) + + +def run(root): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(root / REL / 'verify.py')], + cwd=root, capture_output=True, text=True) + + +with tempfile.TemporaryDirectory(prefix='compact-boundary-') as tmp: + dest = Path(tmp) + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for name in pins['files']: + target = dest / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((ROOT / name).read_bytes()) + shutil.copytree(HERE, dest / REL, ignore=shutil.ignore_patterns('__pycache__')) + clean = run(dest) + if clean.returncode != 0: + raise RuntimeError(clean.stdout + clean.stderr) + verifier = dest / REL / 'verify.py' + original = verifier.read_text() + source = dest / 'notes/compact-control-movement.tex' + original_source = source.read_bytes() + receipt = dest / REL / 'RESULT.json' + original_receipt = receipt.read_bytes() + faults = [ + ('source drift', source, original_source + b'\nsource drift\n'), + ('receipt drift', receipt, original_receipt.replace(b'40800', b'40801')), + ('formula sign', verifier, original.replace('correction = 2 *', 'correction = -2 *').encode()), + ('repair sign', verifier, original.replace('a - 2 * (1 << G)', 'a + 2 * (1 << G)').encode()), + ] + for name, target, replacement in faults: + before = target.read_bytes() + if replacement == before: + raise RuntimeError('Fault injection did not change bytes: ' + name) + target.write_bytes(replacement) + failed = run(dest) + target.write_bytes(before) + if failed.returncode == 0: + raise RuntimeError('Fault was accepted: ' + name) + print('PASS_COMPACT_BOUNDARY_PACKAGE relocated_isolated_optimized=PASS faults=4') diff --git a/research/compact-boundary-cancellation-seed51/verify.py b/research/compact-boundary-cancellation-seed51/verify.py new file mode 100644 index 0000000000..f7eeab9b94 --- /dev/null +++ b/research/compact-boundary-cancellation-seed51/verify.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Exact one-digit boundary census. Standard library; Python >= 3.9.""" +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def literal(y, t, z, G, width, inverse=False): + """Four modular rotations; inversion reverses order and sign.""" + B, Q = 1 << G, 1 << width + if inverse: + t = (t + ((y & 1) ^ z)) % B + y = (y - z * (1 - 2 * t)) % Q + t = (t - (y & 1)) % B + y = (y - 2 * z * t) % Q + else: + y = (y + 2 * z * t) % Q + t = (t + (y & 1)) % B + y = (y + z * (1 - 2 * t)) % Q + t = (t - ((y & 1) ^ z)) % B + return y, t + + +def formula(y, t, z, G, width): + """Independent parity partition, derived in README.md.""" + correction = 2 * (1 << G) if z and (y & 1) and t == (1 << G) - 1 else 0 + return ((y ^ z) + correction) % (1 << width), t + + +def repaired_pair(y, t, z, G, width): + a, b = literal(y, t, z, G, width) + a, b = literal(a, b, z, G, width) + if z and b == (1 << G) - 1: + a = (a - 2 * (1 << G)) % (1 << width) + return a, b + + +def source_pins(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for name, pin in pins['files'].items(): + data = (ROOT / name).read_bytes().replace(b'\r\n', b'\n') + require(hashlib.sha256(data).hexdigest() == pin['lf_sha256'], 'Source drift: ' + name) + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require(blob == pin['git_blob'], 'Git blob mismatch: ' + name) + selected = json.loads((ROOT / 'certificates/selected-result.json').read_text()) + require(selected['kappa'] == '1661960547713947/1000000000000000000', 'Selected kappa changed') + for key in ('certificate', 'source_manifest', 'proof', 'review'): + require(selected[key] in pins['files'], 'Unpinned selected chain: ' + key) + require(pins['files'][selected['certificate']]['lf_sha256'] == selected['certificate_sha256'], + 'Selected assembly binding failed') + return pins['base_commit'] + + +def census(): + total = 0 + rows = [] + # All y,t,z in these 16 complete one-digit rectangles, not random samples. + for G in range(1, 5): + for width in range(G + 2, G + 6): + B, Q = 1 << G, 1 << width + disagreements = pair_support = 0 + images = set() + for z in (0, 1): + images.clear() + for t in range(B): + for y in range(Q): + out = literal(y, t, z, G, width) + require(out == formula(y, t, z, G, width), 'Parity formula') + require(literal(*out, z, G, width, inverse=True) == (y, t), 'Literal inverse') + images.add(out) + disagreements += out != (y ^ z, t) + pair = literal(*out, z, G, width) + expected = ((y + (2 * B if z and t == B - 1 else 0)) % Q, t) + require(pair == expected, 'Boundary translation') + pair_support += pair != (y, t) + require(repaired_pair(y, t, z, G, width) == (y, t), 'Pair repair') + total += 1 + require(len(images) == Q * B, 'Full permutation coverage') + require(disagreements == Q // 2, 'Single-word support cardinality') + require(pair_support == Q, 'Pair support cardinality') + # The exceptional z=1 fibre is one cycle of exact length Q/B. + y, t = 1, B - 1 + order = Q // B + for step in range(1, order + 1): + y, t = literal(y, t, 1, G, width) + require(((y, t) == (1, B - 1)) == (step == order), 'Exact fibre order') + rows.append(dict(G=G, width=width, states=2 * Q * B, + single_support=disagreements, pair_support=pair_support, + exceptional_word_order=order)) + return total, rows + + +def production_comparison(): + # The retained implementation contains actual front/back swaps and full + # two-slot target widths; it is not used by the independent census above. + sys.path.insert(0, str(ROOT / 'scripts')) + spec = importlib.util.spec_from_file_location('retained_compact', ROOT / 'scripts/audit_compact_controls.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + count = 0 + for G, K in ((1, 4), (2, 6), (3, 8)): + B, Q = 1 << G, 1 << (2 * K) + for y in sorted({0, 1, 2, Q - 1, 4 * B, 4 * B + 1, Q - 4 * B - 1}): + for t in range(B): + for z in (0, 1): + for b in range(B): + old = dict(x=z, y=y, t=t, b=b) + out = module.execute(old, 1, K, 0, G) + wanted_y, wanted_t = literal(y, t, z, G, 2 * K) + require(out == dict(old, y=wanted_y, t=wanted_t), 'Retained primitive disagreement') + twice = module.execute(out, 1, K, 0, G) + require(twice == dict(old, y=(y + (2 * B if z and t == B - 1 else 0)) % Q), 'Retained boundary') + fixed = module.repaired(module.repaired(old, 1, K, 0, G), 1, K, 0, G) + require(fixed == old, 'Retained completed cancellation') + count += 1 + return count + + +def negative_controls(): + G, width, y, t, z = 2, 12, 33, 3, 1 + a = literal(y, t, z, G, width) + b = literal(*a, z, G, width) + checks = { + 'raw_word_is_not_ideal': a != (y ^ z, t), + 'raw_pair_is_not_identity': b != (y, t), + 'raw_forward_is_not_inverse': literal(*a, z, G, width) != (y, t), + 'omitting_saturation_test_fails': b != (y, t), + 'wrong_repair_sign_fails': ((b[0] + 8) % (1 << width), b[1]) != (y, t), + 'single_word_half_density_is_not_pair_density': (1 << (width - 1)) != (1 << width), + 'restored_temporary_does_not_imply_identity': b[1] == t and b[0] != y, + 'safe_target_guard_does_not_replace_digit_guard': 8 <= (y >> 1) < 32 - 8 and b != (y, t), + } + for name, value in checks.items(): + require(value, 'Failed rejection control: ' + name) + require(repaired_pair(y, t, z, G, width) == (y, t), 'Correct repair control') + require(literal(*a, z, G, width, inverse=True) == (y, t), 'Correct inverse control') + return sorted(checks) + + +def result(): + base = source_pins() + total, rows = census() + return dict(status='SCOPED NEGATIVE RESULT; NO NEW KAPPA', base_commit=base, + seed=51, exhaustive_states=total, domains=rows, + production_comparisons=production_comparison(), + controls=negative_controls(), witness=dict(G=2, K=6, x=1, y=33, t=3, b=2, + first_y=40, second_y=41, ideal_pair_y=33), + universal_pair_support='1/(2*2^G) over z,y,t; 1/2^G conditional on z=1', + scope='One compact digit, rho=0. General proof is written, not formally checked. Production comparisons are targeted, not exhaustive.') + + +if __name__ == '__main__': + receipt = result() + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n', encoding='utf-8') + else: + require(receipt == json.loads((HERE / 'RESULT.json').read_text()), 'Receipt mismatch') + print('PASS_COMPACT_BOUNDARY_CANCELLATION states=%d production=%d controls=%d no_new_kappa' % + (receipt['exhaustive_states'], receipt['production_comparisons'], len(receipt['controls']))) diff --git a/research/frontier1042-capsule-closure-seed75/CLAIM.md b/research/frontier1042-capsule-closure-seed75/CLAIM.md new file mode 100644 index 0000000000..3b0344d474 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/CLAIM.md @@ -0,0 +1,10 @@ +# Sprint claim + +- Track 75–84, independent verification; OS-random seed **75**. +- Exact base: `ba82555c64e1879e4b7decce28186f208fcb8262`. +- Chosen object: closed, path-safe audit of the selected PR1042 replay capsule. +- Method: standard-library tar/SHA-256 checker; no extraction or construction imports. +- Deliverable: verifier, deterministic receipt, six controls, exact pins and scope note; no new kappa. +- Stopping rule: all members and declared edges checked, all controls reject, optimized run agrees, selected-record checks pass. + +Candidates considered were invoice/outer arithmetic (overlapped PR1112), T16 owner/profile checking (overlapped prior audits), and capsule closure (chosen as distinct publication-evidence coverage). No pinned sprint coordination issue was found. diff --git a/research/frontier1042-capsule-closure-seed75/NOTICE.md b/research/frontier1042-capsule-closure-seed75/NOTICE.md new file mode 100644 index 0000000000..9ef73ad282 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/NOTICE.md @@ -0,0 +1,2 @@ +New material: Copyright 2026 Martin Rv. Apache-2.0. +Prepared with substantial Perplexity AI assistance. PR1042/batch1047 construction, review and predecessor attribution remain with their original contributors and notices. diff --git a/research/frontier1042-capsule-closure-seed75/PINS.json b/research/frontier1042-capsule-closure-seed75/PINS.json new file mode 100644 index 0000000000..18c7db8ec3 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/PINS.json @@ -0,0 +1,13 @@ +{ + "schema": "integer-mult-frontier1042-capsule-closure-v1", + "assignment_seed": 75, + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "kappa": "1672188119205421/1000000000000000000", + "decimal": "0.001672188119205421", + "archive": {"path": "research/community-frontier1042-audit/selected-replay.tar.gz", "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", "members": 458, "declared_artifacts": 457, "expanded_bytes": 45647427}, + "selected_record": {"path": "certificates/selected-result.json", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7"}, + "integration_record": {"path": "docs/research/community-batch1047-integration.json", "sha256": "b04623d39df453804f327a203f07882554b138e6b322b9d1f674d84d94a14a8c"}, + "promoted_receipts": {"ASSEMBLY.json": "t16/ASSEMBLY.json", "BASELINE-BINDING.json": "BASELINE-BINDING.json", "INDEPENDENT-T16.json": "t16/INDEPENDENT-T16.json", "RESULT.json": "RESULT.json", "STAGES.json": "STAGES.json", "T16-REPLAY.json": "t16/REPLAY.json"}, + "stages": ["leaver-manifest", "slots-manifest", "t16-manifest", "base", "cells", "chain", "independent-leaver", "leaver-global", "slots", "t16"] +} diff --git a/research/frontier1042-capsule-closure-seed75/PROOF.md b/research/frontier1042-capsule-closure-seed75/PROOF.md new file mode 100644 index 0000000000..1866e5dbce --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/PROOF.md @@ -0,0 +1,11 @@ +# Closure argument + +Let `A` be the byte-pinned selected replay archive and `R` its archived `RESULT.json`. + +1. Every entry is a unique relative POSIX path, a bounded regular non-executable file; no extraction occurs. +2. `R.artifacts` equals `members(A) - {RESULT.json}` and every declared SHA-256 equals bytes read from `A`. The separately pinned archive digest binds the self-excluded result too. +3. `STAGES.json` equals `R.stages`; the ten fixed names, zero exit codes and log digests are checked. +4. Six promoted public receipts equal their archived bytes. +5. Exact selected and integration record pins bind the value, source head, certificate, source manifest, archive and promoted receipts. + +Therefore all 458 capsule bytes and stated publication edges are authenticated relative to `PINS.json`. This says nothing about execution history or the inherited multiplication theorem assumptions. diff --git a/research/frontier1042-capsule-closure-seed75/README.md b/research/frontier1042-capsule-closure-seed75/README.md new file mode 100644 index 0000000000..3872c61ede --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/README.md @@ -0,0 +1,29 @@ +# Independent PR1042 replay-capsule closure + +**Status:** independent verification; no new construction and no new kappa. + +This package independently checks the frozen publication capsule behind selected PR1042, conditional kappa `1672188119205421 / 10^18`. It was selected by OS-random seed **75** at base `ba82555c64e1879e4b7decce28186f208fcb8262`. + +## Result + +`verify.py` treats `research/community-frontier1042-audit/selected-replay.tar.gz` as untrusted data, uses only the Python standard library, never extracts a member, and imports no construction code. It authenticates 458 safe regular members (45,647,427 expanded bytes), all 457 declared artifact digests, exact inventory closure, ten successful stage/log bindings, six promoted receipts, and the selected/integration publication pins. + +## Reproduce + +```sh +make frontier1042-capsule-closure-verify +``` + +Expected final markers: `PASS_FRONTIER1042_CAPSULE_CLOSURE`, six tests, `OK`. The target also runs under optimized Python so checks cannot depend on removable assertions. + +## Controls + +The suite rejects path traversal, duplicate members, undeclared members, mutated artifact bytes, a nonzero stage, and a promoted-receipt mismatch. + +## Scope + +This is finite integrity and binding evidence about the committed capsule. It does not establish that recorded commands ran, independently recompute T16 mathematics, verify named source packages, discharge inherited interfaces, prove analytic transfer, benchmark multiplication, or formalize the full theorem. + +## Attribution + +Martin Rv (@martinxxx9), with substantial Perplexity AI assistance in research, implementation, verification and writing. It preserves all PR1042 and batch1047 predecessor attribution. Apache-2.0. diff --git a/research/frontier1042-capsule-closure-seed75/RESULT.json b/research/frontier1042-capsule-closure-seed75/RESULT.json new file mode 100644 index 0000000000..95c1d7e617 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/RESULT.json @@ -0,0 +1,22 @@ +{ + "status": "PASS_FRONTIER1042_CAPSULE_CLOSURE", + "assignment_seed": 75, + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "kappa": "1672188119205421/1000000000000000000", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "members": 458, + "declared_artifacts": 457, + "expanded_bytes": 45647427, + "stages": 10, + "promoted_receipts": 6, + "controls": [ + "C1_path_traversal", + "C2_duplicate_member", + "C3_nondeclared_member", + "C4_mutated_artifact_digest", + "C5_nonzero_stage", + "C6_promoted_receipt_mismatch" + ], + "scope": "Independent standard-library, data-only finite closure audit of the frozen PR1042 selected replay capsule. Authenticates paths, complete bytes, receipt edges and publication pins; does not authenticate execution, replay construction code, all-size interfaces, analytic transfer or the multiplication theorem." +} diff --git a/research/frontier1042-capsule-closure-seed75/test_package.py b/research/frontier1042-capsule-closure-seed75/test_package.py new file mode 100644 index 0000000000..6f66740230 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/test_package.py @@ -0,0 +1,50 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +import copy +from pathlib import Path +import sys +import tarfile +import unittest +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify + +class FakeMember: + def __init__(self, name, size=0, mode=0o644, regular=True): + self.name, self.size, self.mode, self._regular = name, size, mode, regular + def isfile(self): return self._regular + +class NamespaceControls(unittest.TestCase): + def test_C1_path_traversal(self): + with self.assertRaisesRegex(ValueError, "unsafe archive"): + verify.validate_namespace([FakeMember("../escape")]) + def test_C2_duplicate_member(self): + with self.assertRaisesRegex(ValueError, "duplicate archive"): + verify.validate_namespace([FakeMember("a"), FakeMember("a")]) + +class ClosureControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.pins = verify.strict_json((verify.HERE / "PINS.json").read_bytes(), "PINS.json") + a = verify.ROOT / cls.pins["archive"]["path"] + cls.names, _, cls.digests, cls.roots = verify.read_capsule(a) + cls.result = verify.strict_json(cls.roots["RESULT.json"], "RESULT.json") + cls.stages = verify.strict_json(cls.roots["STAGES.json"], "STAGES.json") + def validate(self, result=None, stages=None, names=None, digests=None): + return verify.validate_result(result or self.result, stages or self.stages, + names or self.names, digests or self.digests, + self.pins["stages"]) + def test_C3_nondeclared_member(self): + result = copy.deepcopy(self.result); result["artifacts"].pop(next(iter(result["artifacts"]))) + with self.assertRaisesRegex(ValueError, "not exact archive closure"): self.validate(result=result) + def test_C4_mutated_artifact_digest(self): + digests = dict(self.digests); name = next(iter(self.result["artifacts"])); digests[name] = "0" * 64 + with self.assertRaisesRegex(ValueError, "artifact digest differs"): self.validate(digests=digests) + def test_C5_nonzero_stage(self): + stages = copy.deepcopy(self.stages); stages[0]["exit_code"] = 1 + result = copy.deepcopy(self.result); result["stages"] = stages + with self.assertRaisesRegex(ValueError, "recorded stage failed"): self.validate(result=result, stages=stages) + def test_C6_promoted_receipt_mismatch(self): + outer = verify.repository_file("research/community-frontier1042-audit/ASSEMBLY.json") + self.assertNotEqual(outer + b"x", self.roots["t16/ASSEMBLY.json"]) + +if __name__ == "__main__": unittest.main(verbosity=2) diff --git a/research/frontier1042-capsule-closure-seed75/verify.py b/research/frontier1042-capsule-closure-seed75/verify.py new file mode 100644 index 0000000000..1676d89098 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent data-only closure audit of the selected PR1042 replay capsule.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path, PurePosixPath +import re +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HEX64 = re.compile(r"[0-9a-f]{64}") +MAX_MEMBERS = 1000 +MAX_MEMBER_BYTES = 8 * 1024 * 1024 +MAX_TOTAL_BYTES = 64 * 1024 * 1024 +ROOT_MEMBERS = { + "RESULT.json", "STAGES.json", "BASELINE-BINDING.json", + "t16/ASSEMBLY.json", "t16/INDEPENDENT-T16.json", "t16/REPLAY.json", +} + +def require(ok, message): + if not ok: + raise ValueError(message) + +def digest(data): + return sha256(data).hexdigest() + +def strict_json(data, label): + def no_duplicates(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key in {label}: {key}") + out[key] = value + return out + try: + return json.loads(data, object_pairs_hook=no_duplicates) + except (UnicodeDecodeError, json.JSONDecodeError) as exc: + raise ValueError(f"invalid JSON in {label}: {exc}") from exc + +def safe_name(name): + require(type(name) is str and name and "\\" not in name and ":" not in name, + "invalid archive member path") + p = PurePosixPath(name) + require(not p.is_absolute() and p.as_posix() == name and + all(part not in ("", ".", "..") for part in p.parts), + "unsafe archive member path: " + name) + return name + +def validate_namespace(members): + require(type(members) is list and len(members) <= MAX_MEMBERS, + "archive member limit exceeded") + names, total = [], 0 + for member in members: + name = safe_name(member.name) + require(member.isfile(), "archive member is not a regular file: " + name) + require(type(member.size) is int and 0 <= member.size <= MAX_MEMBER_BYTES, + "archive member size limit exceeded: " + name) + require(member.mode & 0o111 == 0, "archive member is executable: " + name) + names.append(name) + total += member.size + require(len(names) == len(set(names)), "duplicate archive member name") + require(total <= MAX_TOTAL_BYTES, "expanded archive size limit exceeded") + return names, total + +def read_capsule(path): + raw_roots, member_digests = {}, {} + with tarfile.open(path, "r:gz") as archive: + members = archive.getmembers() + names, total = validate_namespace(members) + for member in members: + stream = archive.extractfile(member) + require(stream is not None, "archive regular file is unreadable: " + member.name) + payload = stream.read(MAX_MEMBER_BYTES + 1) + require(len(payload) == member.size, "archive member length differs: " + member.name) + member_digests[member.name] = digest(payload) + if member.name in ROOT_MEMBERS: + raw_roots[member.name] = payload + require(ROOT_MEMBERS <= set(raw_roots), "required root receipt missing") + return names, total, member_digests, raw_roots + +def validate_result(result, stages, names, member_digests, expected_stages): + require(type(result) is dict and result.get("status") == "PASS_COMPLETE_PR1042_COMPOSITION", + "unexpected capsule result status") + artifacts = result.get("artifacts") + require(type(artifacts) is dict, "artifact inventory is not an object") + require(set(artifacts) == set(names) - {"RESULT.json"}, + "RESULT artifact inventory is not exact archive closure") + for name, expected in artifacts.items(): + require(type(expected) is str and HEX64.fullmatch(expected) is not None, + "invalid artifact digest: " + name) + require(member_digests[name] == expected, "artifact digest differs: " + name) + recorded_stages = result.get("stages") + require(type(recorded_stages) is list and recorded_stages == stages, + "STAGES.json differs from RESULT stages") + require([item.get("name") for item in stages] == expected_stages, + "stage sequence differs") + for item in stages: + name = item.get("name") + require(type(item.get("exit_code")) is int and item["exit_code"] == 0, + "recorded stage failed: " + str(name)) + expected = item.get("log_sha256") + require(type(expected) is str and HEX64.fullmatch(expected) is not None, + "invalid stage log digest: " + str(name)) + log_name = name + ".log" + require(log_name in member_digests and member_digests[log_name] == expected, + "stage log binding differs: " + str(name)) + return len(artifacts) + +def repository_file(relative, expected=None): + require(type(relative) is str, "invalid repository path") + path = (ROOT / relative).resolve() + require(path.is_relative_to(ROOT.resolve()) and path.is_file(), + "missing repository file: " + relative) + data = path.read_bytes() + if expected is not None: + require(digest(data) == expected, "repository pin differs: " + relative) + return data + +def check(pins): + require(pins.get("schema") == "integer-mult-frontier1042-capsule-closure-v1", + "unsupported pins schema") + archive_pin = pins["archive"] + archive_raw = repository_file(archive_pin["path"], archive_pin["sha256"]) + names, expanded, member_digests, roots = read_capsule(ROOT / archive_pin["path"]) + require(len(names) == archive_pin["members"] and expanded == archive_pin["expanded_bytes"], + "archive count or expanded size differs") + result = strict_json(roots["RESULT.json"], "RESULT.json") + stages = strict_json(roots["STAGES.json"], "STAGES.json") + artifact_count = validate_result(result, stages, names, member_digests, pins["stages"]) + require(artifact_count == archive_pin["declared_artifacts"], "artifact count differs") + require(result.get("kappa") == pins["kappa"] and result.get("decimal") == pins["decimal"], + "capsule selected value differs") + promoted_hashes = {} + for outer, inner in pins["promoted_receipts"].items(): + outer_data = repository_file("research/community-frontier1042-audit/" + outer) + require(outer_data == roots[inner], "promoted receipt differs from capsule: " + outer) + promoted_hashes[outer] = digest(outer_data) + selected_pin = pins["selected_record"] + selected = strict_json(repository_file(selected_pin["path"], selected_pin["sha256"]), selected_pin["path"]) + require(selected.get("audited_source_head") == pins["audited_source_head"], "audited source head differs") + require(selected.get("kappa") == pins["kappa"] and selected.get("decimal") == pins["decimal"], + "published selected value differs") + require(selected.get("certificate") == "research/community-frontier1042-audit/ASSEMBLY.json", + "selected certificate path differs") + require(selected.get("certificate_sha256") == promoted_hashes["ASSEMBLY.json"], + "selected certificate digest differs") + integration_pin = pins["integration_record"] + integration = strict_json(repository_file(integration_pin["path"], integration_pin["sha256"]), integration_pin["path"]) + receipts = integration.get("receipts") + require(type(receipts) is dict, "integration receipt map missing") + require(receipts.get(archive_pin["path"]) == digest(archive_raw), "integration archive digest differs") + for outer, expected in promoted_hashes.items(): + relative = "research/community-frontier1042-audit/" + outer + require(receipts.get(relative) == expected, "integration promoted digest differs: " + outer) + source_path = selected.get("source_manifest") + source_data = repository_file(source_path) + require(receipts.get(source_path) == digest(source_data), "integration source manifest digest differs") + require(result.get("baseline_binding_sha256") == promoted_hashes["BASELINE-BINDING.json"], + "capsule baseline binding differs") + require(result.get("selected_assembly_sha256") == promoted_hashes["ASSEMBLY.json"], + "capsule selected assembly binding differs") + return { + "status": "PASS_FRONTIER1042_CAPSULE_CLOSURE", + "assignment_seed": pins["assignment_seed"], "base_commit": pins["base_commit"], + "audited_source_head": pins["audited_source_head"], "kappa": pins["kappa"], + "archive_sha256": digest(archive_raw), "members": len(names), + "declared_artifacts": artifact_count, "expanded_bytes": expanded, + "stages": len(stages), "promoted_receipts": len(promoted_hashes), + "controls": ["C1_path_traversal", "C2_duplicate_member", "C3_nondeclared_member", + "C4_mutated_artifact_digest", "C5_nonzero_stage", "C6_promoted_receipt_mismatch"], + "scope": "Independent standard-library, data-only finite closure audit of the frozen PR1042 selected replay capsule. Authenticates paths, complete bytes, receipt edges and publication pins; does not authenticate execution, replay construction code, all-size interfaces, analytic transfer or the multiplication theorem." + } + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--out", type=Path) + args = ap.parse_args() + pins = strict_json((HERE / "PINS.json").read_bytes(), "PINS.json") + receipt = check(pins) + raw = (json.dumps(receipt, indent=2) + "\n").encode() + if args.out: + args.out.write_bytes(raw) + print(raw.decode(), end="") + print(receipt["status"]) + +if __name__ == "__main__": + try: + main() + except (KeyError, OSError, ValueError, tarfile.TarError) as exc: + raise SystemExit("FAIL: " + str(exc)) from exc From c62ed26b1538e477f96b578f6d9d8a6b176ed363 Mon Sep 17 00:00:00 2001 From: martinxxx9 Date: Wed, 14 Oct 2026 17:36:34 +0200 Subject: [PATCH 2/2] Fix historical PR1042 capsule selection binding Freeze the original selected record as package data, keep live selection checks separate, and add reproducible receipt comparisons plus regression controls. Remove the accidentally bundled PR1108 package to avoid the reported overlap. --- Makefile | 8 + .../CLAIM.json | 59 ------ .../README.md | 172 ---------------- .../RESULT.json | 160 --------------- .../SOURCES.json | 50 ----- .../VALIDATION.json | 35 ---- .../test_package.py | 51 ----- .../verify.py | 169 --------------- .../CLAIM.md | 4 +- .../NOTICE.md | 1 + .../PINS.json | 2 +- .../PROOF.md | 2 +- .../README.md | 19 +- .../SELECTED-RESULT.json | 194 ++++++++++++++++++ .../test_package.py | 54 ++++- .../verify.py | 15 +- 16 files changed, 291 insertions(+), 704 deletions(-) delete mode 100644 research/compact-boundary-cancellation-seed51/CLAIM.json delete mode 100644 research/compact-boundary-cancellation-seed51/README.md delete mode 100644 research/compact-boundary-cancellation-seed51/RESULT.json delete mode 100644 research/compact-boundary-cancellation-seed51/SOURCES.json delete mode 100644 research/compact-boundary-cancellation-seed51/VALIDATION.json delete mode 100644 research/compact-boundary-cancellation-seed51/test_package.py delete mode 100644 research/compact-boundary-cancellation-seed51/verify.py create mode 100644 research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json diff --git a/Makefile b/Makefile index 4035aaa7cb..0f0b0c1100 100644 --- a/Makefile +++ b/Makefile @@ -619,6 +619,14 @@ frontier1042-verify: selected-record-check @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier1042.XXXXXX"); \ python3 -B scripts/verify_frontier1042.py --work "$$work/replay" +# Historical publication evidence; the live pointer has its own selected-record-check target. +.PHONY: frontier1042-capsule-closure-verify +frontier1042-capsule-closure-verify: + python3 -B research/frontier1042-capsule-closure-seed75/verify.py --check + python3 -O -B research/frontier1042-capsule-closure-seed75/verify.py --check + python3 -B research/frontier1042-capsule-closure-seed75/test_package.py + python3 -O -B research/frontier1042-capsule-closure-seed75/test_package.py + # Independent verification: code-disjoint T37 moment endpoints and kappa reduction (no new kappa). .PHONY: t37-endpoints-independent-verify t37-endpoints-independent-verify: diff --git a/research/compact-boundary-cancellation-seed51/CLAIM.json b/research/compact-boundary-cancellation-seed51/CLAIM.json deleted file mode 100644 index 09329a49da..0000000000 --- a/research/compact-boundary-cancellation-seed51/CLAIM.json +++ /dev/null @@ -1,59 +0,0 @@ -{ - "seed": 51, - "randomness": "System.Security.Cryptography.RandomNumberGenerator.Fill; UInt32 modulo 100", - "track": "Recursive interfaces (50-59)", - "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", - "object": "One-digit earlier-source compact raw forward/return cancellation across recursive boundary", - "method": "Exact parity partition, complete small rectangles, independent retained primitive comparisons", - "deliverable": "Scoped negative result, exact support/order, full inherited recurrence and rejection controls", - "finish": "This session; final quarter reserved for verification and packaging", - "candidates": [ - "T37 restoration deferral (overlap PR1012)", - "Additive echo pool reuse (overlap PR1057)", - "Raw versus repaired compact boundary cancellation (chosen)" - ], - "coordination": "No open issue in earliest 100-item API page; related PRs report no pinned sprint issue. No posting connector/gh available, so claim recorded locally.", - "open_pr_snapshot": { - "count": 763, - "first": 1096, - "last": 1 - }, - "related_prs": [ - { - "number": 1057, - "title": "Research: exact additive echoes with three dirty arrays at any depth (no new kappa)", - "head": "78a062df1dcab2bffea5ff4d8243f3da6e465414" - }, - { - "number": 1012, - "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", - "head": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03" - }, - { - "number": 773, - "title": "Research audit: exact packed-bit repair density via carry states", - "head": "dbd9da3eed9a0045b77de861099e869259f1ad13" - }, - { - "number": 763, - "title": "Research audit: compact interior carries and exact exceptional repair (no new kappa)", - "head": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6" - }, - { - "number": 735, - "title": "Research audit: tighten the packed-bit repair envelope (no new kappa)", - "head": "8d36139e49add1e55795e283b3bfa45e1cfe1bf0" - } - ], - "novelty": "Exact repeated earlier-source one-digit raw pair law, support and order; prior compact audit concerns later-source interior carries.", - "stopping_rule": "Complete all specified rectangles and controls; no optimization search or new frontier", - "result": "Raw pair translates by 2B on saturated z=1 fibre; repaired pair cancels. No new kappa.", - "final_overlap_refresh": { - "open_pr_count": 755, - "newest_pr": 1100, - "query": "compact boundary / compact cancellation / compact involution in full titles and bodies", - "matching_new_prs": [], - "result": "Distinct one-digit earlier-source repetition law; no overlapping PR found." - }, - "completion_time_utc": "2026-10-13T18:11:37.846260+00:00" -} diff --git a/research/compact-boundary-cancellation-seed51/README.md b/research/compact-boundary-cancellation-seed51/README.md deleted file mode 100644 index 3a16ec6f55..0000000000 --- a/research/compact-boundary-cancellation-seed51/README.md +++ /dev/null @@ -1,172 +0,0 @@ -# Compact boundary cancellation requires completed repair - -**Research note / scoped negative result. No new kappa.** Assignment seed 51 -(Windows OS CSPRNG), recursive interfaces. Analysis base -`abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`; selected conditional kappa -`1661960547713947/10^18` (#942), unchanged. - -The explicit proposed mechanism was to keep a compact parity operation open -across a recursive boundary and replace its return by the same forward word, -using the ideal operation's involution. The raw four-rotation implementation -is not an involution. -This note gives the exact one-digit obstruction, its complete support and -order, and the remaining cost recurrence. It does not identify a defect in the -existing repaired construction. - -## Precise statement and proof - -Use one compact digit (`n=1`, `f=2`, offset `rho=0`). Let `B=2^G`, let -`Q=2^N` be the whole target-slot modulus, and assume `G>=1`, `N>=G+2`. -In the retained physical implementation `N=2K`. A control bit `z` is fixed; -the other source bits and the arbitrary back digit are spectators. The -earlier-source sequence S is, in execution order, - -``` -y <- y + 2*z*t mod Q -t <- t + (y mod 2) mod B -y <- y + z*(1-2*t) mod Q -t <- t - ((y mod 2) XOR z) mod B -``` - -Each temporal update is physically swap/rotate/swap. These swaps restore the -back field exactly. The ideal T is `(y,t) -> (y XOR z,t)`. - -If `z=0`, both y updates vanish and the temporary load/unload cancel. If -`z=1`, write the incoming parity as a. For a=0 there is no temporary load, -and the net target displacement is 1. For a=1 and `t=G+4` with `y=8B+1,t=B-1`: the target guard is safe, -but S^2 shifts y by 2B. It is not a phenomenon restricted to tiny empty -guard intervals. The omitted highest selected bit is zero in these witnesses. - -## What the boundary optimization can actually do - -Let E be the **completed, repaired** earlier-source operation controlled by -the parity of a compact front digit u. It preserves u,t,b and is exactly an -involution. Write L_x for the raw modular compact load from x. A later-source -word has the pattern `E L_x E L_x^-1` in execution order, followed by its -outer exceptional repair and highest-bit operation. Two adjacent E's cancel -only when those E's are actually adjacent in the complete program. Moving -outer repair or a recursive child across that boundary needs a separate -commutation/changed-layout proof. This note supplies neither. - -Even granting those adjacencies, using raw S instead of E leaves the -translation above. For an isolated repeated raw pair, its exact correction -is a translation by -2B on `z=1,t=B-1`. The predicate is invariant under S^2; -the correction therefore restores the identity on every address. The -verifier checks this constructive correction, but does not claim a physical -fixed-tape implementation saving. - -In particular, two later-source blocks concatenate as -`E L_x E L_x^-1 E L_z E L_z^-1`. There are no adjacent E's: the inverse -load intervenes. Equal E labels alone do not permit cancellation. No -commutation with L is assumed. - -Price the favorable boundary mechanism before implementation. One isolated -forward/return pair of earlier-source raw words uses eight compact swaps and -eight rotations. A complete ideal E pair can be deleted entirely if adjacent; -a raw S pair left in place needs the correction above. A literal S inverse -already provides an exact alternative return with the original eight swaps -and eight rotations. With an intervening child H, `S^-1 H S` remains the -appropriate conjugated program (composition notation); replacing the inverse -by S needs additional proof, even for the identity child. This optimistic -fixed number of eliminated pairs changes only a node constant. Repair, -highest-bit operations, source/control arithmetic and tape transport must -still be billed. It is not a supplier invoice or an attained construction. - -For a new isolated raw-pair repair, delta=`1/(2B)` over the full complete -rectangle. Under the retained fixed-tape repair interface, extraction, -inverse address calculation, sorting and reinsertion cost - -``` -O(V + M*A^3 + delta*M*A*(R+A)), V=M*R. -``` - -With `G=4*ceil(log2 p)+6`, `A=O(p)` and superpolynomial record width R, -the extra term is O(V). It cannot be silently deleted, even though it is -asymptotically absorbed. Retain source access, rewinds, parking, clearing, -row splits, reservations and every recursive child. Granting a fixed number -of admissible cancellations changes a node constant, not the recurrence - -``` -F(e) <= (s/W)*F(e/m) + O(G^tau*e^tau + 1), -F(e) = O(e) for e < d^beta. -``` - -The child multiplier s/W, chi and leaf exponent are unchanged. This scoped -mechanism alone establishes no improved conditional kappa. Growing batches, -changed rank profiles, multi-digit repair support and transporting children -in a permuted layout are separate problems. - -## Reproduction and evidence - -From the repository root, Python 3.9+ and standard library only: - -```sh -python3 -B research/compact-boundary-cancellation-seed51/verify.py -``` - -Expected: `PASS_COMPACT_BOUNDARY_CANCELLATION states=40800 production=1176 controls=8 no_new_kappa`. -Exact per-domain counts are in RESULT.json. `python3 -O -B .../verify.py` checks the same obligations -with Python assertions disabled. The checker uses explicit failures. - -Sixteen complete one-digit domains have G=1..4 and N=G+2..G+5; every z,y,t -is checked for the parity formula, bijection, literal inverse, repeated-pair -support, exact exceptional order and constructive pair repair. A separate -retained physical interpreter checks targeted two-slot cases including every -back digit in each fixture. Those comparisons are not exhaustive over the -whole source-slot rectangle. Eight negative controls distinguish restoration, -inversion, pair support, guard admission and repair sign. The universal -statement rests on the written parity proof, not a finite or formal theorem -claim. No search or optimality assertion is made. - -Run `python3 -B research/compact-boundary-cancellation-seed51/test_package.py` -for a clean relocated replay under `-I -O -B` and four deliberately injected -faults: source drift, receipt drift, formula sign and repair sign. Expected: -`PASS_COMPACT_BOUNDARY_PACKAGE relocated_isolated_optimized=PASS faults=4`. -VALIDATION.json records the local environment and affected existing tests. - -SOURCES.json pins the consumed sources and the selected construction/review -chain using Git blob SHA1 and SHA256 of LF-normalized text. CRLF-to-LF is the -only permitted normalization; both hashes are checked. No archives or frozen -supplier payloads are regenerated. CLAIM.json records selection and overlap. - -## Scope and attribution - -Credit Douglas Colkitt's compact-control movement/layout construction and -retained simulator, OpenAI's upstream multiplication framework, and the -selected #942 lineage credited in the maintainer review. John-Michael -Smith's #763 compact-carry audit studies later-source interior digit carries; -Precious Oyetunji's #773 and Aryan Sudhir's #735 study the distinct wide-slot -gadget. Their existing guard/repair conclusions are respected. This note adds -an exact **repeated earlier-source boundary** law, support and order, rather -than reopening their carry searches. #1012 studies hosted T37 restoration -mass; #1057 studies additive echo memory. Neither result is imported here. - -Prepared for the requesting contributor with substantial OpenAI Codex -assistance in derivation, implementation, verification and writing; no human -identity is inferred. New material is Apache-2.0 under the repository license. -All-size/compiler, common-label/mutable-source, hosting, fixed-tape, -precision and analytic obligations remain inherited. No full multiplication -proof, current supplier improvement or hosted CI result is claimed. diff --git a/research/compact-boundary-cancellation-seed51/RESULT.json b/research/compact-boundary-cancellation-seed51/RESULT.json deleted file mode 100644 index 5567712562..0000000000 --- a/research/compact-boundary-cancellation-seed51/RESULT.json +++ /dev/null @@ -1,160 +0,0 @@ -{ - "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", - "controls": [ - "omitting_saturation_test_fails", - "raw_forward_is_not_inverse", - "raw_pair_is_not_identity", - "raw_word_is_not_ideal", - "restored_temporary_does_not_imply_identity", - "safe_target_guard_does_not_replace_digit_guard", - "single_word_half_density_is_not_pair_density", - "wrong_repair_sign_fails" - ], - "domains": [ - { - "G": 1, - "exceptional_word_order": 4, - "pair_support": 8, - "single_support": 4, - "states": 32, - "width": 3 - }, - { - "G": 1, - "exceptional_word_order": 8, - "pair_support": 16, - "single_support": 8, - "states": 64, - "width": 4 - }, - { - "G": 1, - "exceptional_word_order": 16, - "pair_support": 32, - "single_support": 16, - "states": 128, - "width": 5 - }, - { - "G": 1, - "exceptional_word_order": 32, - "pair_support": 64, - "single_support": 32, - "states": 256, - "width": 6 - }, - { - "G": 2, - "exceptional_word_order": 4, - "pair_support": 16, - "single_support": 8, - "states": 128, - "width": 4 - }, - { - "G": 2, - "exceptional_word_order": 8, - "pair_support": 32, - "single_support": 16, - "states": 256, - "width": 5 - }, - { - "G": 2, - "exceptional_word_order": 16, - "pair_support": 64, - "single_support": 32, - "states": 512, - "width": 6 - }, - { - "G": 2, - "exceptional_word_order": 32, - "pair_support": 128, - "single_support": 64, - "states": 1024, - "width": 7 - }, - { - "G": 3, - "exceptional_word_order": 4, - "pair_support": 32, - "single_support": 16, - "states": 512, - "width": 5 - }, - { - "G": 3, - "exceptional_word_order": 8, - "pair_support": 64, - "single_support": 32, - "states": 1024, - "width": 6 - }, - { - "G": 3, - "exceptional_word_order": 16, - "pair_support": 128, - "single_support": 64, - "states": 2048, - "width": 7 - }, - { - "G": 3, - "exceptional_word_order": 32, - "pair_support": 256, - "single_support": 128, - "states": 4096, - "width": 8 - }, - { - "G": 4, - "exceptional_word_order": 4, - "pair_support": 64, - "single_support": 32, - "states": 2048, - "width": 6 - }, - { - "G": 4, - "exceptional_word_order": 8, - "pair_support": 128, - "single_support": 64, - "states": 4096, - "width": 7 - }, - { - "G": 4, - "exceptional_word_order": 16, - "pair_support": 256, - "single_support": 128, - "states": 8192, - "width": 8 - }, - { - "G": 4, - "exceptional_word_order": 32, - "pair_support": 512, - "single_support": 256, - "states": 16384, - "width": 9 - } - ], - "exhaustive_states": 40800, - "production_comparisons": 1176, - "scope": "One compact digit, rho=0. General proof is written, not formally checked. Production comparisons are targeted, not exhaustive.", - "seed": 51, - "status": "SCOPED NEGATIVE RESULT; NO NEW KAPPA", - "universal_pair_support": "1/(2*2^G) over z,y,t; 1/2^G conditional on z=1", - "witness": { - "G": 2, - "K": 6, - "b": 2, - "first_y": 40, - "ideal_pair_y": 33, - "second_y": 41, - "t": 3, - "x": 1, - "y": 33 - } -} diff --git a/research/compact-boundary-cancellation-seed51/SOURCES.json b/research/compact-boundary-cancellation-seed51/SOURCES.json deleted file mode 100644 index 5172eabb46..0000000000 --- a/research/compact-boundary-cancellation-seed51/SOURCES.json +++ /dev/null @@ -1,50 +0,0 @@ -{ - "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", - "normalization": "Text CRLF to LF only; no other normalization", - "files": { - "notes/compact-control-movement.tex": { - "lf_sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6", - "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357" - }, - "notes/compact-control-layout.tex": { - "lf_sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87", - "git_blob": "16f4d233471a7d189163ae7e7902becadecbba64" - }, - "scripts/audit_compact_controls.py": { - "lf_sha256": "c3513cd6b41a20bc33b392d66c1536f0a5fcaa76088848361a3aef64074fa989", - "git_blob": "22da5574cb160fafab359a0a41bfe86db5a3bc34" - }, - "scripts/certify.py": { - "lf_sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", - "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a" - }, - "scripts/prepare_layers.py": { - "lf_sha256": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947", - "git_blob": "8e17b52f9573135426d7ba6865c8c9bc8da8639a" - }, - "scripts/search_network.py": { - "lf_sha256": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a", - "git_blob": "f03d5c1b2c81afd6c2f1d3ba9e17d4e7bcd31b9b" - }, - "certificates/selected-result.json": { - "lf_sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3", - "git_blob": "3d7529d77a5f22d8c6f64f98bd5a0e71b8eee892" - }, - "research/community-frontier942-audit/SELECTED-SOURCE.json": { - "lf_sha256": "1cd8dfde15919d1c3df9796b262e67898143d9793d2b86ee7b0a47fc903654c9", - "git_blob": "7bb22cec9e1150f81c2d695c73d9f5fe4c847f84" - }, - "research/community-frontier942-audit/ASSEMBLY.json": { - "lf_sha256": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a", - "git_blob": "9e71e9c1a1c1cbd1979f0c7bac87495322cbfad0" - }, - "research/complex-t37-owners/PROOF.md": { - "lf_sha256": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", - "git_blob": "04bdeda39111678e27e2c4baa3ce5c6e0ac6f64b" - }, - "docs/research/community-batch952-review.md": { - "lf_sha256": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", - "git_blob": "512ce9f18b32007bea71452eb5f3eb85c4d577ad" - } - } -} diff --git a/research/compact-boundary-cancellation-seed51/VALIDATION.json b/research/compact-boundary-cancellation-seed51/VALIDATION.json deleted file mode 100644 index b3b21ee6bf..0000000000 --- a/research/compact-boundary-cancellation-seed51/VALIDATION.json +++ /dev/null @@ -1,35 +0,0 @@ -{ - "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", - "python": "3.12.14 (main, Aug 25 2026, 14:01:42) [MSC v.1944 64 bit (AMD64)]", - "platform": "win32", - "standalone": "PASS states=40800 production=1176 controls=8", - "optimized_standalone": "PASS identical receipt", - "relocated_package": "PASS under -I -O -B; four corruption controls rejected", - "existing_tests": [ - { - "pattern": "test_compact_controls.py", - "passed": 5 - }, - { - "pattern": "test_compact_control_layer.py", - "passed": 7 - }, - { - "pattern": "test_compact_control_patch.py", - "passed": 5 - }, - { - "pattern": "test_selected_result.py", - "passed": 5 - } - ], - "omitted": [ - "Full make verify", - "Selected supplier cold replay", - "Hosted CI", - "Formal theorem proof" - ], - "source_integrity": "All pinned canonical LF SHA256 and Git blob hashes checked; selected assembly digest bound", - "publication": "Local patch only: gh/connector unavailable and no GH_TOKEN/GITHUB_TOKEN in environment", - "patch_checks": "git diff --cached --check; clean base temporary-index git apply --cached --check; reverse application check: PASS" -} diff --git a/research/compact-boundary-cancellation-seed51/test_package.py b/research/compact-boundary-cancellation-seed51/test_package.py deleted file mode 100644 index 3a3c5ada22..0000000000 --- a/research/compact-boundary-cancellation-seed51/test_package.py +++ /dev/null @@ -1,51 +0,0 @@ -"""Relocated replay and four independently injected package faults.""" -import json -from pathlib import Path -import shutil -import subprocess -import sys -import tempfile - -HERE = Path(__file__).resolve().parent -ROOT = HERE.parents[1] -REL = HERE.relative_to(ROOT) - - -def run(root): - return subprocess.run([sys.executable, '-I', '-O', '-B', str(root / REL / 'verify.py')], - cwd=root, capture_output=True, text=True) - - -with tempfile.TemporaryDirectory(prefix='compact-boundary-') as tmp: - dest = Path(tmp) - pins = json.loads((HERE / 'SOURCES.json').read_text()) - for name in pins['files']: - target = dest / name - target.parent.mkdir(parents=True, exist_ok=True) - target.write_bytes((ROOT / name).read_bytes()) - shutil.copytree(HERE, dest / REL, ignore=shutil.ignore_patterns('__pycache__')) - clean = run(dest) - if clean.returncode != 0: - raise RuntimeError(clean.stdout + clean.stderr) - verifier = dest / REL / 'verify.py' - original = verifier.read_text() - source = dest / 'notes/compact-control-movement.tex' - original_source = source.read_bytes() - receipt = dest / REL / 'RESULT.json' - original_receipt = receipt.read_bytes() - faults = [ - ('source drift', source, original_source + b'\nsource drift\n'), - ('receipt drift', receipt, original_receipt.replace(b'40800', b'40801')), - ('formula sign', verifier, original.replace('correction = 2 *', 'correction = -2 *').encode()), - ('repair sign', verifier, original.replace('a - 2 * (1 << G)', 'a + 2 * (1 << G)').encode()), - ] - for name, target, replacement in faults: - before = target.read_bytes() - if replacement == before: - raise RuntimeError('Fault injection did not change bytes: ' + name) - target.write_bytes(replacement) - failed = run(dest) - target.write_bytes(before) - if failed.returncode == 0: - raise RuntimeError('Fault was accepted: ' + name) - print('PASS_COMPACT_BOUNDARY_PACKAGE relocated_isolated_optimized=PASS faults=4') diff --git a/research/compact-boundary-cancellation-seed51/verify.py b/research/compact-boundary-cancellation-seed51/verify.py deleted file mode 100644 index f7eeab9b94..0000000000 --- a/research/compact-boundary-cancellation-seed51/verify.py +++ /dev/null @@ -1,169 +0,0 @@ -#!/usr/bin/env python3 -"""Exact one-digit boundary census. Standard library; Python >= 3.9.""" -import hashlib -import importlib.util -import json -from pathlib import Path -import sys - -HERE = Path(__file__).resolve().parent -ROOT = HERE.parents[1] - - -def require(condition, message): - if not condition: - raise ValueError(message) - - -def literal(y, t, z, G, width, inverse=False): - """Four modular rotations; inversion reverses order and sign.""" - B, Q = 1 << G, 1 << width - if inverse: - t = (t + ((y & 1) ^ z)) % B - y = (y - z * (1 - 2 * t)) % Q - t = (t - (y & 1)) % B - y = (y - 2 * z * t) % Q - else: - y = (y + 2 * z * t) % Q - t = (t + (y & 1)) % B - y = (y + z * (1 - 2 * t)) % Q - t = (t - ((y & 1) ^ z)) % B - return y, t - - -def formula(y, t, z, G, width): - """Independent parity partition, derived in README.md.""" - correction = 2 * (1 << G) if z and (y & 1) and t == (1 << G) - 1 else 0 - return ((y ^ z) + correction) % (1 << width), t - - -def repaired_pair(y, t, z, G, width): - a, b = literal(y, t, z, G, width) - a, b = literal(a, b, z, G, width) - if z and b == (1 << G) - 1: - a = (a - 2 * (1 << G)) % (1 << width) - return a, b - - -def source_pins(): - pins = json.loads((HERE / 'SOURCES.json').read_text()) - for name, pin in pins['files'].items(): - data = (ROOT / name).read_bytes().replace(b'\r\n', b'\n') - require(hashlib.sha256(data).hexdigest() == pin['lf_sha256'], 'Source drift: ' + name) - blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() - require(blob == pin['git_blob'], 'Git blob mismatch: ' + name) - selected = json.loads((ROOT / 'certificates/selected-result.json').read_text()) - require(selected['kappa'] == '1661960547713947/1000000000000000000', 'Selected kappa changed') - for key in ('certificate', 'source_manifest', 'proof', 'review'): - require(selected[key] in pins['files'], 'Unpinned selected chain: ' + key) - require(pins['files'][selected['certificate']]['lf_sha256'] == selected['certificate_sha256'], - 'Selected assembly binding failed') - return pins['base_commit'] - - -def census(): - total = 0 - rows = [] - # All y,t,z in these 16 complete one-digit rectangles, not random samples. - for G in range(1, 5): - for width in range(G + 2, G + 6): - B, Q = 1 << G, 1 << width - disagreements = pair_support = 0 - images = set() - for z in (0, 1): - images.clear() - for t in range(B): - for y in range(Q): - out = literal(y, t, z, G, width) - require(out == formula(y, t, z, G, width), 'Parity formula') - require(literal(*out, z, G, width, inverse=True) == (y, t), 'Literal inverse') - images.add(out) - disagreements += out != (y ^ z, t) - pair = literal(*out, z, G, width) - expected = ((y + (2 * B if z and t == B - 1 else 0)) % Q, t) - require(pair == expected, 'Boundary translation') - pair_support += pair != (y, t) - require(repaired_pair(y, t, z, G, width) == (y, t), 'Pair repair') - total += 1 - require(len(images) == Q * B, 'Full permutation coverage') - require(disagreements == Q // 2, 'Single-word support cardinality') - require(pair_support == Q, 'Pair support cardinality') - # The exceptional z=1 fibre is one cycle of exact length Q/B. - y, t = 1, B - 1 - order = Q // B - for step in range(1, order + 1): - y, t = literal(y, t, 1, G, width) - require(((y, t) == (1, B - 1)) == (step == order), 'Exact fibre order') - rows.append(dict(G=G, width=width, states=2 * Q * B, - single_support=disagreements, pair_support=pair_support, - exceptional_word_order=order)) - return total, rows - - -def production_comparison(): - # The retained implementation contains actual front/back swaps and full - # two-slot target widths; it is not used by the independent census above. - sys.path.insert(0, str(ROOT / 'scripts')) - spec = importlib.util.spec_from_file_location('retained_compact', ROOT / 'scripts/audit_compact_controls.py') - module = importlib.util.module_from_spec(spec) - spec.loader.exec_module(module) - count = 0 - for G, K in ((1, 4), (2, 6), (3, 8)): - B, Q = 1 << G, 1 << (2 * K) - for y in sorted({0, 1, 2, Q - 1, 4 * B, 4 * B + 1, Q - 4 * B - 1}): - for t in range(B): - for z in (0, 1): - for b in range(B): - old = dict(x=z, y=y, t=t, b=b) - out = module.execute(old, 1, K, 0, G) - wanted_y, wanted_t = literal(y, t, z, G, 2 * K) - require(out == dict(old, y=wanted_y, t=wanted_t), 'Retained primitive disagreement') - twice = module.execute(out, 1, K, 0, G) - require(twice == dict(old, y=(y + (2 * B if z and t == B - 1 else 0)) % Q), 'Retained boundary') - fixed = module.repaired(module.repaired(old, 1, K, 0, G), 1, K, 0, G) - require(fixed == old, 'Retained completed cancellation') - count += 1 - return count - - -def negative_controls(): - G, width, y, t, z = 2, 12, 33, 3, 1 - a = literal(y, t, z, G, width) - b = literal(*a, z, G, width) - checks = { - 'raw_word_is_not_ideal': a != (y ^ z, t), - 'raw_pair_is_not_identity': b != (y, t), - 'raw_forward_is_not_inverse': literal(*a, z, G, width) != (y, t), - 'omitting_saturation_test_fails': b != (y, t), - 'wrong_repair_sign_fails': ((b[0] + 8) % (1 << width), b[1]) != (y, t), - 'single_word_half_density_is_not_pair_density': (1 << (width - 1)) != (1 << width), - 'restored_temporary_does_not_imply_identity': b[1] == t and b[0] != y, - 'safe_target_guard_does_not_replace_digit_guard': 8 <= (y >> 1) < 32 - 8 and b != (y, t), - } - for name, value in checks.items(): - require(value, 'Failed rejection control: ' + name) - require(repaired_pair(y, t, z, G, width) == (y, t), 'Correct repair control') - require(literal(*a, z, G, width, inverse=True) == (y, t), 'Correct inverse control') - return sorted(checks) - - -def result(): - base = source_pins() - total, rows = census() - return dict(status='SCOPED NEGATIVE RESULT; NO NEW KAPPA', base_commit=base, - seed=51, exhaustive_states=total, domains=rows, - production_comparisons=production_comparison(), - controls=negative_controls(), witness=dict(G=2, K=6, x=1, y=33, t=3, b=2, - first_y=40, second_y=41, ideal_pair_y=33), - universal_pair_support='1/(2*2^G) over z,y,t; 1/2^G conditional on z=1', - scope='One compact digit, rho=0. General proof is written, not formally checked. Production comparisons are targeted, not exhaustive.') - - -if __name__ == '__main__': - receipt = result() - if '--write' in sys.argv: - (HERE / 'RESULT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n', encoding='utf-8') - else: - require(receipt == json.loads((HERE / 'RESULT.json').read_text()), 'Receipt mismatch') - print('PASS_COMPACT_BOUNDARY_CANCELLATION states=%d production=%d controls=%d no_new_kappa' % - (receipt['exhaustive_states'], receipt['production_comparisons'], len(receipt['controls']))) diff --git a/research/frontier1042-capsule-closure-seed75/CLAIM.md b/research/frontier1042-capsule-closure-seed75/CLAIM.md index 3b0344d474..1f94dcde81 100644 --- a/research/frontier1042-capsule-closure-seed75/CLAIM.md +++ b/research/frontier1042-capsule-closure-seed75/CLAIM.md @@ -4,7 +4,7 @@ - Exact base: `ba82555c64e1879e4b7decce28186f208fcb8262`. - Chosen object: closed, path-safe audit of the selected PR1042 replay capsule. - Method: standard-library tar/SHA-256 checker; no extraction or construction imports. -- Deliverable: verifier, deterministic receipt, six controls, exact pins and scope note; no new kappa. -- Stopping rule: all members and declared edges checked, all controls reject, optimized run agrees, selected-record checks pass. +- Deliverable: verifier, deterministic receipt, six integrity controls and three historical-record regression controls, exact pins and scope note; no new kappa. +- Stopping rule: all members and declared edges checked, all integrity controls reject, optimized run agrees, historical selected-record pins pass. Live selected-pointer validation remains separate. Candidates considered were invoice/outer arithmetic (overlapped PR1112), T16 owner/profile checking (overlapped prior audits), and capsule closure (chosen as distinct publication-evidence coverage). No pinned sprint coordination issue was found. diff --git a/research/frontier1042-capsule-closure-seed75/NOTICE.md b/research/frontier1042-capsule-closure-seed75/NOTICE.md index 9ef73ad282..77cf8befd4 100644 --- a/research/frontier1042-capsule-closure-seed75/NOTICE.md +++ b/research/frontier1042-capsule-closure-seed75/NOTICE.md @@ -1,2 +1,3 @@ New material: Copyright 2026 Martin Rv. Apache-2.0. Prepared with substantial Perplexity AI assistance. PR1042/batch1047 construction, review and predecessor attribution remain with their original contributors and notices. +The historical-record portability fix, reproduction target, and regression controls were prepared with OpenAI Codex assistance. diff --git a/research/frontier1042-capsule-closure-seed75/PINS.json b/research/frontier1042-capsule-closure-seed75/PINS.json index 18c7db8ec3..1642ed9645 100644 --- a/research/frontier1042-capsule-closure-seed75/PINS.json +++ b/research/frontier1042-capsule-closure-seed75/PINS.json @@ -6,7 +6,7 @@ "kappa": "1672188119205421/1000000000000000000", "decimal": "0.001672188119205421", "archive": {"path": "research/community-frontier1042-audit/selected-replay.tar.gz", "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", "members": 458, "declared_artifacts": 457, "expanded_bytes": 45647427}, - "selected_record": {"path": "certificates/selected-result.json", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7"}, + "selected_record": {"path": "SELECTED-RESULT.json", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7", "source_path": "certificates/selected-result.json", "source_commit": "ba82555c64e1879e4b7decce28186f208fcb8262"}, "integration_record": {"path": "docs/research/community-batch1047-integration.json", "sha256": "b04623d39df453804f327a203f07882554b138e6b322b9d1f674d84d94a14a8c"}, "promoted_receipts": {"ASSEMBLY.json": "t16/ASSEMBLY.json", "BASELINE-BINDING.json": "BASELINE-BINDING.json", "INDEPENDENT-T16.json": "t16/INDEPENDENT-T16.json", "RESULT.json": "RESULT.json", "STAGES.json": "STAGES.json", "T16-REPLAY.json": "t16/REPLAY.json"}, "stages": ["leaver-manifest", "slots-manifest", "t16-manifest", "base", "cells", "chain", "independent-leaver", "leaver-global", "slots", "t16"] diff --git a/research/frontier1042-capsule-closure-seed75/PROOF.md b/research/frontier1042-capsule-closure-seed75/PROOF.md index 1866e5dbce..b4642fa493 100644 --- a/research/frontier1042-capsule-closure-seed75/PROOF.md +++ b/research/frontier1042-capsule-closure-seed75/PROOF.md @@ -6,6 +6,6 @@ Let `A` be the byte-pinned selected replay archive and `R` its archived `RESULT. 2. `R.artifacts` equals `members(A) - {RESULT.json}` and every declared SHA-256 equals bytes read from `A`. The separately pinned archive digest binds the self-excluded result too. 3. `STAGES.json` equals `R.stages`; the ten fixed names, zero exit codes and log digests are checked. 4. Six promoted public receipts equal their archived bytes. -5. Exact selected and integration record pins bind the value, source head, certificate, source manifest, archive and promoted receipts. +5. Exact frozen historical selected and integration record pins bind the value, source head, certificate, source manifest, archive and promoted receipts. The selected record is package-local data copied byte-for-byte from the pinned base; the live selected pointer is outside this historical audit. Therefore all 458 capsule bytes and stated publication edges are authenticated relative to `PINS.json`. This says nothing about execution history or the inherited multiplication theorem assumptions. diff --git a/research/frontier1042-capsule-closure-seed75/README.md b/research/frontier1042-capsule-closure-seed75/README.md index 3872c61ede..f58f2ee652 100644 --- a/research/frontier1042-capsule-closure-seed75/README.md +++ b/research/frontier1042-capsule-closure-seed75/README.md @@ -8,18 +8,33 @@ This package independently checks the frozen publication capsule behind selected `verify.py` treats `research/community-frontier1042-audit/selected-replay.tar.gz` as untrusted data, uses only the Python standard library, never extracts a member, and imports no construction code. It authenticates 458 safe regular members (45,647,427 expanded bytes), all 457 declared artifact digests, exact inventory closure, ten successful stage/log bindings, six promoted receipts, and the selected/integration publication pins. +`SELECTED-RESULT.json` is the byte-for-byte historical `certificates/selected-result.json` from base `ba82555c64e1879e4b7decce28186f208fcb8262`, also retained at `certificates/checkpoints/frontier1042.json`. Its original SHA-256, `207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7`, remains pinned in `PINS.json`. The checker reads this package-local snapshot. It does not read the live `certificates/selected-result.json`, so later selected frontiers do not invalidate this historical audit. + ## Reproduce ```sh make frontier1042-capsule-closure-verify ``` -Expected final markers: `PASS_FRONTIER1042_CAPSULE_CLOSURE`, six tests, `OK`. The target also runs under optimized Python so checks cannot depend on removable assertions. +Expected final markers: `PASS_FRONTIER1042_CAPSULE_CLOSURE`, nine tests, `OK`. The target compares both normal and optimized verifier receipts byte-for-byte with the committed `RESULT.json`, then runs the suite in both modes so checks cannot depend on removable assertions. + +The same checks can be run directly with Python 3.9+: + +```sh +python3 -B research/frontier1042-capsule-closure-seed75/verify.py --check +python3 -O -B research/frontier1042-capsule-closure-seed75/verify.py --check +python3 -B research/frontier1042-capsule-closure-seed75/test_package.py +python3 -O -B research/frontier1042-capsule-closure-seed75/test_package.py +``` + +Current selected-pointer validation remains the separate `make selected-record-check` target. It is not a prerequisite of the historical capsule target. ## Controls The suite rejects path traversal, duplicate members, undeclared members, mutated artifact bytes, a nonzero stage, and a promoted-receipt mismatch. +Regression controls run the complete checker in an isolated fixture: it must pass with the live selected pointer absent or advanced to a later frontier, and reject mutated bytes in the frozen selected record. The original `RESULT.json` is unchanged. + ## Scope This is finite integrity and binding evidence about the committed capsule. It does not establish that recorded commands ran, independently recompute T16 mathematics, verify named source packages, discharge inherited interfaces, prove analytic transfer, benchmark multiplication, or formalize the full theorem. @@ -27,3 +42,5 @@ This is finite integrity and binding evidence about the committed capsule. It do ## Attribution Martin Rv (@martinxxx9), with substantial Perplexity AI assistance in research, implementation, verification and writing. It preserves all PR1042 and batch1047 predecessor attribution. Apache-2.0. + +The historical-record portability fix, reproduction target, and regression controls were prepared with OpenAI Codex assistance in response to the maintainer review. diff --git a/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json b/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json new file mode 100644 index 0000000000..f451ced662 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json @@ -0,0 +1,194 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1672188119205421/1000000000000000000", + "decimal": "0.001672188119205421", + "source_prs": [ + 1042, + 1031, + 1028, + 1022, + 1018, + 1005, + 1004, + 987, + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1042-audit/ASSEMBLY.json", + "certificate_sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e", + "proof": "docs/research/community-batch1047-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026", + "docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787", + "scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854" + }, + "review": "docs/research/community-batch1047-review.md", + "validation": "docs/research/community-batch1047-integration.json", + "reproduce": "make frontier1042-verify", + "scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.", + "previous_kappa": "1661960547713947/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier942.json", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903", + "1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f", + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef", + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d" + } +} diff --git a/research/frontier1042-capsule-closure-seed75/test_package.py b/research/frontier1042-capsule-closure-seed75/test_package.py index 6f66740230..6ece284177 100644 --- a/research/frontier1042-capsule-closure-seed75/test_package.py +++ b/research/frontier1042-capsule-closure-seed75/test_package.py @@ -2,9 +2,12 @@ # SPDX-License-Identifier: Apache-2.0 import copy from pathlib import Path +import shutil import sys import tarfile +import tempfile import unittest +from unittest.mock import patch sys.path.insert(0, str(Path(__file__).resolve().parent)) import verify @@ -44,7 +47,54 @@ def test_C5_nonzero_stage(self): result = copy.deepcopy(self.result); result["stages"] = stages with self.assertRaisesRegex(ValueError, "recorded stage failed"): self.validate(result=result, stages=stages) def test_C6_promoted_receipt_mismatch(self): - outer = verify.repository_file("research/community-frontier1042-audit/ASSEMBLY.json") - self.assertNotEqual(outer + b"x", self.roots["t16/ASSEMBLY.json"]) + original = verify.repository_file + def mismatched_receipt(relative, expected=None): + data = original(relative, expected) + return data + b"x" if relative == "research/community-frontier1042-audit/ASSEMBLY.json" else data + with patch.object(verify, "repository_file", side_effect=mismatched_receipt): + with self.assertRaisesRegex(ValueError, "promoted receipt differs from capsule"): + verify.check(self.pins) + +class HistoricalSelectedControls(unittest.TestCase): + def setUp(self): + self.pins = verify.strict_json((verify.HERE / "PINS.json").read_bytes(), "PINS.json") + self.expected = verify.strict_json((verify.HERE / "RESULT.json").read_bytes(), "RESULT.json") + self.temporary = tempfile.TemporaryDirectory() + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) + self.package = self.root / "research" / verify.HERE.name + self.package.mkdir(parents=True) + shutil.copyfile(verify.HERE / self.pins["selected_record"]["path"], + self.package / self.pins["selected_record"]["path"]) + paths = [self.pins["archive"]["path"], self.pins["integration_record"]["path"]] + paths.extend("research/community-frontier1042-audit/" + name + for name in self.pins["promoted_receipts"]) + selected = verify.strict_json(verify.package_file(self.pins["selected_record"]["path"], + self.pins["selected_record"]["sha256"]), "selected") + paths.append(selected["source_manifest"]) + for relative in paths: + target = self.root / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / relative, target) + for name, value in (("ROOT", self.root), ("HERE", self.package)): + patcher = patch.object(verify, name, value) + patcher.start() + self.addCleanup(patcher.stop) + + def test_missing_live_selected_pointer_does_not_affect_history(self): + self.assertFalse((self.root / "certificates/selected-result.json").exists()) + self.assertEqual(verify.check(self.pins), self.expected) + + def test_advanced_live_selected_pointer_does_not_affect_history(self): + live = self.root / "certificates/selected-result.json" + live.parent.mkdir(parents=True) + live.write_text('{"kappa": "1672660197076918/1000000000000000000"}\n', encoding="utf-8") + self.assertEqual(verify.check(self.pins), self.expected) + + def test_mutated_frozen_selected_record_is_rejected(self): + frozen = self.package / self.pins["selected_record"]["path"] + frozen.write_bytes(frozen.read_bytes() + b"x") + with self.assertRaisesRegex(ValueError, "package pin differs: SELECTED-RESULT.json"): + verify.check(self.pins) if __name__ == "__main__": unittest.main(verbosity=2) diff --git a/research/frontier1042-capsule-closure-seed75/verify.py b/research/frontier1042-capsule-closure-seed75/verify.py index 1676d89098..3ab556e1b3 100644 --- a/research/frontier1042-capsule-closure-seed75/verify.py +++ b/research/frontier1042-capsule-closure-seed75/verify.py @@ -117,6 +117,15 @@ def repository_file(relative, expected=None): require(digest(data) == expected, "repository pin differs: " + relative) return data +def package_file(relative, expected): + require(type(relative) is str, "invalid package path") + path = (HERE / relative).resolve() + require(path.is_relative_to(HERE.resolve()) and path.is_file(), + "missing package file: " + relative) + data = path.read_bytes() + require(digest(data) == expected, "package pin differs: " + relative) + return data + def check(pins): require(pins.get("schema") == "integer-mult-frontier1042-capsule-closure-v1", "unsupported pins schema") @@ -137,7 +146,7 @@ def check(pins): require(outer_data == roots[inner], "promoted receipt differs from capsule: " + outer) promoted_hashes[outer] = digest(outer_data) selected_pin = pins["selected_record"] - selected = strict_json(repository_file(selected_pin["path"], selected_pin["sha256"]), selected_pin["path"]) + selected = strict_json(package_file(selected_pin["path"], selected_pin["sha256"]), selected_pin["path"]) require(selected.get("audited_source_head") == pins["audited_source_head"], "audited source head differs") require(selected.get("kappa") == pins["kappa"] and selected.get("decimal") == pins["decimal"], "published selected value differs") @@ -175,10 +184,14 @@ def check(pins): def main(): ap = argparse.ArgumentParser() ap.add_argument("--out", type=Path) + ap.add_argument("--check", action="store_true", + help="require byte equality with the committed RESULT.json") args = ap.parse_args() pins = strict_json((HERE / "PINS.json").read_bytes(), "PINS.json") receipt = check(pins) raw = (json.dumps(receipt, indent=2) + "\n").encode() + if args.check: + require(raw == (HERE / "RESULT.json").read_bytes(), "committed receipt differs") if args.out: args.out.write_bytes(raw) print(raw.decode(), end="")