From f8f274d89991300aad7a7ef850f379a728a50378 Mon Sep 17 00:00:00 2001 From: oggy-dfin <89794951+oggy-dfin@users.noreply.github.com> Date: Wed, 15 Jan 2025 10:53:13 +0100 Subject: [PATCH] feat(IC-1579): TLA annotations for disburse_to_neuron (#3411) Instrument the `disburse_to_neuron` function to check the test traces for compatibility with the TLA model. --- rs/nns/governance/src/governance.rs | 12 +- .../src/governance/tla/disburse_to_neuron.rs | 29 +++ rs/nns/governance/src/governance/tla/mod.rs | 2 + rs/nns/governance/tests/governance.rs | 2 + rs/nns/governance/tla/Claim_Neuron.tla | 2 +- rs/nns/governance/tla/Disburse_To_Neuron.tla | 193 ++++++++++++++++++ .../tla/Disburse_To_Neuron_Apalache.tla | 70 +++++++ 7 files changed, 307 insertions(+), 3 deletions(-) create mode 100644 rs/nns/governance/src/governance/tla/disburse_to_neuron.rs create mode 100644 rs/nns/governance/tla/Disburse_To_Neuron.tla create mode 100644 rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla diff --git a/rs/nns/governance/src/governance.rs b/rs/nns/governance/src/governance.rs index 48a951b8349..ccfeb7948f0 100644 --- a/rs/nns/governance/src/governance.rs +++ b/rs/nns/governance/src/governance.rs @@ -147,8 +147,8 @@ use std::collections::BTreeSet; #[cfg(feature = "tla")] pub use tla::{ tla_update_method, InstrumentationState, ToTla, CLAIM_NEURON_DESC, DISBURSE_NEURON_DESC, - MERGE_NEURONS_DESC, SPAWN_NEURONS_DESC, SPAWN_NEURON_DESC, SPLIT_NEURON_DESC, - TLA_INSTRUMENTATION_STATE, TLA_TRACES_LKEY, TLA_TRACES_MUTEX, + DISBURSE_TO_NEURON_DESC, MERGE_NEURONS_DESC, SPAWN_NEURONS_DESC, SPAWN_NEURON_DESC, + SPLIT_NEURON_DESC, TLA_INSTRUMENTATION_STATE, TLA_TRACES_LKEY, TLA_TRACES_MUTEX, }; // 70 KB (for executing NNS functions that are not canister upgrades) @@ -3541,6 +3541,7 @@ impl Governance { /// stake. /// - The amount to split minus the transfer fee is more than the minimum /// stake. + #[cfg_attr(feature = "tla", tla_update_method(DISBURSE_TO_NEURON_DESC.clone()))] pub async fn disburse_to_neuron( &mut self, id: &NeuronId, @@ -3706,6 +3707,13 @@ impl Governance { // Do the transfer from the parent neuron's subaccount to the child neuron's // subaccount. let memo = created_timestamp_seconds; + + tla_log_locals! { + parent_neuron_id: parent_nid.id, + disburse_amount: disburse_to_neuron.amount_e8s, + child_neuron_id: child_nid.id, + child_account_id: tla::account_to_tla(neuron_subaccount(to_subaccount)) + }; let result: Result = self .ledger .transfer_funds( diff --git a/rs/nns/governance/src/governance/tla/disburse_to_neuron.rs b/rs/nns/governance/src/governance/tla/disburse_to_neuron.rs new file mode 100644 index 00000000000..b114e0b9956 --- /dev/null +++ b/rs/nns/governance/src/governance/tla/disburse_to_neuron.rs @@ -0,0 +1,29 @@ +use super::{extract_common_constants, post_process_trace}; +use lazy_static::lazy_static; +use tla_instrumentation::{Label, TlaConstantAssignment, ToTla, Update, VarAssignment}; + +const PID: &str = "Disburse_To_Neuron"; +lazy_static! { + pub static ref DISBURSE_TO_NEURON_DESC: Update = { + let default_locals = VarAssignment::new() + .add("parent_neuron_id", 0_u64.to_tla_value()) + .add("disburse_amount", 0_u64.to_tla_value()) + .add("child_account_id", "".to_tla_value()) + .add("child_neuron_id", 0_u64.to_tla_value()); + Update { + default_start_locals: default_locals.clone(), + default_end_locals: default_locals, + start_label: Label::new("DisburseToNeuron"), + end_label: Label::new("Done"), + process_id: PID.to_string(), + canister_name: "governance".to_string(), + post_process: |trace| { + let constants = TlaConstantAssignment { + constants: extract_common_constants(PID, trace).into_iter().collect(), + }; + post_process_trace(trace); + constants + }, + } + }; +} diff --git a/rs/nns/governance/src/governance/tla/mod.rs b/rs/nns/governance/src/governance/tla/mod.rs index bf8fa7de13d..45e62e439d2 100644 --- a/rs/nns/governance/src/governance/tla/mod.rs +++ b/rs/nns/governance/src/governance/tla/mod.rs @@ -26,6 +26,7 @@ pub use store::{TLA_INSTRUMENTATION_STATE, TLA_TRACES_LKEY, TLA_TRACES_MUTEX}; mod claim_neuron; mod disburse_neuron; +mod disburse_to_neuron; mod merge_neurons; mod spawn_neuron; mod spawn_neurons; @@ -33,6 +34,7 @@ mod split_neuron; pub use claim_neuron::CLAIM_NEURON_DESC; pub use disburse_neuron::DISBURSE_NEURON_DESC; +pub use disburse_to_neuron::DISBURSE_TO_NEURON_DESC; pub use merge_neurons::MERGE_NEURONS_DESC; pub use spawn_neuron::SPAWN_NEURON_DESC; pub use spawn_neurons::SPAWN_NEURONS_DESC; diff --git a/rs/nns/governance/tests/governance.rs b/rs/nns/governance/tests/governance.rs index 7a11a736248..f1cde600775 100644 --- a/rs/nns/governance/tests/governance.rs +++ b/rs/nns/governance/tests/governance.rs @@ -4264,6 +4264,7 @@ fn fixture_for_approve_kyc() -> GovernanceProto { /// If we approve KYC for Principals 1 and 2, neurons A, B and C should have /// `kyc_verified=true`, while neuron D still has `kyc_verified=false` #[test] +#[cfg_attr(feature = "tla", with_tla_trace_check)] fn test_approve_kyc() { let governance_proto = fixture_for_approve_kyc(); let driver = fake::FakeDriver::default() @@ -6716,6 +6717,7 @@ async fn test_neuron_with_non_self_authenticating_controller_is_now_allowed() { } #[test] +#[cfg_attr(feature = "tla", with_tla_trace_check)] fn test_disburse_to_neuron() { let from = *TEST_NEURON_1_OWNER_PRINCIPAL; // Compute the subaccount to which the transfer would have been made diff --git a/rs/nns/governance/tla/Claim_Neuron.tla b/rs/nns/governance/tla/Claim_Neuron.tla index cd38eebed88..d88dcecb55a 100644 --- a/rs/nns/governance/tla/Claim_Neuron.tla +++ b/rs/nns/governance/tla/Claim_Neuron.tla @@ -72,7 +72,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}; - neuron_id_by_account := account :> neuron_id @@ neuron_id_by_account; +gp 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))); diff --git a/rs/nns/governance/tla/Disburse_To_Neuron.tla b/rs/nns/governance/tla/Disburse_To_Neuron.tla new file mode 100644 index 00000000000..622f87505d2 --- /dev/null +++ b/rs/nns/governance/tla/Disburse_To_Neuron.tla @@ -0,0 +1,193 @@ +---- MODULE Disburse_To_Neuron ---- + +EXTENDS TLC, Integers, FiniteSets, Sequences, Variants + +CONSTANTS + Governance_Account_Ids, + Neuron_Ids + +CONSTANTS + Disburse_To_Neuron_Process_Ids + +CONSTANTS + \* Minimum stake a neuron can have + MIN_STAKE, + \* The transfer fee charged by the ledger canister + TRANSACTION_FEE + +CONSTANT + FRESH_NEURON_ID(_) + +\* Initial value used for uninitialized accounts +DUMMY_ACCOUNT == "" + +\* @type: (a -> b, Set(a)) => a -> b; +Remove_Arguments(f, S) == [ x \in (DOMAIN f \ S) |-> f[x]] +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 + + neuron \in [{} -> {}]; + \* Used to decide whether we should refresh or claim a neuron + neuron_id_by_account \in [{} -> {}]; + \* The set of currently locked neurons + locks = {}; + \* The queue of messages sent from the governance canister to the ledger canister + governance_to_ledger = <<>>; + ledger_to_governance = {}; + spawning_neurons = FALSE; + +macro send_request(caller_id, request_args) { + governance_to_ledger := Append(governance_to_ledger, request(caller_id, request_args)) +}; + +process (Disburse_To_Neuron \in Disburse_To_Neuron_Process_Ids) + variables + parent_neuron_id = 0; + disburse_amount = 0; + child_account_id = DUMMY_ACCOUNT; + child_neuron_id = 0; + { + DisburseToNeuron: + either { + \* Simulate calls that just fail early and don't change the state. + \* Not so useful for model checking, but needed to follow the code traces. + goto Done; + } or { + \* Skipping a few checks again: + \* 1. authorization of the caller + \* 2. that the parent neuron has been dissolved + \* 3. kyc checks + \* 4. checks on the presence and shape of new controller + with(pnid \in DOMAIN(neuron) \ locks; + parent_neuron = neuron[pnid]; + amt \in (MIN_STAKE + TRANSACTION_FEE)..(parent_neuron.cached_stake - parent_neuron.fees - MIN_STAKE); + c_acc_id \in Governance_Account_Ids \ { neuron[n].account : n \in DOMAIN(neuron)}; + ) { + parent_neuron_id := pnid; + disburse_amount := amt; + await parent_neuron.maturity <= TRANSACTION_FEE; + child_account_id := c_acc_id; + child_neuron_id := FRESH_NEURON_ID(DOMAIN(neuron)); + neuron_id_by_account := child_account_id :> child_neuron_id @@ neuron_id_by_account; + neuron := child_neuron_id :> [ cached_stake |-> 0, account |-> child_account_id, fees |-> 0, maturity |-> 0 ] @@ neuron; + \* The Rust code throws an error here if the parent neuron is locked. Instead, we prevent the Disburse_To_Neuron process from running. + \* This is OK since the Rust code doesn't change the canister's state before obtaining the parant lock (if it + \* did, the model wouldn't capture this state and we could miss behaviors). + assert child_neuron_id \notin locks; + \* Note that in the implementation this implies that child_neuron_id != parent_neuron_id, + \* as the locks are taken sequentially there; here, we're sure that these neuron IDs differ, + \* so we omit the extra check. + locks := locks \union {parent_neuron_id, child_neuron_id}; + send_request(self, transfer(parent_neuron.account, child_account_id, disburse_amount - TRANSACTION_FEE, TRANSACTION_FEE)); + }; + }; + DisburseToNeuron_WaitForTransfer: + with(answer \in { resp \in ledger_to_governance: resp.caller = self}) { + ledger_to_governance := ledger_to_governance \ {answer}; + if(answer.response = Variant("Fail", UNIT)) { + neuron := Remove_Arguments(neuron, {child_neuron_id}); + neuron_id_by_account := Remove_Arguments(neuron_id_by_account, {child_account_id}); + } else { + neuron := [ neuron EXCEPT ![parent_neuron_id].cached_stake = @ - disburse_amount, + ![child_neuron_id].cached_stake = disburse_amount - TRANSACTION_FEE ]; + }; + locks := locks \ {parent_neuron_id, child_neuron_id}; + parent_neuron_id := 0; + disburse_amount := 0; + child_account_id := DUMMY_ACCOUNT; + child_neuron_id := 0; + }; + + } +} +*) +\* 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, + 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, + disburse_amount, child_account_id, child_neuron_id >> + +ProcSet == (Disburse_To_Neuron_Process_Ids) + +Init == (* Global variables *) + /\ neuron \in [{} -> {}] + /\ neuron_id_by_account \in [{} -> {}] + /\ locks = {} + /\ governance_to_ledger = <<>> + /\ ledger_to_governance = {} + /\ spawning_neurons = FALSE + (* Process Disburse_To_Neuron *) + /\ parent_neuron_id = [self \in Disburse_To_Neuron_Process_Ids |-> 0] + /\ disburse_amount = [self \in Disburse_To_Neuron_Process_Ids |-> 0] + /\ child_account_id = [self \in Disburse_To_Neuron_Process_Ids |-> DUMMY_ACCOUNT] + /\ child_neuron_id = [self \in Disburse_To_Neuron_Process_Ids |-> 0] + /\ pc = [self \in ProcSet |-> "DisburseToNeuron"] + +DisburseToNeuron(self) == /\ pc[self] = "DisburseToNeuron" + /\ \/ /\ pc' = [pc EXCEPT ![self] = "Done"] + /\ UNCHANGED <> + \/ /\ \E pnid \in DOMAIN(neuron) \ locks: + LET parent_neuron == neuron[pnid] IN + \E amt \in (MIN_STAKE + TRANSACTION_FEE)..(parent_neuron.cached_stake - parent_neuron.fees - MIN_STAKE): + \E c_acc_id \in Governance_Account_Ids \ { neuron[n].account : n \in DOMAIN(neuron)}: + /\ parent_neuron_id' = [parent_neuron_id EXCEPT ![self] = pnid] + /\ disburse_amount' = [disburse_amount EXCEPT ![self] = amt] + /\ parent_neuron.maturity <= TRANSACTION_FEE + /\ child_account_id' = [child_account_id EXCEPT ![self] = c_acc_id] + /\ 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.") + /\ 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, + spawning_neurons >> + +DisburseToNeuron_WaitForTransfer(self) == /\ pc[self] = "DisburseToNeuron_WaitForTransfer" + /\ \E answer \in { resp \in ledger_to_governance: resp.caller = self}: + /\ ledger_to_governance' = ledger_to_governance \ {answer} + /\ IF answer.response = Variant("Fail", UNIT) + THEN /\ neuron' = Remove_Arguments(neuron, {child_neuron_id[self]}) + /\ neuron_id_by_account' = Remove_Arguments(neuron_id_by_account, {child_account_id[self]}) + ELSE /\ neuron' = [ neuron EXCEPT ![parent_neuron_id[self]].cached_stake = @ - disburse_amount[self], + ![child_neuron_id[self]].cached_stake = disburse_amount[self] - TRANSACTION_FEE ] + /\ UNCHANGED neuron_id_by_account + /\ locks' = locks \ {parent_neuron_id[self], child_neuron_id[self]} + /\ parent_neuron_id' = [parent_neuron_id EXCEPT ![self] = 0] + /\ disburse_amount' = [disburse_amount EXCEPT ![self] = 0] + /\ 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, + spawning_neurons >> + +Disburse_To_Neuron(self) == DisburseToNeuron(self) + \/ DisburseToNeuron_WaitForTransfer(self) + +(* Allow infinite stuttering to prevent deadlock on termination. *) +Terminating == /\ \A self \in ProcSet: pc[self] = "Done" + /\ UNCHANGED vars + +Next == (\E self \in Disburse_To_Neuron_Process_Ids: Disburse_To_Neuron(self)) + \/ Terminating + +Spec == Init /\ [][Next]_vars + +Termination == <>(\A self \in ProcSet: pc[self] = "Done") + +\* END TRANSLATION + +==== diff --git a/rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla b/rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla new file mode 100644 index 00000000000..b28dda89c3e --- /dev/null +++ b/rs/nns/governance/tla/Disburse_To_Neuron_Apalache.tla @@ -0,0 +1,70 @@ +---- MODULE Disburse_To_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 + +\* CODE_LINK_INSERT_CONSTANTS + +(* +CONSTANTS + \* @type: Set($account); + Governance_Account_Ids, + \* @type: Set($neuronId); + Neuron_Ids + +CONSTANTS + \* @type: Set($proc); + Disburse_To_Neuron_Process_Ids + +CONSTANTS + \* Minimum stake a neuron can have + \* @type: Int; + MIN_STAKE, + \* The transfer fee charged by the ledger canister + \* @type: Int; + TRANSACTION_FEE +*) + +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; + disburse_amount, + \* @type: $proc -> $account; + child_account_id, + \* @type: $proc -> $neuronId; + child_neuron_id, + \* 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; + spawning_neurons + +\* @type: Set($neuronId) => $neuronId; +FRESH_NEURON_ID(existing_neurons) == CHOOSE nid \in (Neuron_Ids \ existing_neurons): TRUE + +MOD == INSTANCE Disburse_To_Neuron + +Next == [MOD!Next]_MOD!vars + + +====