#!/usr/bin/env python3
# -----------------------------------------------------------------------------
# pqanchor_ceiling_monotonicity_smt.py
#
# SMT proof (z3) of CEILING MONOTONICITY for the AERE post-quantum anchor
# (PqAnchorConfig / PqAnchorProducer): the emergency ceiling
# `aere.pq.anchor.minSealsCeiling` can only LOWER the effective seal threshold
#
#     K_eff(h) = min(K_schedule(h), ceiling)        (when the ceiling is set)
#     K_eff(h) = K_schedule(h)                      (when it is not)
#
# and can NEVER raise it; and for every height K_eff(h) <= maxSeals (the write
# cap `aere.pq.anchor.maxSeals`), so a conforming producer can always WRITE at
# least as many verified seals as the threshold it is asked to meet. A ceiling
# that raised K_eff would let an operator turn an emergency valve into a
# chain-stopping validity rule; min() makes that inexpressible by construction,
# and this file machine-checks it.
#
# Chain facts modelled as LAW (chain 2800, live values):
#   N = 9 validators, QBFT quorum = ceil(2N/3) = 6
#   anchor heights: every 32 blocks from 13,014,000
#   K schedule (height:K): 13,014,000 -> 0 ; 13,034,000 -> 3
#   write cap maxSeals = 5
#   emergency ceiling minSealsCeiling: only LOWERS K (that is the theorem)
#   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 ;
#   every height is covered by EXACTLY one registry
#
# Method (corpus convention): each property is a function that builds the
# constraints; we assert the NEGATION and UNSAT means the property HOLDS.
# Every claim is paired with a firing NEGATIVE CONTROL: the same search run
# against a PLANTED max()-variant (and a planted under-cap) must come back SAT,
# proving the min() and the loader guard are load-bearing, not vacuous.
#
# HONEST BOUNDARY: this checks the DESIGN arithmetic of the threshold pipeline
# (schedule -> ceiling -> effective K -> write cap), not the Besu Java code and
# not the Falcon verifier; heights are unbounded Ints, seal counts are counts
# of already-verified eligible seals (the producer cut sits AFTER verification,
# per the 13.2b design decision).
# -----------------------------------------------------------------------------
from z3 import Int, Bool, Solver, And, Or, Not, Implies, If, sat, unsat

# ---- chain 2800 constants (law) ---------------------------------------------
ANCHOR_START   = 13_014_000       # first anchor height
ANCHOR_STEP    = 32               # anchor every 32 blocks
K_STEP_HEIGHT  = 13_034_000       # schedule step: K goes 0 -> 3 here
K_WARMUP       = 0                # schedule K on [13,014,000 .. 13,034,000)
K_ARMED        = 3                # schedule K from 13,034,000 on
MAX_SEALS      = 5                # write cap aere.pq.anchor.maxSeals
BLOCKING_FORK  = 14_050_000       # no block finalizes without the Falcon quorum
REG1_HEIGHT, REG1_KEYS = 13_014_000, 7   # registry window 1
REG2_HEIGHT, REG2_KEYS = 13_600_000, 9   # registry window 2 (rotation)
N_VALIDATORS   = 9
QBFT_QUORUM    = 6                # ceil(2*9/3)

def k_schedule(h):
    """Height-indexed schedule 13014000:0, 13034000:3 (the live orar)."""
    return If(h >= K_STEP_HEIGHT, K_ARMED, K_WARMUP)

def k_eff(h, ceil_set, ceiling):
    """FIXED rule: the ceiling only ever takes the min (lowers, never raises)."""
    ks = k_schedule(h)
    return If(And(ceil_set, ceiling < ks), ceiling, ks)

def k_eff_buggy_max(h, ceil_set, ceiling):
    """PLANTED BUG for the negative control: max() instead of min()."""
    ks = k_schedule(h)
    return If(And(ceil_set, ceiling > ks), ceiling, ks)

def is_anchor_height(h):
    return And(h >= ANCHOR_START, (h - ANCHOR_START) % ANCHOR_STEP == 0)

def reg_keys(h):
    """Registry rotation: 7 keys before 13,600,000, 9 keys from there on."""
    return If(h >= REG2_HEIGHT, REG2_KEYS, REG1_KEYS)

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 -- CEILING MONOTONICITY: minSealsCeiling can only LOWER K_eff,")
print("### and K_eff <= maxSeals at every height (a conforming producer always suffices)\n")

# ---- CONFIG sanity: the quorum arithmetic and the height lattice are coherent -
s = Solver()
q = Int('q')
s.add(3 * q >= 2 * N_VALIDATORS, 3 * q <= 2 * N_VALIDATORS + 2)  # q = ceil(2N/3)
s.add(q != QBFT_QUORUM)
check(f"CONFIG N={N_VALIDATORS}: QBFT quorum ceil(2N/3) is exactly {QBFT_QUORUM}", s)

s = Solver()
s.add(Int('ok') == (1 if (K_STEP_HEIGHT - ANCHOR_START) % ANCHOR_STEP == 0 else 0))
s.add(Int('ok') == 1)
check(f"CONFIG K-step height {K_STEP_HEIGHT:,} lands ON the 32-block anchor lattice", s,
      expect_unsat=False, kind="CONFIG")

s = Solver()
s.add(Int('ok') == (1 if (BLOCKING_FORK - ANCHOR_START) % ANCHOR_STEP == 0 else 0))
s.add(Int('ok') == 1)
check(f"CONFIG blocking fork {BLOCKING_FORK:,} lands ON the 32-block anchor lattice", s,
      expect_unsat=False, kind="CONFIG")

# =============================================================================
# MONO-1  -- the ceiling NEVER raises the threshold: K_eff(h) <= K_schedule(h)
# for EVERY height and EVERY ceiling value (set or unset). This is exactly the
# UNSAT search the invariant demands: "a ceiling that raises K_eff" has no
# model, i.e. it is INEXPRESSIBLE under the fixed min() rule.
# =============================================================================
s = Solver()
h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(k_eff(h, ceil_set, ceiling) > k_schedule(h))     # search a RAISING case
check("MONO-1 (all heights, all ceilings): a ceiling that RAISES K_eff above the "
      "schedule is inexpressible (K_eff <= K_schedule always)", s)

# =============================================================================
# MONO-2  -- the ceiling is EXACTLY min(): K_eff <= ceiling whenever the
# ceiling is set. Together with MONO-1 this pins K_eff = min(K_schedule, ceil).
# =============================================================================
s = Solver()
h, ceiling = Int('h'), Int('ceiling')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(k_eff(h, True, ceiling) > ceiling)               # negate: K_eff above the ceiling
check("MONO-2 (all heights): with the ceiling SET, K_eff <= ceiling "
      "(the emergency valve really binds from above)", s)

# =============================================================================
# MONO-3  -- a ceiling AT or ABOVE the schedule is a no-op: K_eff == K_schedule.
# The valve is inert unless it actually lowers; setting it high changes nothing.
# =============================================================================
s = Solver()
h, ceiling = Int('h'), Int('ceiling')
s.add(is_anchor_height(h), ceiling >= k_schedule(h))
s.add(k_eff(h, True, ceiling) != k_schedule(h))        # negate: high ceiling changed K
check("MONO-3 (all heights): a ceiling >= K_schedule is a NO-OP "
      "(K_eff == K_schedule, the valve cannot perturb a healthy config)", s)

# =============================================================================
# CAP-1  -- loader guard (AERE-PQC-ANCHOR-CONF-01): the write cap maxSeals
# dominates the WHOLE schedule, so K_eff <= maxSeals at every height under
# every ceiling. This is what makes every threshold satisfiable by writing.
# =============================================================================
s = Solver()
h = Int('h')
s.add(is_anchor_height(h))
s.add(k_schedule(h) > MAX_SEALS)                       # negate: schedule above the cap
check(f"CAP-1a loader guard: K_schedule(h) <= maxSeals={MAX_SEALS} over the WHOLE "
      "schedule (both steps 0 and 3)", s)

s = Solver()
h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(k_eff(h, ceil_set, ceiling) > MAX_SEALS)         # negate: K_eff above the cap
check(f"CAP-1b (all heights, all ceilings): K_eff <= maxSeals={MAX_SEALS} "
      "(the ceiling cannot push the threshold past the write cap)", s)

# =============================================================================
# CAP-2  -- PRODUCIBILITY: a conforming producer that has heard at least K_eff
# verified eligible seals WRITES written = min(heard, maxSeals) and always
# satisfies written >= K_eff. The write cap can never starve the threshold.
# (The cut sits AFTER signature verification, so every written seal counts.)
# =============================================================================
s = Solver()
h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set')
heard = Int('heard')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(heard >= 0, heard <= reg_keys(h))                # at most one seal per registry key
keff = k_eff(h, ceil_set, ceiling)
s.add(heard >= keff)                                   # conforming fleet: threshold heard
written = If(heard < MAX_SEALS, heard, MAX_SEALS)      # producer cut: min(heard, maxSeals)
s.add(written < keff)                                  # negate: written falls short
check("CAP-2 PRODUCIBILITY (all heights): heard >= K_eff  =>  "
      f"written = min(heard, maxSeals={MAX_SEALS}) >= K_eff (cap never starves the threshold)", s)

# =============================================================================
# REG-1  -- registry coverage: EVERY height from 13,014,000 on is covered by
# EXACTLY ONE registry window (7 keys on [13.014M, 13.6M), 9 keys from 13.6M).
# =============================================================================
s = Solver()
h = Int('h')
s.add(h >= ANCHOR_START)
in_w1 = And(h >= REG1_HEIGHT, h < REG2_HEIGHT)
in_w2 = h >= REG2_HEIGHT
s.add(Or(And(in_w1, in_w2), And(Not(in_w1), Not(in_w2))))   # negate: both or neither
check("REG-1 (all heights >= 13,014,000): exactly ONE registry window covers each "
      "height (7-key window and 9-key window partition the range)", s)

# ---- REG-2: the registry always holds at least K_eff keys, so the threshold
#      is meetable by DISTINCT eligible signers in both windows.
s = Solver()
h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(k_eff(h, ceil_set, ceiling) > reg_keys(h))       # negate: threshold above key count
check("REG-2 (all heights, all ceilings): K_eff <= registry key count (7 then 9), "
      "so K_eff distinct eligible seals always EXIST to be heard", s)

# =============================================================================
# FORK-1  -- blocking era (h >= 14,050,000): once no block finalizes without
# the Falcon quorum, an unsatisfiable anchor threshold would be a chain stop.
# Under min(), the blocking era keeps K_eff <= maxSeals AND K_eff <= registry,
# for every ceiling: the emergency valve cannot be turned into a halt switch.
# =============================================================================
s = Solver()
h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set')
s.add(is_anchor_height(h), h >= BLOCKING_FORK, ceiling >= 0)
keff = k_eff(h, ceil_set, ceiling)
s.add(Or(keff > MAX_SEALS, keff > reg_keys(h)))        # negate: unsatisfiable threshold
check(f"FORK-1 blocking era (h >= {BLOCKING_FORK:,}): NO ceiling makes the anchor "
      "threshold unsatisfiable (K_eff <= maxSeals AND K_eff <= registry keys)", s)

# ============================ NEGATIVE CONTROLS ==============================
# Each control PLANTS a violation and must come back SAT, proving the searches
# above are load-bearing (a gate that has never failed cannot be believed).
# =============================================================================

# ---- NEG-CTRL 1: the PLANTED max() variant CAN raise K_eff above the schedule.
# Identical search to MONO-1, run against k_eff_buggy_max: must be SAT.
s = Solver()
h, ceiling = Int('h'), Int('ceiling')
s.add(is_anchor_height(h), ceiling >= 0)
s.add(k_eff_buggy_max(h, True, ceiling) > k_schedule(h))
check("NEG-CTRL 1 PLANTED max() ceiling: a ceiling that RAISES K_eff above the "
      "schedule IS expressible (same search as MONO-1 turns SAT)", s,
      expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 2: the PLANTED max() variant CAN push K_eff past the write cap
# in the BLOCKING era: every conforming certificate is then short, every anchor
# block is invalid, and the chain stops. This is the accident min() forbids.
s = Solver()
h, ceiling = Int('h'), Int('ceiling')
s.add(is_anchor_height(h), h >= BLOCKING_FORK, ceiling >= 0)
s.add(k_eff_buggy_max(h, True, ceiling) > MAX_SEALS)
check(f"NEG-CTRL 2 PLANTED max() ceiling, blocking era: K_eff CAN exceed "
      f"maxSeals={MAX_SEALS} (a settable value becomes a chain-stop switch)", s,
      expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 3: REMOVE the loader guard (AERE-PQC-ANCHOR-CONF-01) and plant
# a write cap BELOW the schedule step (maxSeals=2 < K=3): a conforming producer
# that heard every key still writes short certificates its OWN fleet rejects,
# while every config-side tool stays green (the request is self-consistent).
BAD_MAX_SEALS = 2
s = Solver()
h, heard = Int('h'), Int('heard')
s.add(is_anchor_height(h), h >= K_STEP_HEIGHT)         # armed schedule, K=3
s.add(heard >= 0, heard <= reg_keys(h))
ks = k_schedule(h)
s.add(heard >= ks)                                     # fleet fully conforming
written = If(heard < BAD_MAX_SEALS, heard, BAD_MAX_SEALS)
s.add(written < ks)                                    # certificate falls short anyway
check(f"NEG-CTRL 3 loader guard REMOVED (planted maxSeals={BAD_MAX_SEALS} < K={K_ARMED}): "
      "a fully conforming producer CAN only write rejected certificates "
      "(why AERE-PQC-ANCHOR-CONF-01 refuses this config at startup)", s,
      expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 4: MONO-2 is non-vacuous: a ceiling BELOW the schedule really
# does lower K_eff (the valve does something). Search K_eff < K_schedule: SAT.
s = Solver()
h, ceiling = Int('h'), Int('ceiling')
s.add(is_anchor_height(h), h >= K_STEP_HEIGHT, ceiling >= 0)
s.add(k_eff(h, True, ceiling) < k_schedule(h))
check("NEG-CTRL 4 non-vacuity: a ceiling BELOW the schedule DOES lower K_eff "
      "(the emergency valve is real, not a no-op in disguise)", s,
      expect_unsat=False, kind="NEG-CTRL")

# ------------------------------------------------------------------------------
print("\n=== SUMMARY (PQ anchor ceiling monotonicity) ===")
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 emergency ceiling minSealsCeiling can ONLY lower the effective")
    print("  threshold -- K_eff = min(K_schedule, ceiling), K_eff <= K_schedule for every")
    print("  height and every ceiling (a raising case is UNSAT, i.e. inexpressible), a")
    print("  ceiling at/above the schedule is a no-op, and K_eff <= maxSeals=5 and")
    print("  K_eff <= registry keys (7 then 9) at every height including the blocking era")
    print("  from 14,050,000 -- so a conforming producer (heard >= K_eff) always writes")
    print("  min(heard, maxSeals) >= K_eff and the valve can never become a halt switch.")
    print("  Negative controls FIRE: the planted max() variant raises K_eff (SAT), pushes")
    print("  it past the write cap in the blocking era (SAT, a chain-stop), a planted")
    print("  under-cap without the loader guard yields only rejected certificates (SAT,")
    print("  why AERE-PQC-ANCHOR-CONF-01 exists), and the valve itself is non-vacuous (SAT).")
    print("  BOUNDARY: design arithmetic of the threshold pipeline, not Besu bytecode;")
    print("  seal counts are counts of already-verified eligible seals.")
else:
    print("  NOT fully established (see FAILED / unexpected result above).")
import sys
sys.exit(0 if allok else 1)