diff --git a/docs/research/assembly-domain-receipt-check.md b/docs/research/assembly-domain-receipt-check.md new file mode 100644 index 0000000000..e088378ddc --- /dev/null +++ b/docs/research/assembly-domain-receipt-check.md @@ -0,0 +1,77 @@ +# Exact claims in the assembly-domain diagnostic receipt + +ywz65, with OpenAI Codex assistance. 2026-10-15. Apache-2.0. + +The maintained `scripts/audit_assembly_domain.py --check` now compares saved +Boolean claims and integer counts without Python's numeric type coercions and +rejects duplicate JSON object keys. It still accepts changed object-key order, +whitespace and CRLF line endings. The diagnostic arithmetic, its four frozen +source pins, the saved receipt and the `--write` generator are unchanged. + +This repairs receipt integrity only. It neither changes the production assembly +verifier nor enlarges its parameter domain. In particular, a malformed receipt +previously receiving `PASS` is not evidence that a new multiplication construction +was accepted. + +## Reproduced failure and repair + +The baseline is canonical main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. On its actual command-line checker, +each following edit to `docs/research/assembly-domain-audit.json` received `PASS` +under Python 3.12.14 with `-I -O -B`: + +| Single edit | Lost distinction | Repaired checker | +|---|---|---| +| Replace the first `strict_arithmetic_rejects_with_assumed_bridge: true` value with `1` | Boolean rejection claim versus an integer | Reject | +| Change `published_control.strict_constraint_count` from `47` to `47.0000000000000000000001` | Nonintegral decimal rounds to the float `47.0`, which compares equal to integer `47` | Reject | +| Put a `false` occurrence of the first rejection claim immediately before its existing `true` occurrence | The default JSON decoder silently discards the contradictory first claim | Reject | + +The regression also duplicates the published constraint count as `0` followed by +`47`; the old comparison accepts this and the new checker rejects it. These +counts enumerate constraints and the flags report whether strict arithmetic +rejected a hypothetical row, so their types carry meaning in this receipt. +All rational quantities remain exact strings; this patch does not introduce a +general decimal normalization policy. + +The JSON object hook detects duplicates at every nesting level before decoding +can discard them. Recursive comparison checks identical types, all object keys, +ordered list contents and exact scalar values against the freshly recomputed +report. It does not ignore additional fields. No `assert` gates acceptance. + +## Validation and provenance + +```sh +python3 -I -O -B -m unittest discover -s tests -p test_assembly_domain.py -v +python3 -I -O -B scripts/audit_assembly_domain.py --check docs/research/assembly-domain-audit.json +``` + +All 10 tests passed on Windows with Python 3.12.14. The tests execute the actual +CLI for each of the four formerly accepted mutations, both normally and with +optimization, and retain positive compact/reordered and CRLF receipts. They also +retain the original arithmetic/source controls and reject changed rational +slacks, reordered obligations, missing pins and added claims. Full selected +frontier replay is not needed for this diagnostic-only change and was not run. + +The original domain diagnostic and its mathematical analysis are Douglas +Colkitt's work with OpenAI Codex assistance. The broader typed-comparison failure +class was already documented by +[PR #2040](https://github.com/CrocSwap/integer-mult-bounds/pull/2040), inspected at +`d31c1418c0c23994d1444dbd9d356b9a8238fd5e`; this contribution applies the lesson to +the separate maintained assembly-domain receipt consumer. It does not reproduce +or replace that PR's selected-final payload comparator. + +Task selection used nonce `8ab28c18ff34f63e1b1aeb9c098ffbb2`, priority revision 4, +and the `portable-replay` card's canonical-comparison audit variation, refined to +this receipt. The prescribed baseline binding check passed. Canonical main was +refetched at 2026-10-15 14:22 UTC and remained the commit above. Overlap searched +open PR metadata, Discussions and local notes; the complete cached snapshots +contain 750 open PRs (14:08 UTC) and 1,216 Discussion records (14:10 UTC). +This is not coverage of every code diff or unpublished investigation. + +## Open next questions + +Other maintained receipt consumers need their own field-specific failure witness +before adopting this comparison rule. A useful next check would identify one +consumer with typed Boolean/count claims, mutate those claims through its real +CLI, and preserve every documented normalization. No repository-wide schema or +universal exact-number policy is established here. diff --git a/scripts/audit_assembly_domain.py b/scripts/audit_assembly_domain.py index 09c6d1a172..6beb986f86 100644 --- a/scripts/audit_assembly_domain.py +++ b/scripts/audit_assembly_domain.py @@ -139,6 +139,34 @@ def audit(): 'Extension of interval-enclosure and cutoff ranges']) +def unique_object(pairs): + """Reject contradictory or repeated fields before the JSON decoder loses them.""" + result = {} + for key, value in pairs: + require(key not in result, 'Duplicate diagnostic receipt key: ' + key) + result[key] = value + return result + + +def same_receipt_value(actual, expected): + """Preserve Boolean claims and integer counts, unlike Python's 1 == True.""" + if type(actual) is not type(expected): + return False + if isinstance(expected, dict): + return (actual.keys() == expected.keys() + and all(same_receipt_value(actual[key], value) + for key, value in expected.items())) + if isinstance(expected, list): + return (len(actual) == len(expected) + and all(same_receipt_value(a, e) for a, e in zip(actual, expected))) + return actual == expected + + +def check_receipt(path, report): + saved = json.loads(path.read_text(encoding='utf-8'), object_pairs_hook=unique_object) + require(same_receipt_value(saved, report), 'Diagnostic receipt differs') + + def main(): parser = argparse.ArgumentParser(description=__doc__) group = parser.add_mutually_exclusive_group() @@ -147,7 +175,7 @@ def main(): args = parser.parse_args() report = audit() if args.check: - require(json.loads(args.check.read_text()) == report, 'Diagnostic receipt differs') + check_receipt(args.check, report) print('PASS pinned assembly-domain diagnostic; no production constraint relaxed') elif args.write: args.write.write_text(json.dumps(report, indent=2) + '\n') diff --git a/tests/test_assembly_domain.py b/tests/test_assembly_domain.py index dc5c9d9939..3acd89018a 100644 --- a/tests/test_assembly_domain.py +++ b/tests/test_assembly_domain.py @@ -4,6 +4,8 @@ import importlib.util import json from pathlib import Path +import subprocess +import sys import tempfile import unittest @@ -58,8 +60,71 @@ def test_float_inputs_are_rejected(self): audit.diagnostic_case(0.04, Q(1, 20), Q(19, 500)) def test_receipt_is_reproducible(self): - saved = json.loads((ROOT / 'docs/research/assembly-domain-audit.json').read_text()) - self.assertEqual(saved, self.report) + audit.check_receipt(ROOT / 'docs/research/assembly-domain-audit.json', self.report) + + def check_cli(self, text, *, optimized=False): + with tempfile.TemporaryDirectory() as directory: + receipt = Path(directory) / 'receipt.json' + receipt.write_bytes(text.encode('utf-8')) + flags = ['-I', '-O', '-B'] if optimized else ['-I', '-B'] + return subprocess.run( + [sys.executable, *flags, str(ROOT / 'scripts/audit_assembly_domain.py'), + '--check', str(receipt)], capture_output=True, text=True) + + def test_cli_accepts_reformatting_without_changing_claims(self): + for text in (json.dumps(self.report, sort_keys=True, separators=(',', ':')), + json.dumps(self.report, indent=3).replace('\n', '\r\n')): + with self.subTest(layout=text[:30]): + result = self.check_cli(text) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS pinned assembly-domain diagnostic', result.stdout) + + def test_cli_rejects_type_coercion_and_conflicting_duplicate_claims(self): + original = json.dumps(self.report) + flag = '"strict_arithmetic_rejects_with_assumed_bridge": true' + mutations = { + 'boolean_as_integer': original.replace(flag, flag.replace('true', '1'), 1), + 'fractional_constraint_count': original.replace( + '"strict_constraint_count": 47', + '"strict_constraint_count": 47.0000000000000000000001', 1), + 'contradictory_nested_claim': original.replace( + flag, flag.replace('true', 'false') + ', ' + flag, 1), + 'contradictory_nested_count': original.replace( + '"strict_constraint_count": 47', + '"strict_constraint_count": 0, "strict_constraint_count": 47', 1), + } + for name, text in mutations.items(): + # Establish the old comparison's false acceptance on this exact report. + self.assertEqual(json.loads(text), self.report) + for optimized in (False, True): + with self.subTest(mutation=name, optimized=optimized): + result = self.check_cli(text, optimized=optimized) + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertNotIn('PASS pinned assembly-domain diagnostic', result.stdout) + expected = 'Duplicate diagnostic receipt key' if name.startswith('contradictory') else 'Diagnostic receipt differs' + self.assertIn(expected, result.stderr) + + def test_full_claim_content_remains_bound(self): + mutations = [] + changed = json.loads(json.dumps(self.report)) + changed['cases']['domain_boundary']['failed_slacks']['b_below_one_over32'] = '1/100' + mutations.append(changed) + changed = json.loads(json.dumps(self.report)) + changed['unproved'].reverse() + mutations.append(changed) + changed = json.loads(json.dumps(self.report)) + del changed['source_sha256'] + mutations.append(changed) + changed = json.loads(json.dumps(self.report)) + changed['extra_unproved_claim'] = True + mutations.append(changed) + with tempfile.TemporaryDirectory() as directory: + receipt = Path(directory) / 'receipt.json' + for index, changed in enumerate(mutations): + with self.subTest(mutation=index): + receipt.write_text(json.dumps(changed), encoding='utf-8') + with self.assertRaisesRegex(ValueError, 'Diagnostic receipt differs'): + audit.check_receipt(receipt, self.report) if __name__ == '__main__':