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

Show LocalBlockchain satisfies chain semantics

parent 0fd24c9e
......@@ -190,3 +190,9 @@ Ltac case_match :=
| [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
| [|- context [ match ?x with _ => _ end ]] => destruct x eqn:?
end.
Ltac destruct_units :=
repeat
match goal with
| [u: unit |- _] => destruct u
end.
This diff is collapsed.
......@@ -11,11 +11,11 @@ Section Circulation.
Context {ChainBaseTypes : ChainBaseTypes}.
Context `{Finite Address}.
Definition circulation {Chain : ChainType} (chain : Chain) :=
Definition circulation (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)).
sumZ compute_block_reward (seq (S 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
......@@ -34,10 +34,11 @@ Qed.
Lemma step_from_to_same
{pre : Environment}
{act : Action}
{tx : Tx}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act post new_acts) :
step_from step = step_to step ->
(step : ChainStep pre act tx post new_acts) :
tx_from tx = tx_to tx ->
circulation post = circulation pre.
Proof.
intros from_eq_to.
......@@ -54,12 +55,13 @@ Hint Resolve step_from_to_same.
Lemma step_circulation_unchanged
{pre : Environment}
{act : Action}
{tx : Tx}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act post new_acts) :
(step : ChainStep pre act tx post new_acts) :
circulation post = circulation pre.
Proof.
destruct (address_eqb_spec (step_from step) (step_to step))
destruct (address_eqb_spec (tx_from tx) (tx_to tx))
as [from_eq_to | from_neq_to]; eauto.
destruct (address_reorganize from_neq_to) as [suf perm].
apply Permutation_sym in perm.
......@@ -70,10 +72,10 @@ Proof.
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
pose proof (Permutation_NoDup perm) as perm_set.
assert (from_not_in_suf: ~In (step_from step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
assert (to_not_in_suf: ~In (step_to step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
assert (from_not_in_suf: ~In (tx_from tx) suf).
{ apply (in_NoDup_app _ [tx_from tx; tx_to tx] _); prove. }
assert (to_not_in_suf: ~In (tx_to tx) suf).
{ apply (in_NoDup_app _ [tx_from tx; tx_to tx] _); prove. }
clear perm perm_set.
pose proof (account_balance_post_irrelevant step).
......@@ -86,34 +88,29 @@ Hint Resolve step_circulation_unchanged.
Lemma block_trace_circulation_unchanged
{bef : list Action}
{after : list Action}
(post pre : Environment)
{post pre : Environment}
(trace : BlockTrace pre bef post after)
: circulation post = circulation pre.
Proof.
induction trace;
match goal with
| [IH: _ |- _] => try rewrite <- IH; eauto
| [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.
Lemma circulation_equal (c1 c2 : Chain) :
ChainEquiv c1 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.
Lemma circulation_add_new_block header baker env :
circulation (add_new_block header baker env) =
(circulation env + compute_block_reward (block_height header))%Z.
Proof.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)).
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; prove. }
......@@ -143,62 +140,39 @@ Proof.
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.
{env_start env_end : Environment}
(trace : ChainTrace env_start env_end)
: circulation env_end =
(circulation env_start +
coins_created
(block_height (block_header env_start))
(block_height (block_header env_end)))%Z.
Proof.
induction trace.
- unfold coins_created.
rewrite Nat.sub_diag.
unfold coins_created.
induction trace as
[|prev_start prev_end header baker acts block_start new_end prev_trace IH valid block_trace eq].
- 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.
- unfold IsValidNextBlock in valid.
rewrite (block_header_post_steps block_trace).
rewrite (chain_equiv _ _ eq).
simpl.
rewrite (proj1 valid).
unfold coins_created.
pose proof (block_height_post_trace prev_trace) as height_le.
match goal with
| [|- context[S ?a - ?b]] => replace (S a - b) with (S (a - b)) by lia
end.
rewrite sumZ_seq_S.
unfold coins_created in IH.
rewrite Z.add_assoc, <- IH.
match goal with
| [|- context[S ?a + (?b - ?a)]] => replace (S a + (b - a)) with (S b) by lia
end.
rewrite (block_trace_circulation_unchanged block_trace).
rewrite (circulation_equal _ _ eq).
rewrite circulation_add_new_block.
now rewrite (proj1 valid).
Qed.
End Circulation.
......@@ -81,7 +81,7 @@ Definition validate_rules (rules : Rules) : bool :=
&& (0 <=? rules.(debating_period_in_blocks))%nat.
Definition init
(chain : PackedChain)
(chain : Chain)
(ctx : ContractCallContext)
(setup : Setup) : option State :=
if validate_rules setup.(setup_rules) then
......@@ -93,9 +93,9 @@ Definition init
else
None.
Definition add_proposal (actions : list CongressAction) (chain : PackedChain) (state : State) : State :=
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
let id := state.(next_proposal_id) in
let slot_num := chain.(slot_number) in
let slot_num := chain.(block_header).(slot_number) in
let proposal := {| actions := actions;
votes := FMap.empty;
vote_result := 0;
......@@ -142,12 +142,12 @@ Definition congress_action_to_chain_action (act : CongressAction) : ActionBody :
Definition do_finish_proposal
(pid : ProposalId)
(state : State)
(chain : PackedChain)
(chain : Chain)
: option (State * list ActionBody) :=
do proposal <- FMap.find pid state.(proposals);
let rules := state.(state_rules) in
let debate_end := (proposal.(proposed_in) + rules.(debating_period_in_blocks))%nat in
let cur_slot := chain.(slot_number) in
let cur_slot := chain.(block_header).(slot_number) in
if (cur_slot <? debate_end)%nat then
None
else
......@@ -167,7 +167,7 @@ Definition do_finish_proposal
Some (new_state, response_chain_acts).
Definition receive
(chain : PackedChain)
(chain : Chain)
(ctx : ContractCallContext)
(state : State)
(maybe_msg : option Msg)
......@@ -333,7 +333,7 @@ Next Obligation.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
Ltac show_contract_proper :=
Ltac solve_contract_proper :=
repeat
match goal with
| [|- ?x _ = ?x _] => unfold x
......@@ -349,13 +349,13 @@ Ltac show_contract_proper :=
| _ => 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 init_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq) init.
Proof. repeat intro; solve_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.
Lemma receive_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive.
Proof. repeat intro; solve_contract_proper. Qed.
Definition contract : Contract Setup Msg State :=
build_contract version init init_proper receive receive_proper.
......
......@@ -23,6 +23,8 @@ Module FMap.
Notation size := stdpp.base.size.
Notation of_list := fin_maps.list_to_map.
Notation union := stdpp.base.union.
Notation alter := stdpp.base.alter.
Notation partial_alter := stdpp.base.partial_alter.
Section Theories.
Context {K V : Type} `{countable.Countable K}.
......@@ -52,6 +54,15 @@ Module FMap.
Lemma find_add_ne (m : FMap K V) (k k' : K) (v : V) :
k <> k' -> find k' (add k v m) = find k' m.
Proof. apply fin_maps.lookup_insert_ne. Qed.
Lemma find_partial_alter (m : FMap K V) f k :
find k (partial_alter f k m) = f (find k m).
Proof. apply fin_maps.lookup_partial_alter. Qed.
Lemma find_partial_alter_ne (m : FMap K V) f k k' :
k <> k' ->
find k' (partial_alter f k m) = find k' m.
Proof. apply fin_maps.lookup_partial_alter_ne. Qed.
End Theories.
End FMap.
......
......@@ -27,6 +27,13 @@ Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A)
| [] => []
end.
Definition with_default {A : Type} (a : A) (o : option A) : A :=
match o with
| Some v => v
| None => a
end.
Fixpoint sumZ {A : Type} (f : A -> Z) (xs : list A) : Z :=
match xs with
| [] => 0
......
This diff is collapsed.
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