#!/usr/bin/env python3
"""Offline constraint on the GCP .77 memcpy fault in the log-gate attempt.

Checks signed ARM instructions and the two literal planned copy spans. This
EXCLUDES an intact planned copy from the observed conditional store, but does
NOT reconstruct the actual caller/registers or authorize a hardware retry.
"""
from __future__ import annotations

import ast
import argparse
import struct
from pathlib import Path

from capstone import Cs, CS_ARCH_ARM, CS_MODE_ARM, CS_MODE_THUMB

ELF = Path(__file__).resolve().parents[1] / 'psp_out/versions_win/elf_all/gcp_22.0.0.77_7c426e7f.elf'
FRAME_PC, FRAME_FAR = 0x4011D8, 0x42CFA0


def executable_offset(data: bytes, va: int) -> int:
    assert data[:6] == b'\x7fELF\x01\x01'
    phoff = struct.unpack_from('<I', data, 28)[0]
    entsize, count = struct.unpack_from('<HH', data, 42)
    for i in range(count):
        typ, off, base, _, size, _, flags, _ = struct.unpack_from('<8I', data, phoff+entsize*i)
        if typ == 1 and flags & 1 and base <= va < base+size:
            return off+va-base
    raise ValueError(hex(va))


def literals(path: Path) -> dict[str, int]:
    # AST only: NEVER import/execute the host/card probe.
    body = ast.parse(path.read_text()).body
    out: dict[str, int] = {}
    def value(node: ast.expr) -> int:
        if isinstance(node, ast.Constant) and type(node.value) is int:
            return node.value
        if isinstance(node, ast.Name):
            return out[node.id]
        if isinstance(node, ast.BinOp) and isinstance(node.op, ast.Add):
            return value(node.left)+value(node.right)
        if isinstance(node, ast.BinOp) and isinstance(node.op, ast.Sub):
            return value(node.left)-value(node.right)
        raise ValueError(f'unsupported literal expression: {ast.dump(node)}')
    wanted = {'PARAMS','STACK_DST','SRC_OFF','MLEN','DUMPDST','DUMPLEN','DUMP_OFF','MSGA_OFF','SLOT'}
    for node in body:
        if isinstance(node, ast.Assign) and len(node.targets)==1:
            target=node.targets[0]
            if isinstance(target, ast.Name) and target.id in wanted:
                out[target.id] = value(node.value)
    assert wanted <= out.keys(), wanted-out.keys()
    # Bind the claimed two offsets to the actual top-level qcs invocation,
    # not merely to constants with similar names elsewhere in the script.
    qcs_def=next(n for n in body if isinstance(n,ast.FunctionDef) and n.name=='qcs')
    calls=[n for n in ast.walk(ast.Module(body=body,type_ignores=[]))
           if isinstance(n,ast.Call) and isinstance(n.func,ast.Name) and n.func.id=='qcs']
    assert len(calls)==1
    args=calls[0].args
    assert len(args)==3
    for pos,expected in ((1,out['SLOT']-0x1c),(2,out['SLOT']-4)):
        expr=args[pos]
        assert isinstance(expr,ast.Call) and isinstance(expr.func,ast.Name) and expr.func.id=='disp'
        assert value(expr.args[0])==expected
    writes={}
    for n in ast.walk(qcs_def):
        if isinstance(n,ast.Call) and isinstance(n.func,ast.Attribute) and n.func.attr=='pack_into':
            if len(n.args)>3 and isinstance(n.args[2],ast.Constant):
                writes[n.args[2].value]=n.args[3]
    assert 'dA' in ast.unparse(writes[0x840]) and 'dB' in ast.unparse(writes[0x838])
    assert value(writes[0x81c])==0x40  # eight-byte selector-4 copies
    return out


def main() -> None:
    ap=argparse.ArgumentParser(description=__doc__)
    ap.add_argument('--probe',type=Path,default=Path('/tmp/gcp_rop_sysdrv_loggates_readonly.py'))
    v=literals(ap.parse_args().probe)
    image=ELF.read_bytes()
    md=Cs(CS_ARCH_ARM, CS_MODE_ARM)
    for ea,mnem in ((0x40111C,'cmp'),(0x401154,'beq'),(0x4011A8,'subs'),
                    (0x4011C8,'lsls'),(FRAME_PC,'stmmi')):
        off=executable_offset(image,ea)
        ins=next(md.disasm(image[off:off+4],ea,count=1))
        assert ins.address==ea and ins.mnemonic==mnem,(hex(ea),ins.mnemonic)
    planned=((v['STACK_DST'],v['PARAMS']+v['SRC_OFF'],v['MLEN']),
             (v['DUMPDST'],v['STACK_DST']+v['DUMP_OFF'],v['DUMPLEN']))
    for dest,src,length in planned:
        assert dest%16==src%16==length%16==0,(hex(dest),hex(src),hex(length))
        assert not (dest <= FRAME_FAR < dest+length)
        print(f'planned copy dst=0x{dest:x} src=0x{src:x} len=0x{length:x}: '
              'aligned/16-multiple; cannot execute STMMI tail with intact arguments')
    # FE0A selector 4 performs TWO 8-byte copies to a host-displaced R0.
    # The first's nominal destination, unlike the two ROP copies above,
    # differs from FAR by exactly a page-aligned 0x11000. At this length,
    # ARM 0x40111C can enter 0x4011A4 and execute the STMMI tail.
    thumb=Cs(CS_ARCH_ARM,CS_MODE_THUMB)
    for ea,mnem in ((0x404D44,'add.w'),(0x404D4E,'blx'),
                    (0x404D52,'add.w'),(0x404D5C,'blx')):
        off=executable_offset(image,ea)
        ins=next(thumb.disasm(image[off:off+4],ea,count=1))
        assert ins.address==ea and ins.mnemonic==mnem,(hex(ea),ins.mnemonic)
    first=v['SLOT']-0x1C
    second=v['SLOT']-4
    delta=(FRAME_FAR-first)&0xffffffff
    assert delta==0x11000 and (FRAME_FAR-second)&0xfff != 0
    inferred_base=(v['PARAMS']+delta)&0xffffffff
    print(f'selector-4 first 8-byte chosen-write nominal dst=0x{first:x}; '
          f'FAR=0x{FRAME_FAR:x} implies params VA=0x{inferred_base:x} '
          f'(old assumed 0x{v["PARAMS"]:x} + 0x{delta:x}).')
    print('Second chosen-write would need a non-page-aligned base shift; '
          'first is a strong MATCH, not measured R0/R6 or proof of caller.')
    print('The actual command-buffer VA must be verified independently; '
          'NO hardware retry authorized by this offline inference.')


if __name__=='__main__':
    main()