Commit 79abd5bf authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Add result monad and change add_block to return a result

parent a3605c74
Pipeline #20307 passed with stage
in 9 minutes and 6 seconds
......@@ -26,6 +26,7 @@ execution/theories/Extras.v
execution/theories/Finite.v
execution/theories/LocalBlockchain.v
execution/theories/Monads.v
execution/theories/ResultMonad.v
execution/theories/Serializable.v
-Q embedding/theories ConCert.Embedding
......
......@@ -12,7 +12,7 @@ Require Import Morphisms.
Require Import Permutation.
Require Import Program.Tactics.
From ConCert.Execution Require Import Blockchain Congress Automation Extras.
From ConCert.Execution Require Import Blockchain Congress Automation Extras ResultMonad.
Import ListNotations.
......@@ -519,7 +519,7 @@ Qed.
Corollary cf_backed_after_block {ChainBuilder : ChainBuilderType}
prev hd acts new cf_addr lstate :
builder_add_block prev hd acts = Some new ->
builder_add_block prev hd acts = Ok new ->
env_contracts new cf_addr = Some (cf_contract : WeakContract) ->
cf_state new cf_addr = Some lstate ->
(account_balance (env_chain new) cf_addr >= balance_coq lstate)%Z.
......@@ -537,7 +537,7 @@ Qed.
(** ** The actual contract balance is consistent with the sum of individual contributions *)
Corollary cf_donations_backed_after_block {ChainBuilder : ChainBuilderType}
prev hd acts new cf_addr lstate :
builder_add_block prev hd acts = Some new ->
builder_add_block prev hd acts = Ok new ->
env_contracts new cf_addr = Some (cf_contract : WeakContract) ->
cf_state new cf_addr = Some lstate ->
~~ lstate.(done_coq) ->
......
......@@ -26,4 +26,5 @@ theories/Extras.v
theories/Finite.v
theories/LocalBlockchain.v
theories/Monads.v
theories/ResultMonad.v
theories/Serializable.v
......@@ -64,11 +64,12 @@ From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
Require Import Serializable.
Require Import Monads.
Require Import Extras.
Require Import Automation.
Require Import ChainedList.
Require Import Extras.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.
......@@ -1860,6 +1861,23 @@ End Theories.
End Trace.
End Semantics.
Inductive ActionEvaluationError :=
| amount_negative (* amount is negative *)
| amount_too_high (* sender does not have enough money *)
| no_such_contract (* there is not contract at that address *)
| too_many_contracts (* cannot generate fresh address for new contract *)
| init_failed (* contract init function failed *)
| receive_failed (* contract receive function failed *)
| internal_error. (* unexpected internal error *)
Inductive AddBlockError :=
| invalid_header (* header for next block is invalid *)
| invalid_root_action (act : Action) (* a specified root action is invalid *)
| action_evaluation_depth_exceeded (* out of fuel while evaluating actions recursively *)
| action_evaluation_error (* error when evaluating single action *)
(act : Action)
(err : ActionEvaluationError).
Class ChainBuilderType :=
build_builder {
builder_type : Type;
......@@ -1872,7 +1890,7 @@ Class ChainBuilderType :=
(builder : builder_type)
(header : BlockHeader)
(actions : list Action) :
option builder_type;
result builder_type AddBlockError;
builder_trace (builder : builder_type) :
ChainTrace empty_state (build_chain_state (builder_env builder) []);
......
......@@ -9,6 +9,7 @@ Require Import Containers.
Require Import Extras.
Require Import LocalBlockchain.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
Import ListNotations.
......@@ -112,7 +113,7 @@ Definition deploy_setup :=
registration_deposit := 0; |}.
Local Open Scope list.
Definition boardroom_example :=
Definition boardroom_example : option nat :=
let chain : ChainBuilder := builder_initial in
let creator : Address := A 10 in
let add_block (chain : ChainBuilder) (acts : list Action) :=
......@@ -122,11 +123,11 @@ Definition boardroom_example :=
block_finalized_height := finalized_height chain;
block_creator := creator;
block_reward := 50; |} in
builder_add_block chain next_header acts in
option_of_result (builder_add_block chain next_header acts) in
do chain <- add_block chain [];
let dep := build_act creator (create_deployment 0 (boardroom_voting hash_func) deploy_setup) in
do chain <- add_block chain [dep];
do caddr <- hd None (map Some (FMap.keys (lc_contracts (lcb_lc chain))));
do caddr <- hd_error (FMap.keys (lc_contracts (lcb_lc chain)));
let send addr m := build_act addr (act_call caddr 0 (serialize m)) in
let calls := map (fun '(addr, m) => send addr m) (zip addrs signups) in
do chain <- add_block chain calls;
......@@ -135,6 +136,6 @@ Definition boardroom_example :=
let tally := build_act creator (act_call caddr 0 (serialize tally_votes)) in
do chain <- add_block chain [tally];
do state <- @contract_state _ (@State _ Z) _ (lcb_lc chain) caddr;
result state.
BoardroomVoting.result state.
Check (@eq_refl (option nat) (Some votes_for)) <<: boardroom_example = Some votes_for.
......@@ -8,13 +8,14 @@ From Coq Require Import ZArith.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
Require Import Automation.
Require Import Blockchain.
Require Import Serializable.
Require Import Monads.
Require Import ChainedList.
Require Import Containers.
Require Import Automation.
Require Import Extras.
Require Import ChainedList.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -528,7 +529,7 @@ Qed.
Corollary congress_txs_after_block
{ChainBuilder : ChainBuilderType}
prev new header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......
......@@ -9,13 +9,15 @@ From Coq Require Import ZArith.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
Require Import Automation.
Require Import Blockchain.
Require Import Serializable.
Require Import Monads.
Require Import BoundedN.
Require Import ChainedList.
Require Import Containers.
Require Import Automation.
Require Import Extras.
Require Import BoundedN.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -353,7 +355,7 @@ Section Theories.
block_creator := creator;
block_reward := 50; |} in
let acts := map (build_act creator) act_bodies in
builder_add_block chain next_header acts in
option_of_result (builder_add_block chain next_header acts) in
(* Get some money on the creator *)
do chain <- add_block chain [];
(* Deploy congress and exploit contracts *)
......
......@@ -23,6 +23,7 @@ Require Import Automation.
Require Import Blockchain.
Require Import Extras.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
......@@ -583,7 +584,7 @@ Section Theories.
Corollary escrow_correct
{ChainBuilder : ChainBuilderType}
prev new header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
let trace := builder_trace new in
forall caddr,
env_contracts new caddr = Some (Escrow.contract : WeakContract) ->
......
......@@ -10,6 +10,7 @@ Require Import Congress.
Require Import Containers.
Require Import BoundedN.
Require Import Extras.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -36,7 +37,7 @@ Section LocalBlockchainTests.
Definition chain1 : ChainBuilder := builder_initial.
Definition add_block (chain : ChainBuilder) acts : option ChainBuilder :=
Definition add_block (chain : ChainBuilder) acts : result ChainBuilder AddBlockError :=
let header :=
{| block_height := S (chain_height chain);
block_slot := S (current_slot chain);
......@@ -45,16 +46,25 @@ Section LocalBlockchainTests.
block_reward := 50; |} in
builder_add_block chain header acts.
Definition unpack_result {T E} (r : result T E) :=
match r return match r with
| Ok _ => T
| Err _ => E
end with
| Ok t => t
| Err e => e
end.
(* Creator created an empty block (and gets some coins) *)
Definition chain2 : ChainBuilder :=
unpack_option (add_block chain1 []).
unpack_result (add_block chain1 []).
Compute (account_balance chain2 person_1).
Compute (account_balance chain2 creator).
(* Creator transfers 10 coins to person_1 *)
Definition chain3 : ChainBuilder :=
unpack_option (add_block chain2 [build_act creator (act_transfer person_1 10)]).
unpack_result (add_block chain2 [build_act creator (act_transfer person_1 10)]).
Compute (account_balance chain3 person_1).
Compute (account_balance chain3 creator).
......@@ -71,7 +81,7 @@ Section LocalBlockchainTests.
create_deployment 5 Congress.contract setup.
Definition chain4 : ChainBuilder :=
unpack_option (add_block chain3 [build_act person_1 deploy_congress]).
unpack_result (add_block chain3 [build_act person_1 deploy_congress]).
Definition congress_1 : Address :=
match outgoing_txs (builder_trace chain4) person_1 with
......@@ -115,7 +125,7 @@ Section LocalBlockchainTests.
Definition chain5 : ChainBuilder :=
let acts := [build_act person_1 (add_person person_1);
build_act person_1 (add_person person_2)] in
unpack_option (add_block chain4 acts).
unpack_result (add_block chain4 acts).
Compute (FMap.elements (congress_state chain5).(members)).
Compute (account_balance chain5 congress_1).
......@@ -126,7 +136,7 @@ Section LocalBlockchainTests.
congress_ifc.(send) 0 (Some (create_proposal [cact_transfer person_3 3])).
Definition chain6 : ChainBuilder :=
unpack_option (add_block chain5 [build_act person_1 create_proposal_call]).
unpack_result (add_block chain5 [build_act person_1 create_proposal_call]).
Compute (FMap.elements (congress_state chain6).(proposals)).
......@@ -136,7 +146,7 @@ Section LocalBlockchainTests.
Definition chain7 : ChainBuilder :=
let acts := [build_act person_1 vote_proposal; build_act person_2 vote_proposal] in
unpack_option (add_block chain6 acts).
unpack_result (add_block chain6 acts).
Compute (FMap.elements (congress_state chain7).(proposals)).
......@@ -145,7 +155,7 @@ Section LocalBlockchainTests.
congress_ifc.(send) 0 (Some (finish_proposal 1)).
Definition chain8 : ChainBuilder :=
unpack_option (add_block chain7 [build_act person_3 finish_proposal]).
unpack_result (add_block chain7 [build_act person_3 finish_proposal]).
Compute (FMap.elements (congress_state chain8).(proposals)).
(* Balances before: *)
......@@ -161,7 +171,7 @@ Section LocalBlockchainTests.
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
(prev new : BuilderDF) header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......@@ -173,7 +183,7 @@ Section LocalBlockchainTests.
Definition BuilderBF := LocalChainBuilderBreadthFirst AddrSize.
Lemma congress_txs_after_local_chain_bf_block
(prev new : BuilderBF) header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......
This diff is collapsed.
......@@ -36,14 +36,14 @@ build_monad_laws {
Class MonadTrans (m : Type -> Type) (mt : Type -> Type) : Type :=
{ lift : forall {t}, mt t -> m t }.
Global Instance option_monad : Monad option :=
Global Instance Monad_option : Monad option :=
{| ret _ t := Some t;
bind _ _ v f := match v with
| Some val => f val
| None => None
end |}.
Global Instance option_monad_laws : MonadLaws option_monad.
Global Instance MonadLaws_Monad_option : MonadLaws Monad_option.
Proof.
constructor.
- auto.
......
From ConCert.Execution Require Import Monads.
Inductive result T E :=
| Ok (t : T)
| Err (e : E).
Arguments Ok {_ _}.
Arguments Err {_ _}.
Global Instance Monad_result {E} : Monad (fun T => result T E) :=
{| ret _ t := Ok t;
bind _ _ mt f :=
match mt with
| Ok t => f t
| Err e => Err e
end |}.
Definition result_of_option {T E} (o : option T) (err : E) : result T E :=
match o with
| Some a => Ok a
| None => Err err
end.
Definition option_of_result {T E} (r : result T E) : option T :=
match r with
| Ok t => Some t
| Err e => None
end.
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