formal-consensus: carry the 2026-08-12 fix into falcon_blocking (the old block proved a constant, not the property)

formal-consensus/falcon_blocking_smt.py

@@ -121,12 +121,47 @@ s.add(N - f < q)                                    # negate: honest+correct bel
 check("B-LIVENESS (all N): honest+correct set N-f >= quorum(N) -> a cert can always form", s)
 
 # per-N witness that the honest set alone certifies (non-vacuous, config theorem)
-for N in (4, 5, 7):
-    ok = (N - faultbound(N)) >= quorum(N)
-    s = Solver(); s.add(Int('dummy') == (0 if ok else 1)); s.add(Int('dummy') == 0)
-    check(f"B-LIVENESS N={N}: N-f={N-faultbound(N)} >= quorum={quorum(N)} "
-          f"(honest+correct alone forms the Falcon cert)", s,
-          expect_unsat=not ok, kind="CONFIG")
+#
+# FIXED 2026-08-12. This block used to read:
+#
+#     ok = (N - faultbound(N)) >= quorum(N)
+#     s = Solver(); s.add(Int('dummy') == (0 if ok else 1)); s.add(Int('dummy') == 0)
+#     check(..., s, expect_unsat=not ok, kind="CONFIG")
+#
+# which never asked the solver anything. The verdict `ok` was computed in Python and then used BOTH
+# to build the constraint AND to choose the expected answer, so it passed on either branch: with
+# ok=True the solver saw d==0 AND d==0 (sat, expected sat); with ok=False it saw d==1 AND d==0
+# (unsat, expected unsat). If quorum() or faultbound() were wrong in Python, this still printed
+# PROVED. A check that cannot distinguish the two cases measures nothing, however green it looks.
+#
+# Now z3 is given the property for each concrete N: q and f are constrained by their DEFINING
+# inequalities, exactly as in the unbounded theorem above, and the property is NEGATED. unsat means
+# no counterexample exists, i.e. the property holds. Python is no longer in the decision path; it
+# only names the expected numbers in the label, and those are cross-checked against the solver by
+# the accompanying NEG-CTRL below.
+for Nv in (4, 5, 7):
+    s = Solver()
+    q_, f_ = Int('q'), Int('f')
+    s.add(3 * q_ >= 2 * Nv, 3 * q_ <= 2 * Nv + 2)   # q = ceil(2N/3), as inequalities
+    s.add(3 * f_ <= Nv - 1, Nv - 1 <= 3 * f_ + 2)   # f = floor((N-1)/3)
+    s.add(Nv - f_ < q_)                              # negate the property
+    check(f"B-LIVENESS N={Nv}: N-f={Nv-faultbound(Nv)} >= quorum={quorum(Nv)} "
+          f"(honest+correct alone forms the Falcon cert)", s, kind="CONFIG")
+
+# NEG-CTRL for the block above: if the property were FALSE for some N, the same construction must
+# come back sat, i.e. produce a counterexample. We plant a strictly larger quorum requirement and
+# require the check to FIND one. Without this, the three unsats above could not be distinguished
+# from a solver that says unsat to everything.
+for Nv in (4,):
+    s = Solver()
+    q_, f_ = Int('q'), Int('f')
+    s.add(q_ == Nv)                                  # planted: quorum = N, impossible to meet with f>0
+    s.add(3 * f_ <= Nv - 1, Nv - 1 <= 3 * f_ + 2)
+    s.add(f_ >= 1)
+    s.add(Nv - f_ < q_)                              # same negation as above
+    check(f"NEG-CTRL B-LIVENESS N={Nv}: with quorum forced to N, the honest set does NOT suffice "
+          f"(proves the three checks above can come back sat)", s,
+          expect_unsat=False, kind="NEG-CTRL")
 
 # =============================================================================
 # THRESHOLD  -- WHY N>=7 is required to activate BLOCKING.