feat(IC-1579): combined TLA model of the instrumented governance meth…

…ods (#3499) This creates an overall model of the governance-ledger interaction that can then be model checked using TLC.
dfinity · Feb 21, 2025 · 7c85d44 · 7c85d44
1 parent 98fa250
commit 7c85d44
Show file tree

Hide file tree

Showing 19 changed files with 675 additions and 267 deletions.
diff --git a/rs/nns/governance/src/governance/tla/disburse_neuron.rs b/rs/nns/governance/src/governance/tla/disburse_neuron.rs
@@ -42,6 +42,10 @@ lazy_static! {
                 constants
                     .constants
                     .insert("Account_Ids".to_string(), all_accounts.to_tla_value());
+                constants.constants.insert(
+                    "POSSIBLE_DISBURSE_AMOUNTS(_neurons, neuronId)".to_string(),
+                    TlaValue::Constant("Nat".to_string()),
+                );
                 constants
             },
         }

diff --git a/rs/nns/governance/tla/Claim_Neuron.tla b/rs/nns/governance/tla/Claim_Neuron.tla
@@ -5,8 +5,7 @@ CONSTANT
     FRESH_NEURON_ID(_)
 
 CONSTANTS
-    Governance_Account_Ids,
-    Neuron_Ids
+    Governance_Account_Ids
 
 CONSTANTS
     Claim_Neuron_Process_Ids
@@ -17,8 +16,6 @@ CONSTANTS
     \* The transfer fee charged by the ledger canister
     TRANSACTION_FEE
 
-OP_ACCOUNT_BALANCE == "account_balance"
-ACCOUNT_BALANCE_FAIL == "Err"
 DUMMY_ACCOUNT == ""
 
 \* @type: (a -> b, Set(a)) => a -> b;
@@ -72,7 +69,7 @@ process ( Claim_Neuron \in Claim_Neuron_Process_Ids )
             \* instead of await here, to check that
             assert neuron_id \notin locks;
             locks := locks \union {neuron_id};
-gp            neuron_id_by_account := account :> neuron_id @@ neuron_id_by_account;
+            neuron_id_by_account := account :> neuron_id @@ neuron_id_by_account;
             neuron := neuron_id :> [ cached_stake |-> 0, account |-> account, fees |-> 0, maturity |-> 0 ] @@ neuron;
             \* send_request(self, OP_QUERY_BALANCE, balance_query(account));
             governance_to_ledger := Append(governance_to_ledger, request(self, account_balance(account)));
@@ -102,11 +99,11 @@ gp            neuron_id_by_account := account :> neuron_id @@ neuron_id_by_accou
 
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "a7e1f417" /\ chksum(tla) = "bed42424")
-VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
+\* BEGIN TRANSLATION (chksum(pcal) = "a7e1f417" /\ chksum(tla) = "ded8c980")
+VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
           ledger_to_governance, spawning_neurons, account, neuron_id
 
-vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
+vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
            ledger_to_governance, spawning_neurons, account, neuron_id >>
 
 ProcSet == (Claim_Neuron_Process_Ids)
@@ -129,8 +126,8 @@ ClaimNeuron1(self) == /\ pc[self] = "ClaimNeuron1"
                          \/ /\ \E aid \in Governance_Account_Ids \ DOMAIN(neuron_id_by_account):
                                  /\ account' = [account EXCEPT ![self] = aid]
                                  /\ neuron_id' = [neuron_id EXCEPT ![self] = FRESH_NEURON_ID(DOMAIN(neuron))]
-                                 /\ Assert(neuron_id'[self] \notin locks,
-                                           "Failure of assertion at line 73, column 13.")
+                                 /\ Assert(neuron_id'[self] \notin locks, 
+                                           "Failure of assertion at line 70, column 13.")
                                  /\ locks' = (locks \union {neuron_id'[self]})
                                  /\ neuron_id_by_account' = (account'[self] :> neuron_id'[self] @@ neuron_id_by_account)
                                  /\ neuron' = (neuron_id'[self] :> [ cached_stake |-> 0, account |-> account'[self], fees |-> 0, maturity |-> 0 ] @@ neuron)
@@ -154,7 +151,7 @@ WaitForBalanceQuery(self) == /\ pc[self] = "WaitForBalanceQuery"
                              /\ account' = [account EXCEPT ![self] = DUMMY_ACCOUNT]
                              /\ neuron_id' = [neuron_id EXCEPT ![self] = 0]
                              /\ pc' = [pc EXCEPT ![self] = "Done"]
-                             /\ UNCHANGED << governance_to_ledger,
+                             /\ UNCHANGED << governance_to_ledger, 
                                              spawning_neurons >>
 
 Claim_Neuron(self) == ClaimNeuron1(self) \/ WaitForBalanceQuery(self)

diff --git a/rs/nns/governance/tla/Claim_Neuron_Apalache.tla b/rs/nns/governance/tla/Claim_Neuron_Apalache.tla
@@ -1,16 +1,7 @@
 ---- MODULE Claim_Neuron_Apalache ----
 
 
-EXTENDS TLC, Variants
-
-(*
-@typeAlias: proc = Str;
-@typeAlias: account = Str;
-@typeAlias: neuronId = Int;
-@typeAlias: methodCall = Transfer({ from: $account, to: $account, amount: Int, fee: Int}) | AccountBalance({ account: $account });
-@typeAlias: methodResponse = Fail(UNIT) | TransferOk(UNIT) | BalanceQueryOk(Int);
-*)
-_type_alias_dummy == TRUE
+EXTENDS TLC, Variants, Common_Apalache
 
 \* CODE_LINK_INSERT_CONSTANTS
 
@@ -37,18 +28,6 @@ CONSTANTS
 *)
 
 VARIABLES
-    \* @type: $neuronId -> {cached_stake: Int, account: $account, maturity: Int, fees: Int};
-    neuron,
-    \* @type: $account -> $neuronId;
-    neuron_id_by_account,
-    \* @type: Set($neuronId);
-    locks,
-    \* @type: Seq({caller : $proc, method_and_args: $methodCall });
-    governance_to_ledger,
-    \* @type: Set({caller: $proc, response: $methodResponse });
-    ledger_to_governance,
-    \* @type: $proc -> Str;
-    pc,
     \* @type: $proc -> Int;
     neuron_id,
     \* @type: $proc -> $account;

diff --git a/rs/nns/governance/tla/Common_Apalache.tla b/rs/nns/governance/tla/Common_Apalache.tla
@@ -0,0 +1,29 @@
+---- MODULE Common_Apalache ----
+EXTENDS TLC
+
+(*
+@typeAlias: proc = Str;
+@typeAlias: account = Str;
+@typeAlias: neuronId = Int;
+@typeAlias: methodCall = Transfer({ from: $account, to: $account, amount: Int, fee: Int}) | AccountBalance({ account: $account });
+@typeAlias: methodResponse = Fail(UNIT) | TransferOk(UNIT) | BalanceQueryOk(Int);
+@typeAlias: neurons = $neuronId -> {cached_stake: Int, account: $account, maturity: Int, fees: Int};
+*)
+_type_alias_dummy == TRUE
+
+
+VARIABLES
+    \* @type: $neurons;
+    neuron,
+    \* @type: $account -> $neuronId;
+    neuron_id_by_account,
+    \* @type: Set($neuronId);
+    locks,
+    \* @type: Seq({caller : $proc, method_and_args: $methodCall });
+    governance_to_ledger,
+    \* @type: Set({caller: $proc, response: $methodResponse });
+    ledger_to_governance,
+    \* @type: $proc -> Str;
+    pc
+
+====
diff --git a/rs/nns/governance/tla/Disburse_Neuron.tla b/rs/nns/governance/tla/Disburse_Neuron.tla
@@ -5,7 +5,6 @@ EXTENDS TLC, Integers, FiniteSets, Sequences, Variants
 CONSTANTS
     Governance_Account_Ids,
     Account_Ids,
-    Neuron_Ids,
     Minting_Account_Id
 
 CONSTANTS
@@ -17,6 +16,11 @@ CONSTANTS
     \* The transfer fee charged by the ledger canister
     TRANSACTION_FEE
 
+CONSTANT
+    \* Which argument to give as an amount; for Apalache, we can take Nat,
+    \* for TLC we want to limit this to some finite set
+    POSSIBLE_DISBURSE_AMOUNTS(_, _)
+
 \* Initial value used for uninitialized accounts
 DUMMY_ACCOUNT == ""
 
@@ -88,7 +92,7 @@ process ( Disburse_Neuron \in Disburse_Neuron_Process_Ids )
             \* our model is well-formed.
             \* Note that the user can request to disburse an arbitrary amount. This will only fail once
             \* we send a message to the ledger.
-            with(nid \in DOMAIN(neuron) \ locks; amt \in Nat; account \in Account_Ids) {
+            with(nid \in DOMAIN(neuron) \ locks; amt \in POSSIBLE_DISBURSE_AMOUNTS(neuron, nid); account \in Account_Ids) {
                 neuron_id := nid;
                 disburse_amount := amt;
                 fees_amount := neuron[neuron_id].fees;
@@ -136,13 +140,13 @@ process ( Disburse_Neuron \in Disburse_Neuron_Process_Ids )
     }
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "49bb5804" /\ chksum(tla) = "fa8fb71a")
-VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
-          ledger_to_governance, spawning_neurons, neuron_id, disburse_amount,
+\* BEGIN TRANSLATION (chksum(pcal) = "10c9c7f7" /\ chksum(tla) = "a1672e89")
+VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
+          ledger_to_governance, spawning_neurons, neuron_id, disburse_amount, 
           to_account, fees_amount
 
-vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
-           ledger_to_governance, spawning_neurons, neuron_id, disburse_amount,
+vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
+           ledger_to_governance, spawning_neurons, neuron_id, disburse_amount, 
            to_account, fees_amount >>
 
 ProcSet == (Disburse_Neuron_Process_Ids)
@@ -165,7 +169,7 @@ DisburseNeuron1(self) == /\ pc[self] = "DisburseNeuron1"
                          /\ \/ /\ pc' = [pc EXCEPT ![self] = "Done"]
                                /\ UNCHANGED <<neuron, locks, governance_to_ledger, neuron_id, disburse_amount, to_account, fees_amount>>
                             \/ /\ \E nid \in DOMAIN(neuron) \ locks:
-                                    \E amt \in Nat:
+                                    \E amt \in POSSIBLE_DISBURSE_AMOUNTS(neuron, nid):
                                       \E account \in Account_Ids:
                                         /\ neuron_id' = [neuron_id EXCEPT ![self] = nid]
                                         /\ disburse_amount' = [disburse_amount EXCEPT ![self] = amt]
@@ -181,8 +185,8 @@ DisburseNeuron1(self) == /\ pc[self] = "DisburseNeuron1"
                                                          ELSE /\ neuron' = [neuron EXCEPT ![neuron_id'[self]] = [@ EXCEPT !.cached_stake = 0, !.fees = 0]]
                                                    /\ governance_to_ledger' = Append(governance_to_ledger, request(self, (transfer(neuron'[neuron_id'[self]].account, to_account'[self], disburse_amount'[self], TRANSACTION_FEE))))
                                                    /\ pc' = [pc EXCEPT ![self] = "DisburseNeuron_Stake_WaitForTransfer"]
-                         /\ UNCHANGED << neuron_id_by_account,
-                                         ledger_to_governance,
+                         /\ UNCHANGED << neuron_id_by_account, 
+                                         ledger_to_governance, 
                                          spawning_neurons >>
 
 DisburseNeuron_Fee_WaitForTransfer(self) == /\ pc[self] = "DisburseNeuron_Fee_WaitForTransfer"
@@ -195,19 +199,19 @@ DisburseNeuron_Fee_WaitForTransfer(self) == /\ pc[self] = "DisburseNeuron_Fee_Wa
                                                             /\ to_account' = [to_account EXCEPT ![self] = DUMMY_ACCOUNT]
                                                             /\ fees_amount' = [fees_amount EXCEPT ![self] = 0]
                                                             /\ pc' = [pc EXCEPT ![self] = "Done"]
-                                                            /\ UNCHANGED << neuron,
+                                                            /\ UNCHANGED << neuron, 
                                                                             governance_to_ledger >>
                                                        ELSE /\ IF neuron[neuron_id[self]].cached_stake > fees_amount[self]
                                                                   THEN /\ neuron' = [neuron EXCEPT ![neuron_id[self]] = [@ EXCEPT !.cached_stake = @ - fees_amount[self], !.fees = 0]]
                                                                   ELSE /\ neuron' = [neuron EXCEPT ![neuron_id[self]] = [@ EXCEPT !.cached_stake = 0, !.fees = 0]]
                                                             /\ governance_to_ledger' = Append(governance_to_ledger, request(self, (transfer(neuron'[neuron_id[self]].account, to_account[self], disburse_amount[self], TRANSACTION_FEE))))
                                                             /\ pc' = [pc EXCEPT ![self] = "DisburseNeuron_Stake_WaitForTransfer"]
-                                                            /\ UNCHANGED << locks,
-                                                                            neuron_id,
-                                                                            disburse_amount,
-                                                                            to_account,
+                                                            /\ UNCHANGED << locks, 
+                                                                            neuron_id, 
+                                                                            disburse_amount, 
+                                                                            to_account, 
                                                                             fees_amount >>
-                                            /\ UNCHANGED << neuron_id_by_account,
+                                            /\ UNCHANGED << neuron_id_by_account, 
                                                             spawning_neurons >>
 
 DisburseNeuron_Stake_WaitForTransfer(self) == /\ pc[self] = "DisburseNeuron_Stake_WaitForTransfer"
@@ -224,8 +228,8 @@ DisburseNeuron_Stake_WaitForTransfer(self) == /\ pc[self] = "DisburseNeuron_Stak
                                               /\ to_account' = [to_account EXCEPT ![self] = DUMMY_ACCOUNT]
                                               /\ fees_amount' = [fees_amount EXCEPT ![self] = 0]
                                               /\ pc' = [pc EXCEPT ![self] = "Done"]
-                                              /\ UNCHANGED << neuron_id_by_account,
-                                                              governance_to_ledger,
+                                              /\ UNCHANGED << neuron_id_by_account, 
+                                                              governance_to_ledger, 
                                                               spawning_neurons >>
 
 Disburse_Neuron(self) == DisburseNeuron1(self)

diff --git a/rs/nns/governance/tla/Disburse_Neuron_Apalache.tla b/rs/nns/governance/tla/Disburse_Neuron_Apalache.tla
@@ -1,15 +1,6 @@
 ---- MODULE Disburse_Neuron_Apalache ----
 
-EXTENDS TLC, Variants
-
-(*
-@typeAlias: proc = Str;
-@typeAlias: account = Str;
-@typeAlias: neuronId = Int;
-@typeAlias: methodCall = Transfer({ from: $account, to: $account, amount: Int, fee: Int}) | AccountBalance({ account: $account });
-@typeAlias: methodResponse = Fail(UNIT) | TransferOk(UNIT) | BalanceQueryOk(Int);
-*)
-_type_alias_dummy == TRUE
+EXTENDS TLC, Variants, Common_Apalache, Integers
 
 \* CODE_LINK_INSERT_CONSTANTS
 
@@ -35,21 +26,12 @@ CONSTANTS
     \* The transfer fee charged by the ledger canister
     \* @type: Int;
     TRANSACTION_FEE
+
+\* @type: ($neurons, $neuronId) => Set(Int);
+POSSIBLE_DISBURSE_AMOUNTS(_neuron, _nid) == Nat
 *)
 
 VARIABLES
-    \* @type: $neuronId -> {cached_stake: Int, account: $account, maturity: Int, fees: Int};
-    neuron,
-    \* @type: $account -> $neuronId;
-    neuron_id_by_account,
-    \* @type: Set($neuronId);
-    locks,
-    \* @type: Seq({caller : $proc, method_and_args: $methodCall });
-    governance_to_ledger,
-    \* @type: Set({caller: $proc, response: $methodResponse });
-    ledger_to_governance,
-    \* @type: $proc -> Str;
-    pc,
     \* Not used by this model, but it's a global variable used by spawn_neurons, so
     \* it's the easiest to just add it to all the other models
     \* @type: Bool;
@@ -62,7 +44,7 @@ VARIABLES
     to_account,
     \* @type: $proc -> Int;
     fees_amount
-
+ 
 MOD == INSTANCE Disburse_Neuron
 
 Next == [MOD!Next]_MOD!vars

diff --git a/rs/nns/governance/tla/Disburse_To_Neuron.tla b/rs/nns/governance/tla/Disburse_To_Neuron.tla
@@ -3,8 +3,7 @@
 EXTENDS TLC, Integers, FiniteSets, Sequences, Variants
 
 CONSTANTS
-    Governance_Account_Ids,
-    Neuron_Ids
+    Governance_Account_Ids
 
 CONSTANTS
     Disburse_To_Neuron_Process_Ids
@@ -28,8 +27,6 @@ Max(x, y) == IF x < y THEN y ELSE x
 request(caller, request_args) == [caller |-> caller, method_and_args |-> request_args]
 transfer(from, to, amount, fee) == Variant("Transfer", [from |-> from, to |-> to, amount |-> amount, fee |-> fee])
 
-o_deduct(disb_amount) == disb_amount + TRANSACTION_FEE
-
 (* --algorithm Governance_Ledger_Disburse_To_Neuron {
 
 variables
@@ -109,13 +106,13 @@ process (Disburse_To_Neuron \in Disburse_To_Neuron_Process_Ids)
     }
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "d03e80ed" /\ chksum(tla) = "b79d8d63")
-VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
-          ledger_to_governance, spawning_neurons, parent_neuron_id,
+\* BEGIN TRANSLATION (chksum(pcal) = "d03e80ed" /\ chksum(tla) = "60c4854a")
+VARIABLES pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
+          ledger_to_governance, spawning_neurons, parent_neuron_id, 
           disburse_amount, child_account_id, child_neuron_id
 
-vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger,
-           ledger_to_governance, spawning_neurons, parent_neuron_id,
+vars == << pc, neuron, neuron_id_by_account, locks, governance_to_ledger, 
+           ledger_to_governance, spawning_neurons, parent_neuron_id, 
            disburse_amount, child_account_id, child_neuron_id >>
 
 ProcSet == (Disburse_To_Neuron_Process_Ids)
@@ -148,12 +145,12 @@ DisburseToNeuron(self) == /\ pc[self] = "DisburseToNeuron"
                                            /\ child_neuron_id' = [child_neuron_id EXCEPT ![self] = FRESH_NEURON_ID(DOMAIN(neuron))]
                                            /\ neuron_id_by_account' = (child_account_id'[self] :> child_neuron_id'[self] @@ neuron_id_by_account)
                                            /\ neuron' = (child_neuron_id'[self] :> [ cached_stake |-> 0, account |-> child_account_id'[self], fees |-> 0, maturity |-> 0 ] @@ neuron)
-                                           /\ Assert(child_neuron_id'[self] \notin locks,
-                                                     "Failure of assertion at line 84, column 17.")
+                                           /\ Assert(child_neuron_id'[self] \notin locks, 
+                                                     "Failure of assertion at line 81, column 17.")
                                            /\ locks' = (locks \union {parent_neuron_id'[self], child_neuron_id'[self]})
                                            /\ governance_to_ledger' = Append(governance_to_ledger, request(self, (transfer(parent_neuron.account, child_account_id'[self], disburse_amount'[self] - TRANSACTION_FEE, TRANSACTION_FEE))))
                                 /\ pc' = [pc EXCEPT ![self] = "DisburseToNeuron_WaitForTransfer"]
-                          /\ UNCHANGED << ledger_to_governance,
+                          /\ UNCHANGED << ledger_to_governance, 
                                           spawning_neurons >>
 
 DisburseToNeuron_WaitForTransfer(self) == /\ pc[self] = "DisburseToNeuron_WaitForTransfer"
@@ -171,7 +168,7 @@ DisburseToNeuron_WaitForTransfer(self) == /\ pc[self] = "DisburseToNeuron_WaitFo
                                                /\ child_account_id' = [child_account_id EXCEPT ![self] = DUMMY_ACCOUNT]
                                                /\ child_neuron_id' = [child_neuron_id EXCEPT ![self] = 0]
                                           /\ pc' = [pc EXCEPT ![self] = "Done"]
-                                          /\ UNCHANGED << governance_to_ledger,
+                                          /\ UNCHANGED << governance_to_ledger, 
                                                           spawning_neurons >>
 
 Disburse_To_Neuron(self) == DisburseToNeuron(self)

diff --git a/rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla b/rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla
@@ -1,15 +1,7 @@
 ---- MODULE Disburse_To_Neuron_Apalache ----
 
-EXTENDS TLC, Variants
+EXTENDS TLC, Variants, Common_Apalache
 
-(*
-@typeAlias: proc = Str;
-@typeAlias: account = Str;
-@typeAlias: neuronId = Int;
-@typeAlias: methodCall = Transfer({ from: $account, to: $account, amount: Int, fee: Int}) | AccountBalance({ account: $account });
-@typeAlias: methodResponse = Fail(UNIT) | TransferOk(UNIT) | BalanceQueryOk(Int);
-*)
-_type_alias_dummy == TRUE
 
 \* CODE_LINK_INSERT_CONSTANTS
 
@@ -34,18 +26,6 @@ CONSTANTS
 *)
 
 VARIABLES
-    \* @type: $neuronId -> {cached_stake: Int, account: $account, maturity: Int, fees: Int};
-    neuron,
-    \* @type: $account -> $neuronId;
-    neuron_id_by_account,
-    \* @type: Set($neuronId);
-    locks,
-    \* @type: Seq({caller : $proc, method_and_args: $methodCall });
-    governance_to_ledger,
-    \* @type: Set({caller: $proc, response: $methodResponse });
-    ledger_to_governance,
-    \* @type: $proc -> Str;
-    pc,
     \* @type: $proc -> $neuronId;
     parent_neuron_id,
     \* @type: $proc -> Int;