#!/usr/bin/env python3
"""Independent shifted-boundary ablation and branch-exposure audit."""
import hashlib
import json
import struct
from pathlib import Path

root = Path("/home/alex/sots-re")
out = root / "verify/results/research-completion-abi-independent/run-d94d4516b9d898793318805e"
data = (root / "dumps/sots.exe").read_bytes()
pe = struct.unpack_from("<I", data, 0x3c)[0]
assert data[pe:pe + 4] == b"PE\0\0"
nsec = struct.unpack_from("<H", data, pe + 6)[0]
opt_size = struct.unpack_from("<H", data, pe + 20)[0]
opt = pe + 24
assert struct.unpack_from("<H", data, opt)[0] == 0x10b
base = struct.unpack_from("<I", data, opt + 28)[0]
table = opt + opt_size
sections = []
for i in range(nsec):
    pos = table + 40 * i
    name = data[pos:pos + 8].rstrip(b"\0").decode("ascii")
    vsize, va, raw_size, raw = struct.unpack_from("<IIII", data, pos + 8)
    sections.append((name, va, max(vsize, raw_size), raw, raw_size))

def read_va(address, size):
    rva = address - base
    for name, va, span, raw, raw_size in sections:
        if va <= rva and rva + size <= va + span:
            delta = rva - va
            assert delta + size <= raw_size
            return data[raw + delta:raw + delta + size]
    raise AssertionError(hex(address))

targets = {
    "observed-alloc": (0x57E5E3, "c20400"),
    "player-append": (0x86C62D, "c20400"),
    "player-copy": (0x7694BF, "c20400"),
    "observed-push": (0x7B739E, "c20400"),
    "observed-realloc": (0x7B35EE, "c20400"),
    "string-alloc": (0x424AD9, "c20800"),
    "dedup": (0x825E64, "c20800"),
}
ablations = []
for name, (address, expected_hex) in targets.items():
    expected = bytes.fromhex(expected_hex)
    exact = read_va(address, len(expected))
    minus = read_va(address - 1, len(expected))
    plus = read_va(address + 1, len(expected))
    record = {
        "name": name, "address": hex(address), "expected": expected_hex,
        "exact": exact.hex(), "minus_one": minus.hex(), "plus_one": plus.hex(),
        "exact_pass": exact == expected,
        "shifted_negative_control_pass": minus != expected and plus != expected,
    }
    assert record["exact_pass"] and record["shifted_negative_control_pass"]
    ablations.append(record)

def text(name):
    return (out / (name + ".stdout.txt")).read_text()

exposures = {
    "observed_stride_0x2c": "imul   ecx,ecx,0x2c" in text("observed-alloc-wide"),
    "observed_deep_copy_call": "call   0x79a150" in text("observed-push-wide"),
    "player_stride_0x74": "add    DWORD PTR [edi+0x4],0x74" in text("player-append-wide"),
    "player_deep_copy_call": "call   0x7693f0" in text("player-append-wide"),
    "player_three_delete_calls": text("player-dtor-control").count("call   0x924faa") == 3,
    "description_inequality_call": "call   0x46f8c0" in text("dedup-wide"),
    "dedup_stride_0x74": "add    DWORD PTR [ebp+0x8],0x74" in text("dedup-wide"),
    "three_float_unordered_or_unequal_rejections":
        text("dedup-wide").count("fucompp") == 3
        and text("dedup-wide").count("test   ah,0x44") == 3
        and text("dedup-wide").count("jp     0x825e25") == 3,
}
assert all(exposures.values())
state = json.loads((out / "independent-state.json").read_text())
actual_state = {
    "evnxid_has_4": 4 in state["evnxid_values"],
    "turn3_bucket_has_2": 2 in state["turn3_bucket_counts"],
    "event3_position_defaults": state["event3"]["position_words"] == [2139095039] * 3,
    "whole_state_rebuild": state["coverage"] == {
        "ok": True, "rebuiltBytes": 609080, "inflatedBytes": 609080, "firstDiff": None},
    "rng_leaf": state["rng"]["valueBytes"] == 2503
        and state["rng"]["digest"] == "0978fdf34ff7962f76c2de810dc93e0a",
}
assert all(actual_state.values())
result = {
    "schema": "sots-abi-heldout/1",
    "session": "run-d94d4516b9d898793318805e",
    "binary_sha256": hashlib.sha256(data).hexdigest(),
    "challenge": "direct PE exact versus minus-one/plus-one shifted return encodings",
    "ablations": ablations,
    "branch_exposures": exposures,
    "actual_state_checks": actual_state,
    "pass": True,
}
(out / "heldout-boundary.json").write_text(json.dumps(result, indent=2) + "\n")