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

Break cycle in ChainAction<->Contract and define congress_contract

Previously a contract could not store ChainAction's in its state because
of universe inconsistencies.
parent f0c73550
Pipeline #11034 failed with stage
in 3 minutes and 59 seconds
...@@ -74,41 +74,46 @@ Inductive ContractCallContext := ...@@ -74,41 +74,46 @@ Inductive ContractCallContext :=
ctx_amount : Amount; ctx_amount : Amount;
}. }.
Inductive Contract : Type -> Type -> Type -> Type := Inductive ChainAction :=
| build_contract :
forall (setup_ty msg_ty state_ty : Type),
Version ->
(setup_ty -> ContractCallContext -> option state_ty) -> (* init *)
(state_ty -> ContractCallContext ->
option msg_ty -> option (state_ty * list ChainAction)) -> (* receive *)
Contract setup_ty msg_ty state_ty
with ChainAction :=
| act_transfer (to : Address) (amount : Amount) | act_transfer (to : Address) (amount : Amount)
(* todo: Should we use mutual inductives and store a Contract here?
It does not allow contracts to store chain actions in their state,
but that may be preferable. *)
| act_deploy : | act_deploy :
forall setup_ty msg_ty state_ty, forall setup_ty msg_ty state_ty,
Contract setup_ty msg_ty state_ty -> Version ->
setup_ty -> (ContractCallContext -> setup_ty -> option state_ty) -> (* init *)
(ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction)) -> (* receive *)
ChainAction ChainAction
| act_call (to : Address) (amount : Amount) (msg : OakValue). | act_call (to : Address) (amount : Amount) (msg : OakValue).
Definition contract_version {A B C : Type} (c : Contract A B C) := Record Contract (setup_ty msg_ty state_ty : Type) :=
let 'build_contract _ _ _ ver _ _ := c in ver. build_contract {
contract_version : Version;
Definition contract_init {A B C : Type} (c : Contract A B C) := contract_init : ContractCallContext -> setup_ty -> option state_ty;
let 'build_contract _ _ _ _ init _ := c in init. contract_receive : ContractCallContext -> state_ty ->
option msg_ty -> option (state_ty * list ChainAction);
}.
Definition contract_receive {A B C : Type} (c : Contract A B C) := Arguments build_contract {_ _ _}.
let 'build_contract _ _ _ _ _ recv := c in recv.
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 *)
contract_address : Address; contract_address : Address;
(* The setup that was passed when the contract was deployed *)
setup : setup_ty; setup : setup_ty;
(* 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
a message *)
transfer : Amount -> ChainAction; transfer : Amount -> ChainAction;
(* Make an action calling the contract *)
call : Amount -> msg_ty -> ChainAction; call : Amount -> msg_ty -> ChainAction;
}. }.
(*
(* 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
...@@ -137,4 +142,5 @@ Definition get_contract_interface ...@@ -137,4 +142,5 @@ Definition get_contract_interface
transfer := act_transfer addr; transfer := act_transfer addr;
call amt msg := act_call addr amt (build_oak_value msg_oty msg) |} call amt msg := act_call addr amt (build_oak_value msg_oty msg) |}
| _, _, _ => None | _, _, _ => None
end. end.
\ No newline at end of file *)
\ No newline at end of file
...@@ -5,6 +5,8 @@ From Coq Require Import Program.Basics. ...@@ -5,6 +5,8 @@ From Coq Require Import Program.Basics.
From Containers Require Import OrderedTypeEx. From Containers Require Import OrderedTypeEx.
From Containers Require Import MapInterface. From Containers Require Import MapInterface.
From Containers Require Import SetInterface. From Containers Require Import SetInterface.
From Containers Require MapAVL.
From Containers Require SetAVL.
From SmartContracts Require Import Blockchain. 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.
...@@ -15,7 +17,6 @@ Import ListNotations. ...@@ -15,7 +17,6 @@ Import ListNotations.
Import RecordSetNotations. Import RecordSetNotations.
Open Scope Z. Open Scope Z.
Print Visibility.
Definition ProposalId := nat. Definition ProposalId := nat.
...@@ -83,7 +84,7 @@ Definition validate_rules (rules : Rules) : bool := ...@@ -83,7 +84,7 @@ Definition validate_rules (rules : Rules) : bool :=
&& (rules.(margin_needed_permille) <=? 1000) && (rules.(margin_needed_permille) <=? 1000)
&& (rules.(debating_period_in_blocks) >=? 0). && (rules.(debating_period_in_blocks) >=? 0).
Definition init (chain : Chain) (ctx : ContractCallContext) (setup : Setup) : option State := Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
if validate_rules setup.(setup_rules) then if validate_rules setup.(setup_rules) then
Some {| owner := ctx.(ctx_from); Some {| owner := ctx.(ctx_from);
state_rules := setup.(setup_rules); state_rules := setup.(setup_rules);
...@@ -158,11 +159,11 @@ Definition finish_proposal ...@@ -158,11 +159,11 @@ Definition finish_proposal
Some (new_state, response_acts). Some (new_state, response_acts).
Definition receive Definition receive
(chain : Chain)
(state : State)
(ctx : ContractCallContext) (ctx : ContractCallContext)
(state : State)
(maybe_msg : option Msg) (maybe_msg : option Msg)
: option (State * list ChainAction) := : option (State * list ChainAction) :=
let chain := ctx.(ctx_chain) in
let sender := ctx.(ctx_from) in let sender := ctx.(ctx_from) in
let is_from_owner := (sender =? state.(owner))%address in let is_from_owner := (sender =? state.(owner))%address in
let is_from_member := (sender \in state.(members))%set in let is_from_member := (sender \in state.(members))%set in
...@@ -197,8 +198,11 @@ Definition receive ...@@ -197,8 +198,11 @@ Definition receive
| _, _, Some (FinishProposal pid) => | _, _, Some (FinishProposal pid) =>
finish_proposal pid state chain finish_proposal pid state chain
| _, _, _ => | _, _, _ =>
None None
end. end.
Definition congress_contract : Contract Setup Msg State :=
build_contract version init receive.
\ No newline at end of file
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