binding_substitution.py (17389B)
1 #!/usr/bin/env python3 2 """Isolated core substitution/rewrite candidate, with named-variable oracle. 3 4 No accepted compiler files are edited. Core outputs are later compiled with an 5 explicit authenticated stable core compiler; the rewrite is not a default pass. 6 """ 7 import argparse 8 from dataclasses import dataclass, replace 9 import hashlib 10 import itertools 11 import json 12 import random 13 from pathlib import Path 14 15 from float_multiply import Runner,sha 16 from base_workloads import encode as nat 17 from http_headers import LEAF,TRUE,pair,tree_list,expect 18 from bundle_dag import Intern,read,merge_bundles 19 from binding_analysis import analyze,decision 20 from abstraction_binding_model import programs 21 from fixture_sources import verify, snapshot_bytes 22 23 ROOT=Path(__file__).resolve().parent.parent 24 25 26 @dataclass(frozen=True) 27 class C: 28 kind: int 29 payload: object=None 30 start: int=0 31 end: int=1 32 33 34 def children(n): 35 return n.payload if n.kind in [3,8] else (n.payload,) if n.kind==4 else () 36 37 38 def encode(n): 39 k,p=n.kind,n.payload 40 if k==3:p=pair(*(encode(c) for c in p)) 41 elif k==4:p=encode(p) 42 elif k==8:p=tree_list([encode(c) for c in p]) 43 elif k==2:p=nat(p) 44 elif p is None:p=LEAF 45 return pair(nat(k),pair(p,pair(nat(n.start),nat(n.end)))) 46 47 48 def plain(n): 49 k,p=n.kind,n.payload 50 if k in [3,8]:p=tuple(plain(c) for c in p) 51 elif k==4:p=plain(p) 52 return k,p 53 54 55 # Independent substitution oracle: decode indices to globally fresh binder 56 # names, substitute names, then re-resolve. No index-shift recurrence is reused. 57 def named(n,env=(),prefix='body',counter=None): 58 counter=itertools.count() if counter is None else counter 59 if n.kind==2: 60 name=env[n.payload] if n.payload<len(env) else ('free',n.payload-len(env)) 61 return replace(n,payload=name) 62 if n.kind==4: 63 binder=(prefix,next(counter)) 64 return replace(n,payload=(binder,named(n.payload,(binder,)+env,prefix,counter))) 65 if n.kind in [3,8]:return replace(n,payload=tuple(named(c,env,prefix,counter) for c in n.payload)) 66 return n 67 68 69 def replace_name(n,target,value): 70 if n.kind==2:return value if n.payload==target else n 71 if n.kind==4: 72 binder,body=n.payload 73 return replace(n,payload=(binder,replace_name(body,target,value))) 74 if n.kind in [3,8]:return replace(n,payload=tuple(replace_name(c,target,value) for c in n.payload)) 75 return n 76 77 78 def indexed(n,env=(),free_offset=0): 79 if n.kind==2: 80 name=n.payload 81 index=env.index(name) if name in env else len(env)+name[1]+free_offset 82 return replace(n,payload=index) 83 if n.kind==4: 84 binder,body=n.payload 85 return replace(n,payload=indexed(body,(binder,)+env,free_offset)) 86 if n.kind in [3,8]:return replace(n,payload=tuple(indexed(c,env,free_offset) for c in n.payload)) 87 return n 88 89 90 def substitution(body,rhs): 91 target=('removed',0) 92 return indexed(replace_name(named(body,(target,),prefix='body'),target,named(rhs,prefix='rhs'))) 93 94 95 def shifted(node,amount,cutoff): 96 ambient=tuple(('ambient',i) for i in range(cutoff)) 97 return indexed(named(node,ambient,prefix='shift'),ambient,amount) 98 99 100 def literal_bool(n): 101 if n.kind==1:return True 102 if n.kind in [5,6]:return n.payload in [LEAF,TRUE] 103 leaf=lambda c:c.kind==1 or (c.kind==5 and c.payload==LEAF) 104 return n.kind==3 and all(leaf(c) for c in n.payload) 105 106 107 def bool_rhs(n,negation): 108 return literal_bool(n) or (n.kind==3 and n.payload[0].kind==5 and n.payload[0].payload==negation 109 and (n.payload[1].kind==2 or literal_bool(n.payload[1]))) 110 111 112 def has_lambda(n):return n.kind==4 or any(has_lambda(c) for c in children(n)) 113 114 115 def rewrite(n,selector,negation): 116 if n.kind!=3 or n.payload[0].kind!=4:return 9,n 117 body,rhs=n.payload[0].payload,n.payload[1] 118 code=decision(analyze(plain(body),selector)) 119 if code!=1:return code,n 120 if not bool_rhs(rhs,negation):return 7,n 121 if has_lambda(body):return 8,n 122 return 1,replace(substitution(body,rhs),start=n.start,end=n.end) 123 124 125 def transform(n,selector,negation): 126 if n.kind==3 and n.payload[0].kind==4:return rewrite(n,selector,negation)[1] 127 if n.kind in [3,8]:return replace(n,payload=tuple(transform(c,selector,negation) for c in n.payload)) 128 if n.kind==4:return replace(n,payload=transform(n.payload,selector,negation)) 129 return n 130 131 132 def resolve(expr,globals,env=(),serial=None): 133 serial=itertools.count() if serial is None else serial 134 loc=next(serial)*3 135 k=expr[0] 136 if k=='var': 137 name=expr[1] 138 if name in env:return C(2,env.index(name),loc,loc+2) 139 return C(1,None,loc,loc+2) if name=='t' else C(5,globals[name],loc,loc+2) 140 if k=='lam':return C(4,resolve(expr[2],globals,(expr[1],)+env,serial),loc,loc+2) 141 return C(3,(resolve(expr[1],globals,env,serial),resolve(expr[2],globals,env,serial)),loc,loc+2) 142 143 144 def random_core(rng,depth=4): 145 span=dict(start=rng.randrange(1000),end=rng.randrange(1000,2000)) 146 k=rng.choice([1,2,2,5,6,7] if not depth else [1,2,3,3,4,8]) 147 if k==2:p=rng.randrange(7) 148 elif k==3:p=tuple(random_core(rng,depth-1) for _ in range(2)) 149 elif k==4:p=random_core(rng,depth-1) 150 elif k==8:p=tuple(random_core(rng,depth-1) for _ in range(rng.randrange(4))) 151 elif k in [5,6,7]:p=nat(rng.randrange(64)) 152 else:p=None 153 return C(k,p,**span) 154 155 156 def tree_bytes(nodes,root): 157 out=bytearray();todo=[root] 158 while todo: 159 node=nodes[todo.pop()];out.append(node[0]);todo.extend(reversed(node[1:])) 160 return bytes(out) 161 162 163 HELPERS='''!export * 164 triage leaf stem fork = t (t leaf stem) fork 165 choose yes no value = triage no (_ : yes) (_ _ : yes) value 166 negate x = choose t (t t) x 167 both a b = choose b t a 168 either a b = choose (t t) b a 169 head x = triage t (_ : t) (a _ : a) x 170 tail x = triage t (_ : t) (_ b : b) x 171 copy xs = triage t (_ : t) (a b : t (t a) (copy b)) xs 172 loop x = loop x 173 applyOne f x = f x 174 applyTwo f a b = f a b 175 applyThree f a b c = f a b c 176 unusedFlag f = f (loop t) t 177 branchNegatedHead f = head (f (t t) (t (loop t))) 178 branchNegatedTail f = tail (f t (t (loop t))) 179 adderKnownCarryZero f = tail (f t (loop t) t) 180 adderKnownCarryOne f = tail (f (t t) (t t) (loop t)) 181 ''' 182 183 184 def main(): 185 p=argparse.ArgumentParser(description=__doc__) 186 p.add_argument('tricu',type=Path) 187 p.add_argument('--directory',type=Path,required=True) 188 args=p.parse_args() 189 root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 190 workspace=root/'workspace';workspace.mkdir() 191 files={'substitution.tri':'bench/binding-substitution.tri','analysis.tri':'bench/binding-analysis.tri', 192 'kernels.tri':'bench/float-significands.tri','native_math.tri':'lib/math/native.tri'} 193 for name,path in files.items():(workspace/name).write_bytes((ROOT/path).read_bytes()) 194 (workspace/'helpers.tri').write_text(HELPERS) 195 report=dict(complete=False,mode='isolated-core-candidate-not-installed',runtime_sha256=sha(args.tricu), 196 compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'),harness_sha256=sha(Path(__file__)), 197 analysis_oracle_sha256=sha(ROOT/'test/binding_analysis.py'), 198 fixture_ast_sha256=sha(ROOT/'test/abstraction_binding_model.py'), 199 sources={name:sha(workspace/name) for name in [*files,'helpers.tri']},checks=[],programs=[]) 200 runner=Runner(args.tricu,root,1200,memory_mib=2048) 201 try: 202 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler') 203 for name in ['substitution','helpers']: 204 runner.run('compile-'+name,['compile','--file',workspace/(name+'.tri'),'--toolchain',tool, 205 '--tool-store',runner.store,'--store',runner.store,'--output',root/(name+'.arboricx'), 206 '--compile-timeout','240'],270) 207 pin=runner.imported(root/'substitution.arboricx','substitution') 208 helperpin=runner.imported(root/'helpers.arboricx','helpers') 209 _,_,nodes,exports,_=read(root/'helpers.arboricx') 210 globals={name:tree_bytes(nodes,i) for name,i in exports.items()} 211 selector,negation=globals['choose'],globals['negate'] 212 cert=root/'certificates.tree';cert.write_bytes(pair(selector,negation)) 213 report['certificates']={name:hashlib.sha256(globals[name]).hexdigest() for name in ['choose','negate']} 214 report['substitution_bundle_sha256']=sha(root/'substitution.arboricx') 215 216 def invoke(label,export,values,wanted=None,subject=pin): 217 argv=[] 218 for i,value in enumerate(values): 219 path=root/f'{label}-{i}.tree';path.write_bytes(value);argv += ['--arg-tree-file',path] 220 actual=runner.invoke(label,subject,export,argv) 221 if wanted is not None:expect(actual,wanted,label) 222 report['checks'].append(dict(label=label,result_sha256=hashlib.sha256(actual).hexdigest())) 223 return actual 224 225 rng=random.Random(2701) 226 subs=[(random_core(rng,3),random_core(rng,4)) for _ in range(192)] 227 # Ordered pairs are RHS, body. Explicit capture, shadow, and outer-index cases. 228 subs += [(C(2,0,7,8),C(4,C(3,(C(2,1,20,21),C(2,0,22,23)),18,24),10,30)), 229 (C(4,C(2,0,7,8),6,9),C(4,C(2,1,11,12),10,13)), 230 (C(1,None,1,2),C(2,5,31,32))] 231 for off in range(0,len(subs),24): 232 chunk=subs[off:off+24] 233 invoke('substitute-'+str(off),'substituteBatch', 234 [tree_list([pair(encode(rhs),encode(body)) for rhs,body in chunk])], 235 tree_list([encode(substitution(body,rhs)) for rhs,body in chunk])) 236 shifts=[(rng.randrange(5),rng.randrange(5),random_core(rng)) for _ in range(128)] 237 for off in range(0,len(shifts),24): 238 chunk=shifts[off:off+24] 239 invoke('shift-'+str(off),'shiftBatch', 240 [tree_list([pair(nat(a),pair(nat(c),encode(n))) for a,c,n in chunk])], 241 tree_list([encode(shifted(n,a,c)) for a,c,n in chunk])) 242 report['substitution_cases']=len(subs);report['shift_cases']=len(shifts) 243 244 full={name:resolve(expr,globals) for name,expr in programs().items()} 245 bindings=[] 246 def collect(name,n): 247 if n.kind==3 and n.payload[0].kind==4:bindings.append((name,n)) 248 for child in children(n):collect(name,child) 249 for name,n in full.items():collect(name,n) 250 z=C(2,0,10,11);x=C(2,1,12,13);t=C(1,None,1,2) 251 bind=lambda body,rhs:C(3,(C(4,body,50,60),rhs),40,80) 252 bindings += [('literal-bool',bind(C(3,(C(3,(t,z)),x)),C(3,(t,t)))), 253 ('rhs-lambda',bind(z,C(4,C(2,0)))), 254 ('rhs-unknown',bind(z,C(3,(C(5,globals['copy']),C(2,0))))), 255 ('rhs-negation-computation',bind(z,C(3,(C(5,negation),C(3,(C(5,globals['copy']),C(2,0))))))), 256 ('unrelated-body-lambda',bind(C(3,(C(3,(t,z)),C(4,C(2,0)))),C(5,TRUE))), 257 ('not-binding',C(3,(t,z)))] 258 bindings += [(f'generated-{i}',bind(random_core(rng),C(3,(C(5,negation),C(2,0))))) for i in range(128)] 259 for off in range(0,len(bindings),24): 260 chunk=bindings[off:off+24] 261 invoke('rewrite-'+str(off),'rewriteBatch',[pair(selector,negation),tree_list([encode(n) for _,n in chunk])], 262 tree_list([pair(nat(code),encode(out)) for code,out in [rewrite(n,selector,negation) for _,n in chunk]])) 263 report['rewrite_decisions']=[dict(name=name,code=rewrite(n,selector,negation)[0], 264 unchanged=encode(rewrite(n,selector,negation)[1])==encode(n)) for name,n in bindings] 265 originals=list(full.items()) 266 outputs=invoke('transform-programs','transformBatch',[pair(selector,negation),tree_list([encode(n) for _,n in originals])], 267 tree_list([encode(transform(n,selector,negation)) for _,n in originals])) 268 269 # Authenticate the retained stable core compiler and its source snapshot. 270 rows=verify(ROOT/'test/fixtures') 271 stable=next(row for row in rows if row[2]=='source_stable') 272 assert snapshot_bytes(ROOT/'test/fixtures',stable[4])==(ROOT/'lib/source/stable.tri').read_bytes() 273 compiler=root/'core-compiler.arboricx' 274 merge_bundles(compiler,[(ROOT/'test/fixtures/compiler-library.arboricx', 275 [('source_stable.stableCompileCore','compile')])],prune_unreachable=True) 276 compilerpin=runner.imported(compiler,'core-compiler') 277 report['core_compiler_bundle_sha256']=sha(compiler) 278 # Bind the retained worker to the actual accepted compiler, not merely 279 # to a matching source file: its entire tree must occur in that closure. 280 reference=read(compiler); shipped=read(ROOT/'bootstrap/build-stable.arboricx') 281 intern=Intern(); refids=intern.graph(reference[2]); shippedids=intern.graph(shipped[2]) 282 target=refids[reference[3]['compile']] 283 seen=set();pending=[shipped[3]['sourceBuildGraph']] 284 while pending: 285 index=pending.pop() 286 if index not in seen:seen.add(index);pending.extend(shipped[2][index][1:]) 287 assert target in {shippedids[index] for index in seen}, 'core worker differs from shipped compiler' 288 report['core_compiler_exact_tree_in_shipped_closure']=True 289 compiled={} 290 from source_order import end 291 for name,n in originals: 292 transformed=transform(n,selector,negation) 293 for role,core_node in [('original',n),('candidate',transformed)]: 294 result=invoke('core-'+name+'-'+role,'compile',[encode(core_node)],subject=compilerpin) 295 if result[:4]!=b'\2\1\0\2':raise AssertionError(('core compilation failure',name,role,result[:32])) 296 body=result[4:];tree=body[:end(body)] 297 expect(result,b'\2\1\0\2'+tree+LEAF,'compile envelope') 298 compiled[name,role]=tree 299 unchanged=encode(n)==encode(transformed) 300 if unchanged:expect(compiled[name,'candidate'],compiled[name,'original'],'unchanged function '+name) 301 report['programs'].append(dict(name=name,core_changed=not unchanged, 302 compiled_tree_changed=compiled[name,'candidate']!=compiled[name,'original'])) 303 for bound,inline in [('singleBound','singleInline'),('branchBound','branchInline'),('adderBound','adderInline')]: 304 expect(compiled[bound,'candidate'],compiled[inline,'original'],'known-inline-tree '+bound) 305 306 # Concrete independent results; originals/candidates get identical args. 307 for role in ['original','candidate']: 308 for name in ['singleBound','branchBound','constructorBound']: 309 for f in [False,True]: 310 for xval in [False,True]: 311 xbytes=TRUE if xval else LEAF 312 zbytes=b'\1'+xbytes if name=='constructorBound' else LEAF if xval else TRUE 313 want=pair(zbytes,xbytes) if name=='singleBound' or f else pair(xbytes,zbytes) 314 invoke(f'value-{role}-{name}-{f}-{xval}','applyTwo', 315 [compiled[name,role],TRUE if f else LEAF,xbytes],want,helperpin) 316 for a,b,c in itertools.product([False,True],repeat=3): 317 total=a+b+c 318 invoke(f'adder-{role}-{a}{b}{c}','applyThree', 319 [compiled['adderBound',role]]+[TRUE if v else LEAF for v in [a,b,c]], 320 pair(TRUE if total%2 else LEAF,TRUE if total>=2 else LEAF),helperpin) 321 xs=nat([0,1,2,3]);copied=tree_list([b'\1'+nat(i) for i in range(4)]) 322 invoke('sharing-'+role,'applyOne',[compiled['sharedBound',role],xs],pair(copied,copied),helperpin) 323 invoke('unused-'+role,'applyOne',[compiled['unusedBound',role],TRUE],TRUE,helperpin) 324 invoke('unselected-'+role,'applyOne',[compiled['closedBranchBound',role],LEAF],LEAF,helperpin) 325 # Rejected capture and closed-computation bindings remain exact trees; 326 # both original and candidate must retain their full-observation demand. 327 for name,extra in [('closureBound',[LEAF]),('closedBranchBound',[TRUE])]: 328 try: 329 invoke('demand-'+name+'-'+role,'applyOne',[compiled[name,role],*extra],subject=helperpin) 330 raise AssertionError('expected demand timeout') 331 except RuntimeError as error: 332 if str(error)!='wall-time guard exceeded':raise 333 report.setdefault('demand',[]).append(dict(name=name,role=role,outcome='timeout',seconds=3)) 334 for role in ['original','candidate']: 335 for probe,name,wanted in [ 336 ('unusedFlag','singleBound',pair(TRUE,LEAF)), 337 ('branchNegatedHead','branchBound',LEAF), 338 ('branchNegatedTail','branchBound',LEAF), 339 ('adderKnownCarryZero','adderBound',LEAF), 340 ('adderKnownCarryOne','adderBound',TRUE)]: 341 invoke('partial-'+probe+'-'+role,probe,[compiled[name,role]],wanted,helperpin) 342 report['partial_result_checks']=10 343 report['complete']=True 344 print('PASS: shift/substitution/rewrite core oracles, exact unchanged trees, and isolated compiled controls') 345 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 346 347 348 if __name__=='__main__':main()