diff --git a/research/r437-residual-contract/.gitattributes b/research/r437-residual-contract/.gitattributes new file mode 100644 index 0000000000..c51f720d5b --- /dev/null +++ b/research/r437-residual-contract/.gitattributes @@ -0,0 +1,4 @@ +inputs/** -text -diff +adapter.py -text -diff +R437-UPSTREAM-NOTICE.md -text -diff +R437-LICENSE -text -diff diff --git a/research/r437-residual-contract/EXPECTED.json b/research/r437-residual-contract/EXPECTED.json new file mode 100644 index 0000000000..8e34cd5fbe --- /dev/null +++ b/research/r437-residual-contract/EXPECTED.json @@ -0,0 +1,154 @@ +{ + "add_pass": [ + { + "modulus": 3, + "payload_bits": 108, + "preparations": [ + 2, + 2, + 1, + 1, + 2, + 2 + ] + }, + { + "modulus": 9, + "payload_bits": 972, + "preparations": [ + 2, + 2, + 4, + 4, + 2, + 2 + ] + } + ], + "encoded": [ + { + "coordinate": 0, + "field": 0, + "half": false, + "high_seed": 0, + "kind": "good", + "negative": false, + "preparations": 2, + "reverse": false, + "slots": [ + 1, + 0 + ], + "value": 2 + }, + { + "coordinate": 90, + "field": 0, + "half": false, + "high_seed": 1, + "kind": "good", + "negative": true, + "preparations": 2, + "reverse": false, + "slots": [ + 1, + 0 + ], + "value": 4 + }, + { + "coordinate": 12, + "field": 0, + "half": false, + "high_seed": 0, + "kind": "pair", + "negative": false, + "preparations": 3, + "reverse": false, + "slots": [ + 1, + 0, + 0 + ], + "value": 1 + }, + { + "coordinate": 0, + "field": 57, + "half": false, + "high_seed": 1, + "kind": "pair", + "negative": false, + "preparations": 2, + "reverse": false, + "slots": [ + 1, + 0 + ], + "value": 5 + }, + { + "coordinate": 12, + "field": 70, + "half": false, + "high_seed": 2, + "kind": "pair", + "negative": true, + "preparations": 2, + "reverse": true, + "slots": [ + 1, + 0 + ], + "value": 4 + }, + { + "coordinate": 5, + "field": 0, + "half": true, + "high_seed": 2, + "kind": "unit", + "negative": false, + "preparations": 0, + "reverse": false, + "slots": [], + "value": 1 + } + ], + "leaf": { + "address_cases": 3575, + "digest": "5ffa1c3ea75a1125c86b60610c9d64dc706a88f24210cf97a17675b53b202c7c", + "mutants": [ + "omit_sign", + "wrong_inverse" + ], + "widths": [ + 1, + 2, + 7, + 26, + 63 + ] + }, + "pair_mutant": { + "correct": 5, + "mutant": 1, + "mutation": "replace_pair_numerator_with_denominator" + }, + "scope": "actual word-tape coefficients at finite source-bound controls; literal leaf coordinate algebra, not a complete GL64 packet", + "source": { + "ancestor": 27776, + "copy": 1603, + "current_request_digest": "cbfea55f5cd0b74a2a0d4292ad0139d2b5bb73127951127698030bc90c73c532", + "modulus": 9, + "q": 3, + "ranks": [ + 26, + 7 + ], + "widths": [ + 2048, + 832 + ] + } +} diff --git a/research/r437-residual-contract/PROOF.md b/research/r437-residual-contract/PROOF.md new file mode 100644 index 0000000000..1efe2e325a --- /dev/null +++ b/research/r437-residual-contract/PROOF.md @@ -0,0 +1,274 @@ +# Encoded residual weights and the completed leaf invoice + +This is a source-bound refinement and cost audit, not a new normal form. It +adapts the generated-weight grammar and completed weighted leaf of Jose Manuel's +PR2697 and David Arias's PR2753, and supplies a concrete interface for Nick +Petalas's conditional residual/CALL theorem (PR3041) and the current-source +translation audit PR3986. The new executable evidence uses the actual R437/OQ4 +rank-26 ancestor and rank-seven COPY specification, nonzero high fields and the +unchanged encoded evaluator. The invoice descends through `stream.add_pass`: +**each leaf atom requires six closed coefficient evaluations per physical +prefix**, not the three symbolic ADD requests visible in `trace.leaf`. + +Sources and exact predecessor pins are in SOURCES.json. The normal forms, +weighted leaf identity, word arithmetic, source construction and earlier +conditional correspondence remain credited predecessor results. This note +makes their current interface and previously opaque preparation multiplicities +explicit; it does not claim to have first discovered the weighted-swap identity. + +## 1. Domain and remaining primitive contracts + +Let R=Z/(q^w), for an admitted odd prime q and w>=1. The algebra below actually +works for every odd prime; finite q=3 and q=5 controls are outside the selected +supplier's large-prime admission domain. A compiled source specification has +m=64, rank 1<=r<=42, invertible low header, and a fixed preparation invertible +modulo q. Each frozen raw high field is canonical, with entries in +[0,q^(w-1)). Thus H=(low+q high)B is invertible over R. Its projector is +E=H diag(I_r,0)H^-1. The source code, preparation, rank and good/fallback label +are authenticated, not supplied by an untrusted event. + +The root weight is a unit u, the Program is chronological, and every generated +size is positive and is exactly r floor(n/64), floor(n/64), or +floor(floor(n/64)/2), as declared. Fields retain their complete original source +codes and ordinals. Numerical words have the source's arithmetic margins. + +We use the established word arithmetic and record-codec contracts: encoded +operations compute their stated ring/integer operations and preserve borrowed +inputs, with sufficient scratch capacity. We also retain the physical +`atom_swap`, `add_pass`, `sign_address`, packet-copy and counter contracts when +lifting address algebra to complete Boolean packets. This note proves neither +a new implementation nor a sublinear tariff for those primitives. No payload +independence, zero initialization, distinct prefix values, or distributional +assumption is used. The separate recursive stock, NODE/hosting/return, +parking, source production and complete visited-cell premises remain open. + +## 2. Exact generated coefficient, including pair order + +Let a_l(i) be the weight at coordinate i after l STEP records, with + a_0(i)=u. For a STEP from width n put f=floor(n/64). Define + b(j,t)=a_(l-1)(jf+t) for j<64, and b(j,t)=1 for j>=64. +Let d_k denote the good pivots, or d_j and pi the fallback diagonal and row +permutation, computed from that STEP's frozen projector. + +The exact recurrence is: + +* GOOD: a_l(i)=d_floor(i/f) a_(l-1)(i), 0<=i=64)`. A half flag is admitted only for UNIT. In particular a +half reset does not inherit the root unit or an ancestor coefficient. + +Every quantity in this recurrence is defined and is a unit. A good low class +has nonzero leading pivot minors modulo q; the same pivot denominators remain +units at every high lift. A split rank-r projector with these pivots has zero +Schur block, so `good_pivots`' full-ring check succeeds. For fallback, the +unweighted two-bank residual W_E satisfies W_E^2=I. Unit-pivot elimination over +the local ring therefore produces a diagonal of units. An entry is a unit +exactly when its reduction modulo q is nonzero; induction through the finite +elimination steps shows that the first-unit pivot choices and permutation are +those of the fixed low-class plan. Skipping an exactly zero elimination is +algebraically identical to subtracting its zero multiple. Thus all high lifts +share the compiled itinerary. These are the retained local-ring facts, here +applied to the exact source objects consumed by the callback. + +Induction on l now proves the unit claim. Every head ancestor coordinate is +less than 64f<=n; a tail operand is the constant one. GOOD coordinates are less +than rf (a y, a^-1 x). + +Every pair is disjoint, so a width-c leaf applies this formula simultaneously +to i=0,...,c-1 with tail coordinate c-1-i. The full coordinate map is a +bijection and an involution. Extend it by the identity on each complete prefix +ordinal, unused-row ordinal, and before/gap/suffix coordinate. Composition then +acts on every Boolean payload by the corresponding address permutation. +This is a pointwise statement, so repeated prefixes and arbitrary correlations +or dirty input bits do not change it. Preservation of spectators is stronger +than a volume-only equality. + +For a same-bank fallback child, the retained two half UNIT resets reverse its +second row before and after the main invocation. If f is odd the unpaired +middle atom is a spectator; if f=1 no reset is emitted. PR3041 proves this +geometry and the literal residual/CALL continuation. Its substitution premise +can use the coefficient and leaf contracts above. A width c>=64 still needs +the complete smaller-node contract, original-width stock and physical +CALL/RETURN hypotheses. Strong induction becomes available only after the +completed-primitive and capacity premises of the existing +NODE/hosting/merge implication are discharged; width descent alone +is not that proof. + +## 4. Exact preparation multiplicity and complete component invoice + +Fix one physical prefix and one leaf coordinate. Let the evaluation tree of +a_l(i) contain G GOOD nodes, P PAIR nodes, U UNIT leaves, R root leaves, and C +tail CONSTANT leaves. This tree is the literal callback tree: identical +ancestor coordinates are counted twice when visited twice. + +Beyond arithmetic internal to preparing matrices, it performs exactly: + +| Component inside one `weight` call | Count | +| --- | ---: | +| `prepare` plus `good_pivots` | G | +| `prepare` plus `fallback` | P | +| Scalar multiplications combining returned values | G+2P | +| Pair denominator inversions | P | +| Pending VALUE pops / STEP reads | G+P+U+R / G+P+U | +| Pending MULTIPLY, PAIR and CONSTANT pops | G+P+C | + +Root and UNIT copies, all typed-stack serialization and clearing, index +arithmetic, level/coordinate guards, field/code scans and head resets are also +charged. They are not included in the scalar arithmetic column. At depth l, +G+P<=2^l-1. This is a work bound, not a simultaneous matrix-storage bound. +No root-depth/current-width coupling is used to absorb this exponential +ancestor work into a current-width linear tariff. Such an absorption requires +its own complete source assumptions. +For pi(j)=j<64 the answer simplifies algebraically to d_j, but +`Callback.weight` still evaluates the identical head ancestor twice. The +separate `Page.child_weight` shortcut is not on the production +`selected_coefficient` child path. The encoded fixed-field control below +observes preparations at slots [1,0,0], with answer one. + +Define K_pi(i) to be the complete elementary cost of one positive +`children.coefficient` call on that prefix and coordinate. Its definition +includes two prime-power checks and two Callback constructions/closures, +parent and extended-program validation, all program copying in `extend`, +complete numerical and stack work above, and clearing the temporary program. +The two admissions validate exactly h+(h+1)=2h+1 STEP records for parent depth +h. The legacy seek-from-start implementations charge every intervening record +scan; no random access is free. Matrix preparation includes reading the entire +4096-entry field, raw-header construction, rational constants, inversion and +products. Let J_pi(i) be the additional inverse, negate and disposal cost when +`negative_inverse` is true. K and J are actual costs, not unit-time oracles. + +There are three symbolic ADDs per leaf coordinate. But `stream.add_pass` +executes `traverse(False)` and `traverse(True)`, **each** calling +`prepare_coefficient`. Therefore the exact coefficient contribution is + + sum over physical prefixes pi and i', 'exec'), module.__dict__) + value = module.Catalogue(3) + code = replacement(Path(topology.__file__).read_text(), '==661', '==659', 1) + topo = types.ModuleType('oq4_topology') + sys.modules[topo.__name__] = topo + exec(compile(code, '', 'exec'), topo.__dict__) + return value, topo.SelectedTopology(value) diff --git a/research/r437-residual-contract/check.py b/research/r437-residual-contract/check.py new file mode 100644 index 0000000000..e74f2d772e --- /dev/null +++ b/research/r437-residual-contract/check.py @@ -0,0 +1,258 @@ +"""Actual encoded coefficient controls and independent vector-address algebra. + +The oracle uses native integers solely as an independent finite checker. +The production path keeps Word.inspect disabled; runtime sources are unchanged. +""" +from collections import Counter +from contextlib import contextmanager +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path +import adapter + +HERE=Path(__file__).resolve().parent + +def need(ok,message): + if not ok:raise ValueError(message) + +def eye(n):return [[int(i==j) for j in range(n)] for i in range(n)] +def mul(a,b,M): + out=[[0]*len(b[0]) for _ in a] + for i,row in enumerate(a): + for k,v in enumerate(row): + if v: + for j,w in enumerate(b[k]): + if w:out[i][j]=(out[i][j]+v*w)%M + return out + +def inv(a,M): + n=len(a);rows=[list(r)+e for r,e in zip(a,eye(n))] + for j in range(n): + k=next(k for k in range(j,n) if gcd(rows[k][j],M)==1) + rows[j],rows[k]=rows[k],rows[j] + z=pow(rows[j][j],-1,M);rows[j]=[z*x%M for x in rows[j]] + for i in range(n): + if i!=j: + z=rows[i][j] + if z:rows[i]=[(x-z*y)%M for x,y in zip(rows[i],rows[j])] + return [r[n:] for r in rows] + +def rational(a,M):return [[x.numerator*pow(x.denominator,-1,M)%M for x in r] for r in a] + +def prepare(spec,high,M): + raw=[[(a+spec.template.q*b)%M for a,b in zip(x,y)] for x,y in zip(spec.low,high)] + h=mul(raw,rational(spec.template.preparation,M),M);r=spec.template.rank + return mul([x[:r] for x in h],inv(h,M)[:r],M) + +def pivots(p,r,M): + rows=[x[:] for x in p];out=[] + for k in range(r): + a=rows[k][k];out.append(a);z=pow(a,-1,M) + for i in range(k+1,len(rows)): + c=rows[i][k]*z%M + if c:rows[i]=[(x-c*y)%M for x,y in zip(rows[i],rows[k])] + need(all(x==0 for row in rows[r:] for x in row[r:]),'independent zero Schur complement') + return out + +def fallback(p,M): + n=len(p);rows=[[0]*(2*n) for _ in range(2*n)] + for i in range(n): + for j in range(n): + rows[i][j]=rows[2*n-1-i][2*n-1-j]=(int(i==j)-p[i][j])%M + rows[i][2*n-1-j]=rows[2*n-1-i][j]=p[i][j] + pi=list(range(2*n)) + for j in range(2*n): + k=next(k for k in range(j,2*n) if gcd(rows[k][j],M)==1) + rows[j],rows[k]=rows[k],rows[j];pi[j],pi[k]=pi[k],pi[j] + z=pow(rows[j][j],-1,M) + for i in range(2*n): + if i!=j: + c=rows[i][j]*z%M + if c:rows[i]=[(x-c*y)%M for x,y in zip(rows[i],rows[j])] + need(all(x==0 for i,row in enumerate(rows) for j,x in enumerate(row) if i!=j),'independent diagonal endpoint') + return [row[i] for i,row in enumerate(rows)],pi + +def vector(weights,kind,rank,field,reverse,half,p,M): + f=len(weights)//64 + if kind=='unit':return [1]*(f//2 if half else f) + if kind=='good': + d=pivots(p,rank,M) + return [weights[i]*d[i//f]%M for i in range(rank*f)] + d,pi=fallback(p,M) + def bank(row,j):return weights[row*f+j] if row<64 else 1 + return [d[field]*bank(pi[field],f-1-i if reverse else i)*pow(bank(field,f-1-i if reverse else i),-1,M)%M for i in range(f)] + +def setup(): + catalogue,_=adapter.load() + from catalogue import Specifications + from macro_binding import SelectedBinding + specs=Specifications(catalogue);binding=SelectedBinding(specs);defs={} + for label,ident,common,good in [('ancestor',27776,False,True),('good',1603,True,True),('bad',1603,True,False)]: + t=catalogue.template_for(ident,common);h=eye(64);r=t.rank + if good:h[0][0]=1;h[0][r]=1;h[r][0]=1;h[r][r]=2 + else: + for i in range(r):h[i],h[64-r+i]=h[64-r+i],h[i] + low=tuple(map(tuple,mul(h,inv(rational(t.preparation,3),3),3))) + d=binding.residual(ident,common,low,0) + need(d.plan.good==good,'actual low branch') + defs[label]=d + need(defs['ancestor'].plan.rank==26 and defs['good'].plan.rank==7,'current OQ4 source ranks') + return catalogue,specs,defs + +@contextmanager +def observed_prepare(): + from controller import Callback + from check_support import inspect_count + old=Callback.prepare;calls=[] + def wrapped(self,slot,code,scope): + calls.append((inspect_count(slot),code));return old(self,slot,code,scope) + Callback.prepare=wrapped + try:yield calls + finally:Callback.prepare=old + +def encoded(catalogue,specs,defs,kind,field=0,reverse=False,half=False,coordinate=0,negative=False,high_seed=0,check_value=True): + from check_support import no_decode,inspect_count,audit,bits + from records import Program,Fields + from words import Arena,Ring + from children import coefficient + from plan import Request + res,idx=Arena(5,131072),Arena(13);mod=res.input(9);ring=Ring(mod) + current=defs['good' if kind=='good' else 'bad'];ancestor=defs['ancestor'] + high=[] + for level in range(2): + matrix=[[0]*64 for _ in range(64)] + for k in range(3):matrix[(7*k+level)%64][(11*k+high_seed+1)%64]=(k+1+high_seed)%3 + high.append(matrix) + program=Program.fixture(idx,res,2048,2,[(0,ancestor.code,26,0,0,0)],catalogue.codes.bits) + fields=Fields.fixture(idx,res,[(ancestor.code,high[0]),(current.code,high[1])],catalogue.codes.bits) + saved=bits(program.tape),bits(fields.tape) + p0=prepare(specs[ancestor.code],high[0],9);p1=prepare(specs[current.code],high[1],9) + a=vector([2]*2048,'good',26,0,False,False,p0,9) + expected=vector(a,kind,7,field,reverse,half,p1,9)[coordinate] + index=idx.input(coordinate) + with observed_prepare() as calls: + with no_decode():value=coefficient(ring,idx,program,fields,specs,current.code,Request('child',index,child_kind=kind,field=field,reverse=reverse,half=half,negative_inverse=negative)) + observed=inspect_count(value) + if negative:expected=-pow(expected,-1,9)%9 + if check_value:need(observed==expected,'actual encoded child coefficient equals independent vector contract') + need(saved==(bits(program.tape),bits(fields.tape)),'borrowed program and complete raw fields unchanged') + need(program.tape.head==fields.tape.head==1,'borrowed heads restored') + # A unit descriptor stops immediately; good descends once; pair uses both + # head operands even when the native permutation fixes the field. + if kind=='unit':expected_preparations=0 + elif kind=='good':expected_preparations=2 + else: + _,pi=fallback(p1,9);expected_preparations=1+int(field<64)+int(pi[field]<64) + need(len(calls)==expected_preparations,'exact actual preparation tree count') + record=dict(kind=kind,field=field,reverse=reverse,half=half,coordinate=coordinate,negative=negative,high_seed=high_seed,value=observed,preparations=len(calls),slots=[x[0] for x in calls]) + res.free(value);idx.free(index);program.tape.clear();fields.tape.clear();ring.close();res.free(mod);audit(res);audit(idx) + return record + +def leaf_controls(): + """Literal source trace; independent complete address action, no payload sampling.""" + from numeric import Geometry + from trace import leaf + from words import Arena + from check_support import no_decode,inspect_count,audit + from types import SimpleNamespace + digest=sha256();cases=0;controls=set() + # These finite address checks complement, not prove, the universal matrix identity. + for width in (1,2,7,26,63): + idx=Arena(10);columns,depth=idx.input(1),idx.input(0) + page=Geometry(SimpleNamespace(dimension=64),idx,columns,depth,17,object()) + first,second,c=idx.input(0),idx.input(width),idx.input(width) + ops=[] + with no_decode(): + for e in leaf(page,first,second,c,'good'): + ops.append((e.kind,inspect_count(e.first),None if e.second is None else inspect_count(e.second),None if e.request is None else inspect_count(e.request.coordinate),False if e.request is None else e.request.negative_inverse)) + need(len(ops)==8*width+2,'literal eight-stage count') + need(Counter(x[0] for x in ops)==Counter({'enter':1,'return':1,'atom_swap':4*width,'add':3*width,'sign':width}),'complete primitive invoice') + for M in (3,9,25): + weights=[next(a for a in range(2+(i%3),M+2) if gcd(a,M)==1)%M for i in range(width)] + for x in range(M): + for y in range(M): + original=[(x+3*i)%M for i in range(width)]+[(y+2*i)%M for i in range(width)];state=original[:] + for kind,a,b,i,negative in ops: + if kind=='atom_swap':state[a],state[b]=state[b],state[a] + elif kind=='add':state[a]=(state[a]+(-pow(weights[i],-1,M) if negative else weights[i])*state[b])%M + elif kind=='sign':state[a]=-state[a]%M + target=[weights[i]*original[2*width-1-i]%M for i in range(width)]+[pow(weights[width-1-i],-1,M)*original[width-1-i]%M for i in range(width)] + need(state==target,'literal trace complete coordinate permutation');cases+=1;digest.update(bytes(state)) + # Deleting final sign or reversing middle reciprocal must fail. + a=2 if M%2 else 3 + if gcd(a,M)==1: + for mutant in ('omit_sign','wrong_inverse'): + state=[1,2%M] + for stage in range(8): + if stage%2==0:state.reverse() + elif stage==7: + if mutant!='omit_sign':state[1]=-state[1]%M + else:state[1]=(state[1]+((-pow(a,-1,M) if mutant!='wrong_inverse' else pow(a,-1,M)) if stage==3 else a)*state[0])%M + need(state!=[2*a%M,pow(a,-1,M)],'semantic leaf mutant rejection');controls.add(mutant) + page.close();idx.free_many(columns,depth,first,second,c);audit(idx) + return dict(address_cases=cases,widths=[1,2,7,26,63],digest=digest.hexdigest(),mutants=sorted(controls)) + +def pair_mutant(catalogue,specs,defs): + # Compile one semantic mutation of the authenticated actual method. It still + # executes real words/stacks/matrices; cleanup runs before comparison. + import ast + import controller + path=Path(controller.__file__);tree=ast.parse(path.read_text()) + method=next(x for x in next(x for x in tree.body if isinstance(x,ast.ClassDef) and x.name=='Callback').body if isinstance(x,ast.FunctionDef) and x.name=='weight') + changed=0 + for node in ast.walk(method): + if isinstance(node,ast.Call) and isinstance(node.func,ast.Attribute) and node.func.attr=='multiply' and len(node.args)==2 and all(isinstance(x,ast.Name) for x in node.args) and [x.id for x in node.args]==['coefficient','numerator']: + node.args[1].id='denominator';changed+=1 + need(changed==1,'one exact pair numerator mutation') + namespace=dict(controller.__dict__);exec(compile(ast.fix_missing_locations(ast.Module([method],type_ignores=[])),str(path),'exec'),namespace) + original=controller.Callback.weight;controller.Callback.weight=namespace['weight'] + try:record=encoded(catalogue,specs,defs,'pair',57,False,False,0,False,1,check_value=False) + finally:controller.Callback.weight=original + need(record['value']!=5,'wrong PAIR numerator accepted') + return {'mutation':'replace_pair_numerator_with_denominator','correct':5,'mutant':record['value']} + +def stream_controls(): + from stream import add_pass + from records import Tape + from cardinal_counts import Count + from words import Arena,Ring + from check_support import bits,no_decode,audit + receipts=[] + for M in (3,9): + arena=Arena(M.bit_length()+1);mod=arena.input(M);ring=Ring(mod) + counts=[Count.literal(x) for x in (2,3,2)];extents=[x.marginal() for x in counts] + original=bytes(((i*7)^(i//5)^(i//13))&1 for i in range(12*M*M)) + source=Tape() + for bit in original:source.append(bit) + source.rewind();calls=[] + for coefficient in (2,-pow(2,-1,M)%M,2): + def prepare(): + calls.append(coefficient);return arena.literal(coefficient) + with no_decode():out,_=add_pass(source,ring,*extents,prepare) + expected=bytearray(len(original)) + def offset(b,x,g,y,s):return ((((b*M+x)*3+g)*M+y)*2+s) + for b in range(2): + for x in range(M): + for g in range(3): + for y in range(M): + for suffix in range(2): + expected[offset(b,x,g,(y+coefficient*x)%M,suffix)]=original[offset(b,x,g,y,suffix)] + need(bits(out)==bytes(expected),'actual ADD complete dirty fibre permutation') + need(bits(source)==original and source.head==1,'ADD borrowed source retained and reset') + out.clear() + need(calls==[2,2,-pow(2,-1,M)%M,-pow(2,-1,M)%M,2,2],'six physical preparations for three leaf ADD requests') + source.clear() + for extent in extents+counts:extent.close() + ring.close();arena.free(mod);audit(arena) + receipts.append({'modulus':M,'payload_bits':len(original),'preparations':calls}) + return receipts + +def run(quick=False): + catalogue,specs,defs=setup() + if quick:return {'leaf':leaf_controls(),'add_pass':stream_controls(),'scope':'literal leaf trace finite address controls; encoded coefficient suite omitted'} + cases=[('good',0,False,False,0,False,0),('good',0,False,False,90,True,1),('pair',0,False,False,12,False,0),('pair',57,False,False,0,False,1),('pair',70,True,False,12,True,2),('unit',0,False,True,5,False,2)] + records=[encoded(catalogue,specs,defs,*args) for args in cases] + return {'source':{'ancestor':27776,'copy':1603,'ranks':[26,7],'q':3,'modulus':9,'widths':[2048,832],'current_request_digest':adapter.REQUEST_DIGEST},'encoded':records,'pair_mutant':pair_mutant(catalogue,specs,defs),'leaf':leaf_controls(),'add_pass':stream_controls(),'scope':'actual word-tape coefficients at finite source-bound controls; literal leaf coordinate algebra, not a complete GL64 packet'} + +if __name__=='__main__':print(json.dumps(run(),indent=2,sort_keys=True)) diff --git a/research/r437-residual-contract/inputs/EXPECTED.json b/research/r437-residual-contract/inputs/EXPECTED.json new file mode 100644 index 0000000000..bc2585e140 --- /dev/null +++ b/research/r437-residual-contract/inputs/EXPECTED.json @@ -0,0 +1,34 @@ +{ + "word_gzip_sha256": "e432182d5b62c8bbefeb871fce30317234d707e5e18d4295e65ac21f7fd8365e", + "word_content_sha256": "da77deaf11368d016622348227657b98404b6afbc7e4f3d6fe9a246baae0dcce", + "records_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "template_content_sha256": "c425a64739981b3ae3ed6b36d1a2f42c2d35e93f007649e89d4c677d8e158fe5", + "program_sha256": "a777373994bd84681d6c2be75251ba6a04a1521580910f23afe09bb50db632b2", + "profile": { + "1": 380160, + "2": 400864, + "3": 22176, + "4": 26592, + "5": 29376, + "6": 17376, + "7": 26496, + "26": 32, + "42": 384 + }, + "live": 28416, + "physical": 28425, + "rank_mass": 1808352, + "deficit": 10272, + "emitted_events": 7814016, + "hosted_residuals": 125856, + "BIT_c": "1736646042038446578551/1000000000000000000000000", + "BIT_c_decimal": "0.001736646042038446578551", + "next_grid": "217080755254805822319/125000000000000000000000", + "invoice": { + "prefix_bits": 177, + "charged_prefix": 192, + "two_level_bits": 393, + "charged_two_level": 512, + "ROW": 18355 + } +} diff --git a/research/r437-residual-contract/inputs/geometry.json.gz b/research/r437-residual-contract/inputs/geometry.json.gz new file mode 100644 index 0000000000..a01a33c475 Binary files /dev/null and b/research/r437-residual-contract/inputs/geometry.json.gz differ diff --git a/research/r437-residual-contract/inputs/template.json.gz b/research/r437-residual-contract/inputs/template.json.gz new file mode 100644 index 0000000000..f56efc7ca3 Binary files /dev/null and b/research/r437-residual-contract/inputs/template.json.gz differ diff --git a/research/r437-residual-contract/inputs/word.json.gz b/research/r437-residual-contract/inputs/word.json.gz new file mode 100644 index 0000000000..c558a221dd Binary files /dev/null and b/research/r437-residual-contract/inputs/word.json.gz differ diff --git a/research/r437-residual-contract/test_export.py b/research/r437-residual-contract/test_export.py new file mode 100644 index 0000000000..0dcb3e52ef --- /dev/null +++ b/research/r437-residual-contract/test_export.py @@ -0,0 +1,34 @@ +"""Run the actual optimized quick CLI outside Git, then corrupt its inputs.""" +import json,os,shutil,subprocess,sys,tempfile +from pathlib import Path +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + +def run(): + sources=json.loads((HERE/'SOURCES.json').read_bytes()) + with tempfile.TemporaryDirectory(prefix='r437-residual-gitfree-') as temporary: + root=Path(temporary);package=root/'research/r437-residual-contract' + shutil.copytree(HERE,package,ignore=shutil.ignore_patterns('__pycache__','*.pyc')) + for row in sources['files']: + target=root/row['path'];target.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(ROOT/row['path'],target) + def cli(): + env=os.environ.copy();env.pop('PYTHONPATH',None) + return subprocess.run([sys.executable,'-I','-B','-O',str(package/'verify.py'),'--quick'],cwd=root,env=env,capture_output=True,text=True,timeout=70) + result=cli() + if result.returncode:raise ValueError('Git-free positive control: '+result.stderr[-2000:]) + cases=[('changed_callback',root/'research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py','changed'),('missing_template',package/'inputs/template.json.gz','missing'),('symlinked_word',package/'inputs/word.json.gz','symlink'),('false_preparation_count',package/'EXPECTED.json','receipt')] + for label,path,kind in cases: + original=path.read_bytes() + if kind=='changed':path.write_bytes(original+b'\n# changed input\n') + elif kind=='missing':path.unlink() + elif kind=='symlink': + alternate=root/'same-bytes';alternate.write_bytes(original);path.unlink();path.symlink_to(alternate) + else: + data=json.loads(original);data['add_pass'][0]['preparations']=[2,1,2];path.write_text(json.dumps(data)) + try: + result=cli() + if result.returncode==0:raise ValueError('accepted '+label) + finally: + if path.is_symlink():path.unlink() + path.write_bytes(original) + return {'status':'PASS_GITFREE_QUICK','rejected':[x[0] for x in cases]} diff --git a/research/r437-residual-contract/verify.py b/research/r437-residual-contract/verify.py new file mode 100644 index 0000000000..d0efcead2b --- /dev/null +++ b/research/r437-residual-contract/verify.py @@ -0,0 +1,43 @@ +"""Read-only replay. It never refreshes a receipt or regenerates frozen inputs.""" +import argparse,hashlib,json +from pathlib import Path +import sys +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + +def need(ok,message): + if not ok:raise ValueError(message) + +def regular(path): + need(path.is_file(),'missing input: '+str(path)) + need(not any(p.is_symlink() for p in (path,*path.parents)),'symlinked input: '+str(path)) + +def authenticate(): + sources=json.loads((HERE/'SOURCES.json').read_bytes()) + need(sources['base_commit']=='20ecf2891d80b5acf18d980b2164fb44ea7faa90','canonical base') + for row in sources['files']+sources['retained']: + path=(ROOT if 'usage' in row else HERE)/row['path'];regular(path);data=path.read_bytes() + need(hashlib.sha256(data).hexdigest()==row['sha256'],'source hash: '+row['path']) + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'],'source Git blob: '+row['path']) + expected={r['path'] for r in sources['retained'] if r['path'].startswith('inputs/')} + observed={str(p.relative_to(HERE)) for p in (HERE/'inputs').rglob('*') if p.is_file()} + need(expected==observed,'exact frozen input inventory') + return sources + +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':')) + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--quick',action='store_true');parser.add_argument('--export',action='store_true');args=parser.parse_args() + authenticate();sys.path.insert(0,str(HERE)) + if args.export: + from test_export import run + result=run() + else: + from check import run + result=run(args.quick);expected=json.loads((HERE/'EXPECTED.json').read_bytes()) + if args.quick: + need(canonical({k:result[k] for k in ('leaf','add_pass')})==canonical({k:expected[k] for k in ('leaf','add_pass')}),'typed quick receipt') + else:need(canonical(result)==canonical(expected),'typed complete receipt') + print(json.dumps({'status':'PASS_R437_RESIDUAL_CONTRACT','scope':'quick' if args.quick else 'Git-free quick export' if args.export else 'actual encoded coefficients and finite leaf controls','supplier_admitted':False},sort_keys=True)) + +if __name__=='__main__':main()