Circulation.v 5.19 KB
 Jakob Botsch Nielsen committed Apr 19, 2019 1 2 3 4 ``````(* In this file we prove various results about the circulation of coins in any chain implementing a chain type. More specifically, we show that the circulation does not change during execution of blocks. This is proven under the (implicit) assumption that the address space is finite. *) `````` Jakob Botsch Nielsen committed Apr 22, 2019 5 ``````From Coq Require Import List Permutation ZArith Psatz Morphisms. `````` Jakob Botsch Nielsen committed May 05, 2019 6 ``````From SmartContracts Require Import Automation Blockchain Extras Finite ChainedList. `````` Jakob Botsch Nielsen committed Apr 19, 2019 7 8 9 10 ``````From RecordUpdate Require Import RecordSet. Import ListNotations. Section Circulation. `````` Jakob Botsch Nielsen committed May 14, 2019 11 ``````Context {ChainBase : ChainBase}. `````` Jakob Botsch Nielsen committed Apr 19, 2019 12 13 ``````Context `{Finite Address}. `````` Jakob Botsch Nielsen committed Jun 06, 2019 14 ``````Local Open Scope Z. `````` Jakob Botsch Nielsen committed Apr 19, 2019 15 16 17 ``````Definition circulation (chain : Chain) := sumZ (account_balance chain) (elements Address). `````` Jakob Botsch Nielsen committed Jun 07, 2019 18 ``````(* We then prove that over any single action, the circulation is preserved. `````` Jakob Botsch Nielsen committed Apr 19, 2019 19 20 21 22 23 24 25 26 27 28 ``````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 the sum of their balances is the same as before. For the rest of the list the total balance will then not be affected which follows by induction. *) Lemma address_reorganize {a b : Address} : a <> b -> exists suf, Permutation ([a; b] ++ suf) (elements Address). Proof. intros a_neq_b. apply (NoDup_incl_reorganize _ [a; b]); `````` Jakob Botsch Nielsen committed May 05, 2019 29 30 31 32 `````` repeat constructor; unfold incl; auto. intros Hin. cbn in *. intuition. `````` Jakob Botsch Nielsen committed Apr 19, 2019 33 34 ``````Qed. `````` Jakob Botsch Nielsen committed Jun 07, 2019 35 ``````Lemma eval_action_from_to_same `````` Jakob Botsch Nielsen committed Apr 19, 2019 36 37 38 39 `````` {pre : Environment} {act : Action} {post : Environment} {new_acts : list Action} `````` Jakob Botsch Nielsen committed Jun 07, 2019 40 41 `````` (eval : ActionEvaluation pre act post new_acts) : eval_from eval = eval_to eval -> `````` Jakob Botsch Nielsen committed Apr 19, 2019 42 43 44 45 46 47 `````` circulation post = circulation pre. Proof. intros from_eq_to. unfold circulation. induction (elements Address) as [| x xs IH]. - reflexivity. `````` Jakob Botsch Nielsen committed Apr 26, 2019 48 `````` - cbn in *. `````` Jakob Botsch Nielsen committed Jun 07, 2019 49 `````` rewrite IH, (account_balance_post eval), from_eq_to. `````` Jakob Botsch Nielsen committed Apr 19, 2019 50 51 52 `````` lia. Qed. `````` Jakob Botsch Nielsen committed Jun 07, 2019 53 ``````Hint Resolve eval_action_from_to_same : core. `````` Jakob Botsch Nielsen committed Apr 19, 2019 54 `````` `````` Jakob Botsch Nielsen committed Jun 07, 2019 55 ``````Lemma eval_action_circulation_unchanged `````` Jakob Botsch Nielsen committed Apr 19, 2019 56 57 58 `````` {pre : Environment} {act : Action} {post : Environment} `````` Jakob Botsch Nielsen committed May 09, 2019 59 `````` {new_acts : list Action} : `````` Jakob Botsch Nielsen committed Jun 07, 2019 60 `````` ActionEvaluation pre act post new_acts -> `````` Jakob Botsch Nielsen committed Apr 19, 2019 61 62 `````` circulation post = circulation pre. Proof. `````` Jakob Botsch Nielsen committed Jun 07, 2019 63 64 `````` intros eval. destruct (address_eqb_spec (eval_from eval) (eval_to eval)) `````` Jakob Botsch Nielsen committed Apr 19, 2019 65 66 67 68 `````` as [from_eq_to | from_neq_to]; eauto. destruct (address_reorganize from_neq_to) as [suf perm]. apply Permutation_sym in perm. unfold circulation. `````` Jakob Botsch Nielsen committed May 05, 2019 69 70 `````` rewrite 2!(sumZ_permutation perm). cbn. `````` Jakob Botsch Nielsen committed Jun 07, 2019 71 72 `````` rewrite (account_balance_post_to eval from_neq_to). rewrite (account_balance_post_from eval from_neq_to). `````` Jakob Botsch Nielsen committed May 05, 2019 73 `````` enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by lia. `````` Jakob Botsch Nielsen committed Apr 19, 2019 74 75 `````` pose proof (Permutation_NoDup perm) as perm_set. `````` Jakob Botsch Nielsen committed Jun 07, 2019 76 77 78 79 `````` assert (from_not_in_suf: ~In (eval_from eval) suf). { apply (in_NoDup_app _ [eval_from eval; eval_to eval] _); intuition. } assert (to_not_in_suf: ~In (eval_to eval) suf). { apply (in_NoDup_app _ [eval_from eval; eval_to eval] _); intuition. } `````` Jakob Botsch Nielsen committed Apr 19, 2019 80 81 `````` clear perm perm_set. `````` Jakob Botsch Nielsen committed Jun 07, 2019 82 `````` pose proof (account_balance_post_irrelevant eval) as balance_irrel. `````` Jakob Botsch Nielsen committed May 05, 2019 83 84 85 `````` induction suf as [| x xs IH]; auto. cbn in *. rewrite IH, balance_irrel; auto. `````` Jakob Botsch Nielsen committed Apr 19, 2019 86 87 ``````Qed. `````` Jakob Botsch Nielsen committed Jun 07, 2019 88 ``````Hint Resolve eval_action_circulation_unchanged : core. `````` Jakob Botsch Nielsen committed Apr 19, 2019 89 `````` `````` Jakob Botsch Nielsen committed Apr 22, 2019 90 91 ``````Instance circulation_proper : Proper (ChainEquiv ==> eq) circulation. `````` Jakob Botsch Nielsen committed Apr 19, 2019 92 ``````Proof. `````` Jakob Botsch Nielsen committed Apr 22, 2019 93 `````` intros x y []. `````` Jakob Botsch Nielsen committed Apr 19, 2019 94 `````` unfold circulation, account_balance. `````` Jakob Botsch Nielsen committed May 05, 2019 95 96 97 98 99 100 101 `````` induction (elements Address) as [|z zs IH]; auto. cbn. now repeat match goal with | [H: _ |- _] => rewrite H end. `````` Jakob Botsch Nielsen committed Apr 19, 2019 102 103 ``````Qed. `````` Jakob Botsch Nielsen committed Jun 21, 2019 104 105 106 ``````Lemma circulation_add_new_block header env : circulation (add_new_block_to_env header env) = (circulation env + block_reward header)%Z. `````` Jakob Botsch Nielsen committed Apr 19, 2019 107 ``````Proof. `````` Jakob Botsch Nielsen committed Jun 21, 2019 108 `````` assert (Hperm: exists suf, Permutation ([block_creator header] ++ suf) (elements Address)). `````` Jakob Botsch Nielsen committed May 05, 2019 109 `````` { apply NoDup_incl_reorganize; repeat constructor; unfold incl; auto. } `````` Jakob Botsch Nielsen committed Apr 19, 2019 110 111 112 113 114 `````` destruct Hperm as [suf perm]. symmetry in perm. pose proof (Permutation_NoDup perm (elements_set Address)) as perm_set. unfold circulation. rewrite perm. `````` Jakob Botsch Nielsen committed Apr 26, 2019 115 `````` cbn. `````` Jakob Botsch Nielsen committed Jun 06, 2019 116 117 `````` unfold add_balance. rewrite address_eq_refl. `````` Jakob Botsch Nielsen committed Apr 26, 2019 118 `````` match goal with `````` Jakob Botsch Nielsen committed Jun 06, 2019 119 `````` | [|- ?a + ?b + ?c = ?b + ?d + ?a] => enough (c = d) by lia `````` Jakob Botsch Nielsen committed Apr 26, 2019 120 `````` end. `````` Jakob Botsch Nielsen committed Apr 19, 2019 121 `````` `````` Jakob Botsch Nielsen committed Jun 21, 2019 122 123 124 `````` pose proof (in_NoDup_app (block_creator header) [block_creator header] suf ltac:(intuition) perm_set) as not_in_suf. `````` Jakob Botsch Nielsen committed Jun 06, 2019 125 `````` clear perm perm_set. `````` Jakob Botsch Nielsen committed Apr 19, 2019 126 `````` induction suf as [| x xs IH]; auto. `````` Jakob Botsch Nielsen committed Apr 26, 2019 127 `````` cbn in *. `````` Jakob Botsch Nielsen committed Apr 19, 2019 128 `````` apply Decidable.not_or in not_in_suf. `````` Jakob Botsch Nielsen committed Jun 21, 2019 129 `````` destruct (address_eqb_spec x (block_creator header)); try tauto. `````` Jakob Botsch Nielsen committed Apr 19, 2019 130 131 132 133 `````` specialize (IH (proj2 not_in_suf)). lia. Qed. `````` Jakob Botsch Nielsen committed Jun 07, 2019 134 ``````Lemma step_circulation {prev next} (step : ChainStep prev next) : `````` Jakob Botsch Nielsen committed Apr 29, 2019 135 `````` circulation next = `````` Jakob Botsch Nielsen committed Jun 07, 2019 136 `````` match step with `````` Jakob Botsch Nielsen committed Jun 21, 2019 137 138 `````` | step_block header _ _ _ _ => circulation prev + block_reward header `````` Jakob Botsch Nielsen committed Apr 29, 2019 139 140 `````` | _ => circulation prev end%Z. `````` Jakob Botsch Nielsen committed Apr 19, 2019 141 ``````Proof. `````` Jakob Botsch Nielsen committed Jun 21, 2019 142 `````` destruct_chain_step; try rewrite_environment_equiv. `````` Jakob Botsch Nielsen committed Apr 29, 2019 143 144 `````` - (* New block *) now rewrite circulation_add_new_block. `````` Jakob Botsch Nielsen committed Jun 07, 2019 145 146 `````` - (* New action *) erewrite eval_action_circulation_unchanged; eauto. `````` Jakob Botsch Nielsen committed Apr 29, 2019 147 148 149 150 151 `````` - (* Permute queue *) intuition. Qed. Theorem chain_trace_circulation `````` Jakob Botsch Nielsen committed Jun 21, 2019 152 153 154 `````` {state : ChainState} (trace : ChainTrace empty_state state) : circulation state = sumZ block_reward (trace_blocks trace). `````` Jakob Botsch Nielsen committed Apr 29, 2019 155 156 ``````Proof. remember empty_state as from eqn:eq. `````` Jakob Botsch Nielsen committed Jun 21, 2019 157 `````` induction trace as [| from mid to xs IH x]; subst. `````` Jakob Botsch Nielsen committed Apr 29, 2019 158 `````` - unfold circulation. `````` Jakob Botsch Nielsen committed Apr 22, 2019 159 `````` induction (elements Address); auto. `````` Jakob Botsch Nielsen committed Jun 07, 2019 160 `````` - rewrite (step_circulation x). `````` Jakob Botsch Nielsen committed Jun 21, 2019 161 162 163 164 165 `````` cbn. destruct_chain_step; auto. cbn. rewrite <- IH by auto. lia. `````` Jakob Botsch Nielsen committed Apr 19, 2019 166 167 ``````Qed. End Circulation.``````