Signal Reconstruction

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 #!/usr/bin/env python3
2 """Audit publication integration and preserved evidence; this is not a proof checker."""
3 from pathlib import Path
4 import collections
5 import hashlib
6 import json
7 import re
8 import fitz
9 
10 ROOT = Path(__file__).resolve().parent
11 DOCUMENTS = {
12     'traditional': 'Signal_Reconstruction_Traditional',
13     'visual': 'Signal_Reconstruction_Visual_Guide',
14     'lean': 'Signal_Reconstruction_Lean_Guide',
15 }
16 
17 def digest(path):
18     return hashlib.sha256(path.read_bytes()).hexdigest()
19 
20 def tex_graph(main):
21     seen, contents = set(), []
22     def visit(path):
23         path = path.resolve()
24         if path in seen:
25             return
26         if not path.is_relative_to(ROOT):
27             raise ValueError(f'TeX input outside this bundle: {path}')
28         seen.add(path)
29         source = path.read_text(encoding='utf-8')
30         contents.append(re.sub(r'(?<!\\)%[^\n]*', '', source))
31         for name in re.findall(r'\\(?:input|include)\s*\{([^}]+)\}', source):
32             if '#' in name:
33                 continue
34             candidate = path.parent / name
35             visit(candidate if candidate.suffix else candidate.with_suffix('.tex'))
36     visit(main)
37     return '\n'.join(contents), [p.relative_to(ROOT).as_posix() for p in sorted(seen)]
38 
39 def main():
40     checks, documents = [], {}
41     def check(name, passed, detail=None):
42         checks.append({'check': name, 'passed': bool(passed), 'detail': detail})
43 
44     preservation = json.loads((ROOT / 'verification/SOURCE_PRESERVATION.json').read_text())
45     originals = [f for group in preservation['sources'] for f in group['files']]
46     changed = [f['release_path'] for f in originals
47                if not (ROOT / f['release_path']).is_file()
48                or digest(ROOT / f['release_path']) != f['sha256']]
49     check('preserved_signal_payload_hashes', not changed, {'payloads': len(originals), 'changed': changed})
50     related = json.loads((ROOT / 'provenance/PAPER_V_CHECKED_CHECKPOINT.json').read_text())
51     changed_related = [f['release_path'] for f in related['copied_payloads']
52                        if not (ROOT / f['release_path']).is_file()
53                        or digest(ROOT / f['release_path']) != f['sha256']]
54     check('preserved_related_formal_payload_hashes', not changed_related,
55           {'payloads': len(related['copied_payloads']), 'changed': changed_related})
56     check('malformed_latest_archive_failure_disclosed',
57           (ROOT / 'provenance/PAPER_V_FINAL_ARCHIVE_FAILURE.json').is_file())
58 
59     label_sets, tex_sources = {}, {}
60     for folder, stem in DOCUMENTS.items():
61         tex = ROOT / folder / (stem + '.tex')
62         md, pdf = tex.with_suffix('.md'), tex.with_suffix('.pdf')
63         combined, inputs = tex_graph(tex)
64         tex_sources[folder] = combined
65         labels = re.findall(r'\\label\s*\{([^}]+)\}', combined)
66         label_sets[folder] = set(labels)
67         duplicate = sorted(k for k, v in collections.Counter(labels).items() if v > 1)
68         references = [part.strip() for group in re.findall(
69             r'\\(?:ref|eqref|autoref|cref|Cref)\*?\s*\{([^}]+)\}', combined)
70             for part in group.split(',')]
71         unresolved = sorted(set(references) - set(labels))
72         check(folder + '_unique_labels', not duplicate, duplicate)
73         check(folder + '_resolved_cross_references', not unresolved, unresolved)
74         data = md.read_bytes()
75         controls = [(i, b) for i, b in enumerate(data) if b < 32 and b not in {9, 10}]
76         check(folder + '_markdown_present_and_clean', len(data) > 1000 and not controls,
77               {'bytes': len(data), 'control_characters': controls[:10]})
78         log = tex.with_suffix('.log')
79         warnings = [line for line in log.read_text(errors='replace').splitlines()
80                     if any(term in line for term in ['Overfull', 'undefined references',
81                        'undefined citations', 'multiply defined'])] if log.is_file() else ['Missing build log']
82         check(folder + '_no_material_tex_warnings', not warnings, warnings)
83         with fitz.open(pdf) as doc:
84             outside, empty = [], []
85             for number, page in enumerate(doc, 1):
86                 if not page.get_text().strip():
87                     empty.append(number)
88                 for block in page.get_text('dict')['blocks']:
89                     for line in block.get('lines', []):
90                         for span in line['spans']:
91                             if not span.get('text', '').strip():
92                                 continue
93                             box = fitz.Rect(span['bbox']) * page.rotation_matrix
94                             rect = page.rect
95                             if (box.x0 < rect.x0 - 1 or box.y0 < rect.y0 - 1
96                                 or box.x1 > rect.x1 + 1 or box.y1 > rect.y1 + 1):
97                                 outside.append({'page': number, 'text': span['text'][:100]})
98             check(folder + '_text_within_pages', not outside, outside[:20])
99             check(folder + '_no_empty_text_pages', not empty, empty)
100             pages = len(doc)
101         documents[folder] = {'path': pdf.relative_to(ROOT).as_posix(), 'pages': pages,
102                              'bytes': pdf.stat().st_size, 'sha256': digest(pdf),
103                              'tex_inputs': inputs, 'labels': len(labels),
104                              'references': len(references), 'markdown_bytes': len(data)}
105 
106     concordance_file = ROOT / 'traditional/Claim_Concordance.json'
107     concordance = json.loads(concordance_file.read_text())
108     claims = concordance['claims'] if isinstance(concordance, dict) else concordance
109     ids = [c['claim_id'] for c in claims]
110     check('principal_claim_ids_unique', len(ids) > 0 and len(set(ids)) == len(ids), {'count': len(ids)})
111     scope_missing, labels_missing, anchors_bad, printed_missing, dependencies_bad = [], [], [], [], []
112     for claim in claims:
113         cid = claim['claim_id']
114         if not claim.get('domain') or not claim.get('hypotheses'):
115             scope_missing.append(cid)
116         if claim.get('document_label') not in label_sets['traditional']:
117             labels_missing.append(cid)
118         if claim.get('hypotheses_tex', claim.get('hypotheses')) not in tex_sources['traditional']:
119             printed_missing.append(cid)
120         for dependency in claim.get('dependencies', []):
121             if dependency not in ids:
122                 dependencies_bad.append({'claim': cid, 'dependency': dependency})
123         for anchor in claim.get('source_anchors', claim.get('anchors', [])):
124             path_value = anchor.get('path', anchor.get('file', anchor.get('source_path')))
125             hash_value = anchor.get('sha256', anchor.get('source_sha256'))
126             if not path_value or not hash_value or not (ROOT / path_value).is_file():
127                 anchors_bad.append({'claim': cid, 'anchor': anchor})
128             elif digest(ROOT / path_value) != hash_value:
129                 anchors_bad.append({'claim': cid, 'path': path_value, 'reason': 'hash mismatch'})
130     check('principal_claim_domains_and_hypotheses', not scope_missing, scope_missing)
131     check('principal_claim_document_labels', not labels_missing, labels_missing)
132     check('principal_claim_anchor_hashes', not anchors_bad, anchors_bad)
133     check('principal_claim_hypotheses_printed', not printed_missing, printed_missing)
134     check('principal_claim_dependencies_exist', not dependencies_bad, dependencies_bad)
135     check('principal_claim_markdown_ids',
136           all(cid in (ROOT / 'traditional/Signal_Reconstruction_Traditional.md').read_text() for cid in ids))
137     lean_map = json.loads((ROOT / 'lean/Claim_Lean_Concordance.json').read_text())
138     lean_by_id = {c['claim_id']: c for c in lean_map['claims']}
139     stale_claims = []
140     for claim in claims:
141         counterpart = lean_by_id.get(claim['claim_id'])
142         if counterpart is None or any(counterpart.get(field) != claim.get(field)
143                                       for field in ['title', 'statement_tex', 'hypotheses', 'hypotheses_tex', 'domain']):
144             stale_claims.append(claim['claim_id'])
145     check('lean_concordance_exact_live_claim_fields', not stale_claims and set(lean_by_id) == set(ids), stale_claims)
146     check('lean_concordance_live_input_hash', lean_map['traditional_claim_input_sha256'] == digest(concordance_file))
147     inventory = json.loads((ROOT / 'lean/Related_Declaration_Inventory.json').read_text())
148     declarations = {d['name']: d for d in inventory}
149     bad_declarations = []
150     for counterpart in lean_map['claims']:
151         for anchor in counterpart['related_declarations']:
152             item = declarations.get(anchor['declaration'])
153             source = ROOT / anchor['file']
154             if (item is None or item['file'] != anchor['file']
155                 or item['source_sha256'] != anchor['source_sha256']
156                 or digest(source) != anchor['source_sha256']
157                 or anchor['source_quoted'] not in source.read_text()):
158                 bad_declarations.append({'claim': counterpart['claim_id'], 'declaration': anchor['declaration']})
159     check('lean_concordance_related_source_anchors', not bad_declarations, bad_declarations)
160     literal_anchors = json.loads((ROOT / 'lean/SOURCE_ANCHORS.json').read_text())['anchors']
161     literal_bad = []
162     for anchor in literal_anchors:
163         source = ROOT / anchor['file']
164         quoted = '\n'.join(source.read_text().splitlines()[anchor['start_line'] - 1:anchor['end_line']])
165         if digest(source) != anchor['source_sha256'] or quoted != anchor['source_quoted']:
166             literal_bad.append(anchor['anchor_id'])
167     check('lean_guide_literal_source_excerpts', not literal_bad, {'anchors': len(literal_anchors), 'mismatches': literal_bad})
168     mapping_audit = json.loads((ROOT / 'lean/CLAIM_MAPPING_AUDIT.json').read_text())
169     check('lean_coverage_is_scoped', mapping_audit['full_signal_claims_formally_covered'] == 0
170           and mapping_audit['fresh_lean_execution'] is False)
171     crosswalk = json.loads((ROOT / 'visual/validation/claim_crosswalk.json').read_text())
172     check('visual_crosswalk_current_catalogue_hash',
173           crosswalk['source_concordance_sha256'] == digest(concordance_file))
174     check('visual_crosswalk_covers_all_claims', set(crosswalk['traditional_groups_covered']) == set(ids)
175           and {r['claim_id'] for r in crosswalk['rows']} == set(ids))
176     bad_visual_labels = [r['claim_id'] for r in crosswalk['rows']
177                          if r['document_label'] not in label_sets['visual']]
178     check('visual_crosswalk_labels_exist', not bad_visual_labels, bad_visual_labels)
179     execution_file = ROOT / 'verification/CURRENT_RELEASE_VERIFICATION.json'
180     execution = json.loads(execution_file.read_text())
181     check('current_bounded_verification_record_present', bool(execution))
182     active = execution['active_suites']
183     bad_execution_hashes = []
184     for suite in active:
185         for field in ['manifest', 'scientific_result']:
186             if digest(ROOT / suite[field]) != suite[field + '_sha256']:
187                 bad_execution_hashes.append({'suite': suite['suite'], 'field': field})
188     check('active_evidence_live_hashes', not bad_execution_hashes, bad_execution_hashes)
189     check('active_suite_names_unique', len({s['suite'] for s in active}) == len(active))
190     check('active_check_counts_consistent',
191           sum(s['recorded_checks'] for s in active) == execution['recorded_check_count']
192           and sum(s['counted_unique_checks'] for s in active) == execution['deduplicated_recorded_check_count'])
193     validation = json.loads((ROOT / 'verification/FINAL_EVIDENCE_VALIDATION.json').read_text())
194     stale_validation = [r['manifest'] for r in validation['records']
195                         if digest(ROOT / r['manifest']) != r['manifest_sha256']]
196     check('all_v2_evidence_records_validated', validation['status'] == 'PASS' and not stale_validation,
197           {'records': validation['record_count'], 'stale': stale_validation})
198     historical_status = ROOT / 'visual/validation/HISTORICAL_RUN_STATUS.json'
199     check('evidence_historical_root_declaration_current',
200           validation.get('historical_root_declaration_sha256') == digest(historical_status))
201     traditional_review = json.loads((ROOT / 'reviews/FINAL_TRADITIONAL_AUDIT.json').read_text())
202     visual_review = json.loads((ROOT / 'reviews/FINAL_VISUAL_AUDIT.json').read_text())
203     lean_review = json.loads((ROOT / 'reviews/FINAL_LEAN_AUDIT.json').read_text())
204     review_stale = []
205     for review, entries in [('traditional', traditional_review['artifacts']),
206                             ('visual', visual_review['final_artifacts'])]:
207         review_stale.extend({'review': review, 'path': entry['path']} for entry in entries
208                             if digest(ROOT / entry['path']) != entry['sha256'])
209     review_stale.extend({'review': 'lean', 'path': path}
210                         for path, sha in lean_review['frozen_artifacts'].items()
211                         if digest(ROOT / path) != sha)
212     check('independent_review_bindings_current', not review_stale, review_stale)
213     lean = json.loads((ROOT / 'verification/FRESH_LEAN_STATUS.json').read_text())
214     check('fresh_lean_scope_explicit', lean['fresh_signal_lean_check'] is False)
215     result = {'status': 'PASS_DOCUMENT_AND_SOURCE_INTEGRATION' if all(c['passed'] for c in checks) else 'FAIL',
216               'scope': 'Publication, hash, label, PDF-bound and evidence-presence checks; no new formal proof.',
217               'documents': documents, 'total_pdf_pages': sum(d['pages'] for d in documents.values()),
218               'principal_claim_groups': len(claims), 'preserved_signal_payloads': len(originals),
219               'preserved_related_formal_payloads': len(related['copied_payloads']),
220               'checks': checks, 'fresh_lean': lean,
221               'claim_concordance_sha256': digest(concordance_file),
222               'bounded_verification_sha256': digest(execution_file)}
223     (ROOT / 'PUBLICATION_AUDIT.json').write_text(json.dumps(result, indent=2) + '\n')
224     print(json.dumps({'status': result['status'], 'checks': len(checks),
225                       'total_pdf_pages': result['total_pdf_pages'],
226                       'failed': [c for c in checks if not c['passed']]}))
227     if result['status'] == 'FAIL':
228         raise SystemExit(1)
229 
230 if __name__ == '__main__':
231     main()

Back to source controls

Back to Signal Reconstruction