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

Support block rewards and some preliminary stuff on semantics

parent d580f4f6
This diff is collapsed.
......@@ -4,16 +4,19 @@ does not change during execution of blocks. This is proven under the (implicit)
assumption that the address space is finite. *)
From Coq Require Import List Permutation ZArith Psatz.
From SmartContracts Require Import Automation Blockchain Extras Finite.
From RecordUpdate Require Import RecordSet.
Import ListNotations.
Section Circulation.
Context {ChainBaseTypes : ChainBaseTypes}.
Context {Chain : ChainType}.
Context `{Finite Address}.
Definition circulation (chain : Chain) :=
Definition circulation {Chain : ChainType} (chain : Chain) :=
sumZ (account_balance chain) (elements Address).
Definition coins_created (start_height end_height : nat) : Amount :=
sumZ compute_block_reward (seq start_height (end_height - start_height)).
(* We then prove that over any single step, the circulation is preserved.
The idea behind this proof is that addrs contain from and to so
we can move them to the beginning of the sum and it easily follows that
......@@ -29,10 +32,11 @@ Proof.
Qed.
Lemma step_from_to_same
{pre post : Environment}
{act : ExternalAction}
{new_acts : list ExternalAction}
(step : ChainStep pre post act new_acts) :
{pre : Environment}
{act : Action}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act post new_acts) :
step_from step = step_to step ->
circulation post = circulation pre.
Proof.
......@@ -40,7 +44,7 @@ Proof.
unfold circulation.
induction (elements Address) as [| x xs IH].
- reflexivity.
- simpl.
- simpl in *.
rewrite IH, (account_balance_post step), from_eq_to.
lia.
Qed.
......@@ -48,10 +52,11 @@ Qed.
Hint Resolve step_from_to_same.
Lemma step_circulation_unchanged
{pre post : Environment}
{act : ExternalAction}
{new_acts : list ExternalAction}
(step : ChainStep pre post act new_acts) :
{pre : Environment}
{act : Action}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act post new_acts) :
circulation post = circulation pre.
Proof.
destruct (address_eqb_spec (step_from step) (step_to step))
......@@ -79,9 +84,10 @@ Hint Resolve step_circulation_unchanged.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
{pre post : Environment}
{x y : list ExternalAction}
(trace : BlockTrace pre post x y)
{bef : list Action}
{after : list Action}
(post pre : Environment)
(trace : BlockTrace pre bef post after)
: circulation post = circulation pre.
Proof.
induction trace;
......@@ -89,4 +95,110 @@ Proof.
| [IH: _ |- _] => try rewrite <- IH; eauto
end.
Qed.
Hint Resolve block_trace_circulation_unchanged.
Lemma circulation_equal
{Chain1 : ChainType}
(c1 : Chain1)
{Chain2 : ChainType}
(c2 : Chain2) :
ChainExtEqual (pack_chain c1) (pack_chain c2) ->
circulation c1 = circulation c2.
Proof.
intros [].
unfold circulation, account_balance.
induction (elements Address); prove.
Qed.
Lemma circulation_add_block baker height env :
circulation (add_block_baked baker height env) =
(circulation env + compute_block_reward height)%Z.
Proof.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)).
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; prove. }
destruct Hperm as [suf perm].
symmetry in perm.
pose proof (Permutation_NoDup perm (elements_set Address)) as perm_set.
unfold circulation.
rewrite perm.
simpl.
unfold constructor, set, account_balance.
simpl.
destruct (address_eqb_spec baker baker); try congruence.
simpl.
pose proof (in_NoDup_app baker [baker] suf ltac:(prove) perm_set) as not_in_suf.
repeat rewrite <- Z.add_assoc.
f_equal.
rewrite <- Z.add_comm.
repeat rewrite <- Z.add_assoc.
f_equal.
clear perm perm_set e.
induction suf as [| x xs IH]; auto.
simpl in *.
apply Decidable.not_or in not_in_suf.
destruct (address_eqb_spec x baker); try tauto.
specialize (IH (proj2 not_in_suf)).
lia.
Qed.
Lemma circulation_set_finalized_height n env :
circulation (set_finalized_height n env) = circulation env.
Proof.
unfold circulation.
induction (elements Address); prove.
Qed.
Lemma circulation_set_slot_number n env :
circulation (set_slot_number n env) = circulation env.
Proof.
unfold circulation.
induction (elements Address); prove.
Qed.
Lemma circulation_set_block_height n env :
circulation (set_block_height n env) = circulation env.
Proof.
unfold circulation.
induction (elements Address); prove.
Qed.
Lemma chain_trace_circulation
{Chain : ChainType}
{chain_start chain_end : Chain}
(trace : ChainTrace chain_start chain_end)
: circulation chain_end =
(circulation chain_start +
coins_created (block_height chain_start) (block_height chain_end))%Z.
Proof.
induction trace.
- unfold coins_created.
rewrite Nat.sub_diag.
simpl. lia.
- replace (block_height new_end) with new_block_height.
+ unfold coins_created.
subst new_block_height baked_block.
pose proof (block_height_post_trace trace) as height_le.
replace (S (block_height prev_end) - block_height trace_start)
with (S (block_height prev_end - block_height trace_start)) by lia.
rewrite sumZ_seq_S.
unfold coins_created in IHtrace.
rewrite Z.add_assoc, <- IHtrace.
match goal with
| [|- context[?a + (?b - ?a)]] => replace (a + (b - a)) with b by lia
end.
rewrite <- (circulation_equal block_start prev_end) by auto.
rewrite (circulation_equal new_end block_end) by auto.
erewrite (block_trace_circulation_unchanged block_end env2) by eassumption.
subst env env0 env1 env2.
now rewrite circulation_add_block, circulation_set_finalized_height,
circulation_set_slot_number, circulation_set_block_height.
+ subst new_block_height baked_block.
pose proof (block_height_eq _ _ H5) as height_eq.
simpl in *.
rewrite height_eq.
rewrite (block_height_post_steps H4).
reflexivity.
Qed.
End Circulation.
From Coq Require Import String.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From Coq Require Import Morphisms.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Automation.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -13,7 +14,7 @@ Import ListNotations.
Import RecordSetNotations.
Section Congress.
Context {BaseTypes : ChainBaseTypes} {Chain : ChainType}.
Context {BaseTypes : ChainBaseTypes}.
Local Open Scope Z.
Set Primitive Projections.
......@@ -29,21 +30,17 @@ Record Proposal :=
actions : list CongressAction;
votes : FMap Address Z;
vote_result : Z;
proposed_in : BlockId;
proposed_in : nat;
}.
Instance eta_proposal : Settable _ :=
mkSettable
((constructor build_proposal) <*> actions
<*> votes
<*> vote_result
<*> proposed_in)%settable.
Instance proposal_settable : Settable _ :=
settable! build_proposal <actions; votes; vote_result; proposed_in>.
Record Rules :=
build_rules {
min_vote_count_permille : Z;
margin_needed_permille : Z;
debating_period_in_blocks : Z;
debating_period_in_blocks : nat;
}.
Record Setup :=
......@@ -71,13 +68,8 @@ Record State :=
members : FMap Address unit;
}.
Instance eta_state : Settable _ :=
mkSettable
((constructor build_state) <*> owner
<*> state_rules
<*> proposals
<*> next_proposal_id
<*> members)%settable.
Instance state_settable : Settable _ :=
settable! build_state <owner; state_rules; proposals; next_proposal_id; members>.
Definition version : Version := 1%nat.
......@@ -86,9 +78,12 @@ Definition validate_rules (rules : Rules) : bool :=
&& (rules.(min_vote_count_permille) <=? 1000)
&& (rules.(margin_needed_permille) >=? 0)
&& (rules.(margin_needed_permille) <=? 1000)
&& (rules.(debating_period_in_blocks) >=? 0).
&& (0 <=? rules.(debating_period_in_blocks))%nat.
Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
Definition init
(chain : PackedChain)
(ctx : ContractCallContext)
(setup : Setup) : option State :=
if validate_rules setup.(setup_rules) then
Some {| owner := ctx.(ctx_from);
state_rules := setup.(setup_rules);
......@@ -98,15 +93,15 @@ Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
else
None.
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
Definition add_proposal (actions : list CongressAction) (chain : PackedChain) (state : State) : State :=
let id := state.(next_proposal_id) in
let head_block := chain.(head_block) in
let slot_num := chain.(slot_number) in
let proposal := {| actions := actions;
votes := FMap.empty;
vote_result := 0;
proposed_in := head_block.(block_header).(block_number) |} in
proposed_in := slot_num |} in
let new_proposals := FMap.add id proposal state.(proposals) in
state[[proposals := new_proposals]][[next_proposal_id := (id + 1)%nat]].
state<|proposals := new_proposals|><|next_proposal_id := (id + 1)%nat|>.
Definition vote_on_proposal
(voter : Address)
......@@ -121,8 +116,9 @@ Definition vote_on_proposal
end in
let new_votes := FMap.add voter vote proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote + vote in
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= FMap.add pid new_proposal]]).
let new_proposal :=
proposal<|votes := new_votes|><|vote_result := new_vote_result|> in
Some (state<|proposals ::= FMap.add pid new_proposal|>).
Definition do_retract_vote
(voter : Address)
......@@ -133,10 +129,11 @@ Definition do_retract_vote
do old_vote <- FMap.find voter proposal.(votes);
let new_votes := FMap.remove voter proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote in
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= FMap.add pid new_proposal]]).
let new_proposal :=
proposal<|votes := new_votes|><|vote_result := new_vote_result|> in
Some (state<|proposals ::= FMap.add pid new_proposal|>).
Definition congress_action_to_chain_action (act : CongressAction) : ChainAction :=
Definition congress_action_to_chain_action (act : CongressAction) : ActionBody :=
match act with
| cact_transfer to amt => act_transfer to amt
| cact_call to amt msg => act_call to amt msg
......@@ -145,16 +142,16 @@ Definition congress_action_to_chain_action (act : CongressAction) : ChainAction
Definition do_finish_proposal
(pid : ProposalId)
(state : State)
(chain : Chain)
: option (State * list ChainAction) :=
(chain : PackedChain)
: option (State * list ActionBody) :=
do proposal <- FMap.find pid state.(proposals);
let rules := state.(state_rules) in
let debate_end := (Z.of_nat proposal.(proposed_in)) + rules.(debating_period_in_blocks) in
let cur_block := chain.(head_block) in
if (Z.of_nat cur_block.(block_header).(block_number)) <? debate_end then
let debate_end := (proposal.(proposed_in) + rules.(debating_period_in_blocks))%nat in
let cur_slot := chain.(slot_number) in
if (cur_slot <? debate_end)%nat then
None
else
let new_state := state[[proposals ::= FMap.remove pid]] in
let new_state := state<|proposals ::= FMap.remove pid|> in
let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
let total_members := Z.of_nat (FMap.size state.(members)) in
let aye_votes := (proposal.(vote_result) + total_votes_for_proposal) / 2 in
......@@ -170,30 +167,30 @@ Definition do_finish_proposal
Some (new_state, response_chain_acts).
Definition receive
(chain : PackedChain)
(ctx : ContractCallContext)
(state : State)
(maybe_msg : option Msg)
: option (State * list ChainAction) :=
let chain := ctx.(ctx_chain) in
: option (State * list ActionBody) :=
let sender := ctx.(ctx_from) in
let is_from_owner := (sender =? state.(owner))%address in
let is_from_member := FMap.mem sender state.(members) in
let without_actions := option_map (fun new_state => (new_state, [])) in
match is_from_owner, is_from_member, maybe_msg with
| true, _, Some (transfer_ownership new_owner) =>
Some (state[[owner := new_owner]], [])
Some (state<|owner := new_owner|>, [])
| true, _, Some (change_rules new_rules) =>
if validate_rules new_rules then
Some (state[[state_rules := new_rules]], [])
Some (state<|state_rules := new_rules|>, [])
else
None
| true, _, Some (add_member new_member) =>
Some (state[[members ::= FMap.add new_member tt]], [])
Some (state<|members ::= FMap.add new_member tt|>, [])
| true, _, Some (remove_member old_member) =>
Some (state[[members ::= FMap.remove old_member]], [])
Some (state<|members ::= FMap.remove old_member|>, [])
| _, true, Some (create_proposal actions) =>
Some (add_proposal actions chain state, [])
......@@ -336,8 +333,34 @@ Next Obligation.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
Ltac show_contract_proper :=
repeat
match goal with
| [|- ?x _ = ?x _] => unfold x
| [|- ?x _ _ = ?x _ _] => unfold x
| [|- ?x _ _ _ = ?x _ _ _] => unfold x
| [|- ?x _ _ _ _ = ?x _ _ _ _] => unfold x
| [|- ?x _ _ _ _ = ?x _ _ _ _] => unfold x
| [|- ?x _ _ _ _ _ = ?x _ _ _ _ _] => unfold x
| [|- Some _ = Some _] => f_equal
| [|- pair _ _ = pair _ _] => f_equal
| [|- (if ?x then _ else _) = (if ?x then _ else _)] => destruct x
| [|- match ?x with | _ => _ end = match ?x with | _ => _ end ] => destruct x
| _ => prove
end.
Lemma init_proper ctx setup :
Proper (ChainExtEqual ==> eq) (fun chain => init chain ctx setup).
Proof. intros x y []. show_contract_proper. Qed.
Lemma receive_proper ctx state msg :
Proper (ChainExtEqual ==> eq) (fun chain => receive chain ctx state msg).
Proof. intros x y []. show_contract_proper. Qed.
Definition contract : Contract Setup Msg State :=
build_contract version init receive.
build_contract version init init_proper receive receive_proper.
End Congress.
(*
(* This first property states that the Congress will only send out actions
......@@ -348,5 +371,3 @@ Theorem congress_no_unmatched_actions
(chain : Chain)
(
*)
End Congress.
......@@ -39,6 +39,22 @@ Lemma sumZ_permutation
sumZ f xs = sumZ f ys.
Proof. induction perm_eq; prove. Qed.
Instance sumZ_perm_proper {A : Type} {f : A -> Z} :
Proper (Permutation (A:=A) ==> eq) (sumZ f).
Proof. intros x y perm. now apply sumZ_permutation. Qed.
Local Open Scope Z.
Lemma sumZ_app
{A : Type} {f : A -> Z} {xs ys : list A} :
sumZ f (xs ++ ys) = sumZ f xs + sumZ f ys.
Proof.
revert ys.
induction xs as [| x xs IH]; intros ys; auto.
simpl.
rewrite IH.
lia.
Qed.
Lemma in_app_cons_or {A : Type} (x y : A) (xs ys : list A) :
x <> y ->
In x (xs ++ y :: ys) ->
......@@ -93,3 +109,25 @@ Proof.
rewrite app_assoc in nodup_l_app_m.
generalize in_or_app; prove.
Qed.
Lemma seq_app start len1 len2 :
seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2.
Proof.
revert start.
induction len1 as [| len1 IH]; intros start.
- now rewrite Nat.add_0_r.
- simpl.
rewrite IH.
f_equal; f_equal; f_equal.
lia.
Qed.
Lemma sumZ_seq_S f start len :
sumZ f (seq start (S len)) = sumZ f (seq start len) + f (start + len)%nat.
Proof.
replace (S len) with (len + 1)%nat by lia.
rewrite (seq_app start len 1).
rewrite sumZ_app.
simpl.
lia.
Qed.
......@@ -28,103 +28,54 @@ Instance LocalChainBaseTypes : ChainBaseTypes :=
address_decode_encode := countable.decode_encode;
|}.
Record ChainUpdate :=
build_chain_update {
(* Contracts that had their states updated and the new state *)
upd_contracts : FMap Address OakValue;
(* All transactions caused by update, including internal txs
(due to contract execution) *)
upd_txs : list Tx;
}.
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;
lc_slot : nat;
lc_height : nat;
lc_finalized_height : nat;
lc_incoming_txs : FMap Address (list Tx);
lc_outgoing_txs : FMap Address (list Tx);
lc_contract_states : FMap Address OakValue;
}.
Definition genesis_block : Block :=
{| block_header := {| block_number := 0;
block_coinbase := BoundedN.of_Z_const AddrSize 0; |};
block_txs := [] |}.
Instance eta_local_chain : Settable _ :=
mkSettable
((constructor build_local_chain) <*> lc_blocks
<*> lc_updates)%settable.
Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
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
| [] => None
end.
Definition lc_block_at (lc : LocalChain) (bid : BlockId) : option Block :=
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_blocks) with
| hd :: _ => hd
| [] => genesis_block
end.
Definition lc_incoming_txs (lc : LocalChain) (addr : Address) : list Tx :=
let all_txs := flat_map 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 upd_txs lc.(lc_updates) in
let is_out tx := (tx.(tx_from) =? addr)%address in
filter is_out all_txs.
Definition lc_contract_state (lc : LocalChain) (addr : Address)
: option OakValue :=
find_first (fun u => FMap.find addr u.(upd_contracts)) lc.(lc_updates).
Instance lc_type : ChainType :=
Instance local_chain_settable : Settable _ :=
settable! build_local_chain
< lc_slot; lc_height; lc_finalized_height;
lc_incoming_txs; lc_outgoing_txs; lc_contract_states >.
Instance local_chain_type : ChainType :=
{| chain_type := LocalChain;
chain_at := lc_chain_at;
head_block := lc_head_block;
incoming_txs := lc_incoming_txs;
outgoing_txs := lc_outgoing_txs;
contract_state := lc_contract_state; |}.
slot_number := lc_slot;
block_height := lc_height;
finalized_height := lc_finalized_height;
incoming_txs lc addr := match FMap.find addr lc.(lc_incoming_txs) with
| None => []
| Some l => l
end;
outgoing_txs lc addr := match FMap.find addr lc.(lc_outgoing_txs) with
| None => []
| Some l => l
end;
contract_state lc addr := FMap.find addr lc.(lc_contract_states);
|}.
Definition lc_initial_chain : LocalChain :=
{| lc_blocks := [genesis_block];
lc_updates :=
[{| upd_contracts := FMap.empty;
upd_txs := [] |}] |}.
{| lc_slot := 0;
lc_height := 0;
lc_finalized_height := 0;
lc_incoming_txs := FMap.empty;
lc_outgoing_txs := FMap.empty;
lc_contract_states := FMap.empty; |}.
(* Contains full information about a chain, including contracts *)
Record LocalChainBuilder :=
build_local_chain_builder {
lcb_lc : LocalChain;
lcb_lc :> LocalChain;
lcb_contracts : FMap Address WeakContract;
}.
Instance eta_local_chain_builder : Settable _ :=
mkSettable
((constructor build_local_chain_builder) <*> lcb_lc
<*> lcb_contracts)%settable.
Instance local_chain_builder_settable : Settable _ :=
settable! build_local_chain_builder <lcb_lc; lcb_contracts>.
Definition initial_chain_builder : LocalChainBuilder :=
{| lcb_lc := lc_initial_chain;
......@@ -132,36 +83,169 @@ Definition initial_chain_builder : LocalChainBuilder :=
Section ExecuteActions.
Context (initial_lcb : LocalChainBuilder)
(initial_acts : list ExternalAction).