"""Independent packed-payload witness, not S-FTL's implementation format.

Symbols are LSB-first; PPNs are little-endian. N, bit width and PPN width
are external parameters. No header, allocation or lookup index is counted.
"""
from fractions import Fraction
from hashlib import sha256
import json
from pathlib import Path
import sys


def dimensions(n, bits, width):
    if (type(n) is not int or n < 1 or type(bits) is not int
            or bits not in (1, 2) or type(width) is not int or width < 1):
        raise ValueError("invalid dimensions")
    return (n * bits + 7) // 8


def unpack(data, n, bits, width=4):
    bitmap_size = dimensions(n, bits, width)
    if type(data) is not bytes or len(data) < bitmap_size:
        raise ValueError("missing bitmap")
    bitmap = int.from_bytes(data[:bitmap_size], "little")
    if bitmap >> (n * bits):
        raise ValueError("nonzero padding")
    symbols = [(bitmap >> (i * bits)) & ((1 << bits) - 1) for i in range(n)]
    starts = [i for i, s in enumerate(symbols) if s & (1 << (bits - 1))]
    if len(data) != bitmap_size + len(starts) * width:
        raise ValueError("wrong payload length")
    heads = {pos: int.from_bytes(data[bitmap_size + k * width:
                                      bitmap_size + (k + 1) * width], "little")
             for k, pos in enumerate(starts)}
    values = []
    for i, symbol in enumerate(symbols):
        label = symbol & 1 if bits == 2 else 0
        # Backward search is intentionally separate from model.py's anchors.
        for j in range(i, -1, -1):
            other = symbols[j] & 1 if bits == 2 else 0
            if label == 1 and other != 1:
                raise ValueError("local continuation crossed a base position")
            if j in heads and other == label:
                value = heads[j] + i - j
                break
        else:
            raise ValueError("continuation without head")
        if value >= 256 ** width:
            raise ValueError("reconstructed PPN overflow")
        values.append(value)
    if len(set(values)) != n:
        raise ValueError("duplicate live PPN")
    return values


def pack(encoded, width=4):
    symbols, heads, bits = encoded["symbols"], encoded["heads"], encoded["bits_per_entry"]
    size = dimensions(len(symbols), bits, width)
    if any(type(s) is not int or not 0 <= s < (1 << bits) for s in symbols):
        raise ValueError("invalid symbol")
    expected = [i for i, s in enumerate(symbols) if s & (1 << (bits - 1))]
    if any(not isinstance(h, list) or len(h) != 2
           or type(h[0]) is not int or type(h[1]) is not int
           or not 0 <= h[1] < 256 ** width for h in heads):
        raise ValueError("invalid head")
    if [h[0] for h in heads] != expected:
        raise ValueError("head order does not match bitmap")
    bitmap = sum(s << (i * bits) for i, s in enumerate(symbols))
    data = bitmap.to_bytes(size, "little") + b"".join(
        value.to_bytes(width, "little") for _, value in heads)
    unpack(data, len(symbols), bits, width)
    return data


def history_certificate():
    histories = []
    for costs in ((1636, 1728), (1844, 1728)):
        form, steps = "flat", []
        for cost in costs:
            ratio = Fraction(cost, 2048)
            if form == "flat" and ratio < Fraction(4, 5):
                form = "bitmap"
            elif form == "bitmap" and ratio > Fraction(9, 10):
                form = "flat"
            steps.append({"candidate_bitmap_bytes": cost, "form": form,
                          "selected_payload_bytes": cost if form == "bitmap" else 2048})
        histories.append({"initial_form": "flat", "steps": steps})
    return {"evidence_class": "conditional-size-state-history-not-device-update-trace",
            "flat_bytes": 2048, "final_bitmap_bytes": 1728,
            "final_ratio_exact": "27/32", "payload_difference_bytes": 320,
            "histories": histories}


def certificate():
    root = Path(__file__).parent
    original = (root / "results.json").read_bytes()
    rows = []
    for case in json.loads(original)["cases"]:
        forms = {}
        for name in ("one_bit", "two_bit"):
            data = pack(case[name])
            recovered = unpack(data, len(case["mapping_ppn"]), case[name]["bits_per_entry"])
            if recovered != case["mapping_ppn"]:
                raise RuntimeError("packed round trip differs from frozen input")
            if len(data) != case[name + "_payload_bytes"]:
                raise RuntimeError("actual byte length differs from frozen count")
            forms[name] = {"hex": data.hex(), "bytes": len(data),
                           "sha256": sha256(data).hexdigest()}
        rows.append({"id": case["id"], "forms": forms})
    return {"schema_version": 1,
            "evidence_class": "synthetic-packed-payload-cross-check",
            "format": "Hesela witness only; LSB-first bitmap, little-endian PPNs",
            "external_parameters": ["mapping count", "bitmap width", "PPN width"],
            "excluded": ["format header", "directory", "allocator", "alignment",
                         "lookup index", "replacement state", "dirty buffering", "timing"],
            "size_state_history": history_certificate(),
            "frozen_results_sha256": sha256(original).hexdigest(),
            "packed_code_sha256": sha256(Path(__file__).read_bytes()).hexdigest(),
            "cases": rows}


if __name__ == "__main__":
    result = certificate()
    path = Path(__file__).with_name("packed-results.json")
    if sys.argv[1:] == ["--write"]:
        path.write_text(json.dumps(result, indent=2) + "\n")
    elif sys.argv[1:] == ["--check"]:
        if json.loads(path.read_text()) != result:
            raise SystemExit("packed-results.json is stale")
        print("All 16 packed forms match the eight frozen maps and byte counts")
    else:
        raise SystemExit("usage: packed.py --write|--check")