#!/usr/bin/env python3
"""Independent mathematical model checks; does not execute the Vir backend."""
from collections import Counter, defaultdict
from fractions import Fraction
from itertools import product
from pathlib import Path
import hashlib, json

def changed(bits,mask): return bits ^ mask
def inverse(bits): return int(f'{bits:06b}'[::-1],2)
def nuclear(bits): return ((bits>>1)&7) | (((bits>>2)&7)<<3)
def summarize(lines):
    b=sum((v%2)<<i for i,v in enumerate(lines))
    m=sum((v in (6,9))<<i for i,v in enumerate(lines))
    return {'bits':b,'moving_mask':m,'changed_bits':changed(b,m),'nuclear_bits':nuclear(b),'opposite_bits':b^63,'inverse_bits':inverse(b)}
def question_mask(q):
    return (int.from_bytes(hashlib.sha256(q.encode('utf-8')).digest()[:8],'big') & ((1<<63)-1)) if q else 0
def interval(n,phase):
    return {(49,1):(12,35),(44,2):(12,31),(40,2):(10,29),(40,3):(10,29),(36,3):(10,25),(32,3):(8,23)}[(n,phase)]
def bian(n,left):
    rem=lambda x:1+(x-1)%4
    removed=1+rem(left)+rem(n-left-1)
    return {'removed':removed,'remain':n-removed}

def main():
    root=Path(__file__).parent
    vectors=json.loads((root/'test-vectors.json').read_text())
    for v in vectors['cases']:
        kind=v['kind']; args=v['input']
        got = summarize(args['lines']) if kind=='hexagram' else question_mask(args['question']) if kind=='hash' else bian(args['stalks'],args['left'])
        assert got==v['expected'], (v['id'],got,v['expected'])
    arch=0
    for b in range(64):
        assert (b^63)^63==b
        assert inverse(inverse(b))==b
        assert 0<=nuclear(b)<64
        for m in range(64):
            assert changed(changed(b,m),m)==b
            arch+=1
    coins=Counter(sum(p) for p in product((2,3),repeat=3))
    assert [Fraction(coins[x],8) for x in (6,7,8,9)]==[Fraction(1,8),Fraction(3,8),Fraction(3,8),Fraction(1,8)]
    states={49:Fraction(1)}
    split_checks=0
    for phase in (1,2,3):
        nxt=defaultdict(Fraction)
        for n,p in states.items():
            lo,hi=interval(n,phase)
            for left in range(lo,hi+1):
                out=bian(n,left)
                assert out['removed'] in ((5,9) if phase==1 else (4,8))
                assert out['remain']%4==0
                nxt[out['remain']]+=p/Fraction(hi-lo+1)
                split_checks+=1
        states=nxt
    expected={6:Fraction(1,16),7:Fraction(5,16),8:Fraction(7,16),9:Fraction(3,16)}
    assert {n//4:p for n,p in states.items()}==expected
    for mask in range(256):assert len({x^mask for x in range(256)})==256
    for span in range(2,65):
        limit=(255//span)*span
        counts=Counter(x%span for x in range(limit))
        assert len(set(counts.values()))==1 and len(counts)==span
    report={'verification_scope':'Independent Python model, not the native binary or production HTTP API',
     'synthetic_vectors_passed':len(vectors['cases']), 'changed_pairs_checked':arch,'hexagram_states_checked':64,
     'coin_combinations_checked':8,'yarrow_state_splits_checked':split_checks,
     'yarrow_probability':{str(k):str(v) for k,v in expected.items()},
     'coin_probability':{str(k):str(Fraction(coins[k],8)) for k in (6,7,8,9)},
     'xor_masks_8bit_checked':256,'rejection_spans_8bit_checked':63,
     'native_test':{'status':'compile_failed','compiler':'virc 2026.2.20','test':'tests/test_cast_csprng.vri','errors':['E2001','E3007'],'native_pass_claimed':False},
     'production_fault_injection':'not run for this publication'}
    print(json.dumps(report,indent=2))
    return report

if __name__=='__main__':main()