From 0581402f978addb2eda5306fd124001486c76b08 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 16:43:37 +0000 Subject: [PATCH] Add gate-operand export parity audit for #3004 OQ2 Destination-free gate source lists always make accumulate-XOR and sequential ADD agree; destination-in-sources lists can diverge under export-without-check. Answers the open #2977/#3004 supplier-boundary gate-operand obligation under priority revision 6. No new kappa. --- .../CERTIFICATE.json | 146 +++++++ .../MASTER-HANDOFF.md | 45 ++ research/gate-operand-export-parity/PROOF.md | 69 +++ research/gate-operand-export-parity/README.md | 82 ++++ .../gate-operand-export-parity/SOURCES.json | 55 +++ research/gate-operand-export-parity/TASK.json | 72 ++++ .../gate-operand-export-parity/VERIFY.json | 55 +++ .../gate-operand-export-parity/independent.py | 101 +++++ .../test_package.py | 116 +++++ research/gate-operand-export-parity/verify.py | 405 ++++++++++++++++++ 10 files changed, 1146 insertions(+) create mode 100644 research/gate-operand-export-parity/CERTIFICATE.json create mode 100644 research/gate-operand-export-parity/MASTER-HANDOFF.md create mode 100644 research/gate-operand-export-parity/PROOF.md create mode 100644 research/gate-operand-export-parity/README.md create mode 100644 research/gate-operand-export-parity/SOURCES.json create mode 100644 research/gate-operand-export-parity/TASK.json create mode 100644 research/gate-operand-export-parity/VERIFY.json create mode 100644 research/gate-operand-export-parity/independent.py create mode 100644 research/gate-operand-export-parity/test_package.py create mode 100644 research/gate-operand-export-parity/verify.py diff --git a/research/gate-operand-export-parity/CERTIFICATE.json b/research/gate-operand-export-parity/CERTIFICATE.json new file mode 100644 index 0000000000..97266283c5 --- /dev/null +++ b/research/gate-operand-export-parity/CERTIFICATE.json @@ -0,0 +1,146 @@ +{ + "claim": { + "dest_free_always_agree": true, + "dest_in_can_disagree": true, + "named_witnesses": { + "dest_with_src": { + "d": 0, + "exp": [ + 0, + 3, + 5 + ], + "srcs": [ + 1, + 0 + ], + "sym": [ + 3, + 3, + 5 + ], + "val0": [ + 7, + 3, + 5 + ] + }, + "self_even": { + "d": 0, + "exp": [ + 0, + 3, + 5 + ], + "srcs": [ + 0, + 0 + ], + "sym": [ + 7, + 3, + 5 + ], + "val0": [ + 7, + 3, + 5 + ] + } + }, + "small_domain": { + "dest_free_agree": 4686, + "dest_free_disagree": 0, + "dest_in_agree": 1152, + "dest_in_disagree": 3492, + "disagree_witnesses": [ + [ + 0, + [ + 0, + 0 + ] + ], + [ + 1, + [ + 0, + 1 + ] + ], + [ + 2, + [ + 0, + 2 + ] + ], + [ + 3, + [ + 0, + 3 + ] + ], + [ + 4, + [ + 0, + 4 + ] + ], + [ + 5, + [ + 0, + 5 + ] + ], + [ + 0, + [ + 1, + 0 + ] + ], + [ + 1, + [ + 1, + 1 + ] + ] + ] + } + }, + "controls": { + "checker_rejects": [ + "self_even", + "dest_with_src", + "dup_src", + "self_once" + ], + "dup_src_section_agrees": true, + "scatter_only_guard_misses_gate_self_operand": true, + "self_even_export_records": 27235, + "self_once_section_agrees": true + }, + "kappa_decimal": "0.001672660197076918", + "no_new_kappa": true, + "schema_version": 1, + "selected_word": { + "B0": [ + 127, + 111, + [ + 3 + ] + ], + "distinct_operand_gates": 5472, + "export_records": 27234, + "gates": 5472, + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + "status": "PASS_GATE_OPERAND_EXPORT_PARITY" +} diff --git a/research/gate-operand-export-parity/MASTER-HANDOFF.md b/research/gate-operand-export-parity/MASTER-HANDOFF.md new file mode 100644 index 0000000000..b2665b8c5d --- /dev/null +++ b/research/gate-operand-export-parity/MASTER-HANDOFF.md @@ -0,0 +1,45 @@ +# MASTER-HANDOFF — gate-operand-export-parity + +## Claim (one sentence) + +At the selected PR589 checker/exporter boundary, destination-free gate source +lists always make accumulate-XOR and sequential ADD agree, while +destination-in-sources lists can diverge; the checker rejects them and the +exporter does not. + +## Closest prior + +- #2977 scatter multiplicity counterexample +- #3004 scatter odd-multiplicity agreement; OQ2 left gate operands open +- #2992 / #3273 / #3346 scatter successor schemas (scatter-only) + +## New checkable fact + +Exact Sym/Exp lemma with exhaustive 4686 dest-free agreements, named +`self_even` / `dest_with_src` witnesses, selected-word 5472 distinct gates, +four checker rejects, exporter +1 record on `self_even`. + +## Evidence commands + +```sh +python3.12 -I -B research/gate-operand-export-parity/verify.py +python3.12 -I -O -Werror -B research/gate-operand-export-parity/verify.py +python3.12 -I -B research/gate-operand-export-parity/independent.py +python3.12 -I -B research/gate-operand-export-parity/test_package.py +python3.12 -B scripts/research_package.py --package research/gate-operand-export-parity +``` + +## Soft-overlap vs leave-alones + +Clear of stock-leaf / router / flag-0 / C5 / side-correction / present-head / +groups B–D native clusters. Touches only the #2977 supplier-boundary cascade +at the unanswered #3004 gate-operand OQ. + +## Attribution + +Author Wentao Li ``. Neutral AI assistance disclosure. +No `Co-authored-by: Victor Li`. No CrocSwap PR from this worker (master publishes). + +## Disposition + +Ready for master independent review / publish decision. Kappa unchanged. diff --git a/research/gate-operand-export-parity/PROOF.md b/research/gate-operand-export-parity/PROOF.md new file mode 100644 index 0000000000..d4b761dfb1 --- /dev/null +++ b/research/gate-operand-export-parity/PROOF.md @@ -0,0 +1,69 @@ +# Gate operand symbolic/export parity + +## Claim + +Let a multi-source gate be a triple `(f, d, srcs)` with destination register +`d` and ordered source list `srcs`. Over `F_2`, compare two operators that both +start from a pre-gate valuation `val0`: + +- **Sym** (selected symbolic checker): read every source from `val0`, form + `acc = ⊕_{s ∈ srcs} val0[s]`, then set `val[d] ← val0[d] ⊕ acc`. +- **Exp** (selected record exporter): for each `s` in `srcs` in order, set + `val[d] ← val[d] ⊕ val[s]` using the *current* valuation. + +Then: + +1. If `d ∉ srcs`, then Sym and Exp agree for every `val0` (even when `srcs` + contains repeated indices). +2. If `d ∈ srcs`, they need not agree. Concrete finite witnesses include + `srcs = [d, d]` and `srcs = [a, d]` for any `a ≠ d`. + +The selected PR589 checker rejects every gate with +`len(set([d] + srcs)) ≠ len([d] + srcs)` before export. The exporter does not +enforce distinctness. Scatter-only uniqueness guards therefore leave this gap +open. + +Selected kappa is unchanged. + +## Proof of (1) + +Assume `d ∉ srcs`. In Exp, every assignment writes only register `d`. Every +source read therefore observes `val0[s]`. The net update is + +```text +val[d] ← val0[d] ⊕ (⊕_{s ∈ srcs} val0[s]), +``` + +counting multiplicity. That is exactly Sym. Agreement is independent of order +and of whether source multiplicities are odd or even. + +## Proof of (2) by witness + +Take registers valued in `F_2` (or any `F_2`-vector space) and `d = 0`. + +- `srcs = [0, 0]`. Sym: `acc = val0[0] ⊕ val0[0] = 0`, so `val[0]` is unchanged. + Exp: first ADD forces `val[0] ← 0`; second ADD leaves it `0`. These differ + whenever `val0[0] ≠ 0`. +- `srcs = [1, 0]` with `a = 1 ≠ 0`. Sym: `acc = val0[1] ⊕ val0[0]`, so + `val[0] ← val0[1]`. Exp: after ADD from 1 one has `val[0] = val0[0] ⊕ val0[1]`; + the subsequent self-ADD forces `val[0] ← 0`. These differ whenever + `val0[1] ≠ 0`. + +## Relation to scatter parity (#2977 / #3004) + +For scatter rows the symbolic loop XORs once per occurrence while the exporter +emits one ADD per membership. They agree exactly when every positive +multiplicity is odd. Gate lists are different: both operators are +occurrence-based, yet they still diverge when the destination appears among +the sources because Exp re-reads the updated destination. #3004's open +question on gate operands treated distinctness as schema hygiene with "no +known divergent word"; the witnesses above are divergent under export-without +the checker. Accepted words cannot carry them only because the checker rejects +`bad operands` first. + +## What this does not claim + +- No production adoption and no new kappa. +- No claim that the selected word is defective: every D/A/B/C gate on the + pinned tuned word has distinct operands. +- No native C++ replay and no change to frozen exporters. diff --git a/research/gate-operand-export-parity/README.md b/research/gate-operand-export-parity/README.md new file mode 100644 index 0000000000..7679fbda9d --- /dev/null +++ b/research/gate-operand-export-parity/README.md @@ -0,0 +1,82 @@ +# Gate operand symbolic/export parity + +**Card `supplier-boundary-audit`, priority revision 6**, refined to PR +[#3004](https://github.com/CrocSwap/integer-mult-bounds/pull/3004) open question 2 +under the [#2977](https://github.com/CrocSwap/integer-mult-bounds/pull/2977) +checker/exporter cascade. No new kappa +(`0.001672660197076918`). + +#3004 characterised scatter rows and left gate operand lists as a schema-consistency +question, stating that accepted words cannot diverge and that “no known divergent +word exists.” This package supplies the missing gate-side contract: + +- **Sym** (checker): accumulate source XOR from the pre-gate valuation, then XOR + into the destination. +- **Exp** (exporter): sequential `ADD` of each listed source into the destination, + re-reading the current valuation. + +If the destination is absent from the source list, Sym and Exp always agree — even +with repeated sources. If the destination appears among the sources, they can +disagree. Concrete witnesses include `srcs = [d, d]` and `srcs = [a, d]`. + +The selected checker rejects every non-distinct operand list (`bad operands`) +before export. The exporter does not enforce distinctness and will emit the +extra `ADD`s. A scatter-only uniqueness guard therefore misses this gap. + +```sh +python3.12 -I -B research/gate-operand-export-parity/verify.py +``` + +Expected: + +```text +PASS_GATE_OPERAND_EXPORT_PARITY dest_free_agree=4686 dest_in_disagree_witnesses=2 selected_distinct_gates=5472 checker_rejects=4 no_new_kappa +``` + +## Evidence + +- Exhaustive census on 6 registers and source lists of length 0..4: **4686/4686** + destination-free patterns agree; destination-in patterns include disagreements. +- Named witnesses `self_even` and `dest_with_src` diverge on integer valuations; + destination-free duplicate sources still agree. +- Pinned selected tuned word: all **5472** D/A/B/C gates have distinct operands; + baseline export has **27234** records. +- Mutating `B[0]` from `[127, 111, [3]]` to self-operand forms: checker rejects + all four mutants with `bad operands`; exporter still runs and the `self_even` + mutant emits **27235** records. +- Scatter rows of the self-operand mutant remain unique, so a scatter-only guard + accepts them. + +Default verify is read-only against `CERTIFICATE.json`. Admission uses `need()` +and stays enforced under `python -O`. Explicit `--write` regenerates the +certificate only. + +## Reproduce + +```sh +python3.12 -I -B research/gate-operand-export-parity/verify.py +python3.12 -I -O -Werror -B research/gate-operand-export-parity/verify.py +python3.12 -I -B research/gate-operand-export-parity/independent.py +python3.12 -I -B research/gate-operand-export-parity/test_package.py +python3.12 -B scripts/research_package.py --package research/gate-operand-export-parity +``` + +## Open next questions + +1. **Should a successor schema reject destination-in-sources gates at export time?** + First step: compose the distinct-operand check with an existing opt-in boundary + (`simple-scatter-v1` / `integer-xor-scatter-v1`) before export. Blocked by + maintainer schema adoption, not by arithmetic. +2. **Does native legality independently reject self-operand gates?** First step: + feed the `self_even` export into the native column checker. Blocked by a C++ + toolchain in this session; not required for the Sym/Exp lemma. + +## Credit + +Nick Petalas / #2977 named the scatter multiplicity gap. Kumagi / #3004 gave the +exact scatter agreement contract and left the gate-operand question open. Dylan +Crow authored the exporter; eumemic the symbolic checker; the tuned PR589 word +is the retained selected bit supplier. Predecessor notices are unchanged. + +Prepared by Wentao Li with substantial AI assistance. Apache-2.0. +No independent human or proof-assistant review is claimed. diff --git a/research/gate-operand-export-parity/SOURCES.json b/research/gate-operand-export-parity/SOURCES.json new file mode 100644 index 0000000000..13ef2a34aa --- /dev/null +++ b/research/gate-operand-export-parity/SOURCES.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "size_bytes": 42353 + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "size_bytes": 21651 + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "size_bytes": 3745 + }, + { + "path": "research/scatter-parity-contract-audit/README.md", + "usage": "provenance", + "git_blob": "81cbe8e1756e0952028524addb0ed33188e617d1", + "sha256": "824ea617d818674b25c4d3dc7c7f6a7e252e217837d8473c2409d08096a48788", + "size_bytes": 7389 + }, + { + "path": "research/scatter-parity-contract-audit/TASK.json", + "usage": "provenance", + "git_blob": "fd03dc4c2c5028954e2165fb2358a3dfc70fae56", + "sha256": "b3619e9ad0c4b17b3f5ddffbe55fb25728bb3164fe32d4f614983cb8db28a7e9", + "size_bytes": 7192 + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "size_bytes": 10725 + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "size_bytes": 58553 + } + ] +} diff --git a/research/gate-operand-export-parity/TASK.json b/research/gate-operand-export-parity/TASK.json new file mode 100644 index 0000000000..c23c9b8f17 --- /dev/null +++ b/research/gate-operand-export-parity/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md", + "research/scatter-export-parity-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2977 reported duplicate-scatter counterexample and its opt-in repair. The archive is not a production fix or an independently validated selected-result failure; the selected generator emits unique rows.", + "scope": "Source-binding orientation only; does not replay or validate the reported bug." + }, + "first_experiment": "First check whether the scatter repair has been adopted. If still open, independently reproduce #2977 symbolic-versus-exported parity on the tiny duplicate fixture, compare the selected unique-row positive control, and define either enforced uniqueness or consistent multiplicity semantics. A bounded guard-adoption patch must preserve valid inputs and test the actual exported action. Stop after this obligation; no full historical replay or frontier change follows from the mutant alone.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics" + ] + }, + "scope_status": "refined", + "actual_scope": "For the frozen symbolic checker and record exporter, when do D/A/B/C gate operand lists make accumulate-XOR and sequential ADD agree, and do destination-in-sources gates diverge under export-without-check?", + "scope_change_reason": "PR #3004 answered the scatter agreement contract and left gate operand lists as open question 2, claiming no known divergent word and treating distinctness as schema hygiene. This package answers that obligation with an exact Sym/Exp lemma, exhaustive small-domain census, named witnesses, and selected-word/checker/exporter controls.", + "bottleneck_link": "The checker/exporter pair is a selected source-bound acceptance condition. Knowing that gate self-operands diverge under export while destination-free duplicates do not tells a successor schema what must be enforced beyond scatter uniqueness.", + "budget_minutes": 60, + "stop_rule": "Stop after the Sym/Exp lemma, small-domain census, named witnesses, selected-word distinct-operand census, checker rejects, and exporter self_even control. No native replay, production adoption, or kappa change.", + "outcome": "completed", + "evidence": "CERTIFICATE.json, PROOF.md, verify.py, independent.py and test_package.py. On 4686 destination-free patterns Sym=Exp always; destination-in witnesses self_even and dest_with_src diverge; all 5472 selected gates are distinct; checker rejects four B[0] mutants; exporter emits 27235 records on self_even.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for reading the #2977/#3004 cascade, deriving the Sym/Exp lemma, implementing the verifier and controls, and writing this package.", + "open_questions": [ + { + "question": "Should a successor schema reject destination-in-sources gates at export time?", + "why_it_matters": "Scatter-only uniqueness leaves self-operand gates unchecked at the exporter boundary.", + "first_step": "Compose a distinct-operand gate check with an existing opt-in boundary before export and replay selected artifacts.", + "blocked_by": "Maintainer schema adoption; frozen exporters stay unchanged." + }, + { + "question": "Does native legality independently reject self-operand gate exports?", + "why_it_matters": "It decides whether the symbolic checker is the only barrier or a later native check also rejects them.", + "first_step": "Feed the self_even export into the native column checker with the standard empty-owner staging.", + "blocked_by": "A C++17 toolchain and Boost native replay; not required for the Sym/Exp lemma." + } + ] +} diff --git a/research/gate-operand-export-parity/VERIFY.json b/research/gate-operand-export-parity/VERIFY.json new file mode 100644 index 0000000000..9d1be39777 --- /dev/null +++ b/research/gate-operand-export-parity/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pins; dest-free agreement census; named dest-in witnesses; selected-word distinct-operand census; checker rejects four mutants; exporter emits extra ADD on self_even; certificate admission." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "need() admission remains enforced under -O; identical PASS marker." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Independent small-domain lemma and named witnesses without importing verify.py helpers." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Duplicate JSON keys rejected; temp certificate corruption rejected; package files unchanged after read-only verify." + } + ] +} diff --git a/research/gate-operand-export-parity/independent.py b/research/gate-operand-export-parity/independent.py new file mode 100644 index 0000000000..de8de6ba2a --- /dev/null +++ b/research/gate-operand-export-parity/independent.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Independent recompute of the gate operand Sym/Exp lemma. + +Does not import verify.py helpers. Standard library only. +""" + +from __future__ import annotations + +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +MARKER = ( + "PASS_GATE_OPERAND_INDEPENDENT " + "dest_free_agree=4686 dest_in_disagree>0 " + "witnesses=self_even,dest_with_src" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + value = {} + for key, item in pairs: + need(key not in value, "duplicate JSON key") + value[key] = item + return value + + +def sym_coeffs(d, srcs, n): + basis = [[1 if i == j else 0 for j in range(n)] for i in range(n)] + acc = [0] * n + for s in srcs: + acc = [a ^ b for a, b in zip(acc, basis[s])] + return tuple(a ^ b for a, b in zip(basis[d], acc)) + + +def exp_coeffs(d, srcs, n): + cur = [[1 if i == j else 0 for j in range(n)] for i in range(n)] + for s in srcs: + cur[d] = [a ^ b for a, b in zip(cur[d], cur[s])] + return tuple(cur[d]) + + +def main(): + n = 6 + dest_free_agree = 0 + dest_free_disagree = 0 + dest_in_disagree = 0 + for length in range(0, 5): + for srcs in itertools.product(range(n), repeat=length): + for d in range(n): + agree = sym_coeffs(d, srcs, n) == exp_coeffs(d, srcs, n) + if d not in srcs: + if agree: + dest_free_agree += 1 + else: + dest_free_disagree += 1 + elif not agree: + dest_in_disagree += 1 + need(dest_free_disagree == 0, "dest-free disagreement") + need(dest_free_agree == 4686, "dest-free count") + need(dest_in_disagree > 0, "dest-in disagreements exist") + + # Named witnesses over integer valuations (F2 action on each bit). + def symbolic(d, srcs, val): + out = list(val) + acc = 0 + for s in srcs: + acc ^= val[s] + out[d] ^= acc + return out + + def export_seq(d, srcs, val): + out = list(val) + for s in srcs: + out[d] ^= out[s] + return out + + need(symbolic(0, [0, 0], [7, 3, 5]) != export_seq(0, [0, 0], [7, 3, 5]), + "self_even") + need(symbolic(0, [1, 0], [7, 3, 5]) != export_seq(0, [1, 0], [7, 3, 5]), + "dest_with_src") + need(symbolic(0, [1, 1, 2], [7, 3, 5]) == export_seq(0, [1, 1, 2], [7, 3, 5]), + "dest_free_dup") + + cert = json.loads( + (HERE / "CERTIFICATE.json").read_text(), + object_pairs_hook=pairs_unique, + ) + need(cert["claim"]["small_domain"]["dest_free_agree"] == 4686, "cert census") + need(cert["no_new_kappa"] is True, "no new kappa") + print(MARKER) + + +if __name__ == "__main__": + main() diff --git a/research/gate-operand-export-parity/test_package.py b/research/gate-operand-export-parity/test_package.py new file mode 100644 index 0000000000..34a16859bf --- /dev/null +++ b/research/gate-operand-export-parity/test_package.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Behavioral controls for gate-operand-export-parity.""" + +from __future__ import annotations + +import hashlib +import json +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import verify # noqa: E402 + +MARKER = "PASS_GATE_OPERAND_PACKAGE_TESTS" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def file_hashes(directory): + rows = {} + for path in sorted(directory.rglob("*")): + if path.is_file(): + rows[str(path.relative_to(directory))] = hashlib.sha256( + path.read_bytes() + ).hexdigest() + return rows + + +def test_duplicate_json_keys(): + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "dup.json" + path.write_text('{"a": 1, "a": 2}\n', encoding="utf-8") + try: + verify.read_json(path) + except ValueError as exc: + need(str(exc) == "duplicate JSON key", "duplicate message") + else: + need(False, "duplicate key accepted") + + +def test_certificate_corruption_rejected(): + observed = verify.evaluate() + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "CERTIFICATE.json" + blob = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + blob["claim"]["dest_free_always_agree"] = False + path.write_text(json.dumps(blob, indent=2, sort_keys=True) + "\n", encoding="utf-8") + bad = verify.read_json(path) + try: + verify.need(observed == bad, "certificate mismatch") + except ValueError as exc: + need(str(exc) == "certificate mismatch", "corruption message") + else: + need(False, "corrupt certificate accepted") + live = verify.read_json(HERE / "CERTIFICATE.json") + need(live["claim"]["dest_free_always_agree"] is True, "on-disk certificate mutated") + + +def test_optimized_admission(): + script = ( + "import sys\n" + "from pathlib import Path\n" + f"sys.path.insert(0, {str(HERE)!r})\n" + "import verify\n" + "verify.need(__debug__ is False, 'optimization off')\n" + "try:\n" + " verify.need(False, 'admission')\n" + "except ValueError as exc:\n" + " if str(exc) != 'admission':\n" + " raise SystemExit('wrong admission')\n" + "else:\n" + " raise SystemExit('admission skipped')\n" + "print('PASS_OPTIMIZED_ADMISSION')\n" + ) + done = subprocess.run( + [sys.executable, "-O", "-I", "-B", "-c", script], + check=False, + capture_output=True, + text=True, + ) + need(done.returncode == 0, "optimized admission failed: " + done.stderr) + need("PASS_OPTIMIZED_ADMISSION" in done.stdout, "optimized marker") + + +def test_readonly_verify_unchanged(): + before = file_hashes(HERE) + proc = subprocess.run( + [sys.executable, "-I", "-B", str(HERE / "verify.py")], + cwd=str(ROOT), + capture_output=True, + text=True, + timeout=120, + ) + need(proc.returncode == 0, "verify failed: " + proc.stderr) + need("PASS_GATE_OPERAND_EXPORT_PARITY" in proc.stdout, "missing PASS marker") + after = file_hashes(HERE) + need(before == after, "verify must be read-only") + + +def main(): + test_duplicate_json_keys() + test_certificate_corruption_rejected() + test_optimized_admission() + test_readonly_verify_unchanged() + print(MARKER) + + +if __name__ == "__main__": + main() diff --git a/research/gate-operand-export-parity/verify.py b/research/gate-operand-export-parity/verify.py new file mode 100644 index 0000000000..b20910d610 --- /dev/null +++ b/research/gate-operand-export-parity/verify.py @@ -0,0 +1,405 @@ +#!/usr/bin/env python3 +"""Gate operand symbolic/export parity at the selected checker/exporter boundary. + +Answers PR #3004 open question 2 under the #2977 supplier-boundary cascade: +destination-in-sources gates make accumulate-XOR and sequential ADD disagree, +while destination-free gates always agree. The checker rejects those gates; +the exporter does not. No new kappa. + +Admission uses need() and remains active under python -O. +""" + +from __future__ import annotations + +import copy +import gzip +import hashlib +import itertools +import json +import runpy +import subprocess +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MARKER = ( + "PASS_GATE_OPERAND_EXPORT_PARITY " + "dest_free_agree=4686 dest_in_disagree_witnesses=2 " + "selected_distinct_gates=5472 checker_rejects=4 " + "no_new_kappa" +) +KAPPA_DECIMAL = "0.001672660197076918" +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +CHECKER = "research/e8-bit-p111-tuned/code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" +PRIOR_README = "research/scatter-parity-contract-audit/README.md" +PRIOR_TASK = "research/scatter-parity-contract-audit/TASK.json" +INPUTS = (WORD, CHECKER, EXPORTER) +# B[0] on the selected word: frame 127, dest 111, sources [3]. +B0_FRAME = 127 +B0_DEST = 111 +B0_SRC = 3 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + value = {} + for key, item in pairs: + need(key not in value, "duplicate JSON key") + value[key] = item + return value + + +def read_json(path): + raw = Path(path).read_bytes() + need(len(raw) <= 4_000_000, "input exceeds 4 MB") + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def pin_sources(): + manifest = read_json(HERE / "SOURCES.json") + need(manifest["base_commit"] == "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "base commit pin") + rows = manifest["files"] + inputs = [row for row in rows if row["usage"] == "input"] + need(tuple(row["path"] for row in inputs) == INPUTS, "input inventory") + pinned = {} + for row in rows: + path = ROOT / row["path"] + raw = path.read_bytes() + need(len(raw) == row["size_bytes"], "source size: " + row["path"]) + digest = hashlib.sha256(raw).hexdigest() + need(digest == row["sha256"], "source hash: " + row["path"]) + pinned[row["path"]] = raw + return pinned + + +def symbolic(d, srcs, val): + """Accumulate source XOR from the pre-gate valuation, then XOR into d.""" + out = list(val) + acc = 0 + for s in srcs: + acc ^= val[s] + out[d] ^= acc + return out + + +def export_seq(d, srcs, val): + out = list(val) + for s in srcs: + out[d] ^= out[s] + return out + + +def small_domain_census(n=6, max_len=4): + """Exhaustive agreement census on n registers and source lists length <= max_len.""" + dest_free_agree = 0 + dest_free_disagree = 0 + dest_in_agree = 0 + dest_in_disagree = 0 + disagree_witnesses = [] + for length in range(0, max_len + 1): + for srcs in itertools.product(range(n), repeat=length): + for d in range(n): + # Formal coefficients over F2. + def coeffs(op): + basis = [[1 if i == j else 0 for j in range(n)] for i in range(n)] + if op == "sym": + acc = [0] * n + for s in srcs: + acc = [a ^ b for a, b in zip(acc, basis[s])] + return tuple(a ^ b for a, b in zip(basis[d], acc)) + cur = [row[:] for row in basis] + for s in srcs: + cur[d] = [a ^ b for a, b in zip(cur[d], cur[s])] + return tuple(cur[d]) + + agree = coeffs("sym") == coeffs("exp") + if d not in srcs: + if agree: + dest_free_agree += 1 + else: + dest_free_disagree += 1 + else: + if agree: + dest_in_agree += 1 + else: + dest_in_disagree += 1 + if len(disagree_witnesses) < 8: + disagree_witnesses.append([d, list(srcs)]) + return { + "dest_free_agree": dest_free_agree, + "dest_free_disagree": dest_free_disagree, + "dest_in_agree": dest_in_agree, + "dest_in_disagree": dest_in_disagree, + "disagree_witnesses": disagree_witnesses, + } + + +def named_witnesses(): + """Concrete PROOF.md witnesses with numeric valuations.""" + # self_even: srcs=[d,d] + val = [7, 3, 5] + d = 0 + srcs = [0, 0] + need(symbolic(d, srcs, val) != export_seq(d, srcs, val), "witness self_even") + need(symbolic(d, srcs, val)[0] == 7, "self_even sym keeps value") + need(export_seq(d, srcs, val)[0] == 0, "self_even exp clears") + # dest_with_src: srcs=[a,d] + val = [7, 3, 5] + d = 0 + srcs = [1, 0] + need(symbolic(d, srcs, val) != export_seq(d, srcs, val), "witness dest_with_src") + need(symbolic(d, srcs, val)[0] == 3, "dest_with_src sym = a") + need(export_seq(d, srcs, val)[0] == 0, "dest_with_src exp clears") + # Positive control: d not in srcs, duplicate sources still agree. + val = [7, 3, 5] + d = 0 + srcs = [1, 1, 2] + need(symbolic(d, srcs, val) == export_seq(d, srcs, val), "dest_free dup agrees") + return { + "self_even": {"d": 0, "srcs": [0, 0], "val0": [7, 3, 5], + "sym": symbolic(0, [0, 0], [7, 3, 5]), + "exp": export_seq(0, [0, 0], [7, 3, 5])}, + "dest_with_src": {"d": 0, "srcs": [1, 0], "val0": [7, 3, 5], + "sym": symbolic(0, [1, 0], [7, 3, 5]), + "exp": export_seq(0, [1, 0], [7, 3, 5])}, + "dest_free_dup": {"d": 0, "srcs": [1, 1, 2], "val0": [7, 3, 5], + "sym": symbolic(0, [1, 1, 2], [7, 3, 5]), + "exp": export_seq(0, [1, 1, 2], [7, 3, 5])}, + } + + +def bind_source_lines(pinned): + checker = pinned[CHECKER].decode("utf-8") + exporter = pinned[EXPORTER].decode("utf-8") + prior = pinned[PRIOR_README].decode("utf-8") + prior_task = pinned[PRIOR_TASK].decode("utf-8") + need("len(set(regs)) == len(regs)" in checker, "cite: checker distinct operands") + need("bad operands" in checker, "cite: checker bad-operands message") + compact = exporter.replace(" ", "") + need("forsinsrcs:rec.append((1,d,s,1,f,ph))" in compact, + "cite: exporter one ADD per source occurrence") + need("forrin[d]+srcs:move(r,f)" in compact, + "cite: exporter moves each listed operand") + need("Gate operand lists" in prior, "cite: #3004 OQ2 heading") + need("no known divergent word exists" in prior, "cite: #3004 no-divergence claim") + need("Should the schema validator also cover the gate operand lists?" in prior_task, + "cite: #3004 TASK gate OQ") + # Scatter contrast remains occurrence vs membership. + need("if k in row" in exporter, "cite: scatter membership emission") + + +def load_word(pinned): + return json.loads(gzip.decompress(pinned[WORD]), object_pairs_hook=pairs_unique) + + +def selected_gate_census(word): + total = 0 + distinct = 0 + for name in ("D", "A", "B", "C"): + for gate in word[name]: + need(len(gate) == 3, "malformed gate") + _f, d, srcs = gate + regs = [d] + list(srcs) + total += 1 + if len(set(regs)) == len(regs) and srcs: + distinct += 1 + else: + need(False, "selected word has non-distinct gate operands") + need(word["B"][0] == [B0_FRAME, B0_DEST, [B0_SRC]], "B0 fixture anchor") + return {"gates": total, "distinct_operand_gates": distinct} + + +def section_sim(word, section, mode): + n = 2 * word["v"] + word["R"] + val = [1 << r for r in range(n)] + for _f, d, srcs in word[section]: + if mode == "sym": + val = symbolic(d, srcs, val) + else: + val = export_seq(d, srcs, val) + return val + + +def make_mutant(word, kind): + w = copy.deepcopy(word) + if kind == "self_even": + w["B"][0] = [B0_FRAME, B0_DEST, [B0_DEST, B0_DEST]] + elif kind == "dest_with_src": + w["B"][0] = [B0_FRAME, B0_DEST, [B0_SRC, B0_DEST]] + elif kind == "dup_src": + w["B"][0] = [B0_FRAME, B0_DEST, [B0_SRC, B0_SRC]] + elif kind == "self_once": + w["B"][0] = [B0_FRAME, B0_DEST, [B0_DEST]] + else: + need(False, "unknown mutant") + return w + + +def checker_rejects(pinned, word, kinds): + ns = runpy.run_path(str(ROOT / CHECKER)) + check = ns["check"] + Reject = ns["Reject"] + # Baseline must pass. + check(word) + rejected = [] + for kind in kinds: + mutant = make_mutant(word, kind) + try: + check(mutant) + need(False, "checker unexpectedly accepted " + kind) + except Reject as exc: + need("bad operands" in str(exc), "reject message: " + kind) + rejected.append(kind) + except Exception as exc: # noqa: BLE001 — surface unexpected failures + # Some wrappers raise ValueError via need(). + need("bad operands" in str(exc), "reject message: " + kind) + rejected.append(kind) + return rejected + + +def export_record_count(word): + with tempfile.TemporaryDirectory(prefix="gate-op-export-") as tmp: + wp = Path(tmp) / "w.json.gz" + out = Path(tmp) / "out" + wp.write_bytes(gzip.compress(json.dumps(word, separators=(",", ":")).encode(), mtime=0)) + subprocess.check_call( + ["python3", "-I", "-B", str(ROOT / EXPORTER), str(wp), str(out)], + stdout=subprocess.DEVNULL, + timeout=60, + ) + raw = (out / "249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "aligned records") + return len(raw) // 24 + + +def scatter_only_guard_accepts_self_operand(word): + """A scatter-uniqueness guard does not inspect gate lists.""" + mutant = make_mutant(word, "self_even") + rows = mutant["scatter"] + simple = all(len(row) == len(set(row)) for row in rows) + need(simple, "selected scatter rows remain simple under gate mutant") + return simple + + +def admit_certificate(certificate, write=False): + path = HERE / "CERTIFICATE.json" + if write: + path.write_text(json.dumps(certificate, indent=2, sort_keys=True) + "\n") + return + need(path.is_file(), "missing CERTIFICATE.json") + committed = read_json(path) + need(committed == certificate, "certificate mismatch") + + +def evaluate(write=False): + pinned = pin_sources() + bind_source_lines(pinned) + word = load_word(pinned) + census = small_domain_census() + need(census["dest_free_disagree"] == 0, "dest-free must always agree") + need(census["dest_free_agree"] == 4686, "dest-free agree count") + need(census["dest_in_disagree"] > 0, "dest-in must have disagreements") + witnesses = named_witnesses() + selected = selected_gate_census(word) + need(selected["gates"] == 5472, "selected gate count") + need(selected["distinct_operand_gates"] == 5472, "all selected gates distinct") + + # Section-level Sym/Exp on mutants. + base_sym = section_sim(word, "B", "sym") + base_exp = section_sim(word, "B", "exp") + need(base_sym == base_exp, "baseline B section agrees") + + self_even = make_mutant(word, "self_even") + need(section_sim(self_even, "B", "sym") != section_sim(self_even, "B", "exp"), + "self_even section diverges") + need(section_sim(self_even, "B", "sym")[B0_DEST] != section_sim(self_even, "B", "exp")[B0_DEST], + "self_even diverges at dest") + + dest_with = make_mutant(word, "dest_with_src") + need(section_sim(dest_with, "B", "sym") != section_sim(dest_with, "B", "exp"), + "dest_with_src section diverges") + + dup_src = make_mutant(word, "dup_src") + need(section_sim(dup_src, "B", "sym") == section_sim(dup_src, "B", "exp"), + "dup_src dest-free agrees") + + self_once = make_mutant(word, "self_once") + need(section_sim(self_once, "B", "sym") == section_sim(self_once, "B", "exp"), + "self_once agrees") + + rejected = checker_rejects( + pinned, word, ("self_even", "dest_with_src", "dup_src", "self_once"), + ) + need(len(rejected) == 4, "four checker rejects") + + base_records = export_record_count(word) + need(base_records == 27234, "selected export record count") + # Exporter accepts the mutant bytes and emits an extra ADD for the duplicate. + self_even_records = export_record_count(self_even) + need(self_even_records == base_records + 1, "exporter emits extra ADD on self_even") + + need(scatter_only_guard_accepts_self_operand(word), + "scatter-only guard misses gate self-operand") + + selected_result = read_json(ROOT / "certificates/selected-result.json") + need(selected_result.get("kappa") == "836330098538459/500000000000000000", + "selected kappa fraction unchanged") + + certificate = { + "schema_version": 1, + "status": "PASS_GATE_OPERAND_EXPORT_PARITY", + "kappa_decimal": KAPPA_DECIMAL, + "claim": { + "dest_free_always_agree": True, + "dest_in_can_disagree": True, + "small_domain": census, + "named_witnesses": { + "self_even": witnesses["self_even"], + "dest_with_src": witnesses["dest_with_src"], + }, + }, + "selected_word": { + "path": WORD, + "sha256": hashlib.sha256(pinned[WORD]).hexdigest(), + "gates": selected["gates"], + "distinct_operand_gates": selected["distinct_operand_gates"], + "B0": [B0_FRAME, B0_DEST, [B0_SRC]], + "export_records": base_records, + }, + "controls": { + "checker_rejects": rejected, + "self_even_export_records": self_even_records, + "scatter_only_guard_misses_gate_self_operand": True, + "dup_src_section_agrees": True, + "self_once_section_agrees": True, + }, + "no_new_kappa": True, + } + admit_certificate(certificate, write=write) + return certificate + + +def main(argv=None): + import argparse + + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write", + action="store_true", + help="regenerate CERTIFICATE.json (explicit write path only)", + ) + args = parser.parse_args(argv) + certificate = evaluate(write=args.write) + need(certificate["status"] == "PASS_GATE_OPERAND_EXPORT_PARITY", "status") + print(MARKER) + + +if __name__ == "__main__": + main()