Commit 0bcb6c0c authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Add a working example using the Congress

This adds a small example that uses a local blockchain to deploy a
congress and do a transfer with it.

Also fixes bugs to make this work.
parent c66e14a1
Pipeline #11191 failed with stage
in 2 minutes and 21 seconds
...@@ -3,6 +3,7 @@ src/Blockchain.v ...@@ -3,6 +3,7 @@ src/Blockchain.v
src/Congress.v src/Congress.v
src/Extras.v src/Extras.v
src/LocalBlockchain.v src/LocalBlockchain.v
src/LocalBlockchainTests.v
src/Monads.v src/Monads.v
src/Oak.v src/Oak.v
-R vendor/record-update RecordUpdate -R vendor/record-update RecordUpdate
......
...@@ -168,6 +168,8 @@ Definition contract_to_weak_contract ...@@ -168,6 +168,8 @@ Definition contract_to_weak_contract
end in end in
build_weak_contract c.(version) weak_init weak_recv. build_weak_contract c.(version) weak_init weak_recv.
Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* (*
Record ContractInterface (setup_ty msg_ty state_ty : Type) := Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
build_contract_interface { build_contract_interface {
......
...@@ -59,11 +59,12 @@ Definition genesis_block : Block := ...@@ -59,11 +59,12 @@ Definition genesis_block : Block :=
{| block_header := {| block_number := 0; |}; {| block_header := {| block_number := 0; |};
block_txs := nil |}. block_txs := nil |}.
Definition initial_chain : LocalChain := Definition initial_chain : LocalChainEnvironment :=
{| lc_blocks := [genesis_block]; {| lce_lc := {| lc_blocks := [genesis_block];
lc_updates := lc_updates :=
[{| upd_contracts := []%map; [{| upd_contracts := []%map;
upd_txs := nil |}] upd_txs := nil |}] |};
lce_contracts := nil;
|}. |}.
Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain := Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
...@@ -165,7 +166,7 @@ Section ExecuteActions. ...@@ -165,7 +166,7 @@ Section ExecuteActions.
let acc_c := make_acc_c acc_lce in let acc_c := make_acc_c acc_lce 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 := 0 in (* todo *) let contract_addr := 1 + length acc_lce.(lce_contracts) in (* todo *)
do verify_no_contract contract_addr acc_lce; do verify_no_contract contract_addr acc_lce;
let ctx := {| ctx_chain := acc_c; let ctx := {| ctx_chain := acc_c;
ctx_from := from; ctx_from := from;
...@@ -204,7 +205,10 @@ Section ExecuteActions. ...@@ -204,7 +205,10 @@ Section ExecuteActions.
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_lce with
| None => Some new_ec | None => match msg_opt with
| Some _ => None (* Sending message to non-contract *)
| None => Some new_ec
end
| Some wc => | Some wc =>
let acc_lce := make_acc_lce new_ec in let acc_lce := make_acc_lce new_ec in
let acc_c := make_acc_c acc_lce in let acc_c := make_acc_c acc_lce in
......
From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain.
From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak.
From Containers Require Import SetInterface MapInterface OrderedTypeEx.
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.
Section LocalBlockchainTests.
(* Addresses *)
Let congress_1 := 1.
Let congress_2 := 2.
Let baker := 10.
Let person_1 := 11.
Let person_2 := 12.
Let person_3 := 13.
Let otry x :=
match x with
| Some y => y
| None => LocalBlockchain.initial_chain
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 *)
Let chain2 := otry (LocalBlockchain.add_block baker [] chain1).
Compute (account_balance chain2 person_1).
Compute (account_balance chain2 baker).
(* Baker transfers 10 coins to person_1 *)
Let chain3 := otry (LocalBlockchain.add_block baker [(baker, act_transfer person_1 10)] chain2).
Compute (account_balance chain3 person_1).
Compute (account_balance chain3 baker).
Let setup_rules :=
{| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
margin_needed_permille := 500;
debating_period_in_blocks := 0; |}.
Let deploy_congress : ChainAction :=
act_deploy 5 Congress.contract (serialize setup_rules).
Let chain4 := otry (LocalBlockchain.add_block baker [(person_1, deploy_congress)] chain3).
Compute (account_balance chain4 person_1).
Compute (account_balance chain4 baker).
Compute (account_balance chain4 congress_1).
(* person_1 adds person_1 and person_2 as members of congress *)
Let add_person p :=
act_call congress_1 0 (serialize (add_member p)).
Let chain5 := otry (LocalBlockchain.add_block baker [(person_1, add_person person_1) ;
(person_1, add_person person_2)] chain4).
Compute (account_balance chain5 person_1).
Compute (chain5.(lce_lc).(lc_updates)).
Let congress_state chain : option Congress.State :=
deserialize =<< (contract_state chain congress_1).
Compute (match congress_state chain5 with
| Some x => SetInterface.elements x.(members)
| None => []
end).
Compute (account_balance chain5 congress_1).
(* person_1 creates a proposal to send 3 coins to person_3 using funds
of the contract *)
Let create_proposal_msg :=
serialize (create_proposal [cact_transfer person_3 3]).
Let create_proposal_call :=
act_call congress_1 0 create_proposal_msg.
Let chain6 := otry (LocalBlockchain.add_block baker [(person_1, create_proposal_call)] chain5).
Compute (match congress_state chain6 with
| Some x => MapInterface.elements x.(proposals)
| None => []
end).
(* person_1 and person_2 votes for the proposal *)
Let vote_proposal :=
act_call congress_1 0 (serialize (vote_for_proposal 1)).
Let chain7 := otry (LocalBlockchain.add_block baker [(person_1, vote_proposal);
(person_2, vote_proposal)] chain6).
Compute (match congress_state chain7 with
| Some x => MapInterface.elements x.(proposals)
| None => []
end).
(* Finish the proposal *)
Let finish_proposal :=
act_call congress_1 0 (serialize (finish_proposal 1)).
Let chain8 := otry (LocalBlockchain.add_block baker [(person_1, finish_proposal)] chain7).
(* Balance before: *)
Compute (account_balance chain7 person_3).
(* Balance after: *)
Compute (account_balance chain8 person_3).
End LocalBlockchainTests.
...@@ -4,8 +4,8 @@ Definition option_bind {A B : Type} (v : option A) (f : A -> option B) : option ...@@ -4,8 +4,8 @@ Definition option_bind {A B : Type} (v : option A) (f : A -> option B) : option
| None => None | None => None
end. end.
Notation "c >>= f" := (option_bind f c) (at level 50, left associativity). Notation "c >>= f" := (option_bind c f) (at level 50, left associativity).
Notation "f =<< c" := (option_bind f c) (at level 51, right associativity). Notation "f =<< c" := (option_bind c f) (at level 51, right associativity).
Notation "'do' x <- c1 ; c2" := Notation "'do' x <- c1 ; c2" :=
(option_bind c1 (fun x => c2)) (option_bind c1 (fun x => c2))
......
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