From 34a7003866390618b8e8006dc483e7a37a37903f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 17:36:11 +0100 Subject: [PATCH] test(research): audit joint rank-seven frame paths --- research/rank7-joint-frame-audit/README.md | 137 +++ research/rank7-joint-frame-audit/RESULT.json | 806 ++++++++++++++++++ research/rank7-joint-frame-audit/SOURCES.json | 72 ++ research/rank7-joint-frame-audit/TASK.json | 92 ++ research/rank7-joint-frame-audit/VERIFY.json | 51 ++ research/rank7-joint-frame-audit/frames.py | 236 +++++ research/rank7-joint-frame-audit/lowering.py | 90 ++ .../rank7-joint-frame-audit/test_verify.py | 128 +++ research/rank7-joint-frame-audit/verify.py | 258 ++++++ 9 files changed, 1870 insertions(+) create mode 100644 research/rank7-joint-frame-audit/README.md create mode 100644 research/rank7-joint-frame-audit/RESULT.json create mode 100644 research/rank7-joint-frame-audit/SOURCES.json create mode 100644 research/rank7-joint-frame-audit/TASK.json create mode 100644 research/rank7-joint-frame-audit/VERIFY.json create mode 100644 research/rank7-joint-frame-audit/frames.py create mode 100644 research/rank7-joint-frame-audit/lowering.py create mode 100644 research/rank7-joint-frame-audit/test_verify.py create mode 100644 research/rank7-joint-frame-audit/verify.py diff --git a/research/rank7-joint-frame-audit/README.md b/research/rank7-joint-frame-audit/README.md new file mode 100644 index 0000000000..abbc970fc9 --- /dev/null +++ b/research/rank7-joint-frame-audit/README.md @@ -0,0 +1,137 @@ +# Independent joint rank-seven frame audit + +Both #2979 providers pass a code-disjoint chronological frame recount. The +five isolated groups sum to its stage-one invoice. No finite frame defect was +found. This is a partial audit, not supplier admission or a new kappa. + +## Shared overhead, with losing controls + +For V45, keep the group's 61 gate-frame edits fixed and lower any `k` of +helpers `{249,251,265,267}` from rank eight to rank seven. All 16 endpoint +subsets pass the literal frame and unchanged cleanup-syntax checks. Their +exact paid-profile difference from the parent is + +```text +Delta(k) = (2-k) H1 + 10 H2 + 6 H3 - 10 H4, 0 <= k <= 4. +``` + +Here `Hr` means one rank-`r` child, not a numerical tariff. Thus the partner +cost is paid once and each additional endpoint saves exactly `H1`. The result +holds for any additive rank tariff on these fixed paths. It does not optimize +frames for the proper subsets or prove a global single-lowering bound. + +Substituting the source's integer surrogate prices and its approximate +2,091,300-unit width guide gives the following margins: + +| Lowered endpoints | Number of subsets | Guide margin per subset | +|---:|---:|---:| +| 0 | 1 | -78,512 | +| 1 | 4 | -53,141 | +| 2 | 6 | -27,770 | +| 3 | 4 | -2,399 | +| 4 | 1 | +22,972 | + +These reproduce the source's comparison, but **the guide is not a certified +physical idle tariff**. A positive guide margin does not establish a complete +supplier saving. The symbolic identity above is independent of the guide. + +## Whole stage and final boundary + +The checker partitions all 139 edits by their unique containing group space, +checks each old gate and frame, and reconstructs each group independently. +No scalar, operator, entrance or cleanup gate changes in stage one. + +| Group | Exact paid-profile delta | Gate-frame edits | +|---|---|---:| +| V45 | `-2 H1 +10 H2 +6 H3 -10 H4` | 61 | +| A | `-H1 +20 H2 -14 H3 +2 H4 -2 H5` | 21 | +| B | `-H1 +20 H2 -14 H3 +2 H4 -2 H5` | 21 | +| C | `20 H2 -14 H3 +2 H4 -2 H5` | 18 | +| D | `20 H2 -14 H3 +2 H4 -2 H5` | 18 | + +Their sum is `-4 H1 +90 H2 -50 H3 -2 H4 -8 H5`. Paid rank mass falls +5,166 to 5,144, and helper-width mass falls 3,310 to 3,288. Both providers +also reproduce the shipped final local profile, of mass 5,139, and its +six-width inventory, of mass 3,283. The 408 live helpers remain present. + +The inverse-cleanup syntax and endpoint/buffer bijection give 86 private names +before and after stage one, and 91 in the final word. This counts names; it +neither proves their zero return nor supplies physical storage admission. + +The actual dispatch has 250 base and 416 extra calls. Multiplying the checked +final local profiles by those counts leaves +`17310 H1 +4956 H3 +1728 H5 +28190 H48` when subtracted from the source's +claimed complete invoice. `RESULT.json` labels this remainder conditional: +this check does not reconstruct owner geometry or establish that subtraction +as an independently certified idle bill. [#2987](https://github.com/CrocSwap/integer-mult-bounds/pull/2987) +is the separate chronological-packing audit, not a substitute for native or +physical admission. + +## Evidence and reproduction + +Exact source [#2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979) +is `be191346391661f4d35fc0d1508d0a6029572576`; scientific base is +`836b19bfa309ceafbc8ee32a15e8c4b10dde7e11`, priority revision 6. +All nine live inputs match that original PR's bytes and are bound by Git blob +and SHA256 in `SOURCES.json`. No predecessor Python code is imported or run. +The original author and all inherited source notices retain their attribution. + +```sh +python3.12 scripts/research_package.py --package research/rank7-joint-frame-audit +# Direct deterministic JSON, without Git or a network connection: +python3.12 -B research/rank7-joint-frame-audit/verify.py +``` + +`RESULT.json` records both providers, every subset, each isolated symbolic +invoice, chronological-event hashes and 18 deliberate rejections. Controls +cover stale invoices, a wrong rank-seven space, an omitted gate edit, widened +ends, singular warps, missing cleanup, wrong private names, stale preimages and +extra edits. Five unittest methods also test explicit subspaces, charged +climbs, warp maps, normal/optimized command equality, a Git-free export and +corrupted-source rejection. All acceptance checks survive Python `-O`. + +The scope is exact finite frame accounting and cleanup syntax. The scalar +free-operator maps, symplectic/Clifford phases, arbitrary-dirty-input and +private-zero return, owner embedding, full storage, prefix/precision/tape, +outer release and all-size/compiler implications remain unverified here. +The selected bit/complex caps and selected frontier are unchanged. No new +proof-assistant, native build or complete cold replay was run. + +## Implementation limits + +The frame oracle expands at most 512 points from nine generators, with a +4,096-entry cache. Words have 704 slots, at most 480 warps and 10,000 gates +per section. Input authentication precedes decoding, capped at 2 MB raw and +8 MB decoded per file. All loops traverse these finite domains, five groups +or 16 subsets; no recursion is used. Functions are below 60 physical lines. + +Python's managed allocations are a rule-3 deviation from fixed allocation. +The bounds above limit live collections; the cache stores immutable sets. +Rule 9's callback deviation is confined to the nine local rejection actions; +all targets are visible in `controls`. The standard-library cache decorator +only memoizes `span`; it does not generate or evaluate code. Replacing either +mechanism is warranted only if these finite limits or the checker API change. +Diagnostics use `ruff check --select E4,E7,E9,F,B,I`, `ruff format --check` and +Python development-mode warnings as errors. No shared CI settings change. + +## Open next questions + +Can the independently checked final frame paths and #2987 owner geometry be +joined to one independently checked native residual/phase and physical invoice? +This decides whether the local benefit survives its actual consumer. Start +with one lowered V45 helper's native frame-transition recipe, bind it to this +ledger's chronological events, and check both orientations and its private +buffer endpoint. The missing native/phase, physical storage and precision +bindings block supplier admission; another surrogate-price calculation does +not close them. The full #2979 release remains a separate, larger audit. + +## Credit + +Marius-Paul Dumitrean/#2979 and #2942 supplied the joint construction and +literal words. Jeremy Kothe supplied the frame/cleanup lineage and #2957 +rewrites; Mason Hale/#2917 and Jeremy Diviney/#2908 supplied the paired +extraction chain. This complements ToikY/#2932's older frame ledger and +Ross Richardson's #2960/#2974/#2987 algebra, invoice and packing audits. +Retain Yiyang Lu, Dugongue, Tekalign, icekylinx and the original geometry, +native, owner and compiler contributors' credit. New check by Nick Petalas, +Apache-2.0. No independent human or formal-kernel review is claimed. diff --git a/research/rank7-joint-frame-audit/RESULT.json b/research/rank7-joint-frame-audit/RESULT.json new file mode 100644 index 0000000000..ed620a2bc2 --- /dev/null +++ b/research/rank7-joint-frame-audit/RESULT.json @@ -0,0 +1,806 @@ +{ + "invoice_boundary": { + "calls": { + "extra": 416, + "gauge44": 250 + }, + "conditional_idle_remainder": { + "1": 17310, + "3": 4956, + "5": 1728, + "48": 28190 + }, + "derived_local_profile": { + "1": 1628370, + "2": 470196, + "3": 154512, + "4": 71928, + "5": 11988, + "8": 5328 + }, + "source_claimed_complete_profile": { + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "5": 13716, + "8": 5328, + "48": 28190 + }, + "warning": "Remainder is subtraction from a source claim, not an owner replay. PR2987 independently checks the packing bridge; native and physical admission remain separate." + }, + "providers": { + "base": { + "V45_subsets": [ + { + "helpers": [], + "profile_delta": { + "1": 2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": 78512, + "surrogate_margin": -78512 + }, + { + "helpers": [ + 249 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 251 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 265 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 267 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 249, + 251 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 265 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 251, + 265 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 251, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 265, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 251, + 265 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 251, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 265, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 251, + 265, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 251, + 265, + 267 + ], + "profile_delta": { + "1": -2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -8388172, + "surrogate_margin": 22972 + } + ], + "chronological_event_sha256": [ + "d2bd274279bf9ed0ebf2fa2f55647698cfc03a249318a9287d319c8bbf7a74f1", + "80b46461106259250a8425fa60710460196b74a90066a820ad3d5f1db50d5488", + "1a70ebe616244a79d651632cddb0e70367af1a0a632829124796857ff9431556" + ], + "cleanup_namespaces": [ + { + "cleanup_gates": 4992, + "private_buffers": 86 + }, + { + "cleanup_gates": 4992, + "private_buffers": 86 + }, + { + "cleanup_gates": 5207, + "private_buffers": 91 + } + ], + "controls": { + "extra_edit": "139 declared gate edits", + "missing_cleanup": "cleanup length", + "omitted_frame_edit": "('nonmonotone', ('restore', 126), 62)", + "singular_warp": "invertible warp", + "stale_gate_preimage": "gate edit preimage", + "stale_report": "paid report mismatch", + "widened_endpoint": "paid report mismatch", + "wrong_private_name": "inverse cleanup syntax", + "wrong_rank7_space": "('nonmonotone', ('end', 249), 249)" + }, + "final": { + "profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + "groups": { + "A": { + "gate_frame_edits": 21, + "profile_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -10499041, + "surrogate_margin": 42541, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "B": { + "gate_frame_edits": 21, + "profile_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -10499041, + "surrogate_margin": 42541, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "C": { + "gate_frame_edits": 18, + "profile_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -8382370, + "surrogate_margin": 17170, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "D": { + "gate_frame_edits": 18, + "profile_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -8382370, + "surrogate_margin": 17170, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "V45": { + "gate_frame_edits": 61, + "profile_delta": { + "1": -2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -8388172, + "surrogate_margin": 22972, + "width_delta": { + "7": 4, + "8": -4 + } + } + }, + "parent": { + "profile": { + "1": 2434, + "2": 632, + "3": 286, + "4": 104, + "5": 26, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "7": 62, + "8": 100, + "9": 218 + } + }, + "stage_one": { + "profile": { + "1": 2430, + "2": 722, + "3": 236, + "4": 102, + "5": 18, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 94, + "9": 218 + } + } + }, + "extra": { + "V45_subsets": [ + { + "helpers": [], + "profile_delta": { + "1": 2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": 78512, + "surrogate_margin": -78512 + }, + { + "helpers": [ + 249 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 251 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 265 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 267 + ], + "profile_delta": { + "1": 1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -2038159, + "surrogate_margin": -53141 + }, + { + "helpers": [ + 249, + 251 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 265 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 251, + 265 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 251, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 265, + 267 + ], + "profile_delta": { + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -4154830, + "surrogate_margin": -27770 + }, + { + "helpers": [ + 249, + 251, + 265 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 251, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 265, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 251, + 265, + 267 + ], + "profile_delta": { + "1": -1, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -6271501, + "surrogate_margin": -2399 + }, + { + "helpers": [ + 249, + 251, + 265, + 267 + ], + "profile_delta": { + "1": -2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -8388172, + "surrogate_margin": 22972 + } + ], + "chronological_event_sha256": [ + "d2bd274279bf9ed0ebf2fa2f55647698cfc03a249318a9287d319c8bbf7a74f1", + "80b46461106259250a8425fa60710460196b74a90066a820ad3d5f1db50d5488", + "1a70ebe616244a79d651632cddb0e70367af1a0a632829124796857ff9431556" + ], + "cleanup_namespaces": [ + { + "cleanup_gates": 4992, + "private_buffers": 86 + }, + { + "cleanup_gates": 4992, + "private_buffers": 86 + }, + { + "cleanup_gates": 5207, + "private_buffers": 91 + } + ], + "controls": { + "extra_edit": "139 declared gate edits", + "missing_cleanup": "cleanup length", + "omitted_frame_edit": "('nonmonotone', ('restore', 126), 62)", + "singular_warp": "invertible warp", + "stale_gate_preimage": "gate edit preimage", + "stale_report": "paid report mismatch", + "widened_endpoint": "paid report mismatch", + "wrong_private_name": "inverse cleanup syntax", + "wrong_rank7_space": "('nonmonotone', ('end', 249), 249)" + }, + "final": { + "profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + "groups": { + "A": { + "gate_frame_edits": 21, + "profile_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -10499041, + "surrogate_margin": 42541, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "B": { + "gate_frame_edits": 21, + "profile_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -10499041, + "surrogate_margin": 42541, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "C": { + "gate_frame_edits": 18, + "profile_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -8382370, + "surrogate_margin": 17170, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "D": { + "gate_frame_edits": 18, + "profile_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "surrogate_delta": -8382370, + "surrogate_margin": 17170, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "V45": { + "gate_frame_edits": 61, + "profile_delta": { + "1": -2, + "2": 10, + "3": 6, + "4": -10 + }, + "surrogate_delta": -8388172, + "surrogate_margin": 22972, + "width_delta": { + "7": 4, + "8": -4 + } + } + }, + "parent": { + "profile": { + "1": 2434, + "2": 632, + "3": 286, + "4": 104, + "5": 26, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "7": 62, + "8": 100, + "9": 218 + } + }, + "stage_one": { + "profile": { + "1": 2430, + "2": 722, + "3": 236, + "4": 102, + "5": 18, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 94, + "9": 218 + } + } + } + }, + "scope": "Finite chronological frame paths, exact symbolic paid deltas and cleanup syntax/names only. Surrogate margins do not certify the complete physical cost or a new kappa.", + "status": "PASS_INDEPENDENT_RANK7_JOINT_FRAME_AUDIT" +} diff --git a/research/rank7-joint-frame-audit/SOURCES.json b/research/rank7-joint-frame-audit/SOURCES.json new file mode 100644 index 0000000000..9ad95fc60e --- /dev/null +++ b/research/rank7-joint-frame-audit/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "4450dbbd1d01929022259f523234590f4cce65b9", + "sha256": "ca056a6def333df7afd822c1f34adc2eaa9089b241fc2bdd5803b64066fc9355" + }, + { + "path": "research/rank7-joint-endframes/allocation/DISPATCH.json", + "usage": "input", + "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e", + "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf" + }, + { + "path": "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "usage": "input", + "git_blob": "b06b369ace05b86377f9f73e13586b62b0b77b98", + "sha256": "dfb7d06724bf95367f3fdb398f4828fc70f803d23030bc0eee0b00541457f546" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "usage": "input", + "git_blob": "1ca8287d6ae5eb45d87db65b369be8d09ba692b2", + "sha256": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "usage": "input", + "git_blob": "c39913ce24cbce4c841eabcc9b1e5a18e4ccc754", + "sha256": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6" + }, + { + "path": "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "usage": "input", + "git_blob": "66525d293bd0e615e469b4c2191281e8cafb8788", + "sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + } + ] +} diff --git a/research/rank7-joint-frame-audit/TASK.json b/research/rank7-joint-frame-audit/TASK.json new file mode 100644 index 0000000000..64791e5149 --- /dev/null +++ b/research/rank7-joint-frame-audit/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independent explicit-subspace frame recount of PR2979's parent, joint stage one and shipped final words on both providers; isolated five-group invoices and all 16 fixed-partner V45 endpoint subsets; cleanup syntax and buffer names; conditional local-to-complete-invoice boundary.", + "scope_change_reason": "PR2987 already checks chronological packing but assumes native width derivation. This audit closes the new joint rank-seven chronological frame-path implication, without duplicating its cut or treating a surrogate margin as complete physical admission.", + "bottleneck_link": "Tests whether the changed helper boundaries really deliver the claimed local rank savings before pricing their still-separate physical consumer.", + "budget_minutes": 60, + "stop_rule": "Stop after the finite frame implication and source-impact handoff. Do not expand to lowering searches, native or all-size supplier admission.", + "outcome": "partial", + "evidence": "RESULT.json; five unittest methods, 18 scoped frame/syntax rejections and a source-byte rejection; README.md distinguishes checked identities from the conditional idle remainder and unverified physical/outer costs.", + "author": "Nick Petalas", + "ai_assistance": "Automated assistance supported implementation and checks. No independent human review is claimed.", + "predecessor_head": "be191346391661f4d35fc0d1508d0a6029572576", + "picker_seed": "d819e2456a78b8e79f12bc659fea55ee", + "scope_key": "5e0f415b25b13c102653:2979-stage1-fixed-partner-V45-all-subsets", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18977778", + "freshness": { + "upstream_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "priority_revision": 6, + "checked_at_utc": "2026-10-16T16:34:29Z", + "relevant_guidance_changes": "none since session base", + "overlap_complete_pagination": true, + "open_pr_records": 234, + "closed_pr_records": 2440, + "discussion_records": 1703, + "warnings": [], + "limits": "Metadata/body/comment snapshots are non-atomic and omit arbitrary diffs and unpublished work. No novelty guarantee. PR2987 remains complementary." + }, + "verification": { + "registered_replay": "CPython 3.12.15, Linux, standard library only; PASS_REGISTERED_RESEARCH_PACKAGE", + "additional_interpreter": "CPython 3.13.5 optimized development-mode replay, byte-identical RESULT.json", + "unit_tests": 5, + "frame_and_cleanup_rejections": 18, + "corrupted_source_rejections": 1, + "formal_or_native_build": "not run", + "complete_supplier_cold_replay": "not run", + "independence": "No predecessor Python module is imported or executed. No independent human or formal-kernel review is claimed." + }, + "open_questions": [ + { + "question": "Can the checked final frame paths and PR2987 owner geometry be joined to independently checked native residual/phase and physical costs?", + "why_it_matters": "The local shared-overhead benefit is not a complete supplier saving unless the actual consumer, restoration and physical invoice fit.", + "first_step": "Bind one lowered V45 helper's native transition recipe to this ledger's chronological events and check both orientations plus its private-buffer endpoint.", + "blocked_by": "Native residual/phase, physical storage and prefix/precision bindings are outside this finite frame audit. The complete PR2979 release needs a separately budgeted audit." + } + ] +} diff --git a/research/rank7-joint-frame-audit/VERIFY.json b/research/rank7-joint-frame-audit/VERIFY.json new file mode 100644 index 0000000000..974d7fb5eb --- /dev/null +++ b/research/rank7-joint-frame-audit/VERIFY.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/allocation/DISPATCH.json", + "research/rank7-joint-endframes/allocation/ORDER.json", + "research/rank7-joint-endframes/allocation/PROFILE.json", + "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-X", + "dev", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both providers' chronological frames, five isolated groups, all 16 V45 subsets, exact profiles, cleanup syntax/names and 18 deliberate rejections. Idle subtraction is explicitly conditional." + }, + { + "argv": [ + "{python}", + "-B", + "-X", + "dev", + "-W", + "error", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_*.py" + ], + "timeout_seconds": 120, + "checks": "Explicit-subspace/climb/warp fixtures, normal/optimized equality, Git-free export and corrupted-source rejection." + } + ] +} diff --git a/research/rank7-joint-frame-audit/frames.py b/research/rank7-joint-frame-audit/frames.py new file mode 100644 index 0000000000..ae5454f9e2 --- /dev/null +++ b/research/rank7-joint-frame-audit/frames.py @@ -0,0 +1,236 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Explicit subsets of F2^9, not a Gaussian-elimination basis implementation. + +Independently implements the finite frame contract stated by PR2979 and its +PR2917/PR2894 lineage. No predecessor module is imported or executed. +""" + +from collections import Counter +from functools import lru_cache + + +class Invalid(ValueError): + """The literal word violates the scoped frame or cleanup contract.""" + + +def require(condition, label): + if not condition: + raise Invalid(str(label)) + + +@lru_cache(maxsize=4096) +def span(vectors): + require(len(vectors) <= 9, "at most nine frame generators") + points = {0} + for vector in vectors: + require(type(vector) is int and 0 < vector < 512, "nine-bit generator") + points |= {point ^ vector for point in points} + require(len(points) == 1 << len(vectors), "independent frame generators") + return frozenset(points) + + +def dimension(space): + return len(space).bit_length() - 1 + + +ZERO = span(()) +FULL = span(tuple(1 << bit for bit in range(9))) + + +def roles(gate): + require(gate[0] in ("add", "scale"), "scalar gate kind") + expected = 6 if gate[0] == "add" else 5 + require(len(gate) == expected, "scalar gate shape") + result = gate[1:3] if gate[0] == "add" else gate[1:2] + require(all(type(r) is int and 0 <= r < 704 for r in result), "register range") + return result + + +def boundaries(word): + require( + (word["report"]["v"], word["report"]["h"], word["report"]["R"]) + == (112, 9, 480), + "fixed geometry", + ) + ports = word["ports"] + require(len(ports) == len(set(ports)) == 112, "112 unique ports") + starts = [span((p,)) for p in ports] + [ZERO] * 592 + ends = ( + [FULL] * 112 + + [ + frozenset(x for x in range(512) if (x & p).bit_count() % 2 == 0) + for p in ports + ] + + [FULL] * 480 + ) + for field, frames in (("start_extra", starts), ("helper_final", ends)): + require(len(word[field]) <= 480, "bounded helper boundary") + for role, vectors in word[field].items(): + require(224 <= int(role) < 704, "helper boundary register") + frames[int(role)] = span(tuple(vectors)) + live = set(range(704)) - set(word["removed"]) + require(len(live) == 632 and set(range(224)) <= live, "live geometry") + widths = Counter() + for role in sorted(live - set(range(224))): + require(starts[role] <= ends[role], "entrance inside terminal frame") + widths[dimension(ends[role]) - dimension(starts[role])] += 1 + return starts, ends, live, dict(sorted(widths.items())) + + +def climb(current, paid, events, location, role, destination): + source = current[role] + require(source <= destination, ("nonmonotone", location, role)) + rank = dimension(destination) - dimension(source) + if rank: + paid[rank] += 1 + events.append( + [*location, role, dimension(source), dimension(destination), rank] + ) + current[role] = destination + + +def linear_image(columns, point): + result = 0 + for bit in range(9): + if point & (1 << bit): + result ^= columns[bit] + return result + + +def warp(current, role, columns, old, new, inverse=False): + require( + len(columns) == 9 and all(type(x) is int and 0 <= x < 512 for x in columns), + "warp columns", + ) + old, new = span(tuple(old)), span(tuple(new)) + require( + len({linear_image(columns, x) for x in range(512)}) == 512, "invertible warp" + ) + require(frozenset(linear_image(columns, x) for x in old) == new, "warp image") + source, target = (new, old) if inverse else (old, new) + require(current[role] == source, "warp entrance frame") + current[role] = target + + +def scalar_step(word, current, paid, events, section, index, gate): + if gate[0] == "warp": + require(len(gate) == 5, "A warp shape") + role, operator, old, new = gate[1:] + require(0 < abs(operator) <= len(word["warps"]), "A warp operator") + columns = word["warps"][abs(operator) - 1][2] + # The A gate declares its chronological source/target, even for G^-1. + if operator < 0: + warp(current, role, columns, new, old, inverse=True) + else: + warp(current, role, columns, old, new) + return + destination = span(tuple(gate[-1])) + for role in roles(gate): + climb(current, paid, events, (section, index), role, destination) + + +def centre_copies(word, current, paid, events): + require(len(word["centers"]) == len(word["center_frames"]) == 8, "eight centres") + for index, (role, frame) in enumerate( + zip(word["centers"], word["center_frames"], strict=True) + ): + source = span(tuple(frame)) + require(current[role] == source, "centre entrance") + readers = { + span(tuple(word["target_levels"].get(str(g[1] - 112), []))) + for g in word["cut"] + if g[2] == role + } + for target in sorted(readers, key=lambda s: (-len(s), tuple(sorted(s)))): + require(target <= source, "nested centre copy levels") + rank = dimension(source) - dimension(target) + if rank: + paid[rank] += 1 + events.append( + ["centre", index, role, dimension(source), dimension(target), rank] + ) + source = target + # These are copied readout paths. The main carrier frame is unchanged. + + +def ledger(word, check_report=True): + for section in ("A", "B", "restore", "cut", "cleanup"): + require(len(word[section]) <= 10000, "bounded section") + require(len(word["warps"]) <= 480, "bounded warps") + current, ends, live, widths = boundaries(word) + paid, events = Counter(), [] + for index, gate in enumerate(word["A"]): + scalar_step(word, current, paid, events, "A", index, gate) + for target in range(112): + require( + current[112 + target] + == span(tuple(word["target_levels"].get(str(target), []))), + "target level", + ) + centre_copies(word, current, paid, events) + by_position = {} + for position, role, columns, old, new in word["warps"]: + require(0 <= position <= len(word["B"]), "B warp position") + by_position.setdefault(position, []).append((role, columns, old, new)) + for index in range(len(word["B"]) + 1): + for role, columns, old, new in by_position.get(index, []): + warp(current, role, columns, old, new) + if index < len(word["B"]): + scalar_step(word, current, paid, events, "B", index, word["B"][index]) + for index, gate in enumerate(word["restore"]): + scalar_step(word, current, paid, events, "restore", index, gate) + for role in sorted(live): + climb(current, paid, events, ("end", role), role, ends[role]) + profile = dict(sorted(paid.items())) + if check_report: + require( + profile == {int(r): n for r, n in word["report"]["local_profile"].items()}, + "paid report mismatch", + ) + require( + widths == {int(r): n for r, n in word["report"]["width_inventory"].items()}, + "width report mismatch", + ) + return {"profile": profile, "widths": widths, "events": events} + + +def cleanup_namespace(word): + """Check the literal reverse/inverse syntax and names, not zero-return semantics.""" + require(0 <= word["prelude_events"] <= len(word["A"]), "prelude length") + restored = {int(h) for h in word["helper_final"]} + by_position = {} + for operator, record in enumerate(word["warps"], 1): + by_position.setdefault(record[0], []).append(["warp", record[1], operator]) + forward = list(word["A"][word["prelude_events"] :]) + for index in range(len(word["B"]) + 1): + forward.extend(by_position.get(index, [])) + if index < len(word["B"]): + forward.append(word["B"][index]) + forward.extend(word["restore"]) + inverse = [] + for gate in reversed(forward): + if 112 <= gate[1] < 224: + continue + kind, role = gate[:2] + target = role + 704 if role in restored else role + if kind == "warp": + inverse.append(["warp", target, -gate[2]]) + elif kind == "add": + source = gate[2] + 704 if gate[2] in restored else gate[2] + inverse.append(["add", target, source, -gate[3], gate[4]]) + else: + require(kind == "scale", "inverse gate kind") + inverse.append(["scale", target, gate[3], gate[2]]) + require(len(inverse) == len(word["cleanup"]), "cleanup length") + require(inverse == [g[:-1] for g in word["cleanup"]], "inverse cleanup syntax") + require( + all(span(tuple(g[-1])) == FULL for g in word["cleanup"]), "full cleanup frame" + ) + private = { + r + for g in word["cleanup"] + for r in (g[1:3] if g[0] == "add" else g[1:2]) + if r >= 704 + } + require(private == {704 + h for h in restored}, "cleanup endpoint/buffer bijection") + return {"private_buffers": len(private), "cleanup_gates": len(inverse)} diff --git a/research/rank7-joint-frame-audit/lowering.py b/research/rank7-joint-frame-audit/lowering.py new file mode 100644 index 0000000000..990338a274 --- /dev/null +++ b/research/rank7-joint-frame-audit/lowering.py @@ -0,0 +1,90 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Reconstruct only declared frame edits. Scalar/operator data stay untouched.""" + +from copy import deepcopy + +from frames import require, span + + +def difference(after, before): + return { + r: after.get(r, 0) - before.get(r, 0) + for r in sorted(set(after) | set(before)) + if after.get(r, 0) != before.get(r, 0) + } + + +def edit_groups(record): + require(len(record["groups"]) == 5, "five groups") + spaces = {name: span(tuple(pair[0])) for name, pair in record["groups"].items()} + require(all(len(s) == 128 for s in spaces.values()), "rank-seven groups") + require(len(record["frame_edits"]) == 139, "139 declared gate edits") + grouped = {name: [] for name in spaces} + seen = set() + for edit in record["frame_edits"]: + key = (edit["section"], edit["index"]) + require(key not in seen, "duplicate gate edit") + seen.add(key) + old, new = span(tuple(edit["old_frame"])), span(tuple(edit["new_frame"])) + require(new < old and len(old) == 2 * len(new), "one-dimensional gate lowering") + names = [name for name, space in spaces.items() if new <= space] + require(len(names) == 1, "unambiguous edited-frame group") + grouped[names[0]].append(edit) + helpers = [h for _, hs in record["groups"].values() for h in hs] + require(len(helpers) == len(set(helpers)) == 22, "22 distinct helpers") + require( + set(map(str, helpers)) == set(record["helper_final_changes"]), + "endpoint edit coverage", + ) + return grouped + + +def apply_frames(parent, record, names, endpoints=None): + grouped = edit_groups(record) + require(set(names) <= set(grouped), "known lowering groups") + child = deepcopy(parent) + lowered = set() + for name in names: + frame, helpers = record["groups"][name] + chosen = set(helpers) if endpoints is None else set(endpoints) + require(chosen <= set(helpers), "subset of group endpoints") + for helper in sorted(chosen): + change = record["helper_final_changes"][str(helper)] + old = parent["helper_final"][str(helper)] + require( + old == change["old"] and change["new"] == frame, "endpoint preimage" + ) + require( + span(tuple(frame)) < span(tuple(old)) and len(old) == 8, + "rank-eight to rank-seven endpoint", + ) + child["helper_final"][str(helper)] = list(frame) + lowered.add(helper) + for edit in grouped[name]: + section, index = edit["section"], edit["index"] + require( + section in ("A", "B", "restore") and 0 <= index < len(parent[section]), + "gate edit address", + ) + gate = parent[section][index] + require( + gate[:-1] == edit["gate"] and gate[-1] == edit["old_frame"], + "gate edit preimage", + ) + child[section][index][-1] = list(edit["new_frame"]) + changed = {key for key in parent if parent[key] != child[key]} + require( + changed <= {"helper_final", "A", "B", "restore"}, "frame-only changed fields" + ) + for section in ("A", "B", "restore"): + for old, new in zip(parent[section], child[section], strict=True): + require(old[:-1] == new[:-1], "scalar/operator word unchanged") + touched = new[1:3] if new[0] == "add" else new[1:2] + for helper in set(touched) & lowered: + require( + span(tuple(new[-1])) + <= span(tuple(child["helper_final"][str(helper)])), + "lowered helper gate fits endpoint", + ) + require(child["cleanup"] == parent["cleanup"], "cleanup unchanged") + return child diff --git a/research/rank7-joint-frame-audit/test_verify.py b/research/rank7-joint-frame-audit/test_verify.py new file mode 100644 index 0000000000..2f5afac9e0 --- /dev/null +++ b/research/rank7-joint-frame-audit/test_verify.py @@ -0,0 +1,128 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavior checks for the explicit-subspace oracle and its published command.""" + +import json +import os +import shutil +import subprocess +import sys +import tempfile +import unittest +from collections import Counter +from pathlib import Path + +import frames +import verify + + +class FrameTests(unittest.TestCase): + def test_explicit_span_and_dependence(self): + self.assertEqual(frames.span((1, 2, 4)), frozenset(range(8))) + with self.assertRaisesRegex(frames.Invalid, "independent frame"): + frames.span((1, 2, 3)) + with self.assertRaisesRegex(frames.Invalid, "at most nine"): + frames.span(tuple(range(1, 11))) + + def test_charged_climb_and_non_nested_failure(self): + current, paid, events = [frames.span((1,))], Counter(), [] + frames.climb(current, paid, events, ("test", 0), 0, frames.span((1, 2, 4))) + self.assertEqual(dict(paid), {2: 1}) + self.assertEqual(events, [["test", 0, 0, 1, 3, 2]]) + with self.assertRaisesRegex(frames.Invalid, "nonmonotone"): + frames.climb(current, paid, events, ("test", 1), 0, frames.span((2, 4))) + self.assertEqual(dict(paid), {2: 1}) + + def test_warp_image_and_inverse(self): + columns = [2, 1, 4, 8, 16, 32, 64, 128, 256] + current = [frames.span((1,))] + frames.warp(current, 0, columns, [1], [2]) + self.assertEqual(current, [frozenset({0, 2})]) + frames.warp(current, 0, columns, [1], [2], inverse=True) + self.assertEqual(current, [frozenset({0, 1})]) + with self.assertRaisesRegex(frames.Invalid, "warp image"): + frames.warp(current, 0, columns, [1], [4]) + cycle = [2, 4, 1, 8, 16, 32, 64, 128, 256] + current = [frames.span((2,))] + word = {"warps": [[0, 0, cycle, [1], [2]]]} + frames.scalar_step( + word, current, Counter(), [], "A", 0, ["warp", 0, -1, [2], [1]] + ) + self.assertEqual(current, [frozenset({0, 1})]) + + def test_cli_exact_result_and_optimized_equality(self): + with tempfile.TemporaryDirectory() as temporary: + env = {**os.environ, "PYTHONPYCACHEPREFIX": temporary} + command = [sys.executable, "-B", str(verify.PACKAGE / "verify.py")] + normal = subprocess.run( + command, check=True, capture_output=True, text=True, timeout=60, env=env + ) + optimized = subprocess.run( + command[:1] + ["-O"] + command[1:], + check=True, + capture_output=True, + text=True, + timeout=60, + env=env, + ) + self.assertEqual(normal.stdout, optimized.stdout) + report = json.loads(normal.stdout) + self.assertEqual(report["status"], "PASS_INDEPENDENT_RANK7_JOINT_FRAME_AUDIT") + for tag in ("base", "extra"): + provider = report["providers"][tag] + self.assertEqual( + provider["groups"]["V45"]["profile_delta"], + {"1": -2, "2": 10, "3": 6, "4": -10}, + ) + self.assertEqual( + [ + s["surrogate_margin"] + for s in provider["V45_subsets"] + if len(s["helpers"]) in (0, 1, 4) + ], + [-78512, -53141, -53141, -53141, -53141, 22972], + ) + self.assertEqual(len(provider["controls"]), 9) + self.assertEqual( + report["invoice_boundary"]["conditional_idle_remainder"], + {"1": 17310, "3": 4956, "5": 1728, "48": 28190}, + ) + + def test_git_free_export_and_corrupted_source_rejection(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + package = root / "research" / verify.PACKAGE.name + package.mkdir(parents=True) + for name in ("frames.py", "lowering.py", "verify.py", "SOURCES.json"): + shutil.copyfile(verify.PACKAGE / name, package / name) + records = json.loads((package / "SOURCES.json").read_text())["files"] + for record in records: + if record["usage"] == "input": + target = root / record["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / record["path"], target) + env = {**os.environ, "PYTHONPYCACHEPREFIX": str(root / "bytecode")} + command = [sys.executable, "-O", "-B", str(package / "verify.py")] + good = subprocess.run( + command, check=True, capture_output=True, text=True, timeout=60, env=env + ) + self.assertEqual( + json.loads(good.stdout)["providers"]["base"]["final"]["widths"], + {"4": 26, "5": 2, "6": 16, "7": 52, "8": 99, "9": 213}, + ) + source = root / verify.SOURCE / "data/STAGE1-FRAME-EDITS.json" + source.write_bytes(source.read_bytes() + b" ") + bad = subprocess.run( + command, + check=False, + capture_output=True, + text=True, + timeout=60, + env=env, + ) + self.assertNotEqual(bad.returncode, 0) + self.assertEqual(bad.stdout, "") + self.assertIn("input SHA256:", bad.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/rank7-joint-frame-audit/verify.py b/research/rank7-joint-frame-audit/verify.py new file mode 100644 index 0000000000..bb76f207cc --- /dev/null +++ b/research/rank7-joint-frame-audit/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Source-bound independent audit of PR2979's joint rank-seven frame paths.""" + +import gzip +import hashlib +import io +import json +from collections import Counter +from copy import deepcopy +from itertools import combinations +from pathlib import Path + +from frames import Invalid, cleanup_namespace, ledger, require +from lowering import apply_frames, difference, edit_groups + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/rank7-joint-endframes/" + + +def inputs(): + records = json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + require(len(records) <= 16, "bounded input manifest") + result = {} + for record in records: + if record["usage"] != "input": + continue + path = ROOT / record["path"] + require(path.stat().st_size <= 2_000_000, "bounded input bytes") + raw = path.read_bytes() + require( + hashlib.sha256(raw).hexdigest() == record["sha256"], + "input SHA256: " + record["path"], + ) + if path.suffix == ".gz": + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + raw = stream.read(8_000_001) + require(len(raw) <= 8_000_000, "bounded decoded input") + result[record["path"].removeprefix(SOURCE)] = json.loads(raw) + return result + + +def price(delta, weights): + return sum(n * weights[r] for r, n in delta.items()) + + +def rejected(action, expected): + try: + action() + except Invalid as error: + require(expected in str(error), ("wrong rejection", expected, str(error))) + return str(error) + raise Invalid("mutant accepted: " + expected) + + +def group_audit(parent, record, baseline, prices): + weights = {int(r): c for r, c in prices["weights"]["c"].items()} + break_even = prices["weights"]["break_even"] + results = {} + for name, (_, helpers) in record["groups"].items(): + child = apply_frames(parent, record, [name]) + result = ledger(child, check_report=False) + delta = difference(result["profile"], baseline["profile"]) + declared = next(g for g in prices["stage1"]["groups"] if g["group"] == name) + cost = price(delta, weights) + require(cost == declared["joint_delta"], "isolated joint surrogate price") + require( + -cost - len(helpers) * break_even == declared["joint_margin"], + "joint surrogate margin", + ) + results[name] = { + "profile_delta": delta, + "width_delta": difference(result["widths"], baseline["widths"]), + "surrogate_delta": cost, + "surrogate_margin": -cost - len(helpers) * break_even, + "gate_frame_edits": len(edit_groups(record)[name]), + } + return results + + +def subset_audit(parent, record, baseline, prices): + helpers = record["groups"]["V45"][1] + weights = {int(r): c for r, c in prices["weights"]["c"].items()} + results = [] + require(len(helpers) == 4, "four V45 endpoints") + for count in range(5): + for subset in combinations(helpers, count): + child = apply_frames(parent, record, ["V45"], endpoints=subset) + result = ledger(child, check_report=False) + delta = difference(result["profile"], baseline["profile"]) + expected = {1: 2 - count, 2: 10, 3: 6, 4: -10} + require( + delta == {r: n for r, n in expected.items() if n}, + "all-tariff V45 subset identity", + ) + require( + cleanup_namespace(child) + == {"private_buffers": 86, "cleanup_gates": 4992}, + "subset cleanup contract", + ) + cost = price(delta, weights) + margin = -cost - count * prices["weights"]["break_even"] + if count: + declared = next( + s + for s in prices["stage1"]["groups"][0]["subsets"] + if set(s["helpers"]) == set(subset) + ) + require( + cost == declared["delta"] and margin == declared["margin"], + "source subset surrogate comparison", + ) + require((margin > 0) == (count == 4), "joint-only guide margin") + results.append( + { + "helpers": list(subset), + "profile_delta": delta, + "surrogate_delta": cost, + "surrogate_margin": margin, + } + ) + require(len(results) == 16, "all endpoint subsets checked") + return results + + +def controls(parent, child, record): + results = {} + bad = deepcopy(child) + bad["report"] = deepcopy(parent["report"]) + results["stale_report"] = rejected(lambda: ledger(bad), "paid report mismatch") + bad = deepcopy(child) + bad["helper_final"]["249"] = [256, 128, 64, 32, 16, 8, 4] + results["wrong_rank7_space"] = rejected(lambda: ledger(bad, False), "nonmonotone") + bad = deepcopy(child) + edit = next(e for e in record["frame_edits"] if e["gate"][1] == 249) + bad[edit["section"]][edit["index"]][-1] = edit["old_frame"] + results["omitted_frame_edit"] = rejected(lambda: ledger(bad, False), "nonmonotone") + bad = deepcopy(child) + bad["helper_final"]["249"] = parent["helper_final"]["249"] + results["widened_endpoint"] = rejected(lambda: ledger(bad), "paid report mismatch") + bad = deepcopy(child) + bad["warps"][0][2] = [0] * 9 + results["singular_warp"] = rejected(lambda: ledger(bad, False), "invertible warp") + bad = deepcopy(child) + bad["cleanup"] = bad["cleanup"][1:] + results["missing_cleanup"] = rejected( + lambda: cleanup_namespace(bad), "cleanup length" + ) + bad = deepcopy(child) + bad["cleanup"][0][2] = 704 + 250 + results["wrong_private_name"] = rejected( + lambda: cleanup_namespace(bad), "inverse cleanup syntax" + ) + bad_record = deepcopy(record) + bad_record["frame_edits"][0]["gate"][3] *= -1 + results["stale_gate_preimage"] = rejected( + lambda: apply_frames(parent, bad_record, list(record["groups"])), + "gate edit preimage", + ) + bad_record = deepcopy(record) + bad_record["frame_edits"].append(deepcopy(record["frame_edits"][0])) + results["extra_edit"] = rejected( + lambda: edit_groups(bad_record), "139 declared gate edits" + ) + return results + + +def provider_audit(tag, data): + parent, final = (data[f"data/{kind}-{tag}.json.gz"] for kind in ("PARENT", "WORD")) + record, prices = ( + data["data/STAGE1-FRAME-EDITS.json"], + data["construction/STAGE-PRICES.json"], + ) + before = ledger(parent) + child = apply_frames(parent, record, list(record["groups"])) + child["report"]["local_profile"] = record["declared_local_profile"] + child["report"]["width_inventory"] = record["declared_width_inventory"] + joint, after = ledger(child), ledger(final) + groups = group_audit(parent, record, before, prices) + summed = Counter() + for result in groups.values(): + summed.update(result["profile_delta"]) + require( + {r: n for r, n in summed.items() if n} + == difference(joint["profile"], before["profile"]), + "isolated groups add to complete stage one", + ) + namespaces = [cleanup_namespace(word) for word in (parent, child, final)] + require( + [n["private_buffers"] for n in namespaces] == [86, 86, 91], + "all buffers charged", + ) + stage_delta = difference(joint["profile"], before["profile"]) + require(stage_delta == {1: -4, 2: 90, 3: -50, 4: -2, 5: -8}, "stage-one paid delta") + return { + "parent": {k: v for k, v in before.items() if k != "events"}, + "stage_one": {k: v for k, v in joint.items() if k != "events"}, + "final": {k: v for k, v in after.items() if k != "events"}, + "groups": groups, + "V45_subsets": subset_audit(parent, record, before, prices), + "cleanup_namespaces": namespaces, + "controls": controls(parent, child, record), + "chronological_event_sha256": [ + hashlib.sha256( + json.dumps(x["events"], separators=(",", ":")).encode() + ).hexdigest() + for x in (before, joint, after) + ], + } + + +def conditional_invoice(data, providers): + order, dispatch = data["allocation/ORDER.json"], data["allocation/DISPATCH.json"] + require(len(order) == len(dispatch) == 666, "666 complete calls") + require(len({tuple(pair) for pair in order}) == 666, "unique calls") + require([row[:2] for row in dispatch] == order, "ordered dispatch binding") + tags = {"gauge44": "base", "extra": "extra"} + counts = Counter(row[2] for row in dispatch) + require(set(counts) <= set(tags), "known providers") + local = Counter() + for provider, count in counts.items(): + local.update( + { + r: n * count + for r, n in providers[tags[provider]]["final"]["profile"].items() + } + ) + claimed = {int(r): n for r, n in data["allocation/PROFILE.json"].items()} + remainder = difference(claimed, local) + require( + all(n >= 0 for n in remainder.values()), "nonnegative claimed residual invoice" + ) + return { + "calls": dict(counts), + "derived_local_profile": dict(sorted(local.items())), + "source_claimed_complete_profile": claimed, + "conditional_idle_remainder": remainder, + "warning": "Remainder is subtraction from a source claim, not an owner replay. " + "PR2987 independently checks the packing bridge; native and physical admission remain separate.", + } + + +def main(): + data = inputs() + providers = {tag: provider_audit(tag, data) for tag in ("base", "extra")} + report = { + "status": "PASS_INDEPENDENT_RANK7_JOINT_FRAME_AUDIT", + "providers": providers, + "invoice_boundary": conditional_invoice(data, providers), + "scope": "Finite chronological frame paths, exact symbolic paid deltas and cleanup syntax/names only. " + "Surrogate margins do not certify the complete physical cost or a new kappa.", + } + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()