from fractions import Fraction as F
from math import gcd
import hashlib, json, re
class Rejected(ValueError):
    pass
def need(ok, why):
    if not ok:
        raise Rejected(why)
def fields(x, names):
    need(type(x) is dict and set(x) == set(names.split()), 'FIELD_SET')
def Z(x):
    need(type(x) is str and len(x) <= 1024, 'INTEGER_STRING')
    need(re.fullmatch(r'0|-?[1-9][0-9]*', x) is not None, 'INTEGER_CANON')
    return int(x)
def R(x):
    need(type(x) is str and x.count('/') == 1, 'RATIONAL_STRING')
    a, b = map(Z, x.split('/'))
    need(b > 0 and gcd(abs(a), b) == 1, 'RATIONAL_CANON')
    return F(a, b)
def out(x):
    a, b = str(x.numerator), str(x.denominator)
    Z(a); Z(b)
    return a + '/' + b
def vec(x):
    need(type(x) is list and 1 <= len(x) <= 64, 'VECTOR_SIZE')
    return [R(v) for v in x]
def encode(s, y):
    ss, yy = vec(s), vec(y)
    need(len(ss) == len(yy) and all(v > 0 for v in ss), 'SCALE')
    dd = [v // t for v, t in zip(yy, ss)]
    rr = [v - t*d for v, t, d in zip(yy, ss, dd)]
    return {'m': len(ss), 's': [out(t) for t in ss],
            'd': [str(Z(str(d))) for d in dd], 'rho': [out(r) for r in rr]}
def decode(e):
    fields(e, 'm s d rho')
    ss, rr = vec(e['s']), vec(e['rho'])
    need(type(e['m']) is int and e['m'] == len(ss), 'DIMENSION')
    need(type(e['d']) is list, 'QUOTIENT_VECTOR')
    dd = [Z(d) for d in e['d']]
    need(len(ss) == len(rr) == len(dd), 'DIMENSION')
    need(all(t > 0 and 0 <= r < t for t, r in zip(ss, rr)), 'CELL')
    return [t*d+r for t, d, r in zip(ss, dd, rr)]
def reverse(Q, S, terminal, rhos):
    q, s, v = Z(Q), Z(S), Z(terminal)
    need(q > 0 and s > 0, 'LEDGER_PARAMETERS')
    need(type(rhos) is list and len(rhos) <= 256, 'LEDGER_LENGTH')
    orbit = [v]
    for raw in reversed(rhos):
        r = Z(raw)
        need(0 <= r < s, 'LEDGER_RESIDUAL')
        t = s*v+r
        need(t % q == 0, 'REVERSE_DIVISIBILITY')
        v = t // q
        orbit.append(v)
    return [str(Z(str(d))) for d in reversed(orbit)]
def canonical(x):
    def visit(v):
        if type(v) is str:
            v.encode('utf-8')
        elif v is None or type(v) in (bool, int):
            return
        elif type(v) is list:
            for w in v: visit(w)
        elif type(v) is dict:
            for k, w in v.items():
                need(type(k) is str, 'KEY_TYPE')
                visit(k); visit(w)
        else:
            raise Rejected('JSON_TYPE')
    visit(x)
    return json.dumps(x, sort_keys=True, ensure_ascii=True,
                      separators=(',', ':'), allow_nan=False).encode('ascii')
def loads(text):
    need(type(text) is str and len(text) <= 1000000, 'JSON_SIZE')
    def pairs(items):
        obj = {}
        for k, v in items:
            need(k not in obj, 'DUPLICATE_KEY')
            obj[k] = v
        return obj
    def bad(x):
        raise Rejected('FLOAT_OR_NONFINITE')
    obj = json.loads(text, object_pairs_hook=pairs,
                     parse_float=bad, parse_constant=bad)
    canonical(obj)
    return obj
def compute(a):
    need(type(a) is dict and type(a.get('op')) is str, 'REQUEST')
    op = a['op']
    if op == 'encode':
        fields(a, 'op s y')
        return encode(a['s'], a['y'])
    if op == 'decode':
        fields(a, 'op record')
        return {'y': [out(v) for v in decode(a['record'])]}
    if op == 'verify':
        fields(a, 'op record y')
        yy = decode(a['record'])
        need(vec(a['y']) == yy, 'IDENTITY')
        need(encode(a['record']['s'], a['y']) == a['record'], 'ENCODER')
        return {'valid': True}
    if op == 'rescale':
        fields(a, 'op record s')
        return encode(a['s'], [out(v) for v in decode(a['record'])])
    if op == 'add':
        fields(a, 'op left right')
        x, y = decode(a['left']), decode(a['right'])
        need(a['left']['s'] == a['right']['s'], 'SCALE_MISMATCH')
        return encode(a['left']['s'], [out(v+w) for v, w in zip(x, y)])
    if op == 'reverse_ledger':
        fields(a, 'op Q S terminal rhos')
        return {'orbit': reverse(a['Q'], a['S'], a['terminal'], a['rhos'])}
    if op == 'verify_ledger':
        fields(a, 'op Q S orbit rhos')
        need(type(a['orbit']) is list and 1 <= len(a['orbit']) <= 257, 'ORBIT')
        for d in a['orbit']: Z(d)
        expected = reverse(a['Q'], a['S'], a['orbit'][-1], a['rhos'])
        need(a['orbit'] == expected, 'LEDGER_IDENTITY')
        return {'valid': True}
    raise Rejected('UNSUPPORTED_OPERATION')
def attest(request, expected=None):
    a = loads(canonical(request).decode('ascii'))
    result = compute(a)
    if expected is not None:
        need(canonical(result) == canonical(expected), 'CLAIM_MISMATCH')
    return {'status': 'INSTANCE_CHECKED', 'profile': 'SRSD-RATIONAL/1',
            'request_sha256': hashlib.sha256(canonical(a)).hexdigest(),
            'request': a, 'result': result,
            'scope': 'Only this concrete request; no claim about stored prose or all reals.'}

from itertools import product, permutations, combinations
from math import isqrt
from pathlib import Path
import argparse
OQ=339949771344778
OS=10**15
OD=25*OS
OH=4948372000
OPIN='40bc6a1d52efab3d75cf343e65ac06b314f9c9c375fc02bf6d45bf6bb21f9529'
class BudgetExceeded(RuntimeError):pass
def owire(x):
    if type(x)is int:return str(x)
    if type(x)is list:return [owire(v)for v in x]
    if type(x)is dict:return {k:owire(v)for k,v in x.items()}
    return x
def omv(A,v):return [sum(a*b for a,b in zip(r,v))for r in A]
def omm(A,B):return [[sum(a*B[j][k]for j,a in enumerate(r)if a)for k in range(len(B[0]))]for r in A]
def oti(A):return [list(r)for r in zip(*A)]
def oi(n,a=1):return [[a*int(i==j)for j in range(n)]for i in range(n)]
def ov(v):need(type(v)is list and len(v)==120 and all(type(x)is int for x in v),'OMEGA_VECTOR')
def obuild():
    V=set()
    for i in range(4):
        for s in (-1,1):V.add(tuple((2*s,0)if j==i else(0,0)for j in range(4)))
    for ss in product((-1,1),repeat=4):V.add(tuple((s,0)for s in ss))
    even=[p for p in permutations(range(4))if sum(p[i]>p[j]for i in range(4)for j in range(i+1,4))%2==0]
    for a,b,c in product((-1,1),repeat=3):
        t=((0,0),(a,0),(0,b),(-c,c));V.update(tuple(t[i]for i in p)for p in even)
    V=sorted(V);nb=[[]for _ in V]
    for i,j in combinations(range(len(V)),2):
        x=y=0
        for (a,b),(c,d)in zip(V[i],V[j]):
            u,w=a-c,b-d;x+=u*u+w*w;y+=2*u*w+w*w
        if(x,y)==(8,-4):nb[i].append(j);nb[j].append(i)
    fixture={'coordinate_rule':'vertex coordinate is (a+b*phi)/2 for pair [a,b]','neighbors':nb,'schema':'OMEGA_600CELL_GRAPH_FIXTURE/1','vertex_order':'Python lexicographic order of tuples of four integer pairs','vertices':[[list(p)for p in v]for v in V]}
    need(hashlib.sha256(canonical(fixture)+b'\n').hexdigest()==OPIN,'GRAPH_PIN')
    need(len(V)==120 and all(len(r)==12 for r in nb),'GRAPH_DEGREE')
    M=[[13 if i==j else int(j in nb[i])for j in range(120)]for i in range(120)]
    C0=[[v[j][0]for j in range(4)]for v in V];C1=[[v[j][1]for j in range(4)]for v in V]
    B=[[1]+u+w for u,w in zip(C0,C1)]
    L=[[1]*120]+[[2*C0[i][j]+C1[i][j]for i in range(120)]for j in range(4)]+[[C0[i][j]+3*C1[i][j]for i in range(120)]for j in range(4)]
    K=oi(9,0);K[0][0]=25
    for j in range(4):K[j+1][j+1]=13;K[j+5][j+5]=19;K[j+1][j+5]=K[j+5][j+1]=6
    p=[1]
    for f in [[-x,1]for x in(10,11,13,16,25)]+[[211,-32,1],[205,-30,1]]:
        z=[0]*(len(p)+len(f)-1)
        for i,a in enumerate(p):
            for j,b in enumerate(f):z[i+j]+=a*b
        p=z
    N=oi(120,p[-1])
    for a in reversed(p[1:-1]):
        N=omm(M,N)
        for i in range(120):N[i][i]+=a
    for i in range(120):
        for j in range(120):
            N[i][j],r=divmod(OH*N[i][j],-p[0]);need(r==0,'INVERSE_INTEGRAL')
    return {'vertices_pairs':[[list(x)for x in r]for r in V],'neighbors':nb,'M':M,'C0':C0,'C1':C1,'B':B,'L_numerator':L,'K':K,'N':N}
def ominors(M):
    A=[[M[i][j]-9*int(i==j)for j in range(120)]for i in range(120)];old=1;out=[]
    for k in range(120):
        pivot=A[k][k];need(pivot>0,'POSITIVE_MINOR');out.append(pivot)
        for i in range(k+1,120):
            for j in range(k+1,120):
                A[i][j],r=divmod(A[i][j]*pivot-A[i][k]*A[k][j],old);need(r==0,'BAREISS_DIVISION')
        old=pivot
    return out
def ovalidate(c):
    M,C0,C1,B,L,K,N=[c[k]for k in('M','C0','C1','B','L_numerator','K','N')]
    need(M==oti(M)and all(sum(r)==25 for r in M),'REGULAR_SYMMETRIC')
    for i in range(120):
        x=y=0
        for a,b in c['vertices_pairs'][i]:x+=a*a+b*b;y+=2*a*b+b*b
        need((x,y)==(4,0),'UNIT_VERTEX')
    for j in range(4):
        u=[r[j]for r in C0];w=[r[j]for r in C1]
        need(sum(u)==sum(w)==0,'CENTERED')
        need(omv(M,u)==[13*a+6*b for a,b in zip(u,w)],'GOLDEN_MODE_0')
        need(omv(M,w)==[6*a+19*b for a,b in zip(u,w)],'GOLDEN_MODE_1')
    need(omm(oti(C0),C0)==oi(4,72)and omm(oti(C0),C1)==oi(4,-24)and omm(oti(C1),C1)==oi(4,48),'GRAM')
    need(omm(L,B)==oi(9,120)and omm(M,B)==omm(B,K),'GEOMETRY_INVERSE_UPDATE')
    need(omm(M,N)==oi(120,OH)and omm(N,M)==oi(120,OH),'NETWORK_INVERSE')
    norm=max(sum(abs(x)for x in r)for r in N);need(norm==801320608,'INVERSE_NORM')
    need(73*OQ<OD<74*OQ and 80*OQ>OD and F(73*norm,OH)<12 and F(OD*norm,OQ*OH)<12,'SEPARATION_BOUNDS')
    return ominors(M)
def oforward(d,c):
    ov(d);pairs=[divmod(OQ*z,OD)for z in omv(c['M'],d)]
    return [a for a,b in pairs],[b for a,b in pairs]
def ofull(y,r,c):
    ov(y);ov(r);need(all(0<=x<OD for x in r),'REMAINDER_RANGE');d=[]
    for x in omv(c['N'],[OD*a+b for a,b in zip(y,r)]):
        a,b=divmod(x,OQ*OH);need(b==0,'FULL_INTEGER');d.append(a)
    need(oforward(d,c)==(y,r),'FULL_FORWARD');return d
def odecode(y,s,c,budget=100000):
    ov(y);ov(s);need(all(0<=x<8 for x in s),'RESIDUE_RANGE');N=c['N'];den=2*OQ*OH;dom=[]
    for row,r in zip(N,s):
        center=OD*sum(a*(2*b+1)for a,b in zip(row,y));radius=OD*sum(abs(a)for a in row)
        lo=-((-(center-radius))//den);hi=(center+radius)//den
        vals=list(range(lo+(r-lo)%8,hi+1,8));need(len(vals)<=2,'CANDIDATE_CAP');dom.append(vals)
    a=[-((-OD*v)//OQ)for v in y];b=[-((-OD*(v+1))//OQ)-1 for v in y];nodes=0
    rows=[[(i,13)]+[(j,1)for j in ns]for i,ns in enumerate(c['neighbors'])]
    def search(ds):
        nonlocal nodes
        nodes+=1
        if nodes>budget:raise BudgetExceeded('UNRESOLVED: node budget')
        if any(not v for v in ds):return None
        changed=True
        while changed:
            changed=False
            for i,row in enumerate(rows):
                mn=sum(w*ds[j][0]for j,w in row);mx=sum(w*ds[j][-1]for j,w in row)
                if mn>b[i]or mx<a[i]:return None
                for j,w in row:
                    if len(ds[j])<2:continue
                    old=ds[j];otherlo=mn-w*old[0];otherhi=mx-w*old[-1]
                    vv=[v for v in old if otherlo+w*v<=b[i]and otherhi+w*v>=a[i]]
                    if not vv:return None
                    if vv!=old:ds[j]=vv;changed=True
        free=[j for j,v in enumerate(ds)if len(v)>1]
        if not free:
            d=[v[0]for v in ds];need(oforward(d,c)[0]==y,'MOD8_FORWARD');return d
        j=free[0]
        for v in ds[j]:
            dd=[r[:]for r in ds];dd[j]=[v];ans=search(dd)
            if ans is not None:return ans
        return None
    d=search(dom)
    need(d is not None,'NO_PREDECESSOR');need([x%8 for x in d]==s,'DECODE_RESIDUES');return d
def olambda():
    scale=10**40;r=isqrt(5*scale*scale);need(r*r<5*scale*scale<(r+1)**2,'SQRT_BOUND')
    pl,pu=F(scale+r,2*scale),F(scale+r+1,2*scale)
    def atan(n,m):
        x=sum((F((-1)**k,(2*k+1)*n**(2*k+1))for k in range(m)),F(0));y=x+F((-1)**m,(2*m+1)*n**(2*m+1))
        return min(x,y),max(x,y)
    al,au=atan(5,48);bl,bu=atan(239,16);pil,piu=16*al-4*bu,16*au-4*bl
    ll,lu=pl/(pl+piu),pu/(pu+pil)
    need(F(OQ,OS)<ll<lu<F(OQ+1,OS)and 2*OQ+1<=2*OS*ll and 2*OS*lu<2*OQ+2,'LAMBDA_FLOORS')
    return {'phi':[str(pl),str(pu)],'pi':[str(pil),str(piu)],'lambda':[str(ll),str(lu)],'input':str(2*OS),'q_floor':str(2*OQ),'lambda_floor':str(2*OQ+1)}
def oreplay():
    c=obuild();minors=ovalidate(c);records=[]
    us=[[0,1,0,0,0,0,0,0,0],[1,-3,2,-5,7,11,-13,17,-19],[10**12,-3,5,-7,11,-13,17,-19,23]]
    for u in us:
        d=omv(c['B'],u);y,r=oforward(d,c);s=[x%8 for x in d]
        need(omv(c['L_numerator'],d)==[120*x for x in u],'PARAMETER_INVERSE')
        need(ofull(y,r,c)==odecode(y,s,c)==d,'WITNESS_TRANSLATIONS')
        records.append({'parameters':u,'input':d,'output':y,'r':r,'s':s})
    states=[records[1]['input']];w=[];rem=[]
    for k in range(6):
        d=states[-1];y,r=oforward(d,c);w.append([x%8 for x in d]);rem.append(r);states.append(y)
    back=states[-1]
    for k in range(5,-1,-1):back=odecode(back,w[k],c);need(back==states[k],'HISTORY_STEP')
    need(omv(c['L_numerator'],back)==[120*x for x in us[1]],'HISTORY_PARAMETERS')
    for t in(-10**60,-128,-1,0,1,128,10**60):
        y,r=oforward([t]*120,c);a,b=divmod(OQ*t,OS);need(y==[a]*120 and r==[25*b]*120,'SCALAR_LEDGER')
    yy=records[0]['output'];need(omv(c['B'],omv(c['L_numerator'],yy))!=[120*x for x in yy],'NONCLOSURE_EXAMPLE')
    yy,_=oforward([100]+[0]*119,c);need(F(sum(yy),120)==F(29,120)and OQ*100//(OS*120)==0,'MEAN_COUNTEREXAMPLE')
    rejected=[]
    for key in('L_numerator','N'):
        c[key][0][0]+=1
        try:ovalidate(c)
        except Rejected:rejected.append(key)
        finally:c[key][0][0]-=1
    need(len(rejected)==2,'CORRUPTION_CONTROLS')
    try:odecode(records[0]['output'],records[0]['s'],c,budget=0)
    except BudgetExceeded:pass
    else:raise Rejected('BUDGET_STATUS')
    fact={'graph_sha256':OPIN,'positive_minors':120,'geometric_examples':3,'history_steps':6,'scalar_examples':7,'corruptions_rejected':rejected,'budget_exhaustion':'UNRESOLVED','formal_proof_assistant_executed':False}
    data={**c,'positive_leading_minors_M_minus_9I':minors,'examples':records,'history':{'states':states,'witnesses':w,'remainders':rem},'lambda_enclosure':olambda()}
    return fact,data
def oroot(c):
    keys=('vertices_pairs','neighbors','M','C0','C1','B','L_numerator','K','N','positive_leading_minors_M_minus_9I')
    return hashlib.sha256(canonical(owire({k:c[k]for k in keys}))).hexdigest()
def omain():
    ap=argparse.ArgumentParser();ap.add_argument('log',type=Path);ap.add_argument('--emit',type=Path);args=ap.parse_args()
    raw=args.log.read_text(encoding='utf-8');need(len(raw)<25000,'LOG_SIZE');log=loads(raw)
    need(log['name']=='treeOS_LOG'and log['contract']=='treeOS_LOG/OMEGA-SRSD/1.0','LOG_PROFILE')
    need(log['kernel']['sha256']==hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),'KERNEL_BINDING')
    need((log['omega']['Q'],log['omega']['S'],log['omega']['D'],log['omega']['h'])==(str(OQ),str(OS),str(OD),str(OH)),'LOG_PARAMETERS')
    for test in log['fixtures']:
        try:ans=attest(test['request'],test.get('expected'))
        except Rejected:need(test.get('expected_verdict')=='REJECTED','FIXTURE_REJECTION')
        else:need(test.get('expected_verdict')!='REJECTED','FIXTURE_ACCEPTED')
    fact,data=oreplay();need(oroot(data)==log['evidence']['matrix_root_sha256'],'MATRIX_ROOT')
    if args.emit:
        with args.emit.open('x',encoding='utf-8')as f:json.dump(owire(data),f,sort_keys=True,separators=(',',':'))
    print(json.dumps({'verdict':'INSTANCE_CHECKED','profile':'TREEOS-OMEGA-120/1','log_characters':len(raw),'facts':fact,'matrix_root_sha256':oroot(data),'scope':'Finite replay only; universal deductions are written proofs.'},sort_keys=True))
if __name__=='__main__':
    try:omain()
    except BudgetExceeded as e:print(json.dumps({'verdict':'UNRESOLVED','reason':str(e)}));raise SystemExit(2)
    except Exception as e:print(json.dumps({'verdict':'REJECTED','reason':str(e)}));raise SystemExit(1)