p-adic Canonical Realization

Download original file

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

1 #!/usr/bin/env python3
2 """Read-only replay of frozen execution evidence, completeness, and archive checksums."""
3 from pathlib import Path
4 import json,re,hashlib,sys
5 ROOT=Path(__file__).resolve().parent
6 sys.path.insert(0,str(ROOT/'verification'))
7 from evidence_parser import parse_declared,parse_environment,strip_comments,selftest
8 
9 def sha(p):return hashlib.sha256(p.read_bytes()).hexdigest()
10 def verify():
11     errors=[];checks=0
12     def ck(c,m):
13         nonlocal checks;checks+=1
14         if not c:errors.append(m)
15     def data(p):return json.loads((ROOT/p).read_text())
16     selftest();done=data('results/FINAL_RUN.json');ck(done['status']=='PASS','final run incomplete')
17     for phase in done.get('phases',[]):
18         r=data(f'results/{phase}.json');log=ROOT/r['log']
19         ck(r['pass'] and r['status']=='completed',phase+': incomplete')
20         ck(r['exit_status']==r['expected_exit'],phase+': exit')
21         ck(sha(log)==r['log_sha256'],phase+': log changed')
22         ck(r['input_hashes']==r['input_hashes_after'],phase+': input changed during run')
23         for p,h in r['input_hashes_after'].items():ck((ROOT/p).is_file() and sha(ROOT/p)==h,phase+': source changed '+p)
24         if r.get('expected_diagnostic'):ck(r['expected_diagnostic'] in log.read_text().lower(),phase+': wrong negative diagnostic')
25     inv=data('verification/theorem_inventory.json');names=inv['names'];ck(len(names)==len(set(names))==inv['total'],'declared inventory')
26     declared=parse_declared((ROOT/'results/declared_axioms.log').read_text())
27     env=parse_environment((ROOT/'results/environment_axioms.log').read_text());allowed={'propext','Quot.sound','Classical.choice'}
28     ck(set(declared)==set(names),'declared audit missing or extra names')
29     for n in names:
30         ck(n in env,'declared constant absent from environment '+n)
31         if n in env and n in declared:ck(env[n][1]==declared[n],'axiom routes disagree '+n)
32     for n,(mod,axs) in env.items():ck(axs<=allowed,'unexpected axioms '+n+':'+str(axs))
33     inherited=data('PREDECESSOR_SOURCE_HASHES.json')
34     for p,h in inherited.items():
35         if p!='lean/KomorebiPadic.lean':ck(sha(ROOT/p)==h,'predecessor source changed '+p)
36     import zipfile
37     pre=data('PREDECESSOR_ARCHIVE.json');ck(sha(ROOT/pre['path'])==pre['sha256'],'predecessor archive hash')
38     with zipfile.ZipFile(ROOT/pre['path']) as z:
39         prefix=z.namelist()[0].split('/')[0]+'/'
40         oldroot=z.read(prefix+'lean/KomorebiPadic.lean').decode()
41         ck((ROOT/'lean/KomorebiPadic.lean').read_text()=='import KomorebiPadic.ResidualMinimalityExamples\n'+oldroot,'root changed beyond one new import')
42     sources=list((ROOT/'lean').rglob('*.lean'));source_count=0
43     for src in sources:
44         code=strip_comments(src.read_text());source_count+=len(re.findall(r'\btheorem\s+[A-Za-z_]',code))
45         ck(not re.search(r'\b(?:sorry|admit|axiom|unsafe|native_decide)\b',code),'forbidden production construct '+str(src.relative_to(ROOT)))
46         rel=src.relative_to(ROOT/'lean').with_suffix('')
47         for ext in ['.olean','.ilean']:ck((ROOT/'compiled'/rel.with_suffix(ext)).is_file(),'missing artifact '+str(rel)+ext)
48     ck(source_count==inv['total'],'source theorem syntax count differs from inventory')
49     audit=data('results/audit_residual.json');ck(audit['status']=='PASS' and not audit['failures'],'finite audit')
50     ck(audit['assertions']==sum(audit['counts'].values()),'finite assertion tally')
51     jobs=re.findall(r'Build completed successfully \((\d+) jobs\)',(ROOT/'results/clean_build.log').read_text());ck(bool(jobs),'no final build success marker')
52     if (ROOT/'CHECKSUMS.json').exists():
53         for p,h in data('CHECKSUMS.json').items():ck((ROOT/p).is_file() and sha(ROOT/p)==h,'checksum '+p)
54     return {'status':'PASS' if not errors else 'FAIL','checks':checks,'errors':errors,
55       'scope':'Read-only evidence replay, not a new Lean execution.','production_modules':len(sources),
56       'declared_theorems':len(names),'new_theorems':inv['new'],'inherited_theorems':inv['inherited'],
57       'environment_theorem_constants':len(env),'axiom_free_declared':sum(not declared.get(n,{'missing'}) for n in names),
58       'observed_axioms':sorted(set().union(*(a for _,a in env.values()))) if env else [],
59       'build_jobs':int(jobs[-1]) if jobs else None,'fresh_assertions':audit['assertions'],'final_phases':len(done.get('phases',[]))}
60 if __name__=='__main__':
61     try:r=verify()
62     except Exception as e:r={'status':'FAIL','exception':repr(e)}
63     print(json.dumps(r,indent=2));raise SystemExit(r['status']!='PASS')

Back to source controls

Back to p-adic Canonical Realization