Circulation.v 5.19 KB
Newer Older
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. *)
5
From Coq Require Import List Permutation ZArith Psatz Morphisms.
6
From SmartContracts Require Import Automation Blockchain Extras Finite ChainedList.
7
8
9
10
From RecordUpdate Require Import RecordSet.
Import ListNotations.

Section Circulation.
11
Context {ChainBase : ChainBase}.
12
13
Context `{Finite Address}.

14
Local Open Scope Z.
15
16
17
Definition circulation (chain : Chain) :=
  sumZ (account_balance chain) (elements Address).

18
(* We then prove that over any single action, the circulation is preserved.
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's avatar
Jakob Botsch Nielsen committed
29
30
31
32
    repeat constructor; unfold incl; auto.
  intros Hin.
  cbn in *.
  intuition.
33
34
Qed.

35
Lemma eval_action_from_to_same
36
37
38
39
      {pre : Environment}
      {act : Action}
      {post : Environment}
      {new_acts : list Action}
40
41
      (eval : ActionEvaluation pre act post new_acts) :
  eval_from eval = eval_to eval ->
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.
48
  - cbn in *.
49
    rewrite IH, (account_balance_post eval), from_eq_to.
50
51
52
    lia.
Qed.

53
Hint Resolve eval_action_from_to_same : core.
54

55
Lemma eval_action_circulation_unchanged
56
57
58
      {pre : Environment}
      {act : Action}
      {post : Environment}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
59
      {new_acts : list Action} :
60
  ActionEvaluation pre act post new_acts ->
61
62
  circulation post = circulation pre.
Proof.
63
64
  intros eval.
  destruct (address_eqb_spec (eval_from eval) (eval_to eval))
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's avatar
Jakob Botsch Nielsen committed
69
70
  rewrite 2!(sumZ_permutation perm).
  cbn.
71
72
  rewrite (account_balance_post_to eval from_neq_to).
  rewrite (account_balance_post_from eval from_neq_to).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
73
  enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by lia.
74
75

  pose proof (Permutation_NoDup perm) as perm_set.
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. }
80
81

  clear perm perm_set.
82
  pose proof (account_balance_post_irrelevant eval) as balance_irrel.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
83
84
85
  induction suf as [| x xs IH]; auto.
  cbn in *.
  rewrite IH, balance_irrel; auto.
86
87
Qed.

88
Hint Resolve eval_action_circulation_unchanged : core.
89

90
91
Instance circulation_proper :
  Proper (ChainEquiv ==> eq) circulation.
92
Proof.
93
  intros x y [].
94
  unfold circulation, account_balance.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
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.
102
103
Qed.

104
105
106
Lemma circulation_add_new_block header env :
  circulation (add_new_block_to_env header env) =
  (circulation env + block_reward header)%Z.
107
Proof.
108
  assert (Hperm: exists suf, Permutation ([block_creator header] ++ suf) (elements Address)).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
109
  { apply NoDup_incl_reorganize; repeat constructor; unfold incl; auto. }
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.
115
  cbn.
116
117
  unfold add_balance.
  rewrite address_eq_refl.
118
  match goal with
119
  | [|- ?a + ?b + ?c = ?b + ?d + ?a] => enough (c = d) by lia
120
  end.
121

122
123
124
  pose proof (in_NoDup_app
                (block_creator header)
                [block_creator header] suf ltac:(intuition) perm_set) as not_in_suf.
125
  clear perm perm_set.
126
  induction suf as [| x xs IH]; auto.
127
  cbn in *.
128
  apply Decidable.not_or in not_in_suf.
129
  destruct (address_eqb_spec x (block_creator header)); try tauto.
130
131
132
133
  specialize (IH (proj2 not_in_suf)).
  lia.
Qed.

134
Lemma step_circulation {prev next} (step : ChainStep prev next) :
135
  circulation next =
136
  match step with
137
138
  | step_block header _ _ _ _ =>
    circulation prev + block_reward header
139
140
  | _ => circulation prev
  end%Z.
141
Proof.
142
  destruct_chain_step; try rewrite_environment_equiv.
143
144
  - (* New block *)
    now rewrite circulation_add_new_block.
145
146
  - (* New action *)
    erewrite eval_action_circulation_unchanged; eauto.
147
148
149
150
151
  - (* Permute queue *)
    intuition.
Qed.

Theorem chain_trace_circulation
152
153
154
        {state : ChainState}
        (trace : ChainTrace empty_state state) :
  circulation state = sumZ block_reward (trace_blocks trace).
155
156
Proof.
  remember empty_state as from eqn:eq.
157
  induction trace as [| from mid to xs IH x]; subst.
158
  - unfold circulation.
159
    induction (elements Address); auto.
160
  - rewrite (step_circulation x).
161
162
163
164
165
    cbn.
    destruct_chain_step; auto.
    cbn.
    rewrite <- IH by auto.
    lia.
166
167
Qed.
End Circulation.