float_boundary.py (8134B)
1 #!/usr/bin/env python3 2 """Checked binary64 boundaries: structural rejection and complete arithmetic results.""" 3 import argparse 4 from functools import lru_cache 5 import hashlib 6 import json 7 from pathlib import Path 8 import random 9 10 from float_multiply import Runner, sha 11 from float_quantize import ROOT 12 from float_ieee import cases as operation_cases, OPS, oracle, class_words, QNAN, SIGN 13 from float_working import cases as chain_cases, working_tree, flag_tree 14 from float_chains import raw_rows, chain_oracle, payload 15 from base_workloads import encode as nat 16 from http_headers import LEAF, TRUE, pair, tree_list, expect 17 from source_order import end 18 19 DIAGNOSTIC=tree_list([nat(ord(c)) for c in 'binary64 word']) 20 21 def ok(value,rest=LEAF):return pair(TRUE,pair(value,rest)) 22 def err(rest=LEAF):return pair(LEAF,pair(DIAGNOSTIC,rest)) 23 24 @lru_cache(None) 25 def small_trees(size): 26 if size==1:return (LEAF,) 27 result=[bytes([1])+x for x in small_trees(size-1)] 28 for left in range(1,size-1): 29 result += [pair(a,b) for a in small_trees(left) for b in small_trees(size-1-left)] 30 return tuple(result) 31 32 33 def decode_word(raw): 34 original=raw;value=0;bit=0 35 while raw[0]==2: 36 stop=end(raw,1);head=raw[1:stop];raw=raw[stop:] 37 if head not in (LEAF,TRUE):return None 38 value |= int(head==TRUE)<<bit;bit+=1 39 if bit>64:return None 40 if raw!=LEAF or nat(value)!=original:return None 41 return value 42 43 44 def boundary_cases(): 45 rng=random.Random(756) 46 words=class_words()+[0]+[v for k in range(64) for v in [1<<k,(1<<(k+1))-1]]+[rng.getrandbits(64) for _ in range(128)] 47 rows=[nat(w) for w in words]+[tree for size in range(1,9) for tree in small_trees(size)] 48 for depth in range(65): 49 for bad in [TRUE,pair(LEAF,LEAF),pair(pair(LEAF,LEAF),nat(1)),pair(bytes([1])+TRUE,nat(1))]: 50 for _ in range(depth):bad=pair(TRUE,bad) 51 rows.append(bad) 52 rows += [nat(1<<64),nat((1<<65)-1),nat(1<<256)] 53 return list(dict.fromkeys(rows)) 54 55 56 def main(): 57 parser=argparse.ArgumentParser(description=__doc__) 58 parser.add_argument('tricu',type=Path);parser.add_argument('--directory',type=Path,required=True) 59 parser.add_argument('--library',action='store_true',help='test library-only source closure rather than boundary candidate') 60 parser.add_argument('--support-bundle',type=Path,help='exercise complete binary64 providers from this support artifact') 61 args=parser.parse_args() 62 if args.support_bundle and not args.library:parser.error('--support-bundle requires --library') 63 root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 64 work=root/'workspace';work.mkdir() 65 (work/'tricu.workspace').write_text('tricu.workspace.v1\n') 66 sources={'driver.tri':'bench/float-boundary-driver.tri','float_boundary.tri':'bench/float-boundary.tri','working.tri':'bench/float-working.tri','chains.tri':'bench/float-chains.tri','ieee.tri':'bench/float-ieee.tri','product_quotient.tri':'bench/float-finite-product-quotient.tri', 67 'finite.tri':'bench/float-finite.tri','adders.tri':'bench/float-adders.tri', 68 'multiply.tri':'bench/float-multiply.tri','near.tri':'bench/float-near-jam.tri', 69 'aligned.tri':'bench/float-aligned-quantize.tri','fast.tri':'bench/float-quantize-fast.tri', 70 'quantize.tri':'bench/float-quantize.tri','pipelines.tri':'bench/float-pipelines.tri', 71 'kernels.tri':'bench/float-significands.tri','layouts.tri':'bench/float-layouts.tri', 72 'native_math.tri':'lib/math/native.tri'} 73 if args.library: 74 sources={'driver.tri':'test/float_boundary_driver.tri','binary64.tri':'lib/math/binary64.tri','native_math.tri':'lib/math/native.tri'} 75 for path in sorted((ROOT/'lib/math/binary64').glob('*.tri')): 76 sources['binary64_'+path.name]=str(path.relative_to(ROOT)) 77 for name,path in sources.items():(work/name).write_bytes((ROOT/path).read_bytes()) 78 report=dict(complete=False,scope='checked binary64 boundary and arithmetic acceptance', 79 runtime_sha256=sha(args.tricu),compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'), 80 harness_sha256=sha(Path(__file__)),sources={n:sha(ROOT/p) for n,p in sources.items()},checks=[],demand=[]) 81 report['library_source']=args.library 82 runner=Runner(args.tricu,root,2400,memory_mib=2048) 83 try: 84 if args.support_bundle: 85 from float_fixture import stage_providers 86 report['artifact_providers']=stage_providers(runner,work,args.support_bundle, 87 ['binary64','binary64_kernels','native_math']) 88 report['workspace_sources']={p.name:sha(p) for p in work.glob('*.tri')} 89 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler');bundle=root/'boundary.arboricx' 90 runner.run('compile',['compile','--file',work/'driver.tri','--toolchain',tool,'--tool-store',runner.store, 91 '--store',runner.store,'--output',bundle,'--compile-timeout','240'],270) 92 pin=runner.imported(bundle,'boundary');report['bundle_sha256']=sha(bundle) 93 def run(label,name,rows,wanted): 94 file=root/(label+'.input.tree');file.write_bytes(tree_list(rows)) 95 actual=runner.invoke(label,pin,name,['--arg-tree-file',file,'--profile-full-result']) 96 expect(actual,tree_list(wanted),label) 97 report['checks'].append(dict(label=label,cases=len(rows),input_sha256=sha(file),output_sha256=hashlib.sha256(actual).hexdigest())) 98 rows=boundary_cases();report['boundary_cases']=len(rows) 99 report['accepted_words']=sum(decode_word(r) is not None for r in rows) 100 for name in ['words','imports','transports']: 101 for start in range(0,len(rows),24): 102 batch=rows[start:start+24];wanted=[] 103 for raw in batch: 104 word=decode_word(raw);rest=nat(17) if name!='transports' else LEAF 105 wanted.append(err(rest) if word is None else ok(working_tree(word) if name=='imports' else raw,rest)) 106 run(f'{name}-{start}',name,batch,wanted) 107 bad=[r for r in rows if decode_word(r) is None] 108 for op in OPS: 109 rows=operation_cases(op);report[op+'_cases']=len(rows) 110 for start in range(0,len(rows),12): 111 batch=rows[start:start+12];wanted=[] 112 for a,b in batch: 113 success,result=oracle(a,b,op) 114 wanted.append(ok(payload(result)) if success else err()) 115 run(f'{op}-{start}',op,[pair(nat(a),nat(b)) for a,b in batch],wanted) 116 rejects=[pair(b,nat(QNAN)) for b in bad]+[pair(nat(QNAN),b) for b in bad] 117 for start in range(0,len(rejects),24): 118 batch=rejects[start:start+24];run(f'reject-{op}-{start}',op,batch,[err()]*len(batch)) 119 rows=chain_cases();report['chain_cases']=len(rows) 120 for start in range(0,len(rows),12): 121 batch=rows[start:start+12] 122 # raw_rows encodes a whole list; unwrap its element trees for run(). 123 raw=raw_rows(batch);items=[] 124 while raw!=LEAF: 125 stop=end(raw,1);items.append(raw[1:stop]);raw=raw[stop:] 126 run('chains-'+str(start),'chains',items,[payload(chain_oracle(r)) for r in batch]) 127 flags=[flag_tree([bool(mask&(1<<i)) for i in range(5)]) for mask in range(32)] 128 run('flag-views','flagViews',flags,flags) 129 for name,wanted in [('leftDemand',err()),('bitDemand',err()),('widthDemand',err()), 130 ('highZeroDemand',err()),('remainderDemand',TRUE),('nanValidation',err()),('trustedNanDemand',nat(QNAN|1))]: 131 actual=runner.invoke('demand-'+name,pin,name,['--arg','0']) 132 expect(actual,wanted,name);report['demand'].append(dict(name=name,outcome='expected-result')) 133 report['total_checks']=sum(r['cases'] for r in report['checks']) 134 report['complete']=True 135 print(json.dumps({k:v for k,v in report.items() if k not in ['checks','sources']},indent=2)) 136 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 137 138 if __name__=='__main__':main()