#!/usr/bin/env python3
"""
Sequencing predicates of draft-hawkins-scitt-attested-agent-payment-01
(Section 6 and Check 9 of Section 4), exercised against scenarios.

Text under test:
  draft-hawkins-scitt-attested-agent-payment-01.txt
  sha256 9e6deb7c735a5f776809e3e1431c7e67e1ecc664ab2c0a94895d51778f4080a7

Predicates implemented FROM THE TEXT, with line references, nothing added:

  P-SUB   l.770-773  "sub" = scope digest of the initial scope in the sequence;
                     constant across reissuance, narrowing, revocation.
  P-PAIR  l.773-775  superseding/revoking statement MUST carry the same
                     (iss, sub); different pair supersedes nothing.
  P-SEQ   l.775-777  precedence by explicit monotonic sequence number, never
                     by registration order.
  P-IND   l.573-575  Check 9: an indeterminate result -- the executor cannot
                     determine whether a superseding statement exists -- is
                     fail-closed by default: MUST NOT settle.
  P-EXPL  l.576-579  two explicit routes to indeterminate: null/empty answer;
                     unsigned or position-less answer WHERE THE SERVICE
                     ADVERTISES supersession queries.
  P-DET   l.789-792  determinate "no superseding statement" = signed,
                     position-carrying answer showing the scope's own
                     statement as the highest sequence number for the pair.
  P-ADV   Sec. 6     services that do not advertise the query are out of
                     scope by construction.
  P-AGG   l.540, l.704, l.709
                     aggregate evaluated against the enumeration "for this
                     scope"; executor keeps the enumeration "per scope";
                     execution digest includes the scope digest.
  P-PP    l.304, l.410
                     per-payment bound; every settlement must satisfy it.
  P-INT   l.526      an executor MUST NOT settle the same payment intent
                     identifier more than once under a scope.
  P-HOLD  l.383      if superseded/reissued during a hold, the prior hold
                     confers nothing.
  P-REIS  l.742      issuers SHOULD prefer reissuance to long lifetimes.

Scope digest: this harness uses SHA-256 over the deterministically encoded
CBOR bytes (RFC 8949 s4.2.1) that the text prescribes. The text mandates
the bytes but names NO hash function for the scope digest; the choice of
SHA-256 here is the harness's own, and that gap is itself reported, with
its divergence demonstrated, in check_wire (W1). Scopes are structurally
conformant to the published CDDL ("apk": bstr, etc.).

The harness models the aggregate-accounting predicate of Check 6 and the
per-payment bound, not the full nine-check procedure; outcome lines say
which predicate passed. Where the text does not decide, the row says so;
nothing is guessed.
"""
import hashlib, cbor2

def scope_digest(scope: dict) -> bytes:
    return hashlib.sha256(cbor2.dumps(scope, canonical=True)).digest()

APK = b"\x00" * 32
CODE = {"alg": "sha-256", "artifact": "tdx-mrtd", "digest": b"\x11" * 32}

def scope(aggregate, window, expiry, executor="exec.example", per_payment=10_000):
    s = {"apk": APK, "code": CODE,
         "limits": {"currency": "USDC", "scale": 6, "per_payment": per_payment},
         "expiry": expiry}
    if aggregate is not None:
        s["limits"]["aggregate"] = aggregate; s["limits"]["window"] = window
    if executor is not None:
        s["executor"] = executor
    return s

class TS:
    def __init__(self, advertises=True, signs=True, positions=True):
        self.log, self.advertises, self.signs, self.positions = [], advertises, signs, positions
    def register(self, iss, sub, seqno, sd, kind):
        self.log.append(dict(iss=iss, sub=sub, seqno=seqno, sd=sd, kind=kind, pos=len(self.log)))
    def query(self, iss, sub):
        if not self.advertises:
            return None
        rows = [r for r in self.log if r["iss"] == iss and r["sub"] == sub]
        return dict(signed=self.signs, position=len(self.log) if self.positions else None, rows=rows)

def check9(ts, iss, sub, own_seqno):
    a = ts.query(iss, sub)
    if a is None:
        # P-ADV: the text says non-advertising services are out of scope by
        # construction; P-DET cannot be met without a signed, position-carrying
        # answer; the executor cannot determine supersession status; P-IND applies.
        return "INDETERMINATE (by Check 9 definition; service does not advertise supersession queries)"
    if not a["signed"] or a["position"] is None:
        return "INDETERMINATE (unsigned or position-less answer; explicit route, l.577-579)"
    if not a["rows"]:
        return "INDETERMINATE (empty answer; explicit route, l.576-577)"
    highest = max(r["seqno"] for r in a["rows"])       # P-SEQ
    if highest > own_seqno:  return "STOP (superseding statement present)"
    if highest == own_seqno: return "DETERMINATE-PASS"
    return "TEXT-SILENT (own seqno above highest registered)"

class Executor:
    """P-AGG: enumeration keyed per scope digest (or, in S10, per (iss,sub))."""
    def __init__(self): self.enum = {}
    def settle(self, key, amount, intent):
        self.enum.setdefault(key, []).append((intent, amount))
    def spent(self, key): return sum(a for _, a in self.enum.get(key, []))
    def seen(self, key, intent): return any(i == intent for i, _ in self.enum.get(key, []))

rows = []
def R(name, outcome, cls, note=""): rows.append((name, outcome, cls, note))

iss = "issuer.example"

# ---- S1 basic
ts = TS(); s0 = scope(50_000, 86_400, 1_000); sd0 = scope_digest(s0); sub = sd0
ts.register(iss, sub, 1, sd0, "scope")
R("S1 single statement, advertising TS", check9(ts, iss, sub, 1), "CLEAN")

# ---- S2 reissuance (same sub, new digest)
s1 = scope(50_000, 86_400, 2_000); sd1 = scope_digest(s1)
assert sd1 != sd0, "this reissuance changes expiry, hence the digest"
ts.register(iss, sub, 2, sd1, "reissue")
R("S2 reissue: seq-1 holder", check9(ts, iss, sub, 1), "CLEAN")
R("S2 reissue: seq-2 holder", check9(ts, iss, sub, 2), "CLEAN")

# ---- S3 revocation same pair
ts.register(iss, sub, 3, None, "revoke")
R("S3 revoke under same (iss,sub)", check9(ts, iss, sub, 2), "CLEAN")

# ---- S4 revoke under different pair
t4 = TS(); t4.register(iss, sub, 1, sd0, "scope"); t4.register(iss, b"other-sub", 2, None, "revoke")
R("S4 revoke under DIFFERENT sub", check9(t4, iss, sub, 1), "CLEAN",
  "ignored per P-PAIR (l.774-775); the cost falls on the issuer, by design")

# ---- S5 registration order inverted
t5 = TS(); t5.register(iss, sub, 2, sd1, "reissue"); t5.register(iss, sub, 1, sd0, "scope")
R("S5 log order inverted vs seqno, seq-1 holder", check9(t5, iss, sub, 1), "CLEAN",
  "P-SEQ holds: seqno wins over log position (l.775-777)")

# ---- S6/S7 the A-2 routes
t6 = TS(signs=False); t6.register(iss, sub, 1, sd0, "scope")
R("S6 TS advertises, answers unsigned", check9(t6, iss, sub, 1), "CLEAN (A-2)",
  "explicit route to indeterminate, l.577-579")
t7 = TS(advertises=False); t7.register(iss, sub, 1, sd0, "scope")
R("S7 TS does NOT advertise supersession queries", check9(t7, iss, sub, 1), "CLEAN (A-2); EDITORIAL",
  "The outcome is obtained compositionally: Section 6 says that services that do not advertise "
  "the query are out of scope by construction, while Check 9 defines inability to determine "
  "supersession status as indeterminate. There is no explicit normative branch stating that a "
  "non-advertising service yields an indeterminate result. Editorial candidate: 'If the "
  "Transparency Service does not advertise supersession queries, the executor MUST treat the "
  "supersession status as indeterminate.'")

# ---- S8 (as first written): NON-CONFORMANT INPUT, kept as negative test only
t8 = TS(); t8.register(iss, sd0, 1, sd0, "scope"); t8.register(iss, b"seqB", 1, sd0, "scope")
t8.register(iss, b"seqB", 2, None, "revoke")
R("S8 NEG same digest under sub='seqB' (violates P-SUB l.770-772)", check9(t8, iss, sd0, 1),
  "NEGATIVE TEST", "input is non-conformant: a new authorization's sub MUST equal the initial "
  "scope digest. Not evidence against A-1. Kept as a registration-validation negative case.")

# ---- S8' conformant construction: same scope bytes in two sequences
t8b = TS()
t8b.register(iss, sd0, 1, sd0, "scope")      # A: initial
t8b.register(iss, sd0, 2, sd1, "reissue")    # A: reissue carrying s1
t8b.register(iss, sd1, 1, sd1, "scope")      # B: s1 as initial of its own sequence
t8b.register(iss, sd0, 3, None, "revoke")    # A revoked
R("S8' same scope bytes as A:reissue AND B:initial; A revoked; executor holds B's statement",
  check9(t8b, iss, sd1, 1), "OBSERVATION (I-1)",
  "both registrations conform to P-SUB/P-PAIR; nothing binds scope bytes to a single "
  "sequence. Executed here: revocation of sequence A is invisible to a holder of B's "
  "statement, because the query is keyed by the pair carried on the statement handed to "
  "the executor. Not executed: the accounting consequence; the enumeration is keyed by "
  "scope digest (P-AGG), so whether the two authorizations share one aggregate allowance "
  "is unstated. Converse scope-vs-sequence accounting-identity case of the reissuance "
  "finding; not an A-1 finding.")

# ---- S9 I-1: aggregate accounting across reissuance
# 24 hourly reissues registered in the SAME sequence (sub constant, seqno rising,
# per P-SUB and P-REIS). Under each scope the executor makes five payments of
# 10000, each satisfying the per-payment bound (P-PP) and each passing the
# aggregate predicate of Check 6 against THAT scope's enumeration (P-AGG).
t9 = TS(); ex = Executor(); total = 0; sub9 = None
for h in range(24):
    s = scope(50_000, 86_400, 3_600 * (h + 1)); sd = scope_digest(s)
    if sub9 is None:
        sub9 = sd; t9.register(iss, sub9, 1, sd, "scope")
    else:
        t9.register(iss, sub9, h + 1, sd, "reissue")
    for k in range(5):
        amount = 10_000
        assert amount <= 10_000                       # P-PP
        assert ex.spent(sd) + amount <= 50_000        # aggregate predicate, this scope
        ex.settle(sd, amount, f"intent-{h}-{k}")      # distinct intent ids (P-INT)
        total += amount
R("S9 aggregate 50000/24h; 24 hourly reissues in ONE sequence; five 10000 payments per scope",
  f"settled {total} in 24h; per-payment bound and aggregate predicate of Check 6 pass "
  f"for every settlement", "FINDING (I-1)",
  "P-AGG keys the enumeration by scope digest (l.540, l.704, l.709); when reissuance changes "
  "any scope member, including a refreshed expiry, the scope digest changes while sub remains "
  "constant (l.770-773); the aggregate allowance restarts per reissue, and Sec. 6 recommends "
  "reissuance (l.742). This is the adversarial ceiling (the executor spends the full room "
  "under each scope), not the typical case; every settlement is individually conformant.")

# ---- S10 candidate repair, NOT in text
ex2 = Executor(); total2 = 0
for h in range(24):
    for k in range(5):
        amount = 10_000
        if ex2.spent(sub9) + amount > 50_000: continue
        ex2.settle(sub9, amount, f"intent-{h}-{k}"); total2 += amount
R("S10 same as S9, enumeration keyed by (iss,sub) [candidate repair, NOT in text]",
  f"settled {total2} in 24h", "CANDIDATE",
  "narrowing mid-sequence (e.g. 50000 -> 10000) still needs a rule for which limit governs "
  "the already-accumulated history; the text does not say.")

# ---- S11 hold across reissuance
R("S11 hold opened under seq-1, reissue to seq-2 during hold",
  "prior hold confers nothing; fresh evaluation under seq-2", "CLEAN", "explicit, l.383")

# ---- S12 cross-executor replay under a per-payment-only scope (conditional on V1)
sp = scope(None, None, 5_000, executor=None)   # per-payment only -> executor MAY be omitted (l.323-324)
sdp = scope_digest(sp)
exA, exB = Executor(), Executor()
def try_settle(ex_, intent):
    if ex_.seen(sdp, intent): return "refused (P-INT)"
    ex_.settle(sdp, 1_000, intent); return "settled"
r1 = try_settle(exA, "intent-X"); r2 = try_settle(exA, "intent-X"); r3 = try_settle(exB, "intent-X")
R("S12 per-payment-only scope, no executor; same signed intent to executor A twice, then to B",
  f"A: {r1}, {r2}; B: {r3}", "CONDITIONAL FINDING",
  "P-INT (l.526) binds one executor. Without an executor member nothing binds the instruction "
  "to one executor, so two executors each settle once, both conformant. Exists only if "
  "per-payment-only scopes are permitted (V1 in check_cddl); resolves with V1.")

w = max(len(r[0]) for r in rows)
print(f"{'scenario':<{w}}  outcome / class")
print("-" * (w + 60))
for n, o, c, note in rows:
    print(f"{n:<{w}}  {o}")
    print(f"{'':<{w}}  class: {c}")
    if note: print(f"{'':<{w}}  note: {note}")