#!/usr/bin/env python3
# -----------------------------------------------------------------------------
# registry_rotation_coverage_smt.py
#
# MACHINE-CHECKED (z3) ROTATION COVERAGE for the AERE PQ anchor key registries
# (chain 2800). The Falcon seal registry rotates on block height:
#
#   R1 activates at 13,014,000 with 7 validator keys
#   R2 activates at 13,600,000 with 9 validator keys
#
# INVARIANT (the task target):
#   (C1) every anchor height H >= 13,014,000 (anchors every 32 blocks from
#        13,014,000) is covered by EXACTLY one active registry: no height with
#        zero registries (gap) and no height with two (overlap);
#   (C2) seal validation selects the registry active at the ANCHOR height,
#        never at the validator's CURRENT head height. A historical seal's
#        verdict therefore never changes as the chain advances past a rotation
#        boundary (replay stability), and a key that joined in R2 can never be
#        used to seal an R1-era anchor (no new-key backdating).
#
# Chain facts modelled as law (measured on the live chain, 2026-08):
#   N = 9 validators, QBFT quorum = ceil(2N/3) = 6
#   anchor every 32 blocks from 13,014,000
#   K schedule 13,014,000:0 then 13,034,000:3 (K=3 minimum Falcon seals)
#   write cap maxSeals = 5; emergency minSealsCeiling can only LOWER K
#   blocking fork at 14,050,000: no block finalizes without the Falcon quorum
#   registry rotation 13,014,000 -> 7 keys, 13,600,000 -> 9 keys
#
# Schedule semantics (the design being proved): a registry is active from its
# own activation height up to, but excluding, the next registry's activation
# height; the last registry stays active forever. Coverage is by INTERVAL, so
# a rotation boundary that is not itself anchor-aligned loses no anchor (and
# 13,600,000 is NOT anchor-aligned; proved below, with the interval argument
# closing the hole).
#
# Method: each property is a function that builds the constraints; the
# property's NEGATION is asserted, so UNSAT means the property HOLDS. Each
# load-bearing check is paired with a NEGATIVE CONTROL that plants a violation
# (a gapped schedule, an overlapping schedule, a current-height lookup) and
# MUST come back SAT with a concrete witness; if a negative control did not
# fire, the model would be vacuous.
#
# ASSUMPTIONS (bound every PROVED below):
#   A1. R2 retains R1's 7 keys (indices 0..6) and adds two (indices 7..8),
#       matching the fleet growth from 7 to 9 validators. Only the DIFFERENCE
#       (indices 7..8 exist solely in R2) is load-bearing for the backdating
#       and divergence results.
#   A2. Heights are unbounded nonnegative integers (LIA); "anchor height" means
#       H = 13,014,000 + 32k for some integer k >= 0.
#
# HONEST BOUNDARY: this proves the SCHEDULE ARITHMETIC and the lookup-keying
# design, unbounded in height over LIA. It does not re-prove Falcon signature
# soundness (falcon_*_smt.py) nor QBFT agreement (qbft_safety_smt.py), and it
# checks the design, not the Besu Java bytecode.
# -----------------------------------------------------------------------------
from z3 import Int, Bool, Solver, And, Or, Not, Implies, If, sat, unsat

# ---- chain constants (the law) ----------------------------------------------
N_VALIDATORS   = 9
QBFT_QUORUM    = 6            # ceil(2*9/3)
ANCHOR0        = 13_014_000   # first anchor height and R1 activation
ANCHOR_STEP    = 32
K_STEP_HEIGHT  = 13_034_000   # K schedule: 13014000:0, 13034000:3
K_MIN_SEALS    = 3
MAX_SEALS      = 5            # write cap
FORK_BLOCKING  = 14_050_000   # no finality without the Falcon quorum from here
REG1_HEIGHT    = 13_014_000
REG1_KEYS      = 7
REG2_HEIGHT    = 13_600_000
REG2_KEYS      = 9

NONE, R1, R2 = 0, 1, 2

# ---- schedule semantics: active-from-own-height-until-next ------------------
def active_r1(h):
    return And(h >= REG1_HEIGHT, h < REG2_HEIGHT)

def active_r2(h):
    return h >= REG2_HEIGHT

def coverage_count(h):
    return If(active_r1(h), 1, 0) + If(active_r2(h), 1, 0)

def lookup(h):
    # registry selected for height h, derived from the SAME active predicates
    return If(active_r2(h), R2, If(active_r1(h), R1, NONE))

def reg_size(reg):
    return If(reg == R1, REG1_KEYS, If(reg == R2, REG2_KEYS, 0))

def member(reg, kx):
    # A1: R2 = R1's keys plus indices 7..8
    return Or(And(reg == R1, kx >= 0, kx <= REG1_KEYS - 1),
              And(reg == R2, kx >= 0, kx <= REG2_KEYS - 1))

def add_anchor(s, h, kname):
    # h is an anchor height: h = ANCHOR0 + 32k, k >= 0
    k = Int(kname)
    s.add(h == ANCHOR0 + ANCHOR_STEP * k, k >= 0)
    return k

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

print("### AERE PQ anchor -- REGISTRY ROTATION COVERAGE"
      " (R1@13,014,000 x7 keys, R2@13,600,000 x9 keys)\n")

# =============================================================================
# C1a  NO GAP: every anchor height >= 13,014,000 has at least one registry
# -----------------------------------------------------------------------------
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(coverage_count(h) == 0)          # negate: an anchor with NO registry
check("C1a no gap: every anchor height >= 13,014,000 has an active registry "
      "(unbounded in height)", s)

# =============================================================================
# C1b  NO OVERLAP: no anchor height has two active registries
# -----------------------------------------------------------------------------
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(coverage_count(h) >= 2)          # negate: an anchor with TWO registries
check("C1b no overlap: no anchor height has two active registries "
      "(unbounded in height)", s)

# =============================================================================
# C1c  EXACTLY ONE, stated directly (implied by C1a+C1b; kept as the invariant
#      as worded)
# -----------------------------------------------------------------------------
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(coverage_count(h) != 1)
check("C1c exact coverage: every anchor height is covered by EXACTLY one "
      "registry", s)

# =============================================================================
# BOUNDARY ARITHMETIC: the rotation boundary 13,600,000 is NOT anchor-aligned
# (13,600,000 - 13,014,000 = 586,000 = 32*18312 + 16), and interval coverage
# makes that harmless: C1a already proved no anchor is lost around it. The
# K-step height and the blocking-fork height ARE anchor-aligned.
# -----------------------------------------------------------------------------
s = Solver()
k = Int('k')
s.add(REG2_HEIGHT == ANCHOR0 + ANCHOR_STEP * k)   # negate alignment: no such k
check("boundary: R2 activation 13,600,000 is NOT an anchor height "
      "(no k with 13,600,000 = 13,014,000 + 32k); interval coverage closes "
      "the hole (C1a)", s)

s = Solver()
k, r = Int('k'), Int('r')
s.add(K_STEP_HEIGHT == ANCHOR0 + ANCHOR_STEP * k + r, r >= 1, r <= 31)
check("boundary: K-step height 13,034,000 IS anchor-aligned "
      "(remainder 1..31 is infeasible)", s)

s = Solver()
k, r = Int('k'), Int('r')
s.add(FORK_BLOCKING == ANCHOR0 + ANCHOR_STEP * k + r, r >= 1, r <= 31)
check("boundary: blocking fork 14,050,000 IS anchor-aligned "
      "(remainder 1..31 is infeasible)", s)

# =============================================================================
# C2a  REPLAY STABILITY: with the ANCHOR-keyed rule, a seal's verdict on an
#      anchor at height a is identical at any two current head heights c1, c2.
#      Holds by construction (the rule never reads the current height); the
#      paired NEG-CTRL 3 shows the current-height rule breaks exactly this,
#      so the keying choice is the load-bearing element.
# -----------------------------------------------------------------------------
s = Solver()
a, c1, c2, kx = Int('a'), Int('c1'), Int('c2'), Int('kx')
add_anchor(s, a, 'k')
s.add(c1 >= a, c2 >= a, kx >= 0, kx <= REG2_KEYS - 1)
v1 = member(lookup(a), kx)             # verdict as computed at head c1
v2 = member(lookup(a), kx)             # verdict as computed at head c2
s.add(v1 != v2)                        # negate: verdict changed with the head
check("C2a replay stability: anchor-keyed verdict is independent of the "
      "current head height", s)

# =============================================================================
# C2b  NO NEW-KEY BACKDATING: a key that exists only in R2 (index 7..8) can
#      never validate a seal on an R1-era anchor, no matter how far past the
#      rotation the validating node's head is.
# -----------------------------------------------------------------------------
s = Solver()
a, c, kx = Int('a'), Int('c'), Int('kx')
add_anchor(s, a, 'k')
s.add(a < REG2_HEIGHT)                 # R1-era anchor
s.add(kx >= REG1_KEYS, kx <= REG2_KEYS - 1)   # key added in R2 only
s.add(c >= REG2_HEIGHT)                # validator already lives in the R2 era
s.add(member(lookup(a), kx))           # negate: the seal is ACCEPTED
check("C2b no backdating: an R2-only key is rejected on every R1-era anchor "
      "(anchor-keyed rule)", s)

# =============================================================================
# LAW CROSS-CHECKS: the blocking era is served entirely by R2, and the demanded
# seal count can always be supplied by the active registry.
# -----------------------------------------------------------------------------
# every anchor at/after the blocking fork is covered by R2 and ONLY R2
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(h >= FORK_BLOCKING)
s.add(Or(Not(active_r2(h)), active_r1(h)))     # negate: not-R2 or still-R1
check("blocking era: every anchor >= 14,050,000 is covered by the 9-key R2 "
      "and only by it", s)

# the active registry at any blocking-era anchor can supply the Falcon quorum
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(h >= FORK_BLOCKING)
s.add(reg_size(lookup(h)) < QBFT_QUORUM)       # negate: registry too small
check("blocking era: active registry size (9) >= Falcon quorum (6) at every "
      "blocking-era anchor", s)

# minSealsCeiling only LOWERS K; effective K never exceeds K=3, the write cap
# maxSeals=5, or the size of the registry active at any covered anchor
s = Solver()
h, ceil_ = Int('h'), Int('ceil')
add_anchor(s, h, 'k')
s.add(ceil_ >= 0)
k_eff = If(ceil_ < K_MIN_SEALS, ceil_, K_MIN_SEALS)
s.add(Or(k_eff > K_MIN_SEALS,
         k_eff > MAX_SEALS,
         k_eff > reg_size(lookup(h))))
check("K discipline: effective K (ceiling can only lower 3) never exceeds "
      "K=3 <= maxSeals=5 <= active registry size, at every covered anchor", s)

# ============================ NEGATIVE CONTROLS ==============================

# ---- NEG-CTRL 1 (the task's required control): a GAPPED schedule, R1 ends at
#      13,500,000 but R2 only starts at 13,600,000, MUST make the search for an
#      uncovered anchor SAT (z3 exhibits a concrete orphaned anchor height).
GAP_END = 13_500_000
def buggy_gap_r1(h): return And(h >= REG1_HEIGHT, h < GAP_END)
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(If(buggy_gap_r1(h), 1, 0) + If(active_r2(h), 1, 0) == 0)
check("NEG-CTRL 1 gapped schedule (R1 ends 13,500,000, R2 starts 13,600,000): "
      "an UNCOVERED anchor EXISTS", s, expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 2: an OVERLAPPING schedule (R1's deactivation forgotten, active
#      forever) MUST make the search for a doubly-covered anchor SAT.
def buggy_overlap_r1(h): return h >= REG1_HEIGHT
s = Solver()
h = Int('h')
add_anchor(s, h, 'k')
s.add(If(buggy_overlap_r1(h), 1, 0) + If(active_r2(h), 1, 0) >= 2)
check("NEG-CTRL 2 overlapping schedule (R1 never deactivated): a DOUBLY-"
      "covered anchor EXISTS", s, expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 3: a BUGGY validator keyed on the CURRENT height makes the same
#      historical seal flip verdict as the head crosses 13,600,000: two nodes
#      at different heads DISAGREE on one seal, which is a chain split.
s = Solver()
a, c1, c2, kx = Int('a'), Int('c1'), Int('c2'), Int('kx')
add_anchor(s, a, 'k')
s.add(c1 >= a, c2 >= a, kx >= 0, kx <= REG2_KEYS - 1)
v1 = member(lookup(c1), kx)            # BUG: registry chosen by head height
v2 = member(lookup(c2), kx)
s.add(v1 != v2)
check("NEG-CTRL 3 current-height lookup: one seal, two heads, two VERDICTS "
      "(replay divergence exists)", s, expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 4: the same buggy rule ACCEPTS an R2-only key on an R1-era
#      anchor once the head passes the rotation: history becomes forgeable by
#      a key that did not exist when the anchor was sealed.
s = Solver()
a, c, kx = Int('a'), Int('c'), Int('kx')
add_anchor(s, a, 'k')
s.add(a < REG2_HEIGHT, kx >= REG1_KEYS, kx <= REG2_KEYS - 1, c >= REG2_HEIGHT)
s.add(member(lookup(c), kx))           # BUG accepts the backdated seal
check("NEG-CTRL 4 current-height lookup: an R2-only key CAN seal an R1-era "
      "anchor (backdating accepted)", s, expect_unsat=False, kind="NEG-CTRL")

# ------------------------------------------------------------------------------
print("\n=== SUMMARY (REGISTRY ROTATION COVERAGE) ===")
allok = True
for name, tag, ok, kind in results:
    print(f"  {tag:9} [{kind}]  {name}")
    allok = allok and ok
print()
if allok:
    print("  PROVED: the registry schedule (R1@13,014,000 x7, R2@13,600,000 x9,")
    print("  active-until-next semantics) covers every anchor height >= 13,014,000")
    print("  with EXACTLY one registry, unbounded in height: no gap, no overlap.")
    print("  The rotation boundary 13,600,000 is not anchor-aligned and interval")
    print("  coverage loses no anchor; the K-step and blocking-fork heights are")
    print("  anchor-aligned. Anchor-keyed validation is replay-stable and rejects")
    print("  R2-only keys on R1-era anchors; the blocking era >= 14,050,000 is")
    print("  served entirely by the 9-key registry, which always covers the Falcon")
    print("  quorum (6) and the effective K (<= 3 <= maxSeals 5). All four negative")
    print("  controls FIRE: a gapped schedule orphans an anchor, a forgotten")
    print("  deactivation double-covers one, and a current-height lookup both")
    print("  splits verdicts across heads and accepts a backdated R2-only seal,")
    print("  so the coverage checks and the anchor-height keying are load-bearing.")
    print("  BOUNDARY: schedule arithmetic and lookup keying only (LIA, design")
    print("  level); Falcon soundness and QBFT agreement are proved elsewhere in")
    print("  this corpus, and this is not the Besu bytecode.")
else:
    print("  NOT fully established (see FAILED / unexpected result above).")
import sys
sys.exit(0 if allok else 1)