#!/usr/bin/env python3
# -----------------------------------------------------------------------------
# pq_message_enforcement_smt.py
#
# MACHINE-CHECKED (z3) proof of the ENFORCEMENT RULES for the four post-quantum
# sealed QBFT message layers of chain 2800 (SPEC.md section 2.6), written on
# 2026-09-02, the day the fleet moved to the build that fixed D-311.
#
# WHAT IS MODELLED (design combinatorics, not the Java code and not the chain):
#   - four message TYPES with four DOMAINS (PROPOSAL, PREPARE, ROUND-CHANGE, COMMIT);
#   - a seal = (index, domain, height, round, digest, form) where `form` distinguishes
#     the COMMIT anchor form (signed when the anchor is armed at that height) from the
#     committed-seal digest form;
#   - a registry active at a height binding index -> author;
#   - the per-type enforcement height H_type (absent = never);
#   - the verifier's decision "the vote counts" as a function of the message, its
#     author, the seal it carries, the registry and the height.
#
# PROPERTIES (UNSAT of the negation = holds):
#   P1  ARMED-REQUIRES-VALID: at h >= H_type, a message counts only if it carries a
#       seal bound to its author, accepted by the registry, and verifying over the
#       pre-image of ITS OWN type at ITS OWN (height, round, digest).
#   P2  NO-CROSS-DOMAIN-REPLAY: a seal valid for type X never makes a message of type
#       Y != X count (domains differ, so pre-images differ).
#   P3  NO-CROSS-POSITION-REPLAY: a seal over (h, r, d) never makes a message at a
#       different (h', r', d') count.
#   P4  NO-AUTHOR-SWAP: a seal of index i counts only on a message whose author is
#       the address the registry binds to i.
#   P5  BELOW-FORK-UNCHANGED: at h < H_type an unsealed message still counts (the
#       upstream rule alone decides).
#   P6  COMMIT-FORM-AGREEMENT (D-311): with the anchor armed, an emitter signing the
#       anchor form and a verifier checking the anchor form agree (commits count);
#       the NEGATIVE CONTROL plants the pre-2026-09-02 verifier (digest form) and
#       shows that EVERY honest commit is refused, i.e. the liveness failure the
#       testnet observed at block 999.
#
# NEGATIVE CONTROLS: every property has one; each plants the violation and must
# come back SAT, proving the check can fire. Convention as in the other *_smt.py.
#
# HONEST BOUNDARY: Falcon verification is modelled as equality of the signed
# pre-image tuple (a perfect signature); registry rotation is modelled as a
# height-indexed binding; nothing here says anything about the Java code paths
# beyond the rules SPEC.md 2.6 states, nor about chain 2800's live enforcement
# state (none is armed at the time of writing).
# -----------------------------------------------------------------------------
from z3 import (Int, Bool, BoolVal, Solver, And, Or, Not, Implies, If, sat, unsat)

PROPOSAL, PREPARE, ROUNDCHANGE, COMMIT = 0, 1, 2, 3
DIGEST_FORM, ANCHOR_FORM = 0, 1
N = 9                      # validators / registry indices 0..8
ANCHOR_BLOCK = 13014000    # aere.pq.anchorBlock on 2800
results = []

def bound_author(index, height):
    """registry active at `height` binds index i to author i (modelled identity); indices outside
    0..N-1 are refused. Rotation is modelled by the height guard: below the registry start nothing
    is bound (the model uses one registry; the anchor model covers rotation)."""
    return If(And(index >= 0, index < N), index, -1)

def anchor_armed(height):
    return height + 1 >= ANCHOR_BLOCK

def expected_form(mtype, height):
    """the message form a COMMIT seal must sign at this height (SPEC 2.6, D8); other types
    always sign their own domain pre-image (modelled as DIGEST_FORM of their own domain)."""
    return If(And(mtype == COMMIT, anchor_armed(height)), ANCHOR_FORM, DIGEST_FORM)

def counts(mtype, height, round_, digest, author, has_seal, s_index, s_domain, s_h, s_r, s_d, s_form,
           H_type, verifier_form=None):
    """the vote-counting predicate of SPEC 2.6. `verifier_form` overrides the form the verifier
    expects for COMMIT (used by the D-311 negative control); None = the fixed verifier."""
    armed = height >= H_type
    exp_form = expected_form(mtype, height) if verifier_form is None else verifier_form
    seal_ok = And(has_seal,
                  bound_author(s_index, height) == author,        # rule 2 + 3
                  s_domain == mtype,                                # rule 4: own domain
                  s_h == height, s_r == round_, s_d == digest,      # rule 4: own position
                  s_form == exp_form)                               # rule 4: commit form
    return Or(Not(armed), seal_ok)

def fresh(prefix):
    return (Int(prefix + '_type'), Int(prefix + '_h'), Int(prefix + '_r'), Int(prefix + '_d'),
            Int(prefix + '_author'), Bool(prefix + '_has'), Int(prefix + '_si'), Int(prefix + '_sdom'),
            Int(prefix + '_sh'), Int(prefix + '_sr'), Int(prefix + '_sd'), Int(prefix + '_sform'))

def domain_bounds(t, sdom):
    return And(t >= 0, t <= 3, sdom >= 0, sdom <= 3)

def check(name, negation_constraints, negative_control_constraints):
    s = Solver(); s.add(*negation_constraints); r = s.check()
    holds = (r == unsat)
    s2 = Solver(); s2.add(*negative_control_constraints); r2 = s2.check()
    fires = (r2 == sat)
    results.append((name, holds, fires))
    print(f"{name:28s} property={'HOLDS' if holds else 'FAILS'} ({r})   negative-control={'FIRES' if fires else 'DOES NOT FIRE'} ({r2})")
    return holds and fires

# ---------------------------------------------------------------- P1 armed requires valid
t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p1'); H = Int('p1_H')
base = [domain_bounds(t, sdom), h >= H, a >= 0, a < N]
# negation: armed, and the message counts, yet the seal is absent or not the author's or wrong position
bad_seal = Or(Not(has), bound_author(si, h) != a, sdom != t, sh != h, sr != r, sd != d, sform != expected_form(t, h))
neg = base + [counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H), bad_seal]
# negative control: a planted rule that accepts an unsealed message while armed
planted = base + [Not(has), Or(Not(h >= H), True)]  # "counts" replaced by True: the planted rule ignores the seal
check('P1 armed-requires-valid', neg, planted)

# ---------------------------------------------------------------- P2 no cross-domain replay
t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p2'); H = Int('p2_H')
neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, sdom != t,
       counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)]
# planted: a domain-blind verifier (drops the sdom == t conjunct)
blind = And(has, bound_author(si, h) == a, sh == h, sr == r, sd == d, sform == expected_form(t, h))
planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, sdom != t, blind]
check('P2 no-cross-domain-replay', neg, planted)

# ---------------------------------------------------------------- P3 no cross-position replay
t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p3'); H = Int('p3_H')
neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, Or(sh != h, sr != r, sd != d),
       counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)]
blind = And(has, bound_author(si, h) == a, sdom == t, sform == expected_form(t, h))  # position-blind
planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, Or(sh != h, sr != r, sd != d), blind]
check('P3 no-cross-position-replay', neg, planted)

# ---------------------------------------------------------------- P4 no author swap
t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p4'); H = Int('p4_H')
neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, bound_author(si, h) != a,
       counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)]
blind = And(has, sdom == t, sh == h, sr == r, sd == d, sform == expected_form(t, h))  # author-blind
planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, bound_author(si, h) != a, blind]
check('P4 no-author-swap', neg, planted)

# ---------------------------------------------------------------- P5 below fork unchanged
t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p5'); H = Int('p5_H')
neg = [domain_bounds(t, sdom), h < H, Not(has), a >= 0, a < N,
       Not(counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H))]
# planted: an enforcement that ignores its own height (always armed)
planted = [domain_bounds(t, sdom), h < H, Not(has), a >= 0, a < N, Not(Or(Not(BoolVal(True)), has))]
check('P5 below-fork-unchanged', neg, planted)

# ---------------------------------------------------------------- P6 commit form agreement (D-311)
h = Int('p6_h'); r = Int('p6_r'); d = Int('p6_d'); a = Int('p6_a'); si = Int('p6_si'); H = Int('p6_H')
honest = [h >= H, h + 1 >= ANCHOR_BLOCK, a >= 0, a < N, si == a]  # honest emitter: seal of its own index
emitted_form = ANCHOR_FORM  # what QbftRound.pqSealMessageFor signs when the anchor is armed
# negation: an honest commit under the FIXED verifier does not count
neg = honest + [Not(counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H))]
# negative control: the pre-D-311 verifier (digest form) refuses the same honest commit
planted = honest + [Not(counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H, verifier_form=DIGEST_FORM))]
check('P6 commit-form-agreement', neg, planted)

# ---------------------------------------------------------------- P6b every honest commit refused under the old verifier
# strengthening of the negative control: under the old verifier there is NO honest commit that counts
s = Solver()
s.add(honest[0], honest[1], honest[2], honest[3], honest[4],
      counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H, verifier_form=DIGEST_FORM))
r_all = s.check()
all_refused = (r_all == unsat)
results.append(('P6b old-verifier-refuses-all', all_refused, all_refused))
print(f"{'P6b old-verifier-refuses-all':28s} {'HOLDS' if all_refused else 'FAILS'}: under the digest-form verifier with the anchor armed, no honest commit counts ({r_all}) - the block-999 stop of testnet 28001")

ok = all(hold and fire for _, hold, fire in results)
print(f"\n{'ALL PROPERTIES HOLD AND ALL NEGATIVE CONTROLS FIRE' if ok else 'SOMETHING DID NOT HOLD OR A CONTROL DID NOT FIRE'}: {sum(1 for _,hh,ff in results if hh and ff)}/{len(results)}")
raise SystemExit(0 if ok else 1)