#!/usr/bin/env python3
"""Verify native plane tables and bounded plane/root-leaf instruction paths."""
import gzip
import itertools
import json
from pathlib import Path
import re
import struct
from analyze_area_queries import run
from analyze_chat_crosshair import bits
from analyze_collision_composition import put_word
from analyze_engine_control import control_flow
from analyze_frame_timing import read_address
from analyze_native import elf
from analyze_qvm import write_json
from analyze_vm_extensions import native_functions,verified


def main():
    out={'native':{},'limitations':'Finite synthetic instruction evaluation, not original process execution. '
         'Indirect plane dispatch is explicitly resumed from verified file-backed table entries. '
         'Root traversal begins after the prologue; callback effects are omitted and execution stops '
         'before tail unwind. Only one node with negative children is composed. Complete recursive '
         'geometry, loading, float environment, ABI/lifetime and original-runtime/platform behavior remain open.'}
    for label in ['linux--Quake3-UrT-Ded.x86_64','linux--Quake3-UrT.x86_64']:
        r=json.loads(Path(f'docs/research/native/{label}.json').read_text());data=verified((Path('.cache/UrbanTerror43')/r['source']['path']).read_bytes(),r['source']['sha256'])
        a=r['artifacts']['disassembly.txt'];fs=native_functions(verified(gzip.open(a['path'],'rb').read(),a['uncompressed_sha256']).decode());metadata,_=elf(data)
        g=control_flow(fs['BoxOnPlaneSide']);rows=g['instructions'];jump=next(x for x in rows if x['opcode']=='jmpq')
        table_address=int(re.search(r'\*0x([0-9a-f]+)',jump['operands'])[1],16)
        targets=list(struct.unpack('<8Q',read_address(data,metadata['sections'],table_address,64)[0]))
        if len(set(targets))!=8 or any(t not in {x['address'] for x in rows} for t in targets):raise ValueError('plane table escaped graph')
        returns=[x['address'] for x in rows if x['opcode']=='retq'];probes=[]
        lo=[-2.,-3.,-4.];hi=[5.,6.,7.];minimum,maximum,plane=0x10000,0x20000,0x30000
        cases=[]
        for axis in range(3):
            for distance in [lo[axis]-1,lo[axis],0.,hi[axis],hi[axis]+1]:cases.append((axis,0,[0.,0.,0.],distance))
        for sign in range(8):
            normal=[(-1. if sign&(1<<i) else 1.)*(i+1) for i in range(3)]
            low=sum(normal[i]*(hi[i] if normal[i]<0 else lo[i]) for i in range(3));high=sum(normal[i]*(lo[i] if normal[i]<0 else hi[i]) for i in range(3))
            for distance in [low-1,low,0.,high,high+1]:cases.append((3,sign,normal,distance))
        for sign,distance in itertools.product([8,255],[-1.,0.,1.]):cases.append((3,sign,[1.,2.,3.],distance))
        # General axis-shaped normal demonstrates the axial/general max-face distinction.
        cases.append((3,0,[1.,0.,0.],hi[0]))
        for plane_type,sign,normal,distance in cases:
            m={}
            for i in range(3):
                put_word(m,minimum+4*i,bits(lo[i]));put_word(m,maximum+4*i,bits(hi[i]));put_word(m,plane+4*i,bits(normal[i]))
            put_word(m,plane+12,bits(distance));put_word(m,plane+16,plane_type,1);put_word(m,plane+17,sign,1)
            t=run(g,g['entry'],returns+[jump['address']],m,{'%rdi':minimum,'%rsi':maximum,'%rdx':plane});trace=t['trace'];dispatch=None
            if t['stop']==jump['address']:
                dispatch=targets[t['registers']['r8']];t=run(g,dispatch,returns,t['memory'],t['registers']);trace+=t['trace']
            probes.append({'type':plane_type,'signbits':sign,'normal':normal,'minimum':lo,'maximum':hi,'distance':distance,'result':t['registers']['rax'],'dispatch':dispatch,'trace':trace})
        tree=control_flow(fs['CM_BoxLeafnums_r']);tr=tree['instructions'];start=next(x['address'] for x in tr if x['opcode']=='testl' and x['operands']=='%esi, %esi')
        terminal=next(x['address'] for x in tr if x['opcode']=='movq' and x['operands']=='0x38(%r15), %r11')
        plane_calls=[i for i,x in enumerate(tr) if '<BoxOnPlaneSide>' in x['operands']]
        callbacks=[i for i,x in enumerate(tr) if x['opcode']=='callq' and x['operands']=='*0x38(%r15)']
        slot_ins=next(x for x in tr if x['opcode']=='movq' and '(%rip)' in x['operands']);slot=int(re.search(r'#\s*0x([0-9a-f]+)',slot_ins['operands'])[1],16)
        query,stack,nodes=0x40000,0x50000,0x60000;entry_probes=[];root_probes=[]
        for index in [-3,-1,0,1,2]:
            m={};put_word(m,slot,nodes,8)
            for i in range(3):put_word(m,nodes+16*i,plane+32*i,8)
            t=run(tree,start,[terminal,tr[plane_calls[0]]['address']],m,{'%rsi':index,'%r12':query+24,'%r13':query+36,'%rsp':stack,'%r15':query})
            entry_probes.append({'index':index,'terminal':t['stop']==terminal,'plane_pointer':t['registers'].get('rdx'),'minimum_pointer':t['registers'].get('rdi'),'maximum_pointer':t['registers']['rsi'],'trace':t['trace']})
        for result in [0,1,2,3]:
            m={};put_word(m,stack+8,nodes,8);put_word(m,nodes+8,-6);put_word(m,nodes+12,-10)
            regs={'%rax':result,'%rsp':stack,'%r15':query};pc=tr[plane_calls[0]+1]['address'];visits=[];trace=[]
            while pc!=terminal:
                if len(visits)>=2:raise ValueError('root traversal escaped single-node bound')
                t=run(tree,pc,[terminal]+[tr[i]['address'] for i in callbacks],m,regs);m=t['memory'];regs=t['registers'];trace+=t['trace'];pc=t['stop']
                visits.append((~regs['rsi'])&0xffffffff)
                if pc!=terminal:
                    j=next(i for i in callbacks if tr[i]['address']==pc);pc=tr[j+1]['address']
            root_probes.append({'plane_result':result,'leaf_visits':visits,'trace':trace})
        out['native'][label]={'source':r['source'],'disassembly_sha256':a['uncompressed_sha256'],'graphs':{'BoxOnPlaneSide':g,'CM_BoxLeafnums_r':tree},'table_address':table_address,'table_targets':targets,'plane_probes':probes,'node_base_slot':slot,'entry_probes':entry_probes,'root_probes':root_probes,'plane_call_sites':[tr[i]['address'] for i in plane_calls],'callback_sites':[tr[i]['address'] for i in callbacks]}
    write_json(Path('docs/research/bsp-planes.json'),out)
    print('Recovered 124 plane classifications, 10 node-entry and 8 single-node traversal probes')


if __name__=='__main__':main()