---------------------------- MODULE CAINPBFTCommitSafety ----------------------------
(***************************************************************************)
(* Bounded model of the CAIN-42 PBFT commit and view-change rules for ONE   *)
(* sequence number, N = 4 members, f = 1 Byzantine, quorum Q = 3, views 0  *)
(* and 1, two candidate values.                                            *)
(*                                                                         *)
(* It models the rules as implemented after the 2026-09-23 fix in          *)
(* platform-gateway/cain_pbft_engine_33.py:                                *)
(*   - an honest member PREPAREs only its view's leader proposal;          *)
(*   - it is PREPARED once a certificate exists (leader proposal + Q       *)
(*     distinct PREPARE signers), its own or adopted from a COMMIT;        *)
(*   - it signs COMMIT only when PREPARED (_become_prepared);              *)
(*   - it executes only when PREPARED and Q distinct COMMIT signers exist   *)
(*     for the same (view, value) (_try_commit_local);                     *)
(*   - on view change it reports its prepared certificates; the new        *)
(*     primary re-proposes the value of the highest-view certificate       *)
(*     reported in a quorum of VIEW_CHANGEs, else any value (null).         *)
(* A Byzantine member signs anything, for any view and value, at any time;  *)
(* it cannot forge an honest signature, so a certificate exists only when   *)
(* enough real signatures exist.                                            *)
(*                                                                         *)
(* OldRule = TRUE models the pre-fix rule "a verified prepared certificate *)
(* is enough to execute" (OMEGA-03). IgnoreReports = TRUE models a new      *)
(* primary that does not honour reported certificates. Both are mutants    *)
(* that MUST violate Agreement, or a pass means nothing.                   *)
(*                                                                         *)
(* Scope: a bounded MODEL, not the Python code. One sequence, two views.   *)
(***************************************************************************)
EXTENDS FiniteSets, Naturals

CONSTANTS Byz, OldRule, IgnoreReports

Nodes  == {"n1", "n2", "n3", "n4"}
Honest == Nodes \ Byz
Views  == {0, 1}
Values == {"X", "Y"}
None   == "none"
Q      == 3
Primary(v) == IF v = 0 THEN "n1" ELSE "n2"

ASSUME Byz \subseteq Nodes /\ Cardinality(Byz) <= 1 /\ Primary(1) \notin Byz

VARIABLES view, pp, prep, pcert, com, exec, vcRep, nvVal

vars == <<view, pp, prep, pcert, com, exec, vcRep, nvVal>>

Init ==
  /\ view  = [n \in Nodes |-> 0]
  /\ pp    = [n \in Nodes |-> [v \in Views |-> None]]
  /\ prep  = [n \in Nodes |-> [v \in Views |-> None]]
  /\ pcert = [n \in Nodes |-> [v \in Views |-> None]]
  /\ com   = [n \in Nodes |-> [v \in Views |-> None]]
  /\ exec  = [n \in Nodes |-> None]
  /\ vcRep = [n \in Nodes |-> None]          \* None = no VIEW_CHANGE sent yet
  /\ nvVal = None

\* The leader of v signed a proposal for val.
LeaderSigned(v, val) ==
  \/ Primary(v) \in Byz
  \/ pp[Primary(v)][v] = val

\* A prepared certificate for (v, val) can be assembled from real signatures.
CertExists(v, val) ==
  /\ LeaderSigned(v, val)
  /\ Cardinality({s \in Honest : prep[s][v] = val} \cup Byz) >= Q

CommitQuorum(v, val) ==
  Cardinality({s \in Honest : com[s][v] = val} \cup Byz) >= Q

\* An honest member accepts the leader's proposal of its current view.
PrePrepare(n, v, val) ==
  /\ n \in Honest /\ view[n] = v /\ pp[n][v] = None
  /\ IF Primary(v) \in Byz
       THEN TRUE                                  \* Byzantine leader: any value, per member
       ELSE IF v = 0
         THEN (n = Primary(0) \/ pp[Primary(0)][0] = val)
         ELSE nvVal = val                         \* view 1: the NEW_VIEW proposal
  /\ pp' = [pp EXCEPT ![n][v] = val]
  /\ UNCHANGED <<view, prep, pcert, com, exec, vcRep, nvVal>>

Prepare(n, v) ==
  /\ n \in Honest /\ view[n] = v /\ pp[n][v] # None /\ prep[n][v] = None
  /\ prep' = [prep EXCEPT ![n][v] = pp[n][v]]
  /\ UNCHANGED <<view, pp, pcert, com, exec, vcRep, nvVal>>

BecomePrepared(n, v, val) ==
  /\ n \in Honest /\ view[n] = v /\ pcert[n][v] = None
  /\ CertExists(v, val)
  /\ pcert' = [pcert EXCEPT ![n][v] = val]
  /\ UNCHANGED <<view, pp, prep, com, exec, vcRep, nvVal>>

Commit(n, v) ==
  /\ n \in Honest /\ view[n] = v /\ pcert[n][v] # None /\ com[n][v] = None
  /\ com' = [com EXCEPT ![n][v] = pcert[n][v]]
  /\ UNCHANGED <<view, pp, prep, pcert, exec, vcRep, nvVal>>

Execute(n, v, val) ==
  /\ n \in Honest /\ exec[n] = None
  /\ IF OldRule
       THEN CertExists(v, val)
       ELSE pcert[n][v] = val /\ CommitQuorum(v, val)
  /\ exec' = [exec EXCEPT ![n] = val]
  /\ UNCHANGED <<view, pp, prep, pcert, com, vcRep, nvVal>>

\* An honest member leaves view 0, reporting its prepared certificate.
ViewChange(n) ==
  /\ n \in Honest /\ view[n] = 0
  /\ view' = [view EXCEPT ![n] = 1]
  /\ vcRep' = [vcRep EXCEPT ![n] = pcert[n][0]]
  /\ UNCHANGED <<pp, prep, pcert, com, exec, nvVal>>

\* The (honest) primary of view 1 picks its proposal from a quorum S of
\* VIEW_CHANGEs. A Byzantine member in S may report any certificate that
\* really exists, or nothing.
NewView(S, byzReport, val) ==
  /\ nvVal = None /\ view[Primary(1)] = 1
  /\ S \subseteq Nodes /\ Cardinality(S) >= Q
  /\ \A s \in S \cap Honest : vcRep[s] # None \/ view[s] = 1
  /\ byzReport \in {None} \cup {x \in Values : CertExists(0, x)}
  /\ LET reported == {vcRep[s] : s \in S \cap Honest} \cup (IF S \cap Byz # {} THEN {byzReport} ELSE {})
         certs    == reported \ {None}
     IN IF certs # {} /\ ~IgnoreReports
          THEN val \in certs
          ELSE TRUE
  /\ nvVal' = val
  /\ UNCHANGED <<view, pp, prep, pcert, com, exec, vcRep>>

Next ==
  \/ \E n \in Nodes, v \in Views, val \in Values : PrePrepare(n, v, val)
  \/ \E n \in Nodes, v \in Views : Prepare(n, v) \/ Commit(n, v)
  \/ \E n \in Nodes, v \in Views, val \in Values : BecomePrepared(n, v, val) \/ Execute(n, v, val)
  \/ \E n \in Nodes : ViewChange(n)
  \/ \E S \in SUBSET Nodes, b \in {None} \cup Values, val \in Values : NewView(S, b, val)

Spec == Init /\ [][Next]_vars

\* PROPERTY-001: no two honest members execute different values at one sequence.
Agreement == \A a, b \in Honest : (exec[a] # None /\ exec[b] # None) => exec[a] = exec[b]

\* An honest member never signs COMMIT for a value it is not prepared for (OMEGA-01).
CommitOnlyWhenPrepared == \A n \in Honest, v \in Views : com[n][v] # None => com[n][v] = pcert[n][v]

TypeOK ==
  /\ view \in [Nodes -> Views]
  /\ exec \in [Nodes -> Values \cup {None}]
  /\ nvVal \in Values \cup {None}
=============================================================================
