Audit: exact gate-operand parity contract at the checker/exporter boundary (answers PR3696 OQ1; no new kappa)

research/gate-operand-parity-contract/README.md

@@ -0,0 +1,172 @@
+# Gate-operand parity contract: the exact agreement condition and which export guards separate divergent from agreeing gates
+
+**Boundary audit; no new κ.** The selected κ stays `0.001672660197076918`.
+This is the gate-operand completion of the checker/exporter schema cascade:
+[#2977](https://github.com/CrocSwap/integer-mult-bounds/pull/2977) named the
+scatter multiplicity gap, `research/scatter-parity-contract-audit` (with the
+#2992/#3273/#3346 successors) derived the exact scatter contract, and
+[#3696](https://github.com/CrocSwap/integer-mult-bounds/pull/3696) showed that
+destination-free gates always agree and left open question 1: does a
+simple-support guard on gate operands reject all divergent dest-in-sources
+cases without rejecting agreeing dest-free lists? This package answers it
+exactly, with a measured guard census and the selected word's blast radius.
+
+## The two operators, exactly
+
+One gate `(d, srcs)` over registers `0..n-1`, with the pinned frozen sources:
+
+- **Sym** (checker `xcheck_p.py`, `run`): `acc = XOR(val[s] for s in srcs)`
+  reading pre-gate values, then `val[d] ^= acc` once.
+- **Exp** (exporter `export_records.py`, `run`): one `ADD(d, s)` per listed
+  source, replayed sequentially over current values, so a source equal to `d`
+  re-reads the destination and annihilates whatever it accumulated.
+
+Both are linear maps over F2^n, so agreement on the register basis is
+functional agreement for every valuation. The checker additionally requires
+`srcs` nonempty with all of `[d] + srcs` distinct (`bad operands`), so every
+checker-accepted gate is destination-free.
+
+## The agreement contract
+
+Let `m` be the multiplicity of `d` in `srcs` and `k` the index of its last
+occurrence. Coefficient-wise over F2:
+
+> **Sym and Exp agree iff `d ∉ srcs`, or (`m` odd and every register `r ≠ d`
+> occurring before position `k` occurs an even number of times before `k`).**
+
+- Destination-free: both maps write `x_d ⊕ Σ_{r≠d} occ(r)·x_r`. They agree for
+  every source list, repeated or not.
+- Destination-in, `m` even: Sym keeps a `x_d` term (coefficient `1 ⊕ m = 1`);
+  Exp's last self-ADD annihilates it. Always divergent.
+- Destination-in, `m` odd: the `x_d` terms cancel in Sym; Exp keeps only
+  sources after position `k`. They agree iff the pre-`k` part cancels
+  per-register (`[d]`, `[d,a]`, `[a,a,d]`, `[d,d,d]` agree; `[a,d]`, `[a,b,a,d]`
+  diverge — an even pre-count cancels, an odd one does not).
+
+## Measured census (standard library, independent implementation)
+
+All `(d, srcs)` pairs with 6 registers and source lists of length 0..4 — the
+same bounded domain as the published gate-operand census — plus a length ≤ 5
+extension. Simulation and the coefficient-level prediction agree on **100%**
+of pairs in both domains (asserted per pair):
+
+| class | pairs |
+|---|---:|
+| domain (n=6, len ≤ 4) | 9,330 |
+| destination-free, all agreeing | 4,686 (matches the published census exactly) |
+| destination-in | 4,644 |
+| divergent | 3,492 |
+| agreeing destination-in | 1,152 |
+| extended domain (len ≤ 5) | 55,986 |
+| extended divergent | 26,172 |
+
+## Guard census at the export boundary
+
+| guard (accept iff) | accepted | divergent admitted | agreeing rejected | sound |
+|---|---:|---:|---:|---|
+| `checker_contract` (srcs nonempty, `[d]+srcs` distinct) | 1,230 | 0 | 4,608 | yes |
+| `distinct_only` (drop the nonempty clause) | 1,236 | 0 | 4,602 | yes |
+| `dest_free` (`d ∉ srcs`) | 4,686 | 0 | 1,152 | yes |
+| `srcs_simple` (scatter guard transplanted) | 3,102 | **1,350** | 4,086 | **no** |
+| `exact` (the contract above) | 5,838 | 0 | **0** | yes |
+
+Accepted sets form the strict chain `checker_contract ⊂ distinct_only ⊂
+dest_free ⊂ exact` (1,230 / 1,236 / 4,686 / 5,838). The accepted counts match
+closed forms independently: `checker_contract` accepts 6·Σ P(5,L) = 1,230
+ordered distinct nonempty lists per destination, and the transplanted guard's
+1,350 divergent admissions are exactly the simple destination-in lists with
+`d` not first.
+
+## The answer to the open question
+
+**Not as literally stated, for the simple-support guard.** Distinct-operand
+guards do reject every divergent destination-in gate (all 3,492), but they
+also reject agreeing destination-free lists — 4,608 of them on this domain,
+the smallest being the empty source list and the smallest nonempty one being
+`[a,a]`. Every one of those rejected agreeing lists is already rejected by the
+checker (`bad operands`), so **no checker-accepted word is affected**; the
+boundaries align exactly when the exporter adopts the checker's own operand
+contract. The only guard that is simultaneously sound and free of agreeing
+rejections is the exact minimal guard above. A scatter-style simple-support
+guard on `srcs` alone is **unsound**: it admits 1,350 divergent gates
+(destination among the sources but not first, e.g. `[a,d]`), so the scatter
+schema does not transfer to gates unchanged.
+
+**Blast radius on the selected word.** The pinned tuned word
+(`SHA-256 e3e301e6…`, `v=111`, `R=439`) has **5,472** D/A/B/C gates, every one
+with distinct nonempty operands, and 111 simple scatter rows over nine
+retained totals with 527 terms. Under any of the three sound guards every
+selected gate is accepted and its Sym/Exp agreement is the destination-free
+lemma, so the selected word's exported records are unchanged. This is a
+census of the pinned word's gate lists, not a record-stream replay; the
+27,234-record baseline and the 27,235-record `self_even` mutant emission are
+the published package's measurements and are cited, not re-derived here.
+
+## Reproduce
+
+The registered hook requires Python 3.12; the verifier itself is standard
+library and runs on 3.10+. From the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gate-operand-parity-contract
+python3.12 -I -O -Werror -B research/gate-operand-parity-contract/verify.py
+```
+
+Expected:
+
+```text
+PASS_GATE_OPERAND_PARITY_CONTRACT domain=9330 dest_free_agree=4686 dest_in=4644 divergent=3492 agreeing_dest_in=1152 checker_sound=true checker_over_rejects=4608 transplant_admits=1350 exact_over_rejects=0 selected_gates=5472 selected_distinct=5472 no_new_kappa
+```
+
+Admission uses an explicit `need()` that stays enforced under `-O`. The
+verifier is read-only: it writes nothing. Runtime is a few seconds. The three
+live inputs (tuned word, checker, exporter) are hash-bound in
+[SOURCES.json](SOURCES.json) and their decisive source lines are asserted as
+exact substrings; both operators' semantics are re-implemented here, not
+imported. The published cross-check constant 4,686 comes from the
+gate-operand-export-parity package's census on the same domain and is checked,
+not imported.
+
+## Open next questions
+
+1. **Which sound guard should a successor gate schema adopt?** The checker's
+   own contract is the minimal change (exact boundary alignment, no
+   checker-accepted word affected); `dest_free` additionally admits agreeing
+   duplicate-source gates the checker still rejects; `exact` additionally
+   admits agreeing destination-in gates. Weakening the export guard without
+   loosening the checker contract re-opens the two boundaries. First step:
+   compose the chosen guard with `simple-scatter-v1` / `integer-xor-scatter-v1`
+   in a successor checker/exporter pair. Blocked by the schema-adoption review
+   of the #2977 cascade, not by arithmetic.
+2. **Does the native formal-column checker independently reject a divergent
+   self-operand export?** First step: feed the `[d,d]` mutant's export to the
+   native column checker. Blocked by a C++17 toolchain; the synthetic word is
+   outside the selected producer either way.
+3. **Does the contract survive reordered emission?** The divergence class
+   depends on source order through the last self-occurrence. If a successor
+   exporter reorders or buffers sources, re-derive the condition; the census
+   harness here re-runs with any per-source emission order.
+
+## Scope, credit and verification limits
+
+Base main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6.
+Card `supplier-boundary-audit` with `scope_status: changed` — the scatter-side
+obligation is settled on main by `scatter-parity-contract-audit` and the
+#2992/#3273/#3346 successors, and this package takes PR3696's stated open
+question 1; the scope change and its justification are recorded in
+[TASK.json](TASK.json). Overlap was checked with `scripts/find_overlap.py`
+against open PRs and discussions and by reading the cascade's packages.
+
+Credit **Nick Petalas** for naming the scatter multiplicity gap (#2977);
+Kumagi for the exact scatter agreement contract (#3004); Wentao Li
+(VictorLiwentao) for the gate-operand census, witnesses and open question this
+package completes; Dylan Crow for the exporter; eumemic for the symbolic
+checker; and the retained tuned-word lineage. Predecessor notices and source
+licenses are unchanged.
+
+This contribution was produced by Nick Petalas with AI assistance. Separate
+internal source inspection and review do not constitute independent human or
+proof-assistant review. No new kappa, no supplier admission, no production
+schema adoption, no selected-frontier change, and no claim about any bound for
+multiplication is made here. Full selected cold replay, all-size transfer and
+hosted CI are not claimed.

research/gate-operand-parity-contract/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/code/xcheck_p.py",
+      "usage": "input",
+      "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009",
+      "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e"
+    },
+    {
+      "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py",
+      "usage": "input",
+      "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350",
+      "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3"
+    }
+  ]
+}

research/gate-operand-parity-contract/TASK.json

@@ -0,0 +1,78 @@
+{
+  "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": "changed",
+  "actual_scope": "For the frozen symbolic checker and record exporter, exactly which gate operand lists (d, srcs) make the checker's accumulate-then-write operator and the exporter's sequential per-source ADD agree, which export-time guards separate divergent from agreeing lists, and what the selected tuned word's 5,472-gate blast radius is under each sound guard.",
+  "scope_change_reason": "The card's scatter-side first experiment is settled on main: research/scatter-parity-contract-audit (with PR2992/#3273/#3346 successors) derived the exact scatter agreement contract (all positive multiplicities odd) and measured the simple-support guard as sound but strictly stronger, and PR3696 answered PR3004's gate-operand question by showing destination-free gates always agree and naming divergent destination-in witnesses. The remaining stated open question in this cascade is PR3696's own open question 1: whether a simple-support (or other) guard on gate operands rejects all divergent dest-in-sources cases without rejecting agreeing dest-free lists. This package takes exactly that question and derives the gate-operand analog of the scatter contract decision.",
+  "bottleneck_link": "The checker/exporter operand contract is a selected source-bound acceptance condition: symbolic acceptance must imply agreement of the exported record operator for every accepted word. Settling the gate-operand schema keeps the accepted-word and exported-record semantics aligned without touching any supplier cost or the selected result.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the source-line and hash bindings, the exhaustive domain classification with the independent algebraic cross-check, the guard comparison, the selected-word gate census and the scatter-row control. Do not run the native backend, do not adopt any production schema, do not rebuild the selected chain and do not search for more counterexample classes.",
+  "outcome": "completed",
+  "evidence": "On all 9330 (d, srcs) pairs with 6 registers and source lists of length 0..4, and on the 55986-pair length<=5 extension, the direct basis simulation and an independent coefficient-level prediction agree on 100% of pairs. The measured contract: destination-free gates always agree (4686, matching the published PR3696 census); destination-in gates agree iff the destination multiplicity is odd and every register occurring before the destination's last occurrence occurs an even number of times there (3492 divergent, 1152 agreeing on the main domain). Guard census: the checker's own contract (nonempty, all of [d]+srcs distinct) is sound and rejects 4608 agreeing gates, the smallest being the empty source list and the smallest nonempty destination-free one being [a,a]; distinct-only is sound with 4602 over-rejections; dest-free-only is sound with 1152 over-rejections (exactly the agreeing destination-in residue); the transplanted scatter simple-support guard is UNSOUND, admitting 1350 divergent gates (destination in sources but not first, e.g. [a,d]); the exact minimal guard is sound with zero over-rejections. The pinned selected tuned word (SHA-256 e3e301e6...) has 5472 D/A/B/C gates, every one with distinct nonempty operands, and 111 simple scatter rows over nine retained totals with 527 terms, so every sound guard preserves each selected gate's export. Both operators' decisive source lines are hash-bound: checker operand contract and accumulate-then-write lines; exporter per-source ADD emission.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which of the three sound guards should a successor gate schema adopt: the checker's own contract, dest-free-only, or the exact minimal divergence guard?",
+      "why_it_matters": "The checker's contract is the minimal change (boundaries align exactly; no checker-accepted word is affected), dest-free-only additionally accepts agreeing duplicate-source gates the checker still rejects, and the exact guard additionally accepts agreeing destination-in gates. Adopting a guard weaker than the checker's requires loosening the checker contract in the same change, or the two boundaries diverge again.",
+      "first_step": "Compose the chosen gate guard with the existing opt-in scatter boundaries (simple-scatter-v1 / integer-xor-scatter-v1) in a successor checker/exporter pair, and record which of the 9330 domain points each boundary accepts.",
+      "blocked_by": "The schema decision and adoption review of the PR2977/#2992/#3004 cascade, not any missing arithmetic."
+    },
+    {
+      "question": "Does the native formal-column checker independently reject a divergent self-operand gate export?",
+      "why_it_matters": "It decides whether the export-time guard is the only barrier for divergent destination-in gates or whether a later native check also rejects them, mirroring the scatter case where the native checker rejected the exported mutant.",
+      "first_step": "Feed the [d,d]-mutant export into the native column checker with a C++17 toolchain, as the scatter-export-parity-audit native.py path does.",
+      "blocked_by": "A C++17 toolchain and the synthetic word being outside the selected producer; this audit does not run the native backend."
+    },
+    {
+      "question": "Is the exact agreement condition invariant when a gate's sources are read in a different emission order (e.g. sorted or reversed srcs)?",
+      "why_it_matters": "The divergence class depends on list order through the last self-occurrence; a successor schema that reorders sources for record efficiency would move the boundary, and the condition above would need re-derivation for that lowering.",
+      "first_step": "Re-run the census comparing Sym against a reversed-order Exp lowering and record the new agreement condition.",
+      "blocked_by": "No current exporter reorders sources; this is a successor-schema design question only."
+    }
+  ]
+}

research/gate-operand-parity-contract/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "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}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Linearity controls for both gate operators; exhaustive n=6 length<=4 and length<=5 agreement censuses against an independent coefficient-level prediction; guard soundness/over-rejection comparison including the unsound transplanted scatter guard; selected-word gate inventory, scatter-row and hash bindings; decisive source-line bindings of both pinned operators."
+    }
+  ]
+}