From a7e3e61cd709ccbc22b3e938853e01f838048e72 Mon Sep 17 00:00:00 2001 From: Gareth Davidson Date: Tue, 13 Oct 2026 22:42:04 +0100 Subject: [PATCH 1/2] Audit signed prefix bounds for selected complex provider --- .../complex-signed-prefix-audit/CONTROLS.json | 24 + .../complex-signed-prefix-audit/EXPECTED.json | 1020 +++++++++++++++++ .../complex-signed-prefix-audit/OVERLAP.json | 93 ++ research/complex-signed-prefix-audit/PROOF.md | 178 +++ .../complex-signed-prefix-audit/README.md | 129 +++ .../complex-signed-prefix-audit/SOURCES.json | 54 + .../complex-signed-prefix-audit/TASK.json | 74 ++ .../complex-signed-prefix-audit/VALIDATION.md | 58 + .../complex-signed-prefix-audit/VERIFY.json | 56 + .../complex-signed-prefix-audit/controls.py | 169 +++ .../source_check.py | 38 + .../test_package.py | 110 ++ .../complex-signed-prefix-audit/verify.py | 468 ++++++++ 13 files changed, 2471 insertions(+) create mode 100644 research/complex-signed-prefix-audit/CONTROLS.json create mode 100644 research/complex-signed-prefix-audit/EXPECTED.json create mode 100644 research/complex-signed-prefix-audit/OVERLAP.json create mode 100644 research/complex-signed-prefix-audit/PROOF.md create mode 100644 research/complex-signed-prefix-audit/README.md create mode 100644 research/complex-signed-prefix-audit/SOURCES.json create mode 100644 research/complex-signed-prefix-audit/TASK.json create mode 100644 research/complex-signed-prefix-audit/VALIDATION.md create mode 100644 research/complex-signed-prefix-audit/VERIFY.json create mode 100644 research/complex-signed-prefix-audit/controls.py create mode 100644 research/complex-signed-prefix-audit/source_check.py create mode 100644 research/complex-signed-prefix-audit/test_package.py create mode 100644 research/complex-signed-prefix-audit/verify.py diff --git a/research/complex-signed-prefix-audit/CONTROLS.json b/research/complex-signed-prefix-audit/CONTROLS.json new file mode 100644 index 0000000000..36b983498b --- /dev/null +++ b/research/complex-signed-prefix-audit/CONTROLS.json @@ -0,0 +1,24 @@ +{ + "transport": { + "frame_choices": 6, + "words": 216, + "prefix_cuts": 2376, + "exact_matrix_entries": 57024, + "adverse": [ + "unitary mismatched labels: shadow peak 1, physical peak 2, restored endpoint", + "nonunitary exact labels: shadow peak 1, physical peak 8, identity endpoint", + "unitary labels with inexact recipe: shadow zero, physical value 2", + "partially stored unit vectors: squared norm 41/25 > 1; factor-two square bound needed" + ] + }, + "program_controls": { + "wrong_common_frame": "common scalar frame", + "omit_climb": "common scalar frame", + "wrong_wrapper_terminal_pair": "wrapper terminal pair", + "premature_post_wrapper": "post wrapper placement", + "coefficient_source_alias": "coefficient source alias", + "non_dyadic_scale": "dyadic coefficient", + "wrong_power_two_scale_endpoint": "scalar endpoint", + "register_only_precision_bound": "131088 > 131072 at coefficient preparation" + } +} diff --git a/research/complex-signed-prefix-audit/EXPECTED.json b/research/complex-signed-prefix-audit/EXPECTED.json new file mode 100644 index 0000000000..d52c7fd117 --- /dev/null +++ b/research/complex-signed-prefix-audit/EXPECTED.json @@ -0,0 +1,1020 @@ +{ + "status": "PASS_COMPLEX_SIGNED_PREFIX_AUDIT", + "source_sha256": { + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/community-frontier1094-audit/selected-replay.tar.gz": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "research/complex-k492-owner-repair/code/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "research/gauge44-slots-t16/code/invoice_allcold.py": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8", + "research/e8-lemma-g-lean/PROOF.md": "2a7d84a83d34495dcf46ff9241ee3d7ec18ffc7d49c5476ab15fe0834046f2a3", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9" + }, + "orientations": { + "forward": { + "events": 24767, + "scalar_prefixes": 19693, + "persistent_columns": 704, + "common_frame_checks": true, + "wrapper_unit_rows": 480, + "exact_peak": "131088", + "register_peak": "131072", + "coefficient_peak": "131088", + "strict_bits": 18, + "positive_envelope": "2765345294379392599/1024", + "split_component_squared_bound": "34368127488", + "split_component_bits": 18, + "positive_strict_bits": 52, + "peak_witness": { + "event_index": 24223, + "kind": "coefficient_numerator", + "register": [ + "L", + 103 + ], + "phase": "full_frame_cleanup", + "l1": "131088", + "row": [ + [ + 77, + 8, + 1 + ], + [ + 86, + 65536, + 1 + ], + [ + 93, + 65536, + 1 + ], + [ + 103, + 8, + 1 + ] + ] + }, + "prefix_row_trace_sha256": "831c673effecb355df891418ab771383b9334427003b957e151aa2fd87b248b2", + "phase_peaks": { + "zero_frame_precondition": "34", + "entry_adapters": "34", + "A": "124", + "centers": "124", + "B": "124", + "cleanup_tail": "124", + "final": "124", + "exit_adapters": "124", + "full_frame_cleanup": "131088", + "done": "2" + }, + "dense_integer_crosscheck": true, + "attainment": { + "input_nonzero": 4, + "input_sup": 1, + "observed": "131088", + "primitive_peak": "131088", + "real_component_primitives": 198766, + "reverse_functional_matches": true + } + }, + "backward": { + "events": 24767, + "scalar_prefixes": 19693, + "persistent_columns": 704, + "common_frame_checks": true, + "wrapper_unit_rows": 480, + "exact_peak": "1154896", + "register_peak": "1154896", + "coefficient_peak": "98302", + "strict_bits": 21, + "positive_envelope": "14824960514781440791821/64", + "split_component_squared_bound": "2667569541632", + "split_component_bits": 21, + "positive_strict_bits": 68, + "peak_witness": { + "event_index": 24342, + "kind": "register", + "register": [ + "L", + 93 + ], + "phase": "full_frame_cleanup", + "l1": "1154896", + "row": [ + [ + 17, + 4096, + 1 + ], + [ + 18, + -768, + 1 + ], + [ + 19, + 512, + 1 + ], + [ + 24, + -8192, + 1 + ], + [ + 28, + 49151, + 2 + ], + [ + 29, + 8, + 1 + ], + [ + 30, + -8, + 1 + ], + [ + 38, + 4096, + 1 + ], + [ + 39, + -256, + 1 + ], + [ + 40, + 512, + 1 + ], + [ + 58, + -16385, + 2 + ], + [ + 59, + 8, + 1 + ], + [ + 60, + -8, + 1 + ], + [ + 75, + -16384, + 1 + ], + [ + 77, + -4096, + 1 + ], + [ + 82, + 16384, + 1 + ], + [ + 86, + 1, + 2 + ], + [ + 93, + 1, + 2 + ], + [ + 103, + -4096, + 1 + ], + [ + 107, + -8192, + 1 + ], + [ + 129, + -4096, + 1 + ], + [ + 130, + 768, + 1 + ], + [ + 131, + -512, + 1 + ], + [ + 136, + 8192, + 1 + ], + [ + 140, + -49151, + 2 + ], + [ + 141, + -8, + 1 + ], + [ + 142, + 8, + 1 + ], + [ + 150, + -4096, + 1 + ], + [ + 151, + 256, + 1 + ], + [ + 152, + -512, + 1 + ], + [ + 170, + 16385, + 2 + ], + [ + 171, + -8, + 1 + ], + [ + 172, + 8, + 1 + ], + [ + 187, + 16384, + 1 + ], + [ + 189, + 4096, + 1 + ], + [ + 194, + -16384, + 1 + ], + [ + 198, + -1, + 2 + ], + [ + 205, + -1, + 2 + ], + [ + 215, + 4096, + 1 + ], + [ + 219, + 8192, + 1 + ], + [ + 225, + -8194, + 1 + ], + [ + 226, + 16386, + 1 + ], + [ + 227, + 6018, + 1 + ], + [ + 229, + 6016, + 1 + ], + [ + 230, + 2176, + 1 + ], + [ + 231, + -22402, + 1 + ], + [ + 232, + 18562, + 1 + ], + [ + 233, + 2176, + 1 + ], + [ + 234, + -16386, + 1 + ], + [ + 235, + -18562, + 1 + ], + [ + 236, + -8192, + 1 + ], + [ + 237, + -10368, + 1 + ], + [ + 238, + 24578, + 1 + ], + [ + 239, + 8192, + 1 + ], + [ + 242, + 128, + 1 + ], + [ + 244, + -7168, + 1 + ], + [ + 246, + -129, + 1 + ], + [ + 247, + 8064, + 1 + ], + [ + 248, + -9216, + 1 + ], + [ + 249, + -128, + 1 + ], + [ + 250, + -129, + 1 + ], + [ + 252, + -8064, + 1 + ], + [ + 255, + 128, + 1 + ], + [ + 258, + -8192, + 1 + ], + [ + 259, + 8192, + 1 + ], + [ + 265, + -8192, + 1 + ], + [ + 274, + 7168, + 1 + ], + [ + 276, + 2048, + 1 + ], + [ + 278, + -14368, + 1 + ], + [ + 279, + 5120, + 1 + ], + [ + 280, + -2048, + 1 + ], + [ + 281, + 4097, + 1 + ], + [ + 283, + 2048, + 1 + ], + [ + 284, + 4064, + 1 + ], + [ + 285, + 2048, + 1 + ], + [ + 290, + -66, + 1 + ], + [ + 294, + -1535, + 1 + ], + [ + 295, + 62, + 1 + ], + [ + 296, + 128, + 1 + ], + [ + 297, + 528, + 1 + ], + [ + 299, + 128, + 1 + ], + [ + 300, + 641, + 1 + ], + [ + 301, + 256, + 1 + ], + [ + 302, + -384, + 1 + ], + [ + 303, + -384, + 1 + ], + [ + 313, + 8192, + 1 + ], + [ + 315, + 8192, + 1 + ], + [ + 316, + 8192, + 1 + ], + [ + 317, + 8192, + 1 + ], + [ + 336, + -8192, + 1 + ], + [ + 338, + -9216, + 1 + ], + [ + 340, + -8192, + 1 + ], + [ + 342, + 8706, + 1 + ], + [ + 343, + 15360, + 1 + ], + [ + 344, + 16384, + 1 + ], + [ + 345, + -12289, + 1 + ], + [ + 347, + -32768, + 1 + ], + [ + 348, + -7680, + 1 + ], + [ + 349, + -32768, + 1 + ], + [ + 352, + -2, + 1 + ], + [ + 354, + -62, + 1 + ], + [ + 356, + -2, + 1 + ], + [ + 358, + -4062, + 1 + ], + [ + 359, + -60, + 1 + ], + [ + 360, + 2, + 1 + ], + [ + 361, + 496, + 1 + ], + [ + 363, + -2, + 1 + ], + [ + 364, + -4064, + 1 + ], + [ + 365, + -2, + 1 + ], + [ + 456, + 8256, + 1 + ], + [ + 458, + 1024, + 1 + ], + [ + 459, + 16384, + 1 + ], + [ + 460, + 1537, + 1 + ], + [ + 462, + 4128, + 1 + ], + [ + 464, + -8194, + 1 + ], + [ + 465, + 2048, + 1 + ], + [ + 466, + -1056, + 1 + ], + [ + 467, + 132, + 1 + ], + [ + 468, + 496, + 1 + ], + [ + 469, + -62, + 1 + ], + [ + 470, + 4095, + 1 + ], + [ + 471, + -9216, + 1 + ], + [ + 474, + 8256, + 1 + ], + [ + 476, + -8194, + 1 + ], + [ + 477, + -14336, + 1 + ], + [ + 479, + 8192, + 1 + ], + [ + 480, + -8192, + 1 + ], + [ + 486, + 1022, + 1 + ], + [ + 488, + -1056, + 1 + ], + [ + 489, + 132, + 1 + ], + [ + 492, + -1023, + 1 + ], + [ + 493, + 8192, + 1 + ], + [ + 495, + -256, + 1 + ], + [ + 496, + 16384, + 1 + ], + [ + 520, + -16384, + 1 + ], + [ + 522, + -1026, + 1 + ], + [ + 524, + -8190, + 1 + ], + [ + 525, + 18432, + 1 + ], + [ + 527, + 8192, + 1 + ], + [ + 528, + 1, + 1 + ], + [ + 529, + 8192, + 1 + ], + [ + 534, + 8128, + 1 + ], + [ + 536, + -992, + 1 + ], + [ + 537, + 124, + 1 + ], + [ + 594, + 16384, + 1 + ], + [ + 596, + -16384, + 1 + ], + [ + 600, + 128, + 1 + ], + [ + 602, + 9150, + 1 + ], + [ + 604, + 7102, + 1 + ], + [ + 606, + 8128, + 1 + ], + [ + 608, + 4, + 1 + ], + [ + 609, + 4352, + 1 + ], + [ + 610, + -27810, + 1 + ], + [ + 611, + 132, + 1 + ], + [ + 612, + 9374, + 1 + ], + [ + 613, + 124, + 1 + ], + [ + 614, + -8190, + 1 + ], + [ + 615, + 18432, + 1 + ], + [ + 616, + 32768, + 1 + ], + [ + 618, + -16384, + 1 + ], + [ + 619, + 16384, + 1 + ], + [ + 620, + 8192, + 1 + ], + [ + 621, + 8192, + 1 + ], + [ + 624, + 4, + 1 + ], + [ + 626, + 16382, + 1 + ], + [ + 628, + 8193, + 1 + ], + [ + 630, + 1, + 1 + ], + [ + 631, + 8192, + 1 + ], + [ + 648, + 2048, + 1 + ], + [ + 650, + -1024, + 1 + ], + [ + 652, + -1024, + 1 + ], + [ + 654, + -1024, + 1 + ], + [ + 656, + 16384, + 1 + ], + [ + 658, + -8192, + 1 + ], + [ + 660, + -8192, + 1 + ], + [ + 662, + -8192, + 1 + ] + ] + }, + "prefix_row_trace_sha256": "265ef142b0d7930da4a32e0c2e3229a02509949f3f8384dde919e6ab9e2a855b", + "phase_peaks": { + "zero_frame_precondition": "47", + "entry_adapters": "47", + "A": "101", + "centers": "19", + "B": "20", + "cleanup_tail": "18", + "final": "18", + "exit_adapters": "18", + "full_frame_cleanup": "1154896", + "done": "2" + }, + "dense_integer_crosscheck": true, + "attainment": { + "input_nonzero": 176, + "input_sup": 1, + "observed": "1154896", + "primitive_peak": "1154896", + "real_component_primitives": 198814, + "reverse_functional_matches": true + } + } + }, + "conditional_global": { + "old_local_bits": 68, + "signed_local_bits": 21, + "unchanged_other_allowances": 329, + "old_sufficient_bits": 397, + "signed_sufficient_bits": 350, + "retained_payload_bits": 512 + }, + "scope": "Exact scalar/Horner prefix and conditional unitary common-frame norm corollary. Recursive child internals, physical compiler/hosting, roundoff, native admission and analytic transfer remain inherited. No production payload or kappa change." +} diff --git a/research/complex-signed-prefix-audit/OVERLAP.json b/research/complex-signed-prefix-audit/OVERLAP.json new file mode 100644 index 0000000000..51df9340d9 --- /dev/null +++ b/research/complex-signed-prefix-audit/OVERLAP.json @@ -0,0 +1,93 @@ +{ + "status": "manual_scope_review_not_novelty_certificate", + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-13T21:16:00.073340+00:00", + "complete_pagination": true, + "records": 853 + }, + "discussions": { + "fetched_at": "2026-10-13T21:16:04.557459+00:00", + "complete_pagination": true, + "records": 19 + } + }, + "submission_coverage": { + "open_prs": { + "fetched_at": "2026-10-13T21:39:10.148242+00:00", + "complete_pagination": true, + "record_count": 868 + }, + "discussions": { + "fetched_at": "2026-10-13T21:39:17.066554+00:00", + "complete_pagination": true, + "record_count": 30 + } + }, + "terms": [ + "signed prefix", + "signed-row", + "common-frame", + "precision" + ], + "nearest": [ + { + "number": 821, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/821", + "title": "Research audit: 286-to-160-bit prefix estimate for pinned #626 (no new kappa)", + "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8", + "distinction": "Per-replica norm argument; initial idea stopped as duplicate. Not composed here." + }, + { + "number": 734, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/734", + "title": "Research: prefix-bounded signed-Horner circuits for CK and JP8 (no new kappa)", + "head": "ba76ba3321d000c8996b0b254bcf0d7260e1bbb6", + "distinction": "Changes Horner circuits under old envelopes; our unsigned program is fixed." + }, + { + "number": 745, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/745", + "title": "Independent verification: JP8 adjoint replay and dirty-centre clear witness", + "head": "fc6ebccca3bd61a6eaf6ec3fcbf2e99d2888c35c", + "distinction": "Adjoint endpoint/private-clear audit; reverse functional checking credited." + }, + { + "number": 1184, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1184", + "title": "Tooling: 2.33x faster complete emitted local audit with preserved coverage", + "head": "2f1c9e0e671bb10aecd452e18449130b0601932d", + "distinction": "Accelerates original positive-envelope driver; integer-row technique credited." + }, + { + "number": 1255, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1255", + "title": "Research audit: exact phase criterion for selected PR1094 residual charts", + "head": "add1e2673ef000c097ec0fd70058e644af048d6b", + "distinction": "Exact residual chart phases; charts unchanged in this norm audit." + }, + { + "number": 1263, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1263", + "title": "Finite complex construction: simultaneous k8 gauges save 13,000 primitives", + "head": "5fbaca13028846bddbb001e8e07addc2ab8e5816", + "distinction": "Changes simultaneous helper gauges and scalar work; our source word is unchanged." + }, + { + "number": 1277, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1277", + "title": "Research audit: the selected #1094 reuse replay discards its ancestry recheck; binding certified from committed archives (no new kappa)", + "head": "02d279515ff1fc468ab99a19d89461f1b6391507", + "distinction": "Selected reuse-mode ancestry binding audit; different source-chain obligation, not signed prefix norms." + }, + { + "number": 1278, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1278", + "title": "Research audit: linear subset-budget bound for commuting dirty intervals", + "head": "06b8c006891ae78abe24b30d2fe9d8c188deafe8", + "distinction": "Commuting dirty-stride inverse interval amplification; different recursive word and norm budget." + } + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1260", + "limitations": "Open PR bodies including drafts; Discussion bodies/comments; local README/TASK/ledger. Not all code diffs or worldwide literature." +} diff --git a/research/complex-signed-prefix-audit/PROOF.md b/research/complex-signed-prefix-audit/PROOF.md new file mode 100644 index 0000000000..55384bc6f2 --- /dev/null +++ b/research/complex-signed-prefix-audit/PROOF.md @@ -0,0 +1,178 @@ +# Signed scalar prefixes through unitary frames + +## 1. The proposition and its hypotheses + +Let H be any complex Hilbert space and let finitely many persistent registers +start at arbitrary x_j with ||x_j||₂ ≤ M. Private centres and coefficient +work start at zero. Each register has a label λ and each label denotes a +**unitary** T_λ. Assume the following execution contract at every cut: + +1. A relabel A→B executes exactly T_B T_A⁻¹, with current label A. +2. ADD t,s,q has distinct registers and equal labels, and executes + x_t ← x_t + q x_s. SCALE uses its stated rational coefficient. COPY + inherits the source label; CLEAR writes zero with the stated label. +3. Relabels/complete recursive children are treated at their boundaries. Their + implementations and exact physical realization are separate hypotheses. +4. Coefficient work is cleared, prepared from the unchanged source by the + unsigned binary Horner and halving program, accumulated, then cleared. + The completed complex scalar operation precedes the next frame operation. + +The scalar shadow deletes relabels and runs the remaining scalar operations. +Let S^(k) be its matrix on the persistent input columns at cut k; zero private +input columns contribute nothing. Then + + x_r^(k) = T_(λ_r^(k)) Σ_j S^(k)_(r,j) T_(λ_j^(0))⁻¹ x_j, + ||x_r^(k)||₂ ≤ M Σ_j |S^(k)_(r,j)|. (1) + +The equality is the retained **Lemma G common-frame conjugation theorem**, +applied to each prefix, not a new conjugation theorem. See the pinned +[proof, Theorem 1 and row form](../e8-lemma-g-lean/PROOF.md). Its event induction +commutes ADD/SCALE through a common label, transports a relabel exactly, +and handles COPY/CLEAR. Prefixes inherit its hypotheses. The norm inequality +then follows from unitarity and the triangle inequality. This is a written +corollary; no new Lean theorem is claimed. + +For a fixed nonzero row the bound is attained in this abstract model: choose +a unit vector u and x_j = T_(λ_j^(0)) sign(S_(r,j)) u, using zero for absent +columns. The output has norm M times the row's absolute sum after scaling +inputs by M. This establishes a sharp scalar-shadow/Hilbert input bound for +that cut. It is not a minimum physical fixed-point word length or rounding +error bound. + +Crucially, take the absolute values **after** evaluating the signed row. +The existing recurrence e_t ← e_t + |q| e_s discards cancellations. Both are +valid sufficient bounds under the execution contract; the old estimate is +not an acceptance bug. + +## 2. Coefficient work and partially written complex values + +Write a nonzero reduced dyadic q as ±a/2^d, a>0. Unsigned binary Horner visits +integer multipliers k with 0≤k≤a and reaches a. Subsequent halvings decrease +the magnitude. Thus the exact largest row norm in coefficient preparation is + + a ||row(source)||₁. (2) + +The source is unchanged and differs from the target. The final accumulation +is the new target row; the scratch clear is zero. A power-of-two SCALE is a +monotone sequence of doublings or halvings followed, if needed, by negation; +its endpoints bound its intermediate row norms. COPY/CLEAR are immediate. +Consequently, the maximum over every stored row at scalar boundaries and +(2) covers every *completed complex scalar primitive*, including Horner +scratch. This proof does not assume that a macro endpoint bounds its work. + +A physical store may update real/imaginary components or coordinates +sequentially. Between ideal consecutive values u,v, such a partial value is +P v + (I−P) u for an orthogonal coordinate projection P. Hence + + ||P v + (I−P) u||₂² ≤ ||u||₂² + ||v||₂² ≤ 2 M² L², (3) + +where L is the largest ideal row norm. This possible factor is explicitly +charged. For the two selected programs, exact integer inequalities give + + 2 · 131088² < 2^(2·18), + 2 · 1154896² < 2^(2·21). + +Thus the sufficient 18/21-bit envelopes also cover these partial stores; +no floating-point square root or implicit spare bit is used. Unit norm of +an endpoint alone would not justify this: a partial store from (3/5,4/5) +to (1,0) can have squared norm 41/25. + +## 3. Why the hypotheses cannot be deleted + +These are counterexamples to weakened interfaces, not accepted mutants of +the selected construction. + +* **Equal labels.** Start a=1 and private b=0; COPY b←a; relabel b by −I; + physically subtract b from a without aligning the labels. The shadow + predicts a=0, while the actual value is 2. Add b back, relabel b by −I and + clear b: the persistent endpoint is restored. Every relabel is unitary + and exact, and the unlabelled shadow has maximum 1. The two intervening + cross-label additions are inadmissible. A correct endpoint does not fix + the wrong prefix argument. +* **Unitary labels.** With T₀=I and T₁=diag(K,1), K>1, the exact well-labelled + relabel loop 0→1→0 has scalar shadow I and identity physical endpoint, but + sends (1,0) through (K,0). The general Lemma G equality still holds; the + norm conclusion without condition numbers does not. The executable + control uses K=8, and the displayed family is unbounded in K. +* **Exact recipes.** After COPY b←a=1, declare both labels −I, but execute I + for a's relabel and −I for b's. The declared labels now match; a−=b gives + 2 while the shadow gives zero. Unitarity of the operators actually run + does not replace the exact-recipe condition. +* **Coefficient work.** In the actual selected forward word, persistent + and centre rows never exceed 131072, but event 24223 prepares a numerator + row of norm 131088. The four inputs 77,86,93,103 set to +1 (all others + zero) attain it. An envelope that omits coefficient preparation is false. + +The exact six-frame finite corpus includes noncommuting rational rotations, +216 label choices, 2,376 cuts and 57,024 matrix-entry equalities against the +physical execution. It illustrates (1); the induction above proves the +quantified statement for all finite words satisfying the hypotheses. + +## 4. Selected-source application + +The archived PR1094 provider has v=112, R=480, h=9, 704 arbitrary persistent +inputs and eight initially zero private centres. Both orientations contain +24,767 events and 19,693 scalar macros. The archive is pinned verbatim; +programs match the serialized selected provider and all 144 invocation +program hashes. The original local checker's retained copy has the same +SHA256 as the checker named in the selected source inventory. + +The independent replay checks all 39,386 changed scalar rows twice: sparse +rational maps and dense integer rows with a single dyadic denominator. +Every ADD/COPY frame incidence, frame transition, wrapper interval and +all 960 pre/post wrapper unit rows are checked. All 704 arbitrary-input +endpoint columns are checked in each orientation; private rows vanish. +The full unchanged original local driver is also executed separately with +assertions enabled, including its containment/rank/phase checks and all +25 mutation controls. Its entire regenerated receipt equals the archived +receipt. The original positive estimates are independently recomputed. + +For the physical interpretation, retain the construction's exact +frame/normalization recipes and common-label realization. The Clifford +building blocks P, X, diagonal Gaussian phases and +C_q=((1+i)I+(1−i)X_q)/2 are unitary: X_q is a self-adjoint involution, and the +two C eigenvalues are 1 and i. Products/inverses remain unitary. Normalizer +L,R are Gaussian monomials, also unitary. The extended labels +T_(pre,j)=R_(E,U) T_E and T_(done,j)=L_(E,U)⁻¹ T_U therefore satisfy the norm +hypothesis; see the pinned [hyperplane-end proof](../hyperplane-end-lean/PROOF.md). +This uses the retained recipe interpretation. We have not freshly executed +the full Clifford/native/physical provider replay, nor proved recipe +exactness for every current frame in Lean. The original local driver checks +which recipes are named and when, not all their physical matrix entries. + +| Orientation | Positive envelope | Exact signed/work maximum L | Ideal and partial-store bits | +| --- | ---: | ---: | ---: | +| Forward | 2765345294379392599/1024 (52 bits) | 131088 | 18 | +| Backward | 14824960514781440791821/64 (68 bits) | 1154896 | 21 | + +The forward peak occurs in coefficient preparation at zero-based event +24223, reading L103, with row +8e77 + 65536e86 + 65536e93 + 8e103. The backward peak is register L93 after +event 24342, with 176 nonzero input coefficients recorded in EXPECTED.json. +For each peak, a separate reverse functional replay recovers the entire +row. A numerical scalar run on its signed attaining input executes every +unsigned-Horner primitive in the whole orientation: 198766/198814 real +component operations, matching the archived primitive counts. It attains +the peak and never exceeds it. These scalar runs delete the unitary +relabels; their transfer to physical norms is exactly the conditional +corollary (1), not a claim to have simulated the 73-axis physical program. + +## 5. Downstream arithmetic and limits + +Under the retained global cover, complete-call, and precision compilation +hypotheses, substitute the checked **21-bit bound including partial stores** +for the old local 68-bit estimate in the unchanged source formula: + + 68 + 37 + 144 + 144 + 4 = 397, + 21 + 37 + 144 + 144 + 4 = 350. + +The extra terms retain the original input sup-to-L2 bound, all complete-call +and bridge growth allowances, and primitive arithmetic margin. We do not +use PR821's separate replica-count improvement. 350 is a conditional +sufficient estimate, not an optimal global bound. The production invoice +and 512-bit payload, row reserve, bootstrap, paid profile and selected κ +are unchanged. No current proof obligation is silently discharged: recursive +child internals, exact physical common-label/hosting realization, native +recipe admission, roundoff accumulation, tape/exact recovery and analytic +transfer remain inherited. No improved multiplication exponent or measured +runtime claim follows. diff --git a/research/complex-signed-prefix-audit/README.md b/research/complex-signed-prefix-audit/README.md new file mode 100644 index 0000000000..45fc28b079 --- /dev/null +++ b/research/complex-signed-prefix-audit/README.md @@ -0,0 +1,129 @@ +# Selected PR1094: signed prefix precision audit + +The unchanged R480 programs have exact signed scalar/Horner prefix maxima +**131088 forward and 1154896 backward**, requiring sufficient **18/21-bit** +envelopes rather than the retained positive-recurrence estimates of 52/68 +bits. Exact squared inequalities also cover partially stored real/imaginary +components within the same 18/21 bits. + +This is a **conditional precision-interface audit**, with no new κ. The +[prefix norm proof](PROOF.md) is a corollary of the credited Lemma G +common-frame conjugation theorem. It specifies why unitary labels, exact +recipes and equal labels at ADD are required, and gives exact counterexamples +to omitting them. Cancellations are evaluated before taking absolute values. +The existing larger bound remains valid. + +Under the inherited global execution/precision hypotheses, replacing only +the local term in the selected formula gives **397 → 350 sufficient bits**. +The production payload remains **512**; the supplier, paid profile, selected +record and all predecessor files are unchanged. This is not a fixed-point +roundoff theorem or a new physical compiler admission. + +## Evidence and reproduction + +Python 3.12+ and the standard library, from the repository root: + +```sh +python3 -I -B research/complex-signed-prefix-audit/verify.py +python3 -I -B research/complex-signed-prefix-audit/controls.py +python3 -I -B research/complex-signed-prefix-audit/source_check.py +python3 -I -B research/complex-signed-prefix-audit/test_package.py +``` + +The first command checks all **39,386 scalar prefixes** with sparse rational +and dense integer engines; both 704-column endpoints; frame/wrapper incidence; +960 wrapper unit rows; and Horner scratch. Separate reverse functional and +literal primitive executions certify both attaining inputs and reproduce +**198766/198814** real-component primitive counts. EXPECTED.json records the +complete peak rows, all phase maxima and portable trace digests. + +The controls check 216 exact unitary-frame words, 2,376 prefix cuts and 57,024 +matrix entries, four mathematical boundary examples, and eight selected-word +or bound controls. In particular, omitting scratch underestimates the actual +forward peak: **131088 > 131072**. The source command runs the byte-identical +original driver with assertions enabled and all 25 inherited mutations; +its entire regenerated local receipt matches the archive. The package tests +cover dyadic cancellation, strict bit boundaries, read-only isolated/optimized +relocation, source/pin corruption and a one-unit understated receipt. + +The opt-in registration is: + +```sh +python3 scripts/research_package.py --package research/complex-signed-prefix-audit --check-only +python3.12 scripts/research_package.py --package research/complex-signed-prefix-audit +``` + +See [VALIDATION.md](VALIDATION.md) for the actual environment and results. +The original driver is run in a temporary directory; other default commands +are read-only. `verify.py --output NEW_PATH` writes a checked receipt and +refuses to overwrite an existing file. Immutable source archives are pinned +byte-for-byte; regenerated receipts are compared as decoded JSON. + +## Scope, task and overlap + +Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; selected PR1094 source +`0fc329d0bec93ca7cd288eaea1295172e8789810`, parent PR1087 +`589d1cedf5ef5f231182f4ec86408616311a8af0`. +The fresh OS nonce `9e66acdf5b86cc4b02a0d212138d7b3e` assigned adversarial audit, +`uniform-transfer-audit`, catalogue revision 2. The baseline binding command +passed before refinement. [TASK.json](TASK.json) records the bounded question, +refinement and open questions; [SOURCES.json](SOURCES.json) binds every external +input and historical task provenance. +[Discussion #1260](https://github.com/CrocSwap/integer-mult-bounds/discussions/1260) +records the scoped claim and result. + +The initial replica-prefix idea was stopped when overlap checking found +[PR821](https://github.com/CrocSwap/integer-mult-bounds/pull/821), head +`6b832a6ba4dce8dd6e2fb0897dd4543364b932f8`. Its replica-norm argument is not +repeated here. Other nearest work is: + +- [PR1184](https://github.com/CrocSwap/integer-mult-bounds/pull/1184), + `2f1c9e0e671bb10aecd452e18449130b0601932d`: faster execution of the same + original positive-envelope checker. Integer-row arithmetic is credited + prior technique; this package's result concerns the signed physical norm. +- [PR734](https://github.com/CrocSwap/integer-mult-bounds/pull/734), + `ba76ba3321d000c8996b0b254bcf0d7260e1bbb6`: changed signed-Horner circuits + preserving the older envelopes. Here the unsigned source circuit is unchanged. +- [PR745](https://github.com/CrocSwap/integer-mult-bounds/pull/745), + `fc6ebccca3bd61a6eaf6ec3fcbf2e99d2888c35c`: reverse endpoint checking and + a private-clear witness. Reverse-mode checking is credited prior technique. +- [PR1255](https://github.com/CrocSwap/integer-mult-bounds/pull/1255), + `add1e2673ef000c097ec0fd70058e644af048d6b`: exact residual chart phase; + this package leaves charts fixed and audits a different norm implication. + +The fresh search covered open PR bodies, Discussion bodies/comments and +local package notes; it does not establish worldwide novelty. The scalar +and frame-local checks are fresh. Native Clifford replay, whole global +controller/owner replay, cold supplier regeneration, Lean, full compiler, +roundoff/tape/exact recovery and analytic transfer are not run or discharged. +The source record's retained conditions still apply. + +## Open next questions + +1. **Formalize the prefix norm and partial-store corollaries.** This would + make the precision-interface statement reusable alongside Lemma G. Start + with `Stream.conj_matrix` for an arbitrary prefix and diagonal unitary + labels, then the orthogonal projection inequality. The blocker is a + scoped Hilbert-norm extension to the current algebraic formalization; + finite Python examples are not a formal substitute. +2. **Admit the signed envelope in the production invoice.** It may reduce + conservative reserves for future constructions. Start by integrating the + signed-row checker and exact split-component inequality into one provider + recount, preserving all source/admission controls. Complete native/global + replay and the precise internal compiler/precision obligations are still + required. This package changes neither the 512-bit charge nor κ. + +## Credit + +Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance in the +proof, implementation, checks and writing; no subagents or independent human +review. Apache-2.0. The conjugation theorem and scalar interface are inherited +from Zhihao Chen/PR425 and Lemma G/PR484 (DreamingOfClouds); whole-helper and +normalization work credits chafreaky/PR458, Dugongue/PR471, and the Lemma G, +Lemma A and hyperplane-end formalization authors. Rohan Arun supplies the +selected PR1094 placement; Jeremy Kothe, Hao Yan (icekylinx), Josie Elliston, +Douglas Colkitt and the retained gauge44/Clifford/compiler lineage supply +this provider and its original audits. Sagar Thakrar's adjoint/lowering work, +PR734's authors, and the PR1137/1156/1184 integer-row work retain their credit. +The norm corollary is standard linear algebra; no priority claim is made +for that argument, signed-row arithmetic or reverse functional replay. diff --git a/research/complex-signed-prefix-audit/SOURCES.json b/research/complex-signed-prefix-audit/SOURCES.json new file mode 100644 index 0000000000..8c592e4c83 --- /dev/null +++ b/research/complex-signed-prefix-audit/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-k492-owner-repair/code/hpe_audit_local.py", + "usage": "input", + "git_blob": "17bccb64fdca54f329a3ce16e369449cb76c2802", + "sha256": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + { + "path": "research/gauge44-slots-t16/code/invoice_allcold.py", + "usage": "input", + "git_blob": "d1dd2212917ad1e7f099287a141f741fd52bdcf6", + "sha256": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8" + }, + { + "path": "research/e8-lemma-g-lean/PROOF.md", + "usage": "input", + "git_blob": "6b24da0ab861902a6a3f65d9599bb9c0f964aa1c", + "sha256": "2a7d84a83d34495dcf46ff9241ee3d7ec18ffc7d49c5476ab15fe0834046f2a3" + }, + { + "path": "research/hyperplane-end-lean/PROOF.md", + "usage": "input", + "git_blob": "a94a2ac168c088a1282ea411766bc859178620df", + "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9" + } + ] +} diff --git a/research/complex-signed-prefix-audit/TASK.json b/research/complex-signed-prefix-audit/TASK.json new file mode 100644 index 0000000000..db56d2f147 --- /dev/null +++ b/research/complex-signed-prefix-audit/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit when exact signed scalar-prefix rows imply a Hilbert-space physical prefix bound through changing frames and normalization wrappers; source-bind the selected PR1094 R480 forward/backward words and test the common-frame boundary with exact adverse examples.", + "scope_change_reason": "The initial per-replica norm idea duplicates PR821 and was stopped before computation. The bounded precision-interface refinement instead tracks cancellation across changing unitary frames and primitive coefficient work. Prove the quantified transfer lemma and falsify omission of its common-frame hypothesis; no new global compiler or frontier claim.", + "bottleneck_link": "Clarifies a concrete precision-transfer hypothesis and measures any sufficient prefix headroom for the unchanged selected word. This is an audit contribution, not a paid-profile or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "One source-bound audit of both selected orientations; stop if common-frame/wrapper transport cannot justify the signed bound. Reserve final quarter for controls and review; no search for changed supplier words.", + "outcome": "completed", + "evidence": "PROOF.md: quantified norm corollary. EXPECTED.json: all signed scalar/Horner prefixes and attaining witnesses. CONTROLS.json: semantic controls. source_check.py: full unchanged local driver. test_package.py: six package/kernel tests. VALIDATION.md: actual environments and checks.", + "author": "Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with reasoning, implementation, exact checks and writing; no subagents or independent human review.", + "open_questions": [ + { + "question": "Formalize the prefix norm and partial-store corollaries alongside Lemma G.", + "why_it_matters": "Provides a reusable precision-interface result in the existing formal framework.", + "first_step": "Apply Stream.conj_matrix at an arbitrary prefix with unitary label operators, then prove the orthogonal projection inequality for partial stores.", + "blocked_by": "Hilbert norm/realification setup and a scoped Lean proof; finite examples do not discharge this." + }, + { + "question": "Can the production invoice safely adopt a signed envelope for one current provider?", + "why_it_matters": "Reduces conservative reserves without changing the scalar word; may assist future parameter choices.", + "first_step": "Integrate a signed row recount and exact squared partial-store guard while preserving all source and admission controls.", + "blocked_by": "Fresh complete native/global admission and retained internal compiler/precision obligations; no payload or kappa change is authorized here." + } + ], + "assignment_nonce": "9e66acdf5b86cc4b02a0d212138d7b3e", + "assigned_track": "adversarial-audit", + "assigned_scope_key": "ce7411fb7cf6f3460bfc", + "selected_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "source_parent_head": "589d1cedf5ef5f231182f4ec86408616311a8af0", + "first_step": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "claim_expires_utc": "2026-10-13T23:25:00Z", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1260" +} diff --git a/research/complex-signed-prefix-audit/VALIDATION.md b/research/complex-signed-prefix-audit/VALIDATION.md new file mode 100644 index 0000000000..4fb4e7e100 --- /dev/null +++ b/research/complex-signed-prefix-audit/VALIDATION.md @@ -0,0 +1,58 @@ +# Validation + +Completed locally on 2026-10-13, Linux x86_64 +(`Linux-7.0.0-38-generic-x86_64-with-glibc2.43`). Base and refreshed upstream +main: `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`. + +| Command | Environment | Result | +| --- | --- | --- | +| `python3 -B scripts/research_baseline.py` | CPython 3.14.4 | PASS_RESEARCH_BASELINE_BINDINGS_ONLY; orientation, not supplier replay | +| `/usr/bin/python3.12 scripts/research_package.py --package research/complex-signed-prefix-audit` | CPython 3.12.3 | All four registered commands pass; six package tests pass | +| `python3 -I -O -B research/complex-signed-prefix-audit/verify.py` | CPython 3.14.4 | PASS_COMPLEX_SIGNED_PREFIX_AUDIT; identical receipt | +| `python3 -I -O -B research/complex-signed-prefix-audit/controls.py` | CPython 3.14.4 | PASS_SIGNED_PREFIX_CONTROLS; identical receipt | +| `python3 -I -B research/complex-signed-prefix-audit/source_check.py` | CPython 3.14.4 | Original driver passes both orientations and all 25 controls; entire receipt identical | +| `make selected-record-check` | CPython 3.14.4 | Selected record/source inventory/κ guard passes | + +The registered Python 3.12 command runs `verify.py`, `controls.py`, +`source_check.py`, and `test_package.py`. The last command runs six tests, +including minimal read-only relocation with spaces in its path, isolated +optimized Python, exact dyadic cancellation, strict-power boundaries, +source mutation, a removed mandatory input pin, and a one-unit understatement +of the backward peak. No repository checkout or network is needed for that +relocated verifier; registration's historical metadata validation uses Git. +The source driver runs with `-I` and without `-O` even when its caller uses +optimized mode, so every original assertion remains enabled. + +Portable SHA256 receipts, over sorted compact JSON: + +- Signed prefix: `17c82644f920abd7b9a776481efec1740f0ae75b99c53bf331e3e1442d328300`. +- Controls: `415845cdd798be4ee121c3d7f873b1c6e30c73c1e424bb07bd655d0aac728c65`. +- Complete original local receipt: `510c6ec28beb87ee4c854a6bd492c7de8155b815d306e770245b49a074ac4774`. + +All 39,386 scalar prefixes agree between sparse rational and dense integer +engines. Separate reverse functional checks and numerical primitive replays +attain each maximum. The numerical primitive counts equal the archived +198766/198814 real-component counts. Frame examples check 57,024 exact +matrix entries at 2,376 cuts; eight selected-word/bound controls reject the +specified weakened checks. Four mathematical boundary examples are recorded. + +During development, the phase report was corrected to include unchanged +live rows at each phase entry, and the partial-store projection bound was +made explicit before the final receipts were generated. The initial package +metadata check rejected a structured `evidence` field; it was corrected to +the schema's text field before the successful registered replay. Neither +issue changes a predecessor artifact or the selected construction. + +[OVERLAP.json](OVERLAP.json) records the refreshed complete remote pagination: +868 open PRs and 30 Discussions at 21:39 UTC, including bodies/comments. The +nearest five earlier heads remain unchanged. PR1263 changes scalar gauges; +PR1277 audits ancestry binding; PR1278 bounds a different dirty recursive +word. No duplicate signed-prefix result was found in the inspected scope. +This is coordination evidence, not a novelty certificate. + +Not run: full native/Clifford/provider cold replay, whole global controller +or owner replay, physical compiler realization, roundoff/tape/exact-recovery +proofs, analytic assembly, Lean, or repository-wide historical suites. The +original local checker is run fully; its source assumptions do not become a +complete multiplication proof. Hosted PR CI is a separate status and is +reported at publication rather than inferred from these local passes. diff --git a/research/complex-signed-prefix-audit/VERIFY.json b/research/complex-signed-prefix-audit/VERIFY.json new file mode 100644 index 0000000000..6842edcfe5 --- /dev/null +++ b/research/complex-signed-prefix-audit/VERIFY.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-k492-owner-repair/code/hpe_audit_local.py", + "research/gauge44-slots-t16/code/invoice_allcold.py", + "research/e8-lemma-g-lean/PROOF.md", + "research/hyperplane-end-lean/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both 704-column endpoints; every signed scalar row with two exact arithmetic engines, unsigned-Horner work and partial-store bound; reverse and primitive attaining witnesses; immutable source bindings and committed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 120, + "checks": "216 exact unitary-frame words and 2376 cuts; four mathematical boundary witnesses; eight semantic selected-word/bound controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/source_check.py" + ], + "timeout_seconds": 240, + "checks": "Entire unchanged original local driver, both orientations/all 704 columns and all 25 source controls; complete regenerated receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 240, + "checks": "Six package/kernel tests including isolated optimized read-only relocation and semantic receipt/source/pin corruption." + } + ] +} diff --git a/research/complex-signed-prefix-audit/controls.py b/research/complex-signed-prefix-audit/controls.py new file mode 100644 index 0000000000..58882ff827 --- /dev/null +++ b/research/complex-signed-prefix-audit/controls.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Exact frame-transport examples and semantic program rejection controls. + +Gareth Davidson, with substantial OpenAI Codex assistance. Apache-2.0. +Finite examples corroborate the written quantified proof; they do not replace it. +""" +import copy +from fractions import Fraction as Q +from itertools import product +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as audit + + +def mm(a, b): + return tuple(tuple(sum(x * y for x, y in zip(row, col)) for col in zip(*b)) for row in a) + + +def trans(a): + return tuple(zip(*a)) + + +def plus(a, b, q): + return tuple(tuple(x + q * y for x, y in zip(ar, br)) for ar, br in zip(a, b)) + + +def scale(a, q): + return tuple(tuple(q * x for x in row) for row in a) + + +def transport_examples(): + identity = ((Q(1), Q(0)), (Q(0), Q(1))) + rotation = ((Q(3, 5), Q(-4, 5)), (Q(4, 5), Q(3, 5))) + frames = [identity, scale(identity, -1), ((Q(1), Q(0)), (Q(0), Q(-1))), + ((Q(0), Q(1)), (Q(1), Q(0))), rotation, trans(rotation)] + for frame in frames: + audit.need(mm(frame, trans(frame)) == identity, "example frame unitarity") + cuts = cells = 0 + for a, b, c in product(range(len(frames)), repeat=3): + labels = [0, b, 0] + initial = list(labels) + shadow = [[Q(1), Q(0)], [Q(0), Q(1)], [Q(0), Q(0)]] + physical = [((Q(1), Q(0), Q(0), Q(0)), (Q(0), Q(1), Q(0), Q(0))), + ((Q(0), Q(0), Q(1), Q(0)), (Q(0), Q(0), Q(0), Q(1))), + ((Q(0),) * 4,) * 2] + events = [("relabel", 0, a), ("relabel", 1, a), ("add", 0, 1, Q(3, 2)), + ("relabel", 0, c), ("scale", 0, Q(-2)), ("copy", 2, 0), + ("relabel", 2, a), ("relabel", 1, c), ("add", 1, 0, Q(-1, 2)), + ("clear", 2), ("relabel", 0, b)] + for event in events: + kind, target, *rest = event + if kind == "relabel": + new = rest[0] + physical[target] = mm(mm(frames[new], trans(frames[labels[target]])), physical[target]) + labels[target] = new + elif kind == "add": + source, q = rest + audit.need(labels[target] == labels[source], "example common frame") + physical[target] = plus(physical[target], physical[source], q) + shadow[target] = [x + q * y for x, y in zip(shadow[target], shadow[source])] + elif kind == "scale": + physical[target] = scale(physical[target], rest[0]) + shadow[target] = [rest[0] * x for x in shadow[target]] + elif kind == "copy": + source = rest[0] + labels[target] = labels[source] + physical[target] = physical[source] + shadow[target] = list(shadow[source]) + else: + physical[target] = ((Q(0),) * 4,) * 2 + shadow[target] = [Q(0), Q(0)] + for r in range(3): + blocks = [scale(mm(frames[labels[r]], trans(frames[initial[j]])), shadow[r][j]) + for j in range(2)] + expected = tuple(blocks[0][i] + blocks[1][i] for i in range(2)) + audit.need(physical[r] == expected, "physical prefix conjugation") + cells += 8 + cuts += 1 + # All numbers below are exact. These are failures of weakened hypotheses, + # not alleged admission bugs in the selected construction. + # copy b=a=1; change b's label by -I; inadmissible a-=b. + a, b = Q(1), Q(1) + b = -b + a -= b + audit.need(a == 2 and (Q(1) - Q(1)) == 0, "mismatched frame witness") + # Closed continuation restores a and clears private b: endpoint a=1. + a += b + b = -b + b = Q(0) + audit.need((a, b) == (1, 0), "closed mismatch endpoint") + # Exact, well-labelled relabels with a nonunitary T have scalar shadow I. + # Relabel I -> diag(8,1) -> I has physical peak 8 and endpoint 1. + x = Q(1) + x *= 8 + nonunitary_peak = x + x /= 8 + audit.need(nonunitary_peak == 8 and x == 1, "nonunitary label witness") + # Both declared labels end at -I, but the first recipe wrongly executes I. + # Starting after copy b=a: wrong a relabel, exact b relabel, then a-=b. + a, b = Q(1), Q(-1) + a -= b + audit.need(a == 2, "inexact recipe witness") + # A partially stored unit-norm vector may exceed either endpoint norm. + # Old=(3/5,4/5), new=(1,0), store the first coordinate first. + partial_squared = Q(1) + Q(4, 5) ** 2 + audit.need(partial_squared == Q(41, 25) and 1 < partial_squared < 2, + "split-component norm witness") + return dict(frame_choices=len(frames), words=6 ** 3, prefix_cuts=cuts, + exact_matrix_entries=cells, adverse=[ + "unitary mismatched labels: shadow peak 1, physical peak 2, restored endpoint", + "nonunitary exact labels: shadow peak 1, physical peak 8, identity endpoint", + "unitary labels with inexact recipe: shadow zero, physical value 2", + "partially stored unit vectors: squared norm 41/25 > 1; factor-two square bound needed"]) + + +def rejection_controls(): + word, programs, _, _, _, _ = audit.load() + events = programs["forward"] + rejected = {} + + def reject(name, change, expected_message): + mutant = copy.deepcopy(events) + change(mutant) + try: + audit.audit(word, mutant, "forward", crosscheck=False) + except audit.AuditError as exc: + audit.need(expected_message in str(exc), "wrong rejection: " + name + ": " + str(exc)) + rejected[name] = str(exc) + else: + raise audit.AuditError("accepted mutation: " + name) + + reject("wrong_common_frame", lambda es: next(e for e in es if e[0] == "scalar" and e[2] != 0) + .__setitem__(2, 0), "common scalar frame") + reject("omit_climb", lambda es: es.pop(next(i for i, e in enumerate(es) if e[0] == "climb")), + "common scalar frame") + reject("wrong_wrapper_terminal_pair", lambda es: next(e for e in es if e[0] == "residual_adapter" + and len(e) == 5).__setitem__(4, 1), + "wrapper terminal pair") + reject("premature_post_wrapper", lambda es: es.insert(es.index(["phase", "A"]) + 1, + es.pop(next(i for i, e in enumerate(es) if e[0] == "residual_adapter" and e[1] == "post"))), + "post wrapper placement") + reject("coefficient_source_alias", lambda es: next(e for e in es if e[0] == "scalar" + and e[1][0] == "add")[1].__setitem__(1, next(e for e in es if e[0] == "scalar" + and e[1][0] == "add")[1][2]), "coefficient source alias") + reject("non_dyadic_scale", lambda es: next(e for e in es if e[0] == "scalar" + and e[1][0] == "scale")[1].__setitem__(3, 3), "dyadic coefficient") + reject("wrong_power_two_scale_endpoint", lambda es: next(e for e in es if e[0] == "scalar" + and e[1][0] == "scale")[1].__setitem__(2, -2), "scalar endpoint") + saved = json.loads((audit.PACKAGE / "EXPECTED.json").read_text()) + forward = saved["orientations"]["forward"] + value = audit.literal_witness(events, forward["peak_witness"], 704) + audit.need(Q(value["primitive_peak"]) > Q(forward["register_peak"]), "scratch-work adverse witness") + rejected["register_only_precision_bound"] = "131088 > 131072 at coefficient preparation" + return rejected + + +def main(): + receipt = dict(transport=transport_examples(), program_controls=rejection_controls()) + expected = json.loads((audit.PACKAGE / "CONTROLS.json").read_text()) + audit.need(receipt == expected, "control receipt mismatch") + print("PASS_SIGNED_PREFIX_CONTROLS", "unitary_words=216 cuts=2376 program_controls=8", + "receipt_sha256=" + audit.digest(audit.canonical(receipt))) + + +if __name__ == "__main__": + main() diff --git a/research/complex-signed-prefix-audit/source_check.py b/research/complex-signed-prefix-audit/source_check.py new file mode 100644 index 0000000000..52dd2fe191 --- /dev/null +++ b/research/complex-signed-prefix-audit/source_check.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python3 +"""Replay the byte-pinned original local driver, including all 25 controls. + +Gareth Davidson, with OpenAI Codex assistance. Apache-2.0. +This is separate from the independent signed-prefix verifier. +""" +import json +from pathlib import Path +import subprocess +import sys +import tarfile +import tempfile + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as audit + + +def run(): + audit.pins() + with tempfile.TemporaryDirectory(prefix="signed-prefix-source-") as temp: + work = Path(temp) + with tarfile.open(audit.ROOT / audit.ARCHIVE) as archive: + for name in ("CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz"): + (work / name).write_bytes(archive.extractfile(audit.BASE + name).read()) + retained = json.loads(archive.extractfile(audit.BASE + "INDEPENDENT-LOCAL-REPLAY.json").read()) + # -I ignores PYTHONOPTIMIZE; no -O is passed. All original asserts run. + proc = subprocess.run([sys.executable, "-I", "-B", str(audit.ROOT / audit.LOCAL_CHECKER), str(work)], + text=True, capture_output=True, timeout=180) + audit.need(proc.returncode == 0, "original driver failed:\n" + proc.stdout + proc.stderr) + fresh = json.loads((work / "INDEPENDENT-LOCAL-REPLAY.json").read_text()) + audit.need(fresh == retained, "complete original local receipt changed") + audit.need(len(fresh["negative_controls_rejected"]) == 25, "original control coverage") + print("PASS_ORIGINAL_LOCAL_DRIVER", "orientations=2 columns=704 controls=25 receipt_identical") + print("receipt_sha256=" + audit.digest(audit.canonical(fresh))) + + +if __name__ == "__main__": + run() diff --git a/research/complex-signed-prefix-audit/test_package.py b/research/complex-signed-prefix-audit/test_package.py new file mode 100644 index 0000000000..720a89773b --- /dev/null +++ b/research/complex-signed-prefix-audit/test_package.py @@ -0,0 +1,110 @@ +#!/usr/bin/env python3 +"""Read-only relocation, source/receipt corruption and exact-kernel tests. + +Gareth Davidson, with OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as audit + + +class PackageTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.temp = tempfile.TemporaryDirectory(prefix="signed prefix relocation ") + cls.root = Path(cls.temp.name) + cls.package = cls.root / "research" / audit.PACKAGE.name + shutil.copytree(audit.PACKAGE, cls.package, ignore=shutil.ignore_patterns("__pycache__")) + for name in audit.INPUTS: + dest = cls.root / name + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(audit.ROOT / name, dest) + + @classmethod + def tearDownClass(cls): + cls.temp.cleanup() + + def command(self, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py"), *args], + cwd="/tmp", text=True, capture_output=True, timeout=120) + + def test_strict_bit_boundary(self): + for value, expected in [(Q(1), 1), (Q(2), 2), (Q(3, 2), 1), (Q(1, 2), 0), + (Q(131072), 18), (Q(131088), 18), (Q(1154896), 21)]: + self.assertEqual(audit.strict_bits(value), expected) + + def test_dense_cancellation_and_alias_free_copy(self): + engine = audit.DenseDyadic(3) + engine.step(["copy", ["C", 0], ["L", 0]]) + engine.step(["add", ["L", 0], ["L", 1], -3, 8]) + engine.step(["scale", ["L", 1], 1, -2]) + engine.step(["add", ["L", 0], ["L", 1], -3, 4]) + engine.compare(("L", 0), {0: Q(1)}) + engine.compare(("C", 0), {0: Q(1)}) + engine.step(["clear", ["L", 0]]) + engine.compare(("L", 0), {}) + + def test_read_only_relocation(self): + files = [p for p in self.root.rglob("*") if p.is_file()] + before = {str(p.relative_to(self.root)): audit.digest(p.read_bytes()) for p in files} + try: + for path in files: + path.chmod(0o444) + result = self.command() + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn("PASS_COMPLEX_SIGNED_PREFIX_AUDIT", result.stdout) + after = {str(p.relative_to(self.root)): audit.digest(p.read_bytes()) + for p in self.root.rglob("*") if p.is_file()} + self.assertEqual(before, after) + finally: + for path in files: + path.chmod(0o644) + + def test_source_corruption(self): + path = self.root / audit.LOCAL_CHECKER + original = path.read_bytes() + try: + path.write_bytes(original + b"\n# corruption control\n") + result = self.command() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source hash:", result.stderr) + finally: + path.write_bytes(original) + + def test_missing_input_pin(self): + path = self.package / "SOURCES.json" + original = path.read_bytes() + try: + value = json.loads(original) + value["files"] = [r for r in value["files"] if r["path"] != audit.LOCAL_CHECKER] + path.write_text(json.dumps(value)) + result = self.command() + self.assertNotEqual(result.returncode, 0) + self.assertIn("mandatory source inventory", result.stderr) + finally: + path.write_bytes(original) + + def test_receipt_corruption(self): + path = self.package / "EXPECTED.json" + original = path.read_bytes() + try: + value = json.loads(original) + value["orientations"]["backward"]["exact_peak"] = "1154895" + path.write_text(json.dumps(value)) + result = self.command() + self.assertNotEqual(result.returncode, 0) + self.assertIn("committed receipt mismatch", result.stderr) + finally: + path.write_bytes(original) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/complex-signed-prefix-audit/verify.py b/research/complex-signed-prefix-audit/verify.py new file mode 100644 index 0000000000..9b9acbff43 --- /dev/null +++ b/research/complex-signed-prefix-audit/verify.py @@ -0,0 +1,468 @@ +#!/usr/bin/env python3 +"""Exact signed-prefix audit of the unchanged selected PR1094 local words. + +Gareth Davidson, with substantial OpenAI Codex assistance. Apache-2.0. +Uses the credited Lemma G conjugation invariant; imports no predecessor code. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +ARCHIVE = "research/community-frontier1094-audit/selected-replay.tar.gz" +MANIFEST = "research/community-frontier1094-audit/SELECTED-SOURCE.json" +LOCAL_CHECKER = "research/complex-k492-owner-repair/code/hpe_audit_local.py" +INVOICE = "research/gauge44-slots-t16/code/invoice_allcold.py" +BASE = "candidate/strict/global/base/providers/gauge44/" +INPUTS = {ARCHIVE, MANIFEST, LOCAL_CHECKER, INVOICE, + "research/e8-lemma-g-lean/PROOF.md", "research/hyperplane-end-lean/PROOF.md"} + + +class AuditError(ValueError): + pass + + +def need(condition, message): + if not condition: + raise AuditError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def pins(root=ROOT): + source = json.loads((PACKAGE / "SOURCES.json").read_text()) + live = [x for x in source["files"] if x["usage"] == "input"] + need(len(live) == len(INPUTS) and {x["path"] for x in live} == INPUTS, + "mandatory source inventory") + for item in live: + need(digest((root / item["path"]).read_bytes()) == item["sha256"], + "source hash: " + item["path"]) + selected = json.loads((root / MANIFEST).read_text())["files"] + need(selected[INVOICE] == digest((root / INVOICE).read_bytes()), "selected invoice binding") + need(selected["research/complex-sw4-frame8/local/hpe_audit_local.py"] + == digest((root / LOCAL_CHECKER).read_bytes()), "selected local checker binding") + return {x["path"]: x["sha256"] for x in live} + + +def load(root=ROOT): + hashes = pins(root) + with tarfile.open(root / ARCHIVE) as archive: + def raw(name): + matches = [m for m in archive.getmembers() if m.name == name] + need(len(matches) == 1 and matches[0].isfile(), "unique regular archive member") + return archive.extractfile(matches[0]).read() + def read(name): + b = raw(name) + return json.loads(gzip.decompress(b) if name.endswith(".gz") else b) + word = read(BASE + "CANONICAL-WORD.json.gz") + programs = read(BASE + "LOCAL-PROGRAMS.json.gz") + retained = read(BASE + "INDEPENDENT-LOCAL-REPLAY.json") + checks = read(BASE + "LOCAL-CHECKS.json") + template = read("candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz") + global_prefix = read("candidate/strict/global/audit/GLOBAL-PREFIX.json") + payload = gzip.decompress(raw("candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz")) + need(digest(payload) == global_prefix["template_sha256"], "global template binding") + need(set(template["local_providers"]) == {"gauge44"}, "selected provider set") + reg = template["local_providers"]["gauge44"] + for name, field in [("CANONICAL-WORD.json.gz", "canonical_word_sha256"), + ("LOCAL-PROGRAMS.json.gz", "local_programs_sha256")]: + need(digest(raw(BASE + name)) == retained[field], "local receipt source binding") + need(reg["canonical_word_sha256"] == retained["canonical_word_sha256"], "provider word") + need(programs == reg["local_programs"] and checks == reg["local_program_checks"], + "provider programs/checks") + need(set(programs) == {"forward", "backward"}, "two orientations") + for name, events in programs.items(): + ph = digest(json.dumps(events, separators=(",", ":")).encode()) + need(ph == checks[name]["sha256"], "program hash") + calls = [c for c in template["calls"] if c["orientation"] == name] + need(calls and all(c["local_program_sha256"] == ph and c["provider_id"] == "gauge44" + for c in calls), "all invocation program bindings") + counts = Counter(e["kind"] for e in template["execution_schedule"]) + need(len(template["calls"]) == counts["local_cover_sweep"] + == global_prefix["complete_invocation_cover_sweeps"] == 144, "invocation count") + need(counts["bridge"] == global_prefix["bridge_factor_two_sweeps"] == 144, "bridge count") + need((word["v"], word["R"], word["h"]) == (112, 480, 9), "selected dimensions") + return word, programs, retained, checks, global_prefix, hashes + + +def coefficient(a, b): + need(type(a) is int and type(b) is int and a != 0 and b != 0, "nonzero rational") + q = Q(a, b) + need(q.denominator & (q.denominator - 1) == 0, "dyadic coefficient") + return q + + +def row_record(row): + return [[j, q.numerator, q.denominator] for j, q in sorted(row.items())] + + +def l1(row): + return sum(map(abs, row.values()), Q(0)) + + +def strict_bits(value): + need(value > 0, "positive norm") + k = max(0, value.numerator.bit_length() - value.denominator.bit_length()) + while value >= 2 ** k: + k += 1 + need(value < 2 ** k and (k == 0 or value >= Q(2) ** (k - 1)), "strict bit boundary") + return k + + +class DenseDyadic: + """Independent integer rows; updates and reductions do not use Fraction.""" + def __init__(self, n): + self.n = n + self.rows = {("L", j): (tuple(int(k == j) for k in range(n)), 0) for j in range(n)} + + def normalize(self, nums, exponent): + nonzero = [abs(x) for x in nums if x] + if not nonzero: + return (0,) * self.n, 0 + shift = min(exponent, min((x & -x).bit_length() - 1 for x in nonzero)) + return tuple(x >> shift for x in nums), exponent - shift + + def step(self, op): + tag, target = op[0], tuple(op[1]) + if tag == "clear": + self.rows[target] = ((0,) * self.n, 0) + elif tag == "copy": + self.rows[target] = self.rows[tuple(op[2])] + elif tag in ("scale", "add"): + a, b = op[-2:] + if b < 0: + a, b = -a, -b + need(b > 0 and b & (b - 1) == 0, "dense dyadic denominator") + shift = b.bit_length() - 1 + if tag == "scale": + row, exponent = self.rows[target] + self.rows[target] = self.normalize([a * x for x in row], exponent + shift) + else: + row, exponent = self.rows.get(target, ((0,) * self.n, 0)) + src, sexp = self.rows[tuple(op[2])] + dest_exp = max(exponent, sexp + shift) + nums = [(x << (dest_exp - exponent)) + a * (y << (dest_exp - sexp - shift)) + for x, y in zip(row, src)] + self.rows[target] = self.normalize(nums, dest_exp) + else: + raise AuditError("dense unknown scalar") + + def compare(self, target, sparse): + nums, exponent = self.rows[target] + need(sum(x != 0 for x in nums) == len(sparse), "dense/sparse support") + scale = 1 << exponent + need(all(nums[j] * value.denominator == value.numerator * scale + for j, value in sparse.items()), "dense/sparse row") + + +def audit(word, events, name, crosscheck=True): + n = 2 * word["v"] + word["R"] + rows = {("L", j): {j: Q(1)} for j in range(n)} + envelope = {("L", j): Q(1) for j in range(n)} + dense = DenseDyadic(n) if crosscheck else None + cur, private = list(word["start"]), {} + wrapped = {j for j in range(2 * word["v"], n) + if word["start"][j] != 0 or word["final"][j] != 1} + pre, post, entry, exit_ = set(), set(), set(), set() + phase, witness = None, None + scalar_count = wrapper_units = 0 + peak = ordinary = work_peak = positive = Q(1) + trace, phase_peaks, phases = hashlib.sha256(), {}, [] + + def observe(value, i, kind, register, row): + nonlocal peak, witness + if value > peak: + peak = value + witness = dict(event_index=i, kind=kind, register=list(register), phase=phase, + l1=str(value), row=row_record(row)) + phase_peaks[phase] = max(phase_peaks.get(phase, Q(1)), value) + + def frame(reg, f, target=False): + if reg[0] == "L": + need(0 <= reg[1] < n and cur[reg[1]] == f, "common scalar frame") + if reg[1] in wrapped: + need(reg[1] in pre and reg[1] not in post, "scalar outside wrapper interval") + else: + need(reg[0] == "C" and 0 <= reg[1] < len(word["centers"]), "private namespace") + if target and reg not in private: + need(not rows.get(reg), "unlabelled nonzero private row") + private[reg] = f + need(private.get(reg) == f, "private common frame") + + for i, event in enumerate(events): + tag = event[0] + if tag == "phase": + phase = event[1] + phases.append(phase) + phase_peaks[phase] = max([Q(1)] + [l1(row) for row in rows.values()]) + elif tag == "adapter": + _, direction, r, f = event + if direction == "old_to_new": + need(phase == "entry_adapters" and r not in wrapped and r not in entry + and f == word["start"][r], "entry adapter") + entry.add(r) + else: + need(direction == "new_to_old" and phase == "exit_adapters" and r not in exit_ + and f == word["final"][r] and (r < 2 * word["v"] or f == 1), "exit adapter") + exit_.add(r) + elif tag == "residual_adapter": + _, direction, r, f, *end = event + need(r in wrapped and f == word["start"][r], "wrapper role and entrance") + need(end == ([word["final"][r]] if word["final"][r] != 1 else []), "wrapper terminal pair") + need(rows["L", r] == {r: Q(1)}, "wrapper unit row") + wrapper_units += 1 + if direction == "pre": + need(phase == "entry_adapters" and r not in pre, "pre wrapper placement") + pre.add(r) + else: + need(direction == "post" and phase == "full_frame_cleanup" and r in pre + and r not in post and cur[r] == word["final"][r], "post wrapper placement") + post.add(r) + elif tag == "climb": + _, part, r, a, b, rank = event + need(phase == part and cur[r] == a and rank > 0, "climb label transition") + cur[r] = b + elif tag == "center": + _, k, a, b, rank = event + need(phase == "centers" and private.get(("C", k)) == a and rank > 0, + "centre label transition") + private["C", k] = b + elif tag == "scalar": + _, op, f = event + kind, target = op[0], tuple(op[1]) + source = tuple(op[2]) if kind in ("add", "copy") else None + if kind == "clear" and target[0] == "C": + need(private.get(target, f) == f, "private clear frame") + private.pop(target, None) + else: + frame(target, f, target=True) + if source is not None: + frame(source, f) + if kind == "clear": + rows[target], envelope[target] = {}, Q(0) + elif kind == "copy": + rows[target], envelope[target] = rows[source].copy(), envelope[source] + elif kind == "scale": + q = coefficient(op[2], op[3]) + a = abs(q.numerator) + need(a & (a - 1) == 0, "power-of-two scale") + rows[target] = {j: q * x for j, x in rows[target].items()} + envelope[target] *= abs(q) + elif kind == "add": + need(source != target, "coefficient source alias") + q = coefficient(op[3], op[4]) + numerator = abs(q.numerator) + # Every unsigned-Horner/halving intermediate is k times this + # source row, with 0 <= k <= numerator (PROOF.md). + work = {j: numerator * x for j, x in rows[source].items()} + wnorm = l1(work) + work_peak = max(work_peak, wnorm) + observe(wnorm, i, "coefficient_numerator", source, work) + positive = max(positive, numerator * envelope[source]) + envelope[target] = envelope.get(target, Q(0)) + abs(q) * envelope[source] + row = rows.setdefault(target, {}) + for j, x in rows[source].items(): + value = row.get(j, Q(0)) + q * x + if value: + row[j] = value + else: + row.pop(j, None) + else: + raise AuditError("unknown scalar") + if dense is not None: + dense.step(op) + dense.compare(target, rows[target]) + scalar_count += 1 + rnorm = l1(rows[target]) + ordinary, positive = max(ordinary, rnorm), max(positive, envelope[target]) + observe(rnorm, i, "register", target, rows[target]) + trace.update(canonical([i, op, row_record(rows[target]), str(rnorm)])) + else: + raise AuditError("unknown event") + need(phases == ["zero_frame_precondition", "entry_adapters", "A", "centers", "B", + "cleanup_tail", "final", "exit_adapters", "full_frame_cleanup", "done"], + "phase sequence") + need(cur == word["final"] and not private, "final labels/private state") + need(pre == post == wrapped and entry == set(range(n)) - wrapped, "complete wrappers/entry") + need(exit_ == {j for j in range(n) if j < 2 * word["v"] or word["final"][j] == 1}, + "complete exit adapters") + for j in range(n): + expected = {j: Q(1)} + if name == "forward" and word["v"] <= j < 2 * word["v"]: + expected[j - word["v"]] = Q(1) + elif name == "backward" and j < word["v"]: + expected[j + word["v"]] = Q(-1) + need(rows["L", j] == expected, "scalar endpoint") + need(all(not row for reg, row in rows.items() if reg[0] == "C"), "private zero endpoints") + need(witness is not None, "nontrivial peak") + # Real/imaginary or coordinatewise execution can temporarily combine + # parts of two consecutive complex states. Orthogonal projection gives + # ||P v + (I-P) u||^2 <= ||v||^2 + ||u||^2 <= 2 * peak^2. + split_squared = 2 * peak * peak + split_bits = strict_bits(peak) + while split_squared >= 2 ** (2 * split_bits): + split_bits += 1 + return dict(events=len(events), scalar_prefixes=scalar_count, persistent_columns=n, + common_frame_checks=True, wrapper_unit_rows=wrapper_units, + exact_peak=str(peak), register_peak=str(ordinary), coefficient_peak=str(work_peak), + strict_bits=strict_bits(peak), positive_envelope=str(positive), + split_component_squared_bound=str(split_squared), split_component_bits=split_bits, + positive_strict_bits=strict_bits(positive), peak_witness=witness, + prefix_row_trace_sha256=trace.hexdigest(), + phase_peaks={k: str(v) for k, v in phase_peaks.items()}, dense_integer_crosscheck=crosscheck) + + +def adjoint_witness(events, witness): + """Pull one observed functional back, independently of forward row replay.""" + stop, reg = witness["event_index"], tuple(witness["register"]) + if witness["kind"] == "coefficient_numerator": + op = events[stop][1] + functional = {reg: Q(abs(coefficient(op[3], op[4]).numerator))} + prefix = events[:stop] + else: + functional, prefix = {reg: Q(1)}, events[:stop + 1] + for event in reversed(prefix): + if event[0] != "scalar": + continue + op, target = event[1], tuple(event[1][1]) + weight = functional.get(target, Q(0)) + if not weight: + continue + if op[0] == "clear": + functional.pop(target) + elif op[0] == "scale": + functional[target] *= Q(op[2], op[3]) + else: + source = tuple(op[2]) + if op[0] == "copy": + functional.pop(target) + q = Q(1) + else: + q = Q(op[3], op[4]) + value = functional.get(source, Q(0)) + q * weight + if value: + functional[source] = value + else: + functional.pop(source, None) + need(all(reg[0] == "L" for reg in functional), "witness depends on private initial input") + row = {reg[1]: x for reg, x in functional.items()} + need(row_record(row) == witness["row"], "reverse functional witness") + return row + + +def literal_witness(events, witness, n): + """Run every unsigned-Horner primitive numerically on the attaining input.""" + row = adjoint_witness(events, witness) + state = {("L", j): Q((row.get(j, 0) > 0) - (row.get(j, 0) < 0)) for j in range(n)} + peak, observed, primitives = Q(1), None, 0 + + def touch(value): + nonlocal peak, primitives + peak = max(peak, abs(value)) + primitives += 1 + + for i, event in enumerate(events): + if event[0] != "scalar": + continue + op, target = event[1], tuple(event[1][1]) + if op[0] == "clear": + state[target] = Q(0) + touch(state[target]) + elif op[0] == "copy": + state[target] = state[tuple(op[2])] + touch(state[target]) + elif op[0] == "scale": + q = Q(op[2], op[3]) + for _ in range(abs(q.numerator).bit_length() - 1): + state[target] *= 2 + touch(state[target]) + for _ in range(q.denominator.bit_length() - 1): + state[target] /= 2 + touch(state[target]) + if q < 0: + state[target] = -state[target] + touch(state[target]) + else: + q, source = Q(op[3], op[4]), state[tuple(op[2])] + work = Q(0) + touch(work) + for j, bit in enumerate(bin(abs(q.numerator))[2:]): + if j: + work *= 2 + touch(work) + if bit == "1": + work += source + touch(work) + if i == witness["event_index"] and witness["kind"] == "coefficient_numerator": + observed = work + for _ in range(q.denominator.bit_length() - 1): + work /= 2 + touch(work) + state[target] = state.get(target, Q(0)) + (work if q > 0 else -work) + touch(state[target]) + work = Q(0) + touch(work) + if i == witness["event_index"] and witness["kind"] == "register": + observed = state[tuple(witness["register"])] + need(observed == Q(witness["l1"]) == peak, "attaining primitive witness") + return dict(input_nonzero=len(row), input_sup=1, observed=str(observed), primitive_peak=str(peak), + real_component_primitives=2 * primitives, reverse_functional_matches=True) + + +def result(root=ROOT): + word, programs, retained, checks, global_prefix, hashes = load(root) + reports = {} + for name in ("forward", "backward"): + report = audit(word, programs[name], name) + old = retained["local"][name] + need(report["positive_envelope"] == old["prefix_l1_upper"] + and report["positive_strict_bits"] == old["prefix_bits_upper"], "positive-envelope comparison") + witness = literal_witness(programs[name], report["peak_witness"], report["persistent_columns"]) + need(witness["real_component_primitives"] == checks[name]["real_component_primitive_bound"], + "primitive recount matches source") + report["attainment"] = witness + reports[name] = report + local = max(r["split_component_bits"] for r in reports.values()) + oldlocal = max(r["positive_strict_bits"] for r in reports.values()) + need(oldlocal == global_prefix["local_scalar_coefficient_work_prefix_bits"], "retained local bound") + rest = sum(global_prefix[k] for k in ["stream_input_sup_to_l2_bits", "complete_invocation_cover_sweeps", + "bridge_factor_two_sweeps", "primitive_arithmetic_margin_bits"]) + need(oldlocal + rest == global_prefix["global_prefix_bits"], "retained global arithmetic") + return dict(status="PASS_COMPLEX_SIGNED_PREFIX_AUDIT", source_sha256=hashes, orientations=reports, + conditional_global=dict(old_local_bits=oldlocal, signed_local_bits=local, + unchanged_other_allowances=rest, old_sufficient_bits=oldlocal + rest, + signed_sufficient_bits=local + rest, + retained_payload_bits=global_prefix["retained_payload_bits"]), + scope="Exact scalar/Horner prefix and conditional unitary common-frame norm corollary. " + "Recursive child internals, physical compiler/hosting, roundoff, native admission " + "and analytic transfer remain inherited. No production payload or kappa change.") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write checked receipt to a new path") + args = parser.parse_args() + receipt = result() + need(receipt == json.loads((PACKAGE / "EXPECTED.json").read_text()), "committed receipt mismatch") + if args.output: + with args.output.open("x") as handle: + handle.write(json.dumps(receipt, indent=2) + "\n") + print(receipt["status"], "local_bits=52,68->18,21", + "conditional_global_bits=397->350 payload=512 kappa=unchanged", + "receipt_sha256=" + digest(canonical(receipt))) + + +if __name__ == "__main__": + main() From 851e5232f7c9e105fb6e8f3a7be7a070e7524012 Mon Sep 17 00:00:00 2001 From: Gareth Davidson Date: Tue, 13 Oct 2026 22:43:58 +0100 Subject: [PATCH 2/2] Record publication of signed prefix audit PR 1282 --- research/complex-signed-prefix-audit/README.md | 2 ++ research/complex-signed-prefix-audit/TASK.json | 4 +++- research/complex-signed-prefix-audit/VALIDATION.md | 5 +++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/research/complex-signed-prefix-audit/README.md b/research/complex-signed-prefix-audit/README.md index 45fc28b079..66f8074a3a 100644 --- a/research/complex-signed-prefix-audit/README.md +++ b/research/complex-signed-prefix-audit/README.md @@ -1,5 +1,7 @@ # Selected PR1094: signed prefix precision audit +Contribution: [PR1282](https://github.com/CrocSwap/integer-mult-bounds/pull/1282). + The unchanged R480 programs have exact signed scalar/Horner prefix maxima **131088 forward and 1154896 backward**, requiring sufficient **18/21-bit** envelopes rather than the retained positive-recurrence estimates of 52/68 diff --git a/research/complex-signed-prefix-audit/TASK.json b/research/complex-signed-prefix-audit/TASK.json index db56d2f147..8f29b8eff2 100644 --- a/research/complex-signed-prefix-audit/TASK.json +++ b/research/complex-signed-prefix-audit/TASK.json @@ -70,5 +70,7 @@ "source_parent_head": "589d1cedf5ef5f231182f4ec86408616311a8af0", "first_step": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", "claim_expires_utc": "2026-10-13T23:25:00Z", - "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1260" + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1260", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1282", + "mathematical_commit": "a7e3e61cd709ccbc22b3e938853e01f838048e72" } diff --git a/research/complex-signed-prefix-audit/VALIDATION.md b/research/complex-signed-prefix-audit/VALIDATION.md index 4fb4e7e100..c5a7344655 100644 --- a/research/complex-signed-prefix-audit/VALIDATION.md +++ b/research/complex-signed-prefix-audit/VALIDATION.md @@ -56,3 +56,8 @@ proofs, analytic assembly, Lean, or repository-wide historical suites. The original local checker is run fully; its source assumptions do not become a complete multiplication proof. Hosted PR CI is a separate status and is reported at publication rather than inferred from these local passes. + +Published as [PR1282](https://github.com/CrocSwap/integer-mult-bounds/pull/1282). +The mathematical package commit is `a7e3e61cd709ccbc22b3e938853e01f838048e72`; +the follow-up changes publication metadata only. Staged whitespace and local +documentation-link checks pass.