#!/usr/bin/env python3 # ----------------------------------------------------------------------------- # anchor_rewrite_bound_roundfree_smt.py # # MACHINE-CHECKED (z3) REWRITE BOUND of the AERE post-quantum header anchor on # chain 2800, against the adversary of AIP-22 "Security Considerations" and of # the threat model page: an adversary who holds EVERY classical (secp256k1 ECDSA) # validator key and NO post-quantum key, facing a node that enforces the # published anchor rules. Written 2026-10-07 for the question "where is the # security argument, formal model or reproducible test that establishes the # rewrite bound under the corrected round-free seal model" (AIP-22 erratum of # 2026-10-01); revised the same day after two adversarial reviews (see the dated # block at the end). The written argument is # research/rewrite-bound-round-free-seal-2026-10-07.md. # # THE RULES MODELLED (chain 2800 today; sources: aere-node SPEC.md 3.3/3.4/6.4, # patches/0003-aere-pq-anchor.patch, 0008-aere-pq-aip22.patch, AIP-15, AIP-21/22 # errata of 2026-10-01): # R1 the anchor block A carries, in vanityData, which is UNDER hash(A), the # digest of the certificate it carries for its parent; strip, swap or # reorder the certificate and A is refused. # R2 at an anchor height, the certificate must carry at least K_eff seals # from DISTINCT members of the PARENT's validator set, each verifying over # M(parent) = keccak256(RLP["AERE-PQ-COMMIT-1", chainId, number, hash(parent)]) # which carries NO round. K_eff = min(schedule K, emergency ceiling): # the schedule says 7 since block 20,715,632; a validator runs with no # ceiling (K_eff = 7); the PUBLISHED from-genesis follower runs with # aere.pq.anchor.minSealsCeiling=1 (SPEC 6.4, RUN-A-NODE "Why the # seal-threshold ceiling"), so its K_eff is 1. The keys a seal is checked # against come from the registry epoch bound at the parent's height, # which the node HOLDS (published epoch files) and the chain PINS by hash # (genesis pqRegistryHash, anchor-contract slot 0, v3 epoch hashes); an # epoch the node does not hold is refused, fail closed (AIP-15). # GRID anchors every 32nd block from 13,014,000 (Falcon-512); every 128th # BLOCK also needs SLH-DSA seals (a second scheme; see the boundary). From # 2026-09-05 to 2026-09-29 (blocks 17,225,968 to 20,746,736) the interval # was 128; it is 32 again from 20,746,736, which lies on the same grid. # # THE ADVERSARY: forges any ECDSA artefact (headers, commit seals, message # envelopes) because it holds every classical key, and can therefore build any # block whose validity needs only classical material (chain 2800 is below # AIP-22 stage 5, so a header needs the ECDSA commit quorum of one round, # which it has). This is POSTERIOR corruption: the keys are obtained after the # honest history was produced, with at most f = 3 Byzantine validators at that # time (QBFT safety held, so every height has one decided block and every # proposal extends the decided head: axiom A3 below). It holds j post-quantum # keys, j = 0 in the headline claim; every certificate it presents must be # assembled from seals HONEST validators made plus at most j of its own. It # also holds the Foundation's classical registry-writer key (AIP-22, Security # Considerations, "Registry writer") and can pin a rogue epoch inside its own # tail; it cannot make the victim LOAD an epoch the victim does not hold. # # THE MODEL (combinatorics of acceptance over heights, not cryptography): the # honest chain has a block at every height, anchors on the grid, and every # honest anchor is accepted (so for every honest parent there is a reusable # honest certificate). An alternative history forks at height F (its block at # F differs from the honest one; at every height >= F it differs, because the # hash of a block covers its parent hash, lemma L0a) and ends at head Hp. The # node accepts it only if EVERY anchor height a with F <= a <= Hp carries an # accepted certificate over the alternative parent at a-1. Honest seals exist # over: (i) the honest block at every height, and, under the CORRECTED # (round-free) model, (ii) an UNDECIDED SIBLING of the honest block at a # height, if honest validators committed it in rounds that did not decide it # (AIP-22 erratum, 2026-10-01: seals over M carry no round, so such seals are # indistinguishable from seals over a decided block). A sibling shares the # honest block's PARENT (A3: QBFT proposes only on top of the decided head), so # it can sit in the alternative history only at height F itself, where the # alternative block's parent is still the honest block F-1 (the "common # grandparent" fact). # # ENCODING, quantifier-free on purpose (a first form with ForAll over anchor # heights did not return in five minutes): "every anchor in [F, Hp] is # accepted" is checked on the first U = 40 anchor heights at or above F, i.e. # on a window of 1280 blocks above the fork (5120 in the 128-interval window). # For the PROOFS (UNSAT) this is a NECESSARY condition of acceptance in the # regime the history is confined to, so any bound proved under it holds under # the real, stronger condition; for the NEGATIVE CONTROLS the planted witness # is exactly DEEP = 1000 blocks deep, inside the window, so every anchor of # the witness is checked. keccak is an uninterpreted function with injectivity # instantiated on the terms in play. The headline claims confine the history to # the regime in force today (fork point above 20,746,736: interval 32, K = 7); # the dated 128-interval window has its own pair of proofs (bounds 128 / 129). # # WHAT CARRIES THE BOUND, and what each rule adds (measured by planting, see the # dated block at the end): the bound 32 / 33 rests on R2 with ANY K_eff >= 1 (one # seal the adversary cannot make, over a message that names hash(parent)), the # grid, the hash chain (L0a) and honest validators sealing only blocks they # committed (plus A3 for the one-block limit of the exception). R1 is not what # bounds the depth; it is what makes an anchor's HASH commit to its certificate # (L0b), so a reference hash pins the certificates below it and the public # verifier can check a certificate against a hash. K_eff = 7 with distinctness # is what bounds a PARTIAL post-quantum compromise: with j < K_eff # post-quantum keys the depth is still bounded (P4a), with j = K_eff it is not # (N4a); on the published follower (K_eff = 1) one leaked post-quantum key is # enough (N5d), and one honest seal over a sibling buys the 33rd block (C5c). # # PROVED (negation UNSAT) / LEMMAS / CONFIG / DEFN: # L0 lemmas with their own negative controls: a different parent hash gives # a different block hash (L0a; the parent hash is in the pre-image, N3a # plants it out on the unrolled chain), and (R1) an anchor with a # different certificate has a different hash (L0b; P0c plants the # certificate out of the pre-image). # P1 BASELINE (no sibling seals): any accepted alternative history replaces # at most 32 blocks: the latest anchor block itself (its certificate is # over the honest parent and can be reused) and the 31 blocks after it; # and if the alternative is at least as long as the honest chain, its # fork point is at or above the latest honest anchor: the latest anchor's # PARENT and everything below it are kept. # P2 CORRECTED (round-free seals, sibling certified): the bound becomes 33 # (the anchor's parent can be replaced by its sealed sibling), the fork # point is at or above the latest anchor's parent: the latest anchor's # GRANDPARENT and everything below it are kept; and the extra block needs # K_eff honest seals over the sibling (with fewer, the bound is 32 again). # P3 a node that knows the hash of one honest anchor a_ref refuses every # history that diverges at or below a_ref: ENCODED as the hash chain # unrolled for W_REF = 1280 heights above the fork (the induction step is # L0a; z3 does not induct, so the proof is for a reference at most 1280 # heights above the fork and the step carries it further on paper), with # N3a planting the parent hash out of the pre-image (re-convergence SAT). # P4 PARTIAL post-quantum compromise, validator's K_eff = 7: with j = 6 # post-quantum keys the bound is still 33 and the extra block needs # K_eff - j honest sibling seals; with j = 7 the depth is unbounded (N4a). # P5 the PUBLISHED FOLLOWER, K_eff = 1: bounds 32 / 33 hold against zero # post-quantum keys; one honest sibling seal buys the 33rd block (C5c); # one post-quantum key makes the depth unbounded (N5d). # P6 the dated 128-INTERVAL window (2026-09-05 to 2026-09-29): bounds 128 # and 129, for any K_eff >= 1 in force then. # C1 CONFIG: the 32- and 33-block witnesses are reachable (non-vacuity of # P1/P2), the 33-block witness forking at the latest anchor's parent. # D1 DEFN (an arithmetic restatement, not a proof, no negative control): # below AIP-22 stage 5 a header needs the ECDSA commit quorum, Q = 7 # keys, which this adversary holds and one validator does not. # NEGATIVE CONTROLS (each must be SAT, proving the guard is load-bearing): # N1 a planted rule that accepts anchors without a certificate (K_eff = 0, # also the dated K:0 steps of the schedule): the rewrite depth is unbounded. # N2 an adversary who ALSO holds every post-quantum key: unbounded. # N3 drop the common-grandparent fact (a sealed sibling at ANY height, over # any parent): P2's bound of 33 falls, the depth is unbounded. # N4a j = K_eff post-quantum keys: unbounded (and j = K_eff - 1 is not, P4a). # N5d K_eff = 1 (the published follower) with one post-quantum key: unbounded. # P0c the certificate outside the hashed pre-image: one hash, two certificates. # P3c a node with NO reference accepts a history that diverges below an anchor. # CONTROL OF THE CONTROL: `--plant-bounds` lowers every claimed bound by one; # P1a, P2a, P2c, P3b, P4a, P4b, P5a, P5b, P6a, P6b must then come out FAILED # (sat) and the script must exit 1 (measured: exactly those ten, exit 1). A # gate that has never failed cannot be believed. # # HONEST BOUNDARY (read it, it is the contract of this file): # - this is the combinatorics of the acceptance rules over heights, # certificates and parent/sibling relations; it does not re-prove the # counting rule of R2 (distinctness, registry eligibility, write cap), # which anchor_blocking_quorum_smt.py proves separately, nor Falcon-512 # or keccak (modelled as unforgeable / injective), nor message delivery, # nor the Java or C# code of either client; # - the modelled acceptance predicate is a NECESSARY condition of the real # one (the SLH-DSA seals demanded every 128th block, the acceptable index # order, the per-scheme counts are extra requirements), so a bound proved # here holds a fortiori for the real rules; the negative controls plant # their violations in this predicate; # - it assumes QBFT safety held while the honest history was produced (at # most f Byzantine validators then, A3); a set that was already Byzantine # beyond f when it sealed is outside the claim, as is a validator that # equivocates with its post-quantum key (N2 / N4a are that world); # - it assumes the node verifies seals against registry epochs it holds and # the chain pins by hash; a node that takes its epochs over a classical # channel at sync time, or with a different registry.history, is outside # the claim (an adversary who could install an epoch is N2); # - it says nothing about a node that syncs from genesis with no reference # point (weak subjectivity, AIP-22 section 4 rule 5): such a node can be # shown a history that stops before the first enforced anchor (P3c); P3 is # the statement for a node WITH a reference (aere.pq.checkpoint=:, # patch 0008, inert unless set); history below block 13,014,000 has no # certificates and is covered only through the hash chain from a reference # anchor (P3), and the dated windows in which K_eff was 0 (the warm-up step # 13014000:0, the dated step 17102384:0, the disarmed window D4 of SPEC # section 8) are outside the claim at those heights (N1 is exactly that # rule); a window with K_eff = 1 (D5) is inside it (P5); # - the exception of P2 needs honest validators to have sealed the sibling # in non-deciding rounds at the height of the anchor's parent; whether an # adversary can bring that about is a scheduling question (measured in a # test fixture, AereRoundFreeCertificateTest, with SIX honest seals plus the # seal of one Byzantine validator holding a post-quantum key, not on any # network); this model takes "a sealed sibling with s honest seals exists" # as a free assumption, for every s in [0, N], and shows the bound even then; # - "accepted" here is the header-rule verdict; which chain a node then # treats as canonical is fork choice, modelled only as "at least as long" # (QBFT chains have no work; height decides). # # Convention of this directory: a property is a function that builds the # constraints; UNSAT of the negation means it HOLDS; every proof is paired with a # negative control that plants the violation and must come back SAT. # ----------------------------------------------------------------------------- import sys, time from z3 import (Int, IntVal, Function, IntSort, Solver, And, Or, Not, Implies, If, sat, unsat) # ---- chain facts (LAW, chain 2800, 2026-10-07) ------------------------------ CHAIN_ID = 2800 ANCHOR_START = 13014000 # first anchor height (grid origin) INTERVAL = 32 # Falcon-512 anchor every 32nd block (AIP-22 stage 2, from 20,746,736) INTERVAL_128 = 128 # the dated interval, blocks 17,225,968 .. 20,746,736 (2026-09-05 .. 2026-09-29) WINDOW_128 = (17225968, 20746736) STAGE2_GRID_START = 20746736 # interval 32 again from here; K = 7 in force since 20,715,632 (< this) SLH_INTERVAL = 128 # SLH-DSA also required every 128th BLOCK (second scheme; not modelled) K = 7 # schedule K since 20,715,632 (AIP-22 stage 1); a validator's K_eff K_FOLLOWER = 1 # the published from-genesis follower: minSealsCeiling=1 -> K_eff = 1 (SPEC 6.4) N, Q, F_BYZ = 10, 7, 3 # validators, QBFT commit quorum ceil(2N/3), fault bound BOUND_BASE = 32 # claimed bound, baseline: anchor block + 31 BOUND_CORRECTED = 33 # claimed bound under the round-free exception: + the anchor's parent BOUND_BASE_128 = 128 # the same two bounds inside the dated 128-interval window BOUND_CORR_128 = 129 DEEP = 1000 # "unbounded" witness depth for the negative controls U_ANCHORS = 40 # anchors checked above the fork: 40 * 32 = 1280 > DEEP (+ one interval) W_REF = 1280 # heights unrolled above the fork for the reference-hash proof P3a SOLVER_TIMEOUT_MS = 120000 # an unknown is reported as FAILED, never as a verdict PLANT_BOUNDS = "--plant-bounds" in sys.argv # control of the control: every claimed bound one too low if PLANT_BOUNDS: BOUND_BASE -= 1; BOUND_CORRECTED -= 1; BOUND_BASE_128 -= 1; BOUND_CORR_128 -= 1 print("!!! --plant-bounds: every claimed bound lowered by one; the bound proofs MUST come out FAILED " "and this script MUST exit 1\n") assert U_ANCHORS * INTERVAL > DEEP + INTERVAL, "the negative-control witnesses must lie inside the checked window" assert (STAGE2_GRID_START - ANCHOR_START) % INTERVAL == 0, "the stage-2 grid origin lies on the 13,014,000 grid" assert (WINDOW_128[0] - ANCHOR_START) % INTERVAL_128 == 0 and (WINDOW_128[1] - ANCHOR_START) % INTERVAL_128 == 0, \ "the 128-interval window's ends lie on the 128 sub-grid of the 13,014,000 grid" results = [] def check(name, s, expect_unsat=True, kind="PROOF"): s.set("timeout", SOLVER_TIMEOUT_MS) t0 = time.time() r = s.check() dt = time.time() - t0 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, dt)) print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'}) [{dt:.3f}s]") if r == sat: m = s.model(); wit = {} for d in m.decls(): if d.arity() != 0: continue 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 def is_anchor(h, interval=INTERVAL): return And(h >= ANCHOR_START, (h - ANCHOR_START) % interval == 0) # ---- the honest material the adversary can reuse ---------------------------- # honest_over_honest(n): number of distinct honest validators whose seal over # M(honest block at n) exists; the honest chain is accepted, so at every anchor # parent it is >= the K in force (axiom A1). honest_over_sibling(n): number of # distinct honest validators that sealed an UNDECIDED SIBLING of the honest block # at n in rounds that did not decide it (the round-free exception); 0 in the # baseline, free in [0, N - j] in the corrected model (A2). honest_over_honest = Function('honest_over_honest', IntSort(), IntSort()) honest_over_sibling = Function('honest_over_sibling', IntSort(), IntSort()) class Rules: """One acceptance predicate per variant. cert_ok(a, F) says whether the adversary can present, for the ALTERNATIVE anchor at height a of a history forked at F, a certificate the node accepts over the alternative parent at a-1. The parent is: the honest block (a-1 < F), the alternative block at F (a-1 == F; a sealed sibling only if the variant allows it), or an alternative block above F (a-1 > F). A3 (common grandparent) is the `n == F` case: a sibling fits only where the alternative parent is honest.""" def __init__(self, required=K, siblings=False, adv_pq_keys=0, any_parent=False, interval=INTERVAL, honest_floor=None): self.required = required # K_eff in force (0 = planted "no certificate needed") self.siblings = siblings # round-free exception: honest seals over an undecided sibling exist self.adv_pq_keys = adv_pq_keys # post-quantum keys of distinct validators the adversary holds (j) self.any_parent = any_parent # PLANTED: a sealed sibling may sit over ANY parent (drops A3) self.interval = interval # anchor grid interval in force self.honest_floor = required if honest_floor is None else honest_floor # A1: honest anchors carry >= this assert 0 <= adv_pq_keys <= N def honest_seals_over_alt_parent(self, a, F): n = a - 1 over_honest = honest_over_honest(n) over_sibling = honest_over_sibling(n) if self.siblings else IntVal(0) if self.any_parent: # PLANTED: the alternative block at any height >= F may be a sealed "sibling" return If(n < F, over_honest, over_sibling) # the sibling shares the honest parent, so it fits the alternative history only at F (A3) return If(n < F, over_honest, If(n == F, over_sibling, IntVal(0))) def cert_ok(self, a, F): # the adversary's own post-quantum keys belong to j distinct validators, disjoint from the honest ones return self.honest_seals_over_alt_parent(a, F) + IntVal(self.adv_pq_keys) >= self.required def accepted(self, s, F, Hp, tag): """The node accepts the alternative history (fork F, head Hp): every anchor height in [F, Hp] carries an accepted certificate over its alternative parent. Checked on the first U_ANCHORS anchor heights at or above F (a necessary condition; see the header).""" a1 = Int(f'a1_{tag}') # the first anchor height >= F s.add(is_anchor(a1, self.interval), a1 >= F, a1 < F + self.interval) # posterior corruption: the seals over HONEST blocks were made before any key leaked, by any of # the N validators (A1, cap N); the honest seals over a SIBLING that the adversary may add its own # j to come only from the N - j validators whose keys it does not hold (A2, cap N - j) honest_sibling_max = N - self.adv_pq_keys conds = [] for i in range(U_ANCHORS): a = a1 + i * self.interval # axioms instantiated at every checked anchor height s.add(honest_over_honest(a - 1) >= self.honest_floor, honest_over_honest(a - 1) <= N) # A1 s.add(honest_over_sibling(a - 1) >= 0, honest_over_sibling(a - 1) <= honest_sibling_max) # A2 conds.append(Or(a > Hp, self.cert_ok(a, F))) return And(conds) def history(s, interval=INTERVAL, f_above=STAGE2_GRID_START, hp_below=None): """A fork point F (first height at which the alternative differs), the alternative head Hp, the honest head H and its latest anchor a_last. The history is confined to one regime: F above f_above (interval 32 and K = 7 in force from STAGE2_GRID_START; the headline claim) and, when given, the alternative head below hp_below (the dated 128-interval window).""" F, Hp, H, a_last = Int('F'), Int('Hp'), Int('H'), Int('a_last') s.add(F > f_above) # inside the regime the claim is about s.add(Hp >= F) # at least one alternative block s.add(H >= F, is_anchor(a_last, interval), a_last <= H, H - a_last < interval) # a_last = latest honest anchor <= H if hp_below is not None: s.add(Hp < hp_below, H < hp_below) return F, Hp, H, a_last print("### AERE anchor REWRITE BOUND under the round-free seal model -- chain 2800, " f"N={N}, Q={Q}, K={K} (validator) / K_eff={K_FOLLOWER} (published follower), grid {INTERVAL} from {STAGE2_GRID_START}\n") print(f" adversary: every classical key, j post-quantum keys (j = 0 headline); node: enforces R1 + R2 + grid;" f" acceptance checked on {U_ANCHORS} anchors above the fork\n") # ============================================================================= # L0 -- the hash chain: keccak injective, the hash covers the parent hash, and # (R1) the anchor hash covers the certificate digest. From this, a history that # differs at F differs at every height above F (induction step shown). # ============================================================================= hash_of = Function('hash_of', IntSort(), IntSort(), IntSort()) # hash(parentHash, bodyDigest) -> blockHash hash_body = Function('hash_body', IntSort(), IntSort()) # PLANTED: a hash over the body alone digest_of = Function('digest_of', IntSort(), IntSort()) # keccak over (chainId, parentNumber, parentHash, certificate) def injective_on(s, pairs): """keccak modelled injective: instantiated on the applications in play.""" for (x1, y1), (x2, y2) in pairs: s.add(Implies(hash_of(x1, y1) == hash_of(x2, y2), And(x1 == x2, y1 == y2))) s = Solver() ph, ph2, body = Int('parentHash_hon'), Int('parentHash_alt'), Int('body') injective_on(s, [((ph, body), (ph2, body))]) s.add(ph != ph2, hash_of(ph, body) == hash_of(ph2, body)) check("L0a HASH CHAIN STEP: two blocks with different parent hashes and the SAME body have " "different hashes (a fork at F propagates to every height above F)", s, kind="LEMMA") # the negative control of L0a is N3a below: the same plant (a hash over the body alone), # exercised on the unrolled chain, where the fork re-converges. s = Solver() c1, c2, pp = Int('cert_hon'), Int('cert_alt'), Int('parentHash') injective_on(s, [((pp, digest_of(c1)), (pp, digest_of(c2)))]) s.add(Implies(digest_of(c1) == digest_of(c2), c1 == c2)) s.add(c1 != c2, hash_of(pp, digest_of(c1)) == hash_of(pp, digest_of(c2))) check("L0b R1 UNDER THE HASH: two anchors over the same parent with different certificates " "have different hashes (vanityData = digest(certificate) is in the hashed pre-image, so a " "known anchor hash pins its certificate)", s, kind="LEMMA") # NEG-CTRL for L0b: certificate OUTSIDE the hash (the pre-R1 design, and what a # stripped certificate looks like to a hash check alone): one hash, two certificates. s = Solver() injective_on(s, [((pp, body), (pp, body))]) s.add(c1 != c2, hash_of(pp, body) == hash_of(pp, body)) check("P0c NEG-CTRL: PLANT the certificate outside the hashed pre-image -> two anchors with " "different certificates share one hash (why R1 puts the digest under the hash)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # P1 -- BASELINE: honest seals exist only over honest blocks. Validator's K_eff = 7, # adversary with no post-quantum key, current regime (interval 32, K = 7). # ============================================================================= base = Rules(required=K, siblings=False) s = Solver(); F, Hp, H, a_last = history(s) s.add(base.accepted(s, F, Hp, 'p1a')) s.add(Hp - F + 1 > BOUND_BASE) check(f"P1a REWRITE BOUND, baseline (all F above {STAGE2_GRID_START}, all Hp): an accepted alternative " f"history replaces at most {BOUND_BASE} blocks (the latest anchor block + 31 after it)", s) s = Solver(); F, Hp, H, a_last = history(s) s.add(base.accepted(s, F, Hp, 'p1b'), Hp >= H) # at least as long as the honest chain: fork choice can take it s.add(F < a_last) check("P1b PREFIX KEPT, baseline (all F, Hp, H): an accepted alternative at least as long as the " "honest chain forks at or above the latest honest anchor: that anchor's PARENT and everything " "below it are kept", s) # non-vacuity: the 32-block witness exists (fork AT the latest anchor; its certificate is reused) s = Solver(); F, Hp, H, a_last = history(s) s.add(base.accepted(s, F, Hp, 'c1a'), is_anchor(F), a_last == F, Hp - F + 1 == BOUND_BASE, Hp >= H) check(f"C1a CONFIG witness: an accepted alternative of exactly {BOUND_BASE} blocks exists, forked " "AT the latest anchor height (the anchor's own certificate is over the honest parent and is " "reused: the anchor block is inside the exposed tail)", s, expect_unsat=False, kind="CONFIG") # ============================================================================= # N1 -- PLANTED: anchors need no certificate (K_eff = 0; the warm-up step 13014000:0 # and the dated step 17102384:0 of the real schedule are this rule at those heights). # ============================================================================= plant_k0 = Rules(required=0, siblings=False) s = Solver(); F, Hp, H, a_last = history(s) s.add(plant_k0.accepted(s, F, Hp, 'n1'), Hp - F + 1 == DEEP, Hp >= H) check(f"N1 NEG-CTRL: PLANT a rule that accepts anchors without a certificate (K_eff=0) -> an " f"alternative history {DEEP} blocks deep is accepted (the bound is unbounded; this is " "the real rule inside the dated K:0 steps)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # N2 -- the adversary ALSO holds every post-quantum key. # ============================================================================= adv_pq = Rules(required=K, siblings=False, adv_pq_keys=N) s = Solver(); F, Hp, H, a_last = history(s) s.add(adv_pq.accepted(s, F, Hp, 'n2'), Hp - F + 1 == DEEP, Hp >= H) check(f"N2 NEG-CTRL: give the adversary every post-quantum key -> an alternative history {DEEP} " "blocks deep is accepted (the anchor binds validator behaviour, it is no defence against " "a compromised set)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # P2 -- CORRECTED model (AIP-22 erratum 2026-10-01): honest seals may exist over an # undecided sibling of the honest block, which shares the honest parent (A3). # ============================================================================= corr = Rules(required=K, siblings=True) s = Solver(); F, Hp, H, a_last = history(s) s.add(corr.accepted(s, F, Hp, 'p2a')) s.add(Hp - F + 1 > BOUND_CORRECTED) check(f"P2a REWRITE BOUND, corrected (all F, Hp, all sibling seal counts): an accepted " f"alternative history replaces at most {BOUND_CORRECTED} blocks (the latest anchor's " "parent, replaced by its sealed sibling, the anchor block, and 31 after it)", s) s = Solver(); F, Hp, H, a_last = history(s) s.add(corr.accepted(s, F, Hp, 'p2b'), Hp >= H) s.add(F < a_last - 1) check("P2b PREFIX KEPT, corrected (all F, Hp, H): an accepted alternative at least as long as the " "honest chain forks at or above the latest anchor's PARENT: the anchor's GRANDPARENT and " "everything below it are kept (the block both siblings share)", s) # the exception is real in the model: the 33-block witness exists when the sibling was sealed by >= K, # and it forks exactly at the latest honest anchor's PARENT (a_last = F + 1), as the text says s = Solver(); F, Hp, H, a_last = history(s) s.add(corr.accepted(s, F, Hp, 'c1b'), is_anchor(F + 1), a_last == F + 1, Hp - F + 1 == BOUND_CORRECTED, Hp >= H, honest_over_sibling(F) >= K) check(f"C1b CONFIG witness: with a sibling of the latest anchor's parent sealed by >= K honest " f"validators, an accepted alternative of exactly {BOUND_CORRECTED} blocks exists, forked at that " "parent's height (the exception moves the bound by exactly one block)", s, expect_unsat=False, kind="CONFIG") # and it is exactly the sibling seals that buy that block: with fewer than K of them, 33 is impossible s = Solver(); F, Hp, H, a_last = history(s) s.add(corr.accepted(s, F, Hp, 'p2c'), Hp - F + 1 > BOUND_BASE) s.add(honest_over_sibling(F) < K) # the only height at which a sibling can enter the history is F check(f"P2c THE EXTRA BLOCK NEEDS K_eff SIBLING SEALS (all F, Hp): with fewer than K_eff={K} honest seals over " f"the sibling at the fork height, the corrected model gives the baseline bound {BOUND_BASE} again", s) # ============================================================================= # N3 -- PLANTED: drop the common-grandparent fact (a sealed "sibling" over ANY parent). # ============================================================================= no_gp = Rules(required=K, siblings=True, any_parent=True) s = Solver(); F, Hp, H, a_last = history(s) s.add(no_gp.accepted(s, F, Hp, 'n3'), Hp - F + 1 == DEEP, Hp >= H) check(f"N3 NEG-CTRL: PLANT siblings that may extend ANY parent (no common grandparent, A3 dropped) -> an " f"alternative history {DEEP} blocks deep is accepted (the one-block limit of the exception " "rests on the sibling sharing the honest parent)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # P4 -- PARTIAL post-quantum compromise against a validator (K_eff = 7): the bound is # a function of (K_eff, j): bounded iff j < K_eff. This is what K = 7 buys. # ============================================================================= part = Rules(required=K, siblings=True, adv_pq_keys=K - 1) s = Solver(); F, Hp, H, a_last = history(s) s.add(part.accepted(s, F, Hp, 'p4a'), Hp - F + 1 > BOUND_CORRECTED) check(f"P4a PARTIAL COMPROMISE (K_eff={K}, j={K - 1} post-quantum keys, siblings allowed): the bound is " f"still {BOUND_CORRECTED} (fewer than K_eff distinct post-quantum keys cannot certify an alternative parent)", s) s = Solver(); F, Hp, H, a_last = history(s) s.add(part.accepted(s, F, Hp, 'p4b'), Hp - F + 1 > BOUND_BASE) s.add(honest_over_sibling(F) + (K - 1) < K) # the extra block needs K_eff - j honest sibling seals check(f"P4b PARTIAL COMPROMISE: with j={K - 1} keys the extra block needs K_eff - j = {K - (K - 1)} honest " f"sibling seal(s); with fewer, the bound is {BOUND_BASE} again", s) all_k = Rules(required=K, siblings=False, adv_pq_keys=K) s = Solver(); F, Hp, H, a_last = history(s) s.add(all_k.accepted(s, F, Hp, 'n4a'), Hp - F + 1 == DEEP, Hp >= H) check(f"N4a NEG-CTRL: j = K_eff = {K} post-quantum keys of distinct validators -> an alternative history " f"{DEEP} blocks deep is accepted (the threshold is exactly the number of keys that breaks it)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # P5 -- the PUBLISHED from-genesis FOLLOWER: aere.pq.anchor.minSealsCeiling=1 -> K_eff = 1 # (SPEC 6.4). The honest chain's anchors still carry >= K seals (A1 at the chain's K). # ============================================================================= fol = Rules(required=K_FOLLOWER, siblings=False, honest_floor=K) fol_corr = Rules(required=K_FOLLOWER, siblings=True, honest_floor=K) s = Solver(); F, Hp, H, a_last = history(s) s.add(fol.accepted(s, F, Hp, 'p5a'), Hp - F + 1 > BOUND_BASE) check(f"P5a FOLLOWER (K_eff={K_FOLLOWER}, no post-quantum key): the baseline bound {BOUND_BASE} holds " "(one seal the adversary cannot make is enough)", s) s = Solver(); F, Hp, H, a_last = history(s) s.add(fol_corr.accepted(s, F, Hp, 'p5b'), Hp - F + 1 > BOUND_CORRECTED) check(f"P5b FOLLOWER (K_eff={K_FOLLOWER}, siblings allowed): the corrected bound {BOUND_CORRECTED} holds", s) s = Solver(); F, Hp, H, a_last = history(s) s.add(fol_corr.accepted(s, F, Hp, 'c5c'), is_anchor(F + 1), a_last == F + 1, Hp - F + 1 == BOUND_CORRECTED, Hp >= H, honest_over_sibling(F) == 1) check(f"C5c CONFIG witness, FOLLOWER: ONE honest seal over the sibling buys the {BOUND_CORRECTED}rd block " f"(a validator at K_eff={K} needs {K}: P2c)", s, expect_unsat=False, kind="CONFIG") fol_leak = Rules(required=K_FOLLOWER, siblings=False, adv_pq_keys=1, honest_floor=K) s = Solver(); F, Hp, H, a_last = history(s) s.add(fol_leak.accepted(s, F, Hp, 'n5d'), Hp - F + 1 == DEEP, Hp >= H) check(f"N5d NEG-CTRL, FOLLOWER: ONE leaked post-quantum key -> an alternative history {DEEP} blocks deep " f"is accepted by a node at K_eff={K_FOLLOWER} (the ceiling is a real weakening of the follower, SPEC 6.4)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # P6 -- the dated 128-INTERVAL window (blocks 17,225,968 .. 20,746,736; 2026-09-05 .. # 2026-09-29): the same two bounds, 128 and 129, for ANY K_eff >= 1 in force then # (the predicate at K_eff = 1 accepts every history a larger K_eff accepts). # ============================================================================= win = Rules(required=1, siblings=False, interval=INTERVAL_128) win_corr = Rules(required=1, siblings=True, interval=INTERVAL_128) s = Solver(); F, Hp, H, a_last = history(s, interval=INTERVAL_128, f_above=WINDOW_128[0], hp_below=WINDOW_128[1]) s.add(win.accepted(s, F, Hp, 'p6a'), Hp - F + 1 > BOUND_BASE_128) check(f"P6a DATED 128-INTERVAL WINDOW, baseline (any K_eff >= 1): at most {BOUND_BASE_128} blocks " "(the anchor block + 127 after it)", s) s = Solver(); F, Hp, H, a_last = history(s, interval=INTERVAL_128, f_above=WINDOW_128[0], hp_below=WINDOW_128[1]) s.add(win_corr.accepted(s, F, Hp, 'p6b'), Hp - F + 1 > BOUND_CORR_128) check(f"P6b DATED 128-INTERVAL WINDOW, corrected: at most {BOUND_CORR_128} blocks", s) s = Solver(); F, Hp, H, a_last = history(s, interval=INTERVAL_128, f_above=WINDOW_128[0], hp_below=WINDOW_128[1]) s.add(win.accepted(s, F, Hp, 'c6c'), is_anchor(F, INTERVAL_128), a_last == F, Hp - F + 1 == BOUND_BASE_128, Hp >= H) check(f"C6c CONFIG witness, 128 window: an accepted alternative of exactly {BOUND_BASE_128} blocks exists", s, expect_unsat=False, kind="CONFIG") # ============================================================================= # P3 -- a node with a reference: it knows (a_ref, hash of the honest anchor a_ref). # It treats a history as canonical only if the history reaches a_ref with that # very hash. ENCODED as the hash chain itself: honest and alternative block hashes # at every height, each the hash of (parent hash, body); the fork is a different # hash at F; the reference check is hash equality at a_ref = F + d. Unrolled for # W_REF heights above the fork (the induction step is L0a). # ============================================================================= h_hon, h_alt = Function('h_hon', IntSort(), IntSort()), Function('h_alt', IntSort(), IntSort()) b_hon, b_alt = Function('b_hon', IntSort(), IntSort()), Function('b_alt', IntSort(), IntSort()) def hash_chain(s, F, covers_parent=True): """Both chains above the fork, with injectivity instantiated per height.""" for i in range(1, W_REF + 1): if covers_parent: s.add(h_hon(F + i) == hash_of(h_hon(F + i - 1), b_hon(F + i))) s.add(h_alt(F + i) == hash_of(h_alt(F + i - 1), b_alt(F + i))) injective_on(s, [((h_hon(F + i - 1), b_hon(F + i)), (h_alt(F + i - 1), b_alt(F + i)))]) else: # PLANTED: the hash covers the body only s.add(h_hon(F + i) == hash_body(b_hon(F + i))) s.add(h_alt(F + i) == hash_body(b_alt(F + i))) s = Solver() F, d = Int('F'), Int('d') s.add(F > ANCHOR_START, d >= 0, d <= W_REF) s.add(h_alt(F) != h_hon(F)) # the fork: a different block at F hash_chain(s, F) s.add(Or([And(d == i, h_alt(F + i) == h_hon(F + i)) for i in range(W_REF + 1)])) # reference reached with the honest hash check(f"P3a REFERENCE (all F, all a_ref = F + d, 0 <= d <= {W_REF}): a history that diverges at or below " "the reference anchor cannot reach it with the honest hash, because every hash above the fork " "differs (the hash chain pins the prefix through a_ref, certificates included by L0b)", s) s = Solver() F, d = Int('F'), Int('d') s.add(F > ANCHOR_START, d >= 1, d <= W_REF) s.add(h_alt(F) != h_hon(F)) hash_chain(s, F, covers_parent=False) s.add(Or([And(d == i, h_alt(F + i) == h_hon(F + i)) for i in range(1, W_REF + 1)])) check("N3a NEG-CTRL: PLANT a block hash that does not cover the parent hash -> a history that diverged " "below the reference re-converges to the honest hash at a_ref (the reference would pin nothing)", s, expect_unsat=False, kind="NEG-CTRL") # with the reference (F > a_ref by P3a), even a LONGER alternative (fork choice would take it) # keeps everything through a_ref and is bounded by the corrected bound above its fork point s = Solver(); F, Hp, H, a_last = history(s) a_ref = Int('a_ref') s.add(is_anchor(a_ref), a_ref <= H) s.add(corr.accepted(s, F, Hp, 'p3b'), Hp >= a_ref, a_ref < F, Hp >= H) s.add(Or(F <= a_ref, Hp - F + 1 > BOUND_CORRECTED)) check("P3b REFERENCE + BOUND: with a reference anchor (which forces F > a_ref, P3a), every accepted " f"history keeps everything through a_ref and replaces at most {BOUND_CORRECTED} blocks above its fork point", s) # NEG-CTRL for P3: a node WITHOUT a reference (syncs with no checkpoint) accepts a multi-block # history that diverges at or below an anchor, as long as it stops before the next anchor it # cannot certify; with no honest head to compare against, it cannot tell the history is short. s = Solver(); F, Hp, H, a_last = history(s) a_ref = Int('a_ref') s.add(is_anchor(a_ref), a_ref <= H) s.add(corr.accepted(s, F, Hp, 'p3c'), F <= a_ref, Hp - F + 1 >= 2) # no reference check at all check("P3c NEG-CTRL: a node with NO reference point accepts a (short) history that diverges at or below an " "anchor it never heard of (weak subjectivity: the published rule gives a syncing node a " "recent anchor out of band, aere.pq.checkpoint)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # D1 -- why the exception needs ALL classical keys today, and not after stage 5. # An arithmetic restatement of Q = 7 (no negative control; not counted as a proof). # ============================================================================= keys = Int('classical_keys_held') s = Solver() s.add(keys >= 0, keys <= N, keys < Q) s.add(keys >= Q) # "can forge the ECDSA commit quorum of one round" check(f"D1 DEFN (below AIP-22 stage 5): forging a header needs the ECDSA commit quorum, " f"Q={Q} distinct keys; a holder of fewer than Q (a single validator holds 1) cannot; " f"the adversary modelled here holds {N} and can", s, kind="DEFN") # ============================================================================= print("\n=== SUMMARY (anchor REWRITE BOUND, round-free seal model) ===") allok = True by_kind = {} for name, tag, ok, kind, dt in results: print(f" {tag:9} [{kind:8}] {dt:6.3f}s {name}") allok = allok and ok by_kind[kind] = by_kind.get(kind, 0) + 1 print() print(" checks by kind: " + ", ".join(f"{k} {v}" for k, v in sorted(by_kind.items()))) if PLANT_BOUNDS: print(" --plant-bounds: the result above is the control of the control; it must NOT be fully established.") if allok: print(" PROVED: against an adversary holding every classical validator key and fewer") print(f" than K_eff post-quantum keys, a node enforcing R2 (K_eff distinct valid seals of") print(" the parent's validators over the round-free M(parent)), the grid and the hash") print(f" chain accepts no alternative history that replaces more than {BOUND_BASE} blocks:") print(" the latest anchor block itself (its certificate is over the honest parent and is") print(" reusable) and the 31 blocks after it; the latest anchor's parent and everything") print(" below it are kept. Under the CORRECTED model (seals carry no round, so an") print(f" undecided sibling of the anchor's parent may carry honest seals) the bound is {BOUND_CORRECTED}:") print(" the parent can be replaced by its sealed sibling, and no more, because the") print(" sibling shares the honest grandparent (A3); the grandparent and everything") print(" below it are kept. The extra block costs K_eff - j honest sibling seals: 7 on a") print(" validator, 1 on the published follower (K_eff = 1). A node that knows one honest") print(" anchor hash accepts no divergence at or below it. Every guard is load-bearing:") print(" anchors without certificates (N1), an adversary with every post-quantum key (N2)") print(" or with K_eff of them (N4a, one on the follower: N5d), siblings over arbitrary") print(" parents (N3), a hash that does not cover the parent (N3a) and a certificate") print(" outside the hash (P0c) each break the claim (SAT). Inside the dated 128-interval") print(f" window the bounds are {BOUND_BASE_128} / {BOUND_CORR_128}.") print(" BOUNDARY: acceptance combinatorics over heights; not the seal-counting rule") print(" (anchor_blocking_quorum_smt.py), not cryptography, not delivery, not a node") print(" syncing with no reference, not heights inside the dated K:0 / disarmed windows,") print(" not a node whose registry epochs come over a classical channel, not the client") print(" code of either implementation; QBFT safety while the honest history was produced") print(" is assumed (A3).") else: print(" NOT fully established (see FAILED / unexpected result above).") sys.exit(0 if allok else 1) # ----------------------------------------------------------------------------- # MEASURED 2026-10-07, second form (Windows, python 3.14.4, z3 4.16.0): # the measured output is in anchor_rewrite_bound_roundfree_smt.RESULT.txt next to this file # (written by the same run, dated). The first form of the same day, reviewed adversarially # the same day, had: P3a as an arithmetic tautology (the conclusion `a_ref < F` added as a # premise), C1c (now D1) counted among the proofs, K = 7 and R1 named as what the bound # rests on although planting K = 1 or removing R1 left every bound proof PROVED, no # statement for the published follower's K_eff = 1 nor for a partial post-quantum # compromise, and the fork point allowed inside the dated 128-interval window with the # 32-grid applied there (where the real rule certifies every 128th block only). Each of # those is addressed above: P3a is now the unrolled hash chain with its own negative # control (N3a), D1 is labelled DEFN and not counted, P4/N4a and P5/N5d make K_eff and j # explicit, P6 is the dated window, and the headline histories are confined to the # regime in force today (F above 20,746,736). # -----------------------------------------------------------------------------