binding_semantics.py (10013B)
1 #!/usr/bin/env python3 2 """Broader semantic screen; stop at the first demand/value mismatch. 3 4 Uses the authenticated previous isolated build, not an installed toolchain. 5 Raw function-tree differences after partial application are recorded separately 6 from changes to termination/full observation, which block further integration. 7 """ 8 import argparse,itertools,json,hashlib,random 9 from pathlib import Path 10 from binding_substitution import ROOT,C,encode,tree_bytes,transform 11 from float_multiply import Runner,sha 12 from base_workloads import encode as nat 13 from http_headers import LEAF,TRUE,pair,tree_list,expect 14 from source_order import end 15 from bundle_dag import read 16 17 DRIVER='''!import core as C 18 !import substitution as S 19 !import helpers as H 20 !export * 21 compileOriginal core = C.compile core 22 compileCandidate core = C.compile (S.transform H.choose H.negate core) 23 argument code = case code of 24 0 = t 25 1 = t t 26 2 = t t t 27 3 = t (H.loop t) 28 4 = H.loop t 29 5 = t (H.loop t) (H.loop t) 30 6 = t (t t) 31 _ = t 32 applyArgs f args = H.triage f (_ : f) 33 (a rest : applyArgs (f (argument a)) rest) args 34 observe f args mode = let value = applyArgs f args in case mode of 35 0 = value 36 1 = H.triage 0 (_ : 1) (_ _ : 2) value 37 2 = H.head value 38 3 = H.tail value 39 _ = value 40 ''' 41 42 43 # Grammar is constructor/selector data, with no general beta evaluator in oracle. 44 def syntax(expr,selector): 45 if expr=='z':return C(2,0) 46 if expr=='x':return C(2,2) 47 if expr=='flag':return C(2,1) 48 if expr=='leaf':return C(1) 49 if expr[0]=='pair': 50 a,b=(syntax(x,selector) for x in expr[1:]) 51 return C(3,(C(3,(C(1),a)),b)) 52 out=C(5,selector) 53 for child in expr[1:]:out=C(3,(out,syntax(child,selector))) 54 return out 55 56 57 def program(body,selector,negation): 58 rhs=C(3,(C(5,negation),C(2,1))) 59 return C(4,C(4,C(3,(C(4,syntax(body,selector)),rhs)))) 60 61 62 class Bottom(Exception):pass 63 64 def value(code): 65 return {0:(0,),1:(1,(0,)),2:(2,(0,),(0,)),3:(1,None),4:None,5:(2,None,None),6:(1,(1,(0,)))}[code] 66 67 68 def force(v): 69 if v is None:raise Bottom 70 return v 71 72 73 def evaluate(expr,x,flag): 74 if expr=='leaf':return (0,) 75 if expr=='x':return x 76 if expr=='flag':return flag 77 if expr=='z':return (1,(0,)) if force(x)[0]==0 else (0,) 78 if expr[0]=='pair': 79 # Lazy children are represented as callables so projecting a pair does 80 # not evaluate either expression and accidentally strengthen the oracle. 81 return (2,lambda:evaluate(expr[1],x,flag),lambda:evaluate(expr[2],x,flag)) 82 condition=force(evaluate(expr[3],x,flag)) 83 return evaluate(expr[1] if condition[0] else expr[2],x,flag) 84 85 86 def demanded(v):return force(v() if callable(v) else v) 87 88 def flatten(v): 89 v=demanded(v) 90 return bytes([v[0]])+b''.join(flatten(c) for c in v[1:]) 91 92 93 def expected(expr,codes,mode): 94 v=evaluate(expr,value(codes[0]),value(codes[1])) 95 if mode==1:return nat(demanded(v)[0]) 96 if mode in [2,3]: 97 v=demanded(v);v=v[mode-1] if v[0]==2 else (0,) 98 # mode 2 selects child 1, mode 3 selects child 2. 99 return flatten(v) 100 101 102 def main(): 103 p=argparse.ArgumentParser(description=__doc__) 104 p.add_argument('tricu',type=Path);p.add_argument('--previous',type=Path,required=True) 105 p.add_argument('--directory',type=Path,required=True) 106 args=p.parse_args();previous=args.previous.resolve();root=args.directory.resolve() 107 old=json.loads((previous/'report.json').read_text()) 108 assert old['complete'] and old['core_compiler_exact_tree_in_shipped_closure'] 109 assert sha(args.tricu)==old['runtime_sha256'] 110 assert sha(ROOT/'bootstrap/build-stable.arboricx')==old['compiler_sha256'] 111 assert sha(previous/'substitution.arboricx')==old['substitution_bundle_sha256'] 112 assert sha(previous/'core-compiler.arboricx')==old['core_compiler_bundle_sha256'] 113 assert sha(ROOT/'bench/binding-substitution.tri')==old['sources']['substitution.tri'] 114 root.mkdir(parents=True,exist_ok=False);workspace=root/'workspace';workspace.mkdir() 115 runner=Runner(args.tricu,root,1800,memory_mib=2048) 116 report=dict(complete=False,blocked=False,harness_sha256=sha(Path(__file__)), 117 prior_report_sha256=sha(previous/'report.json'),runtime_sha256=sha(args.tricu), 118 compiler_sha256=old['compiler_sha256'],checks=[],programs=[]) 119 try: 120 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler') 121 for alias,bundle in [('core','core-compiler'),('substitution','substitution'),('helpers','helpers')]: 122 pin=runner.imported(previous/(bundle+'.arboricx'),alias) 123 (workspace/(alias+'.tri')).write_text('!export * from '+pin+'\n') 124 (workspace/'driver.tri').write_text(DRIVER) 125 report['driver_sha256']=sha(workspace/'driver.tri') 126 runner.run('compile-driver',['compile','--file',workspace/'driver.tri','--toolchain',tool, 127 '--tool-store',runner.store,'--store',runner.store,'--output',root/'driver.arboricx', 128 '--compile-timeout','240'],270) 129 pin=runner.imported(root/'driver.arboricx','driver') 130 _,_,nodes,exports,_=read(previous/'helpers.arboricx') 131 selector=tree_bytes(nodes,exports['choose']);negation=tree_bytes(nodes,exports['negate']) 132 assert hashlib.sha256(selector).hexdigest()==old['certificates']['choose'] 133 assert hashlib.sha256(negation).hexdigest()==old['certificates']['negate'] 134 serial=itertools.count() 135 def invoke(export,values,demand=False): 136 label=('demand-' if demand else '')+str(next(serial))+'-'+export 137 argv=[] 138 for i,raw in enumerate(values): 139 path=root/(label+f'-{i}.tree');path.write_bytes(raw);argv+=['--arg-tree-file',path] 140 try:return ('value',runner.invoke(label,pin,export,argv),label) 141 except RuntimeError as error: 142 if str(error)!='wall-time guard exceeded':raise 143 return ('timeout',None,label) 144 bodies=['z',('pair','z','leaf'),('choose','z','leaf','flag'), 145 ('choose','leaf','z','flag'),('choose',('pair','z','x'),('pair','x','z'),'flag'), 146 ('choose','x','flag','z')] 147 rng=random.Random(4409) 148 for _ in range(26): 149 expr=rng.choice(bodies[:6]) 150 for _ in range(rng.randrange(1,4)): 151 expr=rng.choice([('pair',expr,'leaf'),('choose',expr,'x','flag'), 152 ('choose','leaf',expr,'flag'),('choose',expr,expr,'flag')]) 153 bodies.append(expr) 154 compiled=[] 155 for index,body in enumerate(bodies): 156 core=program(body,selector,negation) 157 if encode(core)==encode(transform(core,selector,negation)):raise AssertionError('expected eligible core') 158 programs={} 159 for role,export in [('original','compileOriginal'),('candidate','compileCandidate')]: 160 status,raw,label=invoke(export,[encode(core)]) 161 assert status=='value' and raw[:4]==b'\2\1\0\2' 162 tree=raw[4:4+end(raw[4:])];expect(raw,b'\2\1\0\2'+tree+LEAF,'compile envelope') 163 programs[role]=tree 164 (root/f'program-{index}-{role}.tree').write_bytes(tree) 165 compiled.append(programs) 166 report['programs'].append(dict(index=index,body=body,changed=programs['original']!=programs['candidate'])) 167 168 def check(index,codes,mode,oracle=True): 169 results={} 170 for role,tree in compiled[index].items(): 171 status,raw,label=invoke('observe',[tree,nat(codes),nat(mode)],True) 172 results[role]=dict(status=status,bytes=len(raw) if raw is not None else None, 173 sha256=hashlib.sha256(raw).hexdigest() if raw is not None else None,label=label) 174 row=dict(program=index,args=codes,mode=mode,results=results) 175 if oracle: 176 try:wanted=expected(bodies[index],codes,mode);outcome='value' 177 except Bottom:wanted=None;outcome='timeout' 178 row['expected']=dict(status=outcome,sha256=hashlib.sha256(wanted).hexdigest() if wanted is not None else None) 179 matches=all(v['status']==outcome and v['sha256']==row['expected']['sha256'] for v in results.values()) 180 else: 181 # Function representation itself may differ, but newly divergent 182 # observation is NOT dismissed as a harmless code-tree change. 183 matches=results['original']['status']==results['candidate']['status'] 184 row['different_function_tree']=results['original']['sha256']!=results['candidate']['sha256'] 185 report['checks'].append(row) 186 if not matches: 187 report['blocked']=True;report['counterexample']=row 188 print('BLOCKED:',json.dumps(row));return False 189 return True 190 191 # Finite full application with independent constructor/selector oracle. 192 for index in range(len(bodies)): 193 for codes in itertools.product([0,1,2,6],repeat=2): 194 if not check(index,list(codes),0):return 195 report['finite_full_checks']=len(report['checks']) 196 # Expose the enclosing function-construction boundary, even though the 197 # eliminated variable does not occur beneath a lambda in its own body. 198 for index in range(len(bodies)): 199 for code in [0,1,2,3,5,4]: 200 if not check(index,[code],0,oracle=False):return 201 report['partial_application_checks']=len(report['checks'])-report['finite_full_checks'] 202 # Non-total data and selector inputs, full forcing vs root/projection. 203 for index in range(len(bodies)): 204 for codes,mode in [([3,0],0),([3,1],0),([5,1],1),([4,0],1),([4,1],1),([3,4],2),([3,4],3)]: 205 if not check(index,codes,mode):return 206 report['complete']=True;print('PASS: broader binding semantic screen') 207 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 208 209 210 if __name__=='__main__':main()