Reject unsound binary-frame verifier inputs

certificates/joint-dual-kappa.json

@@ -833,16 +833,16 @@
   "local_source_sha256": {
     "scripts/experiments/binary_frame_compiler.py": "bc6910c8bbe8224285164323d3c06e9035ad3eaa55416abc2867ae0066454a0c",
     "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0",
-    "scripts/experiments/binary_frame_profile_prepare.py": "8a50381cab00b33e62b3a057d199ba5e19647929135c95b0fd63fc8a8ef7c9b3",
+    "scripts/experiments/binary_frame_profile_prepare.py": "16dea3d3ef3dc90db928ed3e35d002f6926d2e7388da4766fc2fd725550f739e",
     "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669",
-    "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc",
+    "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9",
     "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13",
     "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800",
     "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd",
     "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00",
     "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985"
   },
-  "source_manifest_sha256": "fd1aab7d75753b4b55b2377f26119dae74f367b0b4fab66cba42d944b3042cc9",
+  "source_manifest_sha256": "281f9f7445c68b78b8e49274e7963849c856dd06bccd82ac8471c931e5e24d65",
   "sources": [
     {
       "files": {

certificates/joint-dual-validation.json

@@ -226,7 +226,7 @@
     }
   },
   "bit_saving": "2382370177/50000000000000",
-  "certificate_sha256": "2ed658f05365b28825e24a6e7bac9fc9cc015d5a5d63d9579f4ac6e0640ae559",
+  "certificate_sha256": "84a59667edce2bf275aa813365031955e340c453afd54c22be914fc68cd55a30",
   "kappa": "4764513337/100000000000000",
   "margins": 7,
   "producer_words_regenerated_and_matched": true,

certificates/skip-frame-kappa.json

@@ -823,9 +823,9 @@
   "local_source_sha256": {
     "scripts/experiments/binary_frame_compiler.py": "bc6910c8bbe8224285164323d3c06e9035ad3eaa55416abc2867ae0066454a0c",
     "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0",
-    "scripts/experiments/binary_frame_profile_prepare.py": "8a50381cab00b33e62b3a057d199ba5e19647929135c95b0fd63fc8a8ef7c9b3",
+    "scripts/experiments/binary_frame_profile_prepare.py": "16dea3d3ef3dc90db928ed3e35d002f6926d2e7388da4766fc2fd725550f739e",
     "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669",
-    "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc",
+    "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9",
     "scripts/experiments/skip_frame_compiler.py": "8ffd079fd2e4f055b5befefecc5f33e686de9898219e9252f5d3913df8b195d8",
     "scripts/experiments/skip_frame_compose.py": "d48e688ebb9a490f4eaf50d9ab0a4d4e3e76b6588b55d213df14c703c27a7f66",
     "scripts/experiments/verify_skip_frame.py": "fc42dc3d59239ee3908d0e3e95402eb53fd6815a100521911fde1b541070c292"

certificates/skip-frame-validation.json

@@ -226,7 +226,7 @@
     }
   },
   "bit_saving": "116741511/2500000000000",
-  "certificate_sha256": "d6d2ed145539af1acfe95c0df1ceac155fa359d43590ac772cbe1938f92f0092",
+  "certificate_sha256": "9f57831c261dfb6b3bfbe94be75bfa5a3faa05768b7d500281e7398623ad115a",
   "kappa": "4669442391/100000000000000",
   "margins": 7,
   "scope": "Finite conditional witness; unchanged data geometry and general transfer proofs are inherited dependencies.",

docs/reproducibility.md

@@ -21,6 +21,22 @@ The local preparation checks used Python 3.14.6 and Tectonic 0.16.9. The supplie
 GitHub workflow targets Python 3.11, 3.13, and 3.14 on Ubuntu 24.04; a workflow
 configuration is not a claim that those hosted runs have already passed.
 
+The shared finite-word replay and transition preparation require assertions:
+run without `-O`, `-OO` or a nonzero `PYTHONOPTIMIZE`. Both entry points reject
+an optimized interpreter before loading a word or writing profiler inputs.
+They also check physical index domains and bind the complete scatter multiset
+to the output records. Extra cancelling XORs cannot substitute for paid
+incidences; valid reorderings remain accepted because scatter gates change only
+output slots using unchanged scratch sources.
+
+The cancelling-scatter counterexample was identified by **rfu08** in
+[PR #64](https://github.com/CrocSwap/integer-mult-bounds/pull/64), at inspected
+head `2d970ab3ca0271cfb2b609dc9aae1b7073b7774d`. The common checkers now enforce
+that binding; the finite-word controls run in `make verify-joint` and
+`make verify-tests`. `make verify-pair` also replays the selected pair-assembly
+words through these helpers. This strengthens checker coverage while retaining
+the numerical witnesses and the stated full-theorem assumptions.
+
 ## Arithmetic, identities, and patches
 
 ```sh

research/joint-dual/SOURCE.json

@@ -13,7 +13,7 @@
     "certificates/joint-dual-transitions-25.json": "f858c3f71d563c14013c9ae4cc10fce2b9f227da38e468a392c6890613444c8d",
     "certificates/joint-dual-word-23.json.gz": "634da1cb39634be15c6d4070132c6bdf4f5a927331cac3b4f13dc995dd799b6b",
     "certificates/joint-dual-word-25.json.gz": "dd2223d7ee0b91c4445f5acd0b7cad945f56f4e16456b6818f53ddef64a0cb16",
-    "certificates/skip-frame-kappa.json": "d6d2ed145539af1acfe95c0df1ceac155fa359d43590ac772cbe1938f92f0092",
+    "certificates/skip-frame-kappa.json": "9f57831c261dfb6b3bfbe94be75bfa5a3faa05768b7d500281e7398623ad115a",
     "references/frame-compiler/pr48/SOURCE.json": "6ccc673f88d3650d75ed600b082fe2fc2866dd88a172d182a38c1d0cd27d24b3",
     "references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py": "4d27575dcad2b45a281a34054d311409ecd954f373c0c3a62c29bcc843f06a86",
     "references/frame-compiler/pr48/research/copied-fixed/certificate.json": "33b3373c04e18a7f4cee33ba68da6ed71934acc3e0179cca6197696be4befa22",
@@ -45,15 +45,15 @@
     "research/joint-dual/README.md": "ba7d21a7f71cac74fc7c5b802c0f1f642b8130d6b484e73074f117772b8133cb",
     "scripts/experiments/binary_frame_compiler.py": "bc6910c8bbe8224285164323d3c06e9035ad3eaa55416abc2867ae0066454a0c",
     "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0",
-    "scripts/experiments/binary_frame_profile_prepare.py": "8a50381cab00b33e62b3a057d199ba5e19647929135c95b0fd63fc8a8ef7c9b3",
+    "scripts/experiments/binary_frame_profile_prepare.py": "16dea3d3ef3dc90db928ed3e35d002f6926d2e7388da4766fc2fd725550f739e",
     "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669",
-    "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc",
+    "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9",
     "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13",
     "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800",
     "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd",
     "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00",
     "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985",
-    "tests/test_joint_reclaim.py": "e2cfc99a52283c4912f970f83c7da5481ba9840d5f999f7e0e5468e8e8862a41"
+    "tests/test_joint_reclaim.py": "c4e2817bf6e699f462aa3c589ee45e24ab0dcad6bcdb6152ca2a1e16ac7bffeb"
   },
   "producer_pr55_commit": "03e991aa79f9df1a935726213bb6a8631cd0d823",
   "scope": "Explicit reviewed source and finite-input freeze; arithmetic certificates and validation receipts are derived."

research/pair-assembly/frame/frame-certificate.json

@@ -750,9 +750,9 @@
     "research/pair-assembly/frame/frame_verify.py": "fafe25d57166a747eeb847444a2e02dd7eed19038b93a2c495014d147d04a8fb",
     "scripts/experiments/binary_frame_compiler.py": "bc6910c8bbe8224285164323d3c06e9035ad3eaa55416abc2867ae0066454a0c",
     "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0",
-    "scripts/experiments/binary_frame_profile_prepare.py": "8a50381cab00b33e62b3a057d199ba5e19647929135c95b0fd63fc8a8ef7c9b3",
+    "scripts/experiments/binary_frame_profile_prepare.py": "16dea3d3ef3dc90db928ed3e35d002f6926d2e7388da4766fc2fd725550f739e",
     "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669",
-    "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc"
+    "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9"
   },
   "scope": "Pair-assembly graph compiled by PR #57's unchanged joint frame compiler. Ordered affine residual compiler, fixed-tape recursion, finite scalar overhead, balanced transfer, analytic/routing/recovery interfaces and PR #57's compiler argument remain inherited.",
   "sources": {

scripts/experiments/binary_frame_profile_prepare.py

@@ -4,10 +4,12 @@
 from itertools import combinations
 from pathlib import Path
 import json,struct,sys,gzip,argparse
+from binary_frame_replay import check_word
 
 
 def prepare(path,destination):
     raw=Path(path).read_bytes();raw=gzip.decompress(raw) if str(path).endswith('.gz') else raw;d=json.loads(raw)
+    check_word(d)
     h,v,R=d['h'],d['v'],d['R']
     frames=[(0,0,0),(0,0,h)]+[(c,u,1 if c==u else u.bit_count()-c.bit_count()) for c,u in d['frames']]
     physical=[None]*R;transitions=Counter()

scripts/experiments/binary_frame_replay.py

@@ -3,9 +3,63 @@
 from pathlib import Path
 from itertools import combinations
 from collections import Counter
+from math import comb
+
+if sys.flags.optimize:
+ raise ValueError('Assertions must remain enabled')
+
+
+def check_word(d):
+ """Bind physical indices and every scatter incidence to the output plan.
+
+ PR #64's separate audit (rfu08) identified the cancelling-scatter gap:
+ https://github.com/CrocSwap/integer-mult-bounds/pull/64
+ Scatter gates commute: each changes an output using an unchanged scratch
+ source. Compare multisets so reordering remains valid, but extra gates do not.
+ """
+ h,v,R=d['h'],d['v'],d['R']
+ assert type(h) is int and h>=3
+ assert type(v) is int and v==comb(h,3)
+ assert type(R) is int and R>=v
+ frames=d['frames'];universe=(1<<h)-1
+ for c,u in frames:
+  assert type(c) is int and type(u) is int and 0<c<=u<=universe and not c&~u
+  assert (c==u and c.bit_count()==3) or (c!=u and c.bit_count() in (1,2))
+ assert set(d['sources'])=={str(i) for i in range(v)}
+ assert all(type(s) is int and 0<=s<R for s in d['sources'].values())
+ assert len(set(d['sources'].values()))==v
+ for a,b,g in d['ops']:
+  assert type(a) is int and type(b) is int and 0<=a<R and 0<=b<R and a!=b
+  assert type(g) is int and 0<=g<len(frames)
+ triples=list(combinations(range(h),3));lookup={t:i for i,t in enumerate(triples)}
+ center_destinations=[[] for _ in range(h)]
+ for i,triple in enumerate(triples):
+  for common in triple:center_destinations[common].append(i)
+ expected=Counter();outputs=set();centers=set()
+ for s,g,common,triple in d['outputs']:
+  assert type(s) is int and 0<=s<R and s not in outputs
+  assert type(g) is int and 0<=g<len(frames)
+  assert type(common) is int and 0<=common<h
+  assert all(type(point) is int for point in triple)
+  outputs.add(s)
+  if len(triple)==1:
+   assert triple==[common] and common not in centers
+   centers.add(common)
+   destinations=center_destinations[common]
+  else:
+   assert len(triple)==3 and triple==sorted(triple) and common in triple
+   destinations=[lookup[tuple(triple)]]
+  expected.update((v+i,2*v+s) for i in destinations)
+ assert centers==set(range(h))
+ for target,source in d['scatter']:
+  assert type(target) is int and v<=target<2*v
+  assert type(source) is int and 2*v<=source<2*v+R
+ assert Counter(map(tuple,d['scatter']))==expected, 'Scatter differs from paid output incidences'
 
 def replay(path):
- d=json.loads(gzip.decompress(Path(path).read_bytes()) if str(path).endswith('.gz') else Path(path).read_bytes());h,v,R=d['h'],d['v'],d['R'];F=d['frames'];triples=list(combinations(range(h),3));assert len(triples)==v
+ d=json.loads(gzip.decompress(Path(path).read_bytes()) if str(path).endswith('.gz') else Path(path).read_bytes())
+ check_word(d)
+ h,v,R=d['h'],d['v'],d['R'];F=d['frames'];triples=list(combinations(range(h),3));assert len(triples)==v
  ranks=[1 if c==u else u.bit_count()-c.bit_count()for c,u in F]
  for c,u in F:assert c and not c&~u and(c.bit_count()in(1,2)or c==u and c.bit_count()==3)
  physical=[None]*R;symbols=[0]*R;hist=Counter();sources={int(i):s for i,s in d['sources'].items()};assert len(sources)==v and len(set(sources.values()))==v

tests/test_joint_reclaim.py

@@ -4,6 +4,7 @@
 from pathlib import Path
 import gzip
 import json
+import os
 import subprocess
 import sys
 import tempfile
@@ -30,11 +31,13 @@ def reject_mutation(self, mutate, checker='both'):
                 mutate(changed)
                 path = Path(directory)/'word.json'
                 path.write_text(json.dumps(changed, separators=(',', ':'))+'\n')
-                with self.assertRaises((AssertionError, ValueError, IndexError, KeyError)):
-                    if checker != 'transitions':
-                        replay(path)
-                    if checker != 'replay':
-                        prepare(path, Path(directory)/'transitions.bin')
+                checks = {'replay': lambda: replay(path),
+                          'transitions': lambda: prepare(path, Path(directory)/'transitions.bin')}
+                for name, check in checks.items():
+                    if checker in ('both', name):
+                        with self.subTest(checker=name):
+                            with self.assertRaises((AssertionError, ValueError, IndexError, KeyError)):
+                                check()
 
     def test_selected_words_pass_independent_replay(self):
         recorded = json.loads((ROOT/'certificates/joint-dual-compiler.json').read_text())
@@ -77,6 +80,64 @@ def mutate(word):
             word['R'] -= 1
         self.reject_mutation(mutate)
 
+    def test_self_cancelling_uncharged_scatter_is_rejected(self):
+        # PR #64 (rfu08) supplies this checker counterexample. Algebraic
+        # cancellation cannot authorize extra incidences absent from outputs.
+        def mutate(word):
+            outputs = {record[0] for record in word['outputs']}
+            slot = next(s for s in range(word['R']) if s not in outputs)
+            rogue = [word['v'], 2*word['v']+slot]
+            word['scatter'].extend([rogue, rogue])
+        self.reject_mutation(mutate)
+
+    def test_negative_operation_frame_index_is_rejected(self):
+        # Python aliases this to the original frame; the physical format uses
+        # nonnegative indices, as does the unsigned native profiler.
+        def mutate(word):
+            word['ops'][0][2] -= len(word['frames'])
+        self.reject_mutation(mutate, 'replay')
+
+    def test_cancelled_repetitions_of_paid_scatter_are_rejected(self):
+        def mutate(word):
+            word['scatter'].extend([word['scatter'][0], word['scatter'][0]])
+        self.reject_mutation(mutate)
+
+    def test_missing_scatter_is_rejected_by_each_helper(self):
+        self.reject_mutation(lambda word: word['scatter'].pop(0))
+
+    def test_scatter_order_preserves_the_complete_basis_receipt(self):
+        recorded = json.loads((ROOT/'certificates/joint-dual-compiler.json').read_text())
+        for h, original in self.words.items():
+            with self.subTest(h=h), tempfile.TemporaryDirectory() as directory:
+                changed = deepcopy(original)
+                changed['scatter'].reverse()
+                path = Path(directory)/'word.json'
+                path.write_text(json.dumps(changed)+'\n')
+                self.assertEqual(json.loads(json.dumps(replay(path))), recorded['axes'][str(h)]['replay'])
+
+    def test_optimized_helpers_reject_unchecked_word(self):
+        # This word omits every output. Optimized entry points must reject the
+        # interpreter before unchecked replay or profiler artifacts are emitted.
+        word = dict(h=3, v=1, R=1, frames=[[7,7]], sources={'0':0},
+                    ops=[], outputs=[], scatter=[], events=[[0,-1,0]])
+        with tempfile.TemporaryDirectory() as directory:
+            path = Path(directory)/'word.json'
+            path.write_text(json.dumps(word)+'\n')
+            for name in ('binary_frame_replay.py', 'binary_frame_profile_prepare.py'):
+                for flags, optimization in ((['-O'], ''), (['-OO'], ''), ([], '1')):
+                    with self.subTest(entry=name, flags=flags, env=optimization):
+                        destination = Path(directory)/'transitions.bin'
+                        args = [str(path)]
+                        if name == 'binary_frame_profile_prepare.py':
+                            args.append(str(destination))
+                        env = dict(os.environ, PYTHONOPTIMIZE=optimization)
+                        result = subprocess.run([sys.executable, *flags, str(EXPERIMENTS/name), *args],
+                                                capture_output=True, text=True, env=env)
+                        self.assertNotEqual(result.returncode, 0)
+                        self.assertIn('Assertions must remain enabled', result.stderr)
+                        self.assertNotIn('PASS', result.stdout)
+                        self.assertFalse(destination.exists())
+
     def test_complete_pr58_profile_fails_new_bit_saving(self):
         previous = json.loads((ROOT/'references/frame-compiler/pr58/certificates/joint-dual-kappa.json').read_text())
         current = json.loads((ROOT/'certificates/joint-dual-kappa.json').read_text())