Commit 8038826a authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Abstract ChainBuilder and rename LocalChainEnvironment -> LocalChainBuilder

The ChainBuilder represents the full implementation of a blockchain
containing all operations (such as adding blocks) and state (such as
full contracts with their receive functions). Such a value is
convertible to a Chain (but not vice versa). This is where we will state
general properties about how the block chain behaves temporally.
parent 2bc752b0
Pipeline #11318 passed with stage
in 3 minutes and 33 seconds
...@@ -53,31 +53,43 @@ Record Block := ...@@ -53,31 +53,43 @@ Record Block :=
block_txs : list Tx; block_txs : list Tx;
}. }.
(* The ChainInterface is an interface that allows different implementations
of chains. This represents the view of the blockchain that a contract
can access and interact with. This is separate from
*)
Record ChainInterface := Record ChainInterface :=
build_chain_interface { build_chain_interface {
(* Would be nice to encapsulate ChainInterface somewhat here (* Would be nice to encapsulate ChainInterface somewhat here
and avoid these ugly prefixed names *) and avoid these ugly prefixed names *)
ci_chain_type : Type; ci_type : Type;
ci_chain_at : ci_chain_type -> BlockId -> option ci_chain_type; ci_chain_at : ci_type -> BlockId -> option ci_type;
(* Last finished block. During contract execution, this is the previous (* Last finished block. During contract execution, this is the previous
block, i.e. this block does _not_ contain the transaction that caused block, i.e. this block does _not_ contain the transaction that caused
the contract to be called *) the contract to be called *)
ci_head_block : ci_chain_type -> Block; ci_head_block : ci_type -> Block;
ci_incoming_txs : ci_chain_type -> Address -> list Tx; ci_incoming_txs : ci_type -> Address -> list Tx;
ci_outgoing_txs : ci_chain_type -> Address -> list Tx; ci_outgoing_txs : ci_type -> Address -> list Tx;
ci_contract_state : ci_chain_type -> Address -> option OakValue; ci_contract_state : ci_type -> Address -> option OakValue;
}. }.
(* An actual chain interface together with a value of the chain.
For example, one obvious chain implementation could be as a list
of blocks and some operations on such a list. Then, the value is
simply the list of blocks.
This avoids having to either
1. Import an actual instance of ChainInterface when taking a chain, or
2. Abstracting over any implementation of ChainInterface when taking
a chain. *)
Record Chain := Record Chain :=
build_chain { build_chain {
chain_ci : ChainInterface; chain_ci : ChainInterface;
chain_val : chain_ci.(ci_chain_type); chain_val : chain_ci.(ci_type);
}. }.
Section ChainAccessors. Section ChainAccessors.
Context (chain : Chain). Context (chain : Chain).
Let g {A : Type} (p : forall chain : ChainInterface, ci_chain_type chain -> A) Let g {A : Type} (p : forall chain : ChainInterface, ci_type chain -> A)
:= p chain.(chain_ci) chain.(chain_val). := p chain.(chain_ci) chain.(chain_val).
Definition chain_at (bid : BlockId) : option Chain := Definition chain_at (bid : BlockId) : option Chain :=
...@@ -112,10 +124,25 @@ Inductive ContractCallContext := ...@@ -112,10 +124,25 @@ Inductive ContractCallContext :=
ctx_amount : Amount; ctx_amount : Amount;
}. }.
(* Operations that a contract can return that allows it to perform
different actions as a result of its execution. *)
Inductive ChainAction := Inductive ChainAction :=
| act_transfer (to : Address) (amount : Amount) | act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue) | act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue) | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
(* Since one operation is the possibility to deploy a new contract,
this represents an instance of a contract. Note that the act of deploying
a contract has to be a separate thing to the contract deployment a contract
can access during its execution due to positivity constraints. That is,
we would like to allow contracts to obtain information about what another
contract was deployed with (its setup, version and amount transferred). An obvious
way to model this would be to simply store a WeakContract in the chain.
But this is already a non-strict positive occurence, since we dumbed down then
end up with
Record WeakContract := { receive : (Address -> WeakContract) -> State -> State }.
where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments.
*)
with WeakContract := with WeakContract :=
| build_weak_contract | build_weak_contract
(version : Version) (version : Version)
...@@ -124,6 +151,10 @@ with WeakContract := ...@@ -124,6 +151,10 @@ with WeakContract :=
option OakValue (* message *) -> option OakValue (* message *) ->
option (OakValue * list ChainAction)). option (OakValue * list ChainAction)).
(* Represents a strongly-typed contract. This is what user's will primarily
use and interact with when they want deployment. We keep the weak contract
only "internally" for blockchains, while any strongly-typed contract can
be converted to and from *)
Record Contract Record Contract
(setup_ty msg_ty state_ty : Type) (setup_ty msg_ty state_ty : Type)
{eq_setup : OakTypeEquivalence setup_ty} {eq_setup : OakTypeEquivalence setup_ty}
...@@ -167,6 +198,7 @@ Definition contract_to_weak_contract ...@@ -167,6 +198,7 @@ Definition contract_to_weak_contract
Coercion contract_to_weak_contract : Contract >-> WeakContract. Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* Deploy a strongly typed contract with some amount and setup *)
Definition create_deployment Definition create_deployment
{setup_ty msg_ty state_ty : Type} {setup_ty msg_ty state_ty : Type}
{_ : OakTypeEquivalence setup_ty} {_ : OakTypeEquivalence setup_ty}
...@@ -178,6 +210,9 @@ Definition create_deployment ...@@ -178,6 +210,9 @@ Definition create_deployment
: ChainAction := : ChainAction :=
act_deploy amount contract (serialize setup). act_deploy amount contract (serialize setup).
(* The contract interface is the main mechanism allowing a deployed
contract to interact with another deployed contract. This hides
the ugly details everything being OakValue away from contracts. *)
Record ContractInterface {setup_ty msg_ty state_ty : Type} := Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
build_contract_interface { build_contract_interface {
(* The address of the contract being interfaced with *) (* The address of the contract being interfaced with *)
...@@ -217,3 +252,51 @@ Definition get_contract_interface ...@@ -217,3 +252,51 @@ Definition get_contract_interface
get_state := ifc_get_state; get_state := ifc_get_state;
transfer := ifc_transfer; transfer := ifc_transfer;
call := ifc_call; |}. call := ifc_call; |}.
(* A ChainBuilder represents the additional state, operations and specifications
that a concrete implementation of a block chain needs to support. In contrast
to Chain and ChainInterface, this contains the _full_ blockchain information.
Thus, a ChainBuilder should be convertible into a Chain but not vice-versa.
As an example, the builder needs to contains information about all contracts
(including their receive functions) to be able to properly call into contracts
when receiving messages. The ChainBuilder is what supports the actual
"progression of time" induced by new blocks being added. Such a ChainBuilder is
what contracts will reason over when proving interesting temporal properties
of their behavior. *)
(* TODO: Naming of this is kind of bad. It is somewhat descriptive, but not really.
Maybe something like ChainEnvironment or ChainContext could be better. *)
Record ChainBuilderInterface :=
build_chain_builder_interface {
cbi_chain_interface :> ChainInterface;
cbi_type : Type;
cbi_chain : cbi_type -> cbi_chain_interface.(ci_type);
cbi_initial : cbi_type;
cbi_add_block : cbi_type -> (* cur *)
Address (* coinbase *) ->
list (Address * ChainAction) (* actions *) ->
option cbi_type;
}.
Record ChainBuilder :=
build_chain_builder {
chain_builder_cbi : ChainBuilderInterface;
chain_builder_val : chain_builder_cbi.(cbi_type);
}.
Definition chain_builder_chain (cb : ChainBuilder) : Chain :=
let (cbi, val) := cb in
build_chain cbi (cbi.(cbi_chain) val).
Coercion chain_builder_chain : ChainBuilder >-> Chain.
Definition initial_chain_builder (cbi : ChainBuilderInterface) : ChainBuilder :=
build_chain_builder cbi cbi.(cbi_initial).
Definition add_block
(cur : ChainBuilder)
(coinbase : Address)
(actions : list (Address * ChainAction))
: option ChainBuilder :=
let (ifc, val) := cur in
let new_val := ifc.(cbi_add_block) val coinbase actions in
option_map (build_chain_builder ifc) new_val.
...@@ -321,3 +321,13 @@ Qed. ...@@ -321,3 +321,13 @@ Qed.
Definition contract : Contract Setup Msg State := Definition contract : Contract Setup Msg State :=
build_contract version init receive. build_contract version init receive.
(*
(* This first property states that the Congress will only send out actions
to be performed if there is a matching CreateProposal somewhere in the
past. That is, no CreateProposal can lead to two batches of actions being
sent out, and the actions correspond to the ones passed in CreateProposal. *)
Theorem congress_no_unmatched_actions
(chain : Chain)
(
*)
...@@ -42,27 +42,27 @@ Instance eta_local_chain : Settable _ := ...@@ -42,27 +42,27 @@ Instance eta_local_chain : Settable _ :=
<*> lc_updates)%settable. <*> lc_updates)%settable.
(* Contains full information about a chain, including contracts *) (* Contains full information about a chain, including contracts *)
Record LocalChainEnvironment := Record LocalChainBuilder :=
build_local_chain_environment { build_local_chain_builder {
lce_lc : LocalChain; lcb_lc : LocalChain;
lce_contracts : list (Address * WeakContract); lcb_contracts : list (Address * WeakContract);
}. }.
Instance eta_local_chain_environment : Settable _ := Instance eta_local_chain_builder : Settable _ :=
mkSettable mkSettable
((constructor build_local_chain_environment) <*> lce_lc ((constructor build_local_chain_builder) <*> lcb_lc
<*> lce_contracts)%settable. <*> lcb_contracts)%settable.
Definition genesis_block : Block := Definition genesis_block : Block :=
{| block_header := {| block_number := 0; |}; {| block_header := {| block_number := 0; |};
block_txs := [] |}. block_txs := [] |}.
Definition initial_chain : LocalChainEnvironment := Definition initial_chain_builder : LocalChainBuilder :=
{| lce_lc := {| lc_blocks := [genesis_block]; {| lcb_lc := {| lc_blocks := [genesis_block];
lc_updates := lc_updates :=
[{| upd_contracts := FMap.empty; [{| upd_contracts := FMap.empty;
upd_txs := [] |}] |}; upd_txs := [] |}] |};
lce_contracts := []; lcb_contracts := [];
|}. |}.
Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain := Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
...@@ -102,7 +102,7 @@ Definition lc_contract_state (lc : LocalChain) (addr : Address) ...@@ -102,7 +102,7 @@ Definition lc_contract_state (lc : LocalChain) (addr : Address)
find_first (fun u => FMap.find addr u.(upd_contracts)) lc.(lc_updates). find_first (fun u => FMap.find addr u.(upd_contracts)) lc.(lc_updates).
Definition lc_interface : ChainInterface := Definition lc_interface : ChainInterface :=
{| ci_chain_type := LocalChain; {| ci_type := LocalChain;
ci_chain_at := lc_chain_at; ci_chain_at := lc_chain_at;
ci_head_block := lc_head_block; ci_head_block := lc_head_block;
ci_incoming_txs := lc_incoming_txs; ci_incoming_txs := lc_incoming_txs;
...@@ -112,7 +112,7 @@ Definition lc_interface : ChainInterface := ...@@ -112,7 +112,7 @@ Definition lc_interface : ChainInterface :=
Section ExecuteActions. Section ExecuteActions.
Context (initial_lce : LocalChainEnvironment). Context (initial_lcb : LocalChainBuilder).
Record ExecutionContext := Record ExecutionContext :=
build_execution_context { build_execution_context {
...@@ -127,13 +127,13 @@ Section ExecuteActions. ...@@ -127,13 +127,13 @@ Section ExecuteActions.
<*> new_update <*> new_update
<*> new_contracts)%settable. <*> new_contracts)%settable.
Let make_acc_lce ec := Let make_acc_lcb ec :=
let new_lc := (initial_lce.(lce_lc))[[lc_updates ::= cons ec.(new_update)]] in let new_lc := (initial_lcb.(lcb_lc))[[lc_updates ::= cons ec.(new_update)]] in
let new_contracts := ec.(new_contracts) ++ initial_lce.(lce_contracts) in let new_contracts := ec.(new_contracts) ++ initial_lcb.(lcb_contracts) in
{| lce_lc := new_lc; lce_contracts := new_contracts |}. {| lcb_lc := new_lc; lcb_contracts := new_contracts |}.
Let make_acc_c lce : Chain := Let make_acc_c lcb : Chain :=
build_chain lc_interface lce.(lce_lc). build_chain lc_interface lcb.(lcb_lc).
Let verify_amount (c : Chain) (addr : Address) (amt : Amount) Let verify_amount (c : Chain) (addr : Address) (amt : Amount)
: option unit := : option unit :=
...@@ -141,11 +141,11 @@ Section ExecuteActions. ...@@ -141,11 +141,11 @@ Section ExecuteActions.
then Some tt then Some tt
else None. else None.
Let find_contract addr lce := Let find_contract addr lcb :=
option_map snd (find (fun p => fst p =? addr) lce.(lce_contracts)). option_map snd (find (fun p => fst p =? addr) lcb.(lcb_contracts)).
Let verify_no_contract addr lce := Let verify_no_contract addr lcb :=
match find_contract addr lce with match find_contract addr lcb with
| Some _ => None | Some _ => None
| None => Some tt | None => Some tt
end. end.
...@@ -160,12 +160,12 @@ Section ExecuteActions. ...@@ -160,12 +160,12 @@ Section ExecuteActions.
match gas, act with match gas, act with
| 0, _ => None | 0, _ => None
| S gas, (from, act) => | S gas, (from, act) =>
let acc_lce := make_acc_lce ec in let acc_lcb := make_acc_lcb ec in
let acc_c := make_acc_c acc_lce in let acc_c := make_acc_c acc_lcb in
let deploy_contract amount (wc : WeakContract) setup := let deploy_contract amount (wc : WeakContract) setup :=
do verify_amount acc_c from amount; do verify_amount acc_c from amount;
let contract_addr := 1 + length acc_lce.(lce_contracts) in (* todo *) let contract_addr := 1 + length acc_lcb.(lcb_contracts) in (* todo *)
do verify_no_contract contract_addr acc_lce; do verify_no_contract contract_addr acc_lcb;
let ctx := {| ctx_chain := acc_c; let ctx := {| ctx_chain := acc_c;
ctx_from := from; ctx_from := from;
ctx_contract_address := contract_addr; ctx_contract_address := contract_addr;
...@@ -202,16 +202,16 @@ Section ExecuteActions. ...@@ -202,16 +202,16 @@ Section ExecuteActions.
let new_cu := ec.(new_update)[[upd_txs ::= cons new_tx]] in let new_cu := ec.(new_update)[[upd_txs ::= cons new_tx]] in
let new_ec := ec[[new_update := new_cu]] in let new_ec := ec[[new_update := new_cu]] in
let new_ec := if record then new_ec[[block_txs ::= cons new_tx]] else new_ec in let new_ec := if record then new_ec[[block_txs ::= cons new_tx]] else new_ec in
match find_contract to acc_lce with match find_contract to acc_lcb with
| None => match msg_opt with | None => match msg_opt with
| Some _ => None (* Sending message to non-contract *) | Some _ => None (* Sending message to non-contract *)
| None => Some new_ec | None => Some new_ec
end end
| Some wc => | Some wc =>
let acc_lce := make_acc_lce new_ec in let acc_lcb := make_acc_lcb new_ec in
let acc_c := make_acc_c acc_lce in let acc_c := make_acc_c acc_lcb in
let contract_addr := to in let contract_addr := to in
do state <- lc_contract_state acc_lce.(lce_lc) contract_addr; do state <- lc_contract_state acc_lcb.(lcb_lc) contract_addr;
let (ver, init, recv) := wc in let (ver, init, recv) := wc in
let ctx := {| ctx_chain := acc_c; let ctx := {| ctx_chain := acc_c;
ctx_from := from; ctx_from := from;
...@@ -244,7 +244,7 @@ Section ExecuteActions. ...@@ -244,7 +244,7 @@ Section ExecuteActions.
(coinbase : Tx) (coinbase : Tx)
(actions : list (Address * ChainAction)) (actions : list (Address * ChainAction))
(gas : nat) (gas : nat)
: option LocalChainEnvironment := : option LocalChainBuilder :=
let fix go acts ec := let fix go acts ec :=
match acts with match acts with
| [] => Some ec | [] => Some ec
...@@ -257,25 +257,32 @@ Section ExecuteActions. ...@@ -257,25 +257,32 @@ Section ExecuteActions.
upd_txs := [coinbase] |}; upd_txs := [coinbase] |};
new_contracts := [] |} in new_contracts := [] |} in
do ec <- go actions empty_ec; do ec <- go actions empty_ec;
let new_lce := make_acc_lce ec in let new_lcb := make_acc_lcb ec in
let recorded_txs := ec.(block_txs) in let recorded_txs := ec.(block_txs) in
let hdr := {| block_number := length (initial_lce.(lce_lc).(lc_blocks)) |} in let hdr := {| block_number := length (initial_lcb.(lcb_lc).(lc_blocks)) |} in
let block := build_block hdr recorded_txs in let block := build_block hdr recorded_txs in
let new_lce := new_lce[[lce_lc := new_lce.(lce_lc)[[lc_blocks ::= cons block]]]] in let new_lcb := new_lcb[[lcb_lc := new_lcb.(lcb_lc)[[lc_blocks ::= cons block]]]] in
Some new_lce. Some new_lcb.
End ExecuteActions. End ExecuteActions.
(* Adds a block to the chain by executing the specified chain actions. (* Adds a block to the chain by executing the specified chain actions.
Returns the new chain if the execution succeeded (for instance, Returns the new chain if the execution succeeded (for instance,
transactions need enough funds, contracts should not reject, etc. *) transactions need enough funds, contracts should not reject, etc. *)
Definition add_block Definition add_block
(lcb : LocalChainBuilder)
(coinbase : Address) (coinbase : Address)
(actions : list (Address (*from*) * ChainAction)) (actions : list (Address (*from*) * ChainAction))
(lce : LocalChainEnvironment) : option LocalChainBuilder :=
: option LocalChainEnvironment :=
let coinbase_tx := let coinbase_tx :=
{| tx_from := 0; {| tx_from := 0;
tx_to := coinbase; tx_to := coinbase;
tx_amount := 50; tx_amount := 50;
tx_body := tx_empty |} in tx_body := tx_empty |} in
execute_actions lce coinbase_tx actions 10. execute_actions lcb coinbase_tx actions 10.
Definition lc_builder_interface : ChainBuilderInterface :=
{| cbi_chain_interface := lc_interface;
cbi_type := LocalChainBuilder;
cbi_chain lcb := lcb.(lcb_lc);
cbi_initial := initial_chain_builder;
cbi_add_block := add_block; |}.
From SmartContracts Require Import Monads. From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain. From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain. From SmartContracts Require LocalBlockchain.
From SmartContracts Require Import Congress. From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak. From SmartContracts Require Import Oak.
From SmartContracts Require Import Containers. From SmartContracts Require Import Containers.
...@@ -16,27 +16,25 @@ Section LocalBlockchainTests. ...@@ -16,27 +16,25 @@ Section LocalBlockchainTests.
Let person_2 := 12. Let person_2 := 12.
Let person_3 := 13. Let person_3 := 13.
Let chain1 :=
initial_chain_builder LocalBlockchain.lc_builder_interface.
Let otry x := Let otry x :=
match x with match x with
| Some y => y | Some y => y
| None => LocalBlockchain.initial_chain | None => chain1
end. end.
Let lce_to_chain l := build_chain lc_interface l.(lce_lc) .
Local Coercion lce_to_chain : LocalChainEnvironment >-> Chain.
Let chain1 :=
LocalBlockchain.initial_chain.
(* Baker mines an empty block (and gets some coins) *) (* Baker mines an empty block (and gets some coins) *)
Let chain2 := Let chain2 :=
otry (LocalBlockchain.add_block baker [] chain1). otry (chain1.(add_block) baker []).
Compute (account_balance chain2 person_1). Compute (account_balance chain2 person_1).
Compute (account_balance chain2 baker). Compute (account_balance chain2 baker).
(* Baker transfers 10 coins to person_1 *) (* Baker transfers 10 coins to person_1 *)
Let chain3 := Let chain3 :=
otry (LocalBlockchain.add_block baker [(baker, act_transfer person_1 10)] chain2). otry (chain2.(add_block) baker [(baker, act_transfer person_1 10)]).
Compute (account_balance chain3 person_1). Compute (account_balance chain3 person_1).
Compute (account_balance chain3 baker). Compute (account_balance chain3 baker).
...@@ -53,7 +51,7 @@ Section LocalBlockchainTests. ...@@ -53,7 +51,7 @@ Section LocalBlockchainTests.
create_deployment 5 Congress.contract setup. create_deployment 5 Congress.contract setup.
Let chain4 := Let chain4 :=
otry (LocalBlockchain.add_block baker [(person_1, deploy_congress)] chain3). otry (chain3.(add_block) baker [(person_1, deploy_congress)]).
Compute (contract_deployment chain4 congress_1). Compute (contract_deployment chain4 congress_1).
Compute (account_balance chain4 person_1). Compute (account_balance chain4 person_1).
...@@ -94,8 +92,8 @@ Section LocalBlockchainTests. ...@@ -94,8 +92,8 @@ Section LocalBlockchainTests.
Let add_person p := Let add_person p :=
congress_ifc.(call) 0 (add_member p). congress_ifc.(call) 0 (add_member p).
Let chain5 := otry (LocalBlockchain.add_block baker [(person_1, add_person person_1) ; Let chain5 := otry (chain4.(add_block) baker [(person_1, add_person person_1);
(person_1, add_person person_2)] chain4). (person_1, add_person person_2)]).
Compute (FSet.elements (congress_state chain5).(members)). Compute (FSet.elements (congress_state chain5).(members)).
Compute (account_balance chain5 congress_1). Compute (account_balance chain5 congress_1).
...@@ -105,22 +103,22 @@ Section LocalBlockchainTests. ...@@ -105,22 +103,22 @@ Section LocalBlockchainTests.
Let create_proposal_call := Let create_proposal_call :=
congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]). congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
Let chain6 := otry (LocalBlockchain.add_block baker [(person_1, create_proposal_call)] chain5). Let chain6 := otry (chain5.(add_block) baker [(person_1, create_proposal_call)]).
Compute (FMap.elements (congress_state chain6).(proposals)). Compute (FMap.elements (congress_state chain6).(proposals)).
(* person_1 and person_2 vote for the proposal *) (* person_1 and person_2 vote for the proposal *)
Let vote_proposal := Let vote_proposal :=
congress_ifc.(call) 0 (vote_for_proposal 1). congress_ifc.(call) 0 (vote_for_proposal 1).
Let chain7 := otry (LocalBlockchain.add_block baker [(person_1, vote_proposal); Let chain7 := otry (chain6.(add_block) baker [(person_1, vote_proposal);
(person_2, vote_proposal)] chain6). (person_2, vote_proposal)]).
Compute (FMap.elements (congress_state chain7).(proposals)). Compute (FMap.elements (congress_state chain7).(proposals)).
(* Person 3 finishes the proposal (anyone can finish it after voting) *) (* Person 3 finishes the proposal (anyone can finish it after voting) *)
Let finish_proposal := Let finish_proposal :=
congress_ifc.(call) 0 (finish_proposal 1). congress_ifc.(call) 0 (finish_proposal 1).
Let chain8 := otry (LocalBlockchain.add_block baker [(person_3, finish_proposal)] chain7). Let chain8 := otry (chain7.(add_block) baker [(person_3, finish_proposal)]).
Compute (FMap.elements (congress_state chain8).(proposals)). Compute (FMap.elements (congress_state chain8).(proposals)).
(* Balances before: *) (* Balances before: *)
Compute (account_balance chain7 congress_1). Compute (account_balance chain7 congress_1).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment