Governance: TLA Codelink for refresh_neuron #3547
+276
−2
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| use lazy_static::lazy_static; | ||
| use tla_instrumentation::{Label, TlaConstantAssignment, ToTla, Update, VarAssignment}; | ||
|
|
||
| use super::common::default_account; | ||
| use super::{extract_common_constants, post_process_trace}; | ||
|
|
||
| lazy_static! { | ||
| pub static ref REFRESH_NEURON_DESC: Update = { | ||
| const PID: &str = "Refresh_Neuron"; | ||
| let default_locals = VarAssignment::new() | ||
| .add("account", default_account()) | ||
| .add("neuron_id", 0_u64.to_tla_value()); | ||
|
|
||
| Update { | ||
| default_start_locals: default_locals.clone(), | ||
| default_end_locals: default_locals, | ||
| start_label: Label::new("RefreshNeuron1"), | ||
| 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 | ||
| }, | ||
| } | ||
| }; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
| @@ -0,0 +1,164 @@ | ||||||
| ------------ MODULE Refresh_Neuron ------------ | ||||||
| EXTENDS TLC, Sequences, Naturals, FiniteSets, Variants | ||||||
|
|
||||||
| CONSTANT | ||||||
| FRESH_NEURON_ID(_) | ||||||
|
|
||||||
| CONSTANTS | ||||||
| Governance_Account_Ids, | ||||||
| Neuron_Ids | ||||||
|
|
||||||
| CONSTANTS | ||||||
| Refresh_Neuron_Process_Ids | ||||||
|
|
||||||
| CONSTANTS | ||||||
| \* Minimum stake a neuron can have | ||||||
| MIN_STAKE, | ||||||
| \* The transfer fee charged by the ledger canister | ||||||
| TRANSACTION_FEE | ||||||
|
|
||||||
| OP_ACCOUNT_BALANCE == "account_balance" | ||||||
| ACCOUNT_BALANCE_FAIL == "Err" | ||||||
|
Comment on lines
+20
to
+21
There was a problem hiding this comment. These seem unused? And if you get rid of the |
||||||
| DUMMY_ACCOUNT == "" | ||||||
|
|
||||||
| \* @type: (a -> b, Set(a)) => a -> b; | ||||||
| Remove_Arguments(f, S) == [ x \in (DOMAIN f \ S) |-> f[x]] | ||||||
|
|
||||||
| request(caller, request_args) == [caller |-> caller, method_and_args |-> request_args] | ||||||
| account_balance(account) == Variant("AccountBalance", [account |-> account]) | ||||||
|
|
||||||
|
|
||||||
| (* --algorithm Governance_Ledger_Refresh_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 refresh_neuron_reset_local_vars() { | ||||||
| account := DUMMY_ACCOUNT; | ||||||
| neuron_id := 0; | ||||||
| } | ||||||
|
|
||||||
|
|
||||||
| \* Modified from formal-models/tla/governance-ledger | ||||||
| \* A Refresh_Neuron process simulates a call to refresh_neuron | ||||||
| process ( Refresh_Neuron \in Refresh_Neuron_Process_Ids ) | ||||||
| variable | ||||||
| \* There are two ways that the user can invoke a neuron refresh: | ||||||
| \* 1. by specifying an account ID | ||||||
| \* 2. by specifying an existing neuron ID | ||||||
| \* We only model the second option; the second should follow from the invariant that | ||||||
| \* \A nid aid : neuron_id_by_account[aid] = nid <=> neuron[nid].account = aid | ||||||
|
|
||||||
| \* The account is an argument; we let it be chosen non-deteministically | ||||||
| account = DUMMY_ACCOUNT; | ||||||
| \* The neuron_id is determined by account. | ||||||
| neuron_id = 0; | ||||||
| { | ||||||
| RefreshNeuron1: | ||||||
| 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 { | ||||||
| with(nid \in DOMAIN(neuron) \ locks) { | ||||||
| neuron_id := nid; | ||||||
| account := neuron[nid].account; | ||||||
| locks := locks \union {neuron_id}; | ||||||
| governance_to_ledger := Append(governance_to_ledger, request(self, account_balance(account))); | ||||||
| }; | ||||||
| }; | ||||||
| WaitForBalanceQuery: | ||||||
| \* Note that the "with" construct implicitly awaits until the set of values to draw from is non-empty | ||||||
| with(answer \in { resp \in ledger_to_governance : resp.caller = self }) { | ||||||
| ledger_to_governance := ledger_to_governance \ {answer}; | ||||||
| if(answer.response /= Variant("Fail", UNIT)) { | ||||||
| with (b = VariantGetOrElse("BalanceQueryOk", answer.response, 0)) { | ||||||
| if(b >= MIN_STAKE) { | ||||||
| neuron := [neuron EXCEPT ![neuron_id] = [@ EXCEPT !.cached_stake = b] ] | ||||||
|
There was a problem hiding this comment. Apparently you can also write
Suggested change
(I wasn't aware of this syntax before). |
||||||
| }; | ||||||
| }; | ||||||
| }; | ||||||
| locks := locks \ {neuron_id}; | ||||||
| }; | ||||||
| refresh_neuron_reset_local_vars(); | ||||||
| }; | ||||||
|
|
||||||
| } | ||||||
| *) | ||||||
| \* BEGIN TRANSLATION (chksum(pcal) = "5ba99437" /\ chksum(tla) = "546ae43c") | ||||||
| VARIABLES neuron, neuron_id_by_account, locks, governance_to_ledger, | ||||||
| ledger_to_governance, spawning_neurons, pc, account, neuron_id | ||||||
|
|
||||||
| vars == << neuron, neuron_id_by_account, locks, governance_to_ledger, | ||||||
| ledger_to_governance, spawning_neurons, pc, account, neuron_id >> | ||||||
|
|
||||||
| ProcSet == (Refresh_Neuron_Process_Ids) | ||||||
|
|
||||||
| Init == (* Global variables *) | ||||||
| /\ neuron \in [{} -> {}] | ||||||
| /\ neuron_id_by_account \in [{} -> {}] | ||||||
| /\ locks = {} | ||||||
| /\ governance_to_ledger = <<>> | ||||||
| /\ ledger_to_governance = {} | ||||||
| /\ spawning_neurons = FALSE | ||||||
| (* Process Refresh_Neuron *) | ||||||
| /\ account = [self \in Refresh_Neuron_Process_Ids |-> DUMMY_ACCOUNT] | ||||||
| /\ neuron_id = [self \in Refresh_Neuron_Process_Ids |-> 0] | ||||||
| /\ pc = [self \in ProcSet |-> "RefreshNeuron1"] | ||||||
|
|
||||||
| RefreshNeuron1(self) == /\ pc[self] = "RefreshNeuron1" | ||||||
| /\ \/ /\ pc' = [pc EXCEPT ![self] = "Done"] | ||||||
| /\ UNCHANGED <<locks, governance_to_ledger, account, neuron_id>> | ||||||
| \/ /\ \E nid \in DOMAIN(neuron) \ locks: | ||||||
| /\ neuron_id' = [neuron_id EXCEPT ![self] = nid] | ||||||
| /\ account' = [account EXCEPT ![self] = neuron[nid].account] | ||||||
| /\ locks' = (locks \union {neuron_id'[self]}) | ||||||
| /\ governance_to_ledger' = Append(governance_to_ledger, request(self, account_balance(account'[self]))) | ||||||
| /\ pc' = [pc EXCEPT ![self] = "WaitForBalanceQuery"] | ||||||
| /\ UNCHANGED << neuron, neuron_id_by_account, | ||||||
| ledger_to_governance, spawning_neurons >> | ||||||
|
|
||||||
| WaitForBalanceQuery(self) == /\ pc[self] = "WaitForBalanceQuery" | ||||||
| /\ \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 /\ LET b == VariantGetOrElse("BalanceQueryOk", answer.response, 0) IN | ||||||
| IF b >= MIN_STAKE | ||||||
| THEN /\ neuron' = [neuron EXCEPT ![neuron_id[self]] = [@ EXCEPT !.cached_stake = b] ] | ||||||
| ELSE /\ TRUE | ||||||
| /\ UNCHANGED neuron | ||||||
| ELSE /\ TRUE | ||||||
| /\ UNCHANGED neuron | ||||||
| /\ locks' = locks \ {neuron_id[self]} | ||||||
| /\ account' = [account EXCEPT ![self] = DUMMY_ACCOUNT] | ||||||
| /\ neuron_id' = [neuron_id EXCEPT ![self] = 0] | ||||||
| /\ pc' = [pc EXCEPT ![self] = "Done"] | ||||||
| /\ UNCHANGED << neuron_id_by_account, | ||||||
| governance_to_ledger, | ||||||
| spawning_neurons >> | ||||||
|
|
||||||
| Refresh_Neuron(self) == RefreshNeuron1(self) \/ WaitForBalanceQuery(self) | ||||||
|
|
||||||
| (* Allow infinite stuttering to prevent deadlock on termination. *) | ||||||
| Terminating == /\ \A self \in ProcSet: pc[self] = "Done" | ||||||
| /\ UNCHANGED vars | ||||||
|
|
||||||
| Next == (\E self \in Refresh_Neuron_Process_Ids: Refresh_Neuron(self)) | ||||||
| \/ Terminating | ||||||
|
|
||||||
| Spec == Init /\ [][Next]_vars | ||||||
|
|
||||||
| Termination == <>(\A self \in ProcSet: pc[self] = "Done") | ||||||
|
|
||||||
| \* END TRANSLATION | ||||||
|
|
||||||
| ==== | ||||||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| ---- MODULE Refresh_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); | ||
| Account_Ids, | ||
| \* @type: Set($account); | ||
| Governance_Account_Ids, | ||
| \* @type: Set($neuronId); | ||
| Neuron_Ids | ||
|
|
||
| CONSTANTS | ||
| \* @type: Set($proc); | ||
| Claim_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 -> Int; | ||
| neuron_id, | ||
| \* @type: $proc -> $account; | ||
| account, | ||
| \* 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 | ||
|
|
||
| \* Not used in this model. Consider removing (TODO). | ||
| \* @type: Set($neuronId) => $neuronId; | ||
| FRESH_NEURON_ID(existing_neurons) == CHOOSE nid \in (Neuron_Ids \ existing_neurons): TRUE | ||
|
|
||
| MOD == INSTANCE Refresh_Neuron | ||
|
|
||
| Next == [MOD!Next]_MOD!vars | ||
|
|
||
| ==== |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you need the account here (and in the model)? AFAICT you can derive it from the global state (
neuronin the model).