binding_analysis.py (8949B)
1 #!/usr/bin/env python3 2 """Analysis-only resolved-core binding certificate prototype; no compiler rewrite.""" 3 import argparse 4 import hashlib 5 import itertools 6 import json 7 import random 8 from pathlib import Path 9 10 from collections_batch import ProbeRunner 11 from base_workloads import encode as nat 12 from http_headers import LEAF,TRUE,pair,tree_list,expect 13 from bundle_dag import read 14 from abstraction_binding_model import programs 15 16 ROOT=Path(__file__).resolve().parent.parent 17 # Core node as (kind,payload); spans are irrelevant to analysis but are preserved 18 # in the encoded input schema. Literal tree payloads use preorder constructor bytes. 19 def core(kind,payload=None):return (kind,payload) 20 def app(f,x):return core(3,(f,x)) 21 def call(f,*args): 22 for a in args:f=app(f,a) 23 return f 24 25 def encode(node): 26 k,p=node 27 if k==3:p=pair(encode(p[0]),encode(p[1])) 28 elif k==4:p=encode(p) 29 elif k==8:p=tree_list([encode(x) for x in p]) 30 elif k==2:p=nat(p) 31 elif p is None:p=LEAF 32 return pair(nat(k),pair(p,pair(nat(0),nat(0)))) 33 34 35 def analyze(node,selector,depth=0): 36 # Independent oracle enumerates possible use-count paths, rather than just 37 # propagating maxima. Flags: escape, unknown, partial, malformed. 38 def merge(a,b): 39 return a[0]+b[0],{x+y for x in a[1] for y in b[1]},tuple(x or y for x,y in zip(a[2],b[2])) 40 def mark(a,index,condition=True): 41 flags=list(a[2]);flags[index] |= condition;return a[0],a[1],tuple(flags) 42 empty=(0,{0},(False,)*4) 43 k,p=node 44 if k in [1,5,6,7]:return empty 45 if k==2:return (1,{1},(False,)*4) if p==depth else empty 46 if k==4: 47 a=analyze(p,selector,depth+1);return mark(a,0,bool(a[0])) 48 if k==8: 49 out=empty 50 for child in p:out=merge(out,analyze(child,selector,depth)) 51 return out 52 if k!=3:return mark(empty,3) 53 args=[];fun=node 54 while fun[0]==3:args.insert(0,fun[1][1]);fun=fun[1][0] 55 results=[analyze(x,selector,depth) for x in args] 56 out=analyze(fun,selector,depth) 57 for result in results:out=merge(out,result) 58 if fun==(5,selector): 59 if len(args)==3: 60 a,b,c=results 61 return out[0],{branch+condition for branch in a[1]|b[1] for condition in c[1]},out[2] 62 return mark(mark(out,1,bool(out[0])),2,len(args)<3 and bool(out[0])) 63 slots=2 if fun[0]==1 else (2 if fun[0]==5 and fun[1]==LEAF else 64 1 if fun[0]==5 and fun[1][0]==1 else 0) 65 if slots and len(args)<=slots:return out 66 return mark(out,1,bool(out[0])) 67 68 69 def decision(result): 70 uses,paths,(escape,unknown,partial,bad)=result 71 return 6 if bad else 3 if escape else 5 if partial else 4 if unknown else 0 if not uses else 2 if max(paths)>1 else 1 72 73 74 def expected(result): 75 uses,paths,flags=result 76 tail=TRUE if flags[-1] else LEAF 77 for flag in reversed(flags[:-1]):tail=pair(TRUE if flag else LEAF,tail) 78 summary=pair(nat(uses),pair(nat(max(paths)),tail)) 79 return pair(nat(decision(result)),summary) 80 81 82 def resolve(expr,selector,stack=()): 83 k=expr[0] 84 if k=='var': 85 name=expr[1] 86 if name in stack:return core(2,stack.index(name)) 87 if name=='t':return core(1) 88 # Only the explicitly resolved choose literal receives the certificate. 89 return core(5,selector if name=='choose' else nat(17)) 90 if k=='lam':return core(4,resolve(expr[2],selector,(expr[1],)+stack)) 91 return app(resolve(expr[1],selector,stack),resolve(expr[2],selector,stack)) 92 93 94 def cases(selector): 95 rows=[] 96 def collect(name,expr,stack=()): 97 if expr[0]=='lam':collect(name,expr[2],(expr[1],)+stack) 98 elif expr[0]=='app': 99 if expr[1][0]=='lam': 100 _,binding,body=expr[1] 101 rows.append((name,resolve(body,selector,(binding,)+stack))) 102 collect(name,expr[1],stack);collect(name,expr[2],stack) 103 for name,expr in programs().items():collect(name,expr) 104 z,x,t=core(2,0),core(2,1),core(1) 105 sel=core(5,selector) 106 examples={ 107 'alias-same-literal':call(sel,z,t,x), 108 'name-with-wrong-literal':call(core(5,nat(17)),z,t,x), 109 'shadowed-selector':call(core(2,1),z,t,x), 110 'selector-and-branch-use':call(sel,z,t,z), 111 'partial-selector':call(sel,z,t), 112 'oversaturated-selector':call(sel,z,t,x,t), 113 'lambda-shadow-unused':core(4,core(2,0)), 114 'lambda-capture':core(4,core(2,1)), 115 'literal-stem-construction':call(core(5,TRUE),z), 116 'literal-fork-call':call(core(5,pair(LEAF,LEAF)),z), 117 'list-duplicate':core(8,[z,z]), 118 'opaque-consumer':call(core(2,1),z), 119 'malformed-kind':core(99), 120 } 121 rows += list(examples.items()) 122 rng=random.Random(718) 123 def gen(depth): 124 atoms=[t,z,x,core(2,2),core(5,nat(17)),core(5,selector)] 125 if depth==0:return rng.choice(atoms) 126 branch=rng.randrange(6) 127 if branch==0:return rng.choice(atoms) 128 if branch==1:return core(4,gen(depth-1)) 129 if branch==2:return call(t,gen(depth-1),gen(depth-1)) 130 if branch==3:return call(sel,gen(depth-1),gen(depth-1),gen(depth-1)) 131 if branch==4:return core(8,[gen(depth-1),gen(depth-1)]) 132 return app(gen(depth-1),gen(depth-1)) 133 rows += [(f'generated-{i}',gen(4)) for i in range(256)] 134 return rows 135 136 137 SELECTOR='''!export choose 138 triage leaf stem fork = t (t leaf stem) fork 139 choose yes no value = triage no (_ : yes) (_ _ : yes) value 140 ''' 141 142 143 def main(): 144 p=argparse.ArgumentParser(description=__doc__) 145 p.add_argument('tricu',type=Path) 146 p.add_argument('--directory',type=Path,required=True) 147 args=p.parse_args() 148 root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 149 workspace=root/'workspace';workspace.mkdir() 150 files={'analysis.tri':'bench/binding-analysis.tri','kernels.tri':'bench/float-significands.tri', 151 'native_math.tri':'lib/math/native.tri'} 152 for name,path in files.items():(workspace/name).write_bytes((ROOT/path).read_bytes()) 153 (workspace/'selector.tri').write_text(SELECTOR) 154 sha=lambda p:hashlib.sha256(p.read_bytes()).hexdigest() 155 report=dict(complete=False,mode='analysis-only-no-rewrites',runtime_sha256=sha(args.tricu), 156 compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'),harness_sha256=sha(Path(__file__)), 157 fixture_ast_dependency_sha256=sha(ROOT/'test/abstraction_binding_model.py'), 158 sources={name:sha(workspace/name) for name in [*files,'selector.tri']},cases=[]) 159 runner=ProbeRunner(args.tricu,root,600,memory_mib=2048) 160 try: 161 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler') 162 for name in ['analysis','selector']: 163 runner.run('compile-'+name,['compile','--file',workspace/(name+'.tri'),'--toolchain',tool, 164 '--tool-store',runner.store,'--store',runner.store,'--output',root/(name+'.arboricx'), 165 '--compile-timeout','240'],270) 166 pin=runner.imported(root/'analysis.arboricx','analysis') 167 _,_,nodes,exports,_=read(root/'selector.arboricx') 168 out=bytearray();todo=[exports['choose']] 169 while todo: 170 node=nodes[todo.pop()];out.append(node[0]);todo.extend(reversed(node[1:])) 171 selector=bytes(out) 172 report['certificate']=dict(arity=3,exclusive_arguments=[0,1],condition_argument=2, 173 selector_tree_sha256=hashlib.sha256(selector).hexdigest(), 174 selector_bundle_sha256=sha(root/'selector.arboricx'), 175 selector_source_sha256=sha(workspace/'selector.tri'), 176 authority='explicit harness contract, not inferred from source names') 177 report['analysis_bundle_sha256']=sha(root/'analysis.arboricx') 178 rows=cases(selector) 179 selector_path=root/'selector.tree';selector_path.write_bytes(selector) 180 for offset in range(0,len(rows),32): 181 chunk=rows[offset:offset+32] 182 path=root/f'bodies-{offset}.tree';path.write_bytes(tree_list([encode(n) for _,n in chunk])) 183 want=tree_list([expected(analyze(n,selector)) for _,n in chunk]) 184 got=runner.invoke(f'check-{offset}',pin,'batch',['--arg-tree-file',selector_path,'--arg-tree-file',path]) 185 expect(got,want,str(offset)) 186 for label,node in chunk: 187 uses,paths,flags=analyze(node,selector) 188 report['cases'].append(dict(name=label,classification=decision((uses,paths,flags)), 189 uses=uses,max_path_uses=max(paths),path_counts=sorted(paths), 190 escape=flags[0],unknown=flags[1],partial=flags[2],malformed=flags[3])) 191 report['complete']=True 192 print('PASS:',len(rows),'analysis decisions match independent path-enumeration oracle; no rewrites') 193 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 194 195 196 if __name__=='__main__':main()