From 4ce1928d9eaf5a12a26b5ed3eaaab62f986fee52 Mon Sep 17 00:00:00 2001 From: Aere Network Date: Sat, 15 Aug 2026 21:05:47 +0300 Subject: [PATCH] Three formal models for the blocking post-quantum consensus, each with its negative control Written and run against z3 4.16.0, exit 0, on 2026-08-15, the day the blocking fork went live: - anchor_blocking_quorum: past block 14,050,000 no anchor block finalizes with fewer than K=3 distinct valid Falcon seals; the negative control that permits 2 seals is SAT (the violation is expressible), the property itself UNSAT. - pqanchor_ceiling_monotonicity: the emergency ceiling can only LOWER the effective threshold, never raise it, and K_eff always fits under the write cap; a planted max()-instead-of-min() ceiling is SAT. - registry_rotation_coverage: the registry schedule covers every anchor height with exactly one registry, no gap and no overlap, and a seal is checked against the registry active at the ANCHOR height; a planted schedule with a gap is SAT. These extend the existing SMT corpus toward end-to-end verifiability of the consensus, one of the pieces the roadmap calls distinctive. --- .../anchor_blocking_quorum_smt.py | 362 ++++++++++++++++++ .../pqanchor_ceiling_monotonicity_smt.py | 304 +++++++++++++++ .../registry_rotation_coverage_smt.py | 323 ++++++++++++++++ 3 files changed, 989 insertions(+) create mode 100644 formal-consensus/anchor_blocking_quorum_smt.py create mode 100644 formal-consensus/pqanchor_ceiling_monotonicity_smt.py create mode 100644 formal-consensus/registry_rotation_coverage_smt.py diff --git a/formal-consensus/anchor_blocking_quorum_smt.py b/formal-consensus/anchor_blocking_quorum_smt.py new file mode 100644 index 0000000..8360fe1 --- /dev/null +++ b/formal-consensus/anchor_blocking_quorum_smt.py @@ -0,0 +1,362 @@ +#!/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) diff --git a/formal-consensus/pqanchor_ceiling_monotonicity_smt.py b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py new file mode 100644 index 0000000..a2dfd6e --- /dev/null +++ b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py @@ -0,0 +1,304 @@ +#!/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) \ No newline at end of file diff --git a/formal-consensus/registry_rotation_coverage_smt.py b/formal-consensus/registry_rotation_coverage_smt.py new file mode 100644 index 0000000..c8f3a7f --- /dev/null +++ b/formal-consensus/registry_rotation_coverage_smt.py @@ -0,0 +1,323 @@ +#!/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)