Formal gate: reject ambiguous declared proposers and preserve source-bound review checks

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.

formal/gate.py

@@ -56,17 +56,45 @@ 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')
     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')
-    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')

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"
   }
 }

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()

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)