#!/usr/bin/env python3
"""arp03-encoder-crosscheck v1.2 -- 11 Aug 2026, Tiago Pinto (donttrustverify.pt)

Addresses the declared coverage gap "Encoder independence" of the ARP-03
existence-oracle run record. The reference's deterministic CBOR encoder is
checked two ways: (a) against an independently developed library encoder
(cbor2), and (b) against a property verifier written from RFC 8949
Section 4.2.1, scoped to the properties applicable to the ARP encoding
subset (unsigned and negative integers, byte and text strings, arrays,
maps, null and booleans): shortest-form heads, map keys in bytewise
lexicographic order of their encoded form, and full consumption of the
encoding. Floats and indefinite-length items are outside the reference
encoder's domain and are not checked.

Corpus: the structures the existence-oracle class exercises (COSE protected
header, Sig_structure shape, response payload shape) plus adversarial cases:
integer head boundaries (23/24, 255/256, 65535/65536, 2^32-1/2^32), negative
integers, UTF-8 multibyte strings, empty containers, nested maps, mixed-type
map keys, and the divergent key pair {100, -1}, where bytewise ordering of
encoded keys (0x1864 < 0x20, RFC 8949 Section 4.2.1) and length-first
ordering (RFC 8949 Section 4.2.3 variant) disagree.

Semantic round-trip is asserted for every corpus item (cbor2.loads of the
reference bytes equals the original value). The divergence set against
cbor2 is closed: any divergence outside the declared pair, or the declared
pair failing to diverge, exits non-zero. Checks do not rely on assert and
survive python -O.

Usage: place next to conformance/reference/arp_read_ref.py and run with
python3; requires cbor2 (tested with 6.1.4). Exit 0 = all checks pass and
the divergence set matches the declaration exactly.
"""
import re, sys, hashlib, importlib.metadata

def die(msg):
    print("FAIL:", msg)
    sys.exit(1)

def check(cond, msg):
    if not cond:
        die(msg)

SRC = "arp_read_ref.py"
src_bytes = open(SRC, "rb").read()
source_sha256 = hashlib.sha256(src_bytes).hexdigest()
m = re.search(r"(def _head.*?)(?=\n# -----)", src_bytes.decode("utf-8"), re.S)
check(m is not None, "could not extract cbor()/_head() from " + SRC)
ns = {}
exec(m.group(1), ns)
ref_cbor = ns["cbor"]

import cbor2

exercised = [
    {1: -8},
    ["Signature1", b"\xa1\x01\x27", b"", b"payload"],
    {"status": 200, "result": None, "as_of": 12345, "request_binding": b"\x00"*32},
    {4: b"kid-1"},
]
adversarial = [
    0, 23, 24, 255, 256, 65535, 65536, 4294967295, 4294967296,
    -1, -24, -25, -256, -257,
    "", "a", "c\u00e3o", "\u00e9\u4e2d",
    b"", b"\x00", [], {}, [[]], [{}],
    {"b": 1, "aa": 2},
    {100: 0, -1: 1},
    {10: 0, "2": 1, b"x": 2},
    {"outer": {100: 0, -1: 1}, "z": [{-25: True, 24: False}]},
]
corpus = exercised + adversarial

def parse_head(buf, pos):
    ib = buf[pos]; mt, ai = ib >> 5, ib & 0x1f; pos += 1
    if ai < 24: return mt, ai, pos, 1
    n = {24:1, 25:2, 26:4, 27:8}[ai]
    return mt, int.from_bytes(buf[pos:pos+n], "big"), pos + n, 1 + n

def shortest_ok(arg, hl):
    if arg < 24: return hl == 1
    for n, h in ((1,2),(2,3),(4,5),(8,9)):
        if arg < (1 << (8*n)): return hl == h
    return False

def skip(buf, pos, i):
    mt, val, pos, hl = parse_head(buf, pos)
    check(mt == 7 or shortest_ok(val, hl), f"non-shortest head in corpus[{i}]")
    if mt in (0,1,7): return pos
    if mt in (2,3): return pos + val
    if mt == 4:
        for _ in range(val): pos = skip(buf, pos, i)
        return pos
    if mt == 5:
        for _ in range(2*val): pos = skip(buf, pos, i)
        return pos
    if mt == 6: return skip(buf, pos, i)
    die(f"unexpected major type {mt} in corpus[{i}]")

def maps_bytewise(buf, i, pos=0):
    mt, val, p2, hl = parse_head(buf, pos)
    if mt == 5:
        keys, p = [], p2
        for _ in range(val):
            k0 = p; p = skip(buf, p, i); keys.append(buf[k0:p])
            v0 = p; p = skip(buf, p, i); maps_bytewise(buf, i, v0)
        check(keys == sorted(keys),
              f"map keys not bytewise-lex of encoded form in corpus[{i}]")
        return p
    if mt == 4:
        p = p2
        for _ in range(val):
            maps_bytewise(buf, i, p); p = skip(buf, p, i)
        return p
    return skip(buf, pos, i)

EXPECTED_DIVERGENT = [
    {100: 0, -1: 1},
    {"outer": {100: 0, -1: 1}, "z": [{-25: True, 24: False}]},
]

eq = 0; diffs = []; roundtrip_ok = 0; consumed_ok = 0
for i, v in enumerate(corpus):
    a = ref_cbor(v)
    b = cbor2.dumps(v, canonical=True)
    if a == b: eq += 1
    else: diffs.append((i, v, a.hex(), b.hex()))
    check(cbor2.loads(a) == v, f"semantic round-trip failed for corpus[{i}]: {v!r}")
    roundtrip_ok += 1
    end = maps_bytewise(a, i)
    check(end == len(a),
          f"trailing or unparsed bytes in corpus[{i}]: consumed {end}/{len(a)}")
    consumed_ok += 1

unexpected = [d for d in diffs if d[1] not in EXPECTED_DIVERGENT]
missing = [e for e in EXPECTED_DIVERGENT if e not in [d[1] for d in diffs]]

print(f"reference source sha256: {source_sha256}")
print(f"corpus: {len(corpus)} items")
print(f"semantic round-trip (cbor2.loads(ref_bytes) == value): {roundtrip_ok}/{len(corpus)} PASS")
print(f"full consumption (parser end == encoding length): {consumed_ok}/{len(corpus)} PASS")
print(f"cbor2 {importlib.metadata.version('cbor2')} canonical vs reference encoder: {eq}/{len(corpus)} byte-identical")
for i, v, a, b in diffs:
    print(f"  divergent corpus[{i}] = {v!r}\n    reference: {a}\n    cbor2    : {b}")
print(f"RFC 8949 4.2.1 properties, ARP subset (verifier independent of both encoders): {len(corpus)}/{len(corpus)} PASS on reference encoder")
divergent_pair = cbor2.dumps({100: 0, -1: 1}, canonical=True)
# demonstrative: extract the two encoded keys and test 4.2.1 ordering directly
_, n, p, _ = parse_head(divergent_pair, 0)
k1s = p; k1e = skip(divergent_pair, k1s, -1); v1e = skip(divergent_pair, k1e, -1)
k2s = v1e; k2e = skip(divergent_pair, k2s, -1)
k1, k2 = divergent_pair[k1s:k1e], divergent_pair[k2s:k2e]
if [k1, k2] == sorted([k1, k2]):
    print("cbor2 on divergent pair: also satisfies 4.2.1 bytewise ordering")
else:
    print("cbor2 on divergent pair {100,-1}: length-first ordering, the RFC 8949 Section 4.2.3")
    print("variant, not the Section 4.2.1 Core Deterministic ordering ARP-03 pins.")
if unexpected:
    die(f"unexpected divergences: {[(i, v) for i, v, _, _ in unexpected]}")
if missing:
    die(f"expected divergent case did not diverge: {missing}")
print("divergence set matches the declared expectation exactly; exit 0")