From dc5ebe46f65febb19f9548ee31a0830c74e70479 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 09:48:37 -0700 Subject: [PATCH] Harden declared alignment lineage without changing Lean proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reject placeholder identities and check every declared proposer; bind 23 new regression tests and validation scope. Preserve all Lean source, target inventory, execution/axiom/negative-control functions, workflows and scientific state. Dylan Roy — delegated AI work. Implementer OpenAI / GPT-6 Astra Pro, session github-meaningful-advance-20261005T1610Z. Scientific effect NONE. --- formal/LINEAGE_VALIDATION.md | 76 +++++++++++ formal/gate.py | 38 +++++- formal/manifest.json | 10 +- formal/tests/test_alignment_lineage.py | 181 +++++++++++++++++++++++++ formal/tests/test_moment_tail.py | 2 +- formal/tests/test_weighted_law.py | 2 +- 6 files changed, 298 insertions(+), 11 deletions(-) create mode 100644 formal/LINEAGE_VALIDATION.md create mode 100644 formal/tests/test_alignment_lineage.py diff --git a/formal/LINEAGE_VALIDATION.md b/formal/LINEAGE_VALIDATION.md new file mode 100644 index 000000000..5a0c5d20e --- /dev/null +++ b/formal/LINEAGE_VALIDATION.md @@ -0,0 +1,76 @@ +# Declared-author lineage validation + +Scientific effect: **NONE**. This is an engineering successor to the validator, +not an alignment acceptance, new proof, or scientific-status authority. +Implementer: OpenAI / GPT-6 Astra Pro, ChatGPT session +`github-meaningful-advance-20261005T1610Z`, acting under Dylan Roy's delegation. +Pickup: main#229 comment 5998762623. + +## Observed gap and bounded repair + +The previous `check_alignment` compared only `author` and `reviewer`. It ignored +`proposal_authors` even when a record expressly named an unknown or same-provider +proposer. It also treated literal UNKNOWN identities as ordinary nonempty strings. +Thus an ACCEPTED disposition could pass the structural validator despite declared +lineage contradicting [SCOPE's review contract](SCOPE.md#review-contract). +This is not evidence that a controller accepted a false review or that a theorem +passed on an invalid proof. Reviewers withheld the relevant candidate correctly. + +The successor validates `provider`, `family`, and `agent` for the main author, +reviewer, and **every declared proposer**. Values must be nonempty strings. +Whitespace is collapsed and comparisons are case-insensitive. The following exact +normalized placeholders are rejected: `unknown`, `unverified`, `unspecified`, +`tbd`, `n/a`, `none`, `null`, `?`, `not known`, and `not available`. +Every author's three normalized fields must differ from the reviewer's respective +fields, preserving the existing single-author distinctness rule. + +An absent `proposal_authors` retains the historical single-author record shape. +An explicit empty list is valid. A present collection must be a list of identity +objects. Each proposer's optional `targets` must be a nonempty, duplicate-free +list of names in the reviewed target inventory. Omitting that field does not +exempt the proposer from the package's identity checks. Contributor `pr` labels +are descriptive metadata, not authentication. + +## Boundaries that remain external + +This validator cannot discover undeclared proposers, identify model aliases, +authenticate a claimed provider/session, or infer a provider from a role or app +name. It does not prove that all contributors were listed. A controller must still +read the immutable source, native reviewer evidence and contributor history. +Unknown lineage must not be replaced by an invented provider to pass the check. +This change neither authorizes a waiver nor creates a composite-review rule. + +Manifest/scope digests, full target coverage, ACCEPTED disposition and immutable +evidence references remain required. No existing withheld record is edited by +this change. Old accepted records remain records of their old exact manifests; +the new manifest must not be substituted into them without a fresh review. + +## Source preservation and regression checks + +No Lean declaration, target, toolchain, dependency revision, historical proof, +workflow, axiom audit, build/recheck command or executable negative control is +changed. `source_check` additionally requires this note and +`tests/test_alignment_lineage.py` to be hash-bound. The two older Python tests +that pin the whole gate now pin this separately scoped successor; their proof +and toolchain pins and all other test logic are unchanged. + +The new suite has 23 test methods, including role/field/placeholder subcases, +malformed identities, matching proposer identities, valid legacy and declared +proposer records, retained digest/coverage checks and omitted source bindings. +Against the old gate it reported 132 failing subcases and 8 malformed-party +errors in each Python mode. After repair all 23 methods passed in both modes. +The fixtures are synthetic, not fabricated review evidence. + +```sh +python3 -B -S -m unittest discover -s formal/tests -p test_alignment_lineage.py -v +python3 -B -O -S -m unittest discover -s formal/tests -p test_alignment_lineage.py -v +python3 -m unittest discover -s formal/tests -v +python3 -O -m unittest discover -s formal/tests -v +python3 formal/gate.py +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. +Local focused tests are not a Lean kernel replay or independent review. diff --git a/formal/gate.py b/formal/gate.py index 2732c6050..f946c38aa 100644 --- a/formal/gate.py +++ b/formal/gate.py @@ -56,6 +56,20 @@ def check_blueprint(text, targets): 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') @@ -63,10 +77,24 @@ def check_alignment(review, manifest_digest, targets, scope_digest): 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') - a, r = review.get('author', {}), review.get('reviewer', {}) - for key in ('provider', 'family', 'agent'): - require(isinstance(a.get(key), str) and a[key].strip() and isinstance(r.get(key), str) and r[key].strip(), 'missing review lineage') - require(a[key].strip().casefold() != r[key].strip().casefold(), 'lineage not independent: ' + key) + 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') @@ -89,7 +117,7 @@ def source_check(): 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'} + 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') diff --git a/formal/manifest.json b/formal/manifest.json index 025074f1e..5ca70095b 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -75,7 +75,7 @@ "SCOPE.md": "21c4ce34ff1e7536c88de86661c796a0751ad8572b034650631052ad0791f4a1", "blueprint/src/content.tex": "e00ee78344ed27c097bccb8c6360f6bb86a223ab06319a407de2dd0104fd2e28", "evidence/initial-build-failure.log": "43393d2e2b3148a2453e3092a1ff04e257dbd4a6dc97eb2853a8bc0451002591", - "gate.py": "4f14a78bbc6e9b7f929648b13ad3a9ae467256db4be9792e3667680e697a5c94", + "gate.py": "958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68", "lake-manifest.json": "d63753befccc21923783a5085148e3ff028d97134ea52f5a08bd87ecf1b0b043", "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255", "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", @@ -87,10 +87,12 @@ "tests/test_measure_bridge.py": "0e54b2ed7c2e197967180993b4c0c1ece1e63576ad34fd74ac232a4d507628a2", "ResearchFormalCoreR1/WeightedLaw.lean": "f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736", "WEIGHTED_LAW.md": "a530dc957923c4c9111b734d8fcc0f4cd3cdba45b08480cfc2e241ecefc5fba4", - "tests/test_weighted_law.py": "a65005e48c356175592cdc24c02270825dcf11d80975134c072775c693667607", + "tests/test_weighted_law.py": "e4cb5f2cdc58ac1e3af09b548c6dbb24ff3f060a101636589d2db994c0d66b94", "ResearchFormalCoreR1/MomentTail.lean": "87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa", "MOMENT_TAIL.md": "20ecddcd830c41935dc4b366882db4d0432240932af6632d025b981f90e044bd", - "tests/test_moment_tail.py": "a75c575bc0e1853f3a597c338085932aefe05b52e8ea3bcf3277f5cc3753ec81", - "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08" + "tests/test_moment_tail.py": "d5cafe83b3d7afa575cc521e7b6617b4535af217ecab02316307eebbe28a175a", + "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08", + "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893", + "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815" } } diff --git a/formal/tests/test_alignment_lineage.py b/formal/tests/test_alignment_lineage.py new file mode 100644 index 000000000..86636772d --- /dev/null +++ b/formal/tests/test_alignment_lineage.py @@ -0,0 +1,181 @@ +"""Declared-lineage validation only; synthetic fixtures do not authenticate agents.""" +import copy +import importlib.util +import json +import tempfile +from pathlib import Path +import unittest + +ROOT = Path(__file__).resolve().parents[1] +SPEC = importlib.util.spec_from_file_location('lineage_gate_under_test', ROOT / 'gate.py') +gate = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(gate) + +TARGETS = ['ResearchFormalCoreR1.first', 'ResearchFormalCoreR1.second'] +MANIFEST, SCOPE = 'a' * 64, 'b' * 64 + + +def valid_review(): + return { + 'disposition': 'ACCEPTED', 'manifest_sha256': MANIFEST, + 'scope_sha256': SCOPE, 'targets': list(TARGETS), + 'author': {'provider': 'Author Provider', 'family': 'Author Family', 'agent': 'author-session'}, + 'reviewer': {'provider': 'Reviewer Provider', 'family': 'Reviewer Family', 'agent': 'review-session'}, + 'evidence': {'repository': 'fixture/repository', 'path': 'reviews/fixture.md', + 'commit': 'c' * 40, 'sha256': 'd' * 64}, + } + + +def proposer(): + return {'provider': 'Proposal Provider', 'family': 'Proposal Family', 'agent': 'proposal-session', + 'targets': [TARGETS[0]], 'pr': 'fixture#1'} + + +class AlignmentLineageTests(unittest.TestCase): + def check(self, review): + return gate.check_alignment(review, MANIFEST, TARGETS, SCOPE) + + def reject(self, review, reason='lineage'): + with self.assertRaisesRegex(ValueError, reason): + self.check(review) + + def test_legacy_single_author_record(self): + self.check(valid_review()) + + def test_known_distinct_proposer(self): + r = valid_review(); r['proposal_authors'] = [proposer()] + self.check(r) + + def test_explicit_empty_proposer_list(self): + r = valid_review(); r['proposal_authors'] = [] + self.check(r) + + def test_unscoped_known_proposer(self): + r = valid_review(); p = proposer(); del p['targets']; r['proposal_authors'] = [p] + self.check(r) + + def test_every_declared_proposer_is_checked(self): + r = valid_review(); p = proposer(); p['provider'] = r['reviewer']['provider'] + r['proposal_authors'] = [proposer(), p] + self.reject(r) + + def test_same_proposer_provider(self): + r = valid_review(); p = proposer(); p['provider'] = r['reviewer']['provider'] + r['proposal_authors'] = [p]; self.reject(r) + + def test_same_proposer_family(self): + r = valid_review(); p = proposer(); p['family'] = r['reviewer']['family'] + r['proposal_authors'] = [p]; self.reject(r) + + def test_same_proposer_agent(self): + r = valid_review(); p = proposer(); p['agent'] = r['reviewer']['agent'] + r['proposal_authors'] = [p]; self.reject(r) + + def test_proposer_identity_normalization(self): + r = valid_review(); p = proposer(); p['provider'] = ' REVIEWER\tPROVIDER ' + r['proposal_authors'] = [p]; self.reject(r) + + def test_primary_identity_normalization(self): + r = valid_review(); r['author']['provider'] = ' REVIEWER\tPROVIDER ' + self.reject(r) + + def test_placeholder_lineage_in_all_roles(self): + for role in ('author', 'reviewer', 'proposal'): + for key in ('provider', 'family', 'agent'): + for value in ('UNKNOWN', ' unknown ', 'Unverified', 'UNSPECIFIED', 'TBD', + 'N/A', 'NONE', 'null', '?', 'not known', 'Not Available'): + with self.subTest(role=role, key=key, value=value): + r = valid_review(); p = proposer(); r['proposal_authors'] = [p] + (p if role == 'proposal' else r[role])[key] = value + self.reject(r) + + def test_missing_proposer_identity_field(self): + for key in ('provider', 'family', 'agent'): + with self.subTest(key=key): + r = valid_review(); p = proposer(); del p[key]; r['proposal_authors'] = [p] + self.reject(r) + + def test_blank_or_nonstring_proposer_identity(self): + for value in ('', ' \t\n ', None, 7, [], {}): + with self.subTest(value=value): + r = valid_review(); p = proposer(); p['provider'] = value + r['proposal_authors'] = [p]; self.reject(r) + + def test_malformed_primary_and_reviewer_objects(self): + for role in ('author', 'reviewer'): + for value in (None, [], 'provider', 7): + with self.subTest(role=role, value=value): + r = valid_review(); r[role] = value; self.reject(r) + + def test_malformed_proposer_collection(self): + for value in (None, {}, 'provider', 7): + with self.subTest(value=value): + r = valid_review(); r['proposal_authors'] = value; self.reject(r) + + def test_malformed_proposer_object(self): + for value in (None, [], 'provider', 7): + with self.subTest(value=value): + r = valid_review(); r['proposal_authors'] = [value]; self.reject(r) + + def test_invalid_proposer_target_scope(self): + for value in ([], [TARGETS[0], TARGETS[0]], ['Unreviewed.target'], + None, TARGETS[0], [1], [{}]): + with self.subTest(value=value): + r = valid_review(); p = proposer(); p['targets'] = value + r['proposal_authors'] = [p]; self.reject(r, 'proposal target') + + def test_withheld_record_remains_rejected(self): + r = valid_review(); r['disposition'] = 'WITHHELD_PROPOSER_LINEAGE_UNKNOWN' + p = proposer(); p['provider'] = 'UNKNOWN'; r['proposal_authors'] = [p] + self.reject(r, 'alignment not accepted') + + def test_disposition_only_edit_cannot_hide_unknown_proposer(self): + r = valid_review(); p = proposer(); p['provider'] = p['family'] = 'UNKNOWN' + r['proposal_authors'] = [p] + self.reject(r) + + def test_input_not_mutated(self): + r = valid_review(); r['proposal_authors'] = [proposer()]; original = copy.deepcopy(r) + self.check(r); self.assertEqual(r, original) + + def test_existing_digest_scope_and_coverage_checks(self): + for key, value in (('manifest_sha256', 'e' * 64), ('scope_sha256', 'f' * 64), + ('targets', [TARGETS[0]])): + with self.subTest(key=key): + r = valid_review(); r[key] = value + with self.assertRaises(ValueError): self.check(r) + + + def assert_required_lineage_file(self, omitted): + # Fail at the required-file inventory before accessing any source bytes. + 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'} + files = {name: '0' * 64 for name in required if name != omitted} + files.update({ + 'originals/Algebra.lean.txt': '4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae', + 'originals/ProbabilityCompanions.lean.txt': '4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d', + 'COMPATIBILITY.md': '0' * 64, + }) + manifest = {'schema_version': 1, 'scientific_effect': 'NONE', + 'formalization_status': 'proved', 'alignment_status': 'PENDING_INDEPENDENT_REVIEW', + 'files': files} + old_root = gate.ROOT + with tempfile.TemporaryDirectory() as directory: + gate.ROOT = Path(directory) + try: + (gate.ROOT / 'manifest.json').write_text(json.dumps(manifest)) + with self.assertRaisesRegex(ValueError, 'unbound control or scope file'): + gate.source_check() + finally: + gate.ROOT = old_root + + def test_lineage_tests_cannot_be_unbound(self): + self.assert_required_lineage_file('tests/test_alignment_lineage.py') + + def test_lineage_scope_cannot_be_unbound(self): + self.assert_required_lineage_file('LINEAGE_VALIDATION.md') + +if __name__ == '__main__': + unittest.main() diff --git a/formal/tests/test_moment_tail.py b/formal/tests/test_moment_tail.py index 4234e2478..2c222b948 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': '4f14a78bbc6e9b7f929648b13ad3a9ae467256db4be9792e3667680e697a5c94', + 'gate.py': '958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68', } for name, digest in pins.items(): self.assertEqual(m['files'][name], digest) diff --git a/formal/tests/test_weighted_law.py b/formal/tests/test_weighted_law.py index 030951deb..804ff608b 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': '4f14a78bbc6e9b7f929648b13ad3a9ae467256db4be9792e3667680e697a5c94', + 'gate.py': '958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68', 'lean-toolchain': 'd5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b', } for path, digest in pins.items():