diff --git a/research/staged544-stationary-pairs/.gitattributes b/research/staged544-stationary-pairs/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/staged544-stationary-pairs/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/staged544-stationary-pairs/.gitignore b/research/staged544-stationary-pairs/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/staged544-stationary-pairs/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/staged544-stationary-pairs/CHECKS-base.json b/research/staged544-stationary-pairs/CHECKS-base.json new file mode 100644 index 0000000000..8a39a8992b --- /dev/null +++ b/research/staged544-stationary-pairs/CHECKS-base.json @@ -0,0 +1,275 @@ +{ + "baseline_semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + }, + "edited_whole_words": [ + { + "addresses": [ + [ + "A", + 1794 + ], + [ + "B", + 698 + ] + ], + "frames": [ + [ + 85, + 414 + ], + [ + 7, + 17, + 67, + 392 + ] + ], + "profile": { + "1": 2444, + "2": 726, + "3": 222, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "A", + 1807 + ], + [ + "A", + 1810 + ] + ], + "frames": [ + [ + 120, + 435 + ], + [ + 120, + 435 + ] + ], + "profile": { + "1": 2446, + "2": 722, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "B", + 362 + ], + [ + "B", + 366 + ] + ], + "frames": [ + [ + 11, + 18, + 38, + 455 + ], + [ + 2, + 9, + 16, + 36, + 453 + ] + ], + "profile": { + "1": 2439, + "2": 726, + "3": 225, + "4": 101, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "restore", + 164 + ], + [ + "restore", + 165 + ] + ], + "frames": [ + [ + 1, + 4, + 10, + 16, + 34, + 64, + 128, + 256 + ], + [ + 1, + 4, + 10, + 16, + 34, + 64, + 128, + 256 + ] + ], + "profile": { + "1": 2442, + "2": 724, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + } + ], + "ledger": { + "recursive_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "children": 3519, + "rank_mass": 5134, + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "helper_roles": 408, + "dirty_buffers": 91, + "live_inputs": 632, + "native_warps": 72, + "initial_corrections": 36, + "primitive_inventory": { + "precondition": { + "add": 136, + "scale": 56 + }, + "compensation": { + "add": 5736 + }, + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "cut": { + "add": 176 + }, + "B": { + "add": 1796, + "scale": 73 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + } + }, + "scalar_numerator_bits": 4, + "scalar_denominator_bits": 4, + "added_gates_helpers_buffers": 0, + "proved": [ + "All final paired frames and fixed boundaries by exact subspace enumeration; every paired local invoice", + "Arbitrary-dirty operator and cleanup unchanged for every frame-only edit by identical semantic fields", + "Complete exact free-operator baseline plus four edited whole-word controls per provider" + ], + "unknown": [ + "Fresh native Gaussian/Clifford phase implementation", + "Physical allocation/hosting and owner chronology", + "Uniform precision, stock and tape tariffs", + "All-size compiler and outer/supplier admission", + "Analytic and BIT assumptions" + ], + "unknown_costs_are_zero": false, + "new_supplier_or_kappa": false + } +} diff --git a/research/staged544-stationary-pairs/CHECKS-extra.json b/research/staged544-stationary-pairs/CHECKS-extra.json new file mode 100644 index 0000000000..8a39a8992b --- /dev/null +++ b/research/staged544-stationary-pairs/CHECKS-extra.json @@ -0,0 +1,275 @@ +{ + "baseline_semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + }, + "edited_whole_words": [ + { + "addresses": [ + [ + "A", + 1794 + ], + [ + "B", + 698 + ] + ], + "frames": [ + [ + 85, + 414 + ], + [ + 7, + 17, + 67, + 392 + ] + ], + "profile": { + "1": 2444, + "2": 726, + "3": 222, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "A", + 1807 + ], + [ + "A", + 1810 + ] + ], + "frames": [ + [ + 120, + 435 + ], + [ + 120, + 435 + ] + ], + "profile": { + "1": 2446, + "2": 722, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "B", + 362 + ], + [ + "B", + 366 + ] + ], + "frames": [ + [ + 11, + 18, + 38, + 455 + ], + [ + 2, + 9, + 16, + 36, + 453 + ] + ], + "profile": { + "1": 2439, + "2": 726, + "3": 225, + "4": 101, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + }, + { + "addresses": [ + [ + "restore", + 164 + ], + [ + "restore", + 165 + ] + ], + "frames": [ + [ + 1, + 4, + 10, + 16, + 34, + 64, + 128, + 256 + ], + [ + 1, + 4, + 10, + 16, + 34, + 64, + 128, + 256 + ] + ], + "profile": { + "1": 2442, + "2": 724, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "live_inputs": 632, + "dirty_buffers": 91, + "matrix_dimension": 723, + "forward": "PASS", + "dual": "PASS", + "reverse_pullback_equals_forward": true, + "cleanup_boundary_forward_and_reverse": "PASS", + "buffer_to_live_leaks": 0, + "buffer_self_map": "identity", + "nonzero_endpoint_terms": 835 + } + } + ], + "ledger": { + "recursive_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "children": 3519, + "rank_mass": 5134, + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "helper_roles": 408, + "dirty_buffers": 91, + "live_inputs": 632, + "native_warps": 72, + "initial_corrections": 36, + "primitive_inventory": { + "precondition": { + "add": 136, + "scale": 56 + }, + "compensation": { + "add": 5736 + }, + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "cut": { + "add": 176 + }, + "B": { + "add": 1796, + "scale": 73 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + } + }, + "scalar_numerator_bits": 4, + "scalar_denominator_bits": 4, + "added_gates_helpers_buffers": 0, + "proved": [ + "All final paired frames and fixed boundaries by exact subspace enumeration; every paired local invoice", + "Arbitrary-dirty operator and cleanup unchanged for every frame-only edit by identical semantic fields", + "Complete exact free-operator baseline plus four edited whole-word controls per provider" + ], + "unknown": [ + "Fresh native Gaussian/Clifford phase implementation", + "Physical allocation/hosting and owner chronology", + "Uniform precision, stock and tape tariffs", + "All-size compiler and outer/supplier admission", + "Analytic and BIT assumptions" + ], + "unknown_costs_are_zero": false, + "new_supplier_or_kappa": false + } +} diff --git a/research/staged544-stationary-pairs/PROOF.md b/research/staged544-stationary-pairs/PROOF.md new file mode 100644 index 0000000000..e12c0b5d15 --- /dev/null +++ b/research/staged544-stationary-pairs/PROOF.md @@ -0,0 +1,152 @@ +# Stationary two-frame compatibility on the pinned staged544 words + +This is a source-bound finite theorem, not a general property of framed circuits. +On each immutable PR3734 provider, hold all scalar operators and their order, +all native maps and frames, every other scalar frame, cuts, entrance/terminal +frames, helper identities, and the caller fixed. Choose at most two distinct +ADD addresses, and simultaneously replace their common binary frames. Require +the resulting whole framed word to be legal. Then at least one of the two +single-frame replacements gives a legal intermediate word. The complete local +recursive moment cannot decrease for any real `0>v&1 and not f>>v&1:nxt.add(R.join(f,R.span((v,)))) + out.update(nxt);current=nxt + return tuple(sorted(out)) + +def topology(word): + nodes,where,bill=R.tracing(word) + def add(a):return a[0] in ('A','B','restore') and word[a[0]][a[1]][0]=='add' + addresses=sorted({a for a,r in where if add(a)}) + pairs=sorted({(x[0],y[0]) for seq in nodes.values() for x,y in zip(seq,seq[1:]) if add(x[0]) and add(y[0])}) + return nodes,where,bill,addresses,pairs + +def model(word,nodes,where,selected): + """Delete selected frames; retain exact per-register external boundaries.""" + gates=lambda a:word[a[0]][a[1]] + bounds={a:[1,(1<<512)-1] for a in selected};tracks=[];old=Counter() + registers=set(r for a in selected for r in R.touched(gates(a))) + for r in sorted(registers): + seq=nodes[r];positions=sorted(where[(a,r)] for a in selected if r in R.touched(gates(a))) + groups=[] + for pos in positions: + if groups and pos==groups[-1][-1]+1:groups[-1].append(pos) + else:groups.append([pos]) + for group in groups: + successor=seq[group[-1]+1] + require(successor[1]!='map','map must have an explicit entry check') + before,after=seq[group[0]][2],successor[3] + aa=tuple(seq[i][0] for i in group) + for i in group:old[R.rank(seq[i][3])-R.rank(seq[i][2])]+=1 + old[R.rank(after)-R.rank(seq[group[-1]][3])]+=1 + first,last=aa[0],aa[-1] + bounds[first][0]=R.join(bounds[first][0],before);bounds[last][1]&=after + if successor[1]=='check':bounds[last][0]=R.join(bounds[last][0],after) + tracks.append((r,before,aa,after,successor[1])) + return bounds,tracks,old + +def bill_delta(tracks,old,assignment): + new=Counter() + for _,p,aa,q,kind in tracks: + chain=[p]+[assignment[a] for a in aa]+[q] + require(all(R.contained(x,y) for x,y in zip(chain,chain[1:])),'final pair containment') + if kind=='check':require(chain[-2]==q,'fixed native/cut boundary') + for x,y in zip(chain,chain[1:]):new[R.rank(y)-R.rank(x)]+=1 + delta=tuple(new[k]-old[k] if k else 0 for k in range(10)) + require(sum(k*n for k,n in enumerate(delta))==0,'rank mass drift') + return delta + +def direct_orders(tracks,old,a,b,fa,fb,olda,oldb): + # The only nonconstant relation in a coupled pair is Fa <= Fb. + first_a=R.contained(fa,oldb);first_b=R.contained(olda,fb) + for yes,assignment in ((first_a,{a:fa,b:oldb}),(first_b,{a:olda,b:fb})): + if yes:bill_delta(tracks,old,assignment) + return first_a,first_b + +def profiles(hist): + return [{'delta':list(d),'count':n,'caps':R.caps(d),'prefixes':[sum(R.caps(d)[:j]) for j in range(1,9)], + 'nonimproving':R.all_power_nonnegative(d)} for d,n in sorted(hist.items())] + +def census(word): + nodes,where,baseline,addresses,pairs=topology(word) + singles=Counter();joint=Counter();cells=Counter();counts=Counter();quotients=Counter();records=[];samples={};false=[] + for a in addresses: + bounds,tracks,old=model(word,nodes,where,(a,)) + for f in frames(*bounds[a]): + d=bill_delta(tracks,old,{a:f});singles[d]+=1 + intervals=set() + for a,b in pairs: + bounds,tracks,old=model(word,nodes,where,(a,b)) + require(any(aa==(a,b) for _,_,aa,_,_ in tracks),'uncoupled pair leaked') + la,ha=bounds[a];lb,hb=bounds[b] + ha &= hb;lb=R.join(lb,la) + require(R.contained(la,ha) and R.contained(lb,hb),'invalid propagated interval') + intervals.update(((la,ha),(lb,hb))) + quotients[(R.rank(ha)-R.rank(la),R.rank(hb)-R.rank(lb))]+=1 + olda=R.span(tuple(word[a[0]][a[1]][-1]));oldb=R.span(tuple(word[b[0]][b[1]][-1])) + dims=set();rows=[] + for fa in frames(la,ha): + for fb in frames(lb,hb): + if not R.contained(fa,fb):continue + assignment={a:fa,b:fb};delta=bill_delta(tracks,old,assignment) + joint[delta]+=1;dims.add((R.rank(fa),R.rank(fb))) + first_a,first_b=direct_orders(tracks,old,a,b,fa,fb,olda,oldb) + require(first_a or first_b,'legal final pair without direct legal intermediate') + # Recheck the entire affected boundary system for the stated intermediate. + interim={a:fa,b:oldb} if first_a else {a:olda,b:fb} + bill_delta(tracks,old,interim) + counts['first_a_legal']+=first_a;counts['first_b_legal']+=first_b + rows.append([list(R.basis(fa)),list(R.basis(fb)),list(delta),first_a,first_b]) + if fa!=olda and fb!=oldb:samples.setdefault(a[0]+'-'+b[0],[a,b,list(R.basis(fa)),list(R.basis(fb)),list(delta)]) + predicted=set() + for da in range(R.rank(la),R.rank(ha)+1): + for db in range(max(da,R.rank(lb)),R.rank(hb)+1): + cap=R.rank(R.join(la,ha&lb)) + minimum=R.rank(lb)+max(0,da-cap) + if minimum<=db:predicted.add((da,db)) + else:false.append([a,b,da,db,minimum,list(R.basis(la)),list(R.basis(ha)),list(R.basis(lb)),list(R.basis(hb))]) + require(dims==predicted,'dimension-feasibility lemma differs from exhaustive subspaces') + for da,db in dims: + row=next(x for x in rows if len(x[0])==da and len(x[1])==db) + cells[tuple(row[2])]+=1 + records.append([a,b,rows]) + require(all(R.all_power_nonnegative(d) for d in singles|joint),'non-improvement sign not certified') + total=len(addresses)*(len(addresses)-1)//2 + return {'add_addresses':len(addresses),'all_unordered_distinct_pairs':total, + 'coupled_pairs':len(pairs),'uncoupled_pairs_by_independence':total-len(pairs), + 'single_frame_assignments':sum(singles.values()),'pair_frame_assignments':sum(joint.values()), + 'pair_dimension_cells':sum(cells.values()),'sequential':dict(counts),'no_legal_intermediate':0, + 'quotient_dimensions':{str(k):v for k,v in sorted(quotients.items())}, + 'single_profiles':profiles(singles),'joint_profiles':profiles(joint),'dimension_profiles':profiles(cells), + 'false_dimension_cells':len(false),'false_dimension_examples':false[:4], + 'intervals':[[list(R.basis(lo)),list(R.basis(hi))] for lo,hi in sorted(intervals)], + 'all_assignment_stream_sha256':digest(records),'whole_word_samples':list(samples.values()), + 'baseline_profile':baseline} diff --git a/research/staged544-stationary-pairs/test_controls.py b/research/staged544-stationary-pairs/test_controls.py new file mode 100644 index 0000000000..fef22b6b65 --- /dev/null +++ b/research/staged544-stationary-pairs/test_controls.py @@ -0,0 +1,86 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent finite-frame controls and production-path rejection tests.""" +import itertools,json,sys +from collections import Counter +from copy import deepcopy +from pathlib import Path +sys.path.insert(0,str(Path(__file__).resolve().parent)) +import verify as V +S=V.S;R=S.R + +def need(ok,why): + if not ok:raise ValueError(why) +def rejects(f,why): + try:f() + except Exception:return + raise ValueError('accepted '+why) +def independent_span(vs): + pts={0} + for v in vs:pts|={x^v for x in tuple(pts)} + return frozenset(pts) +def independent_interval(lo,hi): + # Choose quotient representatives greedily, then enumerate every subset of + # all quotient vectors. Dimension<=3 makes this independent 2^(2^q) check tiny. + have=independent_span(lo);initial=have;reps=[] + for v in sorted(independent_span(hi)): + if v not in have:reps.append(v);have=independent_span(list(lo)+reps) + qpoints=sorted(independent_span(reps));out=set() + for bits in range(1<>i&1]);out.add(sum(1<=0 for j in range(1,9)),'nonnegative min-basis coefficients');rows+=1 + w=V.load(tag);nodes,where,bill,addresses,pairs=S.topology(w) + # Independent graph definition: the selected gates share a register and + # its chronological address list has no intervening fixed event. + found=set() + allowed=set(addresses) + for r,seq in nodes.items(): + positions={x[0]:i for i,x in enumerate(seq) if x[0] in allowed} + ordered=sorted(positions,key=positions.get) + for a,b in zip(ordered,ordered[1:]): + if positions[b]==positions[a]+1:found.add((a,b)) + need(found==set(pairs),'coupled graph') + # Source, scalar, frame and cleanup faults reach real production checks. + row=json.loads((V.P/'SOURCES.json').read_text())['snapshots'][0] + raw=(V.P/row['local']).read_bytes();rejects(lambda:V.authenticate(raw+b' ',row),'source corruption') + a,b,fa,fb,_=result['whole_word_samples'][0] + changed=deepcopy(w);changed[a[0]][a[1]][3]+=1 + need(V.scalar_projection(changed)!=V.scalar_projection(w),'scalar mutation missed') + bad=deepcopy(w);bad[a[0]][a[1]][-1]=[];rejects(lambda:C.frame_bill(bad),'illegal lowered frame') + bad=deepcopy(w);bad['cleanup']=[] + need(C.derive_cleanup(bad)!=bad['cleanup'],'cleanup mutation missed') + for lo,hi in intervals:need(independent_interval(lo,hi)==set(S.frames(R.span(lo),R.span(hi))),'independent quotient enumeration') + # A genuinely simultaneous legal pair with no legal single-edit intermediate. + # This is an abstract control, not a staged544 occurrence. + a=('A',0);b=('A',1);line1=R.span((1,));line2=R.span((2,));full=R.span((1,2)) + tracks=[(0,1,(a,b),full,'climb')];old=Counter({1:2,0:1}) + need(S.bill_delta(tracks,old,{a:line2,b:line2})==(0,)*10,'crossed-line final legal') + need(S.direct_orders(tracks,old,a,b,line2,line2,line1,line1)==(False,False),'crossed-line detector') + rejects(lambda:S.bill_delta(tracks,old,{a:line2,b:line1}),'first crossed-line intermediate') + rejects(lambda:S.bill_delta(tracks,old,{a:line1,b:line2}),'second crossed-line intermediate') + # Explicit dimension-only false positive on actual B362/B366. + w=V.load('base');nodes,where,*_=S.topology(w);a=('B',362);b=('B',366) + bounds,tracks,old=S.model(w,nodes,where,(a,b));la,ha=bounds[a];lb,hb=bounds[b];ha&=hb;lb=R.join(lb,la) + need(R.rank(la)<=4<=R.rank(ha) and R.rank(lb)<=4<=R.rank(hb),'naive 4,4 admission') + candidates=[(fa,fb) for fa in S.frames(la,ha) for fb in S.frames(lb,hb) if R.rank(fa)==4 and R.rank(fb)==4 and R.contained(fa,fb)] + need(not candidates,'false-positive actual frame assignment') + minimum=R.rank(lb)+max(0,4-R.rank(R.join(la,ha&lb))) + need(minimum==5,'dimension incompatibility witness') + # Paid rank exchange has strict concavity sign in the intended direction. + exchange=(0,1,-2,1,0,0,0,0,0,0) + need(not R.all_power_nonnegative(exchange),'favorable rank exchange wrongly certified non-improving') + need(R.all_power_nonnegative(tuple(-x for x in exchange)),'reverse exchange sign') + print('PASS_STATIONARY_CONTROLS',{'intervals':len(intervals),'sign_rows':rows,'crossed_flag':True,'false_4_4_requires':minimum}) +if __name__=='__main__':main() diff --git a/research/staged544-stationary-pairs/vendor/SOURCE-CREDITS.md b/research/staged544-stationary-pairs/vendor/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-stationary-pairs/vendor/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-stationary-pairs/vendor/audit_core.py b/research/staged544-stationary-pairs/vendor/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/staged544-stationary-pairs/vendor/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/staged544-stationary-pairs/vendor/audit_verify.py b/research/staged544-stationary-pairs/vendor/audit_verify.py new file mode 100644 index 0000000000..7f9fc1df42 --- /dev/null +++ b/research/staged544-stationary-pairs/vendor/audit_verify.py @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""Whole-word cross-check of published RETIMED and DELAYED supplier words. + +Reuses Sagar Thakrar's exact PR3687 audit_core, unchanged and authenticated +before execution. This is not a new interpreter. No construction/native checker +is imported. roger-sato with substantial OpenAI Codex assistance; Apache-2.0. +""" +from collections import Counter +from copy import deepcopy +import gzip +import hashlib +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +STAGED = {1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8} +RETIMED = {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8} +WIDTHS = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} +MOVES = ((591, 1045, 640, 644, 2, [423, 65, 20, 10]), + (641, 1085, 656, 660, -1, [427, 96, 24, 6])) +SOURCE_COMMITS = { + 3605: '3efbb5de06a49ffeea6684482f2d3fe48cdca3fb', + 3642: '044d24f12e74f228dd462c07ae2d7f3ea35e2be9', + 3653: '607a09ff441c79b215a8127a81f4cc70021d0d9b', + 3682: '431e6c6023ef352c41696469de7fb614cd4ded8c', + 3687: 'f798838eb8ede4178e94f240e7b7e54b3f80c82d', +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((HERE / 'SOURCES.json').read_text())['snapshots'] + expected = {(3687, 'vendor/audit_core.py')} + for provider in ('base', 'extra'): + expected.update((number, f'inputs/{kind}-{provider}.json.gz') for number, kind in + ((3605, 'STAGED'), (3642, 'RETIMED'), (3653, 'RETIMED'), (3682, 'DELAYED'))) + keys = [(row['source_pr'], row['local']) for row in rows] + need(len(keys) == len(expected) and set(keys) == expected, 'source mapping inventory differs') + for row in rows: + need(row['source_commit'] == SOURCE_COMMITS[row['source_pr']], 'source commit differs') + raw = (HERE / row['local']).read_bytes() + need(len(raw) == row['bytes'], 'source byte length: ' + row['local']) + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['local']) + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == row['git_blob'], 'source Git blob: ' + row['local']) + core = types.ModuleType('retained_audit_core') + path = HERE / 'vendor/audit_core.py' + # Execute the authenticated source bytes, without accepting a .pyc cache. + exec(compile(path.read_bytes(), str(path), 'exec'), core.__dict__) + return core + + +def load(kind, provider): + return json.loads(gzip.decompress((HERE / 'inputs' / f'{kind}-{provider}.json.gz').read_bytes())) + + +def events(w): + result = [] + for pos in range(len(w['B']) + 1): + result += [('warp', k, deepcopy(rec)) for k, rec in enumerate(w['warps']) if rec[0] == pos] + if pos < len(w['B']): + result.append(('gate', pos, deepcopy(w['B'][pos]))) + return result + + +def replace_events(w, seq): + result = deepcopy(w) + body, warps = [], [None] * len(w['warps']) + for kind, label, gate in seq: + gate = deepcopy(gate) + if kind == 'gate': + body.append(gate) + else: + gate[0] = len(body) + warps[label] = gate + need(all(rec is not None for rec in warps), 'lost warp in reconstruction') + result['B'], result['warps'] = body, warps + return result + + +def reconstruct(C, staged, kind): + """Literal prose recipes: adjacent shear swap, or move before first producer. + + This repeats the credited local structural arguments as an input control; + the new evidence is the full word calculation below. + """ + seq = events(staged) + for start, stop, donor, pivot, coefficient, frame in MOVES: + source = next(x for x in seq if x[:2] == ('gate', start)) + need(source[2] == ['add', donor, pivot, coefficient, 1, [429, 30]], 'source release') + if kind == 'RETIMED': + target = next(x for x in seq if x[:2] == ('gate', start + 1)) + need(target[2][0] == 'add' and target[2][2] == pivot, 'adjacent same-pivot shear') + need(not any(rec[0] == start + 1 for rec in staged['warps']), 'unexpected crossed warp') + where = seq.index(target) + 1 + else: + target = next(x for x in seq if x[:2] == ('gate', stop)) + writes = [i for i, g in enumerate(staged['B']) if i > start and g[1] == pivot] + need(writes[0] == stop, 'first producer cut') + where = seq.index(target) + changed = deepcopy(source[2]) + changed[-1] = frame + seq.insert(where, ('gate', -pivot, changed)) + seq.remove(source) + result = replace_events(staged, seq) + result['cleanup'] = C.derive_cleanup(result) + result['report']['local_profile'] = {str(k): v for k, v in RETIMED.items()} + return result + + +def semantics(C, w): + """All live and buffer inputs are symbols, with no zero-buffer assumption.""" + def endpoint(name, result): + bad_live, dirty_buffers, leaks, buffer_identity = result + need(not bad_live and not dirty_buffers and not leaks and buffer_identity, + name + ' endpoint: ' + repr(result)) + boundary = {} + rows = C.forward_rows(w, symbolic_buffers=True, + snapshot=lambda values: boundary.setdefault('defects', C.boundary_defects(w, values))) + endpoint('forward', C.endpoint_defects(w, rows)) + dual_rows = C.forward_rows(w, dual=True, symbolic_buffers=True) + endpoint('dual', C.endpoint_defects(w, dual_rows, dual=True)) + need(not boundary['defects'], 'cleanup boundary: ' + repr(boundary['defects'])) + pulled = C.transpose(C.reverse_columns(w)) + need(pulled == {r: row for r, row in rows.items() if row}, 'reverse pull-back differs from forward') + pre = C.transpose(C.reverse_columns(w, upto_cleanup=True)) + pre = {r: pre.get(r, {}) for r in set(pre) | set(range(C.N))} + need(not C.boundary_defects(w, pre), 'reverse cleanup-boundary contract') + live = C.N - len(w['removed']) + buffers = len(w['helper_final']) + need((live, buffers, len(rows)) == (632, 91, 723), 'complete symbolic domain') + # Endpoint expectations are derived by the retained checker: live x,y,h + # map to x,y+x,h; all private buffer symbols return unchanged. + return {'live_inputs': live, 'dirty_buffers': buffers, 'matrix_dimension': len(rows), + 'forward': 'PASS', 'dual': 'PASS', 'reverse_pullback_equals_forward': True, + 'cleanup_boundary_forward_and_reverse': 'PASS', + 'buffer_to_live_leaks': 0, 'buffer_self_map': 'identity', + 'nonzero_endpoint_terms': sum(len(row) for row in rows.values())} + + +def inspect(C, w, profile): + C.hygiene(w) + bill, widths, chain, _, _ = C.frame_bill(w) + need(bill == profile, 'computed profile differs') + need(w['report']['local_profile'] == {str(k): v for k, v in bill.items()}, 'declared profile differs') + need(widths == WIDTHS, 'helper widths differ') + need(w['cleanup'] == C.derive_cleanup(w), 'literal cleanup differs') + return {'semantics': semantics(C, w), 'profile': bill, 'widths': widths, + 'rank_mass': sum(r * n for r, n in bill.items())}, chain + + +def expect_rejection(C, fn, phrase): + try: + fn() + except (ValueError, C.AuditFailure) as exc: + need(phrase in str(exc), 'wrong rejection: ' + str(exc)) + return phrase + raise ValueError('mutant unexpectedly passed: ' + phrase) + + +def negative_controls(C, staged, w, kind): + controls = [] + for _, _, donor, pivot, _, _ in MOVES: + seq = events(w) + release = next(x for x in seq if x[0] == 'gate' and x[2][0] == 'add' and x[2][1:3] == [donor, pivot]) + for defect in ('omit', 'flip', 'cross_first_producer'): + changed = deepcopy(seq) + index = seq.index(release) + if defect == 'omit': + changed.pop(index) + elif defect == 'flip': + changed[index][2][3] *= -1 + else: + producer = next(x for x in changed[index + 1:] if x[0] == 'gate' and x[2][1] == pivot) + moved = changed.pop(index) + changed.insert(changed.index(producer) + 1, moved) + bad = replace_events(w, changed) + bad['cleanup'] = C.derive_cleanup(bad) + # Repair the literal inverse so stale cleanup is not the rejection. + reason = expect_rejection(C, lambda: semantics(C, bad), 'forward endpoint') + controls.append({'defect': defect, 'pivot': pivot, 'rejected_by': reason}) + old_cleanup = deepcopy(w) + old_cleanup['cleanup'] = staged['cleanup'] + # The inverse shears commute: this is a format failure, not a wrong operator. + semantic_control = semantics(C, old_cleanup) + need(old_cleanup['cleanup'] != C.derive_cleanup(old_cleanup), 'old cleanup unexpectedly literal') + controls.append({'defect': 'old_cleanup_order', 'semantics': semantic_control, + 'rejected_by': expect_rejection(C, lambda: inspect(C, old_cleanup, RETIMED), 'literal cleanup differs')}) + old_frames = deepcopy(w) + for gate in old_frames['B']: + if gate[0] == 'add' and gate[1:3] in ([640, 644], [656, 660]): + gate[-1] = [429, 30] + need(semantics(C, old_frames) == semantic_control, 'frame-only mutation changed operator') + if kind == 'RETIMED': + need(C.frame_bill(old_frames)[0] == STAGED, 'old frame control does not restore staged bill') + controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS', + 'profile': STAGED, 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'computed profile differs')}) + else: + # The later release encounters a donor that has already climbed, so + # the original rank-2 frame is now illegal, despite the same operator. + controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS', + 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'frame containment fails')}) + fake_report = deepcopy(w) + fake_report['report']['local_profile']['1'] += 1 + controls.append({'defect': 'wrong_declared_profile', 'rejected_by': + expect_rejection(C, lambda: inspect(C, fake_report, RETIMED), 'declared profile differs')}) + return controls + + +def run(C): + results = {} + for provider in ('base', 'extra'): + staged = load('STAGED', provider) + control, old_chain = inspect(C, staged, STAGED) + records = {'STAGED': control} + for kind in ('RETIMED', 'DELAYED'): + w = load(kind, provider) + need(reconstruct(C, staged, kind) == w, 'prose reconstruction differs: ' + kind) + record, chain = inspect(C, w, RETIMED) + deltas = {} + for register in set(chain) | set(old_chain): + before = Counter(d for _, d, _ in old_chain.get(register, []) if type(d) is int and d > 0) + after = Counter(d for _, d, _ in chain.get(register, []) if type(d) is int and d > 0) + delta = {r: after[r] - before[r] for r in set(after) | set(before) if after[r] != before[r]} + if delta: + deltas[register] = delta + need(deltas == {640: {1: -1, 2: -1, 3: 1}, 656: {1: -1, 2: -1, 3: 1}}, 'per-register invoice differs') + record['prose_reconstruction'] = 'exact complete JSON equality' + record['changed_register_bills'] = deltas + record['controls'] = negative_controls(C, staged, w, kind) + records[kind] = record + print('CHECKED', provider, kind, '723-register forward/dual/pull-back and 9 controls', flush=True) + results[provider] = records + return {'status': 'PASS_RETIMED_AND_DELAYED_WHOLE_WORD_AUDIT', + 'scope': 'Reused PR3687 interpreter; finite exact operator/frame audit only. No native Gaussian, owner, root, or complete supplier claim.', + 'providers': results} + + +if __name__ == '__main__': + need(sys.argv[1:] in ([], ['--write']), 'usage: verify.py [--write]') + C = authenticate() + result = run(C) + output = json.dumps(result, sort_keys=True, indent=2) + '\n' + if sys.argv[1:] == ['--write']: + (HERE / 'RESULT.json').write_text(output) + else: + need((HERE / 'RESULT.json').read_text() == output, 'committed result differs') + print(result['status']) diff --git a/research/staged544-stationary-pairs/vendor/retiming.py b/research/staged544-stationary-pairs/vendor/retiming.py new file mode 100644 index 0000000000..c33d7bbcdf --- /dev/null +++ b/research/staged544-stationary-pairs/vendor/retiming.py @@ -0,0 +1,269 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact, fixed-neighbour single-ADD retiming relaxation. + +Chris R / Clear1nsight, with substantial OpenAI assistance. The BORROW-WORD +frame contract and scalar-retiming mechanism are credited in README.md. +This module does not import the retained auditor or a numerical optimiser. +""" +from bisect import bisect_left +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(maxsize=None) +def span(vectors): + points = {0} + for v in vectors: + need(type(v) is int and 0 <= v < 512, 'invalid frame vector') + points |= {x ^ v for x in tuple(points)} + return sum(1 << x for x in points) + + +@lru_cache(maxsize=None) +def basis(mask): + answer = [] + have = 1 + for v in range(1, 512): + if (mask >> v) & 1 and not (have >> v) & 1: + answer.append(v) + have = span(tuple(answer)) + need(have == mask, 'not a binary subspace') + return tuple(answer) + + +@lru_cache(maxsize=None) +def join(a, b): + return span(basis(a) + basis(b)) + + +@lru_cache(maxsize=None) +def rank(mask): + n = mask.bit_count() + need(n > 0 and n & (n - 1) == 0, 'invalid subspace cardinality') + return n.bit_length() - 1 + + +def contained(a, b): + return not a & ~b + + +def touched(gate): + return gate[1:3] if gate[0] == 'add' else gate[1:2] + + +def tracing(word): + """Own chronological trace; centre descent is NOT persistent state. + + A check node is a fixed boundary, not a charged instruction. The census + relaxes it to a virtual climb. Every legal witness has zero such charge. + """ + full = (1 << 512) - 1 + live = set(range(704)) - set(word['removed']) + start, end = {}, {} + for r in live: + if r < 112: + start[r], end[r] = span((word['ports'][r],)), full + elif r < 224: + p = word['ports'][r - 112] + start[r] = 1 + end[r] = sum(1 << x for x in range(512) if (x & p).bit_count() % 2 == 0) + else: + start[r], end[r] = 1, full + for r, fr in word['start_extra'].items(): + start[int(r)] = span(tuple(fr)) + for r, fr in word['helper_final'].items(): + end[int(r)] = span(tuple(fr)) + current = dict(start) + nodes = {r: [] for r in live} + where = {} + bill = Counter() + + def event(r, frame, address, kind='climb'): + before = current[r] + if kind != 'map': + need(contained(before, frame), 'source frame containment') + d = rank(frame) - rank(before) + if kind == 'check': + need(d == 0, 'source fixed boundary') + elif d: + bill[d] += 1 + if kind == 'climb': + where[(address, r)] = len(nodes[r]) + nodes[r].append((address, kind, before, frame)) + current[r] = frame + + for i, gate in enumerate(word['A']): + if gate[0] == 'warp': + event(gate[1], span(tuple(gate[3])), ('check-A', i), 'check') + event(gate[1], span(tuple(gate[4])), ('map-A', i), 'map') + else: + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('A', i)) + levels = {112 + int(r): span(tuple(fr)) for r, fr in word['target_levels'].items()} + for r in range(112, 224): + event(r, levels.get(r, 1), ('target-cut', r), 'check') + for r, fr in zip(word['centers'], word['center_frames']): + u = span(tuple(fr)) + event(r, u, ('centre-cut', r), 'check') + served = {levels.get(g[1], 1) for g in word['cut'] if g[2] == r} + for v in sorted(served, key=lambda x: -rank(x)): + need(contained(v, u), 'centre nesting') + if rank(u) > rank(v): + bill[rank(u) - rank(v)] += 1 + u = v + # The main forward register remains at its declared centre entry. + warps = {} + for j, rec in enumerate(word['warps']): + warps.setdefault(rec[0], []).append((j, rec)) + for i in range(len(word['B']) + 1): + for j, rec in warps.get(i, []): + event(rec[1], span(tuple(rec[3])), ('check-B', j), 'check') + event(rec[1], span(tuple(rec[4])), ('map-B', j), 'map') + if i < len(word['B']): + gate = word['B'][i] + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('B', i)) + for i, gate in enumerate(word['restore']): + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('restore', i)) + for r in live: + event(r, end[r], ('end',)) + return nodes, where, dict(sorted(bill.items())) + + +def crosses(g, h): + """Sufficient exact scalar normal form, not all algebraic commutations.""" + if h[0] == 'add': + return g[1] != h[2] and h[1] != g[2] + return h[0] == 'scale' and h[2] != 0 + + +def segments(word, section): + if section == 'A': + cuts = [word['prelude_events'], len(word['A'])] + elif section == 'B': + cuts = sorted({0, len(word['B'])} | {rec[0] for rec in word['warps']}) + else: + cuts = [0, len(word[section])] + return list(zip(cuts, cuts[1:])) + + +def caps(delta): + return [sum(n * min(r, k) for r, n in enumerate(delta)) for k in range(1, 10)] + + +def all_power_nonnegative(delta): + """Sufficient exact certificate using decreasing positive curvatures.""" + values = caps(delta) + prefix = 0 + for value in values[:-1]: + prefix += value + if prefix < 0: + return False + return values[-1] == 0 + + +def census(word): + nodes, where, bill = tracing(word) + deltas = Counter() + counts = {} + for section in ('A', 'B', 'restore'): + gates = word[section] + count = 0 + for lo, hi in segments(word, section): + occurrences = {} + for i in range(lo, hi): + need(gates[i][0] in ('add', 'scale'), 'unexpected scalar segment') + for r in touched(gates[i]): + occurrences.setdefault(r, []).append(i) + for i in range(lo, hi): + g = gates[i] + if g[0] != 'add': + continue + lower = i + while lower > lo and crosses(g, gates[lower - 1]): + lower -= 1 + upper = i + 1 + while upper < hi and crosses(g, gates[upper]): + upper += 1 + removal = [0] * 10 + reduced, entries, exits = {}, {}, {} + for r in touched(g): + seq = nodes[r] + pos = where[((section, i), r)] + _, _, p, u = seq[pos] + need(pos + 1 < len(seq) and seq[pos + 1][1] != 'map', 'missing successor') + q = seq[pos + 1][3] + removal[rank(u) - rank(p)] -= 1 + removal[rank(q) - rank(u)] -= 1 + removal[rank(q) - rank(p)] += 1 + indices = occurrences[r] + reduced[r] = [x for x in indices if x != i] + entries[r] = seq[where[((section, indices[0]), r)]][2] + last = where[((section, indices[-1]), r)] + need(seq[last + 1][1] != 'map', 'missing exit check') + exits[r] = seq[last + 1][3] + for cut in range(lower, upper + 1): + if cut == i + 1: # Same placement as cut i, counted once. + continue + boundaries = [] + for r in touched(g): + indices = reduced[r] + j = bisect_left(indices, cut) + p = span(tuple(gates[indices[j - 1]][-1])) if j else entries[r] + q = span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r] + boundaries.append((p, q)) + lower_frame = join(boundaries[0][0], boundaries[1][0]) + upper_frame = boundaries[0][1] & boundaries[1][1] + if not contained(lower_frame, upper_frame): + continue + dims = [(rank(p), rank(q)) for p, q in boundaries] + for d in range(rank(lower_frame), rank(upper_frame) + 1): + delta = removal.copy() + for p, q in dims: + delta[q - p] -= 1 + delta[d - p] += 1 + delta[q - d] += 1 + delta[0] = 0 + need(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift') + deltas[tuple(delta)] += 1 + count += 1 + counts[section] = count + return {'per_section': counts, 'candidates': sum(counts.values()), + 'source_profile': bill, + 'deltas': [{'delta': {r: n for r, n in enumerate(d) if n}, 'count': n, + 'caps': caps(d), 'certificate': all_power_nonnegative(d)} + for d, n in sorted(deltas.items())]} + + +def apply_move(word, section, index, cut, frame): + """Apply one exact scalar retiming. Caller must rederive cleanup and audit.""" + need(section in ('A', 'B', 'restore'), 'unknown section') + gates = word[section] + need(type(index) is int and 0 <= index < len(gates), 'bad source index') + need(type(cut) is int and 0 <= cut <= len(gates), 'bad insertion cut') + need(any(lo <= index < hi and lo <= cut <= hi for lo, hi in segments(word, section)), + 'crosses prelude or native warp boundary') + g = deepcopy(gates[index]) + need(g[0] == 'add', 'only ADD moves are covered') + crossed = gates[index + 1:cut] if cut > index else gates[cut:index] + need(all(crosses(g, h) for h in crossed), 'noncommuting scalar barrier') + coefficient = Fraction(g[3], g[4]) + for h in crossed: + if h[0] == 'scale' and h[1] in touched(g): + power = (1 if h[1] == g[1] else -1) * (1 if cut > index else -1) + coefficient *= Fraction(h[2], h[3]) ** power + g[3:5] = [coefficient.numerator, coefficient.denominator] + g[-1] = list(basis(span(tuple(frame)))) + result = deepcopy(word) + result[section].pop(index) + result[section].insert(cut - (cut > index), g) + # Segment length and all warp cuts are unchanged. No warp is crossed. + return result diff --git a/research/staged544-stationary-pairs/verify.py b/research/staged544-stationary-pairs/verify.py new file mode 100644 index 0000000000..213bdf748c --- /dev/null +++ b/research/staged544-stationary-pairs/verify.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Read-only, source-authenticated census and exact dirty-state controls.""" +import gzip,hashlib,json,sys +from collections import Counter +from copy import deepcopy +from pathlib import Path +P=Path(__file__).resolve().parent +# Authenticate retained executable bytes before any retained source executes. +for _row in json.loads((P/'SOURCES.json').read_text())['snapshots']: + _raw=(P/_row['local']).read_bytes() + if len(_raw)!=_row['bytes'] or hashlib.sha256(_raw).hexdigest()!=_row['sha256'] or hashlib.sha1(b'blob '+str(len(_raw)).encode()+b'\0'+_raw).hexdigest()!=_row['git_blob']: + raise ValueError('source authentication before import: '+_row['local']) +sys.path.insert(0,str(P)) +import pairs as S + +def normal(x):return json.loads(json.dumps(x,sort_keys=True)) +def authenticate(raw,row): + S.require(len(raw)==row['bytes'],'source length') + S.require(hashlib.sha256(raw).hexdigest()==row['sha256'],'source SHA256') + S.require(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==row['git_blob'],'source blob') +def setup(): + for row in json.loads((P/'SOURCES.json').read_text())['snapshots']:authenticate((P/row['local']).read_bytes(),row) + return S.module('retained_auditor',P/'vendor/audit_core.py'),S.module('retained_semantics',P/'vendor/audit_verify.py') +def load(tag):return json.loads(gzip.decompress((P/'inputs'/f'BORROW-WORD-43{tag}.json.gz').read_bytes())) +def scalar_projection(word): + # Every semantic field is retained, except frames and derived paid report. + out=deepcopy(word) + for section in ('A','B','restore'): + for g in out[section]: + if g[0]=='add':g[-1]=None + out['report'].pop('local_profile',None) + return out + +def validation(word,result,C,A): + C.hygiene(word);bill,widths,*_=C.frame_bill(word) + S.require(bill=={int(k):v for k,v in result['baseline_profile'].items()},'baseline invoice') + S.require(C.derive_cleanup(word)==word['cleanup'],'baseline cleanup') + baseline=A.semantics(C,word);samples=[] + for a,b,fa,fb,delta in result['whole_word_samples']: + final=deepcopy(word);final[a[0]][a[1]][-1]=fa;final[b[0]][b[1]][-1]=fb + actual,inventory,*_=C.frame_bill(final) + S.require(tuple(actual.get(k,0)-bill.get(k,0) if k else 0 for k in range(10))==tuple(delta),'sample final invoice') + S.require(inventory==widths,'helper inventory') + S.require(C.derive_cleanup(final)==word['cleanup'],'unchanged inverse cleanup') + final['report']['local_profile']={str(k):v for k,v in actual.items()} + C.hygiene(final) + S.require(scalar_projection(word)==scalar_projection(final),'unchanged free-operator program') + semantic=A.semantics(C,final) + samples.append({'addresses':[a,b],'frames':[fa,fb],'profile':actual,'semantics':semantic}) + primitives={sec:dict(sorted(Counter(g[0] for g in word[sec]).items())) for sec in ('precondition','compensation','A','cut','B','restore','cleanup')} + coeff=[g for sec in ('A','B','restore') for g in word[sec] if g[0]=='add'] + return {'baseline_semantics':baseline,'edited_whole_words':samples, + 'ledger':{'recursive_profile':bill,'children':sum(bill.values()),'rank_mass':sum(k*v for k,v in bill.items()), + 'helper_widths':widths,'helper_roles':sum(widths.values()),'dirty_buffers':len(word['helper_final']), + 'live_inputs':C.N-len(word['removed']),'native_warps':len(word['warps']),'initial_corrections':len(word['initial_corrections']), + 'primitive_inventory':primitives,'scalar_numerator_bits':max(abs(g[3]).bit_length() for g in coeff), + 'scalar_denominator_bits':max(g[4].bit_length() for g in coeff),'added_gates_helpers_buffers':0, + 'proved':['All final paired frames and fixed boundaries by exact subspace enumeration; every paired local invoice', + 'Arbitrary-dirty operator and cleanup unchanged for every frame-only edit by identical semantic fields', + 'Complete exact free-operator baseline plus four edited whole-word controls per provider'], + 'unknown':['Fresh native Gaussian/Clifford phase implementation','Physical allocation/hosting and owner chronology', + 'Uniform precision, stock and tape tariffs','All-size compiler and outer/supplier admission','Analytic and BIT assumptions'], + 'unknown_costs_are_zero':False,'new_supplier_or_kappa':False}} + +def main(): + C,A=setup() + for tag in ('base','extra'): + word=load(tag);result=S.census(word) + S.require(normal(result)==json.loads((P/f'RESULT-{tag}.json').read_text()),'census receipt '+tag) + receipt=validation(word,result,C,A) + S.require(normal(receipt)==json.loads((P/f'CHECKS-{tag}.json').read_text()),'validation receipt '+tag) + print('PASS_STATIONARY_PAIRS',tag,result['coupled_pairs'],result['pair_frame_assignments'],flush=True) +if __name__=='__main__':main()