From 5b830a692e30e6466130908693c7db2c56c4bf48 Mon Sep 17 00:00:00 2001 From: Gabriel Roa Date: Tue, 13 Oct 2026 02:17:54 -0300 Subject: [PATCH 1/2] Audit all 14 K492 assembly helper-count reversions --- .../k492-helper-accounting-audit/CLAIM.json | 43 ++ .../EXPECTED.json | 310 +++++++++++++ .../k492-helper-accounting-audit/README.md | 185 ++++++++ .../k492-helper-accounting-audit/SOURCE.json | 52 +++ .../k492-helper-accounting-audit/verify.py | 416 ++++++++++++++++++ 5 files changed, 1006 insertions(+) create mode 100644 research/k492-helper-accounting-audit/CLAIM.json create mode 100644 research/k492-helper-accounting-audit/EXPECTED.json create mode 100644 research/k492-helper-accounting-audit/README.md create mode 100644 research/k492-helper-accounting-audit/SOURCE.json create mode 100644 research/k492-helper-accounting-audit/verify.py diff --git a/research/k492-helper-accounting-audit/CLAIM.json b/research/k492-helper-accounting-audit/CLAIM.json new file mode 100644 index 0000000000..e0dc012198 --- /dev/null +++ b/research/k492-helper-accounting-audit/CLAIM.json @@ -0,0 +1,43 @@ +{ + "track": "Adversarial mathematical audit", + "assignment_seed": 73, + "random_source": "Python secrets.randbelow(100), backed by operating-system randomness", + "drawn_at_utc": "2026-10-13T04:45:58.535853+00:00", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "candidate_tasks": [ + { + "index": 0, + "task": "Audit the dead-port condition for K492 cold-end forward absorptions.", + "decision": "Not selected; related cold-wrapper and restoration audits #702/#712 already active." + }, + { + "index": 1, + "task": "Audit all 14 assembly-side R versus R0 substitutions documented in K492 PROOF-NOTE-R.", + "decision": "Selected: seed % 3 = 1; the maintainer review explicitly excludes the unavailable original revert suite." + }, + { + "index": 2, + "task": "Audit the prime-power inverse resultant/cofactor bound.", + "decision": "Not selected; independent resultant work #668 and composite extension #666 overlap." + } + ], + "claim": { + "object": "research/complex-k492-owner-repair/code/assemble.py: the 14 assemble.* sites in PROOF-NOTE-R.md", + "method": "Pin selected #626 receipts and code, independently recount R/R0 conservation and invoice charges, then revert each documented assembly-side expression in memory one at a time; require the precise intended assertion failure, with unchanged baseline and equivalent-parent positive controls.", + "expected_deliverable": "Standalone standard-library audit, exact deterministic receipt, source pins, mathematical/accounting scope note and one research-audit PR; no new kappa.", + "expected_finish_utc": "2026-10-13T05:26:00Z", + "verification_reserved_from_utc": "2026-10-13T05:16:00Z" + }, + "coordination": { + "checked_at_utc": "2026-10-13T04:49:06.049256+00:00", + "pinned_issues": [], + "open_issues": [ + 650 + ], + "claim_location": "Local: no sprint coordination issue exists.", + "open_pr_snapshot_count": 539, + "open_pr_max": 720, + "overlap": "Read relevant open PR metadata and central ledger; #675 covers owner timing/bridge omission, #706 covers independent moment bounds. Neither supplies the documented source-reversion controls. #626 is incorporated at selected pin; no existing PR will be modified." + }, + "status": "claimed" +} diff --git a/research/k492-helper-accounting-audit/EXPECTED.json b/research/k492-helper-accounting-audit/EXPECTED.json new file mode 100644 index 0000000000..ac10b0cc76 --- /dev/null +++ b/research/k492-helper-accounting-audit/EXPECTED.json @@ -0,0 +1,310 @@ +{ + "accounting": { + "data_rows": 7168, + "helper_roles": 35424, + "hosted_rebased_pervertex": 1833791190482956, + "mapped_spots": [ + 264, + 276, + 288, + 300 + ], + "nonlocal_items": { + "bridges": 16128, + "data_routes": 32256, + "helper_routes": 70848, + "moves": 7168, + "parent_banks": 4536, + "parent_idle": 16128, + "parent_live": 11704, + "parent_physical": 12218, + "port_routes": 16128, + "shifts": 3584, + "wrappers": 4713984 + }, + "old_spot_widths": { + "ck": [ + 7, + 8, + 9, + 7 + ], + "jp8": [ + 8, + 9, + 9, + 8 + ] + }, + "parent_helpers": 504, + "parent_live": 11704, + "parent_physical": 12218, + "physical_rows": 7670, + "provider_helpers": 492, + "providers": { + "ck": { + "columns": 716, + "entrance_rank": 424, + "helpers": 492, + "local": { + "backward": { + "coefficient_work_primitive_count": 111779, + "events": 27256, + "macros": 21936, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "post_wrappers": 238, + "pre_wrappers": 238, + "real_component_primitives": 224986 + }, + "forward": { + "coefficient_work_primitive_count": 111747, + "events": 27256, + "macros": 21936, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "post_wrappers": 238, + "pre_wrappers": 238, + "real_component_primitives": 224938 + } + }, + "local_adapters": 426400, + "terminal_codimension": 146, + "width_inventory": { + "4": 30, + "5": 48, + "7": 68, + "8": 92, + "9": 254 + }, + "width_sum": 3858 + }, + "jp8": { + "columns": 716, + "entrance_rank": 380, + "helpers": 492, + "local": { + "backward": { + "coefficient_work_primitive_count": 127930, + "events": 27909, + "macros": 22693, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "post_wrappers": 226, + "pre_wrappers": 226, + "real_component_primitives": 257280 + }, + "forward": { + "coefficient_work_primitive_count": 127898, + "events": 27909, + "macros": 22693, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "post_wrappers": 226, + "pre_wrappers": 226, + "real_component_primitives": 257232 + } + }, + "local_adapters": 437040, + "terminal_codimension": 146, + "width_inventory": { + "4": 30, + "5": 48, + "7": 36, + "8": 112, + "9": 266 + }, + "width_sum": 3902 + } + }, + "removed_parent_registers": [ + 448, + 458, + 460, + 470, + 472, + 482, + 580, + 590, + 592, + 602, + 604, + 614 + ], + "stale_provider_route_overcharge": 358516260864, + "substituted_parent_bank_undercharge": 22407266304, + "unhosted_pervertex": 1833791190783112 + }, + "audit_controls": [ + "stale_native_helper_count", + "dependent_frame_basis", + "missing_helper_role", + "duplicate_helper_role", + "wrong_helper_width", + "unpinned_source", + "absent_mutation_anchor", + "ambiguous_mutation_anchor" + ], + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "documented_sites": 14, + "selected_kappa": "51110230636731/31250000000000000", + "source_controls": [ + { + "assertion_line": 42, + "mutated_source_sha256": "997153c0535ef9563fef659087abb136f14147b4dac5e148b3c871144015c660", + "name": "assemble.R", + "original": "R=invoice['helpers'];", + "outcome": "rejected_at_expected_assertion", + "replacement": "R=504;" + }, + { + "assertion_line": 43, + "mutated_source_sha256": "a2f4d47192ea7aad60bb7a8edf6501e1f9dbd8439dced76bff410787fdf5304a", + "name": "assemble.owners_per_call", + "original": "owner['owners_per_call']==2*112+R", + "outcome": "rejected_at_expected_assertion", + "replacement": "owner['owners_per_call']==728" + }, + { + "assertion_line": 43, + "mutated_source_sha256": "0d89f93408a88c66ded9a1e3a26142265f75c55b7300f84e78f507a401e113db", + "name": "assemble.hosted_72R", + "original": "==72*R==pin(", + "outcome": "rejected_at_expected_assertion", + "replacement": "==72*504==pin(" + }, + { + "assertion_line": 50, + "mutated_source_sha256": "a608f6f9afb7b2394a6624d97bffa79330b786ce30569a99f314d7c172ce0523", + "name": "assemble.stock_helpers", + "original": "local_helpers=R,", + "outcome": "rejected_at_expected_assertion", + "replacement": "local_helpers=504," + }, + { + "assertion_line": 55, + "mutated_source_sha256": "8e0aef320555f68ada50daa458bf7b842e313c5698f793cb40875c7cd73c65cc", + "name": "assemble.provider_helpers", + "original": "assert p['helpers']==R and", + "outcome": "rejected_at_expected_assertion", + "replacement": "assert p['helpers']==504 and" + }, + { + "assertion_line": 55, + "mutated_source_sha256": "c37d9d84e1271d6ef8a8a9706ae65f7f390a28086f00df3ad5326f18f628161e", + "name": "assemble.provider_n", + "original": "p['n']==2*112+R", + "outcome": "rejected_at_expected_assertion", + "replacement": "p['n']==728" + }, + { + "assertion_line": 60, + "mutated_source_sha256": "d8004f39c174873f180e58c55a99d5f1413e6431f6586661452de6811f7a7dd4", + "name": "assemble.width_sum", + "original": "==9*R-p['entrance_rank']", + "outcome": "rejected_at_expected_assertion", + "replacement": "==9*504-p['entrance_rank']" + }, + { + "assertion_line": 60, + "mutated_source_sha256": "dbe6bc1efdca972f148b44708ae3a71ddfd3764d4e4345aa0bfa70febf9e0b7d", + "name": "assemble.width_len", + "original": "len(p['widths'])==R", + "outcome": "rejected_at_expected_assertion", + "replacement": "len(p['widths'])==504" + }, + { + "assertion_line": 76, + "mutated_source_sha256": "a8261f357c6be313e87a4be2ad9ebdf05c1069a6b9a26cc8a62594db8508ba90", + "name": "assemble.exact_columns", + "original": "z['all_exact_columns']==2*112+R", + "outcome": "rejected_at_expected_assertion", + "replacement": "z['all_exact_columns']==728" + }, + { + "assertion_line": 76, + "mutated_source_sha256": "52e7f0a24e34ca5c823fb57a257c9cf9d2048dda2fa2ee468cd439da8e7da216", + "name": "assemble.dirty_columns", + "original": "z['dirty_helper_columns']==R", + "outcome": "rejected_at_expected_assertion", + "replacement": "z['dirty_helper_columns']==504" + }, + { + "assertion_line": 84, + "mutated_source_sha256": "c25fbaffaecfd9def42f64709f1be3ca4398c4ab55416ba6c7cd67a104cf251d", + "name": "assemble.local_adapters", + "original": "p['children']+2*112+R+8", + "outcome": "rejected_at_expected_assertion", + "replacement": "p['children']+728+8" + }, + { + "assertion_line": 126, + "mutated_source_sha256": "92bdbd579eee47cb2882c391595787a649c35b4a73fcd04b8d556445ab0bd2b9", + "name": "assemble.route_items", + "original": "+2*72*R+", + "outcome": "rejected_at_expected_assertion", + "replacement": "+2*72*504+" + }, + { + "assertion_line": null, + "mutated_source_sha256": "309775c3463e2d74be58a9b80ad56fcf1700983fc11378381a6256e66d2d4488", + "name": "assemble.parent_banks", + "original": "+9*parent_banks+", + "outcome": "accepted_identical_assembly", + "replacement": "+9*504+" + }, + { + "assertion_line": 61, + "mutated_source_sha256": "22d3dbe7e6e6ef563628e2138cd47e04f7ecc6c0dd8a77f47359d1be94a78b01", + "name": "assemble.spot_width8", + "original": "for h in SPOT)", + "outcome": "rejected_at_expected_assertion", + "replacement": "for h in (270,282,294,306))" + }, + { + "assertion_line": 126, + "mutated_source_sha256": "63188cc501e3622ef65580b9c448987295405aa01e20c26cf6d757798731ae31", + "name": "control.parent_banks_use_provider_R", + "original": "+9*parent_banks+", + "outcome": "rejected_at_expected_assertion", + "replacement": "+9*R+" + }, + { + "assertion_line": null, + "mutated_source_sha256": "904bfce7e3e365933c3ac7d888f14cd0c133e51cae7f85623f1734113a03369b", + "name": "control.equivalent_provider_count", + "original": "R=invoice['helpers'];", + "outcome": "accepted_identical_assembly", + "replacement": "R=504-12;" + } + ], + "status": "PASS_SCOPED_K492_HELPER_ACCOUNTING_AUDIT" +} diff --git a/research/k492-helper-accounting-audit/README.md b/research/k492-helper-accounting-audit/README.md new file mode 100644 index 0000000000..5acb8e9dbd --- /dev/null +++ b/research/k492-helper-accounting-audit/README.md @@ -0,0 +1,185 @@ +# Selected K492 helper-count audit + +**Research audit / independent finite recount; no new kappa.** All 14 +`assemble.*` substitutions in the selected construction's +[PROOF-NOTE-R](../complex-k492-owner-repair/PROOF-NOTE-R.md) now have a portable, +source-pinned replay. Thirteen stale-count/index substitutions fail at their +specified assertion. The equivalent `9*504` parent-bank substitution reproduces +the entire selected assembly receipt. No defect is found in these current +assembly checks. + +The [maintainer review](../../docs/research/community-k492-review.md) explicitly +excluded the original author's unavailable 32-site scratch reversion suite. +This package supplies new coverage for its **14 assembly-side sites only**, +using the selected #626 fixture. It does not claim to recover that script, +reproduce the other 18 sites, or repeat its R=504 compatibility fixture. + +## Reproduce + +From any directory, with Python 3.11 or later and only its standard library: + +```sh +python3 -I -B research/k492-helper-accounting-audit/verify.py +``` + +Use an absolute script path when outside the repository. Expected output: + +```text +PASS_SCOPED_K492_HELPER_ACCOUNTING_AUDIT documented_sites=14 rejected=13 equivalent=1 additional_source_controls=2 audit_controls=8 +``` + +The command checks all immutable source pins, independently recounts the finite +inputs, executes the full unchanged assembly and all source controls, and +compares the deterministic result to [EXPECTED.json](EXPECTED.json). +`--output /tmp/k492-audit.json` writes a fresh receipt instead of comparing it. +No repository artifacts are regenerated. Optimized Python (`-O`) is explicitly +rejected before replay because the imported production code requires assertions. + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Selected #626 source: `660de893d27bb7abd1d5b01b1640207528a5c851`. +The unchanged selected saving is +`51110230636731/31250000000000000 = 0.001635527380375392`. +[SOURCE.json](SOURCE.json) pins every consumed repository input and executable +dependency, with the selected dependency heads. [CLAIM.json](CLAIM.json) records +OS-random assignment seed **73**, three candidate tasks and the local claim; +no pinned or other sprint coordination issue was available. + +## What the recount establishes + +The two counts have different meanings: R=492 is the helper count of an executed +provider, whereas R0=504 belongs to the retained parent geometry. Both CK and +JP8 have `2*112+492 = 716` native columns. Independent binary elimination checks +that the stored frames are bases; their ranks give every helper's start and end +dimensions. For each provider the conservation identity is + + sum(helper widths) = 9R - sum(start ranks) - sum(9 - end ranks). + +The exact totals are: + +| Provider | Helpers | Entrance rank | Terminal codimension | Width sum | Local adapters | +|---|---:|---:|---:|---:|---:| +| CK | 492 | 424 | 146 | 3858 | 426400 | +| JP8 | 492 | 380 | 146 | 3902 | 437040 | + +Every literal `(stage, replica, helper)` role occurs exactly once, and its width +matches the native word: `9*8*492 = 35,424` roles. This is a count/width check; +it is not another owner-window or physical-chart proof. The helper map is a +bijection after the twelve removed parent registers are excluded. Translating +the old helper indices `(270,282,294,306)` through the **absolute-register** map +gives `(264,276,288,300)`, all width eight. The old indices have widths +`(7,8,9,7)` in CK and `(8,9,9,8)` in JP8, so retaining them is not equivalent. + +The recount reads all four native `LOCAL-PROGRAMS` orientations. For a scalar +addition with reduced coefficient `n/2^e`, the retained implementation clears +coefficient work, performs `bit_length(|n|)-1` doublings and `popcount(|n|)` +additions, halves e times, accumulates with sign and clears the work. Its cost +per real component is therefore + + bit_length(|n|) + popcount(|n|) + e + 2. + +The new implementation uses this closed formula rather than executing the +production Horner accumulator. It also counts scales, copies, clears, recursive +children and both wrapper endpoints. The complex charge is twice the real +charge. This verifies a count for the **retained implementation**, not minimal +scalar cost, an l1 prefix bound, or scalar endpoint correctness. + +The selected physical stock is `7168+492+8+2 = 7670`. The parent remains +`7168+9*504 = 11704` live rows and `11704+504+8+2 = 12218` physical rows. +The resulting finite parent-envelope price is `1833791190783112`, and its +rebased value is `1833791190482956`. The inherited parent idle count of 16,128 +is consumed from the pinned owner receipt; this audit does **not** reconstruct +the omitted parent `GLOBAL-TEMPLATE` or establish that idle count independently. + +Writing `C = 64*74^3 = 25934336`, two illustrative exact deltas are: + +* Using R0 instead of R for two-way helper routing adds + `8*C*2*72*(504-492) = 358516260864`. +* Using R instead of R0 for the nine parent banks omits + `8*C*9*(504-492) = 22407266304`. + +The first is an **overcharge**, rejected because it disagrees with the fixed +receipt. Its rejection does not show that a larger conservative allowance is +mathematically invalid. The second undercounts the retained parent envelope. +Neither experiment changes the selected construction or proves a new bound. + +## Source controls and their limits + +Each mutation replaces one unique executable substring in memory, leaving the +fixture unchanged. A rejection counts only if it is an `AssertionError` at the +specific expected line in that mutated source. Imports, malformed fixtures, +unrelated assertions and unexpected acceptance fail the audit. The 14 control +names must equal the 14 `assemble.*` rows parsed from the pinned proof note. + +The baseline and every accepted control run the complete production assembly: +provider admission, finite guards, both rational moment engines, conservative +and native endpoints, outer inequalities and the assembly's own endpoint/grid +controls. Their **entire returned JSON objects** must equal the selected +`ASSEMBLY.json`, allowing only JSON's conversion of integer object keys to +strings. No production assertion is removed or replaced with a stub. + +Two extra source controls reject `9*R` for the parent-bank charge and accept +the equivalent `R=504-12`. Eight harness/recount controls cover a stale native +helper count, dependent frame basis, missing/duplicated roles, wrong widths, +source corruption and absent/ambiguous mutation anchors. Two exact toy prices +also check the signed multibit Horner formula and its extra-halving charge. + +This is a bounded audit, not a search: all fourteen specified sites, the two +selected providers and both orientations are covered, then execution stops. +Seed 73 selected candidate index `73 % 3 = 1`; it is not a claim of independence +by itself. Finite replay is not a formal proof of the multiplication theorem. +The archived local algebra/frame/phase/restoration receipts remain inherited; +the suppliers are not cold-rebuilt. Uniform compilation, common-label and +mutable-basis realization, pooled hosting, normalized residuals, precision, +tape and analytic transfer remain conditional. This addition does not require +or claim a repository-wide `make verify` or `make frontier626-verify` rerun. + +## Validation record + +Local verification on 2026-10-13, macOS / CPython 3.11.5: + +* The reproduction command above matches the committed deterministic receipt. +* The existing, unchanged `code/assembly_controls.py` passes all **114** + admission rejection controls on these selected owner/invoice inputs and the + pinned `vendor/multicold` dependency. +* `make selected-record-check` passes. +* A minimal export containing only this package and its 23 pinned input files + passes when invoked by absolute path from `/tmp` with isolated imports. +* Corrupted expected-receipt and source-file exports fail as intended; the + source corruption is rejected before execution. A `-O` export invocation + fails explicitly. `git diff --check` passes. + +These are local results. No remote CI result or cold supplier reconstruction +is claimed. The exported-input and corruption tests use temporary directories; +no frozen source or selected certificate is edited. + +## Concurrent work and credit + +During the final overlap check, Sagar Thakrar / @thakrarsagar's +[PR #724](https://github.com/CrocSwap/integer-mult-bounds/pull/724), pinned at +`624ccfe44b1c5816f0279481d91cca6a5a2290ab`, had already supplied an independent +R/R0 invoice audit and resolved the proof note's introductory pass/fail +contradiction. Its route and parent-bank deltas agree with this recount. +Those conclusions are corroboration, not a priority claim. + +The distinct coverage here is the **complete 14-row assembly reversion table**, +including provider-column, width, local-adapter and mapped-index assertions +outside #724's accounting slice; execution of the **whole assembly** on the +baseline and equivalent controls; and fresh closed-form operation counts from +the four local programs rather than using their invoice totals as inputs. +No #724 implementation is imported. #675's owner timing/bridge audit, #706's +independent moment bounds and #729's helper-frame lifetime audit concern other +obligations and are not dependencies of this result. + +Jeremy Kothe / jeremykothe2 and the credited GlobalR/AtomReviewer and other +Claude research agents supplied #622's K-triangle construction, R generalization +and original reported scratch controls; Jeremy also supplied #623's dispatch. +Chafik Boukhalfa / chafreaky supplied #626's owner repair and portable checks. +Douglas Colkitt supplied the maintainer review and archived replay evidence. +DreamingOfClouds' cold-helper construction, Rohan Arun's #559 recurrence +correction, eumemic's #543 bit supplier, icekylinx and the full retained +compiler/accounting lineage retain credit. Their notices remain unchanged. + +Prepared by **Gabriel Roa / @gaboroa14**, with substantial **OpenAI Codex** +assistance in selection, design, implementation, analysis, verification and +writing. No independent human peer review or proof-assistant certification is +claimed. New files are Apache-2.0, under the repository license. diff --git a/research/k492-helper-accounting-audit/SOURCE.json b/research/k492-helper-accounting-audit/SOURCE.json new file mode 100644 index 0000000000..a9c189e3a0 --- /dev/null +++ b/research/k492-helper-accounting-audit/SOURCE.json @@ -0,0 +1,52 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "audited_source_pr": 626, + "audited_source_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "reviewed_dependency_heads": { + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90" + }, + "assembly_dependency": "research/complex-k492-owner-repair/vendor/multicold", + "subject": "The 14 assemble.* source-reversion sites documented in PROOF-NOTE-R, using selected PR626 archived native inputs and receipts.", + "independence": "New rank elimination, helper enumeration and closed-form Horner price recount; source mutation replay intentionally executes the pinned existing assembly and its three arithmetic engines. This is not an independent moment engine or a cold supplier reconstruction.", + "container_policy": "Hashes pin immutable committed input bytes. The audit writes no compressed artifacts; frame/rank/width checks consume the decompressed JSON payloads.", + "files": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "research/community-k492-audit/pr626/replay/ck-base-k_triangle-construction/HELPER-MAP.json": "688d5115b221be68c96970822cc04ff698e2a84432fa7db9cb59057f6fe55def", + "research/community-k492-audit/pr626/replay/mixed-global/audit/OWNERS-AND-PROFILE.json": "ec7bc4157e7ab1707bddf99994149c932b51365de7e742508fd182051ca57fc1", + "research/community-k492-audit/pr626/replay/mixed-global/audit/PREFIX-AND-INVOICE.json": "367a73f744ea9b7dd6cca5fa3fda47175f560aa3d37e708c9fa1294dbd4b56eb", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/CANONICAL-WORD.json.gz": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98", + "research/community-k492-audit/pr626/replay/mixed-global/base/split-centres/CANONICAL-WORD.json.gz": "66d3c3c70983224650643a0a05a21ac6c6959f84d0f4528650601016f5a76844", + "research/complex-k492-owner-repair/NOTICE.md": "e7e934433919b73f6088a68a444eed4cea029638ae7b0df3fde15099d5369fd1", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "research/complex-k492-owner-repair/code/assemble.py": "1b1a9024ac910dc9b9d9e30150684e1fa9cb228a4c1c275b75ab04b57fdef1dd", + "research/complex-k492-owner-repair/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/complex-k492-owner-repair/code/witness.py": "00789c911a8f32cfe9d52207c7aa78305dc3fce4a8b6305ba402b7e74117103d", + "research/complex-k492-owner-repair/data/OWNERS.json.gz": "251e82cec1f40e6c1289703667f403104b957f1254dc4f6baa6df9a3d0c751de", + "research/complex-k492-owner-repair/data/PLAN.json": "8c48ef6ce079916314126c5c3ff0003b32f24cf0fbfb2a033fc93e1e1949b5d5", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/complex-k492-owner-repair/vendor/multicold/inputs/PR543-EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d" + }, + "attribution": { + "contributor": "Gabriel Roa / @gaboroa14", + "assistance": "Substantial OpenAI Codex assistance in task selection, audit design, code, analysis, verification and writing. No independent human review or formal proof is claimed.", + "predecessors": [ + "Jeremy Kothe / jeremykothe2 and credited Claude research agents: #622 K-triangle construction, R generalization and the originally reported scratch revert suite; #623 dispatch.", + "Chafik Boukhalfa / chafreaky: #626 owner map, portable packaging and independent owner checks.", + "Douglas Colkitt: selected review and archived maintainer receipts; identified the unreproduced scratch-control scope.", + "DreamingOfClouds: cold-helper construction; Rohan Arun: #559 native-complex recurrence correction; eumemic: #543 bit supplier; icekylinx and the retained source/compiler/accounting lineage." + ], + "license": "Apache-2.0, retaining all predecessor notices in their original packages." + } +} diff --git a/research/k492-helper-accounting-audit/verify.py b/research/k492-helper-accounting-audit/verify.py new file mode 100644 index 0000000000..3545cd048f --- /dev/null +++ b/research/k492-helper-accounting-audit/verify.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Scoped audit of the selected K492 assembly's provider/parent helper counts. + +Gabriel Roa / @gaboroa14, with substantial OpenAI Codex assistance. +Apache-2.0. See README.md for attribution, mathematical scope and exclusions. +""" + +import argparse +from collections import Counter +import copy +from fractions import Fraction +import gzip +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import sys + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = Path("research/complex-k492-owner-repair") +REPLAY = Path("research/community-k492-audit/pr626/replay") +BASE = REPLAY / "mixed-global/base" +AUDIT = REPLAY / "mixed-global/audit" +ASSEMBLER = PACKAGE / "code/assemble.py" + + +class AuditError(ValueError): + pass + + +def require(condition, message): + if not condition: + raise AuditError(message) + + +def canonical(value): + """Normalize JSON object keys (in particular integer profile ranks).""" + return json.loads(json.dumps(value)) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def read(relative): + path = ROOT / relative + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def check_pin(data, expected, label): + require(sha(data) == expected, "source hash mismatch: " + label) + + +def rank_f2(rows, dimension): + pivots = {} + for row in rows: + require(type(row) is int and 0 < row < 1 << dimension, "invalid frame vector") + while row: + bit = row.bit_length() - 1 + if bit not in pivots: + pivots[bit] = row + break + row ^= pivots[bit] + return len(pivots) + + +def widths_from_word(word): + v, helpers, dimension = word["v"], word["R"], word["h"] + require(len(word["start"]) == len(word["final"]) == 2*v + helpers, + "native register count") + ranks = [rank_f2(frame, dimension) for frame in word["frames"]] + require(all(rank == len(frame) for rank, frame in zip(ranks, word["frames"])), + "dependent frame basis") + starts = [ranks[f] for f in word["start"][2*v:]] + ends = [ranks[f] for f in word["final"][2*v:]] + widths = [end - start for start, end in zip(starts, ends)] + require(all(0 < w <= dimension for w in widths), "invalid helper width") + return widths, sum(starts), sum(dimension - end for end in ends) + + +def price_program(events): + """Count the retained Horner implementation by a closed integer formula. + + Unlike invoice_allcold.py, this does not execute the Horner accumulator or + propagate an l1 envelope. It checks only the charged operation count. + """ + macros = primitives = coefficient_work = 0 + paid = Counter() + wrappers = {"pre": set(), "post": set()} + for event in events: + tag = event[0] + if tag == "climb": + paid[event[5]] += 1 + elif tag == "center": + paid[event[4]] += 1 + elif tag == "residual_adapter": + side, register = event[1:3] + require(side in wrappers and register not in wrappers[side], "duplicate wrapper") + wrappers[side].add(register) + elif tag == "scalar": + macros += 1 + scalar = event[1] + op = scalar[0] + if op in ("copy", "clear"): + cost = 1 + else: + require(op in ("scale", "add"), "unknown scalar operation") + q = Fraction(*scalar[-2:]) + numerator, denominator = abs(q.numerator), q.denominator + require(numerator > 0 and denominator & (denominator-1) == 0, + "non-dyadic scalar coefficient") + halvings = denominator.bit_length() - 1 + if op == "scale": + require(numerator & (numerator-1) == 0, "non-power-of-two scale") + cost = abs(numerator.bit_length()-1-halvings) + int(q < 0) + else: + # Clear; b-1 doubles; popcount additions; e halvings; + # signed accumulation; clear. Total b+popcount+e+2. + require(scalar[1] != scalar[2], "self-addition") + cost = numerator.bit_length() + numerator.bit_count() + halvings + 2 + coefficient_work += cost + primitives += 2*cost # Real and imaginary components. + else: + require(tag in ("adapter", "phase"), "unknown program event") + require(wrappers["pre"] == wrappers["post"], "unpaired wrappers") + return dict(events=len(events), macros=macros, real_component_primitives=primitives, + coefficient_work_primitive_count=coefficient_work, + pre_wrappers=len(wrappers["pre"]), post_wrappers=len(wrappers["post"]), + paid_profile=dict(sorted(paid.items()))) + + +def check_roles(roles, dispatch, widths): + seen = set() + for role in roles: + call = role["stage"], role["replica"] + require(call in dispatch, "unknown helper call") + key = (*call, role["helper"]) + require(key not in seen, "duplicate helper role") + seen.add(key) + row = widths[dispatch[call]] + require(0 <= role["helper"] < len(row), "helper index outside provider") + require(role["width"] == row[role["helper"]], "literal helper width") + expected = {(*call, h) for call, pid in dispatch.items() for h in range(len(widths[pid]))} + require(seen == expected, "incomplete helper role coverage") + return len(seen) + + +def recount(owner, invoice, spec): + parent = read(BASE / "split-centres/CANONICAL-WORD.json.gz") + plan = read(PACKAGE / "data/PLAN.json") + dispatch = {(s, r): pid for s, r, pid in spec["dispatch"]} + stages, replicas, blocks = plan["L"], plan["T"], plan["K"] + v, dimension, parent_helpers = parent["v"], parent["h"], parent["R"] + require(set(dispatch) == {(s, r) for s in range(stages) for r in range(replicas)}, + "incomplete call grid") + require(len(dispatch) == len(spec["dispatch"]), "duplicate dispatch") + providers, widths, program_counts = {}, {}, {} + for pid, receipt in invoice["providers"].items(): + word = read(BASE / "providers" / pid / "CANONICAL-WORD.json.gz") + programs = read(BASE / "providers" / pid / "LOCAL-PROGRAMS.json.gz") + width, entrance, codim = widths_from_word(word) + widths[pid] = width + require((word["v"], word["h"]) == (v, dimension), "provider geometry") + require(receipt["helpers"] == word["R"] == len(width), "provider helper count") + require(receipt["n"] == 2*v + len(width), "provider column count") + require(receipt["widths"] == width, "receipt width vector") + require(receipt["entrance_rank"] == entrance and receipt["terminal_codimension"] == codim, + "endpoint rank totals") + require(sum(width) == dimension*len(width) - entrance - codim, "width conservation") + require(set(programs) == {"forward", "backward"}, "missing orientation") + counts = {orientation: price_program(events) for orientation, events in programs.items()} + for orientation, count in counts.items(): + for key, value in count.items(): + expected = receipt["paid_profile"] if key == "paid_profile" else receipt["local"][orientation][key] + require(canonical(value) == expected, "program recount: " + pid + ":" + orientation + ":" + key) + program_counts[pid] = counts + children = sum(counts["forward"]["paid_profile"].values()) + adapters = 16*(max(c["macros"] for c in counts.values()) + children + 2*v + len(width) + + len(word["centers"])) + 64*plan["M"] + require(adapters == receipt["local_adapters"], "local adapter count") + providers[pid] = dict(helpers=len(width), columns=2*v+len(width), entrance_rank=entrance, + terminal_codimension=codim, width_sum=sum(width), + width_inventory=dict(sorted(Counter(width).items())), local_adapters=adapters, + local=counts) + require(set(providers) == set(dispatch.values()), "provider dispatch coverage") + require(len({p["helpers"] for p in providers.values()}) == 1, "mixed helper counts") + helpers = next(iter(providers.values()))["helpers"] + require(invoice["helpers"] == helpers, "invoice helper count") + roles = read(PACKAGE / "data/OWNERS.json.gz") + role_count = check_roles(roles, dispatch, widths) + require(role_count == owner["hosted_residuals"] == owner["actual_helper_owner_charts"], + "hosted helper count") + require(owner["owners_per_call"] == 2*v+helpers, "owner column count") + + helper_map = read(REPLAY / "ck-base-k_triangle-construction/HELPER-MAP.json") + mapping = {int(a): b for a, b in helper_map["map"].items()} + removed = set(helper_map["removed_504_helpers"]) + require(set(mapping).isdisjoint(removed) and set(mapping) | removed == set(range(2*v+parent_helpers)), + "helper map domain") + require(len(mapping) == len(set(mapping.values())) == 2*v+helpers + and set(mapping.values()) == set(range(2*v+helpers)), "helper map bijection") + original_spots = (270, 282, 294, 306) + mapped_spots = [mapping[2*v+h] - 2*v for h in original_spots] + require(mapped_spots == spec["width_spot_helpers"], "helper spot translation") + require(all(row[h] == 8 for row in widths.values() for h in mapped_spots), "mapped spot widths") + + data = 2*v*blocks*replicas + centres = len(parent["centers"]) + parent_live = data + stages*parent_helpers + parent_physical = parent_live + parent_helpers + centres + 2 + physical = data + helpers + centres + 2 + require(data == invoice["live"] == owner["live"] and physical == invoice["physical"] == owner["physical"], + "physical stock") + require(invoice["physical_stock_identity"] == dict(data_and_owner_families=data, local_helpers=helpers, + private_centres=centres, coefficient_work=2), "stock categories") + selected = [program_counts[pid]["backward" if stage % 2 else "forward"] + for (stage, replica), pid in dispatch.items()] + scalar = sum(c["real_component_primitives"] for c in selected) + factors_per_wrapper = 2*(plan["M"]-1) + wrappers = factors_per_wrapper*sum(c["pre_wrappers"]+c["post_wrappers"] for c in selected) + require(scalar == invoice["selected_real_component_primitives"], "selected scalar charge") + require(wrappers == invoice["wrapper_elementary_factors_charged"], "selected wrapper charge") + bridges, shifts = 2*v*len(dispatch), blocks*v*replicas + # The parent idle count is a pinned inherited input, not independently + # reconstructed from the omitted parent GLOBAL-TEMPLATE in this audit. + terms = dict(data_routes=blocks*v*len(dispatch), port_routes=2*v*len(dispatch), + helper_routes=2*role_count, parent_idle=owner["source_idle_children_charged"], + parent_banks=parent_live-data, bridges=bridges, shifts=shifts, moves=2*shifts, + parent_live=parent_live, parent_physical=parent_physical, wrappers=wrappers) + compiler = 64*(plan["M"]+1)**3 + adapters = max(p["local_adapters"] for p in providers.values()) + outside = 8*sum(terms.values()) + 64*plan["M"] + unhosted = (scalar + bridges + 3*shifts + parent_live + + (len(dispatch)*adapters + outside)*compiler + 64*parent_physical) + rebased = unhosted + 65*(physical-parent_physical) + data-parent_live + require((unhosted, rebased) == (invoice["unhosted_pervertex"], invoice["hosted_rebased_pervertex"]), + "complete finite invoice recount") + return dict(provider_helpers=helpers, parent_helpers=parent_helpers, helper_roles=role_count, + data_rows=data, physical_rows=physical, parent_live=parent_live, parent_physical=parent_physical, + removed_parent_registers=sorted(removed), mapped_spots=mapped_spots, + old_spot_widths={pid: [row[h] for h in original_spots] for pid, row in widths.items()}, + providers=providers, nonlocal_items=terms, unhosted_pervertex=unhosted, + hosted_rebased_pervertex=rebased, + stale_provider_route_overcharge=2*len(dispatch)*(parent_helpers-helpers)*8*compiler, + substituted_parent_bank_undercharge=stages*(parent_helpers-helpers)*8*compiler) + + +# Exactly the 14 assemble.* rows in the pinned PROOF-NOTE-R table. Replacements +# occur once in executable source, without mutating either input receipt. +MUTATIONS = [ + ("assemble.R", "R=invoice['helpers'];", "R=504;", "R=invoice['helpers'];"), + ("assemble.owners_per_call", "owner['owners_per_call']==2*112+R", "owner['owners_per_call']==728", "assert owner['owners_per_call']"), + ("assemble.hosted_72R", "==72*R==pin(", "==72*504==pin(", "assert owner['owners_per_call']"), + ("assemble.stock_helpers", "local_helpers=R,", "local_helpers=504,", "assert invoice['physical_stock_identity']"), + ("assemble.provider_helpers", "assert p['helpers']==R and", "assert p['helpers']==504 and", "assert p['helpers']==R and"), + ("assemble.provider_n", "p['n']==2*112+R", "p['n']==728", "assert p['helpers']==R and"), + ("assemble.width_sum", "==9*R-p['entrance_rank']", "==9*504-p['entrance_rank']", "assert sum(p['widths'])"), + ("assemble.width_len", "len(p['widths'])==R", "len(p['widths'])==504", "assert sum(p['widths'])"), + ("assemble.exact_columns", "z['all_exact_columns']==2*112+R", "z['all_exact_columns']==728", "assert z['all_exact_columns']"), + ("assemble.dirty_columns", "z['dirty_helper_columns']==R", "z['dirty_helper_columns']==504", "assert z['all_exact_columns']"), + ("assemble.local_adapters", "p['children']+2*112+R+8", "p['children']+728+8", "assert p['local_adapters']"), + ("assemble.route_items", "+2*72*R+", "+2*72*504+", "assert invoice['unhosted_pervertex']"), + ("assemble.parent_banks", "+9*parent_banks+", "+9*504+", None), + ("assemble.spot_width8", "for h in SPOT)", "for h in (270,282,294,306))", "pin(K+'width_digest'"), +] + + +def replace_once(source, old, new): + require(source.count(old) == 1, "mutation must match exactly once: " + old) + require(old.count("\n") == new.count("\n"), "mutation changed line numbering") + return source.replace(old, new) + + +def line_number(source, fragment): + matches = [i for i, line in enumerate(source.splitlines(), 1) if fragment in line] + require(len(matches) == 1, "ambiguous failure location: " + fragment) + return matches[0] + + +def execute_source(source, filename): + namespace = {"__name__": "k492_audit_subject", "__file__": str(ROOT/ASSEMBLER)} + exec(compile(source, filename, "exec"), namespace) + return namespace["assemble"] + + +def source_controls(owner, invoice, expected, spec_path, dependency): + os.environ["WITNESS_SPEC"] = str(spec_path) + os.environ["GAIN_PR564_SOURCE"] = str(dependency) + os.environ.pop("WITNESS_DISCOVER", None) + os.environ.pop("WITNESS_RECORD", None) + witness_path = ROOT/PACKAGE/"code/witness.py" + witness_spec = importlib.util.spec_from_file_location("witness", witness_path) + witness = importlib.util.module_from_spec(witness_spec) + witness_spec.loader.exec_module(witness) + sys.modules["witness"] = witness + source = (ROOT/ASSEMBLER).read_text() + documented = (ROOT/PACKAGE/"PROOF-NOTE-R.md").read_text() + documented_sites = {line.split("|")[1].strip() for line in documented.splitlines() + if line.startswith("| assemble.")} + require({row[0] for row in MUTATIONS} == documented_sites, "documented assembly-site coverage") + owner_hash = sha((ROOT/AUDIT/"OWNERS-AND-PROFILE.json").read_bytes()) + invoice_hash = sha((ROOT/AUDIT/"PREFIX-AND-INVOICE.json").read_bytes()) + + def invoke(text, label): + filename = str(ASSEMBLER) + "::" + label + function = execute_source(text, filename) + return filename, function + + _, baseline = invoke(source, "baseline") + require(canonical(baseline(owner, invoice, owner_hash, invoice_hash)) == expected, + "unchanged assembly differs from selected receipt") + rows = [] + controls = MUTATIONS + [ + ("control.parent_banks_use_provider_R", "+9*parent_banks+", "+9*R+", "assert invoice['unhosted_pervertex']"), + ("control.equivalent_provider_count", "R=invoice['helpers'];", "R=504-12;", None), + ] + for name, old, new, failure in controls: + mutated = replace_once(source, old, new) + filename, function = invoke(mutated, name) + wanted_line = line_number(source, failure) if failure else None + try: + result = function(owner, invoice, owner_hash, invoice_hash) + except AssertionError as error: + trace = error.__traceback__ + while trace.tb_next: + trace = trace.tb_next + require(wanted_line is not None and trace.tb_frame.f_code.co_filename == filename + and trace.tb_lineno == wanted_line, "unrelated rejection: " + name) + outcome = "rejected_at_expected_assertion" + else: + require(wanted_line is None, "invalid source reversion accepted: " + name) + require(canonical(result) == expected, "positive control changed assembly: " + name) + outcome = "accepted_identical_assembly" + rows.append(dict(name=name, original=old, replacement=new, outcome=outcome, + assertion_line=wanted_line, mutated_source_sha256=sha(mutated.encode()))) + return rows + + +def negative_controls(): + caught = [] + + def reject(name, fn, message): + try: + fn() + except AuditError as error: + require(str(error) == message, "unrelated audit rejection: " + name) + caught.append(name) + else: + raise AuditError("audit control accepted: " + name) + + word = read(BASE/"providers/ck/CANONICAL-WORD.json.gz") + bad = copy.deepcopy(word) + bad["R"] = 504 + reject("stale_native_helper_count", lambda: widths_from_word(bad), "native register count") + dependent = copy.deepcopy(word) + dependent["frames"][1].append(dependent["frames"][1][0]) + reject("dependent_frame_basis", lambda: widths_from_word(dependent), "dependent frame basis") + role = dict(stage=0, replica=0, helper=0, width=9) + reject("missing_helper_role", lambda: check_roles([], {(0, 0): "p"}, {"p": [9]}), + "incomplete helper role coverage") + reject("duplicate_helper_role", lambda: check_roles([role, role], {(0, 0): "p"}, {"p": [9]}), + "duplicate helper role") + wrong = dict(role, width=8) + reject("wrong_helper_width", lambda: check_roles([wrong], {(0, 0): "p"}, {"p": [9]}), + "literal helper width") + reject("unpinned_source", lambda: check_pin(b"changed", sha(b"original"), "control"), + "source hash mismatch: control") + reject("absent_mutation_anchor", lambda: replace_once("abc", "missing", "x"), + "mutation must match exactly once: missing") + reject("ambiguous_mutation_anchor", lambda: replace_once("abcabc", "abc", "x"), + "mutation must match exactly once: abc") + # Exact oracle for the independent scalar cost formula, including a signed + # multi-bit numerator. These are counts of the retained implementation. + toy = [["scalar", ["add", ["L", 0], ["L", 1], -13, 8], 0]] + require(price_program(toy)["real_component_primitives"] == 24, "Horner formula control") + toy[0][1][-1] = 16 + require(price_program(toy)["real_component_primitives"] == 26, "halving charge control") + return caught + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a receipt instead of comparing EXPECTED.json") + args = parser.parse_args() + # Imported production verifiers use assert as admission checks. + require(__debug__, "run without -O: the audited source requires assertions") + sys.dont_write_bytecode = True + sys.set_int_max_str_digits(0) + pins = json.loads((HERE/"SOURCE.json").read_text()) + for relative, digest in pins["files"].items(): + check_pin((ROOT/relative).read_bytes(), digest, relative) + owner = read(AUDIT/"OWNERS-AND-PROFILE.json") + invoice = read(AUDIT/"PREFIX-AND-INVOICE.json") + spec = read(PACKAGE/"data/SPEC.json") + expected = read(REPLAY/"ASSEMBLY.json") + accounting = recount(owner, invoice, spec) + mutations = source_controls(owner, invoice, expected, ROOT/PACKAGE/"data/SPEC.json", + ROOT/pins["assembly_dependency"]) + controls = negative_controls() + result = canonical(dict(status="PASS_SCOPED_K492_HELPER_ACCOUNTING_AUDIT", base_commit=pins["base_commit"], + selected_kappa=expected["kappa"], documented_sites=len(MUTATIONS), + accounting=accounting, source_controls=mutations, audit_controls=controls)) + if args.output: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True)+"\n") + else: + require(result == json.loads((HERE/"EXPECTED.json").read_text()), "audit receipt mismatch") + print(result["status"], "documented_sites=14 rejected=13 equivalent=1", + "additional_source_controls=2 audit_controls=" + str(len(controls))) + + +if __name__ == "__main__": + main() From 56bac6775e8882f4c3bfa0cef9bcc9a61da9ba06 Mon Sep 17 00:00:00 2001 From: Gabriel Roa Date: Tue, 13 Oct 2026 02:19:07 -0300 Subject: [PATCH 2/2] Record completed audit and PR 766 handoff --- .../k492-helper-accounting-audit/CLAIM.json | 30 ++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/research/k492-helper-accounting-audit/CLAIM.json b/research/k492-helper-accounting-audit/CLAIM.json index e0dc012198..74e6777fe8 100644 --- a/research/k492-helper-accounting-audit/CLAIM.json +++ b/research/k492-helper-accounting-audit/CLAIM.json @@ -39,5 +39,33 @@ "open_pr_max": 720, "overlap": "Read relevant open PR metadata and central ledger; #675 covers owner timing/bridge omission, #706 covers independent moment bounds. Neither supplies the documented source-reversion controls. #626 is incorporated at selected pin; no existing PR will be modified." }, - "status": "claimed" + "status": "completed and submitted", + "handoff": { + "completed_at_utc": "2026-10-13T05:19:07.318337+00:00", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/766", + "branch": "audit/k492-helper-accounting-seed73", + "result": "All 14 documented assembly source reversions replayed: 13 intended assertion rejections and 1 full-receipt-identical parent-bank control. Additional independent native width/role/program recount, two source controls and eight harness/recount controls pass. No current implementation defect or new kappa claimed.", + "verification_started_by_utc": "2026-10-13T05:15:00Z", + "verification": [ + "Deterministic audit receipt match", + "All 114 existing production assembly admission controls", + "make selected-record-check", + "Minimal 23-input export from unrelated working directory", + "Corrupt source and expected-receipt exports rejected", + "Optimized Python explicitly refused", + "git diff --cached --check" + ], + "final_overlap_snapshot": { + "open_pr_count": 582, + "highest_pr_number": 763, + "concurrent_pr": 724, + "concurrent_head": "624ccfe44b1c5816f0279481d91cca6a5a2290ab", + "additional_coverage": "Compared PR724 source: it replays an AST-selected invoice/finite-guard slice with 7 source rejections and 1 equivalent control. This result replays all 14 documented assembly sites, including earlier provider/width/column/index checks, executes the entire assembly, and counts operations from all four local programs. Matching invoice deltas are credited corroboration, not priority." + }, + "unresolved": [ + "Original other 18 scratch sites and R=504 fixture not reproduced", + "Parent idle count, archived local algebra/restoration/phase admission and all-size/physical/analytic obligations remain inherited", + "No full make verify, cold supplier reconstruction, remote CI or formal theorem verification claimed" + ] + } }