Commit 357cd8df authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Implement execution in LocalBlockChain

This implements a depth first execution of chain actions with support
for deploying contracts from contracts and calling into other contracts
recursively. To support these things, contracts need to exhibit a
bijection of their types from and to OakValue. This machinery is modeled
with type classes. Then, use this to avoid having to store strongly
typed contracts anywhere; instead, a contract can be converted to a
WeakContract instance (using a coercion). The WeakContract verifies that
messages and states serialize/deserialize correctly and then passes
everything along to the strongly typed contract under the hood.
parent f333a5f7
Pipeline #11185 failed with stage
in 6 minutes and 34 seconds
-R src SmartContracts
src/Blockchain.v
src/Congress.v
src/Extras.v
src/LocalBlockchain.v
src/Monads.v
src/Oak.v
-R vendor/record-update RecordUpdate
......
From Coq Require Import String.
From Coq Require OrderedTypeEx.
From Coq Require Import List.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Extras.
Definition Address := nat.
Delimit Scope address_scope with address.
......@@ -22,8 +23,12 @@ Definition Version := nat.
Record ContractDeployment :=
{
deployment_version : Version;
(* todo: model any type/constraints so we can have this. Right now the
problem is that Congress messages can contain _any_ oak value (for
the congress to send out), so there is no bijection from its message type
to oak type.
deployment_msg_ty : OakType;
deployment_state_ty : OakType;
deployment_state_ty : OakType; *)
deployment_setup : OakValue;
}.
......@@ -51,36 +56,18 @@ Record Block :=
block_txs : list Tx;
}.
(* This needs to be polymorphic because ... for reasons. LocalChain does not
work if not. A smaller repro is:
Class interface :=
{ ty : Type;
func : ty -> ty;
}.
(* the problem is that the implementation contains functions taking the
interface *)
Record impl :=
{
callback : interface -> nat;
}.
Definition func_concrete (i : impl) : impl := i.
Instance impl_interface : interface :=
{| ty := impl; func := func_concrete |}.
todo: come back to this and understand universe polymorphism in depth. *)
Polymorphic Record ChainInterface :=
Record ChainInterface :=
build_chain_interface {
(* Would be nice to encapsulate ChainInterface somewhat here
and avoid these ugly prefixed names *)
ci_chain_type : Type;
ci_chain_at : ci_chain_type -> BlockId -> option ci_chain_type;
(* Last finished block. During contract execution, this is the previous
block, i.e. this block does _not_ contain the transaction that caused
the contract to be called *)
ci_head_block : ci_chain_type -> Block;
ci_incoming_txs : ci_chain_type -> Address -> list Tx;
ci_outgoing_txs : ci_chain_type -> Address -> list Tx;
ci_contract_deployment : ci_chain_type -> Address -> option ContractDeployment;
ci_contract_state : ci_chain_type -> Address -> option OakValue;
}.
......@@ -90,27 +77,31 @@ Record Chain :=
chain_val : chain_ci.(ci_chain_type);
}.
Definition chain_at (c : Chain) (bid : BlockId) : option Chain :=
do x <- c.(chain_ci).(ci_chain_at) c.(chain_val) bid;
Some {| chain_val := x |}.
Definition head_block (c : Chain) :=
c.(chain_ci).(ci_head_block) c.(chain_val).
Definition block_at (c : Chain) (bid : BlockId) : option Block :=
do c <- chain_at c bid; Some (head_block c).
Definition incoming_txs (c : Chain) :=
c.(chain_ci).(ci_incoming_txs) c.(chain_val).
Section ChainAccessors.
Context (chain : Chain).
Definition outgoing_txs (c : Chain) :=
c.(chain_ci).(ci_outgoing_txs) c.(chain_val).
Let g {A : Type} (p : forall chain : ChainInterface, ci_chain_type chain -> A)
:= p chain.(chain_ci) chain.(chain_val).
Definition contract_deployment (c : Chain) :=
c.(chain_ci).(ci_contract_deployment) c.(chain_val).
Definition chain_at (bid : BlockId) : option Chain :=
do x <- chain.(chain_ci).(ci_chain_at) chain.(chain_val) bid;
Some {| chain_val := x |}.
Definition contract_state (c : Chain) :=
c.(chain_ci).(ci_contract_state) c.(chain_val).
Definition head_block := g ci_head_block.
Definition incoming_txs := g ci_incoming_txs.
Definition outgoing_txs := g ci_outgoing_txs.
Definition contract_state := g ci_contract_state.
Definition account_balance (addr : Address) : Amount :=
let sum := fold_right Nat.add 0 in
let sum_amounts txs := sum (map tx_amount txs) in
sum_amounts (incoming_txs addr) - sum_amounts (outgoing_txs addr).
Definition contract_deployment (addr : Address) : option ContractDeployment :=
let to_dep tx := match tx.(tx_body) with
| tx_deploy dep => Some dep
| _ => None
end in
find_first to_dep (incoming_txs addr).
End ChainAccessors.
Inductive ContractCallContext :=
build_contract_call_ctx {
......@@ -127,12 +118,55 @@ Inductive ContractCallContext :=
Inductive ChainAction :=
| act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy
{setup_ty msg_ty state_ty : Type}
| act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
with WeakContract :=
| build_weak_contract
(version : Version)
(init : ContractCallContext -> setup_ty -> option state_ty)
(receive : ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction)).
(init : ContractCallContext -> OakValue -> option OakValue)
(receive : ContractCallContext -> OakValue (* state *) ->
option OakValue (* message *) ->
option (OakValue * list ChainAction)).
Record Contract
(setup_ty msg_ty state_ty : Type)
{eq_setup : OakTypeEquivalence setup_ty}
{eq_msg : OakTypeEquivalence msg_ty}
{eq_state : OakTypeEquivalence state_ty} :=
build_contract {
version : Version;
init : ContractCallContext -> setup_ty -> option state_ty;
receive :
ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction);
}.
Arguments version {_ _ _ _ _ _} contract : rename.
Arguments init {_ _ _ _ _ _} contract ctx setup : rename.
Arguments receive {_ _ _ _ _ _} contract ctx state msg : rename.
Arguments build_contract {_ _ _ _ _ _}.
Definition contract_to_weak_contract
{A B C : Type}
{eq_a : OakTypeEquivalence A}
{eq_b : OakTypeEquivalence B}
{eq_c : OakTypeEquivalence C}
(c : Contract A B C) : WeakContract :=
let weak_init ctx oak_setup :=
do setup <- deserialize oak_setup;
do state <- c.(init) ctx setup;
Some (serialize state) in
let weak_recv ctx oak_state oak_msg_opt :=
do state <- deserialize oak_state;
match oak_msg_opt with
| Some oak_msg =>
do msg <- deserialize oak_msg;
do '(new_state, acts) <- c.(receive) ctx state (Some msg);
Some (serialize new_state, acts)
| None =>
do '(new_state, acts) <- c.(receive) ctx state None;
Some (serialize new_state, acts)
end in
build_weak_contract c.(version) weak_init weak_recv.
(*
Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
......
......@@ -18,6 +18,7 @@ Import ListNotations.
Import RecordSetNotations.
Open Scope Z.
Set Primitive Projections.
Definition ProposalId := nat.
......@@ -53,15 +54,15 @@ Record Setup :=
}.
Inductive Msg :=
| TransferOwnership : Address -> Msg
| ChangeRules : Rules -> Msg
| AddMember : Address -> Msg
| RemoveMember : Address -> Msg
| CreateProposal : list CongressAction -> Msg
| VoteForProposal : ProposalId -> Msg
| VoteAgainstProposal : ProposalId -> Msg
| RetractVote : ProposalId -> Msg
| FinishProposal : ProposalId -> Msg.
| transfer_ownership : Address -> Msg
| change_rules : Rules -> Msg
| add_member : Address -> Msg
| remove_member : Address -> Msg
| create_proposal : list CongressAction -> Msg
| vote_for_proposal : ProposalId -> Msg
| vote_against_proposal : ProposalId -> Msg
| retract_vote : ProposalId -> Msg
| finish_proposal : ProposalId -> Msg.
Record State :=
build_state {
......@@ -125,7 +126,7 @@ Definition vote_on_proposal
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= MapInterface.add pid new_proposal]]).
Definition retract_vote
Definition do_retract_vote
(voter : Address)
(pid : ProposalId)
(state : State)
......@@ -143,7 +144,7 @@ Definition congress_action_to_chain_action (act : CongressAction) : ChainAction
| cact_call to amt msg => act_call to amt msg
end.
Definition finish_proposal
Definition do_finish_proposal
(pid : ProposalId)
(state : State)
(chain : Chain)
......@@ -181,37 +182,147 @@ Definition receive
let is_from_member := (sender \in state.(members))%set in
let without_actions := option_map (fun new_state => (new_state, [ ])) in
match is_from_owner, is_from_member, maybe_msg with
| true, _, Some (TransferOwnership new_owner) =>
| true, _, Some (transfer_ownership new_owner) =>
Some (state[[owner := new_owner]], [ ])
| true, _, Some (ChangeRules new_rules) =>
| true, _, Some (change_rules new_rules) =>
if validate_rules new_rules then
Some (state[[state_rules := new_rules]], [ ])
else
None
| true, _, Some (AddMember new_member) =>
| true, _, Some (add_member new_member) =>
Some (state[[members ::= SetInterface.add new_member]], [ ])
| true, _, Some (RemoveMember old_member) =>
| true, _, Some (remove_member old_member) =>
Some (state[[members ::= SetInterface.remove old_member]], [ ])
| _, true, Some (CreateProposal actions) =>
| _, true, Some (create_proposal actions) =>
Some (add_proposal actions chain state, [ ])
| _, true, Some (VoteForProposal pid) =>
| _, true, Some (vote_for_proposal pid) =>
without_actions (vote_on_proposal sender pid 1 state)
| _, true, Some (VoteAgainstProposal pid) =>
| _, true, Some (vote_against_proposal pid) =>
without_actions (vote_on_proposal sender pid (-1) state)
| _, true, Some (RetractVote pid) =>
without_actions (retract_vote sender pid state)
| _, true, Some (retract_vote pid) =>
without_actions (do_retract_vote sender pid state)
| _, _, Some (FinishProposal pid) =>
finish_proposal pid state chain
| _, _, Some (finish_proposal pid) =>
do_finish_proposal pid state chain
| _, _, _ =>
None
end.
Definition deserialize_rules (v : OakValue) : option Rules :=
do '((a, b), c) <- deserialize v;
Some (build_rules a b c).
Program Instance rules_equivalence : OakTypeEquivalence Rules :=
{| serialize r := let (a, b, c) := r in serialize (a, b, c);
(* Why does
deserialize v :=
do '((a, b), c) <- deserialize v;
Some (build_rules a b c); |}.
not work here? *)
deserialize := deserialize_rules; |}.
Program Instance setup_equivalence : OakTypeEquivalence Setup :=
{| serialize s := serialize s.(setup_rules);
deserialize or :=
do rules <- deserialize or;
Some (build_setup rules); |}.
Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
do val <- deserialize v;
Some (match val with
| inl (to, amount) => cact_transfer to amount
| inr (to, amount, msg) => cact_call to amount msg
end).
Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
{| serialize ca :=
serialize
match ca with
| cact_transfer to amount => inl (to, amount)
| cact_call to amount msg => inr (to, amount, msg)
end;
deserialize := deserialize_congress_action; |}.
Next Obligation.
unfold deserialize_congress_action.
rewrite ote_equivalence.
destruct x; reflexivity.
Qed.
Definition deserialize_proposal (v : OakValue) : option Proposal :=
do '(a, b, c, d) <- deserialize v;
Some (build_proposal a b c d).
Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
{| serialize p :=
let (a, b, c, d) := p in
serialize (a, b, c, d);
deserialize := deserialize_proposal;
|}.
Next Obligation.
unfold deserialize_proposal.
rewrite ote_equivalence.
destruct x; reflexivity.
Qed.
Definition serialize_msg (m : Msg) : OakValue :=
serialize
match m with
| transfer_ownership a => (0, serialize a)
| change_rules r => (1, serialize r)
| add_member a => (2, serialize a)
| remove_member a => (3, serialize a)
| create_proposal l => (4, serialize l)
| vote_for_proposal pid => (5, serialize pid)
| vote_against_proposal pid => (6, serialize pid)
| retract_vote pid => (7, serialize pid)
| finish_proposal pid => (8, serialize pid)
end.
Definition deserialize_msg (v : OakValue) : option Msg :=
do '(tag, v) <- deserialize v;
match tag with
| 0 => option_map transfer_ownership (deserialize v)
| 1 => option_map change_rules (deserialize v)
| 2 => option_map add_member (deserialize v)
| 3 => option_map remove_member (deserialize v)
| 4 => option_map create_proposal (deserialize v)
| 5 => option_map vote_for_proposal (deserialize v)
| 6 => option_map vote_against_proposal (deserialize v)
| 7 => option_map retract_vote (deserialize v)
| 8 => option_map finish_proposal (deserialize v)
| _ => None
end.
Program Instance msg_equivalence : OakTypeEquivalence Msg :=
{| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
unfold serialize_msg, deserialize_msg.
destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
Qed.
Definition serialize_state (s : State) : OakValue :=
let (a, b, c, d, e) := s in
serialize (a, b, c, d, e).
Definition deserialize_state (v : OakValue) : option State :=
do '(a, b, c, d, e) <- deserialize v;
Some (build_state a b c d e).
Program Instance state_equivalence : OakTypeEquivalence State :=
{| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
unfold serialize_state, deserialize_state.
destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
Qed.
Definition contract : Contract Setup Msg State :=
build_contract version init receive.
From Coq Require Import List.
Import ListNotations.
Fixpoint find_first {A B : Type} (f : A -> option B) (l : list A)
: option B :=
match l with
| hd :: tl => match f hd with
| Some b => Some b
| None => find_first f tl
end
| [] => None
end.
......@@ -2,107 +2,278 @@ From Coq Require Import ZArith.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From RecordUpdate Require Import RecordUpdate.
From Containers Require Import Maps.
From Coq Require Import List.
From SmartContracts Require Import Extras.
Import RecordSetNotations.
Import ListNotations.
(* Note that [ ] or nil is needed for the empty list
in this file as [] parses an empty map *)
Local Record ContractInstance :=
{
inst_state_ty : OakType;
inst_msg_ty : OakType;
inst_state : interp_type inst_state_ty;
inst_receive : ContractCallContext -> interp_type inst_state_ty ->
option (interp_type inst_msg_ty) -> ChainAction;
}.
Local Record ChainUpdate :=
{
upd_block : Block;
build_chain_update {
(* Contracts that had their states updated and the new state *)
upd_contracts : Map[Address, ContractInstance];
(* Contracts deployed in this block *)
upd_deployments : Map[Address, ContractDeployment];
upd_contracts : Map[Address, OakValue];
(* All transactions caused by update, including internal txs
(due to contract execution) *)
upd_txs : list Tx;
}.
Inductive LocalChain :=
{
Instance eta_chain_update : Settable _ :=
mkSettable
((constructor build_chain_update) <*> upd_contracts
<*> upd_txs)%settable.
(* Contains information about the chain that contracts should have access
to. This does not contain definitions of contracts, for instance. *)
Record LocalChain :=
build_local_chain {
(* List of blocks and updates. Generally such lists have the
same length, except during contract execution, where lc_updates
is one ahead of lc_blocks (to facilitate tracking state within
the block) *)
lc_blocks : list Block;
lc_updates : list ChainUpdate;
}.
Instance eta_local_chain : Settable _ :=
mkSettable
((constructor build_local_chain) <*> lc_blocks
<*> lc_updates)%settable.
(* Contains full information about a chain, including contracts *)
Record LocalChainEnvironment :=
build_local_chain_environment {
lce_lc : LocalChain;
lce_contracts : list (Address * WeakContract);
}.
Instance eta_local_chain_environment : Settable _ :=
mkSettable
((constructor build_local_chain_environment) <*> lce_lc
<*> lce_contracts)%settable.
Definition genesis_block : Block :=
{| block_header := {| block_number := 0; |};
block_txs := nil |}.
Definition initial_chain : LocalChain :=
{| lc_updates :=
[{| upd_block := genesis_block;
upd_contracts := []%map;
upd_deployments := []%map;
{| lc_blocks := [genesis_block];
lc_updates :=
[{| upd_contracts := []%map;
upd_txs := nil |}]
|}.
Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
let is_old u := u.(upd_block).(block_header).(block_number) <=? bid in
let new_updates := filter is_old lc.(lc_updates) in
match new_updates with
| hd :: tl => if hd.(upd_block).(block_header).(block_number) =? bid
then Some {| lc_updates := new_updates |}
let is_old '(b, u) := b.(block_header).(block_number) <=? bid in
let zipped := rev (combine (rev lc.(lc_blocks)) (rev lc.(lc_updates))) in
let zipped_at := filter is_old zipped in
let '(at_blocks, at_updates) := split zipped_at in
match at_blocks with
| hd :: _ => if hd.(block_header).(block_number) =? bid
then Some {| lc_blocks := at_blocks; lc_updates := at_updates; |}
else None
| nil => None
end.
Definition lc_block_at (lc : LocalChain) (bid : BlockId) : option Block :=
let blocks := map upd_block lc.(lc_updates) in
let blocks := lc.(lc_blocks) in
find (fun b => b.(block_header).(block_number) =? bid) blocks.
Definition lc_head_block (lc : LocalChain) : Block :=
match lc.(lc_updates) with
| hd :: _ => hd.(upd_block)
match lc.(lc_blocks) with
| hd :: _ => hd
| nil => genesis_block
end.
Definition lc_incoming_txs (lc : LocalChain) (addr : Address) : list Tx :=
let all_txs := flat_map (fun u => u.(upd_block).(block_txs)) lc.(lc_updates) in
let all_txs := flat_map (fun u => u.(upd_txs)) lc.(lc_updates) in
let is_inc tx := (tx.(tx_to) =? addr)%address in
filter is_inc all_txs.
Definition lc_outgoing_txs (lc : LocalChain) (addr : Address) : list Tx :=
let all_txs := flat_map (fun u => u.(upd_block).(block_txs)) lc.(lc_updates) in
let all_txs := flat_map (fun u => u.(upd_txs)) lc.(lc_updates) in
let is_out tx := (tx.(tx_from) =? addr)%address in
filter is_out all_txs.
Local Definition find_first {A : Type} (f : ChainUpdate -> option A) (lc : LocalChain)
: option A :=
let opts := map f lc.(lc_updates) in
let is_some o := match o with | Some _ => true | None => false end in
match filter is_some opts with
| hd :: _ => hd
| _ => None
end.
Definition lc_contract_deployment (lc : LocalChain) (addr : Address)
: option ContractDeployment :=
find_first (fun u => u.(upd_deployments)[addr]%map) lc.
Definition lc_contract_state (lc : LocalChain) (addr : Address)
: option OakValue :=
let get_state_oak_value u :=
do c <- u.(upd_contracts)[addr]%map;
Some (build_oak_value c.(inst_state_ty) c.(inst_state)) in
find_first get_state_oak_value lc.
find_first (fun u => u.(upd_contracts)[addr]%map) lc.(lc_updates).
Definition local_chain_impl : ChainInterface :=
Definition lc_interface : ChainInterface :=
{| ci_chain_type := LocalChain;
ci_chain_at := lc_chain_at;
ci_head_block := lc_head_block;
ci_incoming_txs := lc_incoming_txs;
ci_outgoing_txs := lc_outgoing_txs;
ci_contract_deployment := lc_contract_deployment;
ci_contract_state := lc_contract_state;
|}.
Section ExecuteActions.
Context (initial_lce : LocalChainEnvironment).
Local Record ExecutionContext :=
build_execution_context {
block_txs : list Tx;
new_update : ChainUpdate;
new_contracts : list (Address * WeakContract);
}.
Local Instance eta_execution_context : Settable _ :=
mkSettable
((constructor build_execution_context) <*> block_txs
<*> new_update
<*> new_contracts)%settable.
Let make_acc_lce ec :=
let new_lc := (initial_lce.(lce_lc))[[lc_updates ::= cons ec.(new_update)]] in
let new_contracts := ec.(new_contracts) ++ initial_lce.(lce_contracts) in
{| lce_lc := new_lc; lce_contracts := new_contracts |}.
Let make_acc_c lce : Chain :=
build_chain lc_interface lce.(lce_lc).
Let verify_amount (c : Chain) (addr : Address) (amt : Amount)
: option unit :=
if (amt <=? account_balance c addr)%nat
then Some tt