diff --git a/.github/workflows/d2-atom-integral.yml b/.github/workflows/d2-atom-integral.yml index 70100d320..19467302e 100644 --- a/.github/workflows/d2-atom-integral.yml +++ b/.github/workflows/d2-atom-integral.yml @@ -21,7 +21,7 @@ permissions: jobs: d2-atom-integral: runs-on: ubuntu-latest - timeout-minutes: 30 + timeout-minutes: 60 env: LEAN_NUM_THREADS: 2 steps: diff --git a/companions/d2_atom_integral_20261006/SCOPE.md b/companions/d2_atom_integral_20261006/SCOPE.md index 71008894a..a5b523d5c 100644 --- a/companions/d2_atom_integral_20261006/SCOPE.md +++ b/companions/d2_atom_integral_20261006/SCOPE.md @@ -174,3 +174,27 @@ bytes. The new tests are synthetic and do not execute Lean. New current-commit kernel receipts and hosted checks are still required after publication. Alignment remains PENDING_INDEPENDENT_REVIEW; scientific effect NONE. + +## RF312 source/receipt engineering proposal, 28 October 2026 + +This dated private proposal preserves the mathematical text and historical evidence above. +Its source basis is RF312 `80946e1cf311b3cbbb051bb3662357b11f8b3d75`, formal tree +`8922fd8c833df0c52d4a8c7b5c3ad802b93098d4`, with the unchanged nine formal Lean/root +blobs, 63 target entries, source modules, dependencies, toolchain and companion Lean/contract bytes. +These are source identities and declared dependencies, not a fresh proof or applicability review. + +The raw manifest SHA256 is `ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062`; +the core receipt instead binds composite source `481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066`. +The fixed strict RF312 overlay contract must match; no raw-receipt fallback is admitted. +The reused identity validator lies outside the formal tree, at `tools/required_formal_check.py` +(blob `0b9d694bdf888c75826ca07ae176c5a5c43b8880`, SHA256 +`6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc`). Its source bytes are +checked before those verified bytes are evaluated; drift, symlink, missing overlay and wrong regimes refuse. +Its identity is also retained in the source snapshot across execution. Atom's two imported companion +Lean pins and all existing runtime re-observation checks are preserved. + +Protocol unit fixtures are synthetic and execute no Lean or finite-law diagnostic. They do not +supply a core or companion kernel/runtime receipt. Existing receipts/reviews remain historical; +fresh actual current-composition core and all three D2 hosted/negative-control/runtime checks, +qualified review and separate integration remain required. Scientific effect NONE; alignment and +scientific acceptance are unchanged. No existing312 source/ref or integration custody follows. diff --git a/companions/d2_atom_integral_20261006/SOURCE_FILES.json b/companions/d2_atom_integral_20261006/SOURCE_FILES.json index 82953007d..1e27e280b 100644 --- a/companions/d2_atom_integral_20261006/SOURCE_FILES.json +++ b/companions/d2_atom_integral_20261006/SOURCE_FILES.json @@ -1,10 +1,10 @@ { - "core_tree": "fc0b11706d064b9de42331ee0a2464865107b87b", + "core_tree": "8922fd8c833df0c52d4a8c7b5c3ad802b93098d4", "files": { ".github/workflows/d2-atom-integral.yml": { "bytes": 1942, - "git_blob": "70100d3205a492bdf3583153d4f82f7e6f2eac7a", - "sha256": "c9b7f107af2dff4cfb71496616a6514a41af39291799b6ec9287977791053a99" + "git_blob": "19467302e94fb03e4afa8e05e7be545a15195917", + "sha256": "790bca4b320dd9cdf1f309cd126ed1334c54680a72b4e3693964386a9ea5d694" }, "companions/d2_atom_integral_20261006/Contract.lean": { "bytes": 3433, @@ -17,14 +17,14 @@ "sha256": "247507c4b7aeaccc033cd4d648442172d61227bb27239a7dacccd0f2fa1ba6c3" }, "companions/d2_atom_integral_20261006/SCOPE.md": { - "bytes": 10928, - "git_blob": "71008894a5a3aa01da18163afbce1903dabe51df", - "sha256": "90f12484ead012929ce0664ed0d4ef90f40c2d75d39d2d8580115f19b2db40ec" + "bytes": 12754, + "git_blob": "a5b523d5c7a704f368fb51c58b15e0e3fbc926ac", + "sha256": "aa3e0d19cda6a032384a00aa994950a1cf14e94143d5bc0400a4210acd7bddb2" }, "companions/d2_atom_integral_20261006/check.py": { - "bytes": 10044, - "git_blob": "eb918b7ee775c0bb61a9ffff2cadba0b76e40673", - "sha256": "df3f8aec73478b74d0d0f2f06d2655097f80b9d9ebbb4c720d6a63076493315d" + "bytes": 11895, + "git_blob": "791ce1ddd1cb2df075a118f061922d323e42ac3d", + "sha256": "14c432a63a2cc9c74d3698be87927fa5e518e64b62a670ac0a3b579095e77749" }, "companions/d2_atom_integral_20261006/replay.sh": { "bytes": 3471, @@ -32,9 +32,9 @@ "sha256": "89d9a0c64fd88aa8cf8c6614df84b3f543c3d4ecc87ad2e529feffda90091c75" }, "companions/d2_atom_integral_20261006/test_check.py": { - "bytes": 8946, - "git_blob": "efa3793f8ffeecc3e504b559601d52c6e68008f0", - "sha256": "83750832498ac74f96297174c494262537069c9c82eacb7aa2315f39a77ad454" + "bytes": 19049, + "git_blob": "59ef016d445913dcb9d6e43ae5cf6774bbbd1ecd", + "sha256": "31658f7cc26a65102710cc7f29e477412403871b724a4b9a861f7c1172a6b99c" } }, "scientific_effect": "NONE", diff --git a/companions/d2_atom_integral_20261006/check.py b/companions/d2_atom_integral_20261006/check.py index eb918b7ee..791ce1ddd 100644 --- a/companions/d2_atom_integral_20261006/check.py +++ b/companions/d2_atom_integral_20261006/check.py @@ -18,9 +18,14 @@ PACKAGE='companions/d2_atom_integral_20261006' WORKFLOW='.github/workflows/d2-atom-integral.yml' REPO='d6g8k5htny-coder/Math-' -CORE_TREE='fc0b11706d064b9de42331ee0a2464865107b87b' -CORE_MANIFEST='7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778' -CORE_GATE='25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a' +CORE_TREE='8922fd8c833df0c52d4a8c7b5c3ad802b93098d4' +CORE_MANIFEST='ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062' +CORE_GATE='509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731' + +CORE_SOURCE_IDENTITY='481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066' +CORE_IDENTITY_PATH='tools/required_formal_check.py' +CORE_IDENTITY_SHA256='6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc' +CORE_IDENTITY_BLOB='0b9d694bdf888c75826ca07ae176c5a5c43b8880' CONSUMED={ 'companions/d2_moment_bridge_20261006/D2MomentBridge.lean':'b3184107e290189b91e3e18fd2aa1cb631bb9bde', 'companions/d2_square_schur_20261006/D2SquareSchur.lean':'4855c92d55254969e1de7f8cf8dec2bdc027cf69'} @@ -54,6 +59,38 @@ def reject(_):raise ValueError('noninteger JSON number') def git(*args): return subprocess.run(['git',*args],cwd=ROOT,check=True,capture_output=True,text=True,timeout=30).stdout.strip() +def core_identity(): + """Bind the outside-tree validator before evaluating its verified bytes.""" + path = ROOT / CORE_IDENTITY_PATH + require(not any(p.is_symlink() for p in (path, *path.parents)) and path.is_file(), + 'core identity validator missing or symlink') + raw = path.read_bytes() + framed = b'blob ' + str(len(raw)).encode() + b'\0' + raw + require(sha(raw) == CORE_IDENTITY_SHA256 + and hashlib.sha1(framed).hexdigest() == CORE_IDENTITY_BLOB, + 'core identity validator changed') + namespace = {'__name__': 'bound_d2_core_identity', '__file__': str(path)} + exec(compile(raw, str(path), 'exec'), namespace) + manifest = ROOT / 'formal/manifest.json' + manifest_raw = manifest.read_bytes() + require(sha(manifest_raw) == CORE_MANIFEST, 'core manifest changed') + digest = namespace['manifest_identity'](manifest, manifest_raw) + require(digest == CORE_SOURCE_IDENTITY, 'core source identity changed') + return digest + + +def validate_core_receipt(core, current): + """The current core receipt binds the composite source, not the raw manifest.""" + require(isinstance(core, dict), 'invalid core receipt') + require(core.get('checked_commit') == current['checked_commit'], + 'core executed different source') + require(core.get('manifest_sha256') == core_identity(), 'core receipt manifest') + require(core.get('formalization_status') == 'kernel-checked', 'no core kernel receipt') + + + + + def source(): meta=strict((SIDE/'SOURCE_FILES.json').read_bytes());head=git('rev-parse','HEAD') require(set(meta)=={'version','scientific_effect','core_tree','targets','files'},'manifest schema') @@ -64,6 +101,7 @@ def source(): require(git('rev-parse',head+':formal')==CORE_TREE,'core tree changed') require(sha((ROOT/'formal/manifest.json').read_bytes())==CORE_MANIFEST,'core manifest changed') require(sha((ROOT/'formal/gate.py').read_bytes())==CORE_GATE,'core verifier changed') + core_identity() if os.environ.get('GITHUB_ACTIONS')=='true': require(os.environ.get('GITHUB_SHA')==head and os.environ.get('GITHUB_REPOSITORY')==REPO,'host/source mismatch') require(os.environ.get('GITHUB_RUN_ID') and os.environ.get('GITHUB_RUN_ATTEMPT'),'missing run identity') @@ -78,7 +116,10 @@ def source(): require(git('rev-parse',head+':'+name)==ids[name]['git_blob'],'dirty source: '+name) if name in PAYLOADS:require(meta['files'][name]==ids[name],'source identity: '+name) if name in CONSUMED:require(CONSUMED[name]==ids[name]['git_blob'],'consumed source changed: '+name) - git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW,*CONSUMED) + helper_id=identity((ROOT/CORE_IDENTITY_PATH).read_bytes()) + require(git('rev-parse',head+':'+CORE_IDENTITY_PATH)==helper_id['git_blob'],'dirty core identity validator') + ids[CORE_IDENTITY_PATH]=helper_id + git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW,CORE_IDENTITY_PATH,*CONSUMED) return {'checked_commit':head,'repository':REPO,'run_id':os.environ.get('GITHUB_RUN_ID','local'), 'run_attempt':os.environ.get('GITHUB_RUN_ATTEMPT','local'),'core_tree':CORE_TREE, 'sources':ids,'declarations':list(TARGETS),'scientific_effect':'NONE'} @@ -149,8 +190,7 @@ def finish(out): require((out/(label+'.status')).read_bytes()==b'1\n','negative status: '+label) negative((out/(label+'.log')).read_text(),label,1) raw=(ROOT/'formal/.lake/formal-evidence/receipt.json').read_bytes();core=strict(raw) - require(core['checked_commit']==current['checked_commit'] and core['manifest_sha256']==CORE_MANIFEST,'core identity') - require(core['formalization_status']=='kernel-checked','no core kernel receipt') + validate_core_receipt(core,current) final=final_runtime(out,core,strict((ROOT/'formal/manifest.json').read_bytes())['dependency_revisions']) result={**current,'axioms':ax,'theorem_count':6,'definition_count':0,'core_receipt_sha256':sha(raw),'final_observation':final, 'formalization_status':'kernel-checked','alignment_status':'PENDING_INDEPENDENT_REVIEW', diff --git a/companions/d2_atom_integral_20261006/test_check.py b/companions/d2_atom_integral_20261006/test_check.py index efa3793f8..59ef016d4 100644 --- a/companions/d2_atom_integral_20261006/test_check.py +++ b/companions/d2_atom_integral_20261006/test_check.py @@ -150,4 +150,205 @@ def test_replay_observes_after_the_last_lean_run_and_finish_requires_it(self): source=(SIDE/'check.py').read_text();body=source[source.index('def finish(out):'):source.index('def main(')] self.assertIn('final_runtime(out,',body) +def copy_formal_fixture(source, destination): + """Copy formal inputs for the actual protocol fixture; never execute Lean.""" + import shutil + return shutil.copytree(source, destination, + ignore=shutil.ignore_patterns('.lake', '__pycache__')) + + +class SourceFixtureIsolationTests(unittest.TestCase): + """Ignored runtime state must not enter a source-only protocol fixture.""" + def test_ignored_runtime_and_python_cache_are_not_copied(self): + import subprocess + with tempfile.TemporaryDirectory() as td: + base = Path(td) + source = base / 'input' / 'formal' + source.mkdir(parents=True) + (source / '.gitignore').write_text('.lake/\n__pycache__/\n') + tracked = source / 'tracked-source.txt' + tracked.write_bytes(b'exact tracked source\n') + tracked.chmod(0o755) + ignored = ('.lake/packages/runtime-cache', '__pycache__/runtime.pyc') + for relative in ignored: + path = source / relative + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(b'ignored runtime sentinel\n') + subprocess.run(['git', '-C', str(source.parent), 'init', '-q'], + check=True, capture_output=True) + subprocess.run(['git', '-C', str(source.parent), 'add', 'formal'], + check=True, capture_output=True) + for relative in ignored: + subprocess.run(['git', '-C', str(source.parent), 'check-ignore', + 'formal/' + relative], check=True, capture_output=True) + copied = base / 'copied-formal' + copy_formal_fixture(source, copied) + for relative in ignored: + with self.subTest(relative=relative): + self.assertFalse((copied / relative).exists(), + 'ignored runtime cache entered the source fixture') + self.assertEqual((copied / tracked.name).read_bytes(), tracked.read_bytes()) + self.assertEqual((copied / tracked.name).stat().st_mode & 0o777, + tracked.stat().st_mode & 0o777) + + def test_actual_tracked_formal_tree_bytes_and_modes_preserved(self): + import subprocess + original = SIDE.parents[1] + def git(root, *args): + return subprocess.check_output(['git', '-C', str(root), *args], text=True).strip() + with tempfile.TemporaryDirectory() as td: + base = Path(td) + copied = base / 'formal' + copy_formal_fixture(original / 'formal', copied) + git(base, 'init', '-q') + git(base, 'add', 'formal') + tree = git(base, 'write-tree') + self.assertEqual(git(base, 'rev-parse', tree + ':formal'), + git(original, 'rev-parse', 'HEAD:formal')) + for relative in git(original, 'ls-files', '--', 'formal').splitlines(): + source = original / relative + target = base / relative + with self.subTest(path=relative): + self.assertEqual(target.read_bytes(), source.read_bytes()) + self.assertEqual(target.stat().st_mode & 0o777, + source.stat().st_mode & 0o777) + + +class CoreIdentityProtocolTests(unittest.TestCase): + """Source/receipt protocol fixtures only; no Lean or finite-law execution.""" + def setUp(self): + import shutil + import subprocess + from unittest import mock + self._subprocess = subprocess + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name).resolve() + original = SIDE.parents[1] + copy_formal_fixture(original / 'formal', self.root / 'formal') + for package in ('d2_moment_bridge', 'd2_square_schur', 'd2_atom_integral'): + relative = Path('companions') / (package + '_20261006') + shutil.copytree(original / relative, self.root / relative) + workflow = Path('.github/workflows') / (package.replace('_', '-') + '.yml') + (self.root / workflow).parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(original / workflow, self.root / workflow) + (self.root / 'tools').mkdir() + shutil.copy2(original / 'tools/required_formal_check.py', + self.root / 'tools/required_formal_check.py') + for args in (('init', '-q'), ('add', '.'), + ('-c', 'user.name=protocol-fixture', + '-c', 'user.email=protocol@example.invalid', + 'commit', '-qm', 'copied exact source protocol fixture')): + subprocess.run(['git', '-C', str(self.root), *args], + check=True, capture_output=True) + self.head = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD'], text=True).strip() + actual_tree = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD:formal'], + text=True).strip() + self.assertEqual(actual_tree, '8922fd8c833df0c52d4a8c7b5c3ad802b93098d4') + self.context = {'checked_commit': self.head} + patch = mock.patch.dict('os.environ', {'GITHUB_ACTIONS': 'false'}) + patch.start() + self.addCleanup(patch.stop) + copied = self.root / 'companions' / SIDE.name / 'check.py' + spec = importlib.util.spec_from_file_location('copied_d2_protocol', copied) + self.c = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.c) + + def validator(self): + function = getattr(self.c, 'validate_core_receipt', None) + self.assertTrue(callable(function), 'production core receipt validator missing') + return function + + def good_receipt(self): + return {'checked_commit': self.head, + 'manifest_sha256': '481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066', + 'formalization_status': 'kernel-checked'} + + def test_source_accepts_exact_reviewed_core_without_lean(self): + try: + current = self.c.source() + except (ValueError, self._subprocess.CalledProcessError) as error: + self.fail('reviewed frozen source cut must bind: ' + str(error)) + self.assertEqual(current['checked_commit'], self.head) + self.assertIn('tools/required_formal_check.py', current['sources']) + + def test_actual_producer_to_receipt_validator(self): + producer_path = self.root / 'formal/gate.py' + spec = importlib.util.spec_from_file_location('copied_rf312_producer', producer_path) + producer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(producer) + _, digest = producer.source_check() + self.assertEqual(digest, self.good_receipt()['manifest_sha256']) + self.validator()( + {'checked_commit': self.head, 'manifest_sha256': digest, + 'formalization_status': 'kernel-checked'}, self.context) + + def test_raw_digest_wrong_commit_and_non_kernel_receipts_refuse(self): + validate = self.validator() + raw = self.c.sha((self.root / 'formal/manifest.json').read_bytes()) + for key, value in (('manifest_sha256', raw), + ('checked_commit', '0' * 40), + ('formalization_status', 'source')): + with self.subTest(key=key): + bad = dict(self.good_receipt(), **{key: value}) + with self.assertRaises(ValueError): + validate(bad, self.context) + + def test_helper_drift_refuses_before_evaluating_changed_code(self): + helper = self.root / 'tools/required_formal_check.py' + helper.write_bytes(helper.read_bytes() + + b"\nraise RuntimeError('untrusted helper evaluated')\n") + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_helper_symlink_and_absence_refuse(self): + helper = self.root / 'tools/required_formal_check.py' + raw = helper.read_bytes() + helper.unlink() + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + outside = self.root / 'outside-validator.py' + outside.write_bytes(raw) + helper.symlink_to(outside) + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_manifest_overlay_and_core_file_drift_refuse(self): + changes = (('formal/manifest.json', b'\n'), + ('formal/manifest.overlay.json', b'\n'), + ('formal/ResearchFormalCoreR1/AlgebraV2.lean', b'\n')) + for relative, suffix in changes: + with self.subTest(path=relative): + path = self.root / relative + raw = path.read_bytes() + path.write_bytes(raw + suffix) + try: + with self.assertRaises((ValueError, self._subprocess.CalledProcessError)): + self.c.source() + finally: + path.write_bytes(raw) + + def test_missing_or_unknown_overlay_regime_never_downgrades(self): + validate = self.validator() + overlay = self.root / 'formal/manifest.overlay.json' + original = overlay.read_bytes() + overlay.unlink() + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(b'{"schema_version":2,"files":{}}') + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(original) + manifest = self.root / 'formal/manifest.json' + raw = manifest.read_bytes() + document = self.c.strict(raw) + document.pop('source_identity') + manifest.write_text(__import__('json').dumps(document)) + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + + + if __name__=='__main__':unittest.main(verbosity=2) diff --git a/companions/d2_moment_bridge_20261006/README.md b/companions/d2_moment_bridge_20261006/README.md index 005796b55..b60408210 100644 --- a/companions/d2_moment_bridge_20261006/README.md +++ b/companions/d2_moment_bridge_20261006/README.md @@ -200,3 +200,27 @@ bytes. The new tests are synthetic and do not execute Lean. New current-commit kernel receipts and hosted checks are still required after publication. Alignment remains PENDING_INDEPENDENT_REVIEW; scientific effect NONE. + +## RF312 source/receipt engineering proposal, 28 October 2026 + +This dated private proposal preserves the mathematical text and historical evidence above. +Its source basis is RF312 `80946e1cf311b3cbbb051bb3662357b11f8b3d75`, formal tree +`8922fd8c833df0c52d4a8c7b5c3ad802b93098d4`, with the unchanged nine formal Lean/root +blobs, 63 target entries, source modules, dependencies, toolchain and companion Lean/contract bytes. +These are source identities and declared dependencies, not a fresh proof or applicability review. + +The raw manifest SHA256 is `ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062`; +the core receipt instead binds composite source `481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066`. +The fixed strict RF312 overlay contract must match; no raw-receipt fallback is admitted. +The reused identity validator lies outside the formal tree, at `tools/required_formal_check.py` +(blob `0b9d694bdf888c75826ca07ae176c5a5c43b8880`, SHA256 +`6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc`). Its source bytes are +checked before those verified bytes are evaluated; drift, symlink, missing overlay and wrong regimes refuse. +Its identity is also retained in the source snapshot across execution. Atom's two imported companion +Lean pins and all existing runtime re-observation checks are preserved. + +Protocol unit fixtures are synthetic and execute no Lean or finite-law diagnostic. They do not +supply a core or companion kernel/runtime receipt. Existing receipts/reviews remain historical; +fresh actual current-composition core and all three D2 hosted/negative-control/runtime checks, +qualified review and separate integration remain required. Scientific effect NONE; alignment and +scientific acceptance are unchanged. No existing312 source/ref or integration custody follows. diff --git a/companions/d2_moment_bridge_20261006/SOURCE_FILES.json b/companions/d2_moment_bridge_20261006/SOURCE_FILES.json index b72d7de79..363ff561c 100644 --- a/companions/d2_moment_bridge_20261006/SOURCE_FILES.json +++ b/companions/d2_moment_bridge_20261006/SOURCE_FILES.json @@ -1,5 +1,5 @@ { - "core_tree": "fc0b11706d064b9de42331ee0a2464865107b87b", + "core_tree": "8922fd8c833df0c52d4a8c7b5c3ad802b93098d4", "definitions": [ "moment", "cubicResidual" @@ -16,14 +16,14 @@ "sha256": "cde3bbd96eb29eb9ab7ff1448ffab1f794fb2b80355ac618800155eea6ccc42f" }, "companions/d2_moment_bridge_20261006/README.md": { - "bytes": 12277, - "git_blob": "005796b5527601c1156d2deaa9c950adf253faf3", - "sha256": "16b5b7e07eaa2a047160c2a295333eea370644d8343b635d6d92a4556a33eff6" + "bytes": 14103, + "git_blob": "b6040821087c473dd7b65d84b83b3fb4b0572fc4", + "sha256": "49640108a670a37fd4322c16c544c0cbf868a4eee824b0eca41139f150c771a7" }, "companions/d2_moment_bridge_20261006/check.py": { - "bytes": 10232, - "git_blob": "867324d3829e35d503df993f1a69a159c4a664c0", - "sha256": "04310a141a4c042eb8d255bba2c073b9ec348460e6dc522b6d7189285acd2730" + "bytes": 12105, + "git_blob": "9ef3412bcd3ff4bde17e0cdbe48c8194a62004a4", + "sha256": "fa71312e4ffe26a5dae1d036bf7339802cfe57fb3d12d8ec405ed90a3fec0954" }, "companions/d2_moment_bridge_20261006/replay.sh": { "bytes": 2793, @@ -31,9 +31,9 @@ "sha256": "1e50e7ffc5c68b3771e32f2574d709d055a9b5b43ef1fa74bcaccfc14e912a68" }, "companions/d2_moment_bridge_20261006/test_bridge.py": { - "bytes": 11134, - "git_blob": "5bcc4628bf61f035f96f7a4faf6c796a38e05fe9", - "sha256": "cf257c0dd750c5cc108d5af5d61129531d7f57e2ed03c6a5ab8261964fb25469" + "bytes": 21237, + "git_blob": "0e083c427ce775b2b2d34f7b8d04445afda7c5c4", + "sha256": "4c0930e6e6f73ead7bf1c562786257c458f51a8083e321568095492bf972b3d9" } }, "schema": 1, diff --git a/companions/d2_moment_bridge_20261006/check.py b/companions/d2_moment_bridge_20261006/check.py index 867324d38..9ef3412bc 100644 --- a/companions/d2_moment_bridge_20261006/check.py +++ b/companions/d2_moment_bridge_20261006/check.py @@ -13,9 +13,14 @@ ROOT=SIDE.parents[1] PACKAGE='companions/d2_moment_bridge_20261006' WORKFLOW='.github/workflows/d2-moment-bridge.yml' -CORE_TREE='fc0b11706d064b9de42331ee0a2464865107b87b' -CORE_MANIFEST='7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778' -CORE_GATE='25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a' +CORE_TREE='8922fd8c833df0c52d4a8c7b5c3ad802b93098d4' +CORE_MANIFEST='ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062' +CORE_GATE='509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731' + +CORE_SOURCE_IDENTITY='481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066' +CORE_IDENTITY_PATH='tools/required_formal_check.py' +CORE_IDENTITY_SHA256='6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc' +CORE_IDENTITY_BLOB='0b9d694bdf888c75826ca07ae176c5a5c43b8880' REPO='d6g8k5htny-coder/Math-' CONTROLS=('RejectZeroAtom','RejectSameRadius') @@ -52,6 +57,38 @@ def names(meta): return result +def core_identity(): + """Bind the outside-tree validator before evaluating its verified bytes.""" + path = ROOT / CORE_IDENTITY_PATH + require(not any(p.is_symlink() for p in (path, *path.parents)) and path.is_file(), + 'core identity validator missing or symlink') + raw = path.read_bytes() + framed = b'blob ' + str(len(raw)).encode() + b'\0' + raw + require(sha(raw) == CORE_IDENTITY_SHA256 + and hashlib.sha1(framed).hexdigest() == CORE_IDENTITY_BLOB, + 'core identity validator changed') + namespace = {'__name__': 'bound_d2_core_identity', '__file__': str(path)} + exec(compile(raw, str(path), 'exec'), namespace) + manifest = ROOT / 'formal/manifest.json' + manifest_raw = manifest.read_bytes() + require(sha(manifest_raw) == CORE_MANIFEST, 'core manifest changed') + digest = namespace['manifest_identity'](manifest, manifest_raw) + require(digest == CORE_SOURCE_IDENTITY, 'core source identity changed') + return digest + + +def validate_core_receipt(core, current): + """The current core receipt binds the composite source, not the raw manifest.""" + require(isinstance(core, dict), 'invalid core receipt') + require(core.get('checked_commit') == current['checked_commit'], + 'core executed different source') + require(core.get('manifest_sha256') == core_identity(), 'core receipt manifest') + require(core.get('formalization_status') == 'kernel-checked', 'no core kernel receipt') + + + + + def source(): meta=metadata();head=git('rev-parse','HEAD') require(re.fullmatch(r'[0-9a-f]{40}',head),'invalid HEAD') @@ -59,6 +96,7 @@ def source(): require(git('rev-parse',head+':formal')==CORE_TREE,'core tree changed; new source review required') require(sha((ROOT/'formal/manifest.json').read_bytes())==CORE_MANIFEST,'core manifest changed') require(sha((ROOT/'formal/gate.py').read_bytes())==CORE_GATE,'core verifier changed') + core_identity() if os.environ.get('GITHUB_ACTIONS')=='true': require(os.environ.get('GITHUB_SHA')==head and os.environ.get('GITHUB_REPOSITORY')==REPO,'host/source mismatch') require(os.environ.get('GITHUB_RUN_ID') and os.environ.get('GITHUB_RUN_ATTEMPT'),'run identity absent') @@ -75,7 +113,11 @@ def source(): if path in meta['files']: require(meta['files'][path]=={'bytes':len(raw),'sha256':sha(raw),'git_blob':bid},'manifest source mismatch: '+path) ids[path]={'sha256':sha(raw),'git_blob':bid,'bytes':len(raw)} - git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW) + helper_raw=(ROOT/CORE_IDENTITY_PATH).read_bytes() + helper_blob=blob(helper_raw) + require(git('rev-parse',head+':'+CORE_IDENTITY_PATH)==helper_blob,'dirty core identity validator') + ids[CORE_IDENTITY_PATH]={'bytes':len(helper_raw),'sha256':sha(helper_raw),'git_blob':helper_blob} + git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW,CORE_IDENTITY_PATH) return {'checked_commit':head,'repository':REPO,'run_id':os.environ.get('GITHUB_RUN_ID','local'), 'run_attempt':os.environ.get('GITHUB_RUN_ATTEMPT','local'),'core_tree':CORE_TREE, 'sources':ids,'declarations':names(meta),'scientific_effect':'NONE'} @@ -166,9 +208,7 @@ def finish(out): require((out/(label+'.status')).read_text()=='0\n','missing successful process: '+label) core=ROOT/'formal/.lake/formal-evidence/receipt.json' raw=core.read_bytes();receipt=strict(raw) - require(receipt['checked_commit']==current['checked_commit'],'core executed different source') - require(receipt['manifest_sha256']==CORE_MANIFEST,'core receipt manifest') - require(receipt['formalization_status']=='kernel-checked','no core kernel receipt') + validate_core_receipt(receipt,current) final=final_runtime(out,receipt,strict((ROOT/'formal/manifest.json').read_bytes())['dependency_revisions']) result={**current,'axioms':ax,'theorem_count':len(metadata()['theorems']), 'definition_count':len(metadata()['definitions']),'core_receipt_sha256':sha(raw),'final_observation':final, diff --git a/companions/d2_moment_bridge_20261006/test_bridge.py b/companions/d2_moment_bridge_20261006/test_bridge.py index 5bcc4628b..0e083c427 100644 --- a/companions/d2_moment_bridge_20261006/test_bridge.py +++ b/companions/d2_moment_bridge_20261006/test_bridge.py @@ -49,7 +49,7 @@ def test_exact_declared_inventory(self): self.assertEqual(meta['theorems'],THEOREMS) self.assertEqual(meta['definitions'],DEFINITIONS) self.assertEqual(meta['scientific_effect'],'NONE') - self.assertEqual(meta['core_tree'],'fc0b11706d064b9de42331ee0a2464865107b87b') + self.assertEqual(meta['core_tree'],'8922fd8c833df0c52d4a8c7b5c3ad802b93098d4') def test_residual_identity_and_exact_equality_class(self): count=0 @@ -198,5 +198,206 @@ def test_replay_observes_after_the_last_lean_run_and_finish_requires_it(self): source=(SIDE/'check.py').read_text();body=source[source.index('def finish(out):'):source.index('def main(')] self.assertIn('final_runtime(out,',body) +def copy_formal_fixture(source, destination): + """Copy formal inputs for the actual protocol fixture; never execute Lean.""" + import shutil + return shutil.copytree(source, destination, + ignore=shutil.ignore_patterns('.lake', '__pycache__')) + + +class SourceFixtureIsolationTests(unittest.TestCase): + """Ignored runtime state must not enter a source-only protocol fixture.""" + def test_ignored_runtime_and_python_cache_are_not_copied(self): + import subprocess + with tempfile.TemporaryDirectory() as td: + base = Path(td) + source = base / 'input' / 'formal' + source.mkdir(parents=True) + (source / '.gitignore').write_text('.lake/\n__pycache__/\n') + tracked = source / 'tracked-source.txt' + tracked.write_bytes(b'exact tracked source\n') + tracked.chmod(0o755) + ignored = ('.lake/packages/runtime-cache', '__pycache__/runtime.pyc') + for relative in ignored: + path = source / relative + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(b'ignored runtime sentinel\n') + subprocess.run(['git', '-C', str(source.parent), 'init', '-q'], + check=True, capture_output=True) + subprocess.run(['git', '-C', str(source.parent), 'add', 'formal'], + check=True, capture_output=True) + for relative in ignored: + subprocess.run(['git', '-C', str(source.parent), 'check-ignore', + 'formal/' + relative], check=True, capture_output=True) + copied = base / 'copied-formal' + copy_formal_fixture(source, copied) + for relative in ignored: + with self.subTest(relative=relative): + self.assertFalse((copied / relative).exists(), + 'ignored runtime cache entered the source fixture') + self.assertEqual((copied / tracked.name).read_bytes(), tracked.read_bytes()) + self.assertEqual((copied / tracked.name).stat().st_mode & 0o777, + tracked.stat().st_mode & 0o777) + + def test_actual_tracked_formal_tree_bytes_and_modes_preserved(self): + import subprocess + original = SIDE.parents[1] + def git(root, *args): + return subprocess.check_output(['git', '-C', str(root), *args], text=True).strip() + with tempfile.TemporaryDirectory() as td: + base = Path(td) + copied = base / 'formal' + copy_formal_fixture(original / 'formal', copied) + git(base, 'init', '-q') + git(base, 'add', 'formal') + tree = git(base, 'write-tree') + self.assertEqual(git(base, 'rev-parse', tree + ':formal'), + git(original, 'rev-parse', 'HEAD:formal')) + for relative in git(original, 'ls-files', '--', 'formal').splitlines(): + source = original / relative + target = base / relative + with self.subTest(path=relative): + self.assertEqual(target.read_bytes(), source.read_bytes()) + self.assertEqual(target.stat().st_mode & 0o777, + source.stat().st_mode & 0o777) + + +class CoreIdentityProtocolTests(unittest.TestCase): + """Source/receipt protocol fixtures only; no Lean or finite-law execution.""" + def setUp(self): + import shutil + import subprocess + from unittest import mock + self._subprocess = subprocess + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name).resolve() + original = SIDE.parents[1] + copy_formal_fixture(original / 'formal', self.root / 'formal') + for package in ('d2_moment_bridge', 'd2_square_schur', 'd2_atom_integral'): + relative = Path('companions') / (package + '_20261006') + shutil.copytree(original / relative, self.root / relative) + workflow = Path('.github/workflows') / (package.replace('_', '-') + '.yml') + (self.root / workflow).parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(original / workflow, self.root / workflow) + (self.root / 'tools').mkdir() + shutil.copy2(original / 'tools/required_formal_check.py', + self.root / 'tools/required_formal_check.py') + for args in (('init', '-q'), ('add', '.'), + ('-c', 'user.name=protocol-fixture', + '-c', 'user.email=protocol@example.invalid', + 'commit', '-qm', 'copied exact source protocol fixture')): + subprocess.run(['git', '-C', str(self.root), *args], + check=True, capture_output=True) + self.head = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD'], text=True).strip() + actual_tree = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD:formal'], + text=True).strip() + self.assertEqual(actual_tree, '8922fd8c833df0c52d4a8c7b5c3ad802b93098d4') + self.context = {'checked_commit': self.head} + patch = mock.patch.dict('os.environ', {'GITHUB_ACTIONS': 'false'}) + patch.start() + self.addCleanup(patch.stop) + copied = self.root / 'companions' / SIDE.name / 'check.py' + spec = importlib.util.spec_from_file_location('copied_d2_protocol', copied) + self.c = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.c) + + def validator(self): + function = getattr(self.c, 'validate_core_receipt', None) + self.assertTrue(callable(function), 'production core receipt validator missing') + return function + + def good_receipt(self): + return {'checked_commit': self.head, + 'manifest_sha256': '481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066', + 'formalization_status': 'kernel-checked'} + + def test_source_accepts_exact_reviewed_core_without_lean(self): + try: + current = self.c.source() + except (ValueError, self._subprocess.CalledProcessError) as error: + self.fail('reviewed frozen source cut must bind: ' + str(error)) + self.assertEqual(current['checked_commit'], self.head) + self.assertIn('tools/required_formal_check.py', current['sources']) + + def test_actual_producer_to_receipt_validator(self): + producer_path = self.root / 'formal/gate.py' + spec = importlib.util.spec_from_file_location('copied_rf312_producer', producer_path) + producer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(producer) + _, digest = producer.source_check() + self.assertEqual(digest, self.good_receipt()['manifest_sha256']) + self.validator()( + {'checked_commit': self.head, 'manifest_sha256': digest, + 'formalization_status': 'kernel-checked'}, self.context) + + def test_raw_digest_wrong_commit_and_non_kernel_receipts_refuse(self): + validate = self.validator() + raw = self.c.sha((self.root / 'formal/manifest.json').read_bytes()) + for key, value in (('manifest_sha256', raw), + ('checked_commit', '0' * 40), + ('formalization_status', 'source')): + with self.subTest(key=key): + bad = dict(self.good_receipt(), **{key: value}) + with self.assertRaises(ValueError): + validate(bad, self.context) + + def test_helper_drift_refuses_before_evaluating_changed_code(self): + helper = self.root / 'tools/required_formal_check.py' + helper.write_bytes(helper.read_bytes() + + b"\nraise RuntimeError('untrusted helper evaluated')\n") + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_helper_symlink_and_absence_refuse(self): + helper = self.root / 'tools/required_formal_check.py' + raw = helper.read_bytes() + helper.unlink() + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + outside = self.root / 'outside-validator.py' + outside.write_bytes(raw) + helper.symlink_to(outside) + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_manifest_overlay_and_core_file_drift_refuse(self): + changes = (('formal/manifest.json', b'\n'), + ('formal/manifest.overlay.json', b'\n'), + ('formal/ResearchFormalCoreR1/AlgebraV2.lean', b'\n')) + for relative, suffix in changes: + with self.subTest(path=relative): + path = self.root / relative + raw = path.read_bytes() + path.write_bytes(raw + suffix) + try: + with self.assertRaises((ValueError, self._subprocess.CalledProcessError)): + self.c.source() + finally: + path.write_bytes(raw) + + def test_missing_or_unknown_overlay_regime_never_downgrades(self): + validate = self.validator() + overlay = self.root / 'formal/manifest.overlay.json' + original = overlay.read_bytes() + overlay.unlink() + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(b'{"schema_version":2,"files":{}}') + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(original) + manifest = self.root / 'formal/manifest.json' + raw = manifest.read_bytes() + document = self.c.strict(raw) + document.pop('source_identity') + manifest.write_text(__import__('json').dumps(document)) + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + + + if __name__=='__main__': unittest.main(verbosity=2) diff --git a/companions/d2_square_schur_20261006/SCOPE.md b/companions/d2_square_schur_20261006/SCOPE.md index 284ff4057..b718ddc31 100644 --- a/companions/d2_square_schur_20261006/SCOPE.md +++ b/companions/d2_square_schur_20261006/SCOPE.md @@ -151,3 +151,27 @@ bytes. The new tests are synthetic and do not execute Lean. New current-commit kernel receipts and hosted checks are still required after publication. Alignment remains PENDING_INDEPENDENT_REVIEW; scientific effect NONE. + +## RF312 source/receipt engineering proposal, 28 October 2026 + +This dated private proposal preserves the mathematical text and historical evidence above. +Its source basis is RF312 `80946e1cf311b3cbbb051bb3662357b11f8b3d75`, formal tree +`8922fd8c833df0c52d4a8c7b5c3ad802b93098d4`, with the unchanged nine formal Lean/root +blobs, 63 target entries, source modules, dependencies, toolchain and companion Lean/contract bytes. +These are source identities and declared dependencies, not a fresh proof or applicability review. + +The raw manifest SHA256 is `ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062`; +the core receipt instead binds composite source `481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066`. +The fixed strict RF312 overlay contract must match; no raw-receipt fallback is admitted. +The reused identity validator lies outside the formal tree, at `tools/required_formal_check.py` +(blob `0b9d694bdf888c75826ca07ae176c5a5c43b8880`, SHA256 +`6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc`). Its source bytes are +checked before those verified bytes are evaluated; drift, symlink, missing overlay and wrong regimes refuse. +Its identity is also retained in the source snapshot across execution. Atom's two imported companion +Lean pins and all existing runtime re-observation checks are preserved. + +Protocol unit fixtures are synthetic and execute no Lean or finite-law diagnostic. They do not +supply a core or companion kernel/runtime receipt. Existing receipts/reviews remain historical; +fresh actual current-composition core and all three D2 hosted/negative-control/runtime checks, +qualified review and separate integration remain required. Scientific effect NONE; alignment and +scientific acceptance are unchanged. No existing312 source/ref or integration custody follows. diff --git a/companions/d2_square_schur_20261006/SOURCE_FILES.json b/companions/d2_square_schur_20261006/SOURCE_FILES.json index 265c35176..c9e626968 100644 --- a/companions/d2_square_schur_20261006/SOURCE_FILES.json +++ b/companions/d2_square_schur_20261006/SOURCE_FILES.json @@ -1,5 +1,5 @@ { - "core_tree": "fc0b11706d064b9de42331ee0a2464865107b87b", + "core_tree": "8922fd8c833df0c52d4a8c7b5c3ad802b93098d4", "files": { ".github/workflows/d2-square-schur.yml": { "bytes": 1650, @@ -17,14 +17,14 @@ "sha256": "e0f9560e6f129216cd989cea3cdf97254972ca9b1cae7bab57df664329ae78fa" }, "companions/d2_square_schur_20261006/SCOPE.md": { - "bytes": 9354, - "git_blob": "284ff4057933a7106d92784b4328bde5adbae1d4", - "sha256": "d0ed0e8665e601407afe00b7293c2fdbae0ac22bc22ed8fc06a3ee7e2a1a98dd" + "bytes": 11180, + "git_blob": "b718ddc31d7725c3ac576e1cb1cdc2430247baa1", + "sha256": "794d2fe362e8c28551af066820ae7ea1461658d7072052c7739add0284de9aec" }, "companions/d2_square_schur_20261006/check.py": { - "bytes": 9803, - "git_blob": "3aea440c6cb1b2ce3f193d36b2058590da816a4c", - "sha256": "73726f63407ee4b612caa7c101d35cf0e285ebc55cc11872a1bc24c75799daf3" + "bytes": 11654, + "git_blob": "5f57381b27c995e98c0d34147a465358b6e5bcc4", + "sha256": "1865267548687f0e1c86f11d9a5311dc47ccff9e3db2aa0e205aa17411c1a131" }, "companions/d2_square_schur_20261006/replay.sh": { "bytes": 3071, @@ -32,9 +32,9 @@ "sha256": "bad86f8be8df812ceb0a13cb7d0dba7e0f3ade11a4525ec5aee9660bbf3e5067" }, "companions/d2_square_schur_20261006/test_check.py": { - "bytes": 7582, - "git_blob": "e058c4548aca3d434d795f012e971342eb0f00ca", - "sha256": "57dfd8f8b8b51a74a9f3ea036bc6d6fb536a920052c399281945319285bb83c4" + "bytes": 17685, + "git_blob": "d1f8b60d86783bed80a20c8d553e36d168d7972c", + "sha256": "7508a7032f5b63a51bd24d2ea1eb85c026e750aeef70900f45f7a0874e7b75be" } }, "scientific_effect": "NONE", diff --git a/companions/d2_square_schur_20261006/check.py b/companions/d2_square_schur_20261006/check.py index 3aea440c6..5f57381b2 100644 --- a/companions/d2_square_schur_20261006/check.py +++ b/companions/d2_square_schur_20261006/check.py @@ -18,9 +18,14 @@ PACKAGE='companions/d2_square_schur_20261006' WORKFLOW='.github/workflows/d2-square-schur.yml' REPO='d6g8k5htny-coder/Math-' -CORE_TREE='fc0b11706d064b9de42331ee0a2464865107b87b' -CORE_MANIFEST='7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778' -CORE_GATE='25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a' +CORE_TREE='8922fd8c833df0c52d4a8c7b5c3ad802b93098d4' +CORE_MANIFEST='ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062' +CORE_GATE='509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731' + +CORE_SOURCE_IDENTITY='481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066' +CORE_IDENTITY_PATH='tools/required_formal_check.py' +CORE_IDENTITY_SHA256='6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc' +CORE_IDENTITY_BLOB='0b9d694bdf888c75826ca07ae176c5a5c43b8880' TARGETS=tuple('D2SquareSchur.'+n for n in ('weighted_square_identity','weighted_square_lower', 'schur_no_upper','schur_from_lower_inputs')) CONTROLS=('RejectSignedWeights','RejectEndpointMaximum','RejectOutsideDirection') @@ -49,6 +54,38 @@ def git(*args): def metadata():return strict((SIDE/'SOURCE_FILES.json').read_bytes()) +def core_identity(): + """Bind the outside-tree validator before evaluating its verified bytes.""" + path = ROOT / CORE_IDENTITY_PATH + require(not any(p.is_symlink() for p in (path, *path.parents)) and path.is_file(), + 'core identity validator missing or symlink') + raw = path.read_bytes() + framed = b'blob ' + str(len(raw)).encode() + b'\0' + raw + require(sha(raw) == CORE_IDENTITY_SHA256 + and hashlib.sha1(framed).hexdigest() == CORE_IDENTITY_BLOB, + 'core identity validator changed') + namespace = {'__name__': 'bound_d2_core_identity', '__file__': str(path)} + exec(compile(raw, str(path), 'exec'), namespace) + manifest = ROOT / 'formal/manifest.json' + manifest_raw = manifest.read_bytes() + require(sha(manifest_raw) == CORE_MANIFEST, 'core manifest changed') + digest = namespace['manifest_identity'](manifest, manifest_raw) + require(digest == CORE_SOURCE_IDENTITY, 'core source identity changed') + return digest + + +def validate_core_receipt(core, current): + """The current core receipt binds the composite source, not the raw manifest.""" + require(isinstance(core, dict), 'invalid core receipt') + require(core.get('checked_commit') == current['checked_commit'], + 'core executed different source') + require(core.get('manifest_sha256') == core_identity(), 'core receipt manifest') + require(core.get('formalization_status') == 'kernel-checked', 'no core kernel receipt') + + + + + def source(): meta=metadata();head=git('rev-parse','HEAD') require(set(meta)=={'version','scientific_effect','core_tree','targets','files'},'manifest schema') @@ -59,6 +96,7 @@ def source(): require(git('rev-parse',head+':formal')==CORE_TREE,'core tree changed') require(sha((ROOT/'formal/manifest.json').read_bytes())==CORE_MANIFEST,'core manifest changed') require(sha((ROOT/'formal/gate.py').read_bytes())==CORE_GATE,'core verifier changed') + core_identity() if os.environ.get('GITHUB_ACTIONS')=='true': require(os.environ.get('GITHUB_SHA')==head and os.environ.get('GITHUB_REPOSITORY')==REPO,'host/source mismatch') require(os.environ.get('GITHUB_RUN_ID') and os.environ.get('GITHUB_RUN_ATTEMPT'),'missing run identity') @@ -72,7 +110,10 @@ def source(): ids[name]=identity(path.read_bytes()) require(git('rev-parse',head+':'+name)==ids[name]['git_blob'],'dirty source: '+name) if name in PAYLOADS:require(meta['files'][name]==ids[name],'source identity: '+name) - git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW) + helper_id=identity((ROOT/CORE_IDENTITY_PATH).read_bytes()) + require(git('rev-parse',head+':'+CORE_IDENTITY_PATH)==helper_id['git_blob'],'dirty core identity validator') + ids[CORE_IDENTITY_PATH]=helper_id + git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW,CORE_IDENTITY_PATH) return {'checked_commit':head,'repository':REPO,'run_id':os.environ.get('GITHUB_RUN_ID','local'), 'run_attempt':os.environ.get('GITHUB_RUN_ATTEMPT','local'),'core_tree':CORE_TREE, 'sources':ids,'declarations':list(TARGETS),'scientific_effect':'NONE'} @@ -147,8 +188,7 @@ def finish(out): require((out/(label+'.status')).read_bytes()==b'1\n','negative status: '+label) negative((out/(label+'.log')).read_text(),label,1) raw=(ROOT/'formal/.lake/formal-evidence/receipt.json').read_bytes();core=strict(raw) - require(core['checked_commit']==current['checked_commit'] and core['manifest_sha256']==CORE_MANIFEST,'core identity') - require(core['formalization_status']=='kernel-checked','no core kernel receipt') + validate_core_receipt(core,current) final=final_runtime(out,core,strict((ROOT/'formal/manifest.json').read_bytes())['dependency_revisions']) result={**current,'axioms':ax,'theorem_count':4,'definition_count':0,'core_receipt_sha256':sha(raw),'final_observation':final, 'formalization_status':'kernel-checked','alignment_status':'PENDING_INDEPENDENT_REVIEW', diff --git a/companions/d2_square_schur_20261006/test_check.py b/companions/d2_square_schur_20261006/test_check.py index e058c4548..d1f8b60d8 100644 --- a/companions/d2_square_schur_20261006/test_check.py +++ b/companions/d2_square_schur_20261006/test_check.py @@ -136,4 +136,205 @@ def test_replay_observes_after_the_last_lean_run_and_finish_requires_it(self): source=(SIDE/'check.py').read_text();body=source[source.index('def finish(out):'):source.index('def main(')] self.assertIn('final_runtime(out,',body) +def copy_formal_fixture(source, destination): + """Copy formal inputs for the actual protocol fixture; never execute Lean.""" + import shutil + return shutil.copytree(source, destination, + ignore=shutil.ignore_patterns('.lake', '__pycache__')) + + +class SourceFixtureIsolationTests(unittest.TestCase): + """Ignored runtime state must not enter a source-only protocol fixture.""" + def test_ignored_runtime_and_python_cache_are_not_copied(self): + import subprocess + with tempfile.TemporaryDirectory() as td: + base = Path(td) + source = base / 'input' / 'formal' + source.mkdir(parents=True) + (source / '.gitignore').write_text('.lake/\n__pycache__/\n') + tracked = source / 'tracked-source.txt' + tracked.write_bytes(b'exact tracked source\n') + tracked.chmod(0o755) + ignored = ('.lake/packages/runtime-cache', '__pycache__/runtime.pyc') + for relative in ignored: + path = source / relative + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(b'ignored runtime sentinel\n') + subprocess.run(['git', '-C', str(source.parent), 'init', '-q'], + check=True, capture_output=True) + subprocess.run(['git', '-C', str(source.parent), 'add', 'formal'], + check=True, capture_output=True) + for relative in ignored: + subprocess.run(['git', '-C', str(source.parent), 'check-ignore', + 'formal/' + relative], check=True, capture_output=True) + copied = base / 'copied-formal' + copy_formal_fixture(source, copied) + for relative in ignored: + with self.subTest(relative=relative): + self.assertFalse((copied / relative).exists(), + 'ignored runtime cache entered the source fixture') + self.assertEqual((copied / tracked.name).read_bytes(), tracked.read_bytes()) + self.assertEqual((copied / tracked.name).stat().st_mode & 0o777, + tracked.stat().st_mode & 0o777) + + def test_actual_tracked_formal_tree_bytes_and_modes_preserved(self): + import subprocess + original = SIDE.parents[1] + def git(root, *args): + return subprocess.check_output(['git', '-C', str(root), *args], text=True).strip() + with tempfile.TemporaryDirectory() as td: + base = Path(td) + copied = base / 'formal' + copy_formal_fixture(original / 'formal', copied) + git(base, 'init', '-q') + git(base, 'add', 'formal') + tree = git(base, 'write-tree') + self.assertEqual(git(base, 'rev-parse', tree + ':formal'), + git(original, 'rev-parse', 'HEAD:formal')) + for relative in git(original, 'ls-files', '--', 'formal').splitlines(): + source = original / relative + target = base / relative + with self.subTest(path=relative): + self.assertEqual(target.read_bytes(), source.read_bytes()) + self.assertEqual(target.stat().st_mode & 0o777, + source.stat().st_mode & 0o777) + + +class CoreIdentityProtocolTests(unittest.TestCase): + """Source/receipt protocol fixtures only; no Lean or finite-law execution.""" + def setUp(self): + import shutil + import subprocess + from unittest import mock + self._subprocess = subprocess + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name).resolve() + original = SIDE.parents[1] + copy_formal_fixture(original / 'formal', self.root / 'formal') + for package in ('d2_moment_bridge', 'd2_square_schur', 'd2_atom_integral'): + relative = Path('companions') / (package + '_20261006') + shutil.copytree(original / relative, self.root / relative) + workflow = Path('.github/workflows') / (package.replace('_', '-') + '.yml') + (self.root / workflow).parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(original / workflow, self.root / workflow) + (self.root / 'tools').mkdir() + shutil.copy2(original / 'tools/required_formal_check.py', + self.root / 'tools/required_formal_check.py') + for args in (('init', '-q'), ('add', '.'), + ('-c', 'user.name=protocol-fixture', + '-c', 'user.email=protocol@example.invalid', + 'commit', '-qm', 'copied exact source protocol fixture')): + subprocess.run(['git', '-C', str(self.root), *args], + check=True, capture_output=True) + self.head = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD'], text=True).strip() + actual_tree = subprocess.check_output( + ['git', '-C', str(self.root), 'rev-parse', 'HEAD:formal'], + text=True).strip() + self.assertEqual(actual_tree, '8922fd8c833df0c52d4a8c7b5c3ad802b93098d4') + self.context = {'checked_commit': self.head} + patch = mock.patch.dict('os.environ', {'GITHUB_ACTIONS': 'false'}) + patch.start() + self.addCleanup(patch.stop) + copied = self.root / 'companions' / SIDE.name / 'check.py' + spec = importlib.util.spec_from_file_location('copied_d2_protocol', copied) + self.c = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.c) + + def validator(self): + function = getattr(self.c, 'validate_core_receipt', None) + self.assertTrue(callable(function), 'production core receipt validator missing') + return function + + def good_receipt(self): + return {'checked_commit': self.head, + 'manifest_sha256': '481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066', + 'formalization_status': 'kernel-checked'} + + def test_source_accepts_exact_reviewed_core_without_lean(self): + try: + current = self.c.source() + except (ValueError, self._subprocess.CalledProcessError) as error: + self.fail('reviewed frozen source cut must bind: ' + str(error)) + self.assertEqual(current['checked_commit'], self.head) + self.assertIn('tools/required_formal_check.py', current['sources']) + + def test_actual_producer_to_receipt_validator(self): + producer_path = self.root / 'formal/gate.py' + spec = importlib.util.spec_from_file_location('copied_rf312_producer', producer_path) + producer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(producer) + _, digest = producer.source_check() + self.assertEqual(digest, self.good_receipt()['manifest_sha256']) + self.validator()( + {'checked_commit': self.head, 'manifest_sha256': digest, + 'formalization_status': 'kernel-checked'}, self.context) + + def test_raw_digest_wrong_commit_and_non_kernel_receipts_refuse(self): + validate = self.validator() + raw = self.c.sha((self.root / 'formal/manifest.json').read_bytes()) + for key, value in (('manifest_sha256', raw), + ('checked_commit', '0' * 40), + ('formalization_status', 'source')): + with self.subTest(key=key): + bad = dict(self.good_receipt(), **{key: value}) + with self.assertRaises(ValueError): + validate(bad, self.context) + + def test_helper_drift_refuses_before_evaluating_changed_code(self): + helper = self.root / 'tools/required_formal_check.py' + helper.write_bytes(helper.read_bytes() + + b"\nraise RuntimeError('untrusted helper evaluated')\n") + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_helper_symlink_and_absence_refuse(self): + helper = self.root / 'tools/required_formal_check.py' + raw = helper.read_bytes() + helper.unlink() + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + outside = self.root / 'outside-validator.py' + outside.write_bytes(raw) + helper.symlink_to(outside) + with self.assertRaisesRegex(ValueError, 'identity validator'): + self.c.source() + + def test_manifest_overlay_and_core_file_drift_refuse(self): + changes = (('formal/manifest.json', b'\n'), + ('formal/manifest.overlay.json', b'\n'), + ('formal/ResearchFormalCoreR1/AlgebraV2.lean', b'\n')) + for relative, suffix in changes: + with self.subTest(path=relative): + path = self.root / relative + raw = path.read_bytes() + path.write_bytes(raw + suffix) + try: + with self.assertRaises((ValueError, self._subprocess.CalledProcessError)): + self.c.source() + finally: + path.write_bytes(raw) + + def test_missing_or_unknown_overlay_regime_never_downgrades(self): + validate = self.validator() + overlay = self.root / 'formal/manifest.overlay.json' + original = overlay.read_bytes() + overlay.unlink() + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(b'{"schema_version":2,"files":{}}') + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + overlay.write_bytes(original) + manifest = self.root / 'formal/manifest.json' + raw = manifest.read_bytes() + document = self.c.strict(raw) + document.pop('source_identity') + manifest.write_text(__import__('json').dumps(document)) + with self.assertRaises(ValueError): + validate(self.good_receipt(), self.context) + + + if __name__=='__main__':unittest.main(verbosity=2) diff --git a/docs/superpowers/plans/2026-10-28-d2-atom-ci-budget.md b/docs/superpowers/plans/2026-10-28-d2-atom-ci-budget.md new file mode 100644 index 000000000..57651c5ff --- /dev/null +++ b/docs/superpowers/plans/2026-10-28-d2-atom-ci-budget.md @@ -0,0 +1,35 @@ +# Bounded Atom CI allocation + +Actual source author `/root/d2_dependency_preflight`, pickup Math-#312/6472861682 +after Root6472823629 and actual R3 integration release6472677571. Immutable input +d88e4820fcec94b91f6b92ffaccf28c0b0815aff. NEW CP15:35/hard16:00UTC28October2026 +or invocation end; previous source/private assignments remain closed. + +The current Atom repository suites took815.619+844.204seconds (27m39.823). +Observed setup/cache and other unit stages leave roughly23seconds of its30min +job for fresh Core and mandatory Atom dependencies/proofs/contracts/axioms/types, +fresh rechecker, negatives, final runtime/dependencies and receipt. A Core child +already permits900seconds. Forty-five minutes leaves about15min for all of those +remaining stages and jitter; no completed Atom duration establishes adequacy. +The reviewed bounded allocation is60min, matching existing Square60 while Atom +also builds two dependencies. This is no completion guarantee. Old cancellation +actor/reason remain UNKNOWN; its original result is not relabelled timeout/PASS. + +1. Change only Atom job timeout30→60. Keep Square and every action, trigger, + permission, command, test, kernel/control and acceptance requirement exact. +2. In a committed temporary Git/source fixture, actual production source() + must reject new workflow bytes with the OLD manifest workflow identity. +3. Update only that workflow's exact byte/SHA256/Gitblob record in Atom's + SOURCE_FILES. Actual source() and inspected metadata-only protocol checks + must pass normally/optimized. No mirrored timeout test is needed. +4. Audit the complete three-path delta, unchanged fields/proofs/Corepins and + consumed sources. Obtain fresh nonauthor engineering/workflow review under + existing SectionC authority, then at most one guarded expected-oldd88 source + fast-forward, native readbacks, final disposition and only-own release. + +Owned paths: Atom workflow, Atom SOURCE_FILES, this plan. No authentic C6/PTY, +mathematics/Lean/kernel/full replay/full suite/new environment/executor/CIrequest, +dispatch/rerun/cancel/settings or denied-route retry. Any actual operation or +owner/capability stop still controls. Old cancelled receipts keep their source; +new-source hosted/Ready/protected integration is a separate successor stage. +Scientific effect NONE; source-exposed/same-family/org0, no future seat. diff --git a/docs/superpowers/plans/2026-10-28-d2-composite-receipt-consumers.md b/docs/superpowers/plans/2026-10-28-d2-composite-receipt-consumers.md new file mode 100644 index 000000000..152075dda --- /dev/null +++ b/docs/superpowers/plans/2026-10-28-d2-composite-receipt-consumers.md @@ -0,0 +1,43 @@ +# D2 composite receipt consumers implementation plan + +> **For agentic workers:** Use superpowers:executing-plans for this single coordinated source task and one fresh whole-branch engineering/security review. + +**Goal:** Make the three existing D2 source/receipt consumers accept the explicitly qualified RF312 source cut and its composite receipt identity while refusing drift and downgrade. + +**Architecture:** Keep raw manifest, formal tree and gate pins distinct from the composite receipt digest. Each checker validates the exact outside-tree `manifest_identity` helper bytes before evaluating those verified bytes, then calls that actual helper. A cohesive `validate_core_receipt(core,current)` used by `finish` checks current source, the composite identity and kernel-status label. Existing source snapshots additionally bind the helper. + +**Tech Stack:** Python standard library, Git metadata and temporary protocol fixtures only. + +**Spec:** [Private proposal pickup](https://github.com/d6g8k5htny-coder/Math-/pull/312#issuecomment-6468894513). Source basis `80946e1cf311b3cbbb051bb3662357b11f8b3d75`; parent four-path source owner retains custody. This private proposal grants no existing312 ref/body/Ready/integration seat. + +## Global constraints + +- Formal tree `8922fd8c833df0c52d4a8c7b5c3ad802b93098d4`; raw manifest SHA256 `ba7d11e43574e39da3c759e0501399a6dcd1b7da32b157a4a6b01f5c133b3062`; gate SHA256 `509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731`. +- Composite receipt identity `481653d73d00f64bf06fefbf24be994f60ebe5c54f826abf899461f6e6937066`. +- Outside-tree validator: `tools/required_formal_check.py`, blob `0b9d694bdf888c75826ca07ae176c5a5c43b8880`, SHA256 `6c27355237b45d3999298522c141984ff5b7c114f18b3c555cc45989976fc6dc`. +- Preserve all formal and companion Lean/contract/import/target/toolchain/dependency/workflow bytes, source scientific dispositions and historical evidence. No original receipt is rebound. +- No finite-law diagnostics, actual mathematics, Lean/kernel, full gate/replay or CI run. Only targeted protocol classes in normal and optimized modes. +- Initial implementation remains private. Existing312 branch publication requires a later actual source-owner handoff and fresh state reconciliation. + +## Review focus + +- Loading an unbound helper outside the formal tree must refuse before evaluating its bytes; symlinks or drift cannot become trusted code. +- A valid composite receipt passes; the raw digest, wrong commit or wrong kernel-status label refuses. +- Manifest, overlay, core tree and helper mutations refuse without a legacy fallback. +- Atom's two unchanged imported companion Lean pins and the existing runtime re-observation controls remain intact. +- New SOURCE_FILES hashes describe actual new code/tests/documentation while all mathematical payload bytes and earlier evidence remain exact. + +## Task1: Update the three consumers + +**Files:** Each companion's `check.py`, existing test file, `SOURCE_FILES.json` and README/SCOPE, plus this plan (13 paths). Moment test file is `test_bridge.py`; square and atom use `test_check.py`. + +**Interfaces:** Reuse `manifest_identity(manifest: Path, raw: bytes) -> str`. Add each checker's `core_identity() -> str` and `validate_core_receipt(core: dict, current: dict) -> None`; `source` and `finish` must use them. + +- [ ] Run the unchanged three `FinalRuntimeTests` classes in normal and optimized modes. Expected21 methods per mode PASS. +- [ ] Add targeted `CoreIdentityProtocolTests`: actual `source()` on a temporary Git copy, actual producer `source_check` plus actual receipt validator, raw-digest/wrong-commit/non-kernel refusal, and helper/manifest/overlay/symlink drift refusal. Run those classes before production edits; expect missing source-cut/receipt support failures. +- [ ] Add the fixed source pins and bound-helper path. Validate helper symlink/hash/blob before evaluating the verified byte string, call actual `manifest_identity`, and require the exact composite digest. Have `source` include the helper's current Git/blob identity and have `finish` call the production receipt validator. +- [ ] Append dated engineering source-cut qualifications without rewriting old mathematical/historical text; regenerate only existing SOURCE_FILES core_tree and changed payload identities. +- [ ] Run the new targeted protocol classes and existing FinalRuntimeTests in both modes; require all PASS. Check whitespace and exact source preservation, including all9 formal Lean blobs and5 companion Lean/contract blobs. +- [ ] Commit one private candidate, obtain fresh distinct whole-branch engineering/security review, and deliver exact parent/head/tree/paths/logs. No publication to the existing312 ref or integration is implied. + +Protocol fixtures may use synthetic receipts and Git commits; they are never hosted or kernel evidence. No same-family scientific review or status promotion is claimed. diff --git a/docs/superpowers/plans/2026-10-28-d2-hosted-source-fixtures.md b/docs/superpowers/plans/2026-10-28-d2-hosted-source-fixtures.md new file mode 100644 index 000000000..a2b66daa3 --- /dev/null +++ b/docs/superpowers/plans/2026-10-28-d2-hosted-source-fixtures.md @@ -0,0 +1,43 @@ +# D2 source-only protocol fixtures + +Actual private proposal author: OpenAI/Codex `/root/d2_dependency_preflight`. +Claim Math-#312/6469891555, narrowed before edits by #312/6470070201. +Input local949d/tree776f is byte-identical to nativeb0ac. Existing integrator +retains source/ref/Ready/base/Main custody; this plan grants no publication role. + +## Defect and evidence boundary + +All three protocol test setups copy the entire formal directory after hosted +workflows install the dependency cache. Seven methods in each of two modes make +fourteen full-directory copies per replay. The source-only author checkout did +not contain that cache. Existing formal fixtures exclude `.lake` and +`__pycache__`; the companion fixtures must use the same bounded source boundary. + +This is an independently demonstrated fixture defect. The original fresh moment +and square hosted error remains UNKNOWN: approved job-log reads returned +Transport closed without trace bytes. No causal attribution or CI rerun follows +from this proposal. The actual bound API exports the required methods; no +speculative API or production change is justified. + +## Bounded implementation + +1. Extract the current unfiltered formal copy into the actual helper called by + each real protocol setup. Add an isolated ignored-cache sentinel regression; + run it before filtering to retain meaningful assertion RED, not missing API. +2. Give that helper the canonical `.lake`/`__pycache__` exclusions. Test that its + copied tracked formal Git tree, physical bytes and file modes remain exact. +3. Update only the three test identities in SOURCE_FILES. Run the targeted + protocol/runtime and new fixture-isolation classes normally and optimized; + no finite-law class, Lean/kernel/math/full gate/replay/hosted rerun. +4. Audit the exact seven-path scope, unchanged production and all mathematical, + dependency, workflow, source identity and historical records. Obtain a fresh + separate whole-candidate engineering review. Native publication, if later + selected, requires actual custody handoff and fresh reconciliation. + +Writable paths: three companion test files, their three SOURCE_FILES documents, +and this plan only. No checker, formal/helper, identity/pin, proof/contract, +target/import/lock/toolchain, README/SCOPE or workflow changes. No old receipt or +review is rebound. Source-exposed/same-family/org0/scienceNONE. + +Checkpoint13:30; hard14:00UTC28October2026 or invocation end. Preserve all scoped +access denials and actual integrator custody; release only the author's own stage. diff --git a/docs/superpowers/plans/2026-10-28-legacy-json-pipe-context.md b/docs/superpowers/plans/2026-10-28-legacy-json-pipe-context.md new file mode 100644 index 000000000..6b2f8a866 --- /dev/null +++ b/docs/superpowers/plans/2026-10-28-legacy-json-pipe-context.md @@ -0,0 +1,33 @@ +# Legacy diagnostic reference pipe context + +Actual author: OpenAI/Codex `/root/d2_dependency_preflight`, new source pickup +Math-#312/6471431957 after Root6471374057 and actual integrator release6471237285. +Input825905cd5cb63fb288aa79ac4baefb14ff0cd9b9/treea0be18b5; CP14:35/hard15:00UTC +28October2026 or invocation end. This is a new stage, not an old lease extension. + +Current square/atom original logs contain38 plain-vs-ANSI diagnostic differences +each. Explicit repository-wide discovery intentionally reaches these tests; +recorded standard-library paths identify Python3.14, not an exact patch/binary. +The reference already models child pipe width, but leaves parent stdout attached +to a TTY while constructing/parsing argparse. Modern argparse may select color +from stdout; the actual captured child's stdout is non-TTY. Old unavailable +b0/3bab failure causes stay UNKNOWN, and all old failures keep their source/run. + +1. Add isolated stdlib-only tests. Observe the actual real ArgumentParser and + HelpFormatter under a synthetic parent stdout whose isatty is true; original + helper must fail the captured-child non-TTY boundary before production edits. +2. Capture reference stdout during BOTH parser construction and parsing, + alongside existing stderr capture. Retain choices, widths, exact bytes and + inherited color environment; no ANSI stripping, forced-color or Python policy. +3. Run only the new harmless methods normally/optimized. Verify real standard + captured-parser bytes, stream restoration and unchanged environment controls. + No authentic C6/PTY/spawn/_contract/replay/math/Lean/CI/held-target execution. +4. Audit three-path scope and unchanged helper code outside that reference, + contracts, original tests, proofs, workflows and source identities. Fresh + separate whole-candidate engineering review precedes one expected-old8259, + forcefalse source amendment with native readbacks and own source release. + +Owned files: tools/legacy_json_replay.py, the new isolated test file and this plan. +This is an explicit reference-instrument correction with a new source/evaluation +identity, not a retroactive pass. Fresh current Core/all-D2 and applicable hosted, +Ready/protected integration remain separate. Scientific effect NONE; org0. diff --git a/docs/superpowers/plans/2026-10-28-rf312-receipt-binding.md b/docs/superpowers/plans/2026-10-28-rf312-receipt-binding.md new file mode 100644 index 000000000..bf0113c80 --- /dev/null +++ b/docs/superpowers/plans/2026-10-28-rf312-receipt-binding.md @@ -0,0 +1,44 @@ +# RF312 receipt binding implementation plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:executing-plans for this single task, followed by one fresh whole-branch engineering review. + +**Goal:** Make the current required-check consumer bind the producer's exact base-manifest plus overlay identity while retaining explicitly non-overlay legacy behavior. + +**Architecture:** Add a fixed opt-in declaration to the base manifest. The consumer derives one identity from that declaration and the original bytes; it never accepts whichever of raw/composite happens to match. Preserve the producer, helper, overlay and every mathematical source byte. + +**Tech Stack:** Python standard library; existing unittest suites; no new dependency. + +**Spec:** [DCL-RF312-BIND-001](https://github.com/d6g8k5htny-coder/Math-/pull/312#pullrequestreview-5658582326), [current source reconciliation](https://github.com/d6g8k5htny-coder/Math-/pull/312#issuecomment-6467595927), and [actual new author pickup](https://github.com/d6g8k5htny-coder/Math-/pull/312#issuecomment-6468228926). + +## Global constraints + +- Base source head: `66d66e43e3f3f58835bc938717dacf8532aaffc3`; current Math Main `4a0d51bbd06f0d9ac731a1d1df38f25999797135` is a separate integration cut. +- Four paths only: this plan, `formal/manifest.json`, `tools/required_formal_check.py`, `tests/test_required_formal_check.py`. +- Exact declaration: `"source_identity": {"schema": "rf312-overlay-v1", "overlay": "manifest.overlay.json"}`. +- Declared mode hashes `manifest_bytes + b'\0RF312-OVERLAY\0' + overlay_bytes` exactly as the unchanged producer does. +- Legacy mode requires both declaration absence and reserved overlay absence; explicit null, unknown contracts and undeclared overlays refuse. +- Overlay must be the fixed regular non-symlink sibling and strict JSON with exactly `schema_version` (integer1) and `files` (string-to-lowercase-64hex bindings). +- Preserve checked commit/run/attempt, clean dependency locks, both runtime observations, receipt/log bytes and all existing acceptance predicates. +- No proof/Lean/source-target/producer/helper/overlay/workflow/status changes, no real Lean or kernel execution, no CI request, Ready or integration. Existing unit fixtures may invoke only copied-tree metadata CLI validation and synthetic runtime responders. +- Three D2 companion pin/raw-receipt holds remain separate and unchanged. Old reviews/receipts keep their original identities; predecessor closeouts remain UNKNOWN. + +## Review focus + +- Legacy raw receipts must remain valid only without any declaration or reserved overlay. +- Unknown/null/extra/path-changing identity declarations and duplicate/invalid JSON must refuse. +- Missing/dangling/symlink/directory overlays must refuse before reading any target. +- Raw/composite source drift and a raw-receipt downgrade must fail without rewriting the original receipt. +- The bridge regression must call the actual producer source-check and actual consumer; its runtime receipt remains an explicitly synthetic fixture, not kernel evidence. + +## Task1: Reconcile source identity at the receipt boundary + +**Files:** the four exact paths above. + +**Interfaces:** Keep `bind_receipt(receipt: Path, manifest: Path, env: dict, git_head: str) -> dict` unchanged. Add internal `manifest_identity(manifest: Path, raw: bytes) -> str`; reuse existing strict JSON validation, context checks and dependency-lock validation with the same captured base bytes. + +- [ ] Run clean existing consumer67 and formal244 unittest suites in normal and optimized modes. Expected: all pass. +- [ ] Add an actual-producer→fixture-receipt→consumer success test and direct malformed/downgrade/refusal controls. Run before production edits. Expected: the bridge fails with the original manifest/receipt mismatch and weak old-consumer cases are exposed. +- [ ] Add only the fixed declaration to the base manifest and implement strict identity selection in the consumer. No raw fallback in the overlay regime. +- [ ] Run the new consumer scope and both complete affected suites in normal and optimized modes. Expected: all existing/new methods pass; no real Lean, dependency/network or mathematical execution. +- [ ] Verify all old manifest fields and every non-owned source/overlay/helper/Lean/workflow byte remain exact; run whitespace validation and record the new raw/composite identity. +- [ ] Commit, obtain separate exact-tree engineering review, then publish at most one expected-old-head guarded fast-forward amendment to existing#312. Keep Draft and release only this source role. Fresh current-base/Ready/hosted qualification and integration remain separate. diff --git a/formal/DECLARATION_ADMISSION.md b/formal/DECLARATION_ADMISSION.md new file mode 100644 index 000000000..253469625 --- /dev/null +++ b/formal/DECLARATION_ADMISSION.md @@ -0,0 +1,13 @@ +# Package declaration admission hardening + +Scientific effect: **NONE**. Engineering successor for RF-GATE-01 (Math- issue #310), implemented by OpenAI / GPT-5.6 Sol in `round11-gate-hardening-20261005`. The #309 mathematical declarations are preserved. + +The predecessor used a column-zero theorem/lemma regex. Lean accepts declarations outside it, so declarations could compile outside manifest and axiom coverage. This successor intentionally enforces a conservative grammar rather than claiming to parse arbitrary Lean: one `namespace ResearchFormalCoreR1`; column-zero `theorem`, `lemma`, `def`, or `noncomputable def`; declaration-bearing alternatives and nested namespaces fail closed after comments and strings are removed. + +The manifest records all package declarations, not just theorem targets. Execute-time transitive-axiom auditing covers definitions as well as theorems; the historical target-only `axioms` receipt field is retained and `declaration_axioms` is additive. Lean4.34.1, dependency pins, leanchecker and all five existing negative controls are unchanged. + +Test-first predecessor `82f4de13f0e41253740d880f26fdc63fda772323` / run37394891831 failed with nine intended regression failures before Lean installation. A successor must pass those regressions, complete Python suites in both modes, source identity and the actual pinned Lean/leanchecker/axiom/type workflow. This is engineering evidence, not independent mathematical alignment or reviewer authentication. + +## Incorporated successor status + +The source-scanner design above is retained as historical test-first context. The incorporated production gate is the reviewed RF-GATE-01 compiled-environment inventory described in [`GATE_HARDENING.md`](GATE_HARDENING.md): the conservative source grammar remains a fail-closed pre-check, while admission completeness and package-wide axiom closure are decided from Lean's compiled environment. `gate_helper.py` preserves that reviewed implementation byte-for-byte; `gate.py` is the bound compatibility entrypoint that additionally retains current-main's exact Lean-release and clean-dependency observations. Neither layer changes mathematical statements or supplies independent alignment. diff --git a/formal/GATE_HARDENING.md b/formal/GATE_HARDENING.md new file mode 100644 index 000000000..9270c1ccb --- /dev/null +++ b/formal/GATE_HARDENING.md @@ -0,0 +1,235 @@ +# Gate hardening RF-GATE-01: environment inventory instead of a source scan + +Scientific effect: **NONE**. Dylan Roy, delegated AI work (Anthropic / Claude, Claude +Code session `session_015wNj8LPTKXsaT68G3DgPPh`). No Lean proof, manifest target, +`SCOPE.md` or status entry changes; `formalization_status` stays `proved` and +`alignment_status` stays `PENDING_INDEPENDENT_REVIEW`. + +## The gap + +Before this change `gate.py` built its target inventory by scanning the source modules +for lines beginning, at column 0, with `theorem` or `lemma`, and compared that list with +`manifest.json["targets"]`. Everything downstream (the `#print axioms` audit, the +elaborated-type dump, the Blueprint link check) ran on that list. A declaration the +scanner did not see was therefore never audited: + +- an indented `theorem`, a `private theorem`, a `protected theorem`, or a `@[simp] theorem` + on the same line; +- a `def`, `instance`, `opaque` or `abbrev` whose body uses `sorry` but is not a target; +- an `axiom` that no target mentions; +- a theorem keyword hidden in a block comment that the scanner mis-counted. + +Such a declaration compiles (Lean only warns on `sorry`), lands in the package's `.olean`, +and is exported to every importer, while the gate reports the manifest targets as clean. +Finding RF-GATE-01 (main#229). + +## The fix: two layers, the second authoritative + +1. **Grammar pre-check on source (`grammar_check`).** The stripper first lexes string + literals (with escapes), raw strings and character literals, so a `--` or `/-` inside a + literal is not a comment; literal contents are kept, so refusals see them. Interpolated + strings (`s!"…"`, and any plain string containing a brace, because macros such as + `throwError` interpolate plain literals), unterminated literals and unterminated block + comments are refused. Comments are then removed (nesting-aware), keeping newlines; a + block comment becomes one space, so `opaque/-x-/hidden` stays two tokens. On the + remaining code: + - every line with a `theorem`/`lemma`/`def` keyword must be the one canonical column-0 + declaration on that line (`theorem `, `lemma `, `def ` or + `noncomputable def `); + - declaration-bearing, metaprogramming and elaborator tokens are refused **anywhere** on a + line, so wrappers such as `set_option … in run_elab`, `open Lean in …` and term-level + `by_elab` are caught (`private`, `protected`, `opaque`, `abbrev`, `structure`, `class`, + `instance`, `inductive`, `mutual`, `syntax`, `macro`, `elab`, `run_elab`, `run_cmd`, + `run_meta`, `run_tac`, `by_elab`, `initialize`, `example`, `attribute`, `notation`, + `section`, `Lean`, `MetaM`, `CoreM`, `addDecl`, every `#` command, and more); `local` + and `scoped` are refused at the start of a line (`open scoped` stays allowed); + - each module has exactly one column-0 `namespace ResearchFormalCoreR1` … `end + ResearchFormalCoreR1` block, so a nested namespace cannot be mis-prefixed; + - no declaration name repeats, and the manifest target list has no duplicates; + - the tokens `sorry`, `axiom`, `native_decide`, `implemented_by`, `extern` and `unsafe` + are refused outright, including inside string literals. + + This is a pre-check: it keeps the source legible for the rest of the pipeline and fails + early, but it is not what the gate trusts. Admission does not depend on it (see the bound + compiled inventory below). + +2. **Environment inventory at execute time (`inventory_source`, `audit_inventory`).** + After `lake build`, the gate writes and runs `Inventory.lean`, a Lean program that + enumerates, from the compiled environment's own module tables + (`env.header.moduleData[idx].constNames` for every module under the package prefix), + **every** constant of every package module: public, private, compiler-generated, used + or unused. For each constant it prints one `INV` line with its kind, its **provenance** + and its module and name; one `MODULE` line per module with the module-system flag and + constant counts; and then it axiom-closes all package constants together in one shared + traversal that replicates `Lean.CollectAxioms.collect` (axiom: record and visit its + type; def/theorem/opaque: type and value; quot: nothing; ctor/rec: type; inductive: type + and constructors). The union is printed as one `AXIOMS` line. + + - **Provenance** is Lean's own record, `findDeclarationRanges?`: `user` when Lean stored + a source range for the constant (every user-written declaration, private or not), `aux` + when it did not (compiler-generated constants). On the current package this splits the + 116 constants into 63 `user` theorems (exactly the targets), 10 `user` definitions and + 43 `aux` theorems (`_proof_N`, `_simp_N_M`, `eq_N`). + - **Names are encoded losslessly.** Each name is printed as its components joined by + `/`, with `s` for a string component and `n` for a numeric one. + `Name.toString` is never parsed, so private names such as + `_private.«.lake».«formal-evidence».hidden_sorry.0.ResearchFormalCoreR1.hiddenAdmission`, + quoted components and names that differ only by escaping all stay distinct and + parseable. Decoding is strict (canonical lowercase hex, valid UTF-8, canonical decimal). + + `audit_inventory` first parses the transcript strictly; any malformed line, a missing + or repeated `AXIOMS`/`CLOSURE` record, or an empty inventory is an + `InventoryProtocolError`, never a rejection. It then collects **every** policy finding + as a `(code, name)` pair and raises `InventoryRejected` with the complete list: + - `unregistered_module`, `missing_module`, `duplicate_module`, `module_system`, + `root_not_empty`, `codegen_extra`: the module table is exactly the registered + `source_modules` plus the empty root, none compiled under the module system, no + code-generator extras; + - `outside_module`, `duplicate_name`, `count_mismatch`, `package_axiom`: every constant + sits in a registered module, names are unique, per-module counts match the table, and + no constant is itself an `axiom`; + - `extra_theorem`, `missing_theorem`: the `user` theorem-kind constants, private ones + included, are exactly the manifest targets, whatever their names look like; + - `unregistered_constant`, `missing_constant`: **the bound compiled inventory.** + `manifest.json["compiled_inventory"]` lists, as reviewed `[kind, origin, module, name]` + records, every constant of the package modules that is not a target theorem: today the + 10 user-written definitions and the 43 compiler-generated theorems. Every such constant + in the compiled environment must match one record exactly (kind and provenance + included), and every record must be present. A theorem a metaprogram adds without a + declaration range, a definition, an `opaque` or anything else not reviewed into this + list is rejected whatever its name, parent or provenance. The source gate checks the + records' shape and that their user-written definitions are exactly the source's + canonical `def` declarations. Adding a declaration therefore means updating this list + in a reviewed manifest change, alongside `targets`; + - `unbound_auxiliary`: in addition, every `aux` theorem-kind constant hangs below a `user` + constant of the same module through compiler suffix components only (`_proof_N`, + `_simp_N_M`, `eq_N`, `eq_def`, `match_N`). The name shape is used only together with + Lean's provenance, a user-written parent and the bound list, never on its own; + - `forbidden_axiom`, `reported_axiom_omitted`, `impossible_closure`: the axiom closure of + the whole package is inside `{propext, Classical.choice, Quot.sound}` (so a `sorry` + anywhere, in any kind of declaration, appears as `sorryAx`), contains every axiom the + per-target `#print axioms` audit reported, and is at least as large as the inventory. + + Union-of-closure is equivalent to the per-constant condition: every constant's axioms + are inside the allowed set if and only if their union is. + +3. **Admission controls, each bound to its own reason (`check_admission`).** The execute + path compiles four files that each append one declaration the old scanner could never + see to the inventory program (with the current file's constants included): + + | Control | Injected declaration | Required findings, exactly | + |---|---|---| + | `hidden_sorry` | `private theorem hiddenAdmission … := by sorry` | `forbidden_axiom sorryAx` and `extra_theorem` (the private name) | + | `hidden_theorem` | indented `@[simp] theorem indentedAdmission … := rfl` | `extra_theorem ResearchFormalCoreR1.indentedAdmission` | + | `hidden_def` | unused `noncomputable def unusedAdmission … := by sorry` | `forbidden_axiom sorryAx` | + | `outside_namespace` | column-0 `theorem outsideNamespaceAdmission` outside the namespace | `extra_theorem outsideNamespaceAdmission` | + + For each, the transcript must parse, the injected constant must appear exactly once with + the expected kind, provenance, privacy and module, and the findings must equal the + required ones by FULL decoded name and multiplicity: the short user-facing name only + locates the injection, so an unrelated private constant with the same short name in + another module is an extra finding and fails the control. A protocol error, a pass, a missing injection or any other set of findings + fails the run; there is no "any `ValueError` counts" path. + +4. **Compiled-package admission experiments (`compiled_admission`).** The controls above + inject into the inventory program's own file. The gate also copies the package (sources + plus the freshly built `.lake/build`, dependencies by symlink) into + `.lake/compiled-admission`, outside the uploaded evidence directory, and audits the + unmodified copy (it must pass and reproduce the real package's inventory digest, the + positive baseline). Then, one at a time, it adds a declaration to + `ResearchFormalCoreR1/AlgebraV2.lean` and runs the same stages as the real package on the + modified copy: `lake build`, `leanchecker`, and the per-target `#print axioms` audit, each + of which must succeed (an unrelated failure fails the run and is never counted as a + rejection), and finally the inventory, which must contain the injected constant and + reject with exactly the expected findings: + + | Experiment | Injected declaration | Required findings, exactly | + |---|---|---| + | `compiled_admission` | `private theorem compiledAdmission : (1 : Nat) = 1 := by sorry` | `forbidden_axiom sorryAx`, `extra_theorem` (private name) | + | `compiled_metaprogram` | `set_option maxRecDepth 1000 in run_elab` + `Lean.addDecl` of `ResearchFormalCoreR1.ec005_fold_gap._proof_999 : True` | `unregistered_constant ResearchFormalCoreR1.ec005_fold_gap._proof_999` | + + The second is the compiled RF312-SUCCESSOR-COMMAND-004 probe (#312, 6009707611): Lean + stores no declaration range for it, so it is `aux`, and it has a real user parent and a + compiler-shaped suffix; only the bound list rejects it. The copy is removed afterwards; + each experiment's four logs and the injected module's sha256 stay in the evidence. + +## History of the admission evidence + +The first helper revision (`dec3f646`) printed names with `Name.toString` and credited any +`ValueError` from `audit_inventory` as a rejection. Replaying its real logs showed 3 of 4 +controls rejected for their intended reason; `hidden_sorry` stopped earlier, at a +malformed-line error on the quoted private name, although `sorryAx` was in that log's +closure (PR #312 comments 6008555025 and 6008954175). That defect and the name-shaped +auxiliary exemption (which let a user-written `ResearchFormalCoreR1._unregistered` theorem +pass, 6009106591) were repaired by the successor `9aee8fd1`. The historical transcript shape +is kept as a regression: it is a protocol error, and `check_admission` does not count it. + +The source audit of `9aee8fd1` (#312, 6009593567) found two more gaps, both repaired here: +RF312-SUCCESSOR-COMMAND-004, wrapped and term-level elaborators passed the line-anchored +pre-check, and a theorem added by `Lean.addDecl` was then admitted as a range-less +auxiliary under a real parent (confirmed compiled in 6009707611); and +RF312-COMPILED-RECHECK-005, the modified package copy was not rechecked by `leanchecker` or +the axiom audit. The audit of `96606a6d` (6014639706) found RF312-CONTROL-PRIVATE-IDENTITY-006: +`check_admission` compared findings after shortening private names, so a second private +`compiledAdmission` in another module collapsed into the expected finding. Findings are now +compared by full name and multiplicity. + +## What the receipt gains + +`receipt.json` has an `inventory` object: number of package constants, number of public +theorems, number of compiler-generated theorems, the axiom closure, the closure size, a +sha256 of the inventory lines, the per-control outcomes with their exact findings, and the +compiled-package experiments' baseline digest and, per injection, outcome, findings, +module, module sha256 and the stages run. +`required_formal_check.py` binds fixed keys and tolerates the extra object. All earlier +receipt fields are unchanged. + +## Cost and measurements (local, Lean 4.34.1, Mathlib `d13f23b7`) + +| Step | Wall time | +|---|---| +| Inventory via whole-environment scan (`env.constants.map₁`) | about 8 minutes (interpreter) | +| Inventory via module tables, with provenance and encoding (shipped) | about 11 seconds | +| Four admission controls plus both compiled-package experiments (local, `leanchecker` skipped) | about 2 minutes | + +The shared closure of all 116 package constants visits 26 853 constants. + +## Limits + +- Provenance is what Lean records, and a missing range is not proof of compiler origin. The + gate therefore does not rely on it alone: every non-target constant must be in the + reviewed `compiled_inventory`, so a metaprogram-added constant is rejected even if it + slips past the pre-check. The cost is that the list must be refreshed, in review, when a + proof change makes Lean generate different auxiliaries. +- The inventory covers constants that reach the environment through the package's + modules. Constants a downstream file realizes lazily (reserved names such as `eq_1`) + belong to that downstream file, not to the package. +- `extraConstNames` (code-generator auxiliaries) must be empty for every package module; + a module that needs compiled code therefore fails this gate on purpose. Inductive types, + structures and instances are refused by the pre-check and would need a reviewed + extension of the auxiliary suffixes before they could be admitted. +- `leanchecker` replays the package, and each modified copy, in the execute path; on one + local 15 GB container it was killed for memory (exit 137), so local precommit runs of + this helper skipped those stages and say so. Complete executions with `leanchecker` exit 0 + are recorded separately. +- The gate still does not decide mathematics. A clean inventory says the package's + compiled declarations are exactly the registered ones and depend on nothing beyond the + three standard axioms; alignment with the prose remains a separate human/nonauthor + review. + +## Tests + +`tests/test_inventory_gate.py` covers the string-aware stripper (comment markers inside +strings, escapes, character and raw literals, refused interpolation and unterminated +literals), the grammar pre-check (spellings, unsupported commands, namespace structure, +duplicates, forbidden tokens), the lossless name encoding (round trips, collisions that a +dotted rendering would make, strict decoding), the generated Lean program's shape, +`audit_inventory` on synthetic inventories (every finding code, the quoted private `sorry` +case, extra user theorems whatever their names, auxiliary binding, the bound compiled +inventory including the RF312-SUCCESSOR-COMMAND-004 probe, protocol errors), +`bound_inventory` validation and the live manifest binding, and `check_admission` (expected +reason, pass, other reason, protocol error, missing or misplaced injection). The pre-check +tests include every wrapped, nested, tactic- and term-level form reported in 6009593567. Sol's PR #312 source-gate regression cases (indented, private, attributed, +unused `sorry` definition, `opaque`, `axiom`, comment ghost, duplicate target, nested +namespace) are replayed against a copied formal tree. The live modules are checked to pass +the grammar and to reproduce `manifest.json["targets"]`. diff --git a/formal/LINEAGE_VALIDATION.md b/formal/LINEAGE_VALIDATION.md index 5a0c5d20e..e96ec4d30 100644 --- a/formal/LINEAGE_VALIDATION.md +++ b/formal/LINEAGE_VALIDATION.md @@ -72,5 +72,5 @@ python3 formal/gate.py --execute Only the focused suite was run in the implementer's partial staging checkout at publication. Full-suite, exact-source and Lean execution claims require their -actual complete-checkout results; the expected main-based suite is 97 tests. +actual complete-checkout results; the complete suite size is not a protocol constant; use the actual current-run count. Local focused tests are not a Lean kernel replay or independent review. diff --git a/formal/gate.py b/formal/gate.py old mode 100644 new mode 100755 index e5975f367..7b226a50a --- a/formal/gate.py +++ b/formal/gate.py @@ -1,254 +1,188 @@ #!/usr/bin/env python3 -"""Source-bound Lean evidence, not a scientific acceptance engine (stdlib only).""" +"""RF-GATE-01 compatibility entrypoint. + +The reviewed compiled-environment gate remains byte-identical in ``gate_helper.py``. +This module re-exports its public API, binds a constrained manifest overlay, and +retains the later exact-runtime/dependency observation contract from current main. +Scientific effect: NONE. +""" import argparse import hashlib +import importlib.util import json import os -from pathlib import Path, PurePosixPath +from pathlib import Path import re -import shutil import subprocess import sys -ALLOWED = frozenset({'propext', 'Classical.choice', 'Quot.sound'}) -NAME = r'[A-Za-z_][A-Za-z0-9_.]*' -AXIOM = re.compile(r"'(" + NAME + r")' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)") -SHA256 = re.compile(r'[0-9a-f]{64}') -COMMIT = re.compile(r'[0-9a-f]{40}') +if 'gate_helper' in sys.modules: + _core = sys.modules['gate_helper'] +else: + _helper_path = Path(__file__).resolve().with_name('gate_helper.py') + _helper_spec = importlib.util.spec_from_file_location('rf312_gate_helper', _helper_path) + if _helper_spec is None or _helper_spec.loader is None: + raise ImportError('cannot load reviewed RF312 helper: ' + str(_helper_path)) + _core = importlib.util.module_from_spec(_helper_spec) + _helper_spec.loader.exec_module(_core) + +# Re-export the reviewed helper API. Tests and callers continue importing `gate`. +for _name in dir(_core): + if not _name.startswith('_'): + globals()[_name] = getattr(_core, _name) + ROOT = Path(__file__).resolve().parent +OVERLAY = ROOT / 'manifest.overlay.json' +_HELPER_LOAD_JSON = _core.load_json +_HELPER_SOURCE_CHECK = _core.source_check +_HELPER_EXECUTE = _core.execute +_ALLOWED_OVERLAY_KEYS = frozenset({'schema_version', 'files'}) + + +def _sync_root(): + """Propagate this module's effective ``ROOT`` to the reviewed helper at every call boundary. + + The helper reads its own module global ``ROOT`` (and this module derives the overlay path + from ``ROOT``) at call time, so a caller that rebinds ``gate.ROOT`` -- the fixtures of the + runtime tests do -- must be observed by every source, overlay and execution read, not only + by this wrapper. Import-time constants would silently keep reading the original tree. + """ + global OVERLAY + root = Path(ROOT) + _core.ROOT = root + OVERLAY = root / 'manifest.overlay.json' + return root + def sha(data): return hashlib.sha256(data).hexdigest() + def require(condition, message): if not condition: raise ValueError(message) + def check_lean_version(text): version = text.strip() - require(re.fullmatch(r'Lean \(version 4\.34\.1, [^()\r\n]+, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release\)', version) is not None, - 'unexpected running Lean version: ' + repr(version)) + require(re.fullmatch( + r'Lean \(version 4\.34\.1, [^()\r\n]+, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release\)', + version) is not None, 'unexpected running Lean version: ' + repr(version)) return version + def check_worktree_clean(name, status): - """`git status --porcelain` output of a dependency: staged, unstaged or untracked changes fail.""" - require(status.strip() == '', 'dependency worktree is not clean: ' + name + ': ' + status.strip()[:200]) + require(status.strip() == '', + 'dependency worktree is not clean: ' + name + ': ' + status.strip()[:200]) + def dependency_state(m): - """Exact locked revision and a clean worktree for every dependency, read from the checkouts.""" + root = _sync_root() actual = {} for name in m['dependency_revisions']: - repo = str(ROOT / '.lake' / 'packages' / name) - actual[name] = subprocess.check_output(['git', '-C', repo, 'rev-parse', 'HEAD'], text=True).strip() + repo = str(root / '.lake' / 'packages' / name) + actual[name] = subprocess.check_output( + ['git', '-C', repo, 'rev-parse', 'HEAD'], text=True).strip() check_worktree_clean(name, subprocess.check_output( ['git', '-C', repo, 'status', '--porcelain', '--untracked-files=normal'], text=True)) require(actual == m['dependency_revisions'], 'installed dependency HEAD differs from lock') return actual + def observation(version, dependencies, digest): - return {'lean_version': version, 'dependency_revisions': dependencies, 'dependency_worktrees': 'CLEAN', - 'manifest_sha256': digest} - -def audit_axioms(text, targets): - require(isinstance(targets, list) and targets and len(set(targets)) == len(targets), 'empty or duplicate target list') - records = {} - for match in AXIOM.finditer(text): - name, raw = match.groups() - require(name in targets and name not in records, 'unexpected or duplicate axiom target: ' + name) - axioms = [] if raw is None or not raw.strip() else [a.strip() for a in raw.split(',')] - require(all(re.fullmatch(NAME, a) for a in axioms), 'malformed axiom name') - require(set(axioms) <= ALLOWED, 'forbidden transitive axiom: ' + repr(set(axioms) - ALLOWED)) - records[name] = sorted(set(axioms)) - require(not AXIOM.sub('', text).strip(), 'unrecognized audit output') - require(set(records) == set(targets), 'missing target axiom report') - return records - -def check_files(root, files): - require(isinstance(files, dict) and files, 'empty file manifest') - root = root.resolve() - for name, digest in files.items(): - p = PurePosixPath(name) - require(not p.is_absolute() and '..' not in p.parts and str(p) == name and '\\' not in name, 'unsafe manifest path') - require(isinstance(digest, str) and SHA256.fullmatch(digest), 'invalid source hash') - target = root / p - require(all(not (root.joinpath(*p.parts[:i])).is_symlink() for i in range(1, len(p.parts) + 1)), 'symlink source') - require(target.is_file() and target.resolve().is_relative_to(root), 'missing or escaping source: ' + name) - require(sha(target.read_bytes()) == digest, 'source hash mismatch: ' + name) - -def check_blueprint(text, targets): - links = re.findall(r'\\lean\{([^}]+)\}', text) - require(links and all(n in targets for n in links), 'missing or unresolved Blueprint declaration') - require('\\leanok' not in text, 'unreviewed Blueprint completion label') - return links - -def lineage_identity(party, role): - """Validate declared identity text, not the truth or completeness of authorship.""" - require(isinstance(party, dict), 'malformed review lineage: ' + role) - placeholders = {'unknown', 'unverified', 'unspecified', 'tbd', 'n/a', - 'none', 'null', '?', 'not known', 'not available'} - result = {} - for key in ('provider', 'family', 'agent'): - value = party.get(key) - require(isinstance(value, str) and value.strip(), 'missing review lineage: ' + role + '.' + key) - normalized = ' '.join(value.split()).casefold() - require(normalized not in placeholders, 'ambiguous review lineage: ' + role + '.' + key) - result[key] = normalized - return result - -def check_alignment(review, manifest_digest, targets, scope_digest): - require(isinstance(review, dict), 'review must be object') - require(review.get('disposition') == 'ACCEPTED', 'alignment not accepted') - require(review.get('manifest_sha256') == manifest_digest, 'stale alignment manifest') - require(review.get('scope_sha256') == scope_digest, 'stale alignment scope') - covered = review.get('targets', []) - require(isinstance(covered, list) and len(covered) == len(set(covered)) and set(covered) == set(targets), 'partial or ambiguous review') - r = lineage_identity(review.get('reviewer'), 'reviewer') - authors = [('author', lineage_identity(review.get('author'), 'author'))] - # Absence preserves the historical single-author schema. Declared proposers - # are additional authors, never ignored metadata or a substitute for author. - proposers = review.get('proposal_authors', []) - require(isinstance(proposers, list), 'malformed review lineage: proposal_authors') - for index, proposer in enumerate(proposers): - role = 'proposal_authors[' + str(index) + ']' - identity = lineage_identity(proposer, role) - if 'targets' in proposer: - scope = proposer['targets'] - require(isinstance(scope, list) and scope and - all(isinstance(name, str) and name in targets for name in scope) and - len(scope) == len(set(scope)), 'invalid proposal target scope: ' + role) - authors.append((role, identity)) - for role, author in authors: - for key in ('provider', 'family', 'agent'): - require(author[key] != r[key], 'lineage not independent: ' + role + '.' + key) - e = review.get('evidence', {}) - require(isinstance(e.get('repository'), str) and re.fullmatch(r'[^/\s]+/[^/\s]+', e['repository']), 'missing evidence repo') - require(isinstance(e.get('commit'), str) and COMMIT.fullmatch(e['commit']), 'mutable review ref') - require(isinstance(e.get('sha256'), str) and SHA256.fullmatch(e['sha256']), 'missing review hash') - require(isinstance(e.get('path'), str) and e['path'] and not PurePosixPath(e['path']).is_absolute() and '..' not in PurePosixPath(e['path']).parts, 'missing or unsafe review path') - # This checks structure, identity and scope. A controller must retrieve and - # authenticate the review evidence; strings do not prove a review happened. - -def load_json(text): - def unique(pairs): - obj = {} - for key, value in pairs: - require(key not in obj, 'duplicate JSON key: ' + key) - obj[key] = value - return obj - return json.loads(text, object_pairs_hook=unique) + return {'lean_version': version, 'dependency_revisions': dependencies, + 'dependency_worktrees': 'CLEAN', 'manifest_sha256': digest} + + +def _overlay_bytes(): + overlay = _sync_root() / 'manifest.overlay.json' + require(overlay.is_file() and not overlay.is_symlink(), 'missing or symlink manifest overlay') + return overlay.read_bytes() + + +def _effective_manifest(text): + base = _HELPER_LOAD_JSON(text) + # Only the formal manifest has this shape; lake/alignment JSON passes through unchanged. + if not (isinstance(base, dict) and 'source_modules' in base and 'targets' in base and 'files' in base): + return base + overlay = _HELPER_LOAD_JSON(_overlay_bytes().decode()) + require(isinstance(overlay, dict) and set(overlay) == _ALLOWED_OVERLAY_KEYS, + 'invalid manifest overlay keys') + require(overlay.get('schema_version') == 1 and isinstance(overlay.get('files'), dict), + 'invalid manifest overlay schema') + require(all(isinstance(k, str) and isinstance(v, str) and re.fullmatch(r'[0-9a-f]{64}', v) + for k, v in overlay['files'].items()), 'invalid manifest overlay file binding') + merged = dict(base) + merged['files'] = dict(base['files']) + merged['files'].update(overlay['files']) + return merged + def source_check(): - raw = (ROOT / 'manifest.json').read_bytes() - m = load_json(raw) - require(m.get('schema_version') == 1 and m.get('scientific_effect') == 'NONE', 'invalid evidence schema') - require(m.get('formalization_status') == 'proved' and m.get('alignment_status') == 'PENDING_INDEPENDENT_REVIEW', 'source metadata cannot self-award execution or review') - required = {'gate.py', 'tests/test_gate.py', 'lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'ResearchFormalCoreR1.lean', 'SCOPE.md', 'GLOSSARY.md', 'README.md', 'blueprint/src/content.tex', 'tests/test_alignment_lineage.py', 'LINEAGE_VALIDATION.md'} - require(required <= set(m['files']), 'unbound control or scope file') - originals = {'originals/Algebra.lean.txt': '4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae', 'originals/ProbabilityCompanions.lean.txt': '4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d'} - require(all(m['files'].get(path) == value for path, value in originals.items()), 'original source identity changed or omitted') - require('COMPATIBILITY.md' in m['files'], 'unbound successor rationale') - check_files(ROOT, m['files']) - require((ROOT / 'lean-toolchain').read_text().strip() == 'leanprover/lean4:v4.34.1', 'wrong Lean toolchain') - lock = load_json((ROOT / 'lake-manifest.json').read_text()) - packages = lock['packages'] - require(len(packages) == len({p['name'] for p in packages}), 'duplicate dependency') - actual = {p['name']: p['rev'] for p in packages} - require(actual == m['dependency_revisions'], 'dependency lock mismatch') - require(all(COMMIT.fullmatch(v) for v in actual.values()), 'unpinned dependency') - expected_root = ''.join('import ' + path[:-5].replace('/', '.') + '\n' for path in m['source_modules']) - require((ROOT / 'ResearchFormalCoreR1.lean').read_text() == expected_root, 'root must only import registered modules') - names = [] - for path in m['source_modules']: - require(path in m['files'], 'unbound source module') - text = (ROOT / path).read_text() - names.extend('ResearchFormalCoreR1.' + n for n in re.findall(r'^(?:theorem|lemma)\s+(' + NAME + ')', text, re.M)) - require(names == m['targets'], 'target inventory differs from source declarations') - check_blueprint((ROOT / 'blueprint/src/content.tex').read_text(), names) - lean_files = {p.relative_to(ROOT).as_posix() for p in ROOT.rglob('*.lean') if '.lake' not in p.relative_to(ROOT).parts} - require(lean_files == set(m['source_modules']) | {'ResearchFormalCoreR1.lean'}, 'unregistered Lean module') - return m, sha(raw) - -def run(command, label, out, expect_success=True): - result = subprocess.run(command, cwd=ROOT, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=900) - (out / (label + '.log')).write_text(result.stdout) - print(label + ': exit ' + str(result.returncode), flush=True) - require((result.returncode == 0) == expect_success, 'unexpected process outcome: ' + label + '\n' + result.stdout[-6000:]) - return result.stdout + root = _sync_root() + raw = (root / 'manifest.json').read_bytes() + original = _core.load_json + try: + _core.load_json = _effective_manifest + m, _ = _HELPER_SOURCE_CHECK() + finally: + _core.load_json = original + # The overlay is read after the helper's own contract has passed: a manifest that fails its + # required-file inventory is refused for that reason, whether or not an overlay exists. + return m, sha(raw + b'\0RF312-OVERLAY\0' + _overlay_bytes()) + def execute(m, digest): - out = ROOT / '.lake' / 'formal-evidence' + root = _sync_root() + out = root / '.lake' / 'formal-evidence' out.mkdir(parents=True, exist_ok=True) - require(not (ROOT / '.lake').is_symlink() and not (ROOT / '.lake/build').is_symlink(), 'symlink build directory') - preflight_version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version-preflight', out)) + require(not (root / '.lake').is_symlink() and not (root / '.lake/build').is_symlink(), + 'symlink build directory') + # Keep test monkeypatches visible to the reviewed helper execution. + _core.run = globals()['run'] + _core.source_check = source_check + preflight_version = check_lean_version(run( + ['lake', 'env', 'lean', '--version'], 'version-preflight', out)) preflight = observation(preflight_version, dependency_state(m), digest) - if (ROOT / '.lake/build').exists(): - shutil.rmtree(ROOT / '.lake/build') # fresh local-package build; dependency cache is untouched - run(['lake', 'build'], 'build', out) - run(['lake', 'env', 'leanchecker', 'ResearchFormalCoreR1'], 'leanchecker', out) - audit = out / 'Audit.lean' - audit.write_text('import ResearchFormalCoreR1\n' + '\n'.join('#print axioms ' + n for n in m['targets']) + '\n') - text = run(['lake', 'env', 'lean', str(audit)], 'axioms', out) - axioms = audit_axioms(text, m['targets']) - types = out / 'Types.lean' - types.write_text('import ResearchFormalCoreR1\nset_option pp.explicit true\n' + '\n'.join('#check ' + n for n in m['targets']) + '\n') - run(['lake', 'env', 'lean', str(types)], 'elaborated-types', out) - # Real counterexample/mutation controls, not comparisons of fixed labels. - cases = { - 'false_fold': ('import ResearchFormalCoreR1\nexample : ResearchFormalCoreR1.foldPotential 1 1 - ResearchFormalCoreR1.foldPotential 1 (-1) = (2 : Real)^3 / 7 := by\n norm_num [ResearchFormalCoreR1.foldPotential]\n', False, None), - 'false_power': ('import ResearchFormalCoreR1\nexample : (2 : Real)^4 <= (2 : Real)^3 := by\n norm_num\n', False, None), - 'sorry': ('import ResearchFormalCoreR1\ntheorem injected : False := by sorry\n#print axioms injected\n', True, 'injected'), - 'custom_imported': ('import ResearchFormalCoreR1\naxiom hiddenPremise : False\ntheorem middle : False := hiddenPremise\ntheorem injected : False := middle\n#print axioms injected\n', True, 'injected'), - 'native': ('import ResearchFormalCoreR1\ntheorem injected : (2 : Nat) + 2 = 4 := by native_decide\n#print axioms injected\n', True, 'injected')} - outcomes = {} - for label, (source, succeeds, target) in cases.items(): - path = out / (label + '.lean'); path.write_text(source) - log = run(['lake', 'env', 'lean', str(path)], label, out, succeeds) - if target: - # Remove compiler diagnostics only by selecting the axiom line onward; - # absence remains an error, never an empty allowlist. - matches = list(AXIOM.finditer(log)) - require(matches, 'negative control missing axiom report: ' + label) - payload = '\n'.join(x.group() for x in matches) - try: - audit_axioms(payload, [target]) - except ValueError: - outcomes[label] = 'REJECTED_BY_AXIOM_GATE' - else: - raise ValueError('negative control escaped: ' + label) - else: - require('unsolved goals' in log or 'norm_num' in log and 'failed' in log, 'negative control did not fail on its proof goal') - outcomes[label] = 'REJECTED_BY_LEAN' - # Recheck after compilation: a build hook must not rewrite bound sources/lock. - _, after = source_check(); require(after == digest, 'manifest changed during execution') - # Final observation after the last Lean execution: the same exact release, the same locked - # and clean dependencies and the same bound sources as before the first one. - version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version', out)) - final = observation(version, dependency_state(m), after) - require(final == preflight, 'runtime, dependencies or sources changed during execution') - head = subprocess.check_output(['git', 'rev-parse', 'HEAD'], cwd=ROOT, text=True).strip() - require(COMMIT.fullmatch(head), 'missing exact checked commit') - receipt = dict(schema_version=1, scientific_effect='NONE', formalization_status='kernel-checked', - alignment_status='PENDING_INDEPENDENT_REVIEW', manifest_sha256=digest, - checked_commit=head, repository=os.environ.get('GITHUB_REPOSITORY'), - workflow_run_id=os.environ.get('GITHUB_RUN_ID'), - workflow_run_attempt=os.environ.get('GITHUB_RUN_ATTEMPT'), lean_version=version, - dependency_revisions=m['dependency_revisions'], dependency_worktrees='CLEAN', - observations={'preflight': preflight, 'final': final}, - axioms=axioms, negative_controls=outcomes) + receipt = _HELPER_EXECUTE(m, digest) + try: + _, after = source_check() + require(after == digest, 'manifest or overlay changed during execution') + version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version-final', out)) + final = observation(version, dependency_state(m), after) + require(final == preflight, 'runtime, dependencies or sources changed during execution') + except BaseException: + # The reviewed helper has already written its own receipt. A run whose final observation + # is refused must leave no receipt behind (the logs stay as evidence of the refusal). + (out / 'receipt.json').unlink(missing_ok=True) + raise + receipt = dict(receipt) + receipt.update( + lean_version=version, + dependency_revisions=m['dependency_revisions'], + dependency_worktrees='CLEAN', + workflow_run_attempt=os.environ.get('GITHUB_RUN_ATTEMPT'), + observations={'preflight': preflight, 'final': final}, + manifest_sha256=digest, + ) receipt['logs'] = {p.name: sha(p.read_bytes()) for p in sorted(out.glob('*.log'))} (out / 'receipt.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n') print(json.dumps(receipt, indent=2, sort_keys=True)) return receipt + def main(): p = argparse.ArgumentParser(description=__doc__) - p.add_argument('--execute', action='store_true', help='run build, transitive axiom audit and negative controls') - p.add_argument('--alignment', type=Path, help='validate a separately authenticated alignment record; never promotes science') + p.add_argument('--execute', action='store_true', + help='run build, compiled inventory, transitive axiom audit and controls') + p.add_argument('--alignment', type=Path, + help='validate a separately authenticated alignment record; never promotes science') args = p.parse_args() try: m, digest = source_check() if args.alignment: - check_alignment(load_json(args.alignment.read_text()), digest, m['targets'], m['files']['SCOPE.md']) + check_alignment(load_json(args.alignment.read_text()), digest, + m['targets'], m['files']['SCOPE.md']) if args.execute: execute(m, digest) else: @@ -258,5 +192,9 @@ def main(): return 1 return 0 + +# The helper must see the effective source check even when it calls back internally. +_core.source_check = source_check + if __name__ == '__main__': sys.exit(main()) diff --git a/formal/gate_helper.py b/formal/gate_helper.py new file mode 100755 index 000000000..d9049f7e8 --- /dev/null +++ b/formal/gate_helper.py @@ -0,0 +1,799 @@ +#!/usr/bin/env python3 +"""Source-bound Lean evidence, not a scientific acceptance engine (stdlib only).""" +import argparse +import hashlib +import json +import os +from pathlib import Path, PurePosixPath +import re +import shutil +import subprocess +import sys + +ALLOWED = frozenset({'propext', 'Classical.choice', 'Quot.sound'}) +NAME = r'[A-Za-z_][A-Za-z0-9_.]*' +AXIOM = re.compile(r"'(" + NAME + r")' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)") +SHA256 = re.compile(r'[0-9a-f]{64}') +COMMIT = re.compile(r'[0-9a-f]{40}') +ROOT = Path(__file__).resolve().parent +PACKAGE = 'ResearchFormalCoreR1' +# Environment-bound inventory lines emitted by the generated Lean audit (RF-GATE-01). +# Every Lean name is printed in a lossless component encoding, never with Name.toString: +# components are joined by `/`; `s` is a string component (lowercase hex of its UTF-8 +# bytes) and `n` a numeric component. Private names (`_private..0.`), +# quoted names (`«.lake»`) and names that differ only by escaping therefore stay distinct. +ENC = r'[sn][0-9a-f]*(?:/[sn][0-9a-f]*)*' +INV = re.compile(r'^INV\|(theorem|def|axiom|opaque|inductive|ctor|rec|quot)\|(user|aux)\|(' + ENC + r')\|(' + ENC + r')$') +MODULE = re.compile(r'^MODULE\|(' + ENC + r')\|(true|false)\|([0-9]+)\|([0-9]+)$') +AXIOMS = re.compile(r'^AXIOMS\|((?:' + ENC + r')(?:,' + ENC + r')*)?$') +CLOSURE = re.compile(r'^CLOSURE\|([0-9]+)$') +SIMPLE = re.compile(r'[A-Za-z_][A-Za-z0-9_]*') +# Suffix components a compiler-generated theorem may carry below its user-written parent. +# Used only together with Lean's own provenance (no declaration range) and a user-written +# parent in the same module; never on its own to classify a constant. +AUX_SUFFIX = re.compile(r'_proof_[0-9]+|_simp_[0-9]+_[0-9]+|eq_[0-9]+|eq_def|match_[0-9]+') +LOCAL_MODULE = ('_local',) +# Conservative declaration grammar the source scanner understands: public theorems +# start at column 0 as `theorem NAME` or `lemma NAME`, definitions as `def NAME` or +# `noncomputable def NAME`; every other spelling (indented, private, protected, +# attributed on the same line) is refused. +DECL_KEYWORD = re.compile(r'(?= 0, 'unterminated raw string literal') + end = close + 1 + hashes + out.append(text[i:end]); i = end + elif text[i] == '"': + require(prev != '!', 'interpolated string literal is not supported by the pre-check') + j = i + 1 + while j < n and text[j] != '"': + j += 2 if text[j] == '\\' else 1 + require(j < n, 'unterminated string literal') + require('{' not in text[i:j + 1], 'string literal with a brace (possible interpolation) is not supported by the pre-check') + out.append(text[i:j + 1]); i = j + 1 + elif text[i] == "'" and not IDENT_CHAR.match(prev): + literal = CHAR_LITERAL.match(text, i) + require(literal, 'unsupported apostrophe or character literal') + out.append(literal.group()); i = literal.end() + else: + out.append(text[i]); i += 1 + require(depth == 0, 'unterminated block comment') + return ''.join(out) + +def grammar_check(text, path, definitions=None): + """Refuse declaration spellings the column-0 scanner cannot inventory, and admission tokens. + + The source scanner is only a pre-check (see GATE_HARDENING.md); the authoritative + package-wide admission check is `audit_inventory` on the compiled environment. + Returns the canonical theorem names in source order; canonical definition names are + appended to `definitions` when a list is given. + """ + code = strip_lean_comments(text) + require(not FORBIDDEN_TOKENS.search(code), 'forbidden token in source module: ' + path) + token = UNSUPPORTED_TOKEN.search(code) + if token: + raise ValueError('unsupported metaprogramming or declaration token ' + repr(token.group()) + ' at ' + path + ':' + str(code.count('\n', 0, token.start()) + 1)) + names, declared, scopes = [], [], [] + for number, line in enumerate(code.splitlines(), 1): + where = path + ':' + str(number) + require(not UNSUPPORTED_COMMAND.match(line), 'unsupported declaration-bearing or metaprogramming command at ' + where) + if SCOPE_COMMAND.match(line): + scopes.append(line.rstrip()) + keywords = len(DECL_KEYWORD.findall(line)) + if not keywords: + continue + canonical = CANONICAL.match(line) + require(canonical and keywords == 1, 'unsupported declaration spelling (indented, private, protected, attributed or shared line) at ' + where) + declared.append(canonical.group(2)) + if canonical.group(1): + names.append(canonical.group(2)) + elif definitions is not None: + definitions.append(canonical.group(2)) + require(scopes == ['namespace ' + PACKAGE, 'end ' + PACKAGE], 'unsupported namespace structure (exactly one column-0 namespace ' + PACKAGE + ' block is allowed): ' + path) + require(len(declared) == len(set(declared)), 'duplicate source declaration: ' + path) + return names + +def inventory_source(include_local=False): + """Lean program that enumerates every constant of every package module from the compiled + environment's module tables, records Lean's own provenance for each, and axiom-closes all + of them in one shared traversal. + + The enumeration reads `env.header.moduleData[idx].constNames` for the modules under the + package prefix (the whole-environment scan `env.constants.map₁` takes minutes in the + interpreter; the module tables are the same data indexed by module). Provenance is + `findDeclarationRanges?`: `user` when Lean stored a source range for the constant (every + user-written declaration, private or not), `aux` when it did not (compiler-generated + constants such as `_proof_N`, `_simp_N_M`, `eq_N`). Names are printed in the lossless + component encoding described at `ENC`. The closure replicates the kernel-side rules of + `Lean.CollectAxioms.collect` (axiom: record and visit its type; def/theorem/opaque: type + and value; quot: nothing; ctor/rec: type; inductive: type and constructors) with one + visited set, so the printed AXIOMS line is the union over every package constant. + """ + local = (' if includeLocal then\n' + ' for (c, ci) in env.constants.map₂.toList do\n' + ' unless (`_inv).isPrefixOf c do\n' + ' consts := consts.push (c, ci, `_local)\n') + return ('import ' + PACKAGE + '\nimport Lean\nopen Lean\n\n' + 'def _inv.kind : ConstantInfo → String\n' + ' | .thmInfo _ => "theorem" | .defnInfo _ => "def" | .axiomInfo _ => "axiom" | .opaqueInfo _ => "opaque"\n' + ' | .inductInfo _ => "inductive" | .ctorInfo _ => "ctor" | .recInfo _ => "rec" | .quotInfo _ => "quot"\n\n' + 'def _inv.hex (s : String) : String :=\n' + ' s.toUTF8.foldl (fun acc b => acc ++ (if b.toNat < 16 then "0" else "") ++ String.ofList (Nat.toDigits 16 b.toNat)) ""\n\n' + 'def _inv.join (a b : String) : String := if a.isEmpty then b else a ++ "/" ++ b\n\n' + 'def _inv.enc : Name → String\n' + ' | .anonymous => ""\n' + ' | .str p s => _inv.join (_inv.enc p) ("s" ++ _inv.hex s)\n' + ' | .num p k => _inv.join (_inv.enc p) ("n" ++ toString k)\n\n' + 'structure _inv.St where\n' + ' visited : NameSet := {}\n' + ' axioms : NameSet := {}\n\n' + 'partial def _inv.collect (env : Environment) (c : Name) : StateM _inv.St Unit := do\n' + ' unless (← get).visited.contains c do\n' + ' modify fun s => { s with visited := s.visited.insert c }\n' + ' let collectExpr (e : Expr) : StateM _inv.St Unit := e.getUsedConstants.forM (_inv.collect env)\n' + ' match env.find? c with\n' + ' | some (.axiomInfo v) => modify (fun s => { s with axioms := s.axioms.insert c }) *> collectExpr v.type\n' + ' | some (.defnInfo v) => collectExpr v.type *> collectExpr v.value\n' + ' | some (.thmInfo v) => collectExpr v.type *> collectExpr v.value\n' + ' | some (.opaqueInfo v) => collectExpr v.type *> collectExpr v.value\n' + ' | some (.quotInfo _) => pure ()\n' + ' | some (.ctorInfo v) => collectExpr v.type\n' + ' | some (.recInfo v) => collectExpr v.type\n' + ' | some (.inductInfo v) => collectExpr v.type *> v.ctors.forM (_inv.collect env)\n' + ' | none => pure ()\n\n' + 'def _inv.main (pkg : Name) (includeLocal : Bool) : CoreM Unit := do\n' + ' let env ← getEnv\n' + ' let header := env.header\n' + ' let names := header.moduleNames\n' + ' let mut consts : Array (Name × ConstantInfo × Name) := #[]\n' + ' for h : idx in [0:names.size] do\n' + ' let m := names[idx]\n' + ' if pkg.isPrefixOf m then\n' + ' let data := header.moduleData[idx]!\n' + ' IO.println s!"MODULE|{_inv.enc m}|{data.isModule}|{data.constNames.size}|{data.extraConstNames.size}"\n' + ' for c in data.constNames do\n' + ' match env.find? c with\n' + ' | some ci => consts := consts.push (c, ci, m)\n' + ' | none => throwError "constant {c} of module {m} is missing from the environment"\n' + + local + + ' let sorted := consts.qsort (fun a b => _inv.enc a.1 < _inv.enc b.1)\n' + ' for (c, ci, m) in sorted do\n' + ' let origin := if (← findDeclarationRanges? c).isSome then "user" else "aux"\n' + ' IO.println s!"INV|{_inv.kind ci}|{origin}|{_inv.enc m}|{_inv.enc c}"\n' + ' let (_, s) := (sorted.forM (fun x => _inv.collect env x.1)).run {}\n' + ' let axs := (s.axioms.toArray.map _inv.enc).qsort (· < ·)\n' + ' IO.println s!"AXIOMS|{",".intercalate axs.toList}"\n' + ' IO.println s!"CLOSURE|{s.visited.size}"\n\n' + '#eval _inv.main `' + PACKAGE + ' ' + ('true' if include_local else 'false') + '\n') + +class InventoryProtocolError(ValueError): + """The inventory output is not a well-formed protocol transcript (nothing was audited).""" + +class InventoryRejected(ValueError): + """A well-formed inventory violates the admission policy; `violations` lists every finding.""" + def __init__(self, violations, inventory): + self.violations, self.inventory = violations, inventory + super().__init__('environment inventory rejected: ' + '; '.join(code + ' ' + render(name) + (' ' + note if note else '') for code, name, note in violations)) + +def decode(enc): + """Decode one ENC name into a tuple of components (str for string, int for numeric).""" + parts = [] + for item in enc.split('/'): + body = item[1:] + if item[0] == 's': + if len(body) % 2: + raise InventoryProtocolError('malformed name encoding: ' + enc) + try: + parts.append(bytes.fromhex(body).decode('utf-8')) + except (ValueError, UnicodeDecodeError): + raise InventoryProtocolError('malformed name encoding: ' + enc) from None + if body != body.lower() or bytes.fromhex(body).decode('utf-8').encode().hex() != body: + raise InventoryProtocolError('non-canonical name encoding: ' + enc) + else: + if not body.isdigit() or str(int(body)) != body: + raise InventoryProtocolError('malformed numeric name component: ' + enc) + parts.append(int(body)) + return tuple(parts) + +def encode(name): + return '/'.join(('n' + str(c)) if isinstance(c, int) else ('s' + c.encode('utf-8').hex()) for c in name) + +def render(name): + """Human-readable name for messages and receipts only; identity is the component tuple.""" + return '.'.join(str(c) if isinstance(c, int) else (c if SIMPLE.fullmatch(c) else '«' + c + '»') for c in name) + +def simple_name(text): + """Component tuple of a dotted name made only of simple identifiers (targets, modules, axioms).""" + parts = tuple(text.split('.')) + require(all(SIMPLE.fullmatch(c) for c in parts), 'unrepresentable name: ' + repr(text)) + return parts + +def user_name(name): + """(user-facing name, is_private) for a private `_private...` constant.""" + if name and name[0] == '_private': + for index, c in enumerate(name): + if isinstance(c, int): + return name[index + 1:], True + return name, False + +ALLOWED_NAMES = frozenset(simple_name(a) for a in ALLOWED) + +KINDS = ('theorem', 'def', 'axiom', 'opaque', 'inductive', 'ctor', 'rec', 'quot') + +def bound_inventory(records, targets, modules): + """The manifest's reviewed, exact non-target compiled inventory as a set of tuples. + + Each record is [kind, origin, module, name] with simple dotted names. Every constant of a + package module that is not a user-written target theorem must appear here, and every + entry must be present; admission therefore does not depend on the source pre-check or + on Lean's provenance alone (RF312-SUCCESSOR-COMMAND-004). + """ + require(isinstance(records, list), 'missing compiled inventory binding') + registered, wanted = {simple_name(m) for m in modules}, {simple_name(t) for t in targets} + result = set() + for record in records: + require(isinstance(record, list) and len(record) == 4 and all(isinstance(x, str) for x in record), 'malformed compiled inventory record: ' + repr(record)) + kind, origin, module, name = record + require(kind in KINDS and kind != 'axiom' and origin in ('user', 'aux'), 'invalid compiled inventory kind or origin: ' + repr(record)) + entry = (kind, origin, simple_name(module), simple_name(name)) + require(entry[2] in registered, 'compiled inventory record outside registered modules: ' + repr(record)) + require(not (kind == 'theorem' and origin == 'user'), 'user-written theorems belong in targets, not the compiled inventory: ' + repr(record)) + require(entry[3] not in wanted and entry not in result, 'duplicate or target-shadowing compiled inventory record: ' + repr(record)) + result.add(entry) + require(len({e[3] for e in result}) == len(result), 'duplicate name in compiled inventory') + return frozenset(result) + +def parse_inventory(text): + """Strictly parse the protocol lines; any malformed or missing record is a protocol error.""" + lines = [line for line in text.splitlines() if line.startswith(('INV|', 'MODULE|', 'AXIOMS|', 'CLOSURE|'))] + modules, constants, axioms, closures = [], [], [], [] + for line in lines: + if line.startswith('MODULE|'): + match = MODULE.fullmatch(line) + if not match: + raise InventoryProtocolError('malformed module line: ' + line) + modules.append((decode(match.group(1)), match.group(2) == 'true', int(match.group(3)), int(match.group(4)))) + elif line.startswith('INV|'): + match = INV.fullmatch(line) + if not match: + raise InventoryProtocolError('malformed inventory line: ' + line) + kind, origin, module, name = match.groups() + constants.append((kind, origin, decode(module), decode(name))) + elif line.startswith('AXIOMS|'): + match = AXIOMS.fullmatch(line) + if not match: + raise InventoryProtocolError('malformed axiom closure line: ' + line) + axioms.append([] if not match.group(1) else [decode(a) for a in match.group(1).split(',')]) + else: + match = CLOSURE.fullmatch(line) + if not match: + raise InventoryProtocolError('malformed closure line: ' + line) + closures.append(int(match.group(1))) + if not constants or not modules: + raise InventoryProtocolError('empty environment inventory') + if len(axioms) != 1 or len(closures) != 1: + raise InventoryProtocolError('inventory must report exactly one axiom closure') + return dict(modules=modules, constants=constants, axioms=axioms[0], closure=closures[0], lines=lines) + +def inventory_violations(inventory, targets, modules, allow_local=False, reported_axioms=None, bound=frozenset()): + """Every admission-policy finding on a parsed inventory, as sorted (code, name, note) triples. + + - the module table is exactly the registered modules plus an empty root module, none + compiled under the module system, none with code-generator extras; + - every constant sits in a registered module (or the current file in local mode), names + are unique, per-module counts match the table, and no constant is itself an axiom; + - the user-written (`user`) theorem-kind constants, private ones included, are exactly + the manifest targets; + - every compiler-generated (`aux`) theorem-kind constant hangs below a user-written + constant of the same module through compiler suffix components only; + - every other constant of a registered module (definitions, compiler theorems, anything + added by a metaprogram) is exactly one of the manifest's bound `compiled_inventory` + records, and every bound record is present; + - the axiom closure of all constants together is inside ALLOWED, and contains every + axiom the per-target audit reported. + """ + require(isinstance(targets, list) and targets and len(set(targets)) == len(targets), 'empty or duplicate target list') + require(isinstance(modules, (list, set, frozenset)) and modules, 'empty module registry') + registered = {simple_name(m) for m in modules} + root, wanted = simple_name(PACKAGE), {simple_name(t) for t in targets} + found = set() + def flag(code, name, note=''): + found.add((code, encode(name), note)) + counts, seen_modules = {}, set() + for name, is_module, constants, extra in inventory['modules']: + if name in seen_modules: + flag('duplicate_module', name) + seen_modules.add(name) + if is_module: + flag('module_system', name) + if name == root: + if constants or extra: + flag('root_not_empty', name) + elif name not in registered: + flag('unregistered_module', name) + else: + if extra: + flag('codegen_extra', name, str(extra)) + counts[name] = constants + for name in sorted(registered - seen_modules, key=encode): + flag('missing_module', name) + if root not in seen_modules: + flag('missing_module', root) + seen, per_module, user = set(), {name: 0 for name in registered}, {} + for kind, origin, module, name in inventory['constants']: + if name in seen: + flag('duplicate_name', name) + seen.add(name) + if not (module in registered or (allow_local and module == LOCAL_MODULE)): + flag('outside_module', name, render(module)) + if kind == 'axiom': + flag('package_axiom', name) + if module in per_module: + per_module[module] += 1 + if origin == 'user': + user.setdefault(module, set()).add(name) + for name in sorted(registered, key=encode): + if name in counts and per_module[name] != counts[name]: + flag('count_mismatch', name, str(per_module[name]) + '/' + str(counts[name])) + public = set() + for kind, origin, module, name in inventory['constants']: + if kind != 'theorem': + continue + if origin == 'user': + public.add(name) + if name not in wanted: + flag('extra_theorem', name) + continue + parents = [name[:k] for k in range(len(name) - 1, 0, -1) if name[:k] in user.get(module, set())] + if not parents or not all(isinstance(c, str) and AUX_SUFFIX.fullmatch(c) for c in name[len(parents[0]):]): + flag('unbound_auxiliary', name) + for name in sorted(wanted - public, key=encode): + flag('missing_theorem', name) + observed = set() + for kind, origin, module, name in inventory['constants']: + if module not in registered or (kind == 'theorem' and origin == 'user'): + continue + entry = (kind, origin, module, name) + observed.add(entry) + if entry not in bound: + flag('unregistered_constant', name, kind + '/' + origin) + for kind, origin, module, name in sorted(set(bound) - observed, key=lambda e: encode(e[3])): + flag('missing_constant', name, kind + '/' + origin) + closure = set(inventory['axioms']) + if len(closure) != len(inventory['axioms']): + flag('duplicate_axiom', ('AXIOMS',)) + for name in sorted(closure - ALLOWED_NAMES, key=encode): + flag('forbidden_axiom', name) + if reported_axioms is not None: + reported = {simple_name(a) for values in reported_axioms.values() for a in values} + for name in sorted(reported - closure, key=encode): + flag('reported_axiom_omitted', name) + if inventory['closure'] < len(inventory['constants']): + flag('impossible_closure', ('CLOSURE',), str(inventory['closure'])) + return [(code, decode(name), note) for code, name, note in sorted(found)] + +def audit_inventory(text, targets, modules, allow_local=False, reported_axioms=None, bound=frozenset()): + """Package-wide admission check on the compiled environment, not on source text. + + Raises InventoryProtocolError on a malformed transcript and InventoryRejected (with the + complete violation list) on any policy finding; see `inventory_violations`. + """ + inventory = parse_inventory(text) + violations = inventory_violations(inventory, targets, modules, allow_local, reported_axioms, bound) + if violations: + raise InventoryRejected(violations, inventory) + public = sorted(render(name) for kind, origin, module, name in inventory['constants'] if kind == 'theorem' and origin == 'user') + auxiliary = sum(1 for kind, origin, module, name in inventory['constants'] if kind == 'theorem' and origin == 'aux') + return dict(declarations=len(inventory['constants']), public_theorems=public, auxiliary_theorems=auxiliary, + axioms=sorted(render(a) for a in inventory['axioms']), closure=inventory['closure'], + sha256=sha('\n'.join(inventory['lines']).encode())) + +def lineage_identity(party, role): + """Validate declared identity text, not the truth or completeness of authorship.""" + require(isinstance(party, dict), 'malformed review lineage: ' + role) + placeholders = {'unknown', 'unverified', 'unspecified', 'tbd', 'n/a', + 'none', 'null', '?', 'not known', 'not available'} + result = {} + for key in ('provider', 'family', 'agent'): + value = party.get(key) + require(isinstance(value, str) and value.strip(), 'missing review lineage: ' + role + '.' + key) + normalized = ' '.join(value.split()).casefold() + require(normalized not in placeholders, 'ambiguous review lineage: ' + role + '.' + key) + result[key] = normalized + return result + +def check_alignment(review, manifest_digest, targets, scope_digest): + require(isinstance(review, dict), 'review must be object') + require(review.get('disposition') == 'ACCEPTED', 'alignment not accepted') + require(review.get('manifest_sha256') == manifest_digest, 'stale alignment manifest') + require(review.get('scope_sha256') == scope_digest, 'stale alignment scope') + covered = review.get('targets', []) + require(isinstance(covered, list) and len(covered) == len(set(covered)) and set(covered) == set(targets), 'partial or ambiguous review') + r = lineage_identity(review.get('reviewer'), 'reviewer') + authors = [('author', lineage_identity(review.get('author'), 'author'))] + # Absence preserves the historical single-author schema. Declared proposers + # are additional authors, never ignored metadata or a substitute for author. + proposers = review.get('proposal_authors', []) + require(isinstance(proposers, list), 'malformed review lineage: proposal_authors') + for index, proposer in enumerate(proposers): + role = 'proposal_authors[' + str(index) + ']' + identity = lineage_identity(proposer, role) + if 'targets' in proposer: + scope = proposer['targets'] + require(isinstance(scope, list) and scope and + all(isinstance(name, str) and name in targets for name in scope) and + len(scope) == len(set(scope)), 'invalid proposal target scope: ' + role) + authors.append((role, identity)) + for role, author in authors: + for key in ('provider', 'family', 'agent'): + require(author[key] != r[key], 'lineage not independent: ' + role + '.' + key) + e = review.get('evidence', {}) + require(isinstance(e.get('repository'), str) and re.fullmatch(r'[^/\s]+/[^/\s]+', e['repository']), 'missing evidence repo') + require(isinstance(e.get('commit'), str) and COMMIT.fullmatch(e['commit']), 'mutable review ref') + require(isinstance(e.get('sha256'), str) and SHA256.fullmatch(e['sha256']), 'missing review hash') + require(isinstance(e.get('path'), str) and e['path'] and not PurePosixPath(e['path']).is_absolute() and '..' not in PurePosixPath(e['path']).parts, 'missing or unsafe review path') + # This checks structure, identity and scope. A controller must retrieve and + # authenticate the review evidence; strings do not prove a review happened. + +def load_json(text): + def unique(pairs): + obj = {} + for key, value in pairs: + require(key not in obj, 'duplicate JSON key: ' + key) + obj[key] = value + return obj + return json.loads(text, object_pairs_hook=unique) + +def source_check(): + raw = (ROOT / 'manifest.json').read_bytes() + m = load_json(raw) + require(m.get('schema_version') == 1 and m.get('scientific_effect') == 'NONE', 'invalid evidence schema') + require(m.get('formalization_status') == 'proved' and m.get('alignment_status') == 'PENDING_INDEPENDENT_REVIEW', 'source metadata cannot self-award execution or review') + required = {'gate.py', 'tests/test_gate.py', 'lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'ResearchFormalCoreR1.lean', 'SCOPE.md', 'GLOSSARY.md', 'README.md', 'blueprint/src/content.tex', 'tests/test_alignment_lineage.py', 'LINEAGE_VALIDATION.md', 'tests/test_inventory_gate.py', 'GATE_HARDENING.md'} + require(required <= set(m['files']), 'unbound control or scope file') + originals = {'originals/Algebra.lean.txt': '4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae', 'originals/ProbabilityCompanions.lean.txt': '4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d'} + require(all(m['files'].get(path) == value for path, value in originals.items()), 'original source identity changed or omitted') + require('COMPATIBILITY.md' in m['files'], 'unbound successor rationale') + check_files(ROOT, m['files']) + require((ROOT / 'lean-toolchain').read_text().strip() == 'leanprover/lean4:v4.34.1', 'wrong Lean toolchain') + lock = load_json((ROOT / 'lake-manifest.json').read_text()) + packages = lock['packages'] + require(len(packages) == len({p['name'] for p in packages}), 'duplicate dependency') + actual = {p['name']: p['rev'] for p in packages} + require(actual == m['dependency_revisions'], 'dependency lock mismatch') + require(all(COMMIT.fullmatch(v) for v in actual.values()), 'unpinned dependency') + expected_root = ''.join('import ' + path[:-5].replace('/', '.') + '\n' for path in m['source_modules']) + require((ROOT / 'ResearchFormalCoreR1.lean').read_text() == expected_root, 'root must only import registered modules') + names, definitions = [], [] + for path in m['source_modules']: + require(path in m['files'], 'unbound source module') + require(path.startswith(PACKAGE + '/') and path.endswith('.lean') and path.count('/') == 1, 'source module outside the package directory: ' + path) + text = (ROOT / path).read_text() + # Pre-check only: the scanner refuses any theorem spelling it cannot count, and the + # compiled environment is audited package-wide in execute() (RF-GATE-01). + names.extend(PACKAGE + '.' + n for n in grammar_check(text, path, definitions)) + require(isinstance(m.get('targets'), list) and len(m['targets']) == len(set(m['targets'])), 'empty or duplicate target list') + require(len(names) == len(set(names)), 'duplicate source theorem') + require(names == m['targets'], 'target inventory differs from source declarations') + modules = {PACKAGE + '.' + path[len(PACKAGE) + 1:-5] for path in m['source_modules']} + bound = bound_inventory(m.get('compiled_inventory'), m['targets'], modules) + bound_definitions = {render(e[3]) for e in bound if e[:2] == ('def', 'user')} + require(bound_definitions == {PACKAGE + '.' + d for d in definitions} and len(definitions) == len(set(definitions)), + 'compiled inventory user definitions differ from source definitions') + check_blueprint((ROOT / 'blueprint/src/content.tex').read_text(), names) + lean_files = {p.relative_to(ROOT).as_posix() for p in ROOT.rglob('*.lean') if '.lake' not in p.relative_to(ROOT).parts} + require(lean_files == set(m['source_modules']) | {'ResearchFormalCoreR1.lean'}, 'unregistered Lean module') + return m, sha(raw) + +def run(command, label, out, expect_success=True, cwd=ROOT): + result = subprocess.run(command, cwd=cwd, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=900) + (out / (label + '.log')).write_text(result.stdout) + print(label + ': exit ' + str(result.returncode), flush=True) + require((result.returncode == 0) == expect_success, 'unexpected process outcome: ' + label + '\n' + result.stdout[-6000:]) + return result.stdout + +def check_admission(text, label, injected, expected, targets, modules, allow_local, bound): + """One admission experiment: the transcript must parse, contain the injected constant exactly + once, and be rejected with exactly the expected findings. + + `injected` is (kind, origin, user-facing name, is_private, module or None); `expected` is a + set of (code, user-facing name, is_private). The user-facing name only locates the injected + constant. Findings are then compared by FULL decoded name and multiplicity: an expected + entry naming the injection stands for that exact constant, every other expected entry must + be a public name, and any further finding (an unrelated private constant with the same short + name in another module, say) fails the experiment (RF312-CONTROL-PRIVATE-IDENTITY-006). A + protocol error, a missing injection or a pass also fails instead of counting as a rejection. + """ + inventory = parse_inventory(text) + kind, origin, name, private, module = injected + hits = [c for c in inventory['constants'] if c[0] == kind and c[1] == origin and user_name(c[3]) == (name, private) and (module is None or c[2] == module)] + require(len(hits) == 1, 'admission control did not inject exactly one ' + kind + ' ' + render(name) + ': ' + label) + full = hits[0][3] + wanted = [] + for code, short, is_private in expected: + if (short, is_private) == (name, private): + wanted.append((code, encode(full))) + else: + require(not is_private, 'expected private finding other than the injection is not identifiable: ' + label) + wanted.append((code, encode(short))) + found = inventory_violations(inventory, targets, modules, allow_local, bound=bound) + got = [(code, encode(n)) for code, n, note in found] + require(sorted(got) == sorted(wanted), 'admission control rejected for an unexpected reason: ' + label + ' expected=' + + repr(sorted(code + ' ' + render(decode(e)) for code, e in wanted)) + ' got=' + repr(sorted(code + ' ' + render(decode(e)) for code, e in got))) + return dict(outcome='REJECTED_FOR_EXPECTED_REASON', injected=render(full), + violations=[code + ' ' + render(n) for code, n, note in found]) + +COMPILED_INJECTIONS = ( + # A private theorem proved by sorry: kernel-valid, so build, recheck and the per-target + # axiom audit all pass; only the package-wide inventory can reject it. + ('compiled_admission', 'private theorem compiledAdmission : (1 : Nat) = 1 := by sorry\n', + ('theorem', 'user', (PACKAGE, 'compiledAdmission'), True), + {('forbidden_axiom', ('sorryAx',), False), ('extra_theorem', (PACKAGE, 'compiledAdmission'), True)}), + # RF312-SUCCESSOR-COMMAND-004: a wrapped elaborator adds a range-less theorem under a real + # user parent with a compiler-shaped suffix. It must fail the bound compiled inventory. + ('compiled_metaprogram', 'set_option maxRecDepth 1000 in run_elab\n Lean.addDecl <| .thmDecl {\n' + ' name := `ResearchFormalCoreR1.ec005_fold_gap._proof_999\n levelParams := []\n' + ' type := Lean.mkConst ``True\n value := Lean.mkConst ``True.intro\n }\n', + ('theorem', 'aux', (PACKAGE, 'ec005_fold_gap', '_proof_999'), False), + {('unregistered_constant', (PACKAGE, 'ec005_fold_gap', '_proof_999'), False)})) + +def compiled_admission(m, modules, baseline, bound, out): + """Inject declarations into a compiled copy of the package and require each to be rejected. + + The package is copied (sources plus the fresh `.lake/build`, dependencies by symlink) and + first audited unchanged: it must pass with the same inventory digest as the real package + (positive baseline). Then, for each entry of COMPILED_INJECTIONS in turn, the first source + module gains the declaration and the copy runs the same stages as the real package: + `lake build`, `leanchecker`, the per-target `#print axioms` audit (each must succeed; an + unrelated failure fails the run, it is never counted as a rejection), and finally the + inventory, which must contain the injected constant and reject with exactly the expected + findings (RF312-COMPILED-RECHECK-005). The copy lives under `.lake` outside the uploaded + evidence directory and is removed afterwards; only its logs remain. + """ + work = ROOT / '.lake' / 'compiled-admission' # outside the uploaded evidence directory + require(not work.is_symlink(), 'symlink compiled-admission directory') + if work.exists(): + shutil.rmtree(work) + path = m['source_modules'][0] + module = simple_name(PACKAGE + '.' + path[len(PACKAGE) + 1:-5]) + results = {} + try: + pkg = work / 'formal' + shutil.copytree(ROOT, pkg, ignore=lambda d, names: ['.lake'] if Path(d) == ROOT else []) + shutil.copytree(ROOT / '.lake' / 'build', pkg / '.lake' / 'build') + (pkg / '.lake' / 'packages').symlink_to(ROOT / '.lake' / 'packages', target_is_directory=True) + program = work / 'Inventory.lean' + program.write_text(inventory_source()) + audit = work / 'Audit.lean' + audit.write_text('import ' + PACKAGE + '\n' + '\n'.join('#print axioms ' + n for n in m['targets']) + '\n') + clean = audit_inventory(run(['lake', 'env', 'lean', str(program)], 'compiled_baseline', out, cwd=pkg), m['targets'], modules, bound=bound) + require(clean['sha256'] == baseline['sha256'], 'compiled-admission copy does not reproduce the package inventory') + original = (pkg / path).read_text() + marker = '\nend ' + PACKAGE + '\n' + require(original.count(marker) == 1, 'compiled-admission module has no unique namespace end: ' + path) + for label, declaration, (kind, origin, name, private), expected in COMPILED_INJECTIONS: + injected = original.replace(marker, '\n' + declaration + marker) + (pkg / path).write_text(injected) + run(['lake', 'build'], label + '_build', out, cwd=pkg) + run(['lake', 'env', 'leanchecker', PACKAGE], label + '_leanchecker', out, cwd=pkg) + audit_axioms(run(['lake', 'env', 'lean', str(audit)], label + '_axioms', out, cwd=pkg), m['targets']) + log = run(['lake', 'env', 'lean', str(program)], label, out, cwd=pkg) + result = check_admission(log, label, (kind, origin, name, private, module), expected, m['targets'], modules, False, bound) + result.update(module=render(module), module_sha256=sha(injected.encode()), + stages=['build', 'leanchecker', 'axioms', 'inventory']) + results[label] = result + (pkg / path).write_text(original) + finally: + if work.exists(): + shutil.rmtree(work) + return dict(baseline_sha256=clean['sha256'], injections=results) + +def execute(m, digest): + out = ROOT / '.lake' / 'formal-evidence' + out.mkdir(parents=True, exist_ok=True) + require(not (ROOT / '.lake').is_symlink() and not (ROOT / '.lake/build').is_symlink(), 'symlink build directory') + if (ROOT / '.lake/build').exists(): + shutil.rmtree(ROOT / '.lake/build') # fresh local-package build; dependency cache is untouched + run(['lake', 'build'], 'build', out) + run(['lake', 'env', 'leanchecker', 'ResearchFormalCoreR1'], 'leanchecker', out) + audit = out / 'Audit.lean' + audit.write_text('import ResearchFormalCoreR1\n' + '\n'.join('#print axioms ' + n for n in m['targets']) + '\n') + text = run(['lake', 'env', 'lean', str(audit)], 'axioms', out) + axioms = audit_axioms(text, m['targets']) + types = out / 'Types.lean' + types.write_text('import ResearchFormalCoreR1\nset_option pp.explicit true\n' + '\n'.join('#check ' + n for n in m['targets']) + '\n') + run(['lake', 'env', 'lean', str(types)], 'elaborated-types', out) + # Package-wide admission check bound to the compiled environment, not to source text: + # every constant in a registered module is enumerated by Lean itself and axiom-audited, + # and the user-written theorems must be exactly the manifest targets (RF-GATE-01). + modules = {PACKAGE + '.' + path[len(PACKAGE) + 1:-5] for path in m['source_modules']} + inventory = out / 'Inventory.lean' + inventory.write_text(inventory_source()) + bound = bound_inventory(m['compiled_inventory'], m['targets'], modules) + inventory_report = audit_inventory(run(['lake', 'env', 'lean', str(inventory)], 'inventory', out), m['targets'], modules, reported_axioms=axioms, bound=bound) + # Admission controls: declarations the source scanner could never see, or would + # mis-prefix, must be caught by the environment inventory for their own reason. Each + # compiles (sorry only warns), must appear in the inventory, and must be rejected with + # exactly the expected findings; any other outcome fails the run. + P = (PACKAGE,) + admissions = { + 'hidden_sorry': ('namespace ' + PACKAGE + '\n private theorem hiddenAdmission : (1 : Nat) = 1 := by sorry\nend ' + PACKAGE + '\n', + ('theorem', 'user', P + ('hiddenAdmission',), True, LOCAL_MODULE), + {('forbidden_axiom', ('sorryAx',), False), ('extra_theorem', P + ('hiddenAdmission',), True)}), + 'hidden_theorem': ('namespace ' + PACKAGE + '\n @[simp] theorem indentedAdmission : (1 : Nat) = 1 := rfl\nend ' + PACKAGE + '\n', + ('theorem', 'user', P + ('indentedAdmission',), False, LOCAL_MODULE), + {('extra_theorem', P + ('indentedAdmission',), False)}), + 'hidden_def': ('namespace ' + PACKAGE + '\n noncomputable def unusedAdmission : Nat := by sorry\nend ' + PACKAGE + '\n', + ('def', 'user', P + ('unusedAdmission',), False, LOCAL_MODULE), + {('forbidden_axiom', ('sorryAx',), False)}), + 'outside_namespace': ('theorem outsideNamespaceAdmission : (1 : Nat) = 1 := rfl\n', + ('theorem', 'user', ('outsideNamespaceAdmission',), False, LOCAL_MODULE), + {('extra_theorem', ('outsideNamespaceAdmission',), False)})} + admission_outcomes = {} + for label, (declaration, injected, expected) in admissions.items(): + path = out / (label + '.lean') + path.write_text(inventory_source(include_local=True).replace('import Lean\n', 'import Lean\n' + declaration, 1)) + log = run(['lake', 'env', 'lean', str(path)], label, out) + admission_outcomes[label] = check_admission(log, label, injected, expected, m['targets'], modules, True, bound) + compiled = compiled_admission(m, modules, inventory_report, bound, out) + # Real counterexample/mutation controls, not comparisons of fixed labels. + cases = { + 'false_fold': ('import ResearchFormalCoreR1\nexample : ResearchFormalCoreR1.foldPotential 1 1 - ResearchFormalCoreR1.foldPotential 1 (-1) = (2 : Real)^3 / 7 := by\n norm_num [ResearchFormalCoreR1.foldPotential]\n', False, None), + 'false_power': ('import ResearchFormalCoreR1\nexample : (2 : Real)^4 <= (2 : Real)^3 := by\n norm_num\n', False, None), + 'sorry': ('import ResearchFormalCoreR1\ntheorem injected : False := by sorry\n#print axioms injected\n', True, 'injected'), + 'custom_imported': ('import ResearchFormalCoreR1\naxiom hiddenPremise : False\ntheorem middle : False := hiddenPremise\ntheorem injected : False := middle\n#print axioms injected\n', True, 'injected'), + 'native': ('import ResearchFormalCoreR1\ntheorem injected : (2 : Nat) + 2 = 4 := by native_decide\n#print axioms injected\n', True, 'injected')} + outcomes = {} + for label, (source, succeeds, target) in cases.items(): + path = out / (label + '.lean'); path.write_text(source) + log = run(['lake', 'env', 'lean', str(path)], label, out, succeeds) + if target: + # Remove compiler diagnostics only by selecting the axiom line onward; + # absence remains an error, never an empty allowlist. + matches = list(AXIOM.finditer(log)) + require(matches, 'negative control missing axiom report: ' + label) + payload = '\n'.join(x.group() for x in matches) + try: + audit_axioms(payload, [target]) + except ValueError: + outcomes[label] = 'REJECTED_BY_AXIOM_GATE' + else: + raise ValueError('negative control escaped: ' + label) + else: + require('unsolved goals' in log or 'norm_num' in log and 'failed' in log, 'negative control did not fail on its proof goal') + outcomes[label] = 'REJECTED_BY_LEAN' + # Recheck after compilation: a build hook must not rewrite bound sources/lock. + _, after = source_check(); require(after == digest, 'manifest changed during execution') + version = run(['lake', 'env', 'lean', '--version'], 'version', out).strip() + require('version 4.34.1' in version, 'unexpected running Lean version') + actual_dependencies = {name: subprocess.check_output(['git', '-C', str(ROOT / '.lake/packages' / name), 'rev-parse', 'HEAD'], text=True).strip() for name in m['dependency_revisions']} + require(actual_dependencies == m['dependency_revisions'], 'installed dependency HEAD differs from lock') + head = subprocess.check_output(['git', 'rev-parse', 'HEAD'], cwd=ROOT, text=True).strip() + require(COMMIT.fullmatch(head), 'missing exact checked commit') + receipt = dict(schema_version=1, scientific_effect='NONE', formalization_status='kernel-checked', + alignment_status='PENDING_INDEPENDENT_REVIEW', manifest_sha256=digest, + checked_commit=head, repository=os.environ.get('GITHUB_REPOSITORY'), + workflow_run_id=os.environ.get('GITHUB_RUN_ID'), lean_version=version, + dependency_revisions=m['dependency_revisions'], axioms=axioms, negative_controls=outcomes, + inventory=dict(declarations=inventory_report['declarations'], public_theorems=len(inventory_report['public_theorems']), + auxiliary_theorems=inventory_report['auxiliary_theorems'], + axioms=inventory_report['axioms'], closure=inventory_report['closure'], + sha256=inventory_report['sha256'], admission_controls=admission_outcomes, + compiled_admission=compiled)) + receipt['logs'] = {p.name: sha(p.read_bytes()) for p in sorted(out.glob('*.log'))} + (out / 'receipt.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n') + print(json.dumps(receipt, indent=2, sort_keys=True)) + return receipt + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--execute', action='store_true', help='run build, transitive axiom audit and negative controls') + p.add_argument('--alignment', type=Path, help='validate a separately authenticated alignment record; never promotes science') + args = p.parse_args() + try: + m, digest = source_check() + if args.alignment: + check_alignment(load_json(args.alignment.read_text()), digest, m['targets'], m['files']['SCOPE.md']) + if args.execute: + execute(m, digest) + else: + print('SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): ' + digest) + except (ValueError, KeyError, TypeError, OSError, subprocess.SubprocessError) as e: + print('FORMAL_GATE_FAIL: ' + str(e), file=sys.stderr) + return 1 + return 0 + +if __name__ == '__main__': + sys.exit(main()) diff --git a/formal/manifest.json b/formal/manifest.json index 444642fb4..894b030e3 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -1,4 +1,8 @@ { + "source_identity": { + "schema": "rf312-overlay-v1", + "overlay": "manifest.overlay.json" + }, "schema_version": 1, "scientific_effect": "NONE", "formalization_status": "proved", @@ -94,45 +98,102 @@ "ResearchFormalCoreR1.d2_gaussian_control", "ResearchFormalCoreR1.d2_degenerate_control" ], + "compiled_inventory": [ + ["def", "user", "ResearchFormalCoreR1.AlgebraV2", "ResearchFormalCoreR1.foldPotential"], + ["theorem", "aux", "ResearchFormalCoreR1.AlgebraV2", "ResearchFormalCoreR1.foldPotential._proof_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha._proof_1"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha._proof_2"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Delta"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Delta.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2DetV"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2DetV.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Gamma"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Gamma.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Numerator"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Numerator.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur._proof_1"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur.eq_1"], + ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau._proof_1"], + ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau.eq_1"], + ["theorem", "aux", "ResearchFormalCoreR1.MeasureBridge", "ResearchFormalCoreR1.p02_lm008_integral_cs._simp_1_1"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_1"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_2"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_3"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_4"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_5"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_6"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_7"], + ["def", "user", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.badJetEvent"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_1"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_2"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_3"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_4"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_5"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_6"], + ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_7"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_1"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_2"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_3"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_4"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_5"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_6"], + ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_7"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_1"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_2"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_3"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_4"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_5"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_6"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_7"], + ["def", "user", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw._proof_1"], + ["theorem", "aux", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw.eq_1"] + ], "files": { ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374", "COMPATIBILITY.md": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247", "GLOSSARY.md": "6bdda2ce054915efc26e8db462dbe8fd9d0c1db30e02328857bebc6568e05ce9", - "README.md": "52c4829c23c5caa8142b4c8d7152766b92cb966b1cb8213ff5210e6fa4ef080e", + "README.md": "00fa04b316e1a208a38b80c726c5763aea09605df4da6f36e0a7dee195c71417", "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3", "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f", "ResearchFormalCoreR1.lean": "c55cc116ff3ffbffdb692226e215450a5d2e85b60d27b1b04d529b87bdef38f8", "SCOPE.md": "8fa7e879e23742aba77df8687659ca9dcfd13a19e0add6192229c2f80629b3cb", "blueprint/src/content.tex": "0c976e8e4a5e69a443e93796c8f6cbf91bf73c224448c4256de72a041e04161f", "evidence/initial-build-failure.log": "43393d2e2b3148a2453e3092a1ff04e257dbd4a6dc97eb2853a8bc0451002591", - "gate.py": "25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a", + "gate.py": "ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4", "lake-manifest.json": "d63753befccc21923783a5085148e3ff028d97134ea52f5a08bd87ecf1b0b043", "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255", "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", "originals/Algebra.lean.txt": "4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae", "originals/ProbabilityCompanions.lean.txt": "4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d", - "tests/test_gate.py": "e279e5b1e8c14f913728a18fa345dd1060d856799369fc4c9dce4a5f6dfb7574", + "tests/test_gate.py": "5df769901bbf53a7a434c2794c8685242ecfdc32f15d72fae8c2030dff7a9aa2", "ResearchFormalCoreR1/MeasureBridge.lean": "28ac130db490c3c3e2fbfabf3ac5be43c854ab1468bf573bf5a8c0dd2c50955f", "MEASURE_BRIDGE.md": "bdb6c06f359f17d493d6057adbed61edb20236b7a3a3ca4880ae0b33d8a7200e", "tests/test_measure_bridge.py": "0e54b2ed7c2e197967180993b4c0c1ece1e63576ad34fd74ac232a4d507628a2", "ResearchFormalCoreR1/WeightedLaw.lean": "f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736", "WEIGHTED_LAW.md": "a530dc957923c4c9111b734d8fcc0f4cd3cdba45b08480cfc2e241ecefc5fba4", - "tests/test_weighted_law.py": "46c0f11a7a441f085cd339a9f61aa27d1574691c279ef8b6a7a500d089374d27", + "tests/test_weighted_law.py": "acd4da143467fdcfefd1b041f18d48a7be3c3504ff1edd7e3d76df3fa5e917b0", "ResearchFormalCoreR1/MomentTail.lean": "87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa", "MOMENT_TAIL.md": "20ecddcd830c41935dc4b366882db4d0432240932af6632d025b981f90e044bd", - "tests/test_moment_tail.py": "4aa8ef5b1646f4cbef837a5b024da18fd75bf9d5dcb1489835482874d8cb48df", + "tests/test_moment_tail.py": "d50c46220ff6c4b95ee1cb42b037738740d314508019161ad6fb478ed3b0f7d5", "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08", "ResearchFormalCoreR1/MomentGenerality.lean": "fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509", "MOMENT_GENERALITY.md": "5386c763f95ecd0946e0f23a22d1ba90e7956ff1a1bfcada0d454d1b5ace0cf2", - "tests/test_moment_generality.py": "c6bdd3a3952358a14e2a211f8f6369367ab80703e8eb5196ec9c9f3a97878c8d", + "tests/test_moment_generality.py": "66a0a3d319cd5816d355c3bfa6100f16fa681bb95a2263426af6e14a9057a05d", "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893", "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815", "ResearchFormalCoreR1/WeightPerturbation.lean": "50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f", "WEIGHT_PERTURBATION.md": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212", - "tests/test_weight_perturbation.py": "0a978f8b56faceb3be6c91dea62b8837e06874ef4fcad3356842aa475d339854", + "tests/test_weight_perturbation.py": "115f3e027e29da1ae7e52c364d8ad6367c6f47658c29dcf5c325a796a35f9213", "evidence/weight-perturbation-initial-build-failure.log": "2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c", "D2_SCHUR.md": "c25f4add4c92479ae0f6dfaac43fc9be7a71766f050a79acbc2c72acf47ef4d3", "ResearchFormalCoreR1/D2Schur.lean": "d3fb3ed7b4043227f1d5a06e208de9d94eb413c067e9d0f8802388407c9e15b9", - "tests/test_d2_schur.py": "3db66384d7068129346871ca169e602b5bcd2594693090f4ddfc5d5297678f83" + "tests/test_d2_schur.py": "89badcfc82490290d7ad3671cd6f40f8980824b82a3945796e87c47712585ed9", + "tests/test_inventory_gate.py": "93bb736b73a8c93a0a6c5aa7ce8822d15013b32897cd6864bd97d0b1c9914bdb", + "GATE_HARDENING.md": "328addf8aa0946b0d62249305047ecd8e3e74b6efc44dbcf400442e5c98aa735" } } diff --git a/formal/manifest.overlay.json b/formal/manifest.overlay.json new file mode 100644 index 000000000..274930a1b --- /dev/null +++ b/formal/manifest.overlay.json @@ -0,0 +1,13 @@ +{ + "files": { + "DECLARATION_ADMISSION.md": "88bda3e378128ef3b8f4cf4e8842ba4a6f89ee5bcecf810a5a3b583079a0cedb", + "LINEAGE_VALIDATION.md": "593f8cbdb0a9261a57eded9c559963a9247a1036d5e501c9d6bbd77efe9b0c3a", + "README.md": "52c4829c23c5caa8142b4c8d7152766b92cb966b1cb8213ff5210e6fa4ef080e", + "gate.py": "509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731", + "gate_helper.py": "ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4", + "tests/test_declaration_admission.py": "6a869f853e886772a825794f06a8399fb62a541fa45e6d881029bb57e4dd7af7", + "tests/test_gate.py": "62bd0f6b3c149b30aa4ad2817aba59667b87ed5c80445f3fd64b005814968a9b", + "tests/test_gate_compatibility.py": "920811ebad0bf7f5c9d057d4396669ad340aae353e224d2e5dbc32ae94587b57" + }, + "schema_version": 1 +} diff --git a/formal/tests/test_d2_schur.py b/formal/tests/test_d2_schur.py index 7e6b23b7f..1a565babb 100644 --- a/formal/tests/test_d2_schur.py +++ b/formal/tests/test_d2_schur.py @@ -52,7 +52,7 @@ def test_manifest_exact_extension(self): for path in (MODULE, 'D2_SCHUR.md', 'tests/test_d2_schur.py'): self.assertEqual(hashlib.sha256((ROOT/path).read_bytes()).hexdigest(), m['files'][path]) self.assertEqual(m['files']['gate.py'], - '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a') + 'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4') self.assertEqual(m['files']['ResearchFormalCoreR1/WeightPerturbation.lean'], '50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f') diff --git a/formal/tests/test_declaration_admission.py b/formal/tests/test_declaration_admission.py new file mode 100644 index 000000000..0b86d6bb8 --- /dev/null +++ b/formal/tests/test_declaration_admission.py @@ -0,0 +1,150 @@ +"""Regression tests for RF-GATE-01 declaration admission. + +These tests exercise the real source-only gate in a copied formal tree. They do +not run Lean; hosted execute-time controls remain separate. +""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +FORMAL = Path(__file__).resolve().parents[1] +MODULE = "ResearchFormalCoreR1/AlgebraV2.lean" +PREFIX = "ResearchFormalCoreR1." + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +class DeclarationAdmissionRegressionTests(unittest.TestCase): + def fixture(self): + td = tempfile.TemporaryDirectory() + root = Path(td.name) / "formal" + shutil.copytree( + FORMAL, + root, + ignore=shutil.ignore_patterns(".lake", "__pycache__", "*.pyc"), + ) + return td, root + + def write_module(self, root: Path, extra: str): + p = root / MODULE + text = p.read_text() + marker = "\nend ResearchFormalCoreR1\n" + self.assertIn(marker, text) + p.write_text(text.replace(marker, "\n" + extra + "\n" + marker, 1)) + mpath = root / "manifest.json" + manifest = json.loads(mpath.read_text()) + manifest["files"][MODULE] = sha256(p) + mpath.write_text(json.dumps(manifest, indent=2) + "\n") + + def run_gate(self, root: Path): + return subprocess.run( + [sys.executable, "gate.py"], + cwd=root, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + timeout=60, + ) + + def assert_rejected(self, extra: str): + td, root = self.fixture() + try: + self.write_module(root, extra) + result = self.run_gate(root) + self.assertNotEqual( + result.returncode, + 0, + "source gate admitted an unregistered Lean declaration:\n" + + extra + + "\nstdout:\n" + + result.stdout + + "\nstderr:\n" + + result.stderr, + ) + finally: + td.cleanup() + + def test_hidden_declaration_forms_are_rejected(self): + cases = ( + " theorem rf_gate_indented : False := by sorry", + "private theorem rf_gate_private : False := by sorry", + "@[simp] theorem rf_gate_attributed : False := by sorry", + "def rf_gate_unused : False := by sorry", + "opaque rf_gate_opaque : False", + "axiom rf_gate_axiom : False", + ) + for source in cases: + with self.subTest(source=source): + self.assert_rejected(source) + + def test_comment_text_is_not_inventoried_as_a_declaration(self): + td, root = self.fixture() + try: + self.write_module( + root, + "/-\ntheorem rf_gate_comment_ghost : False := by sorry\n-/", + ) + result = self.run_gate(root) + self.assertEqual( + result.returncode, + 0, + "comment text was treated as a package declaration:\n" + + result.stdout + + result.stderr, + ) + finally: + td.cleanup() + + def test_duplicate_target_list_is_rejected_source_side(self): + td, root = self.fixture() + try: + extra = "theorem ec005_fold_gap (s : ℝ) : True := by trivial" + self.write_module(root, extra) + mpath = root / "manifest.json" + manifest = json.loads(mpath.read_text()) + name = PREFIX + "ec005_fold_gap" + insert_at = manifest["targets"].index(PREFIX + "ec014_contact_power") + 1 + manifest["targets"].insert(insert_at, name) + mpath.write_text(json.dumps(manifest, indent=2) + "\n") + result = self.run_gate(root) + self.assertNotEqual( + result.returncode, + 0, + "duplicate source/manifest target escaped source-side validation", + ) + finally: + td.cleanup() + + def test_nested_namespace_cannot_be_misprefixed(self): + td, root = self.fixture() + try: + extra = ( + "namespace Nested\n" + "theorem rf_gate_nested : True := by trivial\n" + "end Nested" + ) + self.write_module(root, extra) + mpath = root / "manifest.json" + manifest = json.loads(mpath.read_text()) + insert_at = manifest["targets"].index(PREFIX + "ec014_contact_power") + 1 + manifest["targets"].insert(insert_at, PREFIX + "rf_gate_nested") + mpath.write_text(json.dumps(manifest, indent=2) + "\n") + result = self.run_gate(root) + self.assertNotEqual( + result.returncode, + 0, + "nested declaration escaped with a fabricated flat namespace name", + ) + finally: + td.cleanup() + + +if __name__ == "__main__": + unittest.main() diff --git a/formal/tests/test_gate.py b/formal/tests/test_gate.py index e031f0b9b..e36177a1f 100644 --- a/formal/tests/test_gate.py +++ b/formal/tests/test_gate.py @@ -17,6 +17,57 @@ if spec and spec.loader and (ROOT / 'gate.py').exists(): spec.loader.exec_module(gate) +STD_AXIOMS = ('Classical.choice', 'Quot.sound', 'propext') + + +def neutral_overlay(root): + """Write an empty RF312 manifest overlay into a copied formal tree. + + The production overlay rebinds the compatibility files; these fixtures recompute every + binding from the copied bytes instead, so the effective manifest is exactly the one the + test edits. Call before hashing the tree, so the overlay file's own hash is bound too. + """ + (root / 'manifest.overlay.json').write_text(json.dumps({'files': {}, 'schema_version': 1})) + + +def encode_name(value): + return gate.encode(tuple(value) if isinstance(value, tuple) else tuple(value.split('.'))) + + +def inventory_transcript(root, manifest, injected=()): + """A clean compiled-environment inventory for the copied package, as the generated Lean + program would print it (RF-GATE-01 protocol), with optional injected constants. + + User theorems are placed in the module whose source declares them, exactly as the + source pre-check does; every other constant comes from the manifest's bound + `compiled_inventory`. `injected` entries are (kind, origin, module, name, extra_axioms) + with module/name as component tuples; a registered module's count grows with them. + """ + package = gate.PACKAGE + modules = [package + '.' + path[len(package) + 1:-5] for path in manifest['source_modules']] + constants, counts, definitions = [], {m: 0 for m in modules}, [] + for path, module in zip(manifest['source_modules'], modules): + for theorem in gate.grammar_check((root / path).read_text(), path, definitions): + constants.append(('theorem', 'user', encode_name(module), encode_name(package + '.' + theorem))) + counts[module] += 1 + for kind, origin, module, name in manifest['compiled_inventory']: + constants.append((kind, origin, encode_name(module), encode_name(name))) + counts[module] += 1 + axioms = set(STD_AXIOMS) + for kind, origin, module, name, extra in injected: + constants.append((kind, origin, gate.encode(module), gate.encode(name))) + rendered = '.'.join(str(c) for c in module) + if rendered in counts: + counts[rendered] += 1 + axioms.update(extra) + lines = ['MODULE|' + encode_name(m) + '|false|' + str(counts[m]) + '|0' for m in modules] + lines.append('MODULE|' + encode_name(package) + '|false|0|0') + lines.extend('INV|' + '|'.join(c) for c in constants) + lines.append('AXIOMS|' + ','.join(sorted(encode_name(a) for a in axioms))) + lines.append('CLOSURE|' + str(len(constants) + 1000)) + return '\n'.join(lines) + '\n' + + class GateTests(unittest.TestCase): def setUp(self): self.assertTrue(hasattr(gate, 'audit_axioms'), 'formal evidence gate not implemented') @@ -109,6 +160,7 @@ def fixture(self): self.addCleanup(self.tmp.cleanup) p = Path(self.tmp.name) / 'formal' shutil.copytree(ROOT, p, ignore=shutil.ignore_patterns('.lake', '__pycache__')) + neutral_overlay(p) self.previous = gate.ROOT; gate.ROOT = p self.addCleanup(lambda: setattr(gate, 'ROOT', self.previous)) self.m = json.loads((p/'manifest.json').read_text()) @@ -130,6 +182,34 @@ def test_root_declaration_cannot_evade_audit(self): root.write_text(root.read_text()+'theorem hidden : False := by sorry\n') self.m['files']['ResearchFormalCoreR1.lean']=hashlib.sha256(root.read_bytes()).hexdigest(); self.save() with self.assertRaises(ValueError): gate.source_check() + def test_rebound_root_redirects_source_overlay_and_evidence_reads(self): + # RF312 regression: rebinding `gate.ROOT` must redirect every read of the layered gate -- + # the helper's manifest and source checks, the overlay, and the execution evidence + # directory -- not only this wrapper's own reads (dot's failure map, Math-#312). + p = self.fixture(); self.save() + + def overlay(files): + path = p / 'manifest.overlay.json' + path.write_text(json.dumps({'schema_version': 1, 'files': files})) + self.m['files']['manifest.overlay.json'] = hashlib.sha256(path.read_bytes()).hexdigest() + self.save() + + _, digest = gate.source_check() + self.assertEqual(Path(gate._core.ROOT), p, 'helper still reads the original tree') + self.assertEqual(Path(gate.OVERLAY), p / 'manifest.overlay.json') + # A wrong binding written only into the copy's overlay is seen, so the overlay read moved. + overlay({'README.md': '0' * 64}) + with self.assertRaisesRegex(ValueError, 'source hash mismatch: README.md'): + gate.source_check() + # The digest binds the overlay bytes that were actually read. + overlay({'README.md': hashlib.sha256((p / 'README.md').read_bytes()).hexdigest()}) + _, other = gate.source_check() + self.assertNotEqual(digest, other) + # A source edit made only in the copy is seen by the helper's own file check. + (p / 'README.md').write_bytes((p / 'README.md').read_bytes() + b'\n') + with self.assertRaisesRegex(ValueError, 'source hash mismatch: README.md'): + gate.source_check() + def test_duplicate_json_rejected(self): with self.assertRaises(ValueError): gate.load_json('{"a":1,"a":2}') def test_json_object(self): @@ -145,6 +225,7 @@ def fixture(self): self.addCleanup(tmp.cleanup) self.root = Path(tmp.name) / 'formal' shutil.copytree(ROOT, self.root, ignore=shutil.ignore_patterns('.lake', '__pycache__')) + neutral_overlay(self.root) previous = gate.ROOT gate.ROOT = self.root self.addCleanup(lambda: setattr(gate, 'ROOT', previous)) @@ -162,15 +243,51 @@ def fixture(self): def execute_synthetic(self, versions, version_exit=0, mutate_source=False, wrong_dependency=False, dirty_dependency=None, drift_dependency=False, env=None): + # The layered gate observes the running Lean three times: the wrapper's preflight, the + # reviewed helper's own check after its controls, and the wrapper's final observation. + # `versions` keeps its two-entry meaning: [preflight, final]; the helper's read sees the + # preflight release (nothing changes it during the helper's own execution). + schedule = [versions[0], versions[0], versions[-1]] + package = gate.PACKAGE + first_module = self.manifest['source_modules'][0] + local = gate.LOCAL_MODULE + admissions = { + 'hidden_sorry': [('theorem', 'user', local, ('_private', 'fixture', 0, package, 'hiddenAdmission'), ('sorryAx',))], + 'hidden_theorem': [('theorem', 'user', local, (package, 'indentedAdmission'), ())], + 'hidden_def': [('def', 'user', local, (package, 'unusedAdmission'), ('sorryAx',))], + 'outside_namespace': [('theorem', 'user', local, ('outsideNamespaceAdmission',), ())], + } + + def effective_root(kwargs): + cwd = kwargs.get('cwd') + if cwd is not None and Path(cwd).resolve().is_relative_to(self.root.resolve()): + return Path(cwd) + return self.root + + def compiled_injections(package_root): + # The compiled-admission copy carries the injected declaration in its first module. + text = (package_root / first_module).read_text() + module = tuple((package + '.' + first_module[len(package) + 1:-5]).split('.')) + found = [] + for label, declaration, (kind, origin, name, private), expected in gate.COMPILED_INJECTIONS: + if declaration in text: + full = ('_private', 'fixture', 0) + name if private else name + extra = ('sorryAx',) if 'sorry' in declaration else () + found.append((kind, origin, module, full, extra)) + return found + def external_run(command, **kwargs): self.calls.append(command) if command == ['lake', 'env', 'lean', '--version']: - text = versions[min(self.version_index, len(versions) - 1)] + '\n' + text = schedule[min(self.version_index, len(schedule) - 1)] + '\n' self.version_index += 1 return subprocess.CompletedProcess(command, version_exit, text) - if command == ['lake', 'build'] and mutate_source: - path = self.root / 'lake-manifest.json' - path.write_bytes(path.read_bytes() + b'\n') + if command == ['lake', 'build']: + # A synthetic build leaves a build directory, as the real one does. + (effective_root(kwargs) / '.lake' / 'build').mkdir(parents=True, exist_ok=True) + if mutate_source: + path = self.root / 'lake-manifest.json' + path.write_bytes(path.read_bytes() + b'\n') label = Path(command[-1]).stem if label == 'Audit': text = '\n'.join("'" + n + "' does not depend on any axioms" for n in self.manifest['targets']) @@ -179,6 +296,12 @@ def external_run(command, **kwargs): elif label in ('sorry', 'custom_imported', 'native'): forbidden = {'sorry': 'sorryAx', 'custom_imported': 'hiddenPremise', 'native': 'injected._nativeDecide_1'}[label] text = "'injected' depends on axioms: [" + forbidden + ']' + elif label == 'Inventory': + # User theorems come from the fixture's own (uninjected) sources; the compiled- + # admission copy differs only by the declaration it injected, read from `cwd`. + text = inventory_transcript(self.root, self.manifest, compiled_injections(effective_root(kwargs))) + elif label in admissions: + text = inventory_transcript(self.root, self.manifest, admissions[label]) else: text = '' return subprocess.CompletedProcess(command, 0, text) @@ -239,7 +362,7 @@ def test_other_commit_after_execution_refuses_receipt(self): wrong = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit ' + 'f' * 40 + ', Release)' with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'): self.execute_synthetic([self.RELEASE, wrong]) - self.assertEqual(self.version_index, 2) + self.assertEqual(self.version_index, 3) # preflight, the helper's own check, final self.assertFalse(self.sentinel.exists()) self.assert_no_receipt() @@ -265,7 +388,7 @@ def test_success_checks_before_build_and_after_controls_and_binds_both_logs(self self.assertEqual(self.calls[0], ['lake', 'env', 'lean', '--version']) self.assertEqual(self.calls[1], ['lake', 'build']) self.assertEqual(self.calls[-1], ['lake', 'env', 'lean', '--version']) - self.assertEqual(self.version_index, 2) + self.assertEqual(self.version_index, 3) # preflight, the helper's own check, final self.assertFalse(self.sentinel.exists()) self.assertEqual(receipt['lean_version'], self.RELEASE) self.assertEqual(receipt['manifest_sha256'], self.digest) @@ -280,7 +403,7 @@ def test_version_change_after_execution_refuses_receipt(self): self.fixture() with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'): self.execute_synthetic([self.RELEASE, self.RELEASE.replace('4.34.1', '4.34.10')]) - self.assertEqual(self.version_index, 2) + self.assertEqual(self.version_index, 3) # preflight, the helper's own check, final self.assert_no_receipt() def test_source_change_during_build_still_refuses_receipt(self): @@ -326,7 +449,7 @@ def test_dependency_dirtied_during_execution_refuses_receipt(self): self.fixture() with self.assertRaisesRegex(ValueError, 'dependency worktree is not clean'): self.execute_synthetic([self.RELEASE, self.RELEASE], dirty_dependency='final') - self.assertEqual(self.version_index, 2) + self.assertEqual(self.version_index, 3) # the wrapper's final observation sees the dirty tree self.assert_no_receipt() def test_dependency_moved_during_execution_refuses_receipt(self): diff --git a/formal/tests/test_gate_compatibility.py b/formal/tests/test_gate_compatibility.py new file mode 100644 index 000000000..50ead82d2 --- /dev/null +++ b/formal/tests/test_gate_compatibility.py @@ -0,0 +1,63 @@ +import importlib.util +import json +import pathlib +import sys +import tempfile +import types +import unittest +from unittest import mock + +HERE = pathlib.Path(__file__).resolve().parents[1] + +class CompatibilityTests(unittest.TestCase): + def load(self): + helper = types.ModuleType('gate_helper') + helper.ROOT = HERE + helper.load_json = json.loads + helper.source_check = lambda: ({'source_modules': [], 'targets': [], 'files': {}}, 'old') + helper.execute = lambda m, d: {'manifest_sha256': d} + helper.run = lambda *a, **k: 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)\n' + helper.check_alignment = lambda *a: None + sys.modules['gate_helper'] = helper + spec = importlib.util.spec_from_file_location('gate_under_test', HERE / 'gate.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module, helper + + def test_exact_release_guard(self): + gate, _ = self.load() + good = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)' + self.assertEqual(gate.check_lean_version(good + '\n'), good) + for bad in ('', good.replace('5045d005', '00000000'), good + '\nnoise'): + with self.assertRaises(ValueError): + gate.check_lean_version(bad) + + def test_overlay_is_files_only(self): + gate, _ = self.load() + with tempfile.TemporaryDirectory() as td: + root = pathlib.Path(td) + gate.ROOT = root; gate.OVERLAY = root / 'manifest.overlay.json' + gate.OVERLAY.write_text(json.dumps({'schema_version': 1, 'files': {'gate.py': '0' * 64}})) + base = {'source_modules': [], 'targets': [], 'files': {'x': '1' * 64}} + merged = gate._effective_manifest(json.dumps(base)) + self.assertEqual(merged['files']['gate.py'], '0' * 64) + gate.OVERLAY.write_text(json.dumps({'schema_version': 1, 'files': {}, 'targets': []})) + with self.assertRaises(ValueError): gate._effective_manifest(json.dumps(base)) + + def test_execute_augments_receipt(self): + gate, helper = self.load() + with tempfile.TemporaryDirectory() as td: + root = pathlib.Path(td); (root / '.lake/formal-evidence').mkdir(parents=True) + gate.ROOT = root; helper.ROOT = root + gate.run = helper.run + gate.source_check = lambda: ({'dependency_revisions': {'x': 'a' * 40}}, 'digest') + gate.dependency_state = lambda m: dict(m['dependency_revisions']) + helper.execute = lambda m, d: {'manifest_sha256': d, 'logs': {}} + gate._HELPER_EXECUTE = helper.execute + with mock.patch.dict(gate.os.environ, {'GITHUB_RUN_ATTEMPT': '7'}): + receipt = gate.execute({'dependency_revisions': {'x': 'a' * 40}}, 'digest') + self.assertEqual(receipt['workflow_run_attempt'], '7') + self.assertEqual(receipt['observations']['preflight'], receipt['observations']['final']) + self.assertEqual(json.loads((root / '.lake/formal-evidence/receipt.json').read_text()), receipt) + +if __name__ == '__main__': unittest.main() diff --git a/formal/tests/test_inventory_gate.py b/formal/tests/test_inventory_gate.py new file mode 100644 index 000000000..a826d636d --- /dev/null +++ b/formal/tests/test_inventory_gate.py @@ -0,0 +1,622 @@ +"""RF-GATE-01: the environment inventory, grammar pre-check and comment stripper. + +Synthetic fixtures only; nothing here compiles Lean. The authoritative inventory is produced +by `inventory_source()` inside `gate.py --execute` and audited by `audit_inventory`. The +source-gate regression cases first published by Sol on PR #312 are replayed against a copied +formal tree in `SourceGateRegressionTests`. +""" +import hashlib +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +SPEC = importlib.util.spec_from_file_location('inventory_gate_under_test', ROOT / 'gate.py') +gate = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(gate) + +P = gate.PACKAGE +ALPHA, BETA = P + '.Alpha', P + '.Beta' +MODULES = {ALPHA, BETA} +TARGETS = [P + '.first', P + '.second'] +STD = ('Classical.choice', 'Quot.sound', 'propext') +LOCAL = ('_local',) +# The private name Lean gave the dec3f646 hidden_sorry control (file .lake/formal-evidence/hidden_sorry.lean). +QUOTED_PRIVATE = ('_private', '.lake', 'formal-evidence', 'hidden_sorry', 0, P, 'hiddenAdmission') + + +def name(value): + return tuple(value.split('.')) if isinstance(value, str) else tuple(value) + + +def enc(value): + return gate.encode(name(value)) + + +def inv(kind, origin, module, constant): + return 'INV|' + kind + '|' + origin + '|' + enc(module) + '|' + enc(constant) + + +def table(alpha=5, beta=4, root='0', is_module='false', extra='0'): + return [ + 'MODULE|' + enc(ALPHA) + '|' + is_module + '|' + str(alpha) + '|' + extra, + 'MODULE|' + enc(BETA) + '|' + is_module + '|' + str(beta) + '|' + extra, + 'MODULE|' + enc(P) + '|false|' + root + '|' + root, + ] + + +def axioms_line(axioms=STD): + return 'AXIOMS|' + ','.join(sorted(enc(a) for a in axioms)) + + +def clean(axioms=STD, closure='500', **kw): + return '\n'.join(table(**kw) + [ + inv('theorem', 'user', ALPHA, P + '.first'), + inv('theorem', 'user', BETA, P + '.second'), + inv('def', 'user', ALPHA, P + '.helper'), + inv('theorem', 'aux', ALPHA, P + '.first._proof_1'), + inv('theorem', 'aux', ALPHA, P + '.helper._simp_1_2'), + inv('theorem', 'aux', ALPHA, P + '.helper.eq_1'), + inv('inductive', 'user', BETA, P + '.Shape'), + inv('ctor', 'user', BETA, P + '.Shape.circle'), + inv('rec', 'aux', BETA, P + '.Shape.rec'), + axioms_line(axioms), + 'CLOSURE|' + closure, + ]) + + +BOUND_RECORDS = [['def', 'user', ALPHA, P + '.helper'], ['theorem', 'aux', ALPHA, P + '.first._proof_1'], + ['theorem', 'aux', ALPHA, P + '.helper._simp_1_2'], ['theorem', 'aux', ALPHA, P + '.helper.eq_1'], + ['inductive', 'user', BETA, P + '.Shape'], ['ctor', 'user', BETA, P + '.Shape.circle'], + ['rec', 'aux', BETA, P + '.Shape.rec']] +BOUND = gate.bound_inventory(BOUND_RECORDS, TARGETS, MODULES) + + +def bound_with(*records): + return BOUND | gate.bound_inventory([list(r) for r in records], TARGETS, MODULES) + + +def audit(text, targets=TARGETS, modules=MODULES, bound=None, **kw): + return gate.audit_inventory(text, targets, modules, bound=BOUND if bound is None else bound, **kw) + + +def plus(*lines, **kw): + return clean(**kw) + '\n' + '\n'.join(lines) + + +def codes(text, targets=TARGETS, modules=MODULES, bound=None, **kw): + """The exact (code, rendered name) findings of a well-formed but rejected inventory.""" + try: + audit(text, targets, modules, bound, **kw) + except gate.InventoryRejected as e: + return {(code, gate.render(n)) for code, n, note in e.violations} + raise AssertionError('inventory unexpectedly passed') + + +def wrap(body): + return 'namespace ' + P + '\n' + body + 'end ' + P + '\n' + + +class StripCommentsTests(unittest.TestCase): + def test_line_comment(self): + self.assertEqual(gate.strip_lean_comments('theorem a -- theorem hidden\n:= rfl'), 'theorem a \n:= rfl') + + def test_block_comment_nested(self): + self.assertEqual(gate.strip_lean_comments('x /- a /- theorem b -/ sorry -/ y'), 'x y') + + def test_doc_comment(self): + self.assertEqual(gate.strip_lean_comments('/-- doc with sorry -/\ntheorem a : True := trivial'), ' \ntheorem a : True := trivial') + + def test_line_comment_inside_block_does_not_close(self): + self.assertEqual(gate.strip_lean_comments('/- -- still -/ z'), ' z') + + def test_newline_positions_preserved(self): + text = 'a -- c\n/- b\n c -/ d\n/- x /- y\n -/ -/ e\n' + stripped = gate.strip_lean_comments(text) + self.assertEqual(stripped.count('\n'), text.count('\n')) + self.assertEqual(stripped.splitlines()[2], ' d') + + def test_block_comment_separates_tokens(self): + # RF312-SUCCESSOR-COMMAND-004: `opaque/-x-/hidden` must not become `opaquehidden`. + self.assertEqual(gate.strip_lean_comments('opaque/-x-/hidden'), 'opaque hidden') + + def test_unterminated(self): + with self.assertRaises(ValueError): + gate.strip_lean_comments('/- open forever') + + def test_no_comments(self): + text = 'theorem a : True := trivial\n' + self.assertEqual(gate.strip_lean_comments(text), text) + + def test_comment_markers_inside_string_are_not_comments(self): + # The old stripper cut the rest of this line, hiding the code after the string. + self.assertEqual(gate.strip_lean_comments('def s := "a -- b" ++ sorry'), 'def s := "a -- b" ++ sorry') + self.assertEqual(gate.strip_lean_comments('def s := "/-" ++ x -- "-/"'), 'def s := "/-" ++ x ') + + def test_escaped_quote_does_not_end_string(self): + self.assertEqual(gate.strip_lean_comments('def s := "a \\" -- b" -- c'), 'def s := "a \\" -- b" ') + + def test_character_literals(self): + self.assertEqual(gate.strip_lean_comments("def c := '\"' -- \"\nx"), "def c := '\"' \nx") + self.assertEqual(gate.strip_lean_comments("def c := '\\'' -- q"), "def c := '\\'' ") + + def test_apostrophe_in_identifier_is_not_a_literal(self): + self.assertEqual(gate.strip_lean_comments("theorem h' : x' = x' := rfl -- c"), "theorem h' : x' = x' := rfl ") + + def test_raw_strings(self): + self.assertEqual(gate.strip_lean_comments('def s := r"--" -- c'), 'def s := r"--" ') + self.assertEqual(gate.strip_lean_comments('def s := r#"a "-- b"# -- c'), 'def s := r#"a "-- b"# ') + + def test_comment_contents_never_open_strings(self): + self.assertEqual(gate.strip_lean_comments('-- an "unterminated\n/- also " -/ ok'), '\n ok') + + def test_unsupported_literals_refused(self): + for text in ('def s := s!"x"', 'def s := "{x}"', 'def s := "open', "def c := f ' x", 'def s := r#"open', "def c := 'ab'"): + with self.assertRaises(ValueError, msg=text): + gate.strip_lean_comments(text) + + +class GrammarCheckTests(unittest.TestCase): + def test_canonical_names(self): + text = wrap('theorem first : True := trivial\nlemma second : True := trivial\nnoncomputable def third : Nat := 1\n') + self.assertEqual(gate.grammar_check(text, 'm.lean'), ['first', 'second']) + + def test_refused_spellings(self): + for body in (' theorem hidden : True := trivial\n', 'private theorem hidden : True := trivial\n', + 'protected theorem hidden : True := trivial\n', '@[simp] theorem hidden : True := trivial\n', + ' def hidden : Nat := 1\n', 'private def hidden : Nat := 1\n', + 'def a : Nat := 1 theorem b : True := trivial\n', + 'def s : String := "a theorem walks in"\n', + 'private\ttheorem hidden : True := trivial\n', 'public theorem hidden : True := trivial\n', + 'theorem\thidden : True := trivial\n'): + with self.assertRaises(ValueError, msg=body): + gate.grammar_check(wrap(body), 'm.lean') + + def test_unsupported_commands_refused(self): + for body in ('opaque hidden : Nat\n', 'abbrev hidden : Nat := 1\n', 'instance : Inhabited Nat := ⟨0⟩\n', + 'example : True := trivial\n', 'structure S where\n x : Nat\n', 'inductive T where\n | a\n', + 'mutual\nend\n', 'macro "m" : term => `(1)\n', 'elab "e" : term => pure default\n', + 'attribute [simp] first\n', 'notation "n" => 1\n', 'run_cmd pure ()\n', '#eval 1\n', + ' #print axioms first\n', 'initialize pure ()\n', 'local notation "n" => 1\n', + 'section\nend\n', 'class C where\n'): + with self.assertRaises(ValueError, msg=body): + gate.grammar_check(wrap(body), 'm.lean') + + def test_attribute_previous_line_allowed(self): + self.assertEqual(gate.grammar_check(wrap('@[simp]\ntheorem ok : True := trivial\n'), 'm.lean'), ['ok']) + + def test_keyword_inside_comment_ignored(self): + text = wrap('-- theorem commented : False\n/- lemma also : False\nprivate theorem x -/\ntheorem ok : True := trivial\n') + self.assertEqual(gate.grammar_check(text, 'm.lean'), ['ok']) + + def test_keyword_as_identifier_part_ignored(self): + self.assertEqual(gate.grammar_check(wrap('def my_theorem_count : Nat := 1\ntheorem ok : True := Function.eq_def\n'), 'm.lean'), ['ok']) + + def test_comment_marker_in_string_cannot_hide_code(self): + with self.assertRaises(ValueError): + gate.grammar_check(wrap('def s : String := "--" ++ by sorry\n'), 'm.lean') + + def test_apostrophe_and_unicode_names_refused(self): + for bad in ("foo'", '«hidden»', 'foo✓'): + with self.assertRaises(ValueError): + gate.grammar_check(wrap('theorem ' + bad + ' : True := trivial\n'), 'm.lean') + + def test_namespace_structure(self): + gate.grammar_check(wrap(''), 'm.lean') + for text in ('theorem a : True := trivial\n', 'namespace Other\ntheorem a : True := trivial\nend Other\n', + wrap('namespace Nested\ntheorem a : True := trivial\nend Nested\n'), wrap('') + wrap(''), + 'namespace ' + P + '\n', ' namespace ' + P + '\nend ' + P + '\n'): + with self.assertRaises(ValueError, msg=text): + gate.grammar_check(text, 'm.lean') + + def test_duplicate_declaration_refused(self): + with self.assertRaises(ValueError): + gate.grammar_check(wrap('theorem a : True := trivial\ntheorem a : True := trivial\n'), 'm.lean') + + def test_refusal_names_original_line_number(self): + text = '/- a\n b -/\n-- c\nnamespace ' + P + '\n theorem hidden : True := trivial\nend ' + P + '\n' + with self.assertRaises(ValueError) as cm: + gate.grammar_check(text, 'm.lean') + self.assertIn('m.lean:5', str(cm.exception)) + + def test_forbidden_tokens(self): + for body in ('theorem bad : False := by sorry\n', 'axiom hidden : False\n', 'theorem t : 2 + 2 = 4 := by native_decide\n', + '@[implemented_by f]\ndef g : Nat := 0\n', '@[extern "c"]\ndef g : Nat := 0\n', 'unsafe def g : Nat := 0\n'): + with self.assertRaises(ValueError, msg=body): + gate.grammar_check(wrap(body), 'm.lean') + + def test_forbidden_token_inside_string_refused(self): + with self.assertRaises(ValueError): + gate.grammar_check(wrap('def s : String := "sorry"\n'), 'm.lean') + + def test_tokens_in_comments_and_identifiers_allowed(self): + self.assertEqual(gate.grammar_check(wrap('-- no sorry here\ntheorem ok : True := trivial -- sorryAx\n'), 'm.lean'), ['ok']) + + def test_unterminated_comment_refused(self): + with self.assertRaises(ValueError): + gate.grammar_check(wrap('/- theorem a : True := trivial\n'), 'm.lean') + + def test_wrapped_and_term_level_metaprograms_refused(self): + # RF312-SUCCESSOR-COMMAND-004 reproduction (#312, 6009593567) plus nested and term forms. + for body in ('set_option maxRecDepth 1000 in run_elab pure ()\n', 'open Lean in run_elab pure ()\n', + 'set_option maxRecDepth 1000 in #check True\n', 'opaque/-separator-/hidden : Nat := 0\n', + 'theorem t : True := by_elab pure default\n', 'set_option a 1 in\nset_option b 2 in\n run_elab pure ()\n', + 'theorem t : True := by\n run_tac pure ()\n', 'theorem t : True := by\n #check True\n trivial\n', + 'set_option maxRecDepth 1000 in\n Lean.addDecl x\n', 'def m : MetaM Unit := pure ()\n', + 'set_option x 1 in opaque y : Nat\n', 'theorem t : True := (by exact trivial : True) -- ok\nelab_rules : term | _ => default\n'): + with self.assertRaises(ValueError, msg=body): + gate.grammar_check(wrap(body), 'm.lean') + + def test_set_option_in_before_theorem_allowed(self): + self.assertEqual(gate.grammar_check(wrap('set_option maxHeartbeats 400000 in\ntheorem ok : True := trivial\n'), 'm.lean'), ['ok']) + + def test_definitions_collected(self): + definitions = [] + gate.grammar_check(wrap('noncomputable def f : Nat := 1\ndef g : Nat := 2\ntheorem ok : True := trivial\n'), 'm.lean', definitions) + self.assertEqual(definitions, ['f', 'g']) + + +class NameEncodingTests(unittest.TestCase): + def test_round_trip(self): + for n in (('a',), (P, 'first'), QUOTED_PRIVATE, ('', 'x'), ('été', 7), ('a.b',)): + self.assertEqual(gate.decode(gate.encode(n)), n) + + def test_lossless_where_dotted_rendering_collides(self): + pairs = ((('a.b',), ('a', 'b')), (('0',), (0,)), (('x', '1'), ('x', 1))) + for left, right in pairs: + self.assertNotEqual(gate.encode(left), gate.encode(right)) + + def test_malformed_encodings_refused(self): + for bad in ('s6', 's6G', 'sC3', 'n01', 'n', 'sff', 's61/n1x'): + with self.assertRaises(gate.InventoryProtocolError, msg=bad): + gate.decode(bad) + + def test_render_marks_quoted_components(self): + self.assertEqual(gate.render(QUOTED_PRIVATE), '_private.«.lake».«formal-evidence».hidden_sorry.0.' + P + '.hiddenAdmission') + + def test_private_user_name(self): + self.assertEqual(gate.user_name(QUOTED_PRIVATE), ((P, 'hiddenAdmission'), True)) + self.assertEqual(gate.user_name((P, 'first')), ((P, 'first'), False)) + + def test_simple_name_refuses_unrepresentable_targets(self): + for bad in ('a..b', 'a.', "a'", '«x»'): + with self.assertRaises(ValueError): + gate.simple_name(bad) + + +class InventorySourceTests(unittest.TestCase): + def test_package_import_and_module_table_enumeration(self): + src = gate.inventory_source() + self.assertTrue(src.startswith('import ' + P + '\nimport Lean\n')) + for piece in ('header.moduleData[idx]!', 'pkg.isPrefixOf m', 'data.constNames', 'e.getUsedConstants.forM', + 'findDeclarationRanges? c', '_inv.enc m', '_inv.enc c', 's.toUTF8.foldl', '| .num p k =>'): + self.assertIn(piece, src, piece) + for rule in ('.axiomInfo v', '.defnInfo v', '.thmInfo v', '.opaqueInfo v', '.quotInfo _', '.ctorInfo v', '.recInfo v', '.inductInfo v', '| none'): + self.assertIn(rule, src, rule) + self.assertNotIn('toString c', src) + self.assertTrue(src.rstrip().endswith('`' + P + ' false')) + + def test_local_mode_adds_current_file_constants(self): + src = gate.inventory_source(include_local=True) + self.assertIn('map₂', src) + self.assertIn('`_local', src) + self.assertEqual(src.count('import Lean\n'), 1) + self.assertTrue(src.rstrip().endswith('`' + P + ' true')) + + def test_missing_constant_is_fatal_in_lean(self): + self.assertIn('throwError "constant', gate.inventory_source()) + + +class AuditInventoryTests(unittest.TestCase): + def test_clean_passes(self): + report = audit(clean()) + self.assertEqual(report['public_theorems'], sorted(TARGETS)) + self.assertEqual(report['declarations'], 9) + self.assertEqual(report['auxiliary_theorems'], 3) + self.assertEqual(report['axioms'], ['Classical.choice', 'Quot.sound', 'propext']) + self.assertEqual(report['closure'], 500) + self.assertEqual(len(report['sha256']), 64) + + def test_axiom_free_closure_passes(self): + self.assertEqual(audit(clean(axioms=()))['axioms'], []) + + def test_report_is_deterministic(self): + self.assertEqual(audit(clean()), audit(clean())) + + def test_noise_lines_ignored_but_inventory_required(self): + audit('warning: something\n' + clean() + '\ntrailing') + with self.assertRaises(gate.InventoryProtocolError): + audit('warning: only\n') + + def test_quoted_private_sorry_rejected_for_both_reasons(self): + # The dec3f646 helper stopped at a malformed-line error on this name; it now parses. + text = plus(inv('theorem', 'user', ALPHA, QUOTED_PRIVATE), axioms=STD + ('sorryAx',), alpha=6) + self.assertEqual(codes(text), {('forbidden_axiom', 'sorryAx'), ('extra_theorem', gate.render(QUOTED_PRIVATE))}) + + def test_custom_axiom_in_closure_rejected(self): + self.assertEqual(codes(clean(axioms=STD + ('Other.hidden',))), {('forbidden_axiom', 'Other.hidden')}) + + def test_extra_user_theorem_rejected_whatever_its_name(self): + # Astra's synthetic records (#312, 6009106591) and an underscore name: shape is irrelevant. + for extra in (P + '.indentedExtra', P + '._unregistered', P + '.proof_999', P + '.first.eq_99', + P + '.helper._simp_999_999', P + '.first._proof_7'): + self.assertEqual(codes(plus(inv('theorem', 'user', ALPHA, extra), alpha=6)), {('extra_theorem', extra)}, extra) + + def test_auxiliary_theorem_needs_user_parent_in_same_module(self): + ok = (P + '.first.match_1.eq_1', P + '.helper.eq_def', P + '.first._proof_1._simp_2_3') + for aux in ok: + audit(plus(inv('theorem', 'aux', ALPHA, aux), alpha=6), bound=bound_with(('theorem', 'aux', ALPHA, aux))) + bad = ((ALPHA, P + '.orphan._proof_1'), (ALPHA, P + '._proof_1'), (BETA, P + '.first._proof_9'), + (ALPHA, P + '.first.helperLemma'), (ALPHA, P + '.first.proof_1'), (ALPHA, P + '.first.eq_1.extra')) + for module, aux in bad: + counts = dict(alpha=6) if module == ALPHA else dict(beta=5) + # Bound in the manifest, so only the parent rule speaks. + self.assertEqual(codes(plus(inv('theorem', 'aux', module, aux), **counts), bound=bound_with(('theorem', 'aux', module, aux))), + {('unbound_auxiliary', aux)}, aux) + + def test_auxiliary_parent_must_be_user_written(self): + text = plus(inv('theorem', 'aux', ALPHA, P + '.first._proof_1.eq_1'), alpha=6) + audit(text, bound=bound_with(('theorem', 'aux', ALPHA, P + '.first._proof_1.eq_1'))) # user parent, compiler suffixes + text = plus(inv('def', 'aux', ALPHA, P + '.gen'), inv('theorem', 'aux', ALPHA, P + '.gen.eq_1'), alpha=7) + bound = bound_with(('def', 'aux', ALPHA, P + '.gen'), ('theorem', 'aux', ALPHA, P + '.gen.eq_1')) + self.assertEqual(codes(text, bound=bound), {('unbound_auxiliary', P + '.gen.eq_1')}) + + def test_non_theorem_auxiliaries_are_closure_only(self): + records = (('def', 'aux', ALPHA, P + '.helper._unsafe_rec'), ('opaque', 'aux', ALPHA, P + '.x')) + audit(plus(*(inv(*r) for r in records), alpha=7), bound=bound_with(*records)) + + def test_axiom_kind_rejected_even_if_unused(self): + self.assertEqual(codes(plus(inv('axiom', 'user', ALPHA, P + '.hiddenPremise'), alpha=6)), + {('package_axiom', P + '.hiddenPremise'), ('unregistered_constant', P + '.hiddenPremise')}) + + def test_module_table_findings(self): + self.assertEqual(codes(plus('MODULE|' + enc(P + '.Gamma') + '|false|1|0', inv('def', 'user', P + '.Gamma', P + '.stray'))), + {('unregistered_module', P + '.Gamma'), ('outside_module', P + '.stray')}) + self.assertEqual(codes(plus(inv('def', 'user', P + '.Gamma', P + '.stray'))), {('outside_module', P + '.stray')}) + text = '\n'.join(line for line in clean().splitlines() if not line.startswith('MODULE|' + enc(BETA) + '|')) + self.assertEqual(codes(text), {('missing_module', BETA)}) + self.assertEqual(codes(clean(is_module='true')), {('module_system', ALPHA), ('module_system', BETA)}) + self.assertEqual(codes(clean(root='1')), {('root_not_empty', P)}) + self.assertEqual(codes(clean(extra='1')), {('codegen_extra', ALPHA), ('codegen_extra', BETA)}) + self.assertEqual(codes(clean(alpha=4)), {('count_mismatch', ALPHA)}) + self.assertEqual(codes(plus('MODULE|' + enc(ALPHA) + '|false|5|0')), {('duplicate_module', ALPHA)}) + + def test_local_module_only_when_allowed(self): + text = plus(inv('def', 'user', LOCAL, '_eval')) + self.assertEqual(codes(text), {('outside_module', '_eval')}) + audit(text, allow_local=True) + + def test_local_user_theorem_rejected_even_when_local_allowed(self): + text = plus(inv('theorem', 'user', LOCAL, P + '.indentedAdmission')) + self.assertEqual(codes(text, allow_local=True), {('extra_theorem', P + '.indentedAdmission')}) + + def test_missing_target_rejected(self): + text = '\n'.join(line for line in clean(beta=3).splitlines() if enc(P + '.second') not in line) + self.assertEqual(codes(text), {('missing_theorem', P + '.second')}) + + def test_target_only_as_auxiliary_or_private_is_missing(self): + text = '\n'.join(line for line in clean().splitlines() if enc(P + '.second') not in line) + self.assertIn(('missing_theorem', P + '.second'), codes(text + '\n' + inv('theorem', 'aux', BETA, P + '.second'))) + private = ('_private', P, 'Beta', 0, P, 'second') + self.assertEqual(codes(text + '\n' + inv('theorem', 'user', BETA, private)), + {('missing_theorem', P + '.second'), ('extra_theorem', gate.render(private))}) + + def test_duplicate_name_rejected(self): + self.assertEqual(codes(plus(inv('theorem', 'user', ALPHA, P + '.first'), alpha=6)), {('duplicate_name', P + '.first')}) + + def test_axiom_closure_line_required_exactly_once(self): + with self.assertRaises(gate.InventoryProtocolError): + audit(plus('AXIOMS|')) + for prefix in ('AXIOMS|', 'CLOSURE|'): + with self.assertRaises(gate.InventoryProtocolError): + audit('\n'.join(l for l in clean().splitlines() if not l.startswith(prefix))) + + def test_closure_smaller_than_inventory_rejected(self): + self.assertEqual(codes(clean(closure='3')), {('impossible_closure', 'CLOSURE')}) + + def test_per_target_audit_cross_check(self): + audit(clean(), reported_axioms={TARGETS[0]: ['propext'], TARGETS[1]: []}) + audit(clean(), reported_axioms={}) + self.assertEqual(codes(clean(axioms=('propext',)), reported_axioms={TARGETS[0]: ['propext', 'Quot.sound']}), + {('reported_axiom_omitted', 'Quot.sound')}) + + def test_malformed_lines_are_protocol_errors(self): + for bad in ('INV|theorem|user|' + enc(ALPHA), 'INV|macro|user|' + enc(ALPHA) + '|' + enc('x'), + 'INV|theorem|' + enc(ALPHA) + '|' + enc(P + '.first'), 'INV|theorem|maybe|' + enc(ALPHA) + '|' + enc('x'), + 'INV|theorem|user|' + ALPHA + '|' + P + '.x', 'INV|theorem|user|' + enc(ALPHA) + '|s6', + 'MODULE|' + enc(ALPHA) + '|maybe|1|0', 'AXIOMS|[propext]', 'CLOSURE|x'): + with self.assertRaises(gate.InventoryProtocolError, msg=bad): + audit(plus(bad)) + + def test_every_finding_is_reported(self): + text = plus(inv('theorem', 'user', ALPHA, P + '.extra'), inv('axiom', 'user', BETA, P + '.ax'), axioms=STD + ('sorryAx',), alpha=6, beta=5) + self.assertEqual(codes(text), {('extra_theorem', P + '.extra'), ('package_axiom', P + '.ax'), ('unregistered_constant', P + '.ax'), + ('forbidden_axiom', 'sorryAx')}) + + def test_unbound_constants_rejected_whatever_their_provenance(self): + # The compiled RF312-SUCCESSOR-COMMAND-004 probe: a range-less theorem added by a wrapped + # elaborator under a real user parent with a compiler-shaped suffix (#312, 6009707611). + probe = P + '.first._proof_999' + self.assertEqual(codes(plus(inv('theorem', 'aux', ALPHA, probe), alpha=6)), {('unregistered_constant', probe)}) + for record in (('def', 'user', ALPHA, P + '.extraDef'), ('def', 'aux', BETA, P + '.second._unsafe_rec'), + ('opaque', 'user', BETA, P + '.hiddenOpaque'), ('inductive', 'user', ALPHA, P + '.T')): + counts = dict(alpha=6) if record[2] == ALPHA else dict(beta=5) + self.assertEqual(codes(plus(inv(*record), **counts)), {('unregistered_constant', record[3])}, record) + + def test_bound_record_must_match_kind_and_provenance(self): + text = '\n'.join(l for l in clean().splitlines() if enc(P + '.helper.eq_1') not in l) + changed = text + '\n' + inv('theorem', 'user', ALPHA, P + '.helper.eq_1') + self.assertEqual(codes(changed), {('extra_theorem', P + '.helper.eq_1'), ('missing_constant', P + '.helper.eq_1')}) + relabeled = clean().replace(inv('def', 'user', ALPHA, P + '.helper'), inv('def', 'aux', ALPHA, P + '.helper')) + self.assertEqual(codes(relabeled), {('unregistered_constant', P + '.helper'), ('missing_constant', P + '.helper'), + ('unbound_auxiliary', P + '.helper._simp_1_2'), ('unbound_auxiliary', P + '.helper.eq_1')}) + + def test_missing_bound_constant_rejected(self): + text = '\n'.join(l for l in clean(alpha=4).splitlines() if enc(P + '.helper.eq_1') not in l) + self.assertEqual(codes(text), {('missing_constant', P + '.helper.eq_1')}) + + def test_default_bound_is_empty(self): + with self.assertRaises(gate.InventoryRejected): + gate.audit_inventory(clean(), TARGETS, MODULES) + + +class BoundInventoryTests(unittest.TestCase): + def test_valid_records(self): + self.assertEqual(len(BOUND), 7) + self.assertIn(('theorem', 'aux', name(ALPHA), name(P + '.first._proof_1')), BOUND) + + def test_invalid_records_refused(self): + for records in (None, {}, [['def', 'user', ALPHA]], [['axiom', 'user', ALPHA, P + '.x']], [['theorem', 'user', ALPHA, P + '.x']], + [['def', 'maybe', ALPHA, P + '.x']], [['def', 'user', P + '.Gamma', P + '.x']], [['def', 'user', ALPHA, P + '.first']], + [['def', 'user', ALPHA, P + '.x'], ['def', 'user', ALPHA, P + '.x']], + [['def', 'user', ALPHA, P + '.x'], ['opaque', 'user', ALPHA, P + '.x']], [['def', 'user', ALPHA, "x'"]], [[1, 2, 3, 4]]): + with self.assertRaises(ValueError, msg=repr(records)): + gate.bound_inventory(records, TARGETS, MODULES) + + def test_live_manifest_binding(self): + m = gate.load_json((ROOT / 'manifest.json').read_text()) + modules = {P + '.' + path[len(P) + 1:-5] for path in m['source_modules']} + bound = gate.bound_inventory(m['compiled_inventory'], m['targets'], modules) + kinds = sorted({(e[0], e[1]) for e in bound}) + self.assertEqual(kinds, [('def', 'user'), ('theorem', 'aux')]) + self.assertEqual(len(bound), 53) + definitions = [] + for path in m['source_modules']: + gate.grammar_check((ROOT / path).read_text(), path, definitions) + self.assertEqual({gate.render(e[3]) for e in bound if e[0] == 'def'}, {P + '.' + d for d in definitions}) + + def test_empty_targets_or_modules_rejected(self): + for targets, modules in (([], MODULES), (TARGETS + [TARGETS[0]], MODULES), (TARGETS, set())): + with self.assertRaises(ValueError): + gate.audit_inventory(clean(), targets, modules) + + +class AdmissionCheckTests(unittest.TestCase): + INJECTED = ('theorem', 'user', (P, 'hiddenAdmission'), True, LOCAL) + EXPECTED = {('forbidden_axiom', ('sorryAx',), False), ('extra_theorem', (P, 'hiddenAdmission'), True)} + PRIVATE = ('_private', '.lake', 'formal-evidence', 'hidden_sorry', 0, P, 'hiddenAdmission') + + def check(self, text, injected=None, expected=None): + return gate.check_admission(text, 'hidden_sorry', injected or self.INJECTED, self.EXPECTED if expected is None else expected, TARGETS, MODULES, True, BOUND) + + def test_expected_reason_counts(self): + result = self.check(plus(inv('theorem', 'user', LOCAL, self.PRIVATE), axioms=STD + ('sorryAx',))) + self.assertEqual(result['outcome'], 'REJECTED_FOR_EXPECTED_REASON') + self.assertEqual(result['injected'], gate.render(self.PRIVATE)) + + def test_passing_inventory_fails_the_experiment(self): + with self.assertRaises(ValueError) as cm: + self.check(plus(inv('theorem', 'aux', LOCAL, self.PRIVATE)), injected=('theorem', 'aux', (P, 'hiddenAdmission'), True, LOCAL)) + self.assertIn('unexpected reason', str(cm.exception)) + + def test_other_reason_fails_the_experiment(self): + # sorryAx missing from the closure: rejected, but not for the control's reason. + with self.assertRaises(ValueError) as cm: + self.check(plus(inv('theorem', 'user', LOCAL, self.PRIVATE))) + self.assertIn('unexpected reason', str(cm.exception)) + with self.assertRaises(ValueError): + self.check(plus(inv('theorem', 'user', LOCAL, self.PRIVATE), inv('axiom', 'user', LOCAL, P + '.extraAx'), axioms=STD + ('sorryAx',))) + + def test_protocol_error_fails_the_experiment(self): + # The historical dec3f646 transcript shape: the private name was printed with + # Name.toString and failed the old pattern. Such output is never a rejection. + old = plus('INV|theorem|_local|_private.«.lake».«formal-evidence».hidden_sorry.0.' + P + '.hiddenAdmission', axioms=STD + ('sorryAx',)) + with self.assertRaises(gate.InventoryProtocolError): + self.check(old) + + def test_missing_injection_fails_the_experiment(self): + with self.assertRaises(ValueError) as cm: + self.check(plus(inv('theorem', 'user', LOCAL, (P, 'otherName')), axioms=STD + ('sorryAx',)), + expected={('forbidden_axiom', ('sorryAx',), False), ('extra_theorem', (P, 'otherName'), False)}) + self.assertIn('did not inject', str(cm.exception)) + + def test_same_short_private_name_elsewhere_fails_the_experiment(self): + # RF312-CONTROL-PRIVATE-IDENTITY-006 (#312, 6014639706): an unrelated private theorem with + # the same short name in another module must not collapse into the expected finding. + injected = ('theorem', 'user', (P, 'compiledAdmission'), True, name(ALPHA)) + expected = {('forbidden_axiom', ('sorryAx',), False), ('extra_theorem', (P, 'compiledAdmission'), True)} + mine = ('_private',) + name(ALPHA) + (0, P, 'compiledAdmission') + other = ('_private',) + name(BETA) + (0, P, 'compiledAdmission') + alone = plus(inv('theorem', 'user', ALPHA, mine), axioms=STD + ('sorryAx',), alpha=6) + result = gate.check_admission(alone, 'compiled_admission', injected, expected, TARGETS, MODULES, False, BOUND) + self.assertEqual(result['injected'], gate.render(mine)) + both = plus(inv('theorem', 'user', ALPHA, mine), inv('theorem', 'user', BETA, other), axioms=STD + ('sorryAx',), alpha=6, beta=5) + with self.assertRaises(ValueError) as cm: + gate.check_admission(both, 'compiled_admission', injected, expected, TARGETS, MODULES, False, BOUND) + self.assertIn('unexpected reason', str(cm.exception)) + self.assertIn(gate.render(other), str(cm.exception)) + + def test_unidentifiable_private_expectation_refused(self): + injected = ('theorem', 'user', (P, 'hiddenAdmission'), True, LOCAL) + expected = {('extra_theorem', (P, 'hiddenAdmission'), True), ('extra_theorem', (P, 'otherPrivate'), True)} + with self.assertRaises(ValueError): + gate.check_admission(plus(inv('theorem', 'user', LOCAL, self.PRIVATE)), 'x', injected, expected, TARGETS, MODULES, True, BOUND) + + def test_injection_in_wrong_module_fails_the_experiment(self): + with self.assertRaises(ValueError): + self.check(plus(inv('theorem', 'user', ALPHA, self.PRIVATE), axioms=STD + ('sorryAx',), alpha=6)) + + +class SourceCheckIntegrationTests(unittest.TestCase): + def test_live_modules_pass_grammar_and_match_manifest(self): + m = gate.load_json((ROOT / 'manifest.json').read_text()) + names = [] + for path in m['source_modules']: + names.extend(P + '.' + n for n in gate.grammar_check((ROOT / path).read_text(), path)) + self.assertEqual(names, m['targets']) + + def test_required_files_bound(self): + m = gate.load_json((ROOT / 'manifest.json').read_text()) + for required in ('tests/test_inventory_gate.py', 'GATE_HARDENING.md', 'gate.py'): + self.assertIn(required, m['files']) + + +class SourceGateRegressionTests(unittest.TestCase): + """Sol's #312 source-gate regression cases, replayed against a copied formal tree.""" + MODULE = 'ResearchFormalCoreR1/AlgebraV2.lean' + + def fixture(self, extra, targets=()): + td = tempfile.TemporaryDirectory() + self.addCleanup(td.cleanup) + root = Path(td.name) / 'formal' + shutil.copytree(ROOT, root, ignore=shutil.ignore_patterns('.lake', '__pycache__', '*.pyc')) + path = root / self.MODULE + marker = '\nend ' + P + '\n' + text = path.read_text() + self.assertEqual(text.count(marker), 1) + path.write_text(text.replace(marker, '\n' + extra + '\n' + marker)) + manifest = json.loads((root / 'manifest.json').read_text()) + manifest['files'][self.MODULE] = hashlib.sha256(path.read_bytes()).hexdigest() + at = manifest['targets'].index(P + '.ec014_contact_power') + 1 + manifest['targets'][at:at] = list(targets) + (root / 'manifest.json').write_text(json.dumps(manifest, indent=2) + '\n') + return subprocess.run([sys.executable, 'gate.py'], cwd=root, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, timeout=120) + + def test_hidden_declaration_forms_are_rejected(self): + for extra in (' theorem rf_gate_indented : False := by sorry', 'private theorem rf_gate_private : False := by sorry', + '@[simp] theorem rf_gate_attributed : False := by sorry', 'def rf_gate_unused : False := by sorry', + 'opaque rf_gate_opaque : False', 'axiom rf_gate_axiom : False', + 'def rf_gate_string : String := "--" ++ "x"\nprivate theorem rf_gate_after : True := trivial'): + with self.subTest(extra=extra): + self.assertNotEqual(self.fixture(extra).returncode, 0) + + def test_comment_text_is_not_inventoried_as_a_declaration(self): + result = self.fixture('/-\ntheorem rf_gate_comment_ghost : False := by sorry\n-/') + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + + def test_duplicate_target_list_is_rejected_source_side(self): + result = self.fixture('theorem ec005_fold_gap (s : ℝ) : True := by trivial', [P + '.ec005_fold_gap']) + self.assertNotEqual(result.returncode, 0) + + def test_nested_namespace_cannot_be_misprefixed(self): + result = self.fixture('namespace Nested\ntheorem rf_gate_nested : True := by trivial\nend Nested', [P + '.rf_gate_nested']) + self.assertNotEqual(result.returncode, 0) + + +if __name__ == '__main__': + unittest.main() diff --git a/formal/tests/test_moment_generality.py b/formal/tests/test_moment_generality.py index 22672d3df..6560d01fc 100644 --- a/formal/tests/test_moment_generality.py +++ b/formal/tests/test_moment_generality.py @@ -55,7 +55,7 @@ def test_predecessor_and_gate_pins_preserved(self): pins = { 'ResearchFormalCoreR1/MomentTail.lean': '87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa', 'ResearchFormalCoreR1/WeightedLaw.lean': 'f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736', - 'gate.py': '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a', + 'gate.py': 'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4', } for path, digest in pins.items(): self.assertEqual(m['files'][path], digest) diff --git a/formal/tests/test_moment_tail.py b/formal/tests/test_moment_tail.py index d0c0869f3..aa389def4 100644 --- a/formal/tests/test_moment_tail.py +++ b/formal/tests/test_moment_tail.py @@ -57,7 +57,7 @@ def test_retained_control_and_proof_pins(self): pins = { 'ResearchFormalCoreR1/MeasureBridge.lean': '28ac130db490c3c3e2fbfabf3ac5be43c854ab1468bf573bf5a8c0dd2c50955f', 'ResearchFormalCoreR1/WeightedLaw.lean': 'f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736', - 'gate.py': '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a', + 'gate.py': 'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4', } for name, digest in pins.items(): self.assertEqual(m['files'][name], digest) diff --git a/formal/tests/test_weight_perturbation.py b/formal/tests/test_weight_perturbation.py index ce462f979..8c9efe3ff 100644 --- a/formal/tests/test_weight_perturbation.py +++ b/formal/tests/test_weight_perturbation.py @@ -65,7 +65,7 @@ def test_predecessor_and_gate_identity_contract(self): pins = { 'ResearchFormalCoreR1/WeightedLaw.lean': 'f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736', 'ResearchFormalCoreR1/MomentGenerality.lean': 'fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509', - 'gate.py': '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a', + 'gate.py': 'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4', } for path, digest in pins.items(): self.assertEqual(m['files'][path], digest) diff --git a/formal/tests/test_weighted_law.py b/formal/tests/test_weighted_law.py index ceac05678..f95157d90 100644 --- a/formal/tests/test_weighted_law.py +++ b/formal/tests/test_weighted_law.py @@ -57,7 +57,7 @@ def test_parent_proofs_and_execution_controls_retained(self): m = json.loads((ROOT/'manifest.json').read_text()) pins = { 'ResearchFormalCoreR1/MeasureBridge.lean': '28ac130db490c3c3e2fbfabf3ac5be43c854ab1468bf573bf5a8c0dd2c50955f', - 'gate.py': '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a', + 'gate.py': 'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4', 'lean-toolchain': 'd5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b', } for path, digest in pins.items(): diff --git a/tests/test_legacy_json_capture_context.py b/tests/test_legacy_json_capture_context.py new file mode 100644 index 000000000..ce21bea89 --- /dev/null +++ b/tests/test_legacy_json_capture_context.py @@ -0,0 +1,122 @@ +"""In-memory reference-context controls; no checker, PTY, spawn or replay.""" +import argparse +import contextlib +import importlib.util +import io +import os +from pathlib import Path +import sys +import unittest +from unittest import mock + +ROOT = Path(__file__).resolve().parents[1] +SPEC = importlib.util.spec_from_file_location( + 'legacy_capture_context_subject', ROOT / 'tools/legacy_json_replay.py') +HELPER = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(HELPER) + + +class SyntheticParentTTY(io.StringIO): + def isatty(self): + return True + + +def captured_standard_diagnostic(width): + """Independent stdlib parser in the actual captured-stream context.""" + stdout, stderr = io.StringIO(), io.StringIO() + with contextlib.redirect_stdout(stdout), contextlib.redirect_stderr(stderr): + parser = argparse.ArgumentParser( + prog='reference-child.py', + formatter_class=lambda prog: argparse.HelpFormatter(prog, width=width)) + parser.add_argument('--mutant', choices=HELPER.C6_CHOICES) + try: + parser.parse_args(['--mutant', 'unknown']) + except SystemExit as error: + if error.code != 2: + raise + else: + raise AssertionError('standard grammar did not reject') + if stdout.getvalue(): + raise AssertionError('standard invalid argument emitted stdout') + return stderr.getvalue().encode('utf-8') + + +class LegacyCaptureContextTests(unittest.TestCase): + def test_constructor_parse_and_real_formatter_observe_captured_stdout(self): + seen = {'constructor': [], 'parse': [], 'formatter': []} + real_init = argparse.ArgumentParser.__init__ + real_parse = argparse.ArgumentParser.parse_args + real_formatter_init = argparse.HelpFormatter.__init__ + + def formatter_init(actual, *args, **kwargs): + seen['formatter'].append(sys.stdout.isatty()) + return real_formatter_init(actual, *args, **kwargs) + + def parser_init(actual, *args, **kwargs): + seen['constructor'].append(sys.stdout.isatty()) + return real_init(actual, *args, **kwargs) + + def parse(actual, *args, **kwargs): + seen['parse'].append(sys.stdout.isatty()) + return real_parse(actual, *args, **kwargs) + + parent_out, parent_err = SyntheticParentTTY(), io.StringIO() + with contextlib.redirect_stdout(parent_out), contextlib.redirect_stderr(parent_err): + with mock.patch.object(argparse.ArgumentParser, '__init__', parser_init), \ + mock.patch.object(argparse.ArgumentParser, 'parse_args', parse), \ + mock.patch.object(argparse.HelpFormatter, '__init__', formatter_init): + result = HELPER._unknown_stderr('c6-cluster', 'reference-child.py') + self.assertIs(sys.stdout, parent_out) + self.assertIs(sys.stderr, parent_err) + self.assertTrue(result) + self.assertEqual(parent_out.getvalue(), '') + self.assertEqual(parent_err.getvalue(), '') + for phase, observations in seen.items(): + with self.subTest(phase=phase): + self.assertTrue(observations, 'real stdlib boundary was not observed') + self.assertEqual(observations, [False] * len(observations), + 'reference inherited the parent TTY instead of child capture') + + def test_exact_bytes_match_captured_standard_parser_for_width_inputs(self): + for columns, width in ((None, 78), ('35', 33), ('80', 78), ('220', 218), + (' 110 ', 108), ('', 78), ('0', 78), + ('-3', 78), ('not-a-number', 78)): + with self.subTest(columns=columns), mock.patch.dict(os.environ): + os.environ.pop('COLUMNS', None) + if columns is not None: + os.environ['COLUMNS'] = columns + expected = captured_standard_diagnostic(width) + with contextlib.redirect_stdout(SyntheticParentTTY()): + actual = HELPER._unknown_stderr('c6-cluster', 'reference-child.py') + self.assertEqual(actual, expected) + + def test_color_environment_controls_remain_unchanged(self): + controls = ('PYTHON_COLORS', 'NO_COLOR', 'FORCE_COLOR', 'TERM') + for values in ({'PYTHON_COLORS': '0'}, {'PYTHON_COLORS': '1'}, + {'NO_COLOR': '1'}, {'FORCE_COLOR': '1'}, {'TERM': 'dumb'}): + with self.subTest(values=values), mock.patch.dict(os.environ): + for key in (*controls, 'COLUMNS'): + os.environ.pop(key, None) + os.environ.update(values) + before = dict(os.environ) + expected = captured_standard_diagnostic(78) + with contextlib.redirect_stdout(SyntheticParentTTY()): + actual = HELPER._unknown_stderr('c6-cluster', 'reference-child.py') + self.assertEqual(actual, expected) + self.assertEqual(dict(os.environ), before) + + def test_parent_streams_restored_after_real_formatter_boundary_error(self): + parent_out, parent_err = SyntheticParentTTY(), io.StringIO() + with contextlib.redirect_stdout(parent_out), contextlib.redirect_stderr(parent_err): + with mock.patch.object(argparse, 'HelpFormatter', + side_effect=RuntimeError('inert fixture refusal')): + with self.assertRaisesRegex(RuntimeError, 'inert fixture refusal'): + HELPER._unknown_stderr('c6-cluster', 'reference-child.py') + self.assertIs(sys.stdout, parent_out) + self.assertIs(sys.stderr, parent_err) + self.assertEqual(parent_out.getvalue(), '') + self.assertEqual(parent_err.getvalue(), '') + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/tests/test_required_formal_check.py b/tests/test_required_formal_check.py index e9d2e6f39..6163fb182 100644 --- a/tests/test_required_formal_check.py +++ b/tests/test_required_formal_check.py @@ -5,6 +5,7 @@ import json import os from pathlib import Path +import shutil import subprocess import sys import tempfile @@ -586,3 +587,157 @@ def test_manifest_without_exact_lock_refused(self): for name in ('preflight', 'final'): self.record['observations'][name]['manifest_sha256'] = self.record['manifest_sha256'] self.refused('manifest has no exact dependency lock') + +class LayeredManifestBindingTests(unittest.TestCase): + """Real producer/consumer boundary and fail-closed overlay identity regimes.""" + setUp = RequiredCheckTests.setUp + write_receipt = RequiredCheckTests.write_receipt + binding = RequiredCheckTests.binding + CONTRACT = {'schema': 'rf312-overlay-v1', 'overlay': 'manifest.overlay.json'} + + def identity(self, digest): + self.record['manifest_sha256'] = digest + for observed in self.record['observations'].values(): + observed['manifest_sha256'] = digest + self.write_receipt() + + def layered(self): + document = json.loads(self.manifest.read_text()) + document['source_identity'] = dict(self.CONTRACT) + self.manifest.write_text(json.dumps(document) + '\n') + self.overlay = self.manifest.with_name('manifest.overlay.json') + self.overlay.write_text('{"schema_version":1,"files":{}}\n') + self.composite_receipt() + + def composite_receipt(self): + # Hand-derived contract bytes, independent of the consumer implementation. + self.identity(hashlib.sha256( + self.manifest.read_bytes() + b'\0RF312-OVERLAY\0' + + self.overlay.read_bytes()).hexdigest()) + + def test_actual_producer_source_check_receipt_binds(self): + # Exercise the actual source validator, without calling execute or any Lean process. + formal = self.root / 'formal' + shutil.copytree(ROOT / 'formal', formal, + ignore=shutil.ignore_patterns('.lake', '__pycache__', '*.pyc')) + self.manifest = formal / 'manifest.json' + prior_helper = sys.modules.pop('gate_helper', None) + try: + spec = importlib.util.spec_from_file_location('receipt_binding_producer', ROOT / 'formal/gate.py') + producer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(producer) + producer.ROOT = formal + checked, digest = producer.source_check() + finally: + if prior_helper is not None: + sys.modules['gate_helper'] = prior_helper + self.record['repository'] = self.env['GITHUB_REPOSITORY'] = 'd6g8k5htny-coder/Math-' + self.record['dependency_revisions'] = dict(checked['dependency_revisions']) + for observed in self.record['observations'].values(): + observed['dependency_revisions'] = dict(checked['dependency_revisions']) + self.identity(digest) + before = self.receipt.read_bytes() + result = self.binding() + self.assertEqual(result['checked_commit'], 'a' * 40) + self.assertEqual(result['receipt_sha256'], hashlib.sha256(before).hexdigest()) + self.assertEqual(self.receipt.read_bytes(), before) + + def test_empty_files_overlay_receipt_binds(self): + self.layered() + self.assertEqual(self.binding()['run_attempt'], '2') + + def test_raw_or_overlay_byte_drift_refused(self): + self.layered() + for path in (self.manifest, self.overlay): + with self.subTest(path=path.name): + original = path.read_bytes() + path.write_bytes(original + b' ') + try: + with self.assertRaisesRegex(ValueError, 'manifest/receipt mismatch'): + self.binding() + finally: + path.write_bytes(original) + + def test_missing_symlink_dangling_and_nonregular_overlay_refused(self): + self.layered() + original = self.overlay.read_bytes() + target = self.root / 'overlay-target.json' + target.write_bytes(original) + for kind in ('missing', 'symlink', 'dangling', 'directory'): + with self.subTest(kind=kind): + self.overlay.unlink() + if kind == 'symlink': + self.overlay.symlink_to(target) + elif kind == 'dangling': + self.overlay.symlink_to(self.root / 'absent-overlay-target.json') + elif kind == 'directory': + self.overlay.mkdir() + try: + with self.assertRaises((ValueError, OSError)): + self.binding() + finally: + if self.overlay.is_dir() and not self.overlay.is_symlink(): + self.overlay.rmdir() + elif self.overlay.is_symlink(): + self.overlay.unlink() + self.overlay.write_bytes(original) + + def test_overlay_strict_json_and_binding_shape_refused(self): + self.layered() + for raw in ( + b'{', b'[]', b'null', b'{"schema_version":1,"files":{},"files":{}}', + b'{"schema_version":NaN,"files":{}}', + b'{"schema_version":true,"files":{}}', + b'{"schema_version":2,"files":{}}', + b'{"schema_version":1,"files":[]}', + b'{"schema_version":1,"files":{"gate.py":"invalid"}}', + b'{"schema_version":1,"files":{},"targets":[]}', b'\xff', + ): + with self.subTest(raw=raw): + self.overlay.write_bytes(raw) + self.composite_receipt() + with self.assertRaises(ValueError): + self.binding() + + def test_unknown_identity_contract_never_becomes_legacy(self): + self.layered() + document = json.loads(self.manifest.read_text()) + overlay_bytes = self.overlay.read_bytes() + for value in ( + None, {}, [], 'rf312-overlay-v1', + {'schema': 'rf312-overlay-v2', 'overlay': 'manifest.overlay.json'}, + {'schema': 'rf312-overlay-v1', 'overlay': '../manifest.overlay.json'}, + {'schema': 'rf312-overlay-v1', 'overlay': '/tmp/manifest.overlay.json'}, + {'schema': 'rf312-overlay-v1', 'overlay': 'manifest.overlay.json', 'extra': True}, + ): + for present in (False, True): + with self.subTest(contract=value, overlay_present=present): + document['source_identity'] = value + self.manifest.write_text(json.dumps(document) + '\n') + if present: + self.overlay.write_bytes(overlay_bytes) + else: + self.overlay.unlink(missing_ok=True) + # A raw receipt must not make an invalid regime acceptable. + self.identity(hashlib.sha256(self.manifest.read_bytes()).hexdigest()) + with self.assertRaises(ValueError): + self.binding() + + def test_undeclared_overlay_refused_with_otherwise_valid_raw_receipt(self): + self.manifest.with_name('manifest.overlay.json').write_text( + '{"schema_version":1,"files":{}}\n') + with self.assertRaisesRegex(ValueError, 'undeclared manifest overlay'): + self.binding() + + def test_raw_receipt_cannot_downgrade_declared_overlay(self): + self.layered() + self.identity(hashlib.sha256(self.manifest.read_bytes()).hexdigest()) + with self.assertRaisesRegex(ValueError, 'manifest/receipt mismatch'): + self.binding() + + def test_missing_declared_overlay_cannot_downgrade_to_raw(self): + self.layered() + self.overlay.unlink() + self.identity(hashlib.sha256(self.manifest.read_bytes()).hexdigest()) + with self.assertRaisesRegex(ValueError, 'manifest overlay'): + self.binding() diff --git a/tools/legacy_json_replay.py b/tools/legacy_json_replay.py index 854db466a..1aa66bb31 100755 --- a/tools/legacy_json_replay.py +++ b/tools/legacy_json_replay.py @@ -118,19 +118,21 @@ def _unknown_stderr(family: str, script_name: str) -> bytes: if columns <= 0: columns = 80 # CPython 3.11--3.13 HelpFormatter subtracts two from the terminal columns. - parser = argparse.ArgumentParser( - prog=script_name, - formatter_class=lambda prog: argparse.HelpFormatter(prog, width=columns - 2)) - parser.add_argument('--mutant', choices=C6_CHOICES) stream = io.StringIO() - try: - with contextlib.redirect_stderr(stream): + # Construct and format under the child's captured stdout context as well: + # newer argparse can select colors from stdout. Keep color environment intact. + with contextlib.redirect_stdout(io.StringIO()), contextlib.redirect_stderr(stream): + parser = argparse.ArgumentParser( + prog=script_name, + formatter_class=lambda prog: argparse.HelpFormatter(prog, width=columns - 2)) + parser.add_argument('--mutant', choices=C6_CHOICES) + try: parser.parse_args(['--mutant', 'unknown']) - except SystemExit as exc: - if exc.code != 2: - raise ProtocolError('reference argument grammar did not reject') from exc - else: - raise ProtocolError('reference argument grammar unexpectedly accepted') + except SystemExit as exc: + if exc.code != 2: + raise ProtocolError('reference argument grammar did not reject') from exc + else: + raise ProtocolError('reference argument grammar unexpectedly accepted') return stream.getvalue().encode('utf-8') diff --git a/tools/required_formal_check.py b/tools/required_formal_check.py index ea5af2c89..0b9d694bd 100644 --- a/tools/required_formal_check.py +++ b/tools/required_formal_check.py @@ -68,6 +68,32 @@ def runtime_observation(value, lock: dict, name: str) -> dict: return value +def manifest_identity(manifest: Path, raw: bytes) -> str: + """Select one declared source identity; never downgrade an overlay receipt.""" + document = strict_json(raw.decode('utf-8')) + require(isinstance(document, dict), 'manifest must be an object') + overlay = manifest.with_name('manifest.overlay.json') + if 'source_identity' not in document: + require(not overlay.exists() and not overlay.is_symlink(), 'undeclared manifest overlay') + return hashlib.sha256(raw).hexdigest() + require(document['source_identity'] == { + 'schema': 'rf312-overlay-v1', 'overlay': 'manifest.overlay.json'}, + 'unsupported source identity contract') + require(not overlay.is_symlink() and overlay.is_file(), + 'missing or nonregular manifest overlay') + overlay_raw = overlay.read_bytes() + value = strict_json(overlay_raw.decode('utf-8')) + require(isinstance(value, dict) and set(value) == {'schema_version', 'files'}, + 'invalid manifest overlay keys') + require(type(value['schema_version']) is int and value['schema_version'] == 1 + and isinstance(value['files'], dict), 'invalid manifest overlay schema') + require(all(isinstance(name, str) and isinstance(digest, str) + and re.fullmatch(r'[0-9a-f]{64}', digest) is not None + for name, digest in value['files'].items()), + 'invalid manifest overlay file binding') + return hashlib.sha256(raw + b'\0RF312-OVERLAY\0' + overlay_raw).hexdigest() + + def bind_receipt(receipt: Path, manifest: Path, env: dict, git_head: str) -> dict: ctx = context(env) require(git_head == ctx['checked_commit'], 'checkout/tested commit mismatch') @@ -81,12 +107,13 @@ def bind_receipt(receipt: Path, manifest: Path, env: dict, git_head: str) -> dic ('formalization_status', 'kernel-checked'), ('scientific_effect', 'NONE')]: require(record.get(key) == expected, 'receipt mismatch: '+key) - require(record.get('manifest_sha256') == hashlib.sha256(manifest.read_bytes()).hexdigest(), + manifest_raw = manifest.read_bytes() + require(record.get('manifest_sha256') == manifest_identity(manifest, manifest_raw), 'manifest/receipt mismatch') # The producer's runtime fields are validated, not only hashed: the exact release, the # locked and clean dependencies, this attempt, and equal observations before the first # and after the last Lean execution. A missing or older-schema field refuses. - lock = dependency_lock(manifest.read_bytes()) + lock = dependency_lock(manifest_raw) require(record.get('workflow_run_attempt') == ctx['run_attempt'], 'receipt mismatch: workflow_run_attempt') require(isinstance(record.get('lean_version'), str) and LEAN_RELEASE.fullmatch(record['lean_version']) is not None, 'receipt runtime is not the pinned Lean release')