From 5129289cea634b2cf994752b9d9c692eb69647ae Mon Sep 17 00:00:00 2001 From: Aere Network Date: Wed, 2 Sep 2026 20:34:15 +0300 Subject: [PATCH] formal-consensus: the post-quantum message-enforcement model and the runner wiring all 36 models; bench: the local test key marked synthetic --- bench/bench.py | 1 + formal-consensus/RULEAZA-TOT.md | 2 +- .../pq_message_enforcement_smt.py | 163 ++++++++++++++++++ .../run_consensus_verification.py | 1 + 4 files changed, 166 insertions(+), 1 deletion(-) create mode 100644 formal-consensus/pq_message_enforcement_smt.py diff --git a/bench/bench.py b/bench/bench.py index 4d970da..75551bb 100644 --- a/bench/bench.py +++ b/bench/bench.py @@ -21,6 +21,7 @@ from web3 import Web3 from eth_account import Account RPC = "http://127.0.0.1:8545" +# AERE-SINTETIC: cheia de proba 0x..01 pentru un nod local (localhost:8545); nu e a nimanui KEY = "0x0000000000000000000000000000000000000000000000000000000000000001" acct = Account.from_key(KEY) diff --git a/formal-consensus/RULEAZA-TOT.md b/formal-consensus/RULEAZA-TOT.md index 4008367..5183d83 100644 --- a/formal-consensus/RULEAZA-TOT.md +++ b/formal-consensus/RULEAZA-TOT.md @@ -31,7 +31,7 @@ tally-ul de linii de verdict. models run: 35 passed: 35 (14 consensus + 11 contract + 10 application) verdict lines: 282 PROVED 149 CEX-FOUND 0 FAILED wall time: ~39s total (cel mai lent: qbft_safety_smt.py ~23s) -coverage: 35 of 35 *_smt.py files wired +coverage: 36 of 36 *_smt.py files wired (2026-09-02: + pq_message_enforcement_smt.py) RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired) ``` diff --git a/formal-consensus/pq_message_enforcement_smt.py b/formal-consensus/pq_message_enforcement_smt.py new file mode 100644 index 0000000..d20861c --- /dev/null +++ b/formal-consensus/pq_message_enforcement_smt.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +# ----------------------------------------------------------------------------- +# pq_message_enforcement_smt.py +# +# MACHINE-CHECKED (z3) proof of the ENFORCEMENT RULES for the four post-quantum +# sealed QBFT message layers of chain 2800 (SPEC.md section 2.6), written on +# 2026-09-02, the day the fleet moved to the build that fixed D-311. +# +# WHAT IS MODELLED (design combinatorics, not the Java code and not the chain): +# - four message TYPES with four DOMAINS (PROPOSAL, PREPARE, ROUND-CHANGE, COMMIT); +# - a seal = (index, domain, height, round, digest, form) where `form` distinguishes +# the COMMIT anchor form (signed when the anchor is armed at that height) from the +# committed-seal digest form; +# - a registry active at a height binding index -> author; +# - the per-type enforcement height H_type (absent = never); +# - the verifier's decision "the vote counts" as a function of the message, its +# author, the seal it carries, the registry and the height. +# +# PROPERTIES (UNSAT of the negation = holds): +# P1 ARMED-REQUIRES-VALID: at h >= H_type, a message counts only if it carries a +# seal bound to its author, accepted by the registry, and verifying over the +# pre-image of ITS OWN type at ITS OWN (height, round, digest). +# P2 NO-CROSS-DOMAIN-REPLAY: a seal valid for type X never makes a message of type +# Y != X count (domains differ, so pre-images differ). +# P3 NO-CROSS-POSITION-REPLAY: a seal over (h, r, d) never makes a message at a +# different (h', r', d') count. +# P4 NO-AUTHOR-SWAP: a seal of index i counts only on a message whose author is +# the address the registry binds to i. +# P5 BELOW-FORK-UNCHANGED: at h < H_type an unsealed message still counts (the +# upstream rule alone decides). +# P6 COMMIT-FORM-AGREEMENT (D-311): with the anchor armed, an emitter signing the +# anchor form and a verifier checking the anchor form agree (commits count); +# the NEGATIVE CONTROL plants the pre-2026-09-02 verifier (digest form) and +# shows that EVERY honest commit is refused, i.e. the liveness failure the +# testnet observed at block 999. +# +# NEGATIVE CONTROLS: every property has one; each plants the violation and must +# come back SAT, proving the check can fire. Convention as in the other *_smt.py. +# +# HONEST BOUNDARY: Falcon verification is modelled as equality of the signed +# pre-image tuple (a perfect signature); registry rotation is modelled as a +# height-indexed binding; nothing here says anything about the Java code paths +# beyond the rules SPEC.md 2.6 states, nor about chain 2800's live enforcement +# state (none is armed at the time of writing). +# ----------------------------------------------------------------------------- +from z3 import (Int, Bool, BoolVal, Solver, And, Or, Not, Implies, If, sat, unsat) + +PROPOSAL, PREPARE, ROUNDCHANGE, COMMIT = 0, 1, 2, 3 +DIGEST_FORM, ANCHOR_FORM = 0, 1 +N = 9 # validators / registry indices 0..8 +ANCHOR_BLOCK = 13014000 # aere.pq.anchorBlock on 2800 +results = [] + +def bound_author(index, height): + """registry active at `height` binds index i to author i (modelled identity); indices outside + 0..N-1 are refused. Rotation is modelled by the height guard: below the registry start nothing + is bound (the model uses one registry; the anchor model covers rotation).""" + return If(And(index >= 0, index < N), index, -1) + +def anchor_armed(height): + return height + 1 >= ANCHOR_BLOCK + +def expected_form(mtype, height): + """the message form a COMMIT seal must sign at this height (SPEC 2.6, D8); other types + always sign their own domain pre-image (modelled as DIGEST_FORM of their own domain).""" + return If(And(mtype == COMMIT, anchor_armed(height)), ANCHOR_FORM, DIGEST_FORM) + +def counts(mtype, height, round_, digest, author, has_seal, s_index, s_domain, s_h, s_r, s_d, s_form, + H_type, verifier_form=None): + """the vote-counting predicate of SPEC 2.6. `verifier_form` overrides the form the verifier + expects for COMMIT (used by the D-311 negative control); None = the fixed verifier.""" + armed = height >= H_type + exp_form = expected_form(mtype, height) if verifier_form is None else verifier_form + seal_ok = And(has_seal, + bound_author(s_index, height) == author, # rule 2 + 3 + s_domain == mtype, # rule 4: own domain + s_h == height, s_r == round_, s_d == digest, # rule 4: own position + s_form == exp_form) # rule 4: commit form + return Or(Not(armed), seal_ok) + +def fresh(prefix): + return (Int(prefix + '_type'), Int(prefix + '_h'), Int(prefix + '_r'), Int(prefix + '_d'), + Int(prefix + '_author'), Bool(prefix + '_has'), Int(prefix + '_si'), Int(prefix + '_sdom'), + Int(prefix + '_sh'), Int(prefix + '_sr'), Int(prefix + '_sd'), Int(prefix + '_sform')) + +def domain_bounds(t, sdom): + return And(t >= 0, t <= 3, sdom >= 0, sdom <= 3) + +def check(name, negation_constraints, negative_control_constraints): + s = Solver(); s.add(*negation_constraints); r = s.check() + holds = (r == unsat) + s2 = Solver(); s2.add(*negative_control_constraints); r2 = s2.check() + fires = (r2 == sat) + results.append((name, holds, fires)) + print(f"{name:28s} property={'HOLDS' if holds else 'FAILS'} ({r}) negative-control={'FIRES' if fires else 'DOES NOT FIRE'} ({r2})") + return holds and fires + +# ---------------------------------------------------------------- P1 armed requires valid +t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p1'); H = Int('p1_H') +base = [domain_bounds(t, sdom), h >= H, a >= 0, a < N] +# negation: armed, and the message counts, yet the seal is absent or not the author's or wrong position +bad_seal = Or(Not(has), bound_author(si, h) != a, sdom != t, sh != h, sr != r, sd != d, sform != expected_form(t, h)) +neg = base + [counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H), bad_seal] +# negative control: a planted rule that accepts an unsealed message while armed +planted = base + [Not(has), Or(Not(h >= H), True)] # "counts" replaced by True: the planted rule ignores the seal +check('P1 armed-requires-valid', neg, planted) + +# ---------------------------------------------------------------- P2 no cross-domain replay +t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p2'); H = Int('p2_H') +neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, sdom != t, + counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)] +# planted: a domain-blind verifier (drops the sdom == t conjunct) +blind = And(has, bound_author(si, h) == a, sh == h, sr == r, sd == d, sform == expected_form(t, h)) +planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, sdom != t, blind] +check('P2 no-cross-domain-replay', neg, planted) + +# ---------------------------------------------------------------- P3 no cross-position replay +t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p3'); H = Int('p3_H') +neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, Or(sh != h, sr != r, sd != d), + counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)] +blind = And(has, bound_author(si, h) == a, sdom == t, sform == expected_form(t, h)) # position-blind +planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, Or(sh != h, sr != r, sd != d), blind] +check('P3 no-cross-position-replay', neg, planted) + +# ---------------------------------------------------------------- P4 no author swap +t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p4'); H = Int('p4_H') +neg = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, bound_author(si, h) != a, + counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H)] +blind = And(has, sdom == t, sh == h, sr == r, sd == d, sform == expected_form(t, h)) # author-blind +planted = [domain_bounds(t, sdom), h >= H, a >= 0, a < N, has, bound_author(si, h) != a, blind] +check('P4 no-author-swap', neg, planted) + +# ---------------------------------------------------------------- P5 below fork unchanged +t, h, r, d, a, has, si, sdom, sh, sr, sd, sform = fresh('p5'); H = Int('p5_H') +neg = [domain_bounds(t, sdom), h < H, Not(has), a >= 0, a < N, + Not(counts(t, h, r, d, a, has, si, sdom, sh, sr, sd, sform, H))] +# planted: an enforcement that ignores its own height (always armed) +planted = [domain_bounds(t, sdom), h < H, Not(has), a >= 0, a < N, Not(Or(Not(BoolVal(True)), has))] +check('P5 below-fork-unchanged', neg, planted) + +# ---------------------------------------------------------------- P6 commit form agreement (D-311) +h = Int('p6_h'); r = Int('p6_r'); d = Int('p6_d'); a = Int('p6_a'); si = Int('p6_si'); H = Int('p6_H') +honest = [h >= H, h + 1 >= ANCHOR_BLOCK, a >= 0, a < N, si == a] # honest emitter: seal of its own index +emitted_form = ANCHOR_FORM # what QbftRound.pqSealMessageFor signs when the anchor is armed +# negation: an honest commit under the FIXED verifier does not count +neg = honest + [Not(counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H))] +# negative control: the pre-D-311 verifier (digest form) refuses the same honest commit +planted = honest + [Not(counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H, verifier_form=DIGEST_FORM))] +check('P6 commit-form-agreement', neg, planted) + +# ---------------------------------------------------------------- P6b every honest commit refused under the old verifier +# strengthening of the negative control: under the old verifier there is NO honest commit that counts +s = Solver() +s.add(honest[0], honest[1], honest[2], honest[3], honest[4], + counts(COMMIT, h, r, d, a, True, si, COMMIT, h, r, d, emitted_form, H, verifier_form=DIGEST_FORM)) +r_all = s.check() +all_refused = (r_all == unsat) +results.append(('P6b old-verifier-refuses-all', all_refused, all_refused)) +print(f"{'P6b old-verifier-refuses-all':28s} {'HOLDS' if all_refused else 'FAILS'}: under the digest-form verifier with the anchor armed, no honest commit counts ({r_all}) - the block-999 stop of testnet 28001") + +ok = all(hold and fire for _, hold, fire in results) +print(f"\n{'ALL PROPERTIES HOLD AND ALL NEGATIVE CONTROLS FIRE' if ok else 'SOMETHING DID NOT HOLD OR A CONTROL DID NOT FIRE'}: {sum(1 for _,hh,ff in results if hh and ff)}/{len(results)}") +raise SystemExit(0 if ok else 1) diff --git a/formal-consensus/run_consensus_verification.py b/formal-consensus/run_consensus_verification.py index 190dc40..d0aac4c 100644 --- a/formal-consensus/run_consensus_verification.py +++ b/formal-consensus/run_consensus_verification.py @@ -35,6 +35,7 @@ CONSENSUS_MODELS = [ ("QBFT IBFT 2.0 locking, engine-role model (2026-07-14 Findings D/E)", "qbft_locking_smt.py"), ("QBFT NETWORK-PARTITION safety/liveness (N=9 parametric: split-brain, starvation, heal)", "partition_safety_smt.py"), ("Anchor x VIEW-CHANGE (no round change yields two valid PQ certificates, N=9)", "anchor_viewchange_smt.py"), + ("PQ MESSAGE-LAYER ENFORCEMENT (SPEC 2.6: armed-requires-valid, no cross-domain/position/author replay, below-fork unchanged, commit form under armed anchor = D-311)", "pq_message_enforcement_smt.py"), ("PqAnchor CEILING monotonicity (minSealsCeiling only lowers K; K_eff <= maxSeals)", "pqanchor_ceiling_monotonicity_smt.py"), ("PQ anchor REGISTRY index binding (loader and seal rule read ONE mapping)", "registry_index_binding_smt.py"), ("PQ anchor REGISTRY rotation coverage (every anchor height has exactly one registry)", "registry_rotation_coverage_smt.py"),