Commit c9329d33 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Start of concrete blockchain implementation

parent 9c389c3c
Pipeline #11056 passed with stage
in 4 minutes and 45 seconds
...@@ -42,7 +42,6 @@ Record Tx := ...@@ -42,7 +42,6 @@ Record Tx :=
Record BlockHeader := Record BlockHeader :=
build_block_header { build_block_header {
block_number : BlockId; block_number : BlockId;
block_hash : BlockHash;
}. }.
Record Block := Record Block :=
...@@ -51,19 +50,67 @@ Record Block := ...@@ -51,19 +50,67 @@ Record Block :=
block_txs : list Tx; block_txs : list Tx;
}. }.
Inductive Chain := (* 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 :=
build_chain_interface {
ifc_chain_type : Type;
ifc_chain_at : ifc_chain_type -> BlockId -> option ifc_chain_type;
ifc_head_block : ifc_chain_type -> Block;
ifc_incoming_txs : ifc_chain_type -> Address -> list Tx;
ifc_outgoing_txs : ifc_chain_type -> Address -> list Tx;
ifc_contract_deployment : ifc_chain_type -> Address -> option ContractDeployment;
ifc_contract_state : ifc_chain_type -> Address -> option OakValue;
}.
Record Chain :=
build_chain { build_chain {
get_chain_at : BlockId -> option Chain; chain_ifc : ChainInterface;
get_block_at : BlockId -> option Block; chain_val : ifc_chain_type chain_ifc
head_block : Block;
get_incoming_txs : Address -> list unit;
get_outgoing_txs : Address -> list unit;
get_contract_deployment : Address -> option ContractDeployment;
get_contract_state : Address -> option OakValue;
}. }.
Definition chain_at (c : Chain) (bid : BlockId) : option Chain :=
do x <- c.(chain_ifc).(ifc_chain_at) c.(chain_val) bid;
Some {| chain_val := x |}.
Definition head_block (c : Chain) :=
c.(chain_ifc).(ifc_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_ifc).(ifc_incoming_txs) c.(chain_val).
Definition outgoing_txs (c : Chain) :=
c.(chain_ifc).(ifc_outgoing_txs) c.(chain_val).
Definition contract_deployment (c : Chain) :=
c.(chain_ifc).(ifc_contract_deployment) c.(chain_val).
Definition contract_state (c : Chain) :=
c.(chain_ifc).(ifc_contract_state) c.(chain_val).
Inductive ContractCallContext := Inductive ContractCallContext :=
build_contract_call_ctx { build_contract_call_ctx {
(* Chain *) (* Chain *)
ctx_chain : Chain; ctx_chain : Chain;
(* Address sending the funds *) (* Address sending the funds *)
...@@ -72,32 +119,19 @@ Inductive ContractCallContext := ...@@ -72,32 +119,19 @@ Inductive ContractCallContext :=
ctx_contract_address : Address; ctx_contract_address : Address;
(* Amount of GTU passed in call *) (* Amount of GTU passed in call *)
ctx_amount : Amount; ctx_amount : Amount;
}. }.
Inductive ChainAction := Inductive ChainAction :=
| act_transfer (to : Address) (amount : Amount) | act_transfer (to : Address) (amount : Amount)
(* todo: Should we use mutual inductives and store a Contract here? | act_call (to : Address) (amount : Amount) (msg : OakValue)
It does not allow contracts to store chain actions in their state, | act_deploy
but that may be preferable. *) {setup_ty msg_ty state_ty : Type}
| act_deploy : (version : Version)
forall setup_ty msg_ty state_ty, (init : ContractCallContext -> setup_ty -> option state_ty)
Version -> (receive : ContractCallContext -> state_ty ->
(ContractCallContext -> setup_ty -> option state_ty) -> (* init *) option msg_ty -> option (state_ty * list ChainAction)).
(ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction)) -> (* receive *)
ChainAction
| act_call (to : Address) (amount : Amount) (msg : OakValue).
Record Contract (setup_ty msg_ty state_ty : Type) :=
build_contract {
contract_version : Version;
contract_init : ContractCallContext -> setup_ty -> option state_ty;
contract_receive : ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction);
}.
Arguments build_contract {_ _ _}.
(*
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 *)
...@@ -106,18 +140,19 @@ Record ContractInterface (setup_ty msg_ty state_ty : Type) := ...@@ -106,18 +140,19 @@ Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
setup : setup_ty; 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 transferirng money to the contract without (* Make an action transferring money to the contract without
a message *) a message *)
transfer : Amount -> ChainAction; transfer : Amount -> ContractAction;
(* Make an action calling the contract *) (* Make an action calling the contract *)
call : Amount -> msg_ty -> ChainAction; call : Amount -> msg_ty -> ContractAction;
}. }.
*)
(* (*
(* todo: this should be easier -- we want actual strong typed (* todo: this should be easier -- we want actual strong typed
interface by equivalence of oak type (iterated product, for instance) interface by equivalence of oak type (iterated product, for instance)
to types in contracts. Right now the interface received allows you to types in contracts. Right now the interface received allows you
only to interact with a contrat using interpreted types. *) only to interact with a contract using interpreted types. *)
Definition get_contract_interface Definition get_contract_interface
(setup_oty msg_oty state_oty : OakType) (setup_oty msg_oty state_oty : OakType)
(chain : Chain) (chain : Chain)
......
From Coq Require Import String. From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import ZArith. From Coq Require Import ZArith.
From Coq Require Import Program.Basics. From Coq Require Import Program.Basics.
From Containers Require Import OrderedTypeEx. From Containers Require Import OrderedTypeEx.
...@@ -11,6 +10,8 @@ From SmartContracts Require Import Blockchain. ...@@ -11,6 +10,8 @@ From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak. From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads. From SmartContracts Require Import Monads.
From RecordUpdate Require Import RecordUpdate. From RecordUpdate Require Import RecordUpdate.
(* This is included last to default things to list rather than map/set *)
From Coq Require Import List.
Import MapNotations. Import MapNotations.
Import ListNotations. Import ListNotations.
...@@ -20,9 +21,13 @@ Open Scope Z. ...@@ -20,9 +21,13 @@ Open Scope Z.
Definition ProposalId := nat. Definition ProposalId := nat.
Inductive CongressAction :=
| cact_transfer (to : Address) (amount : Amount)
| cact_call (to : Address) (amount : Amount) (msg : OakValue).
Record Proposal := Record Proposal :=
build_proposal { build_proposal {
actions : list ChainAction; actions : list CongressAction;
votes : Map[Address, Z]; votes : Map[Address, Z];
vote_result : Z; vote_result : Z;
proposed_in : BlockId; proposed_in : BlockId;
...@@ -52,7 +57,7 @@ Inductive Msg := ...@@ -52,7 +57,7 @@ Inductive Msg :=
| ChangeRules : Rules -> Msg | ChangeRules : Rules -> Msg
| AddMember : Address -> Msg | AddMember : Address -> Msg
| RemoveMember : Address -> Msg | RemoveMember : Address -> Msg
| CreateProposal : list ChainAction -> Msg | CreateProposal : list CongressAction -> Msg
| VoteForProposal : ProposalId -> Msg | VoteForProposal : ProposalId -> Msg
| VoteAgainstProposal : ProposalId -> Msg | VoteAgainstProposal : ProposalId -> Msg
| RetractVote : ProposalId -> Msg | RetractVote : ProposalId -> Msg
...@@ -94,7 +99,7 @@ Definition init (ctx : ContractCallContext) (setup : Setup) : option State := ...@@ -94,7 +99,7 @@ Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
else else
None. None.
Definition add_proposal (actions : list ChainAction) (chain : Chain) (state : State) : State := Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
let id := state.(next_proposal_id) in let id := state.(next_proposal_id) in
let head_block := chain.(head_block) in let head_block := chain.(head_block) in
let proposal := {| actions := actions; let proposal := {| actions := actions;
...@@ -132,6 +137,12 @@ Definition retract_vote ...@@ -132,6 +137,12 @@ Definition retract_vote
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= MapInterface.add pid new_proposal]]). Some (state[[proposals ::= MapInterface.add pid new_proposal]]).
Definition congress_action_to_chain_action (act : CongressAction) : ChainAction :=
match act with
| cact_transfer to amt => act_transfer to amt
| cact_call to amt msg => act_call to amt msg
end.
Definition finish_proposal Definition finish_proposal
(pid : ProposalId) (pid : ProposalId)
(state : State) (state : State)
...@@ -156,7 +167,8 @@ Definition finish_proposal ...@@ -156,7 +167,8 @@ Definition finish_proposal
if (enough_voters && enough_ayes)%bool if (enough_voters && enough_ayes)%bool
then proposal.(actions) then proposal.(actions)
else [ ] in else [ ] in
Some (new_state, response_acts). let response_chain_acts := map congress_action_to_chain_action response_acts in
Some (new_state, response_chain_acts).
Definition receive Definition receive
(ctx : ContractCallContext) (ctx : ContractCallContext)
...@@ -202,7 +214,4 @@ Definition receive ...@@ -202,7 +214,4 @@ Definition receive
| _, _, _ => | _, _, _ =>
None None
end. end.
\ No newline at end of file
Definition congress_contract : Contract Setup Msg State :=
build_contract version init receive.
\ No newline at end of file
From Coq Require Import ZArith.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From Containers Require Import Maps.
From Coq Require Import List.
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;
(* 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];
(* All transactions caused by update, including internal txs
(due to contract execution) *)
upd_txs : list Tx;
}.
Inductive LocalChain :=
{
lc_updates : list ChainUpdate;
}.
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;
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 |}
else None
| nil => None
end.
Definition lc_block_at (lc : LocalChain) (bid : BlockId) : option Block :=
let blocks := map upd_block lc.(lc_updates) 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)
| 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 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 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.
Definition local_chain_impl : ChainInterface :=
{| ifc_chain_type := LocalChain;
ifc_chain_at := lc_chain_at;
ifc_head_block := lc_head_block;
ifc_incoming_txs := lc_incoming_txs;
ifc_outgoing_txs := lc_outgoing_txs;
ifc_contract_deployment := lc_contract_deployment;
ifc_contract_state := lc_contract_state;
|}.
\ No newline at end of file
Markdown is supported
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