diff --git a/research/simple-scatter-boundary/README.md b/research/simple-scatter-boundary/README.md new file mode 100644 index 0000000000..6f421d80e8 --- /dev/null +++ b/research/simple-scatter-boundary/README.md @@ -0,0 +1,119 @@ +# Simple-support scatter enforcement at both entry points + +This opt-in successor rejects PR2977's paired-duplicate scatter before either +symbolic checking or record export. The unchanged selected word still produces +all three original artifacts byte for byte: 27,234 records, states and frames. +All 661 arbitrary-input F2 columns agree with the intended endpoint. + +Nick Petalas's [PR2977 audit](../scatter-export-parity-audit/README.md) found the +counterexample and provided a candidate validation function. This package +answers its schema/enforcement handoff: one shared validator is now called by +two usable entry modes, which execute authenticated original scripts on private +input snapshots. The counterexample, source scripts and selected construction +are retained unchanged. No new kappa or supplier admission is claimed. + +## The explicit contract + +`simple-scatter-v1` adds a simple-support contract to the pinned `bitE8/1` word: + +- `v` is a positive exact integer, excluding Boolean values. +- `ret` is a list; `scatter` is a list of exactly `v` rows. +- Each row is a list of distinct exact integers `k` with `0 <= k < len(ret)`. +- Empty rows and arbitrary row order are allowed. Duplicate indices, including + odd multiplicities, are rejected; no coefficient normalization occurs. + +The contract does not validate every other word field or require nine totals +in isolation. Retained-role legality, frames, dirty-state endpoints and H1-H5 +remain obligations of the inherited checkers. + +For abstract copied values `c_k`, symbolic scatter adds +`XOR(c_k for k in row)`, while export adds +`XOR(c_k for k in range(len(ret)) if k in row)`. Under simple support, +each coefficient is exactly the same 0 or 1. Since these operations only add +to the target roles, their order does not affect this F2 equality. This is a +sufficient schema; repeated odd multiplicities can also agree, as PR2977 +already explains. The wrapper deliberately chooses the stricter contract. + +The wrapper parses and validates the input before any delegate or output +directory is created, hashes the delegate's bytes against [SOURCES.json](SOURCES.json), +and copies both the word and delegate into a private temporary directory. +Changing the original input path after validation cannot change what executes. +The child runs without inherited Python optimization flags; its original +success/failure code is returned. The snapshots are removed on completion. + +## Use and reproduce + +From the repository root: + +```sh +python3 -I -B research/simple-scatter-boundary/boundary.py check \ + research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz +python3 -I -B research/simple-scatter-boundary/boundary.py export \ + research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz /tmp/simple-scatter-records + +python3.12 -B scripts/research_package.py --package research/simple-scatter-boundary +python3 -I -O -Werror -B research/simple-scatter-boundary/verify.py +python3 -I -O -Werror -B research/simple-scatter-boundary/test_boundary.py +``` + +`check` adds schema enforcement to the complete pinned symbolic checker. +`export` adds schema enforcement to the pinned exporter; it does **not** run the +symbolic checker or establish the semantic correctness of an arbitrary word. +Use the full symbolic/export/native sequence when evaluating a supplier. + +The registered replay is standard-library-only and takes about ten seconds +locally. Its exact [receipt](RESULT.json) binds all three baseline artifacts to +their original bytes, reproduces the predecessor's paired-null symbolic +acceptance and incorrect exported endpoint, and rejects the pair through both +new entry modes before output creation. A separate F2 interpreter checks all +661 dirty-input basis columns, COPY/ERASE closure and the dirty-register-472 +witness. It is a scalar projection, not an independent frame or native proof. + +All 364 ordered rows of length at most five over three indices are enumerated: +16 simple supports pass, 348 repeated rows reject. Each accepted row is checked +on all eight assignments of copied bits. Nine behavioral test groups also +exercise malformed rows and types through both real CLIs, odd duplicates, +existing-output preservation, row permutation, input-path replacement, +delegate source corruption, semantic-checker failure propagation, and omitted +ADD/truncated-record controls. A disabled duplicate validator fails the same +enumeration. Explicit checks remain active under `-O`. + +## Scope and remaining obligations + +Base canonical main `836b19bfa309ceafbc8ee32a15e8c4b10dde7e11`, priority +revision 6. [TASK.json](TASK.json) records the accepted draw and the changed +scope from `bit-helper-contract` to this explicit bit-interface handoff. +This is a local boundary module, with no helper search or family expansion. +The original-card first experiment was replaced by PR2977's known-working +audit, which reproduced before implementation. + +The selected input/record checks and source pins are local evidence. Native +compilation, complete selected cold replay, hosting/precision, all-size transfer +and hosted CI are not claimed. Selected sources, their manifests and the +frontier are unchanged. An invalid word can still pass schema-only export; +the tests explicitly retain that distinction. Only schema rejection and source +pin failure are promised to leave output untouched; delegate failures retain +the original exporter's behavior. + +## Open next questions + +Should a reviewed successor supplier adopt this simple-support contract? +It would close the identified source-to-record ambiguity at both boundaries. +First review the schema, entry points and controls, then repin a successor +manifest and run the full symbolic/export/native chain. Maintainer adoption +and the inherited supplier obligations are the blockers; frozen packages +should not be repinned merely to install this opt-in module. + +## Credit + +Arham Tahir, with substantial OpenAI Codex assistance in investigation, +implementation, verification and writing. Apache-2.0. No independent human or +proof-assistant review is claimed. + +Nick Petalas/PR2977 retains discovery, dirty-witness, prior guard and handoff +credit. The new delta is enforcing a named schema in both operational entry +points, snapshotting validated inputs, and testing that integration. Credit +eumemic for the punctured generator/checker and PR543/PR555 lineage, +DreamingOfClouds for PR589 and retained bit-supplier construction, Dylan Crow +for the exporter/native lineage, and Douglas Colkitt for selected bindings and +research guidance. Original scripts are invoked unchanged with their notices. diff --git a/research/simple-scatter-boundary/RESULT.json b/research/simple-scatter-boundary/RESULT.json new file mode 100644 index 0000000000..91e89dcebf --- /dev/null +++ b/research/simple-scatter-boundary/RESULT.json @@ -0,0 +1,20 @@ +{ + "artifacts_sha256": { + "249-records.bin": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a", + "249-states.json": "701ca802279b23ba23ffd502935ae9f34a33fc81fdfd266042f3208a2cb16265", + "frames.json": "d006b3bfe0c04afecfea7aecfa59dfe4298b99501c70da3938e40289bc2f5010" + }, + "columns": 661, + "enumeration": { + "accepted": 16, + "rejected": 348, + "rows": 364 + }, + "paired_mutant_rejected_modes": [ + "check", + "export" + ], + "predecessor_paired_symbolic_accepts": true, + "records": 27234, + "schema": "simple-scatter-v1" +} diff --git a/research/simple-scatter-boundary/SOURCES.json b/research/simple-scatter-boundary/SOURCES.json new file mode 100644 index 0000000000..b10fb0e15a --- /dev/null +++ b/research/simple-scatter-boundary/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "4450dbbd1d01929022259f523234590f4cce65b9", + "sha256": "ca056a6def333df7afd822c1f34adc2eaa9089b241fc2bdd5803b64066fc9355" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/scatter-export-parity-audit/RESULT.json", + "usage": "input", + "git_blob": "fa50f464d0b47dd564a95f4c611fd8f701b2ac72", + "sha256": "b86e1d99b607fbffacfb4bcd1885c3a5e925bf292a2675a3d7ba2fca88e7e985" + } + ] +} diff --git a/research/simple-scatter-boundary/TASK.json b/research/simple-scatter-boundary/TASK.json new file mode 100644 index 0000000000..0a7e99e4de --- /dev/null +++ b/research/simple-scatter-boundary/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 6, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Enforce a versioned simple-support scatter schema at opt-in checker and exporter entry points, with exact selected-word artifact identity and paired-duplicate rejection before output.", + "scope_change_reason": "Revision 6 prefers concrete central handoffs. PR2977 establishes the duplicate-scatter cross-stage mismatch and requests successor schema enforcement; this is a bounded bit-interface reliability result rather than a new helper-mixing construction.", + "bottleneck_link": "The bit supplier requires a sound source-to-record boundary. Shared simple-support validation makes occurrence XOR and membership lowering agree, without asserting that either replaces native columns or H1-H5.", + "budget_minutes": 60, + "stop_rule": "One shared schema validator, two thin entry modes, exact selected baseline and paired-mutant controls, bounded schema enumeration, focused replay and review. No supplier search or adoption.", + "outcome": "completed", + "evidence": "RESULT.json; verify.py checks exact artifacts, all columns, the predecessor counterexample and 364 support rows; test_boundary.py provides nine behavioral groups.", + "author": "Arham Tahir", + "ai_assistance": "Substantial OpenAI Codex assistance in source investigation, implementation, verification and writing; no independent human review.", + "open_questions": [ + { + "question": "Should a reviewed successor supplier adopt simple-scatter-v1 at its source and export boundaries?", + "why_it_matters": "Opt-in enforcement is not source-bound admission into the selected replay.", + "first_step": "Review the schema and wrapper, repin a successor supplier manifest, then run its complete symbolic/export/native chain.", + "blocked_by": "Maintainer source-binding and admission review; selected frozen sources remain unchanged." + } + ], + "draw_seed": "a8623f4b135f646e52feb50249e2f2db", + "declared_milestone": "local boundary module", + "method": "Snapshot validated words before invoking unchanged authenticated checker/exporter scripts; compare every generated artifact and test real CLI rejection and exact F2 endpoints.", + "unresolved_obligations": "No new source manifests for supplier adoption, native-frame/hosting/precision replay, all-size theorem or kappa change.", + "family_expansion_decision": "Narrow to PR2977 successor schema handoff; no construction expansion.", + "predecessors": [ + { + "pr": 2977, + "head": "cd23d242dfe0e7a71cafba0ad5590dc4f2fbf4f2", + "author": "Nick Petalas", + "delta": "Publishes schema enforcement in two usable opt-in entry modes rather than only a standalone candidate guard." + } + ], + "overlap": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T16:34:05.297362+00:00", + "complete_pagination": true, + "records": 234 + }, + "discussions": { + "fetched_at": "2026-10-16T16:34:42.120317+00:00", + "complete_pagination": true, + "records": 1703 + }, + "closed_prs": { + "fetched_at": "2026-10-16T16:35:04.411993+00:00", + "complete_pagination": true, + "records": 2440 + } + }, + "warnings": [], + "limitations": "Remote title/body/comment coverage; sparse local notes; no exhaustive diffs or unpublished work.", + "result": "Final refreshed search found PR2977 and this scoped claim, with no competing successor schema enforcement identified." + }, + "freshness": { + "upstream_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "priority_revision": 6, + "checked_at_utc": "2026-10-16T16:35:13.461054+00:00" + }, + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2976#discussioncomment-18977810", + "scope_key": "simple-scatter-v1:authenticated-check-and-export-snapshots", + "validation": { + "registered_replay": "Passed on CPython 3.12.14; two commands, primary replay plus nine behavioral groups.", + "optimized_replay": "Primary replay and all nine behavioral groups passed on CPython 3.14.7 under -O -Werror.", + "selected_byte_identity": "All three exporter artifacts and 27,234 records identical; all 661 F2 columns checked.", + "not_run": "Native compilation, complete selected cold replay, all-size/hosting/precision admission and hosted CI." + } +} diff --git a/research/simple-scatter-boundary/VERIFY.json b/research/simple-scatter-boundary/VERIFY.json new file mode 100644 index 0000000000..5972253044 --- /dev/null +++ b/research/simple-scatter-boundary/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/scatter-export-parity-audit/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact selected artifact identity, all 661 dirty columns, predecessor paired counterexample, both CLI guard boundaries and all 364 ordered support rows." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_boundary.py" + ], + "timeout_seconds": 120, + "checks": "Nine behavioral groups: malformed inputs, output preservation, reordered supports, immutable snapshots, source corruption, semantic failure propagation and record mutations." + } + ] +} diff --git a/research/simple-scatter-boundary/boundary.py b/research/simple-scatter-boundary/boundary.py new file mode 100644 index 0000000000..8f205a335a --- /dev/null +++ b/research/simple-scatter-boundary/boundary.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +"""Opt-in simple-scatter-v1 entry points. Arham Tahir; Apache-2.0. + +Substantial OpenAI Codex assistance. The original checker/exporter and their +notices remain unchanged. Export mode adds schema validation, not a symbolic +or native endpoint check. +""" + +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SCHEMA = "simple-scatter-v1" +SCRIPTS = { + "check": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "export": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", +} + + +def validate_scatter(word): + """Rows are simple supports; multiplicities are rejected, never normalized.""" + if type(word) is not dict: + raise ValueError("word must be an object") + v, retained, rows = word.get("v"), word.get("ret"), word.get("scatter") + if type(v) is not int or v <= 0: + raise ValueError("v must be a positive integer") + if type(retained) is not list: + raise ValueError("ret must be a list") + if type(rows) is not list or len(rows) != v: + raise ValueError("scatter must have exactly v rows") + for t, row in enumerate(rows): + if type(row) is not list: + raise ValueError(f"scatter row {t} must be a list") + seen = set() + for k in row: + if type(k) is not int or not 0 <= k < len(retained): + raise ValueError(f"scatter row {t}: index must be an integer in range") + if k in seen: + raise ValueError(f"scatter row {t}: duplicate index {k}") + seen.add(k) + + +def script_bytes(root, mode): + path = SCRIPTS[mode] + pins = json.loads((PACKAGE / "SOURCES.json").read_bytes())["files"] + pin = next(row for row in pins if row["path"] == path and row["usage"] == "input") + body = (root / path).read_bytes() + if hashlib.sha256(body).hexdigest() != pin["sha256"]: + raise ValueError("source pin mismatch: " + path) + return body + + +def execute(mode, input_path, output=None, root=ROOT): + """Validate once, then delegate using private snapshots of word and script.""" + if mode not in SCRIPTS or (mode == "export") != (output is not None): + raise ValueError("export requires an output directory; check takes none") + raw = input_path.read_bytes() + word = json.loads(gzip.decompress(raw) if input_path.suffix == ".gz" else raw) + validate_scatter(word) + body = script_bytes(root, mode) + with tempfile.TemporaryDirectory(prefix="simple-scatter-") as temporary: + directory = Path(temporary) + script, snapshot = directory / "delegate.py", directory / "word.json.gz" + script.write_bytes(body) + snapshot.write_bytes(gzip.compress(json.dumps(word).encode(), mtime=0)) + command = [sys.executable, "-I", "-B", str(script), str(snapshot)] + if output is not None: + command.append(str(output)) + return subprocess.run(command, check=False, timeout=60).returncode + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("mode", choices=SCRIPTS) + parser.add_argument("word", type=Path) + parser.add_argument("output", type=Path, nargs="?") + args = parser.parse_args() + try: + return execute(args.mode, args.word, args.output) + except (ValueError, OSError, subprocess.TimeoutExpired) as error: + print(f"REJECT {SCHEMA}: {error}", file=sys.stderr) + return 2 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/simple-scatter-boundary/test_boundary.py b/research/simple-scatter-boundary/test_boundary.py new file mode 100644 index 0000000000..73f66cf36b --- /dev/null +++ b/research/simple-scatter-boundary/test_boundary.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Behavioral boundary controls. Arham Tahir with OpenAI Codex; Apache-2.0.""" + +import copy +import gzip +import json +from pathlib import Path +import runpy +import struct +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +boundary = runpy.run_path(str(PACKAGE / "boundary.py")) +verify = runpy.run_path(str(PACKAGE / "verify.py")) + + +class BoundaryTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = verify["inputs"]() + cls.word = json.loads(gzip.decompress(cls.data[verify["WORD"]])) + + def test_schema_and_coefficient_enumeration(self): + self.assertEqual(verify["support_enumeration"](boundary["validate_scatter"]), + {"rows": 364, "accepted": 16, "rejected": 348}) + with self.assertRaisesRegex(ValueError, "multiplicity accepted"): + verify["support_enumeration"](lambda word: None) + for retained, rows in (([], [[]]), ([4], [[0]]), ([4, 5], [[1, 0]])): + boundary["validate_scatter"]({"v": 1, "ret": retained, "scatter": rows}) + + def test_malformed_schema_both_real_entry_modes(self): + cases = [] + for row in ([0, 0], [0, 0, 0], [True], [0.0], ["0"], [-1], [9], "0", None): + word = copy.deepcopy(self.word) + word["scatter"][0] = row + cases.append(word) + for key, value in (("scatter", []), ("scatter", {}), ("ret", {}), ("v", True), ("v", 0)): + cases.append({**self.word, key: value}) + cases.extend(([], {}, None)) + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json" + output = directory / "output" + for word in cases: + fixture.write_text(json.dumps(word)) + for mode in ("check", "export"): + with self.subTest(word=str(word)[:50], mode=mode): + result = verify["cli"](mode, fixture, output if mode == "export" else None) + self.assertEqual(result.returncode, 2, result.stdout + result.stderr) + self.assertIn("REJECT simple-scatter-v1", result.stderr) + self.assertFalse(output.exists()) + + def test_rejection_preserves_existing_outputs(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + output = directory / "output" + output.mkdir() + sentinel = output / "249-records.bin" + sentinel.write_bytes(b"existing evidence") + paired = copy.deepcopy(self.word) + paired["scatter"][0].extend([0, 0]) + fixture = directory / "word.json" + fixture.write_text(json.dumps(paired)) + result = verify["cli"]("export", fixture, output) + self.assertEqual(result.returncode, 2) + self.assertEqual({p.name: p.read_bytes() for p in output.iterdir()}, + {"249-records.bin": b"existing evidence"}) + + def test_permuted_simple_rows_keep_all_artifacts(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json" + fixture.write_text(json.dumps(self.word)) + original = verify["cli"]("export", fixture, directory / "original") + self.assertEqual(original.returncode, 0, original.stderr) + permuted = {**self.word, "scatter": [row[::-1] for row in self.word["scatter"]]} + fixture.write_text(json.dumps(permuted)) + before = fixture.read_bytes() + self.assertEqual(verify["cli"]("check", fixture).returncode, 0) + self.assertEqual(verify["cli"]("export", fixture, directory / "permuted").returncode, 0) + self.assertEqual(before, fixture.read_bytes()) + for name in verify["ARTIFACTS"]: + self.assertEqual((directory / "original" / name).read_bytes(), + (directory / "permuted" / name).read_bytes()) + + def test_original_input_replacement_cannot_bypass_validation(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json" + paired = copy.deepcopy(self.word) + paired["scatter"][0].extend([0, 0]) + real_run = subprocess.run + snapshots = [] + + def replace_original(command, **kwargs): + fixture.write_text(json.dumps(paired)) + snapshots.append(Path(command[-1] if "check" == current_mode else command[-2])) + self.assertEqual(json.loads(gzip.decompress(snapshots[-1].read_bytes())), self.word) + return real_run(command, **kwargs, capture_output=True, text=True) + + for current_mode in ("check", "export"): + fixture.write_text(json.dumps(self.word)) + with patch.object(subprocess, "run", side_effect=replace_original): + status = boundary["execute"](current_mode, fixture, + directory / "output" if current_mode == "export" else None) + self.assertEqual(status, 0) + self.assertTrue(all(not path.exists() for path in snapshots)) + actual, expected = verify["columns"]((directory / "output/249-records.bin").read_bytes(), self.word) + self.assertEqual(actual, expected) + + def test_source_mismatch_before_delegation(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + fixture = root / "word.json" + fixture.write_text(json.dumps(self.word)) + for mode, name in boundary["SCRIPTS"].items(): + source = root / name + source.parent.mkdir(parents=True, exist_ok=True) + source.write_bytes(self.data[name] + b"\n") + with self.subTest(mode=mode), patch.object(subprocess, "run") as child: + with self.assertRaisesRegex(ValueError, "source pin mismatch"): + boundary["execute"](mode, fixture, root / "out" if mode == "export" else None, root) + child.assert_not_called() + self.assertFalse((root / "out").exists()) + + def test_schema_does_not_replace_semantic_checker(self): + single = copy.deepcopy(self.word) + single["scatter"][0].append(0) + boundary["validate_scatter"](single) + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json" + fixture.write_text(json.dumps(single)) + result = verify["cli"]("check", fixture) + self.assertEqual(result.returncode, 1, result.stderr) + self.assertIn("targets not y + x", result.stdout) + result = verify["cli"]("export", fixture, directory / "output") + self.assertEqual(result.returncode, 0, result.stderr) + actual, expected = verify["columns"]((directory / "output/249-records.bin").read_bytes(), single) + self.assertNotEqual(actual, expected) + + def test_bad_input_and_argument_errors(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json.gz" + for body in (b"broken", gzip.compress(b"{")): + fixture.write_bytes(body) + result = verify["cli"]("export", fixture, directory / "output") + self.assertEqual(result.returncode, 2, result.stderr) + self.assertFalse((directory / "output").exists()) + fixture.write_bytes(self.data[verify["WORD"]]) + for mode, output in (("export", None), ("check", directory / "output")): + self.assertEqual(verify["cli"](mode, fixture, output).returncode, 2) + + def test_export_mutation_controls(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + fixture = directory / "word.json" + fixture.write_text(json.dumps(self.word)) + self.assertEqual(verify["cli"]("export", fixture, directory / "output").returncode, 0) + raw = (directory / "output/249-records.bin").read_bytes() + with self.assertRaisesRegex(ValueError, "aligned records"): + verify["columns"](raw[:-1], self.word) + records = list(struct.iter_unpack("<6i", raw)) + cut = next(i for i, record in enumerate(records) if record[0] == 1 and record[1] == 111) + mutated = b"".join(struct.pack("<6i", *record) for i, record in enumerate(records) if i != cut) + actual, expected = verify["columns"](mutated, self.word) + self.assertNotEqual(actual, expected) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/simple-scatter-boundary/verify.py b/research/simple-scatter-boundary/verify.py new file mode 100644 index 0000000000..551af0180d --- /dev/null +++ b/research/simple-scatter-boundary/verify.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Exact boundary replay. Arham Tahir with OpenAI Codex; Apache-2.0.""" + +import argparse +import copy +import gzip +import hashlib +import itertools +import json +from pathlib import Path +import runpy +import struct +import subprocess +import sys +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +SELECTED = "research/community-frontier1094-audit/SELECTED-SOURCE.json" +PREDECESSOR = "research/scatter-export-parity-audit/RESULT.json" +ARTIFACTS = ("249-records.bin", "249-states.json", "frames.json") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def inputs(): + pins = json.loads((PACKAGE / "SOURCES.json").read_bytes())["files"] + result = {} + for row in pins: + if row["usage"] == "input": + body = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(body).hexdigest() == row["sha256"], row["path"]) + result[row["path"]] = body + selected = json.loads(result[SELECTED])["files"] + scripts = runpy.run_path(str(PACKAGE / "boundary.py"))["SCRIPTS"] + for path in (WORD, *scripts.values()): + require(hashlib.sha256(result[path]).hexdigest() == selected[path], "selected binding") + return result + + +def run(command): + return subprocess.run(command, capture_output=True, text=True, timeout=60, check=False) + + +def cli(mode, word, output=None): + command = [sys.executable, "-I", "-B", str(PACKAGE / "boundary.py"), mode, str(word)] + return run(command + ([] if output is None else [str(output)])) + + +def columns(raw, word): + """Separate F2 interpreter, retaining arbitrary dirty input coordinates.""" + n = 2 * word["v"] + word["R"] + require(len(raw) % 24 == 0, "aligned records") + values, owner = [1 << i for i in range(n)] + [0], None + for op, a, b, coefficient, _frame, _phase in struct.iter_unpack("<6i", raw): + if op == 0: + continue + require(0 <= a <= n and 0 <= b <= n, "record registers") + if op == 1: + require(a < n and (b < n or owner is not None), "ADD temporary") + if coefficient % 2: + values[a] ^= values[b] + elif op == 2: + require(owner is None and a < n and b == n and values[n] == 0, "fresh COPY") + values[n], owner = values[a], a + elif op == 3: + require(owner == a and b == n and values[n] == values[a], "bound ERASE") + values[n], owner = 0, None + else: + raise ValueError("record opcode") + require(owner is None and values[n] == 0, "closed temporary") + expected = [1 << i for i in range(n)] + for t in range(word["v"]): + expected[word["v"] + t] ^= 1 << t + return values[:-1], expected + + +def support_enumeration(validate): + """Every ordered row of length <=5 on three indices: 364 cases.""" + accepted, rejected = 0, 0 + for length in range(6): + for row in itertools.product(range(3), repeat=length): + word = {"v": 1, "ret": [10, 11, 12], "scatter": [list(row)]} + counts = [sum(k == j for k in row) for j in range(3)] + simple = all(m <= 1 for m in counts) + try: + validate(word) + except ValueError: + require(not simple, "valid support rejected") + rejected += 1 + continue + require(simple, "multiplicity accepted") + for values in itertools.product((0, 1), repeat=3): + literal = sum(values[k] for k in row) % 2 + membership = sum(values[k] for k in range(3) if k in row) % 2 + require(literal == membership, "scatter coefficient mismatch") + accepted += 1 + return {"rows": accepted + rejected, "accepted": accepted, "rejected": rejected} + + +def audit(directory): + data = inputs() + boundary = runpy.run_path(str(PACKAGE / "boundary.py")) + word = json.loads(gzip.decompress(data[WORD])) + fixture = directory / "word.json.gz" + fixture.write_bytes(data[WORD]) + original, successor = directory / "original", directory / "successor" + script = directory / "original-export.py" + script.write_bytes(data[boundary["SCRIPTS"]["export"]]) + old = run([sys.executable, "-I", "-B", str(script), str(fixture), str(original)]) + require(old.returncode == 0, old.stderr) + for mode, output in (("check", None), ("export", successor)): + result = cli(mode, fixture, output) + require(result.returncode == 0, result.stdout + result.stderr) + digests = {} + for name in ARTIFACTS: + body = (original / name).read_bytes() + require(body == (successor / name).read_bytes(), "artifact identity: " + name) + digests[name] = hashlib.sha256(body).hexdigest() + raw = (successor / ARTIFACTS[0]).read_bytes() + actual, expected = columns(raw, word) + require(actual == expected and len(actual) == 661, "all dirty columns") + predecessor = json.loads(data[PREDECESSOR]) + require(digests[ARTIFACTS[0]] == predecessor["baseline"]["records_sha256"], "predecessor baseline") + paired = copy.deepcopy(word) + paired["scatter"][0].extend([0, 0]) + fixture.write_bytes(gzip.compress(json.dumps(paired).encode(), mtime=0)) + checker = directory / "original-check.py" + checker.write_bytes(data[boundary["SCRIPTS"]["check"]]) + old_check = run([sys.executable, "-I", "-B", str(checker), str(fixture)]) + require(old_check.returncode == 0, "predecessor paired symbolic acceptance") + original_bad = directory / "original-mutant" + old = run([sys.executable, "-I", "-B", str(script), str(fixture), str(original_bad)]) + require(old.returncode == 0, "predecessor mutant exported") + old_raw = (original_bad / ARTIFACTS[0]).read_bytes() + require(hashlib.sha256(old_raw).hexdigest() == predecessor["mutant"]["records_sha256"], "same counterexample") + actual_bad, _ = columns(old_raw, paired) + require([i for i in range(661) if actual_bad[i] != expected[i]] == [111], "one changed target") + require(actual_bad[111] >> 472 & 1, "dirty-input witness") + rejected = directory / "rejected" + for mode, output in (("check", None), ("export", rejected)): + result = cli(mode, fixture, output) + require(result.returncode == 2 and "duplicate index 0" in result.stderr, "entry guard") + require(not rejected.exists(), "reject before output creation") + return {"schema": boundary["SCHEMA"], "columns": 661, "records": len(raw) // 24, + "artifacts_sha256": digests, "paired_mutant_rejected_modes": ["check", "export"], + "predecessor_paired_symbolic_accepts": True, + "enumeration": support_enumeration(boundary["validate_scatter"])} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix="scatter-boundary-verify-") as temporary: + result = audit(Path(temporary)) + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((PACKAGE / "RESULT.json").read_bytes()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), "typed receipt") + print("PASS_SIMPLE_SCATTER_BOUNDARY columns=661 artifacts=3 rows=364 modes=2 no_new_kappa") + + +if __name__ == "__main__": + main()