"""Fresh modal checks and guarded replay of the supplied rational tube witnesses."""
from fractions import Fraction as F
from pathlib import Path
import json
import tube_kernel as k

R=[F(9,10),F(417,500)]+[F(7,10)]*6
S=[F(9,10)]+[F(7,10)]*7


class ModalCertificate:
    def __init__(self):self.M=k.M;self.inverse=k.MI;self.center=k.C0;self.preparation=k.P0
    def membership(self,center,halfwidths=None,radius=R):
        eps=[F(0)]*8 if halfwidths is None else list(map(F,halfwidths));center=list(map(F,center))
        if len(center)!=8 or len(eps)!=8 or min(eps)<0:raise ValueError('Eight coordinates and nonnegative halfwidths required.')
        a=k.matvec(self.inverse,[center[i]-self.center[i] for i in k.N8])
        used=[abs(a[i])+sum(abs(self.inverse[i][j])*eps[j] for j in k.N8) for i in k.N8]
        return dict(contained=all(used[i]<=radius[i] for i in k.N8),used=used,slack=[radius[i]-used[i] for i in k.N8])
    def check(self):
        M,MI,c=self.M,self.inverse,self.center;N=k.N8
        J=k.jacobian(c,F(3,25));JM=[[sum(J[i][z]*M[z][j] for z in N) for j in N] for i in N]
        A=[[sum(MI[i][z]*JM[z][j] for z in N) for j in N] for i in N];b=k.matvec(MI,k.field(c,F(3,25)))
        widths=[sum(abs(v) for v in row) for row in M];d=widths
        products=[d[0]*d[1],d[0]*d[4],(2*d[1]+d[3])*d[2],(2*d[1]+d[3])*d[3],d[4]*d[7]]
        den=k.D_-c[0];rem=45*F(573,10)*d[0]**2/(den**2*(den-d[0]))
        n=[sum(k.TV[j][i]*products[j] for j in range(5))+abs(MI[i][0])*rem for i in N]
        data=k.cert0
        assert A==[[F(v) for v in row] for row in data['linear']]
        assert b==[F(row[0]) for row in data['residual']]
        assert n==[F(row[0]) for row in data['nonlinear_bound']]
        phys=[f-sum(abs(g)*w for g,w in zip(grad,widths)) for f,grad in zip(k.faces(c),k.FACE_GRAD)];assert min(phys)>0
        velocity=[F(0),-F(67,2)]+[F(0)]*6;E=[130*F(1,10**6)*abs(MI[i][0]) for i in N];rows={}
        for label,q in [('R',R),('S',S)]:
            budget=[A[i][i]*q[i]+sum(abs(A[i][j])*q[j] for j in N if j!=i)+abs(b[i])+n[i] for i in N]
            assert all(budget[i]+E[i]<velocity[i] for i in N)
            w=[sum(abs(M[j][i])*q[i] for i in N) for j in N]
            HG=F(21,100)*(50-c[2]-c[3]-w[2]-w[3]);HT=F(21,10)*(F(505,1000)-c[4]-w[4])*(c[7]-w[7])
            assert HG>F(207,20) and HT>(F(391,100) if label=='R' else F(401,100))
            rows[label]=dict(face_budgets=budget,source_perturbation=E,face_velocity=velocity,service_lower=(HG,HT),projection_halfwidths=w)
        wrange=2*sum(k.ELLM[i]*S[i] for i in N);assert wrange<F(1,10)
        ptest=self.membership(self.preparation,[F(1,2000000)]*8);assert ptest['contained']
        relative=self.membership(self.preparation,[F(1,1000)*v for v in self.preparation]);assert not relative['contained']
        slack=[R[i]-(F(5,6) if i==1 else F(0)) for i in N]
        uniform=min(slack[i]/sum(abs(v) for v in MI[i]) for i in N)
        return dict(regions=rows,physical_unit_box_margins=phys,storage_range_S=wrange,deadline=F(1,250),shortfall_bound=F(9,25000),
            narrow_preparation=ptest,independent_point_one_percent_box=relative,largest_uniform_halfwidth_around_p=uniform,
            scope='Fresh rational field/Jacobian/remainder and face checks. Affine moving-box and continuation theorems supply existence, capture and indefinite service for maintained supply. No attraction or contraction is asserted; Lean is not rerun.')


class TubeCertificate:
    def __init__(self,name):
        if name not in ['tube_nominal','tube_Q120','tube_Q60']:raise ValueError('Unknown fixed witness.')
        self.name=name;self.data=json.loads((Path(__file__).parent/(name+'.json')).read_text())
    def validate_structure(self):
        d=self.data;ts=list(map(F,d['times']));n=len(ts)
        assert F(d['horizon'])==k.HOR and F(d['tau'])==k.TAU and F(d['kappa'])==k.KAPPA and F(d['donor_tolerance'])==k.QC0
        assert len(d['reference'])==len(d['radii'])==len(d['donor_reference'])==len(d['donor_radii'])==n
        assert all(len(row)==8 for row in d['reference']+d['radii'])
        assert all(F(v)>0 for row in d['radii'] for v in row) and all(F(v)>0 for v in d['donor_radii'])
        assert d['V']=={'tube_nominal':'inf','tube_Q120':'1000','tube_Q60':'500'}[self.name]
        if d['V']!='inf':assert all(F(3,25)-(F(c)+F(r))/F(d['V'])>0 for c,r in zip(d['donor_reference'],d['donor_radii']))
        return True
    def verify(self):
        self.validate_structure();result=k.verify(self.name,quiet=True,certificate=self.data)
        if self.name=='tube_Q60':assert result['mission_failure_at_H'] and F(result['exact']['HT_upper_at_H'])<F(39132,10000)
        else:
            assert result['mission_success'];assert F(result['exact']['min_LT_after_tau'])>=F(4034,1000)
            assert F(result['exact']['shortfall'])<=F(11,100000)
        result['scope']='Exact replay of every moving-face inequality, including center drift and physical margins. Preparation/donor sets are fixed. Shortfall reported here is BEFORE tau; for Q60 later failure adds further shortfall. Numerical references are proposals, not evidence.'
        return result
    def slices(self):
        rows=[];d=self.data
        for t,u,q,C,qC in zip(d['times'],d['reference'],d['radii'],d['donor_reference'],d['donor_radii']):
            u=list(map(F,u));q=list(map(F,q));w=[sum(abs(k.M[j][i])*q[i] for i in k.N8) for j in k.N8]
            lower=F(21,10)*(F(505,1000)-u[4]-w[4])*(u[7]-w[7]);upper=F(21,10)*(F(505,1000)-u[4]+w[4])*(u[7]+w[7])
            inv=F(0) if d['V']=='inf' else 1/F(d['V']);slo=F(3,25)-(F(C)+F(qC))*inv;shi=F(3,25)-(F(C)-F(qC))*inv
            rows.append((float(F(t)),float(lower),float(upper),float(slo),float(shi)))
        return rows


def fixed_band_stock(horizon,stock=None,affinity=None):
    H=F(horizon);D=16*H;s0=F(3,25);delta=F(1,10**6)
    if H<F(1,250):raise ValueError('Mission must extend to the recovery deadline.')
    linear=s0*D/delta
    result=dict(horizon=H,consumption_upper=D,linear_sufficient_initial_stock=linear,linear_conversion=D/delta)
    if stock is not None and affinity is not None:
        Q,K=F(stock),F(affinity)
        if K<=0 or Q<=D:raise ValueError('Positive affinity and stock above the conservative consumption budget required.')
        fall=s0*K*D/(Q*(K+Q-D));result.update(saturating_stock=Q,affinity=K,source_fall_upper=fall,saturating_passes=fall<=delta)
    return result