From b465e509063e56e63aede8e2057761851cb68cbd Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:32:44 +0530 Subject: [PATCH 1/2] Verify selected JP8 scalar endpoints by exact adjoint replay --- research/jp8-adjoint-restoration/CLAIM.md | 15 + .../jp8-adjoint-restoration/EXPECTED.json | 313 ++++++++++++++++++ research/jp8-adjoint-restoration/README.md | 210 ++++++++++++ research/jp8-adjoint-restoration/SOURCES.json | 22 ++ .../jp8-adjoint-restoration/VALIDATION.json | 106 ++++++ research/jp8-adjoint-restoration/verify.py | 265 +++++++++++++++ 6 files changed, 931 insertions(+) create mode 100644 research/jp8-adjoint-restoration/CLAIM.md create mode 100644 research/jp8-adjoint-restoration/EXPECTED.json create mode 100644 research/jp8-adjoint-restoration/README.md create mode 100644 research/jp8-adjoint-restoration/SOURCES.json create mode 100644 research/jp8-adjoint-restoration/VALIDATION.json create mode 100644 research/jp8-adjoint-restoration/verify.py diff --git a/research/jp8-adjoint-restoration/CLAIM.md b/research/jp8-adjoint-restoration/CLAIM.md new file mode 100644 index 0000000000..c71024e02d --- /dev/null +++ b/research/jp8-adjoint-restoration/CLAIM.md @@ -0,0 +1,15 @@ +# Sprint claim + +- Track: independent verification or formalization. OS assignment seed: **79**, drawn with Python `secrets.randbelow(100)` on 2026-10-13. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Object: the selected #626 JP8 emitted scalar programs, including target preconditioning, dirty-helper compensation, early cleanup, full cleanup, and private-centre clear/copy operations. Seed 79 chooses index `79 % 2 = 1` in the sorted selected supplier list `[ck, jp8]`. +- Method: independently written exact reverse-mode pullback of every output coordinate in both orientations. No constructor or production replay imports. Mutate compensation, cleanup, copy and clear operations to obtain exact counterexamples. +- Deliverable: one standalone Python verifier, pinned input/certificate data, a scoped mathematical explanation, and validation evidence. No new kappa claim. +- Started: 2026-10-13 04:46 UTC. Expected finish: 2026-10-13 05:26 UTC. Reserve 05:16–05:26 UTC for verification and handoff. +- Coordination: GitHub's pinned-issue query returned no issues. Claim is local as requested; no reservation issue was opened. Open PR metadata was checked through #720 before claiming. + +Three candidates were considered: the raw K-triangle read identity, cold-wrapper amplitudes, and the emitted dirty-input restoration identity. #646/#683/#687 cover K-triangle schedules; #702/#712 cover wrapper amplitudes. The chosen check uses a different execution direction from the selected forward state-map replays and includes arbitrary initial private-centre coordinates. #692 concerns weighted-stride structural closures and bilinear duality, not these concrete JP8 programs. Existing source and review attribution will be retained. + +Scope is confined to this directory. The construction, selected frontier, `upstream/`, physical frame/wrapper semantics, recursion, cost model, and global assembly remain unchanged. Acceptance requires all output-coordinate identities in both orientations, meaningful rejected semantic mutations, source binding, and a reproducible offline command. This is a finite scalar verification, not a formal proof of the multiplication theorem. + +Prepared for Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex assistance. diff --git a/research/jp8-adjoint-restoration/EXPECTED.json b/research/jp8-adjoint-restoration/EXPECTED.json new file mode 100644 index 0000000000..1fc30efe69 --- /dev/null +++ b/research/jp8-adjoint-restoration/EXPECTED.json @@ -0,0 +1,313 @@ +{ + "checks": { + "backward": { + "input_coordinates": 724, + "nonzero_matrix_entries": 828, + "operation_counts": { + "add": 22219, + "clear": 16, + "scale": 458 + }, + "output_coordinates_checked": 724, + "output_covectors_sha256": "7aea79a488659cb6e814a688b5d6db5ac6e1c30dfd9484d0c906903f6333cd65", + "persistent_outputs": 716, + "private_outputs": 8, + "scalar_operations": 22693 + }, + "forward": { + "input_coordinates": 724, + "nonzero_matrix_entries": 828, + "operation_counts": { + "add": 22211, + "clear": 16, + "copy": 8, + "scale": 458 + }, + "output_coordinates_checked": 724, + "output_covectors_sha256": "5e8888bf5824130caf079705289c24f23419aa6ed7f9543653ee7c95bbe0f8e7", + "persistent_outputs": 716, + "private_outputs": 8, + "scalar_operations": 22693 + } + }, + "dirty_centre_gap": { + "all_716_L_input_columns_unchanged": true, + "all_private_outputs_zero": true, + "defect_rank": 1, + "event_index": 13113, + "input_coordinate": [ + "C", + 0 + ], + "nonzero_output_coefficients": [ + [0, "-1"], + [2, "-1"], + [7, "-1"], + [9, "-1"], + [10, "-1"], + [11, "-1"], + [12, "-1"], + [17, "-1"], + [18, "-1"], + [19, "-1"], + [22, "-1"], + [23, "-1"], + [24, "-1"], + [25, "-1"], + [27, "-1"], + [31, "-1"], + [32, "-1"], + [33, "-1"], + [34, "-1"], + [35, "-1"], + [38, "-1"], + [39, "-1"], + [40, "-1"], + [45, "-1"], + [48, "-1"], + [49, "-1"], + [50, "-1"], + [54, "-1"], + [55, "-1"], + [56, "-1"], + [57, "-1"], + [61, "-1"], + [62, "-1"], + [63, "-1"], + [70, "-1"], + [71, "-1"], + [72, "-1"], + [76, "-1"], + [77, "-1"], + [79, "-1"], + [81, "-1"], + [85, "-1"], + [87, "-1"], + [89, "-1"], + [90, "-1"], + [91, "-1"], + [92, "-1"], + [94, "-1"], + [98, "-1"], + [100, "-1"], + [101, "-1"], + [102, "-1"], + [103, "-1"], + [107, "-1"], + [108, "-1"], + [109, "-1"], + [224, "-1"], + [225, "1"], + [226, "-2"], + [228, "-1"], + [229, "-1"], + [231, "1"], + [238, "-1"], + [240, "-1"], + [241, "-1"], + [243, "-2"], + [244, "-1"], + [245, "-1"], + [247, "1"], + [254, "-1"], + [256, "-1"], + [257, "-1"], + [259, "-2"], + [260, "-1"], + [261, "-1"], + [263, "1"], + [270, "-1"], + [272, "-1"], + [273, "-1"], + [275, "1"], + [276, "-1"], + [283, "-2"], + [285, "-1"], + [286, "-1"], + [287, "-2"], + [288, "-1"], + [289, "-1"], + [291, "1"], + [292, "-1"], + [299, "-2"], + [301, "-1"], + [302, "-1"], + [303, "-2"], + [304, "-1"], + [305, "-1"], + [307, "1"], + [308, "-1"], + [315, "-2"], + [317, "-1"], + [318, "-1"], + [319, "-2"], + [320, "-1"], + [322, "-1"], + [323, "-1"], + [331, "-1"], + [334, "-1"], + [335, "-1"] + ] + }, + "omission_witnesses": { + "backward_initial_centre_clear": { + "actual": "-1", + "direction": "backward", + "event_index": 13113, + "expected": "0", + "input_basis_coordinate": [ + "C", + 0 + ], + "operation": [ + "clear", + [ + "C", + 0 + ], + null, + "1" + ], + "output_coordinate": [ + "L", + 0 + ], + "phase": "centers" + }, + "forward_centre_copy": { + "actual": "3/4", + "direction": "forward", + "event_index": 13114, + "expected": "1", + "input_basis_coordinate": [ + "L", + 0 + ], + "operation": [ + "copy", + [ + "C", + 0 + ], + [ + "L", + 229 + ], + "1" + ], + "output_coordinate": [ + "L", + 112 + ], + "phase": "centers" + }, + "forward_compensation": { + "actual": "-1", + "direction": "forward", + "event_index": 169, + "expected": "0", + "input_basis_coordinate": [ + "L", + 224 + ], + "operation": [ + "add", + [ + "L", + 118 + ], + [ + "L", + 224 + ], + "1" + ], + "output_coordinate": [ + "L", + 113 + ], + "phase": "zero_frame_precondition" + }, + "forward_early_cleanup": { + "actual": "1", + "direction": "forward", + "event_index": 17243, + "expected": "0", + "input_basis_coordinate": [ + "L", + 0 + ], + "operation": [ + "add", + [ + "L", + 448 + ], + [ + "L", + 76 + ], + "-1" + ], + "output_coordinate": [ + "L", + 448 + ], + "phase": "cleanup_tail" + }, + "forward_final_centre_clear": { + "actual": "1", + "direction": "forward", + "event_index": 13144, + "expected": "0", + "input_basis_coordinate": [ + "L", + 0 + ], + "operation": [ + "clear", + [ + "C", + 0 + ], + null, + "1" + ], + "output_coordinate": [ + "C", + 0 + ], + "phase": "centers" + }, + "forward_full_cleanup": { + "actual": "-1/4", + "direction": "forward", + "event_index": 18676, + "expected": "0", + "input_basis_coordinate": [ + "L", + 8 + ], + "operation": [ + "add", + [ + "L", + 489 + ], + [ + "L", + 561 + ], + "-1" + ], + "output_coordinate": [ + "L", + 489 + ], + "phase": "full_frame_cleanup" + } + }, + "scope": "Exact finite scalar projection; frames, wrappers, costs and all-size interfaces are inherited.", + "status": "PASS_JP8_ADJOINT_RESTORATION", + "supplier": "jp8" +} diff --git a/research/jp8-adjoint-restoration/README.md b/research/jp8-adjoint-restoration/README.md new file mode 100644 index 0000000000..bffabf6318 --- /dev/null +++ b/research/jp8-adjoint-restoration/README.md @@ -0,0 +1,210 @@ +# Independent JP8 scalar restoration check + +The selected #626 JP8 scalar programs have the expected endpoint maps on all +716 persistent registers and eight arbitrary incoming private-centre registers. +A new exact reverse-mode checker verifies every output coordinate in both +orientations, using only Python's standard library. It imports no constructor, +production auditor, or finite-field helper. + +There is a concrete coverage difference. Removing backward event **13113**, the +initial `C0` clear, preserves every ordinary input column and leaves all private +outputs zero. It nevertheless sends an incoming `C0=1` to **107 nonzero persistent +outputs**, including `L0=-1` and `L224=-1`. The certificate records the entire +rank-one defect. The original program passes the stronger check. + +Status: **independent finite verification**, with no new kappa claim. At the exact +base `66849e1475c930fd7732b1a0067ffee7e1e95f60`, the selected conditional witness is +`51110230636731/31250000000000000 = 0.001635527380375392`, #626 with #543. + +## Reproduce + +From the repository root, with Python 3.11 or later: + +```sh +python3 -I -B research/jp8-adjoint-restoration/verify.py +``` + +Expected final line: + +```text +PASS_JP8_ADJOINT_RESTORATION outputs=724x2 inputs=724 controls=6 kappa=unchanged +``` + +`--report` prints the recomputed certificate after comparing every field with +[EXPECTED.json](EXPECTED.json). The command is offline, writes no outputs, and +works with `-O`. It takes about four seconds on the recorded macOS environment. +[VALIDATION.json](VALIDATION.json) records the measured checks, not a benchmark +claim or a Linux CI result. + +[SOURCES.json](SOURCES.json) pins the selected record, its source inventory, the +actual #626 SPEC, and the predecessor checker and emitter. The verifier follows +the selected record to its inventory, checks that inventory's SPEC hash, and +checks the SPEC's whole-artifact and per-orientation program hashes. The two +gzip inputs use decompressed payload hashes, so changing gzip timestamps or +compression streams does not change mathematical equality. No receipt's PASS +field is taken as evidence for the new endpoint calculation. + +## Statement and method + +Write the persistent input as `x,y,h`, with 112 sources, 112 targets, and 492 +helpers. Write the eight private-centre inputs as `c`. The scalar projections +of the literal emitted programs satisfy + +```text +forward: (x, y, h, c) -> (x, y+x, h, 0) +backward: (x, y, h, c) -> (x-y, y, h, 0). +``` + +Every coordinate is arbitrary. In particular, all 492 helper values are +restored and all outputs are independent of incoming `c`. + +For a scalar operation matrix `A` and an output functional `w`, substituting +the operation into the functional gives `A^T w`. If the forward program is +`A_m ... A_1`, processing operations in reverse order computes +`A_1^T ... A_m^T w`. Starting with every output basis functional therefore +computes every row of the complete program matrix. Clear and copy are handled +by substitution; they are not assumed invertible. + +| Literal operation | Pullback of the functional coefficients | +|---|---| +| `target += q * source` | `w[source] += q * w[target]` | +| `target *= q` | `w[target] *= q` | +| `target = source` | Transfer `w[target]` to `w[source]`, then remove `w[target]` | +| `target = 0` | Remove `w[target]` | + +The parser rejects same-register add/copy operations, unknown scalar operations, +invalid register indices, zero denominators, and primitives outside the pinned +dyadic contract. Exact `Fraction` arithmetic prevents rounding or tolerance +acceptance. Both orientations have 22,693 scalar operations. The checker proves +1,448 output-functional equalities, each on 724 possible input coordinates. +The resulting matrices each have 828 nonzero entries. + +The implementation differs from the predecessor `hpe_emit_local.check_local` +and `hpe_audit_local.local`: those propagate all live input rows forward through +the stream. This checker propagates one output functional at a time backward. +It also includes incoming `C` coordinates, whereas the predecessor scalar +endpoint routines initialize only `L` coordinates. A small fixed algebra check +covers all four operation types. Each reported omission witness is separately +executed as a scalar basis-vector input in forward time, for both the intact +and damaged streams. + +## Exact negative controls + +All event indices below are zero-based indices in the pinned emitted event +arrays, including nonscalar events. Delete exactly the named event and set only +the indicated input coordinate to one. + +| Omission | Direction / event | Input | Observed output | Required value | +|---|---|---|---|---:| +| First compensation addition | forward / 169 | `L224` | `L113 = -1` | 0 | +| First early cleanup addition | forward / 17243 | `L0` | `L448 = 1` | 0 | +| First full cleanup addition | forward / 18676 | `L8` | `L489 = -1/4` | 0 | +| First centre copy | forward / 13114 | `L0` | `L112 = 3/4` | 1 | +| Final `C0` clear | forward / 13144 | `L0` | `C0 = 1` | 0 | +| Initial `C0` clear | backward / 13113 | `C0` | `L0 = -1` | 0 | + +For the last control, the checker does more than find one witness. It recomputes +all 724 output rows and verifies the exact formula + +```text +damaged_program - intact_program = d * e_C0^T, +``` + +where `d` is the complete 107-entry vector in +`EXPECTED.json:dirty_centre_gap.nonzero_output_coefficients`. All entries outside +those persistent output rows are zero. This certifies that the damaged and +intact programs agree on **all 716 ordinary input columns**, not merely on one +test input. They also both clear their private outputs. An endpoint test with +private inputs fixed to zero cannot detect this omission. A separately executed +call to the pinned predecessor's `local()` routine confirms acceptance of that +restricted endpoint test; see the validation record. + +This does not show that full production admission accepts the damaged artifact. +Its source hashes and event-order checks are separate obligations. Nor does it +show a violated predecessor promise about dirty private inputs. The new result +states the stronger scalar property and makes the distinction reproducible. + +To reproduce the predecessor comparison from the repository root, run this +separate command **without `-O`**, so the predecessor's assertions remain active: + +```sh +python3 -B - <<'PY' +import copy +import hashlib +import json +import sys +from pathlib import Path + +if sys.flags.optimize: + raise RuntimeError('Predecessor assertions must be enabled') +source = Path('research/complex-k492-owner-repair/code/hpe_audit_local.py') +provider = Path('research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8') +pins = json.loads(Path('research/jp8-adjoint-restoration/SOURCES.json').read_text()) +if hashlib.sha256(source.read_bytes()).hexdigest() != pins['files_sha256'][str(source)]: + raise RuntimeError('Changed predecessor source') +sys.argv = [str(source), str(provider)] +namespace = {'__name__': 'predecessor_comparison'} +# This unique boundary excludes the reporting and output-writing driver. +prefix, _ = source.read_text().split('profiles={};checks={}') +exec(compile(prefix, str(source), 'exec'), namespace) +events = copy.deepcopy(namespace['ir']['local_programs']['backward']) +if events[13113] != ['scalar', ['clear', ['C', 0]], 0]: + raise RuntimeError('Changed event position') +del events[13113] +_, result = namespace['local'](events, True) +print(result['all_exact_columns'], result['private_work_erased']) +PY +``` + +Expected: `716 True`. This calls only the historical local routine on an +in-memory mutation, not its full admission driver. It writes no source files +or receipts. The primary verifier above independently establishes the whole +restricted-map equality without executing the predecessor. + +## Scope, provenance, and limits + +This is a complete exact check of the two fixed finite scalar projections. It +is not a sampled search, a formal proof-assistant development, or a proof of the +full integer multiplication theorem. No construction search was run. Seed 79 +selects JP8 from the two selected suppliers; it does not determine randomized +test inputs. Coverage ends after all output rows, six specified omissions, and +the complete one-clear defect are checked. + +Frame changes, centre transport, and ordinary/residual adapters are recognized +metadata events and are excluded from the scalar map. Their geometric and +operator semantics are inherited. The check does not rerun wrapper amplitudes, +all-size compilation, common-label or mutable-basis realization, whole-call +hosting, coefficient-work implementation, prefix bounds, costs, moments, +precision/tape/recovery, analytic transfer, or outer assembly. Arbitrary scalar +centre inputs do not by themselves prove a dirty physical centre interface. +The selected frontier and all existing files remain unchanged. + +Credit belongs to Jeremy Kothe's #622/#623 K-triangle and supplier work, +Chafik Boukhalfa's #626 selected allocation/package, DreamingOfClouds' independent +scalar auditor and cold-helper work, icekylinx's emitter/compiler lineage, +Dugongue's scalar ancestry, eumemic's #543 bit supplier, Rohan Arun's recurrence +work, and the predecessors retained in their notices. The selected construction +and review are linked by +[the selected record](../../certificates/selected-result.json) and +[the maintainer review](../../docs/research/community-k492-review.md). + +The overlap review considered #646/#683/#687 on K-triangle schedules, +#702/#712 on wrapper amplitudes, #692 on weighted-stride duality, and #675 on +owner timing versus scalar bridges. A refreshed 553-PR queue through #734 also +included #722's JP8 coefficient-work sharing, #729's frame-lifetime audit, and +#734's bounded signed-Horner lowering. **Concurrent #734 already includes +arbitrary private inputs in its forward primitive replay.** This package adds +a reverse-mode implementation for the original selected scalar stream and the +complete rank-one clear-omission defect. It makes no priority claim for private +input coverage. These results are compatible; no pending patch is imported or +used as a dependency. The immediate pre-submission refresh through #743 found +no later submission on this same endpoint/omission obligation. The local +[sprint claim](CLAIM.md) records the seed, alternatives, timing, and absence of a +pinned coordination issue. + +Prepared for **Sagar Thakrar (@thakrarsagar)** with substantial OpenAI Codex +assistance in research, implementation, exact checks, review, and writing. A +separate Codex worker checked the mathematics and concrete counterexamples; +this is not independent human peer review. New code and prose are under the +repository's Apache-2.0 license. No predecessor license or attribution is +replaced. diff --git a/research/jp8-adjoint-restoration/SOURCES.json b/research/jp8-adjoint-restoration/SOURCES.json new file mode 100644 index 0000000000..3a3dec2048 --- /dev/null +++ b/research/jp8-adjoint-restoration/SOURCES.json @@ -0,0 +1,22 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 79, + "selected_provider": "jp8", + "reviewed_heads": { + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851" + }, + "files_sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/community-k492-audit/SELECTED-SOURCE.json": "36e9e421230c4cb7b6a537d76a4bdfb6f667730d383e56062d4e45957484ab9e", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/complex-k492-owner-repair/code/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + "programs_path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz", + "programs_payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "word_path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/CANONICAL-WORD.json.gz", + "word_payload_sha256": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b" +} diff --git a/research/jp8-adjoint-restoration/VALIDATION.json b/research/jp8-adjoint-restoration/VALIDATION.json new file mode 100644 index 0000000000..766275770d --- /dev/null +++ b/research/jp8-adjoint-restoration/VALIDATION.json @@ -0,0 +1,106 @@ +{ + "checks": [ + { + "check": "python3 -I -B research/jp8-adjoint-restoration/verify.py", + "passed": true, + "exit_code": 0 + }, + { + "check": "python3 -I -O -B research/jp8-adjoint-restoration/verify.py", + "passed": true, + "exit_code": 0 + }, + { + "check": "python3.11 -I -O -B research/jp8-adjoint-restoration/verify.py", + "python": "3.11.15", + "passed": true, + "exit_code": 0 + }, + { + "check": "make selected-record-check", + "passed": true, + "exit_code": 0 + }, + { + "check": "minimal checkout in path with spaces, unrelated working directory", + "exit_code": 0, + "passed": true, + "seconds": 5.7 + }, + { + "check": "both gzip streams recompressed", + "exit_code": 0, + "passed": true, + "seconds": 3.752 + }, + { + "check": "changed SPEC source rejected", + "exit_code": 1, + "passed": true, + "seconds": 0.047 + }, + { + "check": "changed program payload rejected", + "exit_code": 1, + "passed": true, + "seconds": 0.07 + }, + { + "check": "changed exact certificate rejected", + "exit_code": 1, + "passed": true, + "seconds": 4.03 + } + ], + "environment": { + "machine": "arm64", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "python": "3.14.8" + }, + "date_utc": "2026-10-13", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "status": "PASS", + "predecessor_comparison": { + "recipe": "README.md, separate predecessor comparison command", + "assertions_enabled": true, + "exit_code": 0, + "output": "716 True", + "scope": "Only the historical local() routine, not full admission; no production source or receipt was changed." + }, + "independent_review": { + "method": "Separate Codex worker executed raw scalar events forward on the C0 basis input, without importing verify.py or its decoder.", + "defect_nonzeros": 107, + "canonical_defect_sha256": "05a12929be75313bcd23933b5d048c3547e474e078034e36e8abd51b138f92be", + "all_private_outputs_zero": true, + "exact_certificate_entries_agree": true, + "human_peer_review": false + }, + "overlap": { + "open_pr_count": 553, + "through_pr": 734, + "recent_related": [ + { + "number": 722, + "head": "a0766ab0fab379e1997fadc3ca157578d57986c1", + "distinction": "Changes coefficient-work reuse; this verifies the unchanged scalar projection." + }, + { + "number": 729, + "head": "deaed262cebc50bdb0c27c6ba132b8f8289b3eef", + "distinction": "Checks helper-frame lifetimes; this checks scalar endpoint functionals." + }, + { + "number": 734, + "head": "21606831df4b08f79d87fd420c558a520dca571e", + "distinction": "Also checks arbitrary private inputs, using forward primitive replay of a changed lowering. This contributes reverse scalar replay and an exact omitted-clear rank-one defect." + } + ] + }, + "not_run": [ + "Full make verify", + "Cold selected supplier reconstruction", + "Remote Linux CI", + "Lean", + "Wrapper, phase, hosting, cost, prefix-envelope and analytic re-audits" + ] +} diff --git a/research/jp8-adjoint-restoration/verify.py b/research/jp8-adjoint-restoration/verify.py new file mode 100644 index 0000000000..e50f09029a --- /dev/null +++ b/research/jp8-adjoint-restoration/verify.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Exact output-covector audit of the pinned selected JP8 scalar programs. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +Apache-2.0. No production checker or constructor is imported. +""" + +import gzip +import hashlib +import json +import sys +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +V, N, CENTRES = 112, 716, 8 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def load_inputs(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for path, expected in pins['files_sha256'].items(): + require(digest((ROOT / path).read_bytes()) == expected, 'source pin: ' + path) + selected = json.loads((ROOT / 'certificates/selected-result.json').read_text()) + manifest = json.loads((ROOT / selected['source_manifest']).read_text()) + spec_path = 'research/complex-k492-owner-repair/data/SPEC.json' + require(manifest['files'][spec_path] == pins['files_sha256'][spec_path], 'selected SPEC binding') + for pr, head in pins['reviewed_heads'].items(): + require(selected['reviewed_dependency_heads'][pr] == head, 'reviewed head: ' + pr) + spec = json.loads((ROOT / spec_path).read_text()) + require(sorted(spec['providers'])[pins['assignment_seed'] % 2] == 'jp8', 'seed selection') + provider = spec['providers']['jp8'] + loaded = [] + for kind, artifact in [('programs', 'LOCAL-PROGRAMS.json.gz'), ('word', 'CANONICAL-WORD.json.gz')]: + payload = gzip.decompress((ROOT / pins[kind + '_path']).read_bytes()) + expected = pins[kind + '_payload_sha256'] + require(digest(payload) == expected, 'payload pin: ' + kind) + require(provider['artifact_semantic_sha256'][artifact] == expected, 'SPEC artifact: ' + kind) + loaded.append(json.loads(payload)) + programs, word = loaded + require((word['v'], word['R']) == (V, N - 2 * V), 'word dimensions') + require(set(programs) == {'forward', 'backward'}, 'program orientations') + for name, events in programs.items(): + require(digest(canonical(events)) == provider['program_hashes'][name], 'SPEC program: ' + name) + return programs, word + + +def register(value): + require(isinstance(value, list) and len(value) == 2, 'register shape') + bank, index = value + require(type(index) is int, 'register index type') + require((bank == 'L' and 0 <= index < N) or + (bank == 'C' and 0 <= index < CENTRES), 'register range') + return index if bank == 'L' else N + index + + +def decode(events): + """Retain literal event indices and phase names for mutation witnesses.""" + result, phase = [], None + for index, event in enumerate(events): + tag = event[0] + if tag == 'phase': + phase = event[1] + elif tag == 'scalar': + op = event[1] + kind, target = op[0], register(op[1]) + require(kind in {'add', 'scale', 'copy', 'clear'}, 'unknown scalar operation') + require(len(op) == {'add': 5, 'scale': 4, 'copy': 3, 'clear': 2}[kind], 'scalar arity') + source = register(op[2]) if kind in {'add', 'copy'} else None + require(source != target, 'self read/write') + coefficient = Fraction(1) + if kind in {'add', 'scale'}: + a, b = op[-2:] + require(type(a) is int and type(b) is int and b != 0, 'coefficient syntax') + coefficient = Fraction(a, b) + require(coefficient != 0, 'zero coefficient') + denominator = coefficient.denominator + require(denominator & (denominator - 1) == 0, 'non-dyadic coefficient') + if kind == 'scale': + numerator = abs(coefficient.numerator) + require(numerator & (numerator - 1) == 0, 'nonbinary scale') + result.append((kind, target, source, coefficient, index, phase)) + else: + # These describe frame/wrapper transport, outside the scalar projection. + require(tag in {'adapter', 'residual_adapter', 'climb', 'center'}, 'unknown event') + return result + + +def pullback(operations, output): + """Pull one output linear functional back to all arbitrary input coordinates.""" + covector = {output: Fraction(1)} + for kind, target, source, coefficient, _, _ in reversed(operations): + weight = covector.get(target) + if not weight: + continue + if kind == 'scale': + covector[target] = weight * coefficient + else: + if kind in {'copy', 'clear'}: + del covector[target] + if kind in {'add', 'copy'}: + value = covector.get(source, 0) + weight * coefficient + if value: + covector[source] = value + else: + covector.pop(source, None) + return covector + + +def expected_row(direction, output): + if output >= N: + return {} + row = {output: Fraction(1)} + if direction == 'forward' and V <= output < 2 * V: + row[output - V] = Fraction(1) + elif direction == 'backward' and output < V: + row[output + V] = Fraction(-1) + return row + + +def coordinate(index): + return ['L', index] if index < N else ['C', index - N] + + +def direct_basis_value(operations, input_coordinate, output): + """Scalar-value replay of one witness, independent of covector propagation.""" + values = [Fraction(0)] * (N + CENTRES) + values[input_coordinate] = Fraction(1) + for kind, target, source, coefficient, _, _ in operations: + if kind == 'add': + values[target] += coefficient * values[source] + elif kind == 'scale': + values[target] *= coefficient + elif kind == 'copy': + values[target] = values[source] + elif kind == 'clear': + values[target] = Fraction(0) + return values[output] + + +def check_program(direction, operations): + rows = [] + for output in range(N + CENTRES): + actual = pullback(operations, output) + require(actual == expected_row(direction, output), f'endpoint mismatch: {direction} {coordinate(output)}') + rows.append([[j, str(q)] for j, q in sorted(actual.items())]) + return { + 'scalar_operations': len(operations), + 'operation_counts': dict(sorted(Counter(op[0] for op in operations).items())), + 'input_coordinates': N + CENTRES, + 'output_coordinates_checked': len(rows), + 'persistent_outputs': N, + 'private_outputs': CENTRES, + 'nonzero_matrix_entries': sum(map(len, rows)), + 'output_covectors_sha256': digest(canonical(rows)), + } + + +def omission_witness(direction, operations, operation_index): + dropped = operations[operation_index] + mutant = operations[:operation_index] + operations[operation_index + 1:] + for output in range(N + CENTRES): + actual = pullback(mutant, output) + expected = expected_row(direction, output) + for input_coordinate in sorted(actual.keys() | expected.keys()): + a, e = actual.get(input_coordinate, 0), expected.get(input_coordinate, 0) + if a != e: + require(direct_basis_value(mutant, input_coordinate, output) == a, 'witness forward replay') + require(direct_basis_value(operations, input_coordinate, output) == e, 'baseline witness replay') + return { + 'direction': direction, 'event_index': dropped[4], 'phase': dropped[5], + 'operation': [dropped[0], coordinate(dropped[1]), + coordinate(dropped[2]) if dropped[2] is not None else None, str(dropped[3])], + 'input_basis_coordinate': coordinate(input_coordinate), + 'output_coordinate': coordinate(output), 'expected': str(e), 'actual': str(a), + } + raise ValueError('omission control did not change the scalar map') + + +def dirty_centre_gap(operations, operation_index): + """Check the whole omitted-clear defect, including its invisible L-only restriction.""" + dropped = operations[operation_index] + require(dropped[0] == 'clear' and dropped[1] == N, 'C0 initial clear') + mutant = operations[:operation_index] + operations[operation_index + 1:] + defect = [] + for output in range(N + CENTRES): + actual = pullback(mutant, output) + expected = expected_row('backward', output) + require({j: q for j, q in actual.items() if j < N} == expected, + 'mutant changed L-input restriction') + require(all(j < N or j == N for j in actual), 'unexpected dirty-centre dependency') + if N in actual: + defect.append([output, str(actual[N])]) + require(defect and all(output < N for output, _ in defect), 'persistent-only nonzero defect') + return {'event_index': dropped[4], 'input_coordinate': ['C', 0], + 'all_716_L_input_columns_unchanged': True, 'all_private_outputs_zero': True, + 'nonzero_output_coefficients': defect, + 'defect_rank': 1} + + +def self_check(): + # Overwriting a dirty destination must kill its former input coefficient. + ops = [('copy', 1, 0, Fraction(1), 0, 'test'), + ('add', 2, 1, Fraction(3, 2), 1, 'test'), + ('scale', 2, None, Fraction(-2), 2, 'test'), + ('clear', 1, None, Fraction(1), 3, 'test')] + require(pullback(ops, 0) == {0: 1}, 'self-check identity') + require(pullback(ops, 1) == {}, 'self-check clear') + require(pullback(ops, 2) == {0: -3, 2: -2}, 'self-check mixed operations') + + +def compute(): + self_check() + programs, word = load_inputs() + decoded = {name: decode(events) for name, events in programs.items()} + checks = {name: check_program(name, ops) for name, ops in decoded.items()} + forward, backward = decoded['forward'], decoded['backward'] + first = lambda ops, predicate: next(i for i, op in enumerate(ops) if predicate(op)) + copy_index = first(forward, lambda op: op[0] == 'copy') + final_clear_index = next(i for i in range(copy_index + 1, len(forward)) + if forward[i][0] == 'clear' and forward[i][1] == forward[copy_index][1]) + backward_clear_index = first(backward, lambda op: op[0] == 'clear') + controls = [ + ('forward_compensation', 'forward', len(word['precondition'])), + ('forward_early_cleanup', 'forward', first(forward, lambda op: op[5] == 'cleanup_tail')), + ('forward_full_cleanup', 'forward', first(forward, lambda op: op[5] == 'full_frame_cleanup')), + ('forward_centre_copy', 'forward', copy_index), + ('forward_final_centre_clear', 'forward', final_clear_index), + ('backward_initial_centre_clear', 'backward', backward_clear_index), + ] + require(forward[len(word['precondition'])][5] == 'zero_frame_precondition', 'compensation location') + witnesses = {name: omission_witness(direction, decoded[direction], index) + for name, direction, index in controls} + require(witnesses['backward_initial_centre_clear']['input_basis_coordinate'][0] == 'C', 'dirty-centre control') + return {'status': 'PASS_JP8_ADJOINT_RESTORATION', 'supplier': 'jp8', + 'checks': checks, 'omission_witnesses': witnesses, + 'dirty_centre_gap': dirty_centre_gap(backward, backward_clear_index), + 'scope': 'Exact finite scalar projection; frames, wrappers, costs and all-size interfaces are inherited.'} + + +def main(): + require(sys.argv[1:] in ([], ['--report']), 'usage: verify.py [--report]') + report = compute() + require(report == json.loads((HERE / 'EXPECTED.json').read_text()), 'certificate mismatch') + if sys.argv[1:]: + print(json.dumps(report, indent=2, sort_keys=True)) + print('PASS_JP8_ADJOINT_RESTORATION outputs=724x2 inputs=724 controls=6 kappa=unchanged') + + +if __name__ == '__main__': + main() From fc6ebccca3bd61a6eaf6ec3fcbf2e99d2888c35c Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:33:19 +0530 Subject: [PATCH 2/2] Record completed sprint contribution and PR handoff --- research/jp8-adjoint-restoration/CLAIM.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/research/jp8-adjoint-restoration/CLAIM.md b/research/jp8-adjoint-restoration/CLAIM.md index c71024e02d..51b5f60728 100644 --- a/research/jp8-adjoint-restoration/CLAIM.md +++ b/research/jp8-adjoint-restoration/CLAIM.md @@ -13,3 +13,21 @@ Three candidates were considered: the raw K-triangle read identity, cold-wrapper Scope is confined to this directory. The construction, selected frontier, `upstream/`, physical frame/wrapper semantics, recursion, cost model, and global assembly remain unchanged. Acceptance requires all output-coordinate identities in both orientations, meaningful rejected semantic mutations, source binding, and a reproducible offline command. This is a finite scalar verification, not a formal proof of the multiplication theorem. Prepared for Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex assistance. + +## Result update + +Completed on 2026-10-13 at 05:03 UTC and submitted as +[PR #745](https://github.com/CrocSwap/integer-mult-bounds/pull/745). +All 724 output functionals pass in both orientations on 724 arbitrary input +coordinates. Six omission controls are rejected. The complete rank-one defect +from deleting backward event 13113 has 107 nonzero persistent outputs while +preserving all 716 ordinary input columns. A separate forward implementation +reproduced every coefficient. No new kappa is claimed. + +The final portion of the session covered normal and optimized execution, +Python 3.14.8/3.11.15, minimal relocation, gzip recompression, corruption +rejection, the predecessor comparison, selected-record integrity, and handoff. +The final overlap check reached #743. Concurrent #734's private-input coverage +is explicitly credited; this adds reverse-mode evidence and the exact +clear-omission defect. Full cold/repository-wide and geometric/analytic checks +remain inherited, as recorded in README.md and VALIDATION.json.