Refactor and prove a link between trace and account_balance

theories/Blockchain.v

@@ -17,7 +17,6 @@ Import ListNotations.
 Definition Version := nat.
 
 Definition Amount := Z.
-
 Bind Scope Z_scope with Amount.
 
 Class ChainBase :=
@@ -41,29 +40,35 @@ Delimit Scope address_scope with address.
 Bind Scope address_scope with Address.
 Infix "=?" := address_eqb (at level 70) : address_scope.
 
+Lemma address_eq_refl `{ChainBase} x :
+  address_eqb x x = true.
+Proof. destruct (address_eqb_spec x x); auto; congruence. Qed.
+
+Lemma address_eq_ne `{ChainBase} x y :
+  x <> y ->
+  address_eqb x y = false.
+Proof. destruct (address_eqb_spec x y) as [->|]; tauto. Qed.
+
+Lemma address_eq_sym `{ChainBase} x y :
+  address_eqb x y = address_eqb y x.
+Proof.
+  destruct (address_eqb_spec x y) as [->|].
+  - now rewrite address_eq_refl.
+  - rewrite address_eq_ne; auto.
+Qed.
+
 Global Ltac destruct_address_eq :=
   repeat
     match goal with
-    | [H: context[address_eqb ?a ?b] |- _] => destruct (address_eqb_spec a b)
-    | [|- context[address_eqb ?a ?b]] => destruct (address_eqb_spec a b)
+    | [H: context[address_eqb ?a ?b] |- _] =>
+      try rewrite (address_eq_sym b a) in *; destruct (address_eqb_spec a b)
+    | [|- context[address_eqb ?a ?b]] =>
+      try rewrite (address_eq_sym b a) in *; destruct (address_eqb_spec a b)
     end.
 
 Section Blockchain.
 Context {BaseTypes : ChainBase}.
 
-Lemma address_eq_refl x :
-  address_eqb x x = true.
-Proof. destruct_address_eq; auto; congruence. Qed.
-
-Lemma address_eq_sym x y :
-  address_eqb x y = address_eqb y x.
-Proof. destruct_address_eq; auto; congruence. Qed.
-
-Lemma address_eq_ne x y :
-  x <> y ->
-  address_eqb x y = false.
-Proof. destruct_address_eq; auto; congruence. Qed.
-
 Record BlockHeader :=
   build_block_header {
     block_height : nat;
@@ -326,7 +331,7 @@ Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amou
 Definition set_chain_contract_state
            (addr : Address) (state : OakValue) (map : Address -> option OakValue)
   : Address -> option OakValue :=
-  fun a => if address_eqb a addr
+  fun a => if (a =? addr)%address
            then Some state
            else map a.
 
@@ -718,10 +723,28 @@ Definition outgoing_txs
            (addr : Address) : list Tx :=
   filter (fun tx => (tx_from tx =? addr)%address) (trace_txs trace).
 
+Fixpoint blocks_baked {from to : ChainState}
+         (trace : ChainTrace from to) (addr : Address) : list nat :=
+  match trace with
+  | snoc trace' evt =>
+    match evt with
+    | @evt_block _ header baker _ _ _ _ _ =>
+      if (baker =? addr)%address
+      then block_height header :: blocks_baked trace' addr
+      else blocks_baked trace' addr
+    | _ => blocks_baked trace' addr
+    end
+  | clnil => []
+  end.
+
 Section Theories.
 Ltac destruct_chain_event :=
   match goal with
-  | [evt: ChainEvent _ _ |- _] => destruct evt
+  | [evt: ChainEvent _ _ |- _] =>
+    destruct evt as
+        [prev header baker next queue_prev valid_header acts_from_accs env_eq|
+         prev act acts next new_acts queue_prev step queue_new|
+         prev new prev_new perm]
   end.
 
 Ltac destruct_chain_step :=
@@ -857,6 +880,33 @@ Proof.
     end.
 Qed.
 
+Local Open Scope Z.
+Lemma account_balance_trace state (trace : ChainTrace empty_state state) addr :
+  account_balance state addr =
+  sumZ tx_amount (incoming_txs trace addr) +
+  sumZ compute_block_reward (blocks_baked trace addr) -
+  sumZ tx_amount (outgoing_txs trace addr).
+Proof.
+  unfold incoming_txs, outgoing_txs.
+  remember empty_state as from_state.
+  induction trace; [|destruct_chain_event].
+  - subst. cbn. lia.
+  - (* Block *)
+    rewrite_environment_equiv.
+    cbn.
+    unfold add_balance.
+    rewrite IHtrace by auto.
+    destruct_address_eq; subst; cbn; lia.
+  - (* Step *)
+    cbn.
+    destruct_chain_step; cbn; rewrite_environment_equiv; cbn.
+    all: unfold add_balance; rewrite IHtrace by auto.
+    all: destruct_address_eq; cbn; lia.
+  - cbn.
+    rewrite <- prev_new.
+    auto.
+Qed.
+
 End Theories.
 End Trace.
 End Semantics.
@@ -894,7 +944,11 @@ Arguments build_contract_interface {_ _ _ _}.
 
 Ltac destruct_chain_event :=
   match goal with
-  | [evt: ChainEvent _ _ |- _] => destruct evt
+  | [evt: ChainEvent _ _ |- _] =>
+    destruct evt as
+        [prev header baker next queue_prev valid_header acts_from_accs env_eq|
+         prev act acts next new_acts queue_prev step queue_new|
+         prev new prev_new perm]
   end.
 
 Ltac destruct_chain_step :=

theories/Congress.v

@@ -694,12 +694,6 @@ Arguments num_cacts_in_raw_state : simpl never.
 Arguments num_cacts_in_state : simpl never.
 Arguments num_outgoing_acts !l.
 
-Local Ltac rewrite_queues :=
-  repeat
-    match goal with
-    | [H: chain_state_queue _ = _ |- _] => rewrite H in *
-    end.
-
 Local Ltac solve_single :=
   solve [
       repeat (progress subst; cbn in *; auto);
@@ -780,9 +774,10 @@ Proof.
   remember empty_state eqn:eq.
   (* Contract cannot have been deployed in empty trace so we solve that immediately. *)
   induction trace as [|? ? ? evts IH evt]; subst; try solve_by_inversion.
-  destruct_chain_event; rewrite_queues.
+  destruct_chain_event.
   - (* New block added, does not change any of the values *)
     (* so basically just use IH directly. *)
+    rewrite queue_prev in *.
     rewrite_environment_equiv.
     specialize_hypotheses.
     simpl_goal_invariant.
@@ -790,7 +785,7 @@ Proof.
   - (* Step *)
     unfold outgoing_txs, incoming_txs in *.
     cbn [trace_txs].
-    rewrite_queues.
+    rewrite queue_prev, queue_new in *.
     remember (chain_state_env prev).
     destruct_chain_step; subst pre; cbn [step_tx].
     + (* Transfer step: cannot be to contract, but can come from contract. *)
@@ -819,7 +814,7 @@ Proof.
         (* Outgoing actions in queue is 0 *)
         assert (num_outgoing_acts (chain_state_queue prev) contract = 0)
           as out_acts by eauto.
-        rewrite_queues.
+        rewrite queue_prev in out_acts.
         assert (act_from act <> contract)
           by (eapply undeployed_contract_not_from_self; eauto).
         simpl_hyp_invariant.
@@ -847,7 +842,7 @@ Proof.
         match goal with
         | [H1: wc_receive _ _ _ _ _ = Some _,
            H2: contract_state _ _ = Some _ |- _] =>
-          generalize (wc_receive_state_well_behaved _ _ _ _ _ _ _ _ _ evts e2 e4)
+          generalize (wc_receive_state_well_behaved _ _ _ _ _ _ _ _ _ evts H2 H1)
         end.
         simpl_goal_invariant.
         rewrite num_outgoing_acts_call.
@@ -867,10 +862,7 @@ Proof.
     | [Hperm: Permutation _ _ |- _] => rewrite <- Hperm
     end.
     cbn.
-    match goal with
-    | [H: chain_state_env prev = chain_state_env new |- _] =>
-      rewrite <- H in *
-    end; auto.
+    rewrite <- prev_new in *; auto.
 Qed.
 
 Corollary congress_txs_after_block

theories/LocalBlockchain.v

@@ -444,8 +444,7 @@ Definition add_block
            (finalized_height : nat)
   : option LocalChainBuilder.
 Proof.
-  refine (
-      let lcopt :=
+  set (lcopt :=
          let lc := lcb_lc lcb in
          let new_header :=
              {| block_height := S (block_height (lc_header lc));
@@ -454,12 +453,11 @@ Proof.
          do validate_header new_header (lc_header lc);
          do validate_actions actions;
          let lc := add_new_block new_header baker lc in
-         execute_actions 1000 actions lc depth_first in
-      _).
+         execute_actions 1000 actions lc depth_first).
 
   destruct lcopt as [lc|] eqn:exec; [|exact None].
   subst lcopt.
-  cbn -[execute_actions address_is_contract] in exec.
+  cbn -[execute_actions] in exec.
   destruct (validate_header _) eqn:validate; [|simpl in *; congruence].
   destruct (validate_actions _) eqn:validate_actions; [|simpl in *; congruence].
   destruct_units.