Add ChainEvent, ChainState and CursorList types

These abstract the list structure of the trace away from the events, so
that a trace is now a CursorList of ChainEvent values. The ChainState is
a new type for the environment and queue.

src/Automation.v

@@ -180,3 +180,8 @@ Ltac destruct_units :=
     match goal with
     | [u: unit |- _] => destruct u
     end.
+
+Ltac solve_by_rewrite :=
+  match goal with
+  | [H: _ |- _] => now rewrite H
+  end.

src/Blockchain.v

@@ -8,6 +8,7 @@ From SmartContracts Require Import Oak.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Extras.
 From SmartContracts Require Import Automation.
+From SmartContracts Require Import CursorList.
 From RecordUpdate Require Import RecordUpdate.
 From stdpp Require countable.
 
@@ -712,146 +713,93 @@ Definition IsValidNextBlock (new old : BlockHeader) : Prop :=
   finalized_height new >= finalized_height old /\
   finalized_height new < block_height new.
 
-Definition empty_env : Environment :=
-  {| env_chain :=
-       {| block_header :=
-            {| block_height := 0;
-               slot_number := 0;
-               finalized_height := 0; |};
-          incoming_txs a := [];
-          outgoing_txs a := [];
-          blocks_baked a := [];
-          contract_state a := None; |};
-     env_contracts a := None; |}.
+Record ChainState :=
+  build_chain_state {
+    chain_state_env :> Environment;
+    chain_state_queue : list Action;
+  }.
 
-(* The ChainTrace captures that there is a valid execution where,
-starting from one environment and queue of actions, we end up in a
-different environment and queue of actions. *)
-Inductive ChainTrace :
-  Environment -> list Action ->
-  Environment -> list Action -> Type :=
-  | ctrace_refl :
-      forall {env l}, ChainTrace env l env l
-  (* Add a new block to the trace *)
-  | ctrace_block :
-      forall {from : Environment}
-             {from_queue : list Action}
-             {prev_to : Environment}
+Inductive ChainEvent : ChainState -> ChainState -> Type :=
+  | evt_block :
+      forall {prev : ChainState}
              {header : BlockHeader}
              {baker : Address}
-             {to : Environment}
-             {queue : list Action},
-        ChainTrace from from_queue prev_to [] ->
-        IsValidNextBlock header (block_header prev_to) ->
-        Forall (fun act => address_is_contract (act_from act) = false) queue ->
+             {next : ChainState},
+        chain_state_queue prev = [] ->
+        IsValidNextBlock header (block_header prev) ->
+        Forall
+          (fun act => address_is_contract (act_from act) = false)
+          (chain_state_queue next) ->
         EnvironmentEquiv
-          to
-          (add_new_block_header header baker prev_to) ->
-        ChainTrace from from_queue to queue
-  (* Execute an action *)
-  | ctrace_step :
-      forall {from : Environment}
-             {from_queue : list Action}
-             {prev_to : Environment}
+          next
+          (add_new_block_header header baker prev) ->
+        ChainEvent prev next
+  | evt_step :
+      forall {prev : ChainState}
              {act : Action}
              {acts : list Action}
-             {new : Environment}
+             {next : ChainState}
              {new_acts : list Action},
-        ChainTrace from from_queue prev_to (act :: acts) ->
-        ChainStep prev_to act new new_acts ->
-        ChainTrace from from_queue new (new_acts ++ acts)
-  (* Reorder action order *)
-  | ctrace_permute :
-      forall {from : Environment}
-             {from_queue : list Action}
-             {to : Environment}
-             {to_queue to_queue' : list Action},
-        ChainTrace from from_queue to to_queue ->
-        Permutation to_queue to_queue' ->
-        ChainTrace from from_queue to to_queue'.
-
-Fixpoint trace_app
-            {from mid to : Environment}
-            {from_queue mid_queue to_queue : list Action}
-            (c1 : ChainTrace from from_queue mid mid_queue)
-            (c2 : ChainTrace mid mid_queue to to_queue)
-   : ChainTrace from from_queue to to_queue :=
-  match c2 with
-  | ctrace_refl => fun c1 => c1
-  | ctrace_block pref valid from_accs eq =>
-    fun c1 => ctrace_block (trace_app c1 pref) valid from_accs eq
-  | ctrace_step pref step =>
-    fun c1 => ctrace_step (trace_app c1 pref) step
-  | ctrace_permute pref perm =>
-    fun c1 => ctrace_permute (trace_app c1 pref) perm
-  end c1.
-
-Infix "++" := trace_app (right associativity, at level 60).
-
-Definition trace_prefix
-           {from mid to : Environment}
-           {from_queue mid_queue to_queue : list Action}
-           (pref : ChainTrace from from_queue mid mid_queue)
-           (full : ChainTrace from from_queue to to_queue) : Prop :=
-  exists suffix, full = pref ++ suffix.
-
-Definition trace_suffix
-           {from mid to : Environment}
-           {from_queue mid_queue to_queue : list Action}
-           (suf : ChainTrace mid mid_queue to to_queue)
-           (full : ChainTrace from from_queue to to_queue) : Prop :=
-  exists prefix, full = prefix ++ suf.
-
-Section Theories.
-Lemma trace_app_refl_l
-      {from to from_queue to_queue}
-      (trace : ChainTrace from from_queue to to_queue) :
-  ctrace_refl ++ trace = trace.
-Proof.
-  induction trace; cbn; auto;
-    match goal with
-    | [IH: _ |- _] => now rewrite IH
-    end.
-Qed.
+        chain_state_queue prev = act :: acts ->
+        ChainStep prev act next new_acts ->
+        chain_state_queue next = new_acts ++ acts ->
+        ChainEvent prev next
+  | evt_permute :
+      forall {prev new : ChainState},
+        chain_state_env prev = chain_state_env new ->
+        Permutation (chain_state_queue prev) (chain_state_queue new) ->
+        ChainEvent prev new.
+
+Definition empty_state : ChainState :=
+  {| chain_state_env :=
+       {| env_chain :=
+            {| block_header :=
+                 {| block_height := 0;
+                    slot_number := 0;
+                    finalized_height := 0; |};
+               incoming_txs a := [];
+               outgoing_txs a := [];
+               blocks_baked a := [];
+               contract_state a := None; |};
+          env_contracts a := None; |};
+     chain_state_queue := [] |}.
 
-Lemma trace_app_assoc
-      {env1 env2 env3 env4 queue1 queue2 queue3 queue4}
-      (c1 : ChainTrace env1 queue1 env2 queue2)
-      (c2 : ChainTrace env2 queue2 env3 queue3)
-      (c3 : ChainTrace env3 queue3 env4 queue4) :
-  c1 ++ c2 ++ c3 = (c1 ++ c2) ++ c3.
-Proof.
-  revert env1 env2 queue1 queue2 c1 c2.
-  induction c3; intros env1 env2 queue1 queue2 c1 c2; cbn; auto;
-    match goal with
-    | [IH: _ |- _] => now rewrite IH
-    end.
-Qed.
+(* The ChainTrace captures that there is a valid execution where,
+starting from one environment and queue of actions, we end up in a
+different environment and queue of actions. *)
+Definition ChainTrace := CursorList ChainState ChainEvent.
 
+Section Theories.
 Ltac rewrite_environment_equiv :=
   match goal with
   | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
   end.
 
+Ltac destruct_event :=
+  match goal with
+  | [H: ChainEvent _ _ |- _] => destruct H
+  end.
+
 Ltac destruct_step :=
   match goal with
   | [H: ChainStep _ _ _ _ |- _] => destruct H
   end.
 
 Lemma contract_addr_format
-      {to to_queue}
-      (trace : ChainTrace empty_env [] to to_queue)
+      {to}
+      (trace : ChainTrace empty_state to)
       (addr : Address) (wc : WeakContract) :
   env_contracts to addr = Some wc ->
   address_is_contract addr = true.
 Proof.
   intros contract_at_addr.
-  remember empty_env eqn:eq.
-  induction trace; rewrite eq in *; clear eq;
-    try rewrite_environment_equiv; cbn in *; auto.
-  - congruence.
-  - destruct_step; rewrite_environment_equiv; cbn in *; auto.
-    destruct_address_eq; subst; auto.
+  remember empty_state eqn:eq.
+  induction trace; rewrite eq in *; clear eq.
+  - cbn in *; congruence.
+  - destruct_event.
+    + rewrite_environment_equiv; cbn in *; auto.
+    + destruct_step; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
+    + intuition.
 Qed.
 
 End Theories.
@@ -875,18 +823,12 @@ Class ChainBuilderType :=
       option builder_type;
 
     builder_trace (b : builder_type) :
-      inhabited (ChainTrace empty_env [] (builder_env b) []);
+      inhabited (ChainTrace empty_state (build_chain_state (builder_env b) []));
   }.
 
 Global Coercion builder_type : ChainBuilderType >-> Sortclass.
 End Blockchain.
 
-Delimit Scope trace_scope with trace.
-Bind Scope trace_scope with ChainTrace.
-Infix "++" := trace_app (right associativity, at level 60) : trace_scope.
-Infix "`prefix_of`" := trace_prefix (at level 70) : trace_scope.
-Infix "`suffix_of`" := trace_suffix (at level 70) : trace_scope.
-
 Arguments version {_ _ _ _ _ _ _}.
 Arguments init {_ _ _ _ _ _ _}.
 Arguments receive {_ _ _ _ _ _ _}.

src/Circulation.v

@@ -3,7 +3,7 @@ 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 ZArith Psatz Morphisms.
-From SmartContracts Require Import Automation Blockchain Extras Finite.
+From SmartContracts Require Import Automation Blockchain Extras Finite CursorList.
 From RecordUpdate Require Import RecordSet.
 Import ListNotations.
 
@@ -118,29 +118,44 @@ Proof.
   lia.
 Qed.
 
-Theorem chain_trace_circulation
-        {env : Environment}
-        (trace : ChainTrace empty_env [] env [])
-  : circulation env =
-    sumZ compute_block_reward (seq 1 (block_height (block_header env))).
+Lemma event_circulation {prev next} (evt : ChainEvent prev next) :
+  circulation next =
+  match evt with
+  | evt_block _ _ _ _ =>
+    circulation prev + compute_block_reward (block_height (block_header next))
+  | _ => circulation prev
+  end%Z.
 Proof.
-  remember empty_env as from eqn:eq.
-  induction trace; rewrite eq in *; clear eq;
+  destruct evt;
     repeat
       match goal with
-      | [H: EnvironmentEquiv empty_env _ |- _] => rewrite <- H in *; clear H
       | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *; clear H
       end.
-  - (* Initial chain *)
-    unfold circulation.
+  - (* New block *)
+    now rewrite circulation_add_new_block.
+  - (* New step *)
+    erewrite step_circulation_unchanged; eauto.
+  - (* Permute queue *)
+    intuition.
+Qed.
+
+Theorem chain_trace_circulation
+        {state : ChainState}
+        (trace : ChainTrace empty_state state)
+  : circulation state =
+    sumZ compute_block_reward (seq 1 (block_height (block_header state))).
+Proof.
+  remember empty_state as from eqn:eq.
+  induction trace as [| from mid to xs IH x]; rewrite eq in *; clear eq.
+  - unfold circulation.
     induction (elements Address); auto.
-  - (* New block header. Generates new coins, so idea is to just split the sumZ. *)
-    rewrite circulation_add_new_block.
-    cbn.
-    match goal with
-    | [H: IsValidNextBlock _ _, IH: _ |- _] => now rewrite (proj1 H), sumZ_seq_S, IH
-    end.
-  - erewrite step_circulation_unchanged, block_header_post_step; eauto.
-  - auto.
+  - rewrite (event_circulation x).
+    destruct x.
+    + match goal with
+      | [H: EnvironmentEquiv _ _, H': IsValidNextBlock _ _ |- _] =>
+        now rewrite H in *; cbn; rewrite (proj1 H'), sumZ_seq_S, IH
+      end.
+    + erewrite block_header_post_step; eauto.
+    + intuition.
 Qed.
 End Circulation.

src/CursorList.v

+(* This file implements, for lack of a better name, a cursor list.
+This is a list for which each element contains a "cursor" type: each
+element is parameterized over a 'from' and 'to' element of this type,
+which must match with the previous element. For that reason this is
+also a snoc list. Note that this is not unlike fhlist from CPDT,
+except we place further restrictions on it. *)
+From SmartContracts Require Import Automation.
+Section CursorList.
+Context {cursor_type : Type} {elm_type : cursor_type -> cursor_type -> Type}.
+
+Inductive CursorList : cursor_type -> cursor_type -> Type :=
+  | nil : forall {elm}, CursorList elm elm
+  | snoc : forall {from mid to}, CursorList from mid -> elm_type mid to -> CursorList from to.
+
+Definition snoc_eq
+           {from mid mid' to}
+           (xs : CursorList from mid)
+           (x : elm_type mid' to) :
+  mid' = mid -> CursorList from to :=
+  fun eq =>
+    snoc xs (match eq with eq_refl => x end).
+
+Fixpoint clist_app
+           {from mid to}
+           (xs : CursorList from mid)
+           (ys : CursorList mid to) : CursorList from to :=
+  match ys with
+  | nil => fun xs => xs
+  | snoc ys' y => fun xs => snoc (clist_app xs ys') y
+  end xs.
+
+Infix "++" := clist_app (right associativity, at level 60).
+
+Definition clist_prefix
+           {from mid to}
+           (prefix : CursorList from mid)
+           (full : CursorList from to) : Prop :=
+  exists suffix, full = prefix ++ suffix.
+
+Definition clist_suffix
+           {from mid to}
+           (suffix : CursorList mid to)
+           (full : CursorList from to) : Prop :=
+  exists prefix, full = prefix ++ suffix.
+
+Infix "`prefix_of`" := clist_prefix (at level 70).
+Infix "`suffix_of`" := clist_suffix (at level 70).
+
+Section Theories.
+Lemma clist_app_nil_l {from to} (xs : CursorList from to) :
+  nil ++ xs = xs.
+Proof. induction xs; auto; cbn; solve_by_rewrite. Qed.
+
+Lemma clist_app_assoc
+      {c1 c2 c3 c4}
+      (xs : CursorList c1 c2)
+      (ys : CursorList c2 c3)
+      (zs : CursorList c3 c4) :
+  xs ++ ys ++ zs = (xs ++ ys) ++ zs.
+Proof. induction zs; intros; auto; cbn; solve_by_rewrite. Qed.
+End Theories.
+
+Lemma prefix_of_app
+      {from mid to to'}
+      {prefix : CursorList from mid}
+      {xs : CursorList from to}
+      {suffix : CursorList to to'} :
+  prefix `prefix_of` xs ->
+  prefix `prefix_of` xs ++ suffix.
+Proof.
+  intros [ex_suffix ex_suffix_eq_app].
+  exists (ex_suffix ++ suffix).
+  rewrite clist_app_assoc; congruence.
+Qed.
+End CursorList.
+
+Delimit Scope clist_scope with trace.
+Bind Scope clist_scope with CursorList.
+Infix "++" := clist_app (right associativity, at level 60) : clist_scope.
+
+Infix "`prefix_of`" := clist_prefix (at level 70) : clist_scope.
+Infix "`suffix_of`" := clist_suffix (at level 70) : clist_scope.
+
+Arguments CursorList : clear implicits.

src/LocalBlockchain.v

@@ -9,6 +9,7 @@ From SmartContracts Require Import Extras.
 From SmartContracts Require Import Automation.
 From SmartContracts Require Import BoundedN.
 From SmartContracts Require Import Circulation.
+From SmartContracts Require Import CursorList.
 From RecordUpdate Require Import RecordUpdate.
 From Coq Require Import List.
 From Coq Require Import Psatz.
@@ -323,9 +324,9 @@ Section ExecuteActions.
   Qed.
 
   Lemma execute_steps_trace gas acts (lc lc_final : LocalChain) df :
-    inhabited (ChainTrace empty_env [] lc acts) ->
+    inhabited (ChainTrace empty_state (build_chain_state lc acts)) ->
     execute_steps gas acts lc df = Some lc_final ->
-    inhabited (ChainTrace empty_env [] lc_final []).
+    inhabited (ChainTrace empty_state (build_chain_state lc_final [])).
   Proof.
     revert acts lc lc_final.
     induction gas as [| gas IH]; intros acts lc lc_final trace exec; cbn in *.
@@ -335,9 +336,15 @@ Section ExecuteActions.
         cbn in *; try congruence.
       destruct (execute_action_step _ _ _ _ exec_once) as [step].
       destruct trace as [trace].
-      Hint Constructors ChainTrace : core.
+      Hint Constructors ChainEvent : core.
+      Hint Constructors CursorList.
+      Hint Unfold ChainTrace.
+      destruct df; eapply IH; try eassumption; eauto.
+      (* BF case, where we need to permute *)
       assert (Permutation (new_acts ++ xs) (xs ++ new_acts)) by perm_simplify.
-      destruct df; eauto.
+      cut (ChainTrace
+             empty_state
+             (build_chain_state lc_after (new_acts ++ xs))); eauto.
   Qed.
 End ExecuteActions.
 
@@ -355,15 +362,15 @@ Definition lc_initial : LocalChain :=
 Record LocalChainBuilder :=
   build_local_chain_builder {
     lcb_lc : LocalChain;
-    lcb_trace : inhabited (ChainTrace empty_env [] lcb_lc []);
+    lcb_trace : inhabited (ChainTrace empty_state (build_chain_state lcb_lc []));
   }.
 
 Definition lcb_initial : LocalChainBuilder.
 Proof.
   refine
     {| lcb_lc := lc_initial; lcb_trace := _ |}.
-  Hint Resolve ctrace_refl build_env_equiv build_chain_equiv : core.
-  auto.
+  constructor.
+  apply CursorList.nil.
 Defined.
 
 Definition validate_header (new old : BlockHeader) : option unit :=
@@ -478,14 +485,16 @@ Proof.
   destruct_units.
   destruct lcb as [prev_lc_end prev_lcb_trace].
   refine (Some {| lcb_lc := lc; lcb_trace := _ |}).
-  Hint Resolve
-       validate_header_valid validate_actions_valid
-       execute_steps_trace add_new_block_header_equiv
-       ctrace_block : core.
-  (* auto does not pick up reflexivity for reflexive relations. *)
-  Hint Extern 1 (EnvironmentEquiv _ _) => reflexivity : core.
+  cbn -[execute_steps] in exec.
   destruct prev_lcb_trace as [prev_lcb_trace].
-  eauto 7.
+
+  refine (execute_steps_trace _ _ _ _ _ _ exec).
+  constructor.
+  refine (snoc prev_lcb_trace _).
+  Hint Resolve validate_header_valid validate_actions_valid.
+  eapply evt_block; eauto.
+  apply add_new_block_header_equiv.
+  reflexivity.
 Defined.
 
 Global Instance lcb_chain_builder_type : ChainBuilderType :=