binding_stable_validation.py (6037B)
1 #!/usr/bin/env python3 2 """Validate source-owned certificates, guarded core outputs and real source builds.""" 3 import argparse,hashlib,json 4 from pathlib import Path 5 from binding_substitution import ROOT,C,encode,rewrite,transform,resolve,HELPERS,tree_bytes 6 from binding_analysis import cases,analyze,expected 7 from abstraction_binding_model import programs 8 from float_multiply import Runner,sha 9 from http_headers import pair,tree_list,expect,LEAF,TRUE 10 from base_workloads import encode as nat 11 from bundle_dag import read,Intern 12 13 14 def main(): 15 p=argparse.ArgumentParser(description=__doc__) 16 p.add_argument('tricu',type=Path);p.add_argument('--integration',required=True,type=Path) 17 p.add_argument('--directory',required=True,type=Path) 18 p.add_argument('--prior-workload',type=Path,default=Path('/tmp/tricu-binding-compiler-measure-retry')) 19 args=p.parse_args();integration=args.integration.resolve();root=args.directory.resolve() 20 old=json.loads((integration/'report.json').read_text()) 21 assert old['complete'] and old['exact_self_rebuild'] 22 assert sha(integration/'stage-1.arboricx')==old['stages'][1]['bundle_sha256'] 23 root.mkdir(parents=True,exist_ok=False);workspace=root/'workspace';workspace.mkdir() 24 runner=Runner(args.tricu,root,900,memory_mib=2048) 25 report=dict(complete=False,accepted=False,harness_sha256=sha(Path(__file__)), 26 integration_report_sha256=sha(integration/'report.json'),checks=[]) 27 try: 28 accepted=runner.imported(ROOT/'bootstrap/build-stable.arboricx','accepted') 29 candidate=runner.imported(integration/'stage-1.arboricx','candidate') 30 for alias in ['source_binding','source_binding_support']: 31 pin=runner.imported(integration/f'stage-1-{alias}.arboricx',alias) 32 (workspace/(alias+'.tri')).write_text('!export * from '+pin+'\n') 33 (workspace/'driver.tri').write_text('''!import source_binding as B 34 !import source_binding_support as K 35 !export * 36 analysisBatch xs = K.map B.bindingAnalyze xs 37 inspectBatch xs = K.map B.bindingInspect xs 38 transformBatch xs = K.map B.bindingTransform xs 39 ''') 40 runner.run('compile-probe',['compile','--file',workspace/'driver.tri','--toolchain',accepted, 41 '--tool-store',runner.store,'--store',runner.store,'--output',root/'probe.arboricx','--compile-timeout','120'],150) 42 probe=runner.imported(root/'probe.arboricx','probe') 43 (workspace/'helpers.tri').write_text(HELPERS) 44 runner.run('compile-helpers',['compile','--file',workspace/'helpers.tri','--toolchain',accepted, 45 '--tool-store',runner.store,'--store',runner.store,'--output',root/'helpers.arboricx','--compile-timeout','120'],150) 46 _,_,nodes,exports,_=read(root/'helpers.arboricx');globals={name:tree_bytes(nodes,i) for name,i in exports.items()} 47 selector,negation=globals['choose'],globals['negate'] 48 def invoke(label,export,inputs,wanted): 49 path=root/(label+'.tree');path.write_bytes(tree_list(inputs)) 50 raw=runner.invoke(label,probe,export,['--arg-tree-file',path]) 51 expect(raw,tree_list(wanted),label);report['checks'].append(label) 52 def located(node): 53 k,p=node 54 if k in [3,8]:p=tuple(located(x) for x in p) 55 elif k==4:p=located(p) 56 return C(k,p) 57 bodies=cases(selector) 58 for off in range(0,len(bodies),24): 59 chunk=bodies[off:off+24] 60 invoke('analysis-'+str(off),'analysisBatch',[encode(located(n)) for _,n in chunk], 61 [expected(analyze(n,selector)) for _,n in chunk]) 62 bindings=[] 63 for _,body in bodies: 64 for rhs in [C(1),C(5,TRUE),C(3,(C(5,negation),C(2,0))),C(4,C(2,0)),C(3,(C(5,globals['copy']),C(2,0)))]: 65 bindings.append(C(3,(C(4,located(body)),rhs))) 66 for off in range(0,len(bindings),24): 67 chunk=bindings[off:off+24];wanted=[rewrite(n,selector,negation) for n in chunk] 68 invoke('inspect-'+str(off),'inspectBatch',[encode(n) for n in chunk], 69 [pair(nat(code),encode(out)) for code,out in wanted]) 70 full=[resolve(expr,globals) for expr in programs().values()] 71 invoke('programs','transformBatch',[encode(n) for n in full],[encode(transform(n,selector,negation)) for n in full]) 72 report.update(analysis_cases=len(bodies),binding_cases=len(bindings),program_cases=len(full)) 73 # Build the original arithmetic workspace with the new explicit backend. 74 workload=root/'arithmetic';workload.mkdir() 75 prior=json.loads((args.prior_workload/'report.json').read_text());assert prior['complete'] 76 for name,digest in prior['sources'].items(): 77 path=args.prior_workload/'workspace'/name;assert sha(path)==digest 78 (workload/name).write_bytes(path.read_bytes()) 79 runner.run('compile-arithmetic',['compile','--file',workload/'driver.tri','--toolchain',candidate, 80 '--tool-store',runner.store,'--store',root/'arithmetic-store','--output',root/'arithmetic.arboricx', 81 '--compile-timeout','240'],270) 82 reference=args.prior_workload/'compile-4-candidate.arboricx' 83 assert sha(reference)==next(x['bundle_sha256'] for x in prior['compile_samples'] if x['role']=='candidate' and x['repeat']==4) 84 intern=Intern();graphs=[] 85 for path in [reference,root/'arithmetic.arboricx']: 86 _,_,ns,es,_=read(path);ids=intern.graph(ns);graphs.append({name:ids[i] for name,i in es.items()}) 87 assert graphs[0]==graphs[1], 'source-owned backend changes checked arithmetic trees' 88 report['arithmetic_exports_exact']=len(graphs[0]);report['arithmetic_bundle_sha256']=sha(root/'arithmetic.arboricx') 89 report['complete']=True 90 print('PASS:',len(bodies),'analyses,',len(bindings),'binding decisions,',len(full),'cores,',len(graphs[0]),'exact arithmetic exports') 91 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 92 93 94 if __name__=='__main__':main()