Verificators of inclusion

1 files changed, 286 insertions, 206 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index e55cd461..8adc92f9 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -14,7 +14,7 @@ Local Open Scope option_monad_scope.
 
 (** * TODO: refine symbolic values/symbolic memories with hash-consed symbolic values *)
 
-(** * Implementation of local symbolic internal states *)
+(** * Implementation of local symbolic internal states - definitions and core simulation properties *)
 
 (** name : Hash-consed Symbolic Internal state local. Later on we will use the
     refinement to introduce hash consing *)
@@ -82,15 +82,6 @@ Proof.
   intuition congruence.
 Qed.
 
-(*
-Lemma sok_local_no_abort ge sp rs0 m0 st:
-  sok_local ge sp rs0 m0 st -> sabort_local ge sp st rs0 m0 -> False.
-Proof.
-  unfold sok_local, sabort_local. 
-  intros (H1 & H2 & H3) [A1 | [A2 | (r & A3)]]; intuition eauto.
-Qed.
-*)
-
 Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
      (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None)
   /\ (forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None).
@@ -107,20 +98,14 @@ Proof.
   intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto.
 Qed.
 
+Definition is_subset {A: Type} (lv2 lv1: list A) := forall v, In v lv2 -> In v lv1.
+
 Definition hsilocal_simu_core (hst1 hst2: hsistate_local) :=
-     (forall sm, List.In sm (hsi_lsmem hst2) -> List.In sm (hsi_lsmem hst1))
-  /\ (forall sv, List.In sv (hsi_ok_lsval hst2) -> List.In sv (hsi_ok_lsval hst1))
+     is_subset (hsi_lsmem hst2) (hsi_lsmem hst1)
+  /\ is_subset (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
   /\ (forall r, hsi_sreg_get hst2 r = hsi_sreg_get hst1 r)
   /\ hsi_smem_get hst1 = hsi_smem_get hst2.
 
-Definition hsilocal_simu_coreb (hst1 hst2: hsistate_local) := OK tt.
-
-Theorem hsilocal_simu_coreb_correct hst1 hst2:
-  hsilocal_simu_coreb hst1 hst2 = OK tt ->
-  hsilocal_simu_core hst1 hst2.
-Proof.
-Admitted.
-
 Lemma hsilocal_simu_core_nofail ge1 ge2 sp rs0 m0 hst1 hst2:
   hsilocal_simu_core hst1 hst2 ->
   (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
@@ -204,14 +189,6 @@ Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := fora
   hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
   siexit_simu dm f ctx se1 se2.
 
-(* Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
-  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
-    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
-    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
-    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
-  else Error (msg "siexit_simub: conditions do not match")
-. *)
-
 Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
   hsiexit_simu_core dm f hse1 hse2 ->
   (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
@@ -279,47 +256,6 @@ Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop :=
 Definition hsiexits_simu_core dm f lhse1 lhse2: Prop :=
   list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2.
 
-(* Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
-  match lhse1 with
-  | nil =>
-      match lhse2 with
-      | nil => OK tt
-      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
-      end
-  | hse1 :: lhse1 =>
-      match lhse2 with
-      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
-      | hse2 :: lhse2 =>
-          do _ <- hsiexit_simub dm f hse1 hse2;
-          do _ <- hsiexits_simub dm f lhse1 lhse2;
-          OK tt
-      end
-  end. *)
-
-(* Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
-  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
-  hsiexits_simu dm f ctx lhse1 lhse2.
-Proof.
-(*   induction lhse1.
-  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
-    inv HEREFS1. inv HEREFS2. constructor.
-  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
-    fold hsiexits_simub in EQ1.
-    eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
-    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
-    apply EQ1; assumption. *)
-Admitted.
- *)
-
-(* TODO *)
-Definition hsiexits_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := OK tt.
-
-Theorem hsiexits_simu_coreb_correct dm f lhse1 lhse2:
-  hsiexits_simu_coreb dm f lhse1 lhse2 = OK tt ->
-  hsiexits_simu_core dm f lhse1 lhse2.
-Proof.
-Admitted.
-
 Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx:
   hsiexits_simu_core dm f lhse1 lhse2 ->
   hsiexits_simu dm f ctx lhse1 lhse2.
@@ -343,14 +279,6 @@ Definition hsistate_simu_core dm f (hse1 hse2: hsistate) :=
   /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2)
   /\ hsilocal_simu_core (hsi_local hse1) (hsi_local hse2).
 
-Definition hsistate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate) := OK tt. (* TODO *)
-
-Theorem hsistate_simu_coreb_correct dm f hse1 hse2:
-  hsistate_simu_coreb dm f hse1 hse2 = OK tt ->
-  hsistate_simu_core dm f hse1 hse2.
-Proof.
-Admitted.
-
 Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop :=
   hsi_pc hst = si_pc st
   /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st).
@@ -527,14 +455,6 @@ Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: s
   | _ => hf1 = hf2
   end.
 
-Definition hfinal_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval) := OK tt. (* TODO *)
-
-Theorem hfinal_simu_coreb_correct dm f hf1 hf2:
-  hfinal_simu_coreb dm f hf1 hf2 = OK tt ->
-  hfinal_simu_core dm f hf1 hf2.
-Proof.
-Admitted.
-
 Lemma svident_simu_refl f ctx s:
   svident_simu f ctx s s.
 Proof.
@@ -583,14 +503,6 @@ Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2
      hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
   /\ hfinal_simu_core dm f (hfinal hst1) (hfinal hst2).
 
-Definition hsstate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)
-
-Theorem hsstate_simu_coreb_correct dm f hst1 hst2:
-  hsstate_simu_coreb dm f hst1 hst2 = OK tt ->
-  hsstate_simu_core dm f hst1 hst2.
-Proof.
-Admitted.
-
 Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
   forall st1 st2,
   hsstate_refines hst1 st1 ->
@@ -610,6 +522,285 @@ Proof.
   eapply FSIMU.
 Qed.
 
+(** * Verificators of *_simu_core properties *)
+
+(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
+Fixpoint sval_simub (sv1 sv2: sval) :=
+  match sv1 with
+  | Sinput r =>
+      match sv2 with
+      | Sinput r' => if (Pos.eq_dec r r') then OK tt else Error (msg "sval_simub: Sinput different registers")
+      | _ => Error (msg "sval_simub: Sinput expected")
+      end
+  | Sop op lsv sm =>
+      match sv2 with
+      | Sop op' lsv' sm' =>
+          if (eq_operation op op') then
+            do _ <- list_sval_simub lsv lsv';
+            smem_simub sm sm'
+          else Error (msg "sval_simub: different operations in Sop")
+      | _ => Error (msg "sval_simub: Sop expected")
+      end
+  | Sload sm trap chk addr lsv =>
+      match sv2 with
+      | Sload sm' trap' chk' addr' lsv' =>
+          if (trapping_mode_eq trap trap') then
+            if (chunk_eq chk chk') then
+              if (eq_addressing addr addr') then
+                do _ <- smem_simub sm sm';
+                list_sval_simub lsv lsv'
+              else Error (msg "sval_simub: addressings do not match")
+            else Error (msg "sval_simub: chunks do not match")
+          else Error (msg "sval_simub: trapping modes do not match")
+          (* FIXME - should be refined once we introduce non trapping loads *)
+      | _ => Error (msg "sval_simub: Sload expected")
+      end
+  end
+with list_sval_simub (lsv1 lsv2: list_sval) :=
+  match lsv1 with
+  | Snil =>
+      match lsv2 with
+      | Snil => OK tt
+      | _ => Error (msg "list_sval_simub: lists of different lengths (lsv2 is bigger)")
+      end
+  | Scons sv1 lsv1 =>
+      match lsv2 with
+      | Snil => Error (msg "list_sval_simub: lists of different lengths (lsv1 is bigger)")
+      | Scons sv2 lsv2 =>
+          do _ <- sval_simub sv1 sv2;
+          list_sval_simub lsv1 lsv2
+      end
+  end
+with smem_simub (sm1 sm2: smem) :=
+  match sm1 with
+  | Sinit =>
+      match sm2 with
+      | Sinit => OK tt
+      | _ => Error (msg "smem_simub: Sinit expected")
+      end
+  | Sstore sm chk addr lsv sv =>
+      match sm2 with
+      | Sstore sm' chk' addr' lsv' sv' =>
+          if (chunk_eq chk chk') then
+            if (eq_addressing addr addr') then
+              do _ <- smem_simub sm sm';
+              do _ <- list_sval_simub lsv lsv';
+              sval_simub sv sv'
+            else Error (msg "smem_simub: addressings do not match")
+          else Error (msg "smem_simub: chunks not match")
+      | _ => Error (msg "smem_simub: Sstore expected")
+      end
+  end.
+
+Lemma sval_simub_correct sv1: forall sv2,
+  sval_simub sv1 sv2 = OK tt -> sv1 = sv2.
+Proof.
+  induction sv1 using sval_mut with
+    (P0 := fun lsv1 => forall lsv2, list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2)
+    (P1 := fun sm1 => forall sm2, smem_simub sm1 sm2 = OK tt -> sm1 = sm2); simpl; auto.
+  (* Sinput *)
+  - destruct sv2; try discriminate.
+    destruct (Pos.eq_dec r r0); [congruence|discriminate].
+  (* Sop *)
+  - destruct sv2; try discriminate.
+    destruct (eq_operation _ _); [|discriminate]. subst.
+    intro. explore. apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
+  (* Sload *)
+  - destruct sv2; try discriminate.
+    destruct (trapping_mode_eq _ _); [|discriminate].
+    destruct (chunk_eq _ _); [|discriminate].
+    destruct (eq_addressing _ _); [|discriminate].
+    intro. explore. assert (sm = sm0) by auto. assert (lsv = lsv0) by auto.
+    congruence.
+  (* Snil *)
+  - destruct lsv2; [|discriminate]. congruence.
+  (* Scons *)
+  - destruct lsv2; [discriminate|]. intro. explore.
+    apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
+  (* Sinit *)
+  - destruct sm2; [|discriminate]. congruence.
+  (* Sstore *)
+  - destruct sm2; [discriminate|].
+    destruct (chunk_eq _ _); [|discriminate].
+    destruct (eq_addressing _ _); [|discriminate].
+    intro. explore.
+    assert (sm = sm2) by auto. assert (lsv = lsv0) by auto. assert (sv1 = srce) by auto.
+    congruence.
+Qed.
+
+Lemma list_sval_simub_correct lsv1: forall lsv2,
+  list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2.
+Proof.
+  induction lsv1; simpl; auto.
+  - destruct lsv2; try discriminate. reflexivity.
+  - destruct lsv2; try discriminate. intro. explore.
+    apply sval_simub_correct in EQ. assert (lsv1 = lsv2) by auto.
+    congruence.
+Qed.
+
+Lemma smem_simub_correct sm1: forall sm2,
+  smem_simub sm1 sm2 = OK tt -> sm1 = sm2.
+Proof.
+  induction sm1; simpl; auto.
+  - destruct sm2; try discriminate. reflexivity.
+  - destruct sm2; try discriminate.
+    destruct (chunk_eq _ _); [|discriminate].
+    destruct (eq_addressing _ _); [|discriminate]. intro. explore.
+    apply sval_simub_correct in EQ2. apply list_sval_simub_correct in EQ1.
+    apply IHsm1 in EQ. congruence.
+Qed.
+
+Definition is_structural {A: Type} (cmp: A -> A -> bool) :=
+  forall x y, cmp x y = true -> x = y.
+
+Fixpoint is_part_of {A: Type} (cmp: A -> A -> bool) (elt: A) (lv: list A): bool :=
+  match lv with
+  | nil => false
+  | v::lv => if (cmp elt v) then true else is_part_of cmp elt lv
+  end.
+
+Lemma is_part_of_correct {A: Type} cmp lv (e: A):
+  is_structural cmp ->
+  is_part_of cmp e lv = true ->
+  In e lv.
+Proof.
+  induction lv.
+  - intros. simpl in H0. discriminate.
+  - intros. simpl in H0. destruct (cmp e a) eqn:CMP.
+    + apply H in CMP. subst. constructor; auto.
+    + right. apply IHlv; assumption.
+Qed.
+
+(* Checks if lv2 is a subset of lv1 *)
+Fixpoint is_subsetb {A: Type} (cmp: A -> A -> bool) (lv2 lv1: list A): bool :=
+  match lv2 with
+  | nil => true
+  | v2 :: lv2 => if (is_part_of cmp v2 lv1) then is_subsetb cmp lv2 lv1
+                 else false
+  end.
+
+Lemma is_subset_cons {A: Type} (x: A) lv lx:
+  In x lv /\ is_subset lx lv -> is_subset (x::lx) lv.
+Proof.
+  intros (ISIN & ISSUB). unfold is_subset.
+  intros. inv H.
+  - assumption.
+  - apply ISSUB. assumption.
+Qed.
+
+Lemma is_subset_correct {A: Type} cmp (lv2 lv1: list A):
+  is_structural cmp ->
+  is_subsetb cmp lv2 lv1 = true ->
+  is_subset lv2 lv1.
+Proof.
+  induction lv2.
+  - simpl. intros. intro. intro. apply in_nil in H1. contradiction.
+  - intros. simpl in H0. apply is_subset_cons.
+    explore. apply is_part_of_correct in EQ; [|assumption].
+    apply IHlv2 in H0; [|assumption]. constructor; assumption.
+Qed.
+
+Definition simub_bool {A: Type} (simub: A -> A -> res unit) (sv1 sv2: A) :=
+  match simub sv1 sv2 with
+  | OK tt => true
+  | _ => false
+  end.
+
+Lemma simub_bool_correct {A: Type} simub (sv1 sv2: A):
+  (forall x y, simub x y = OK tt -> x = y) ->
+  simub_bool simub sv1 sv2 = true -> sv1 = sv2.
+Proof.
+  intros. unfold simub_bool in H0. destruct (simub sv1 sv2) eqn:SIMU; explore.
+  - apply H. assumption.
+  - discriminate.
+Qed.
+
+Definition hsilocal_simu_coreb hst1 hst2 :=
+  if (is_subsetb (simub_bool smem_simub) (hsi_lsmem hst2) (hsi_lsmem hst1)) then
+    if (is_subsetb (simub_bool sval_simub) (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)) then
+      (* TODO - compare on the whole ptree *) OK tt
+    else Error (msg "hsi_ok_lsval sets aren't included")
+  else Error (msg "hsi_lsmem sets aren't included").
+
+Theorem hsilocal_simu_coreb_correct hst1 hst2:
+  hsilocal_simu_coreb hst1 hst2 = OK tt ->
+  hsilocal_simu_core hst1 hst2.
+Proof.
+Admitted.
+
+(* Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
+  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
+    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
+    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
+    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
+  else Error (msg "siexit_simub: conditions do not match")
+. *)
+
+(* Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
+  match lhse1 with
+  | nil =>
+      match lhse2 with
+      | nil => OK tt
+      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
+      end
+  | hse1 :: lhse1 =>
+      match lhse2 with
+      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
+      | hse2 :: lhse2 =>
+          do _ <- hsiexit_simub dm f hse1 hse2;
+          do _ <- hsiexits_simub dm f lhse1 lhse2;
+          OK tt
+      end
+  end. *)
+
+(* Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
+  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
+  hsiexits_simu dm f ctx lhse1 lhse2.
+Proof.
+(*   induction lhse1.
+  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
+    inv HEREFS1. inv HEREFS2. constructor.
+  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
+    fold hsiexits_simub in EQ1.
+    eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
+    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
+    apply EQ1; assumption. *)
+Admitted.
+ *)
+
+(* TODO *)
+Definition hsiexits_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := OK tt.
+
+Theorem hsiexits_simu_coreb_correct dm f lhse1 lhse2:
+  hsiexits_simu_coreb dm f lhse1 lhse2 = OK tt ->
+  hsiexits_simu_core dm f lhse1 lhse2.
+Proof.
+Admitted.
+
+Definition hsistate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate) := OK tt. (* TODO *)
+
+Theorem hsistate_simu_coreb_correct dm f hse1 hse2:
+  hsistate_simu_coreb dm f hse1 hse2 = OK tt ->
+  hsistate_simu_core dm f hse1 hse2.
+Proof.
+Admitted.
+
+Definition hsstate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)
+
+Theorem hsstate_simu_coreb_correct dm f hst1 hst2:
+  hsstate_simu_coreb dm f hst1 hst2 = OK tt ->
+  hsstate_simu_core dm f hst1 hst2.
+Proof.
+Admitted.
+
+Definition hfinal_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval) := OK tt. (* TODO *)
+
+Theorem hfinal_simu_coreb_correct dm f hf1 hf2:
+  hfinal_simu_coreb dm f hf1 hf2 = OK tt ->
+  hfinal_simu_core dm f hf1 hf2.
+Proof.
+Admitted.
+
 Lemma hsistate_refines_stat_pceq st hst:
   hsistate_refines_stat hst st ->
   (hsi_pc hst) = (si_pc st).
@@ -624,6 +815,8 @@ Proof.
   unfold hsistate_refines_dyn; intuition.
 Qed.
 
+
+
 Local Hint Resolve hsistate_refines_dyn_local_refines: core.
 
 
@@ -1114,119 +1307,6 @@ Proof.
   unfold revmap_check_single. explore; try discriminate. congruence.
 Qed.
 
-(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
-Fixpoint sval_simub (sv1 sv2: sval) :=
-  match sv1 with
-  | Sinput r =>
-      match sv2 with
-      | Sinput r' => if (Pos.eq_dec r r') then OK tt else Error (msg "sval_simub: Sinput different registers")
-      | _ => Error (msg "sval_simub: Sinput expected")
-      end
-  | Sop op lsv sm =>
-      match sv2 with
-      | Sop op' lsv' sm' =>
-          if (eq_operation op op') then
-            do _ <- list_sval_simub lsv lsv';
-            smem_simub sm sm'
-          else Error (msg "sval_simub: different operations in Sop")
-      | _ => Error (msg "sval_simub: Sop expected")
-      end
-  | Sload sm trap chk addr lsv =>
-      match sv2 with
-      | Sload sm' trap' chk' addr' lsv' =>
-          if (trapping_mode_eq trap trap') then
-            if (chunk_eq chk chk') then
-              if (eq_addressing addr addr') then
-                do _ <- smem_simub sm sm';
-                list_sval_simub lsv lsv'
-              else Error (msg "sval_simub: addressings do not match")
-            else Error (msg "sval_simub: chunks do not match")
-          else Error (msg "sval_simub: trapping modes do not match")
-          (* FIXME - should be refined once we introduce non trapping loads *)
-      | _ => Error (msg "sval_simub: Sload expected")
-      end
-  end
-with list_sval_simub (lsv1 lsv2: list_sval) :=
-  match lsv1 with
-  | Snil =>
-      match lsv2 with
-      | Snil => OK tt
-      | _ => Error (msg "list_sval_simub: lists of different lengths (lsv2 is bigger)")
-      end
-  | Scons sv1 lsv1 =>
-      match lsv2 with
-      | Snil => Error (msg "list_sval_simub: lists of different lengths (lsv1 is bigger)")
-      | Scons sv2 lsv2 =>
-          do _ <- sval_simub sv1 sv2;
-          list_sval_simub lsv1 lsv2
-      end
-  end
-with smem_simub (sm1 sm2: smem) :=
-  match sm1 with
-  | Sinit =>
-      match sm2 with
-      | Sinit => OK tt
-      | _ => Error (msg "smem_simub: Sinit expected")
-      end
-  | Sstore sm chk addr lsv sv =>
-      match sm2 with
-      | Sstore sm' chk' addr' lsv' sv' => 
-          if (chunk_eq chk chk') then
-            if (eq_addressing addr addr') then
-              do _ <- smem_simub sm sm';
-              do _ <- list_sval_simub lsv lsv';
-              sval_simub sv sv'
-            else Error (msg "smem_simub: addressings do not match")
-          else Error (msg "smem_simub: chunks not match")
-      | _ => Error (msg "smem_simub: Sstore expected")
-      end
-  end.
-
-Lemma sval_simub_correct sv1: forall sv2,
-  sval_simub sv1 sv2 = OK tt -> sv1 = sv2.
-Proof.
-  induction sv1 using sval_mut with
-    (P0 := fun lsv1 => forall lsv2, list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2)
-    (P1 := fun sm1 => forall sm2, smem_simub sm1 sm2 = OK tt -> sm1 = sm2); simpl; auto.
-  (* Sinput *)
-  - destruct sv2; try discriminate.
-    destruct (Pos.eq_dec r r0); [congruence|discriminate].
-  (* Sop *)
-  - destruct sv2; try discriminate.
-    destruct (eq_operation _ _); [|discriminate]. subst.
-    intro. explore. apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
-  (* Sload *)
-  - destruct sv2; try discriminate.
-    destruct (trapping_mode_eq _ _); [|discriminate].
-    destruct (chunk_eq _ _); [|discriminate].
-    destruct (eq_addressing _ _); [|discriminate].
-    intro. explore. assert (sm = sm0) by auto. assert (lsv = lsv0) by auto.
-    congruence.
-  (* Snil *)
-  - destruct lsv2; [|discriminate]. congruence.
-  (* Scons *)
-  - destruct lsv2; [discriminate|]. intro. explore.
-    apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
-  (* Sinit *)
-  - destruct sm2; [|discriminate]. congruence.
-  (* Sstore *)
-  - destruct sm2; [discriminate|].
-    destruct (chunk_eq _ _); [|discriminate].
-    destruct (eq_addressing _ _); [|discriminate].
-    intro. explore.
-    assert (sm = sm2) by auto. assert (lsv = lsv0) by auto. assert (sv1 = srce) by auto.
-    congruence.
-Qed.
-
-Lemma list_sval_simub_correct lsv1: forall lsv2,
-  list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2.
-Proof.
-  induction lsv1; simpl; auto.
-  - destruct lsv2; try discriminate. reflexivity.
-  - destruct lsv2; try discriminate. intro. explore.
-    apply sval_simub_correct in EQ. assert (lsv1 = lsv2) by auto.
-    congruence.
-Qed.
 
 Local Hint Resolve genv_match ssem_local_refines_hok: core.