Sufficient Resolution

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 """Verify publication sources, inventories, original-source preservation, and PDFs."""
3 from pathlib import Path
4 import collections
5 import csv
6 import hashlib
7 import io
8 import json
9 import re
10 import zipfile
11 import fitz
12 
13 ROOT = Path(__file__).resolve().parent
14 ORIGINAL = ROOT / 'provenance' / 'Komorebi_Sufficient_Resolution_Lean_v0.16.0.zip'
15 EXPECTED_ORIGINAL = 'ebb2d71a211ea9938c1b223f9858d5636d0973b5aa519244667200646b832ff4'
16 DOCUMENTS = [
17     ('traditional', 'Sufficient_Resolution_Traditional'),
18     ('visual', 'Sufficient_Resolution_Visual_Guide'),
19     ('lean', 'Sufficient_Resolution_Lean_Guide'),
20 ]
21 
22 def digest(path):
23     return hashlib.sha256(path.read_bytes()).hexdigest()
24 
25 def tex_graph(main):
26     seen = set()
27     texts = []
28     def visit(path):
29         path = path.resolve()
30         if path in seen:
31             return
32         if not path.is_relative_to(ROOT):
33             raise ValueError(f'TeX source outside the bundle: {path}')
34         seen.add(path)
35         source = path.read_text(encoding='utf-8')
36         source = re.sub(r'(?<!\\)%[^\n]*', '', source)
37         texts.append(source)
38         for name in re.findall(r'\\(?:input|include)\s*\{([^}]+)\}', source):
39             candidate = path.parent / name
40             if candidate.suffix == '':
41                 candidate = candidate.with_suffix('.tex')
42             visit(candidate)
43     visit(main)
44     return '\n'.join(texts), sorted(str(p.relative_to(ROOT)) for p in seen)
45 
46 def main():
47     checks = []
48     details = {}
49     def check(name, ok, detail=None):
50         checks.append({'check': name, 'passed': bool(ok), 'detail': detail})
51     check('original_archive_sha256', digest(ORIGINAL) == EXPECTED_ORIGINAL)
52     with zipfile.ZipFile(ORIGINAL) as z:
53         check('original_archive_crc', z.testzip() is None)
54         prefix = 'Komorebi_Sufficient_Resolution_Lean_v0.16.0/'
55         source_names = sorted(n for n in z.namelist()
56                               if n.startswith(prefix + 'Komorebi/') and n.endswith('.lean'))
57         changed = []
58         for name in source_names:
59             local = ROOT / 'formal' / name[len(prefix):]
60             if not local.is_file() or local.read_bytes() != z.read(name):
61                 changed.append(name[len(prefix):])
62         check('93_production_sources_preserved', len(source_names) == 93 and not changed, changed)
63         original_index = list(csv.DictReader(io.StringIO(
64             z.read(prefix + 'DECLARATION_INDEX_v0.16.0.csv').decode('utf-8'))))
65     with (ROOT / 'lean' / 'Declaration_Inventory.csv').open(newline='', encoding='utf-8') as f:
66         declarations = list(csv.DictReader(f))
67     with (ROOT / 'lean' / 'Module_Inventory.csv').open(newline='', encoding='utf-8') as f:
68         modules = list(csv.DictReader(f))
69     original_names = {(x['name'], x['kind'], x['file']) for x in original_index}
70     release_names = {(x['name'], x['kind'], x['file']) for x in declarations}
71     check('declaration_inventory_matches_original', original_names == release_names
72           and len(declarations) == 1159)
73     check('module_inventory_count', len(modules) == 93)
74     module_mismatches = [x['file'] for x in modules
75                          if digest(ROOT / 'formal' / x['file']) != x['sha256']]
76     check('module_inventory_live_hashes', not module_mismatches, module_mismatches)
77     declaration_mismatches = [x['name'] for x in declarations
78                               if digest(ROOT / 'formal' / x['file']) != x['source_sha256']]
79     check('declaration_inventory_live_hashes', not declaration_mismatches,
80           declaration_mismatches)
81     kinds = dict(collections.Counter(x['kind'] for x in declarations))
82     check('formal_declaration_kind_counts',
83           kinds == {'theorem': 998, 'def': 144, 'abbrev': 9, 'structure': 8}, kinds)
84 
85     document_labels = {}
86     for folder, stem in DOCUMENTS:
87         tex = ROOT / folder / (stem + '.tex')
88         md = tex.with_suffix('.md')
89         pdf = tex.with_suffix('.pdf')
90         combined, sources = tex_graph(tex)
91         labels = re.findall(r'\\label\s*\{([^}]+)\}', combined)
92         references = [part.strip() for group in re.findall(
93             r'\\(?:ref|eqref|autoref|cref|Cref)\*?\s*\{([^}]+)\}', combined)
94             for part in group.split(',')]
95         duplicates = sorted(k for k, v in collections.Counter(labels).items() if v > 1)
96         unresolved = sorted(set(references) - set(labels))
97         document_labels[folder] = set(labels)
98         check(folder + '_unique_labels', not duplicates, duplicates)
99         check(folder + '_resolved_references', not unresolved, unresolved)
100         source_includes = [name for name in re.findall(
101             r'\\includegraphics(?:\[[^\]]*\])?\s*\{([^}]+)\}', combined)
102                            if '#' not in name]
103         # The visual source uses this known two-argument macro together with
104         # graphicspath{figures/}. Check its actual calls, not the #1 template.
105         source_includes.extend('figures/' + name + '.pdf' for name in re.findall(
106             r'\\guidefig\s*\{([^}]+)\}', combined))
107         missing_images = []
108         for name in source_includes:
109             candidate = tex.parent / name
110             options = [candidate] if candidate.suffix else [candidate.with_suffix(s) for s in
111                                                           ['.pdf', '.png', '.jpg', '.svg']]
112             if not any(p.is_file() for p in options):
113                 missing_images.append(name)
114         check(folder + '_figure_sources_exist', not missing_images, missing_images)
115         md_bytes = md.read_bytes()
116         controls = [(i, b) for i, b in enumerate(md_bytes) if b < 32 and b not in {9, 10}]
117         check(folder + '_markdown_controls', not controls, controls[:10])
118         check(folder + '_markdown_present', len(md_bytes) > 1000)
119         log = tex.with_suffix('.log')
120         warnings = []
121         if log.is_file():
122             warnings = [line for line in log.read_text(errors='replace').splitlines()
123                         if any(s in line for s in ['Overfull', 'undefined references',
124                                                   'undefined citations', 'multiply defined'])]
125         check(folder + '_no_material_tex_warnings', not warnings, warnings)
126         with fitz.open(pdf) as doc:
127             outside = []
128             for page_number, page in enumerate(doc, 1):
129                 for block in page.get_text('dict')['blocks']:
130                     for line in block.get('lines', []):
131                         for span in line['spans']:
132                             if not span.get('text', '').strip():
133                                 continue
134                             box = fitz.Rect(span['bbox']) * page.rotation_matrix
135                             rect = page.rect
136                             if (box.x0 < rect.x0 - 1 or box.y0 < rect.y0 - 1 or
137                                 box.x1 > rect.x1 + 1 or box.y1 > rect.y1 + 1):
138                                 outside.append({'page': page_number,
139                                                 'text': span['text'][:100]})
140             check(folder + '_text_inside_pages', not outside, outside[:20])
141             pages = len(doc)
142         details[folder] = {'pdf': str(pdf.relative_to(ROOT)), 'pages': pages,
143                            'bytes': pdf.stat().st_size, 'sha256': digest(pdf),
144                            'tex_source_files': sources, 'labels': len(labels),
145                            'references': len(references), 'figures': len(source_includes),
146                            'unique_figure_sources': len(set(source_includes)),
147                            'markdown_bytes': len(md_bytes)}
148     concordance_path = ROOT / 'traditional' / 'Claim_Lean_Concordance.json'
149     concordance = json.loads(concordance_path.read_text(encoding='utf-8'))
150     claims = concordance['claims']
151     claim_ids = [x['claim_id'] for x in claims]
152     check('64_unique_principal_claim_groups', len(claim_ids) == 64
153           and len(set(claim_ids)) == 64)
154     known_declarations = {x['name'] for x in declarations}
155     bad_anchors = []
156     bad_labels = []
157     empty_scope = []
158     missing_printed_scope = []
159     traditional_tex = (ROOT / 'traditional' / 'Sufficient_Resolution_Traditional.tex').read_text(encoding='utf-8')
160     for claim in claims:
161         if not claim.get('hypotheses') or not claim.get('domain'):
162             empty_scope.append(claim['claim_id'])
163         if not claim.get('anchors'):
164             bad_anchors.append((claim['claim_id'], 'NO_ANCHORS'))
165         for anchor in claim.get('anchors', []):
166             if anchor['name'] not in known_declarations:
167                 bad_anchors.append((claim['claim_id'], anchor['name']))
168             p = ROOT / 'formal' / anchor['file']
169             if not p.is_file() or digest(p) != anchor['source_sha256']:
170                 bad_anchors.append((claim['claim_id'], 'SOURCE_HASH'))
171         if claim.get('document_label') not in document_labels['traditional']:
172             bad_labels.append(claim['claim_id'])
173         printed = claim.get('hypotheses_tex')
174         if not printed or printed not in traditional_tex:
175             missing_printed_scope.append(claim['claim_id'])
176     check('principal_claim_declarations_and_hashes', not bad_anchors, bad_anchors)
177     check('principal_claim_document_labels', not bad_labels, bad_labels)
178     check('principal_claim_explicit_domains_and_hypotheses', not empty_scope, empty_scope)
179     check('principal_claim_hypotheses_printed_in_manuscript', not missing_printed_scope
180           and traditional_tex.count(r'\textbf{Hypotheses.}') == 64, missing_printed_scope)
181     traditional_md = (ROOT / 'traditional' / 'Sufficient_Resolution_Traditional.md').read_text(encoding='utf-8')
182     check('principal_claim_hypotheses_preserved_in_markdown',
183           traditional_md.count('**Hypotheses.**') == 64)
184     check('16_blocks_present', {int(x['block']) for x in claims} == set(range(1, 17)))
185     lean_claims = json.loads((ROOT / 'lean' / 'Claim_Lean_Concordance.json').read_text(encoding='utf-8'))
186     lean_by_id = {x['claim_id']: x for x in lean_claims}
187     stale_mapping = []
188     for claim in claims:
189         other = lean_by_id.get(claim['claim_id'])
190         if other is None or (other['formula_tex'] != claim['statement_tex'] or
191                              other['hypotheses'] != claim['hypotheses'] or
192                              other['hypotheses_tex'] != claim['hypotheses_tex'] or
193                              other['declarations'] != [a['name'] for a in claim['anchors']]):
194             stale_mapping.append(claim['claim_id'])
195     check('lean_claim_map_matches_current_manuscript', not stale_mapping
196           and len(lean_claims) == 64, stale_mapping)
197     mapping_audit = json.loads((ROOT / 'lean' / 'CLAIM_MAPPING_AUDIT.json').read_text())
198     check('lean_claim_map_live_concordance_hash',
199           mapping_audit['input_sha256'] == digest(concordance_path))
200     visual_crosswalk = json.loads((ROOT / 'visual' / 'validation' / 'claim_crosswalk.json').read_text())
201     check('visual_covers_all_principal_claim_groups',
202           visual_crosswalk['traditional_groups_covered'] == [f'SR-{i:02d}' for i in range(1, 65)])
203     evidence = json.loads((ROOT / 'verification' / 'FINAL_EVIDENCE_VALIDATION.json').read_text())
204     stale_evidence = [x['manifest'] for x in evidence['records']
205                       if digest(ROOT / x['manifest']) != x['manifest_sha256']]
206     check('18_current_evidence_manifests_validated', evidence['status'] == 'PASS'
207           and len(evidence['records']) == 18 and not stale_evidence, stale_evidence)
208     execution = json.loads((ROOT / 'verification' / 'CURRENT_RELEASE_VERIFICATION.json').read_text())
209     passed = all(x['passed'] for x in checks)
210     record = {'status': 'PASS_DOCUMENT_AND_SOURCE_INTEGRATION' if passed else 'FAIL',
211               'scope': 'Publication source, inventory, hash and PDF-bound checks; no new formal proof.',
212               'documents': details, 'total_pdf_pages': sum(x['pages'] for x in details.values()),
213               'principal_claim_groups': len(claims), 'formal_declarations': len(declarations),
214               'production_modules': len(modules), 'checks': checks,
215               'fresh_python': {k: execution['fresh_python'][k] for k in
216                                ['status', 'suite_count', 'native_counted_assertions',
217                                 'additional_fixed_sanity_groups',
218                                 'additional_main_mathematical_assert_statements']},
219               'evidence_manifests': {'base_records': 17, 'visual_example_records': 1,
220                                      'total': len(evidence['records']),
221                                      'verification': 'verification/FINAL_EVIDENCE_VALIDATION.json',
222                                      'assertion_counts_merged': False},
223               'fresh_lean': execution['fresh_lean']}
224     (ROOT / 'PUBLICATION_AUDIT.json').write_text(json.dumps(record, indent=2) + '\n',
225                                                encoding='utf-8')
226     print(json.dumps({'status': record['status'], 'checks': len(checks),
227                       'failed': [x for x in checks if not x['passed']],
228                       'total_pdf_pages': record['total_pdf_pages']}))
229     if not passed:
230         raise SystemExit(1)
231 
232 if __name__ == '__main__':
233     main()

Back to source controls

Back to Sufficient Resolution