Formalize and prove some circulation results

src/Circulation.v

+(* 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. *)
+From Coq Require Import List Permutation.
+From SmartContracts Require Import Automation Blockchain Extras.
+Import ListNotations.
+
+Section Circulation.
+Context {Chain : ChainType}.
+
+(* First, we must define the circulation. We will define it as a finite
+sum of the balance over all valid addresses. This is where the assumption
+about finite address space comes into play. With some work this result could
+be improved to assume only that the set of addresses which has seen transactions
+is finite. *)
+Definition IsSetOfAllAddresses (addrs : list Address) : Prop :=
+  NoDup addrs /\ forall a, valid_address a -> In a addrs.
+
+Context {addrs : list Address} (all_addrs : IsSetOfAllAddresses addrs).
+
+Definition circulation (chain : Chain) := sumZ (account_balance chain) addrs.
+
+(* We then prove that over any single step, the circulation is preserved.
+The idea behind this proof is that all_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 transfer_reorganize
+      {pre post : Environment}
+      {act : InternalAction}
+      (transfer : Transfer act pre post)
+  : exists suf, Permutation ([iact_from act; iact_to act] ++ suf) addrs.
+Proof.
+  pose proof (valid_address_from transfer).
+  pose proof (valid_address_to transfer).
+  pose proof (from_neq_to transfer).
+  unfold IsSetOfAllAddresses in *.
+  apply (NoDup_incl_reorganize _ ([iact_from act; iact_to act]));
+    repeat constructor; unfold incl; prove.
+Qed.
+
+Lemma act_circulation_unchanged
+      {pre post : Environment}
+      {act : InternalAction}
+      (transfer : Transfer act pre post) :
+  circulation post = circulation pre.
+Proof.
+  unfold circulation.
+  destruct (transfer_reorganize transfer) as [suf perm].
+  apply Permutation_sym in perm.
+  rewrite 2!(sumZ_permutation perm); prove.
+  rewrite (account_balance_from_pre_post transfer).
+  rewrite (account_balance_to_pre_post transfer).
+  enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
+
+  destruct all_addrs as [addrs_set all_addrs_in].
+  pose proof (Permutation_NoDup perm addrs_set) as perm_set.
+  assert (from_not_in_suf: ~In (iact_from act) suf).
+  { apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
+  assert (to_not_in_suf: ~In (iact_to act) suf).
+  { apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
+
+  clear perm perm_set.
+  pose proof (account_balance_unrelated_pre_post transfer).
+  induction suf as [| x xs IH]; prove.
+Qed.
+
+Hint Resolve act_circulation_unchanged.
+
+Lemma step_circulation_unchanged
+      {pre post : Environment}
+      {x y : list InternalAction}
+      (step : ChainStep pre post x y) :
+  circulation post = circulation pre.
+Proof. destruct step; eauto. Qed.
+
+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 InternalAction}
+      (trace : BlockTrace pre post x y)
+  : circulation post = circulation pre.
+Proof. induction trace; prove; eauto. Qed.
+End Circulation.