#!/usr/bin/env python3
# -----------------------------------------------------------------------------
# anchor_blocking_quorum_smt.py
#
# MACHINE-CHECKED (z3) proof of BLOCKING-QUORUM SAFETY for the AERE post-quantum
# anchor once the blocking fork is active (height >= 14,050,000).
#
#   INVARIANT (the task target):
#     With the blocking fork active, no ANCHOR block can be finalized with fewer
#     than K=3 valid Falcon seals from DISTINCT signers of the registry ACTIVE
#     at that height; and a NON-anchor block requires no seals at all.
#
# Finalization is modelled as a function of (a) the multiset of HEARD seals and
# (b) the height SCHEDULE. Chain facts taken as LAW (chain 2800):
#   N=9 validators, QBFT quorum ceil(2N/3) = 6
#   anchor every 32 blocks starting at height 13,014,000
#   min-seals schedule on heights: 13014000:0, 13034000:3  (so K=3 at the fork)
#   producer write cap maxSeals = 5
#   emergency minSealsCeiling can only LOWER the effective K, never raise it
#   blocking fork from 14,050,000: no block finalizes without the Falcon quorum
#   registry rotation on heights: 13014000 -> 7 keys, 13600000 -> 9 keys,
#   every height covered by EXACTLY one registry
#
# Convention (same as computemarket_smt.py / falcon_blocking_smt.py): every
# property is a function that builds constraints; UNSAT of the negation means
# the property HOLDS; and every proof is paired with a NEGATIVE CONTROL that
# plants the violation and must come back SAT, proving the check can fire.
# The mandated negative control here: a planted rule that PERMITS 2 seals must
# make "finalized with only 2 distinct seals" SAT, while the original rule is
# UNSAT on the same scenario.
#
# HONEST BOUNDARY: this checks the DESIGN combinatorics of the finalization
# predicate (seal counting, distinctness, registry eligibility, schedule,
# ceiling, write cap), not the Besu Java code and not the live chain. The
# height 14,050,000 fork is modelled as given by the operator decision of
# 2026-08-15; registry key sets are modelled as index sets (7-key set is a
# prefix of the 9-key set; a 10th index stands for a key in NO registry).
# -----------------------------------------------------------------------------
from z3 import (Int, Bool, BoolVal, Solver, And, Or, Not, Implies, If, Sum,
                sat, unsat)

# ---- chain facts (LAW) ------------------------------------------------------
FORK_BLOCKING   = 14050000      # blocking fork height
ANCHOR_START    = 13014000      # first anchor height
ANCHOR_INTERVAL = 32            # anchor every 32nd block
SCHED_K3_FROM   = 13034000      # min-seals schedule: 13014000:0, 13034000:3
K_TARGET        = 3             # the K in force at and after the blocking fork
MAX_SEALS       = 5             # producer write cap
QBFT_N, QBFT_Q  = 9, 6          # validator count, QBFT commit quorum ceil(2N/3)
REG1_START, REG1_KEYS = 13014000, 7    # first registry: 7 Falcon keys
REG2_START, REG2_KEYS = 13600000, 9    # second registry: 9 Falcon keys
NKEYS = 10                      # key slots 0..8 = registry keys; slot 9 = a key
                                # that is in NO registry (foreign / rotated-out)

results = []
def check(name, s, expect_unsat=True, kind="PROOF"):
    r = s.check()
    if expect_unsat:
        ok = (r == unsat); tag = "PROVED" if ok else "FAILED"
    else:
        ok = (r == sat);   tag = "CEX-FOUND" if ok else "FAILED"
    results.append((name, tag, ok, kind))
    print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})")
    if r == sat:
        m = s.model(); wit = {}
        for d in m.decls():
            try: wit[str(d)] = m[d].as_long()
            except Exception:
                try: wit[str(d)] = bool(m[d])
                except Exception: wit[str(d)] = "?"
        print("             witness:", {k: wit[k] for k in sorted(wit)})
    return ok

# ---- the finalization predicate, as a function of heard seals + schedule ----
def is_anchor(h):
    """Anchor heights: every 32nd block from 13,014,000."""
    return And(h >= ANCHOR_START, (h - ANCHOR_START) % ANCHOR_INTERVAL == 0)

def sched_K(h):
    """The min-seals schedule on heights: 13014000:0, 13034000:3."""
    return If(h >= SCHED_K3_FROM, K_TARGET, 0)

def eligible(i, h):
    """Is key index i in the registry ACTIVE at height h?  Exactly one registry
       covers each height: [13014000,13600000) -> 7 keys, [13600000,oo) -> 9.
       Index 9 is in NO registry, ever."""
    return If(h >= REG2_START, BoolVal(i < REG2_KEYS),
              And(h >= REG1_START, BoolVal(i < REG1_KEYS)))

class Block:
    """Symbolic state of one block: height, the multiset of heard seals
       (per-key multiplicity + validity), the emergency ceiling, and the
       QBFT commit count."""
    def __init__(self):
        self.h        = Int('h')
        self.heard    = [Int(f'heard_{i}') for i in range(NKEYS)]   # seals heard from key i
        self.valid    = [Bool(f'valid_{i}') for i in range(NKEYS)]  # key i's seal verifies
        self.ceil_set = Bool('ceil_set')                            # emergency ceiling engaged?
        self.ceil_val = Int('ceil_val')                             # its value (>= 0)
        self.qbft     = Int('qbft_commits')                         # ECDSA commit seals

    def wf(self):
        return [self.h >= ANCHOR_START] \
             + [self.heard[i] >= 0 for i in range(NKEYS)] \
             + [self.qbft >= 0, self.qbft <= QBFT_N, self.ceil_val >= 0]

    def distinct_eligible_valid(self):
        """The rule the code enforces: count DISTINCT signers (multiplicity
           collapses to 1) whose seal VERIFIES and who are in the ACTIVE
           registry at this height."""
        return Sum([If(And(self.heard[i] >= 1, self.valid[i], eligible(i, self.h)), 1, 0)
                    for i in range(NKEYS)])

    def K_eff(self):
        """Effective K: the schedule value, LOWERED (never raised) by the
           emergency ceiling when engaged."""
        K = sched_K(self.h)
        return If(self.ceil_set, If(self.ceil_val <= K, self.ceil_val, K), K)

    def finalized(self):
        """Post-fork blocking finalization: QBFT commit quorum ALWAYS, plus the
           Falcon quorum ON ANCHOR HEIGHTS ONLY. Non-anchor blocks carry no
           Falcon requirement at all."""
        falcon_ok = If(is_anchor(self.h), self.distinct_eligible_valid() >= self.K_eff(),
                       BoolVal(True))
        return And(self.qbft >= QBFT_Q, falcon_ok)

    def finalized_planted_K2(self):
        """PLANTED VIOLATION for the mandated negative control: same rule but
           the anchor threshold guard is weakened to permit 2 seals."""
        falcon_ok = If(is_anchor(self.h), self.distinct_eligible_valid() >= 2,
                       BoolVal(True))
        return And(self.qbft >= QBFT_Q, falcon_ok)

    def finalized_multiplicity_bug(self):
        """PLANTED VIOLATION: counts seal MESSAGES instead of distinct signers
           (a replayed seal counts every time)."""
        multi = Sum([If(And(self.valid[i], eligible(i, self.h)), self.heard[i], 0)
                     for i in range(NKEYS)])
        falcon_ok = If(is_anchor(self.h), multi >= self.K_eff(), BoolVal(True))
        return And(self.qbft >= QBFT_Q, falcon_ok)

    def finalized_no_registry_check(self):
        """PLANTED VIOLATION: counts ANY valid seal, ignoring the active
           registry (a foreign key's seal counts)."""
        anykey = Sum([If(And(self.heard[i] >= 1, self.valid[i]), 1, 0)
                      for i in range(NKEYS)])
        falcon_ok = If(is_anchor(self.h), anykey >= self.K_eff(), BoolVal(True))
        return And(self.qbft >= QBFT_Q, falcon_ok)

print("### AERE anchor BLOCKING-QUORUM SAFETY -- fork at 14,050,000, K=3, N=9, q=6\n")
print(f"    anchor grid: every {ANCHOR_INTERVAL} blocks from {ANCHOR_START}; "
      f"fork {FORK_BLOCKING} is {'ON' if (FORK_BLOCKING-ANCHOR_START)%ANCHOR_INTERVAL==0 else 'OFF'} the grid "
      f"((14050000-13014000)/32 = {(FORK_BLOCKING-ANCHOR_START)//ANCHOR_INTERVAL})\n")

# =============================================================================
# S0 CONFIG -- sanity of the constants the invariant leans on.
# =============================================================================
s = Solver()
s.add(Int('r') == (FORK_BLOCKING - ANCHOR_START) % ANCHOR_INTERVAL, Int('r') != 0)
check("S0a CONFIG: the blocking-fork height 14,050,000 lies ON the anchor grid "
      "(it is itself an anchor height)", s)

s = Solver()
h = Int('h')
s.add(h >= FORK_BLOCKING, sched_K(h) != K_TARGET)
check("S0b SCHEDULE (all h >= fork): the min-seals schedule pins K == 3 at every "
      "blocking-era height (13034000:3 step is below the fork)", s)

s = Solver()
h = Int('h')
r1 = And(h >= REG1_START, h < REG2_START)
r2 = (h >= REG2_START)
s.add(h >= ANCHOR_START, Not(Or(And(r1, Not(r2)), And(r2, Not(r1)))))
check("S0c REGISTRY PARTITION (all h): every height from 13,014,000 on is covered "
      "by EXACTLY one registry (7-key window then 9-key window, no gap, no overlap)", s)

s = Solver()
h = Int('h')
s.add(h >= FORK_BLOCKING, Not(h >= REG2_START))
check("S0d REGISTRY AT FORK (all h >= fork): the active registry in the blocking "
      "era is the 9-key registry (fork 14,050,000 > rotation 13,600,000)", s)

# =============================================================================
# S1 -- THE INVARIANT (positive result). An anchor block at h >= fork, with the
# emergency ceiling NOT engaged, can NEVER be finalized with <= 2 distinct
# valid registry-eligible Falcon seals. UNSAT = the property HOLDS.
# =============================================================================
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(b.finalized())
s.add(b.distinct_eligible_valid() <= 2)
check("S1 BLOCKING-QUORUM SAFETY: post-fork ANCHOR block finalized with <= 2 "
      "distinct valid eligible Falcon seals is IMPOSSIBLE (K=3 floor holds)", s)

# same, with the ceiling engaged but at/above K: still no hole below 3
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), b.ceil_set, b.ceil_val >= K_TARGET)
s.add(b.finalized())
s.add(b.distinct_eligible_valid() <= 2)
check("S1b CEILING AT/ABOVE K: with minSealsCeiling engaged at >= 3 the K=3 floor "
      "still holds (a ceiling >= K opens no hole)", s)

# =============================================================================
# S2 -- MANDATED NEGATIVE CONTROL: permit 2 seals and demand finalization.
# The planted rule (threshold guard weakened to 2) MUST be SAT on exactly the
# scenario S1 just proved impossible: the violation IS expressible, so S1's
# UNSAT is earned, not vacuous.
# =============================================================================
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(b.finalized_planted_K2())
s.add(b.distinct_eligible_valid() == 2)
check("S2 NEG-CTRL (mandated): PLANT a rule that permits 2 seals -> a post-fork "
      "anchor block finalizes with exactly 2 distinct valid seals (violation is "
      "expressible; the K>=3 guard in S1 is load-bearing)", s,
      expect_unsat=False, kind="NEG-CTRL")

# =============================================================================
# S3 -- NON-ANCHOR blocks require NO seals (both directions).
# =============================================================================
# (a) zero heard seals can never block a non-anchor block: UNSAT of "QBFT quorum
#     met, zero seals, NOT finalized".
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, Not(is_anchor(b.h)), b.qbft >= QBFT_Q)
s.add(*[b.heard[i] == 0 for i in range(NKEYS)])
s.add(Not(b.finalized()))
check("S3a NON-ANCHOR NEEDS NO SEALS (all h >= fork): a non-anchor block with the "
      "QBFT quorum and ZERO heard seals is ALWAYS finalized (seals never required)", s)

# (b) non-vacuity witness: such a block exists (SAT with a concrete height).
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, Not(is_anchor(b.h)), b.qbft >= QBFT_Q)
s.add(*[b.heard[i] == 0 for i in range(NKEYS)])
s.add(b.finalized())
check("S3b CONFIG witness: a concrete post-fork non-anchor height finalizes with "
      "zero seals (the S3a implication is not vacuous)", s,
      expect_unsat=False, kind="CONFIG")

# =============================================================================
# S4 -- DISTINCTNESS is load-bearing: replayed seals collapse to one signer.
# =============================================================================
# (a) correct rule: 3+ seal MESSAGES from <= 2 distinct signers do NOT finalize.
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(Sum([b.heard[i] for i in range(NKEYS)]) >= 3)      # >= 3 raw seal messages
s.add(b.distinct_eligible_valid() <= 2)                  # but <= 2 distinct signers
s.add(b.finalized())
check("S4a DISTINCT SIGNERS: >= 3 heard seal MESSAGES from <= 2 distinct eligible "
      "signers can never finalize a post-fork anchor block (replay collapses)", s)

# (b) NEG-CTRL: a rule counting messages (multiplicity) accepts ONE signer
#     replayed three times.
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(b.distinct_eligible_valid() <= 1)                  # a single distinct signer
s.add(b.finalized_multiplicity_bug())
check("S4b NEG-CTRL: PLANT multiplicity counting -> one signer replayed 3x "
      "finalizes the anchor block (distinctness is load-bearing)", s,
      expect_unsat=False, kind="NEG-CTRL")

# =============================================================================
# S5 -- REGISTRY ELIGIBILITY is load-bearing: a key outside the ACTIVE registry
# can never be the third seal.
# =============================================================================
# (a) correct rule: 2 eligible + 1 foreign (index 9, in NO registry) do NOT
#     finalize, even though 3 distinct VALID seals were heard.
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(b.heard[9] >= 1, b.valid[9])                       # a valid FOREIGN seal heard
s.add(b.distinct_eligible_valid() == 2)                  # only 2 eligible signers
s.add(b.finalized())
check("S5a REGISTRY ELIGIBILITY: 2 eligible + 1 valid seal from a key in NO "
      "registry can never finalize a post-fork anchor block", s)

# (b) NEG-CTRL: a rule that skips the registry check accepts the foreign key as
#     the third seal.
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set))
s.add(b.heard[9] >= 1, b.valid[9])
s.add(b.distinct_eligible_valid() == 2)
s.add(b.finalized_no_registry_check())
check("S5b NEG-CTRL: PLANT a rule without the registry check -> the foreign key "
      "counts as the third seal and the block finalizes (eligibility is "
      "load-bearing)", s, expect_unsat=False, kind="NEG-CTRL")

# =============================================================================
# S6 -- the emergency ceiling can only LOWER K, never raise it.
# =============================================================================
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.K_eff() > sched_K(b.h))
check("S6a CEILING ONLY LOWERS (all h, all ceiling values): effective K can never "
      "exceed the schedule K (minSealsCeiling cannot raise the threshold)", s)

# CONFIG: the engaged ceiling is the ONLY legal path below 3 -- with ceiling 1 a
# 1-seal anchor block finalizes. This documents WHY S1 assumes the ceiling is
# not engaged; it is the designed emergency lowering, not a bug.
b = Block()
s = Solver(); s.add(b.wf())
s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), b.ceil_set, b.ceil_val == 1)
s.add(b.distinct_eligible_valid() == 1)
s.add(b.finalized())
check("S6b CONFIG: with the emergency ceiling engaged at 1, a 1-seal anchor block "
      "finalizes (the ceiling is the ONLY legal path below K=3, by design)", s,
      expect_unsat=False, kind="CONFIG")

# =============================================================================
# S7 -- the write cap maxSeals=5 never starves the certificate below K=3.
# =============================================================================
c, w = Int('c'), Int('w')
s = Solver()
s.add(c >= 0, w == If(c <= MAX_SEALS, c, MAX_SEALS))     # producer writes min(c, 5)
s.add(c >= K_TARGET, w < K_TARGET)                       # negate: cap drops below K
check("S7a WRITE CAP (all counts): with maxSeals=5 >= K=3, capping the written "
      "certificate can never drop a >= 3-seal certificate below K", s)

# NEG-CTRL: a cap BELOW K (2) starves the certificate -- this is exactly why the
# config loader refuses maxSeals below the largest schedule K.
c, w = Int('c'), Int('w')
s = Solver()
s.add(c >= 0, w == If(c <= 2, c, 2))                     # planted cap 2 < K
s.add(c >= K_TARGET, w < K_TARGET)
check("S7b NEG-CTRL: PLANT a cap of 2 < K -> a 3-seal certificate is written short "
      "of the quorum (why maxSeals below the schedule K is refused at load)", s,
      expect_unsat=False, kind="NEG-CTRL")

# =============================================================================
print("\n=== SUMMARY (anchor BLOCKING-QUORUM SAFETY) ===")
allok = True
for name, tag, ok, kind in results:
    print(f"  {tag:9} [{kind}]  {name}")
    allok = allok and ok
print()
if allok:
    print("  PROVED: with the blocking fork active (h >= 14,050,000) no anchor block")
    print("  can be finalized with fewer than K=3 valid Falcon seals from DISTINCT")
    print("  signers of the registry active at that height (the 9-key registry, since")
    print("  the fork lies above the 13,600,000 rotation), and non-anchor blocks")
    print("  require no seals at all (proved in both directions). The mandated")
    print("  negative control FIRES: a planted rule permitting 2 seals finalizes an")
    print("  anchor block with exactly 2 seals (SAT), so the K>=3 guard is load-")
    print("  bearing and the S1 UNSAT is non-vacuous. Distinctness (replay collapses)")
    print("  and registry eligibility (foreign keys never count) are each load-")
    print("  bearing, with firing controls. The emergency ceiling can only LOWER K")
    print("  (and is the single designed path below 3); the maxSeals=5 write cap can")
    print("  never starve a certificate below K, and a planted cap of 2 does.")
    print("  BOUNDARY: design combinatorics of the finalization predicate, not Besu")
    print("  bytecode, not the live chain; registries modelled as index sets.")
else:
    print("  NOT fully established (see FAILED / unexpected result above).")
import sys
sys.exit(0 if allok else 1)