Commit 11c14413 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Add Blockchain.get_contract_interface and create_deployment

These functions allow interacting with contracts in a strongly-typed
manner without having to serialize/deserialize manually.
Also adjust test to use these.
parent 0bcb6c0c
Pipeline #11203 failed with stage
in 2 minutes and 51 seconds
...@@ -21,7 +21,7 @@ Definition BlockHash := string. ...@@ -21,7 +21,7 @@ Definition BlockHash := string.
Definition Version := nat. Definition Version := nat.
Record ContractDeployment := Record ContractDeployment :=
{ build_contract_deployment {
deployment_version : Version; deployment_version : Version;
(* todo: model any type/constraints so we can have this. Right now the (* todo: model any type/constraints so we can have this. Right now the
problem is that Congress messages can contain _any_ oak value (for problem is that Congress messages can contain _any_ oak value (for
...@@ -146,11 +146,11 @@ Arguments receive {_ _ _ _ _ _} contract ctx state msg : rename. ...@@ -146,11 +146,11 @@ Arguments receive {_ _ _ _ _ _} contract ctx state msg : rename.
Arguments build_contract {_ _ _ _ _ _}. Arguments build_contract {_ _ _ _ _ _}.
Definition contract_to_weak_contract Definition contract_to_weak_contract
{A B C : Type} {setup_ty msg_ty state_ty : Type}
{eq_a : OakTypeEquivalence A} {_ : OakTypeEquivalence setup_ty}
{eq_b : OakTypeEquivalence B} {_ : OakTypeEquivalence msg_ty}
{eq_c : OakTypeEquivalence C} {_ : OakTypeEquivalence state_ty}
(c : Contract A B C) : WeakContract := (c : Contract setup_ty msg_ty state_ty) : WeakContract :=
let weak_init ctx oak_setup := let weak_init ctx oak_setup :=
do setup <- deserialize oak_setup; do setup <- deserialize oak_setup;
do state <- c.(init) ctx setup; do state <- c.(init) ctx setup;
...@@ -170,51 +170,53 @@ Definition contract_to_weak_contract ...@@ -170,51 +170,53 @@ Definition contract_to_weak_contract
Coercion contract_to_weak_contract : Contract >-> WeakContract. Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* Definition create_deployment
Record ContractInterface (setup_ty msg_ty state_ty : Type) := {setup_ty msg_ty state_ty : Type}
{_ : OakTypeEquivalence setup_ty}
{_ : OakTypeEquivalence msg_ty}
{_ : OakTypeEquivalence state_ty}
(amount : Amount)
(contract : Contract setup_ty msg_ty state_ty)
(setup : setup_ty)
: ChainAction :=
act_deploy amount contract (serialize setup).
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 *)
contract_address : Address; contract_address : Address;
(* Version of the contract *)
contract_version : Version;
(* The setup that was passed when the contract was deployed *) (* The setup that was passed when the contract was deployed *)
setup : setup_ty; contract_setup : setup_ty;
(* Obtain the state at some point of time *) (* Obtain the state at some point of time *)
get_state : Chain -> option state_ty; get_state : Chain -> option state_ty;
(* Make an action transferring money to the contract without (* Make an action transferring money to the contract without
a message *) a message *)
transfer : Amount -> ContractAction; transfer : Amount -> ChainAction;
(* Make an action calling the contract *) (* Make an action calling the contract *)
call : Amount -> msg_ty -> ContractAction; call : Amount -> msg_ty -> ChainAction;
}. }.
*)
(* Arguments ContractInterface _ _ _ : clear implicits.
(* todo: this should be easier -- we want actual strong typed Arguments build_contract_interface {_ _ _}.
interface by equivalence of oak type (iterated product, for instance)
to types in contracts. Right now the interface received allows you
only to interact with a contract using interpreted types. *)
Definition get_contract_interface Definition get_contract_interface
(setup_oty msg_oty state_oty : OakType)
(chain : Chain) (chain : Chain)
(addr : Address) (addr : Address)
: option (ContractInterface (setup_ty msg_ty state_ty : Type)
(interp_type setup_oty) {_ : OakTypeEquivalence setup_ty}
(interp_type msg_oty) {_ : OakTypeEquivalence msg_ty}
(interp_type state_oty)) := {_ : OakTypeEquivalence state_ty}
do deployment <- chain.(get_contract_deployment) addr; : option (ContractInterface setup_ty msg_ty state_ty) :=
let (deploy_setup_oty, deploy_setup) := deployment.(deployment_setup) in do 'build_contract_deployment ver ov_setup <- contract_deployment chain addr;
match eq_oak_type_dec setup_oty deploy_setup_oty, do setup <- deserialize ov_setup;
eq_oak_type_dec msg_oty deployment.(deployment_msg_ty), let ifc_get_state chain := deserialize =<< (contract_state chain addr) in
eq_oak_type_dec state_oty deployment.(deployment_state_ty) let ifc_transfer := act_transfer addr in
with let ifc_call amount msg := act_call addr amount (serialize msg) in
| left _, left _, left _ => Some {| contract_address := addr;
Some {| contract_version := ver;
contract_address := addr; contract_setup := setup;
setup := let x : interp_type setup_oty := ltac:(subst; exact deploy_setup) in x; get_state := ifc_get_state;
get_state futureChain := transfer := ifc_transfer;
do val <- futureChain.(get_contract_state) addr; call := ifc_call; |}.
extract_oak_value state_oty val;
transfer := act_transfer addr;
call amt msg := act_call addr amt (build_oak_value msg_oty msg) |}
| _, _, _ => None
end.
*)
...@@ -3,7 +3,7 @@ From SmartContracts Require Import Blockchain. ...@@ -3,7 +3,7 @@ From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain. From SmartContracts Require Import LocalBlockchain.
From SmartContracts Require Import Congress. From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak. From SmartContracts Require Import Oak.
From Containers Require Import SetInterface MapInterface OrderedTypeEx. From Containers Require SetInterface MapInterface OrderedTypeEx.
From Coq Require Import List. From Coq Require Import List.
From Coq Require Import ZArith. From Coq Require Import ZArith.
Import ListNotations. Import ListNotations.
...@@ -11,7 +11,6 @@ Import ListNotations. ...@@ -11,7 +11,6 @@ Import ListNotations.
Section LocalBlockchainTests. Section LocalBlockchainTests.
(* Addresses *) (* Addresses *)
Let congress_1 := 1. Let congress_1 := 1.
Let congress_2 := 2.
Let baker := 10. Let baker := 10.
Let person_1 := 11. Let person_1 := 11.
Let person_2 := 12. Let person_2 := 12.
...@@ -25,81 +24,107 @@ Section LocalBlockchainTests. ...@@ -25,81 +24,107 @@ Section LocalBlockchainTests.
Let lce_to_chain l := build_chain lc_interface l.(lce_lc) . Let lce_to_chain l := build_chain lc_interface l.(lce_lc) .
Local Coercion lce_to_chain : LocalChainEnvironment >-> Chain. Local Coercion lce_to_chain : LocalChainEnvironment >-> Chain.
Let chain1 := LocalBlockchain.initial_chain. Let chain1 :=
(* Baker mines an empty block *) LocalBlockchain.initial_chain.
Let chain2 := otry (LocalBlockchain.add_block baker [] chain1).
(* Baker mines an empty block (and gets some coins) *)
Let chain2 :=
otry (LocalBlockchain.add_block baker [] chain1).
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 := otry (LocalBlockchain.add_block baker [(baker, act_transfer person_1 10)] chain2). Let chain3 :=
otry (LocalBlockchain.add_block baker [(baker, act_transfer person_1 10)] chain2).
Compute (account_balance chain3 person_1). Compute (account_balance chain3 person_1).
Compute (account_balance chain3 baker). Compute (account_balance chain3 baker).
(* person_1 deploys a Congress contract *)
Let setup_rules := Let setup_rules :=
{| min_vote_count_permille := 200; (* 20% of congress needs to vote *) {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
margin_needed_permille := 500; margin_needed_permille := 500;
debating_period_in_blocks := 0; |}. debating_period_in_blocks := 0; |}.
Let setup := Congress.build_setup setup_rules.
Let deploy_congress : ChainAction := Let deploy_congress : ChainAction :=
act_deploy 5 Congress.contract (serialize setup_rules). create_deployment 5 Congress.contract setup.
Let chain4 := otry (LocalBlockchain.add_block baker [(person_1, deploy_congress)] chain3). Let chain4 :=
otry (LocalBlockchain.add_block baker [(person_1, deploy_congress)] chain3).
Compute (contract_deployment chain4 congress_1).
Compute (account_balance chain4 person_1). Compute (account_balance chain4 person_1).
Compute (account_balance chain4 baker). Compute (account_balance chain4 baker).
Compute (account_balance chain4 congress_1). Compute (account_balance chain4 congress_1).
Let congress_ifc :=
match get_contract_interface
chain4 congress_1
Congress.Setup Congress.Msg Congress.State with
| Some x => x
(* This stuff is just to make the test example easier
since we know it will not fail *)
| None =>
build_contract_interface
0
0
setup
(fun c => None)
(fun a => deploy_congress)
(fun a m => deploy_congress)
end.
Let congress_state chain : Congress.State :=
match congress_ifc.(get_state) chain with
| Some s => s
| None => {| owner := 0;
state_rules := setup_rules;
proposals := MapInterface.empty Proposal;
next_proposal_id := 0;
members := SetInterface.empty |}
end.
Compute (congress_ifc.(get_state) chain4).
Compute (SetInterface.elements (congress_state chain4).(members)).
(* person_1 adds person_1 and person_2 as members of congress *) (* person_1 adds person_1 and person_2 as members of congress *)
Let add_person p := Let add_person p :=
act_call congress_1 0 (serialize (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 (LocalBlockchain.add_block baker [(person_1, add_person person_1) ;
(person_1, add_person person_2)] chain4). (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 := Compute (SetInterface.elements (congress_state chain4).(members)).
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). Compute (account_balance chain5 congress_1).
(* person_1 creates a proposal to send 3 coins to person_3 using funds (* person_1 creates a proposal to send 3 coins to person_3 using funds
of the contract *) of the contract *)
Let create_proposal_msg :=
serialize (create_proposal [cact_transfer person_3 3]).
Let create_proposal_call := Let create_proposal_call :=
act_call congress_1 0 create_proposal_msg. 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 (LocalBlockchain.add_block baker [(person_1, create_proposal_call)] chain5).
Compute (match congress_state chain6 with Compute (MapInterface.elements (congress_state chain6).(proposals)).
| Some x => MapInterface.elements x.(proposals)
| None => []
end).
(* person_1 and person_2 votes for the proposal *) (* person_1 and person_2 votes for the proposal *)
Let vote_proposal := Let vote_proposal :=
act_call congress_1 0 (serialize (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 (LocalBlockchain.add_block baker [(person_1, vote_proposal);
(person_2, vote_proposal)] chain6). (person_2, vote_proposal)] chain6).
Compute (match congress_state chain7 with Compute (MapInterface.elements (congress_state chain7).(proposals)).
| Some x => MapInterface.elements x.(proposals)
| None => []
end).
(* Finish the proposal *) (* Finish the proposal *)
Let finish_proposal := Let finish_proposal :=
act_call congress_1 0 (serialize (finish_proposal 1)). congress_ifc.(call) 0 (finish_proposal 1).
Let chain8 := otry (LocalBlockchain.add_block baker [(person_1, finish_proposal)] chain7). Let chain8 := otry (LocalBlockchain.add_block baker [(person_1, finish_proposal)] chain7).
(* Balances before: *)
(* Balance before: *) Compute (account_balance chain7 congress_1).
Compute (account_balance chain7 person_3). Compute (account_balance chain7 person_3).
(* Balance after: *) (* Balances after: *)
Compute (account_balance chain8 congress_1).
Compute (account_balance chain8 person_3). Compute (account_balance chain8 person_3).
End LocalBlockchainTests. End LocalBlockchainTests.
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