diff --git a/formal-consensus/registry_index_binding_smt.py b/formal-consensus/registry_index_binding_smt.py new file mode 100644 index 0000000..1ddc9f7 --- /dev/null +++ b/formal-consensus/registry_index_binding_smt.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Registry index binding: the seal rule and the registry loader must read ONE mapping. + +Motivated by a real defect found 2026-08-15 by a from-genesis import proof: a node built from +the public patch set bound the 7-key registry correctly at height 13,014,000 (the loader saw +key index 0), yet its seal-validation rule rejected the first real anchor certificate saying +"index 0 is unbound". Two code paths derived the index->address mapping from the same registry +file and disagreed. Production accepts the same block, so the divergence is between the two +paths, not in the data. + +This model states the property those paths must satisfy, and shows exactly what breaks when +they do not: + + P1 (agreement): for every index i in [0, n), loader_binds(i) == rule_binds(i). + P2 (fail-closed under agreement): if the shared mapping binds no address to an index carried + by a certificate, the certificate is rejected (an unbound index never validates). + P3 (the two failure modes when P1 is broken): + a) rule sees FEWER indices than the loader -> a VALID certificate is rejected + (liveness loss: the honest chain stops importing, the defect found today), and + b) rule sees MORE indices than the loader -> a certificate carrying an index the + registry never vouched for can validate (safety loss: worse, and silent). + +Encoding: mappings are uninterpreted functions Index -> Address, Address 0 means unbound. +UNSAT of the negated property = the property holds. Each proof has a negative control that +plants the divergence and must come back SAT (the solver exhibits the bad world), otherwise +the proof proves nothing. +""" +import sys +from z3 import (Solver, Function, IntSort, BitVecSort, BitVecVal, Int, BitVec, + And, Or, Not, Implies, ForAll, Exists, sat, unsat) + +ADDR = BitVecSort(64) # abstracted addresses; 0 = unbound +N = 9 # indices 0..8, the live set size + +def fresh_solver(): + s = Solver() + s.set("timeout", 60000) + return s + +results = [] + +def record(name, expect, got): + ok = (expect == got) + results.append((name, expect, got, ok)) + print(f" {name}: expected {expect}, got {got} -> {'OK' if ok else 'BROKEN'}") + return ok + +print("Registry index binding, SMT model (z3)") +print(f"set size n={N}, Address 0 = unbound\n") + +loader = Function('loader_binds', IntSort(), ADDR) +rule = Function('rule_binds', IntSort(), ADDR) +i = Int('i') +cert_idx = Int('cert_idx') + +in_range = lambda x: And(x >= 0, x < N) + +# ---- P1+P2: under agreement, an unbound index never validates ------------------------------ +# validates(cert_idx) is modeled as: the rule binds cert_idx to a nonzero address. +# Property: agreement AND loader leaves cert_idx unbound => the rule rejects it. +print("P2 under P1: with one shared mapping, an unbound index can never validate") +s = fresh_solver() +s.add(ForAll([i], Implies(in_range(i), loader(i) == rule(i)))) # P1 assumed +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) == BitVecVal(0, 64)) # registry does not vouch +s.add(rule(cert_idx) != BitVecVal(0, 64)) # ...but the rule validates +record("P2-holds (negation UNSAT)", "unsat", str(s.check())) + +# negative control: drop the agreement assumption and the bad world must exist +s = fresh_solver() +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) == BitVecVal(0, 64)) +s.add(rule(cert_idx) != BitVecVal(0, 64)) +record("P2-control (no agreement, bad world SAT)", "sat", str(s.check())) + +# ---- P3a: rule sees fewer -> valid certificate rejected (today's defect) ------------------- +print("\nP3a: a rule that binds FEWER indices than the loader rejects a valid certificate") +s = fresh_solver() +# there is an index the loader vouches for that the rule does not +s.add(Exists([i], And(in_range(i), loader(i) != BitVecVal(0, 64), rule(i) == BitVecVal(0, 64)))) +# the certificate carries exactly such an index +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) != BitVecVal(0, 64)) +s.add(rule(cert_idx) == BitVecVal(0, 64)) +record("P3a-exhibited (divergent world SAT)", "sat", str(s.check())) +# and under P1 this world is impossible: +s = fresh_solver() +s.add(ForAll([i], Implies(in_range(i), loader(i) == rule(i)))) +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) != BitVecVal(0, 64)) +s.add(rule(cert_idx) == BitVecVal(0, 64)) +record("P3a-impossible-under-P1 (UNSAT)", "unsat", str(s.check())) + +# ---- P3b: rule sees more -> unvouched index validates (the silent, worse direction) -------- +print("\nP3b: a rule that binds MORE indices than the loader validates an unvouched index") +s = fresh_solver() +s.add(Exists([i], And(in_range(i), loader(i) == BitVecVal(0, 64), rule(i) != BitVecVal(0, 64)))) +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) == BitVecVal(0, 64)) +s.add(rule(cert_idx) != BitVecVal(0, 64)) +record("P3b-exhibited (divergent world SAT)", "sat", str(s.check())) +s = fresh_solver() +s.add(ForAll([i], Implies(in_range(i), loader(i) == rule(i)))) +s.add(in_range(cert_idx)) +s.add(loader(cert_idx) == BitVecVal(0, 64)) +s.add(rule(cert_idx) != BitVecVal(0, 64)) +record("P3b-impossible-under-P1 (UNSAT)", "unsat", str(s.check())) + +# ---- verdict ------------------------------------------------------------------------------- +print() +bad = [r for r in results if not r[3]] +if bad: + print("RESULT: MODEL BROKEN, " + ", ".join(r[0] for r in bad)) + sys.exit(1) +print("RESULT: PROVED. One shared index->address mapping makes 'unbound never validates' a") +print("theorem, and BOTH divergence directions (valid-rejected, the defect measured on") +print("2026-08-15, and unvouched-accepted, the silent one) are exhibited by the solver and") +print("proven impossible under agreement. The engineering consequence: the loader and the") +print("seal rule must call one function, not two implementations of the same idea.") +sys.exit(0)