end of merge with Cyril's proof

2 files changed, 227 insertions, 59 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 50bdd7a6..44d14e38 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -92,6 +92,7 @@ Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem :=
     (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
 *)
 
+
 Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
   match sv1, sv2 with
   | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
@@ -112,6 +113,21 @@ Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
   | _,_ => RET false
   end.
 
+
+Lemma and_true_split a b: a && b = true <-> a = true /\ b = true.
+Proof.
+  destruct a; simpl; intuition.
+Qed.
+
+Lemma hsval_hash_eq_correct x y:
+  WHEN hsval_hash_eq x y ~> b THEN 
+   b = true -> hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque hsval_hash_eq.
+Local Hint Resolve hsval_hash_eq_correct: wlp.
+
 Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool :=
   match lsv1, lsv2 with
   | HSnil _, HSnil _ => RET true
@@ -123,6 +139,15 @@ Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool :=
   | _,_ => RET false
   end.
 
+Lemma list_hsval_hash_eq_correct x y:
+  WHEN list_hsval_hash_eq x y ~> b THEN 
+   b = true -> list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque list_hsval_hash_eq.
+Local Hint Resolve list_hsval_hash_eq_correct: wlp.
+
 Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
   match sm1, sm2 with
   | HSinit _, HSinit _ => RET true
@@ -137,6 +162,16 @@ Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
   | _,_ => RET false
   end.
 
+Lemma hsmem_hash_eq_correct x y:
+  WHEN hsmem_hash_eq x y ~> b THEN 
+   b = true -> hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque hsmem_hash_eq.
+Local Hint Resolve hsmem_hash_eq_correct: wlp.
+
+
 Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
 Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}.
 Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.
@@ -228,6 +263,32 @@ Local Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval g
 Local Notation "'smem_refines' ge sp rs0 m0 hm sm" := (seval_hsmem ge sp hm rs0 m0 = seval_smem ge sp sm rs0 m0)
   (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hm at next level, sm at next level).
 
+Lemma hsval_set_hid_correct x y ge sp rs0 m0:
+  hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid ->
+  seval_hsval ge sp x rs0 m0 = seval_hsval ge sp y rs0 m0.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve hsval_set_hid_correct: core.
+
+Lemma list_hsval_set_hid_correct x y ge sp rs0 m0:
+  list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid ->
+  seval_list_hsval ge sp x rs0 m0 = seval_list_hsval ge sp y rs0 m0.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve list_hsval_set_hid_correct: core.
+
+Lemma hsmem_set_hid_correct x y ge sp rs0 m0:
+  hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid ->
+  seval_hsmem ge sp x rs0 m0 = seval_hsmem ge sp y rs0 m0.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve hsmem_set_hid_correct: core.
+
+
+
 Definition hsi_sreg_proj (hst: PTree.t hsval) r: sval :=
    match PTree.get r hst with
    | None => Sinput r
@@ -1198,14 +1259,40 @@ Definition hsexec (f: function) (pc:node): ?? hsstate :=
             RET {| hinternal := hst; hfinal := hsvf |}
   end.
 
-Lemma hsexec_correct f pc:
+Lemma hsexec_correct_aux f pc:
   WHEN hsexec f pc ~> hst THEN
   exists st, sexec f pc = Some st /\ hsstate_refines hst st.
 Admitted.
-Global Opaque hsexec_correct.
+Global Opaque hsexec.
 
 End CanonBuilding.
 
+(** Correction of concrete symbolic execution wrt abstract symbolic execution *)
+Theorem hsexec_correct
+  (hC_hsval : hashinfo hsval -> ?? hsval)
+  (hC_list_hsval : hashinfo list_hsval -> ?? list_hsval)
+  (hC_hsmem : hashinfo hsmem -> ?? hsmem)
+  (f : function) 
+  (pc : node):
+       WHEN hsexec hC_hsval hC_list_hsval hC_hsmem f pc ~> hst THEN forall
+        (hC_hsval_correct: forall hs,
+            WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0,
+                seval_sval ge sp (hsval_proj (hdata hs)) rs0 m0 =
+                seval_sval ge sp (hsval_proj hs') rs0 m0)
+        (hC_list_hsval_correct: forall lh,
+            WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0,
+              seval_list_sval ge sp (hsval_list_proj (hdata lh)) rs0 m0 =
+              seval_list_sval ge sp (hsval_list_proj lh') rs0 m0)
+         (hC_hsmem_correct: forall hm,
+            WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0,
+              seval_smem ge sp (hsmem_proj (hdata hm)) rs0 m0 =
+              seval_smem ge sp (hsmem_proj hm') rs0 m0),
+         exists st : sstate, sexec f pc = Some st /\ hsstate_refines hst st.
+Proof.
+  wlp_simplify.
+  eapply hsexec_correct_aux; eauto.
+Qed.
+
 Local Hint Resolve hsexec_correct: wlp.
 
 (** * Intermediate specifications of the simulation test *)
@@ -1592,7 +1679,7 @@ Qed.
 
 
 (** ** Specification of the simulation test on [sfval].
-       It is motivated by [hsistate_simu_core_correct theorem] below
+       It is motivated by [hfinal_simu_core_correct theorem] below
 *)
 
 
@@ -1643,60 +1730,34 @@ Lemma list_proj_refines_eq ge ge' sp rs0 m0 lsv lhsv:
   hsval_list_proj lhsv = hsval_list_proj lhsv' ->
   seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
 Proof.
-  intros GFS H lhsv' lsv' H0 H1.
-  erewrite <- H, H1.
+  intros GFS H lhsv' lsv' H' H0.
+  erewrite <- H, H0.
   erewrite list_sval_eval_preserved; eauto.
 Qed.
 
-(*
-Lemma barg_proj_refines_eq_single ge ge' sp rs0 m0:
+Lemma barg_proj_refines_eq ge ge' sp rs0 m0:
   (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
-  forall hsv sv, barg_refines ge sp rs0 m0 hsv sv ->
-  forall hsv' sv', barg_refines ge' sp rs0 m0 hsv' sv' ->
-  builtin_arg_map hsval_proj hsv = builtin_arg_map hsval_proj hsv' ->
-  seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0.
+  forall lhsv lsv, bargs_refines ge sp rs0 m0 lhsv lsv ->
+  forall lhsv' lsv', bargs_refines ge' sp rs0 m0 lhsv' lsv' ->
+  List.map (builtin_arg_map hsval_proj) lhsv = List.map (builtin_arg_map hsval_proj) lhsv' ->
+  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
 Proof.
-  intro GFS hsv sv H hsv' sv' H' H0.
-  
-  all: try (simpl; intros hsv' sv' BREF' BPROJ';
-    destruct hsv'; simpl in BPROJ'; try discriminate;
-    inv BPROJ'; inv BREF'; simpl; try reflexivity;
-    erewrite sval_refines_proj; eauto).
-(* BA_splitlong *)
-  - simpl. intros hsv' sv' BREF' BPROJ'.
-    destruct hsv'; simpl in BPROJ'; try discriminate.
-    inv BPROJ'. inv BREF'. simpl.
-    erewrite IHbarg_refines2; eauto.
-    erewrite IHbarg_refines1. 2: eapply H5.
-    all: eauto.
-(* BA_addptr *)
-  - simpl. intros hsv' sv' BREF' BPROJ'.
-    destruct hsv'; simpl in BPROJ'; try discriminate.
-    inv BPROJ'. inv BREF'. simpl.
-    erewrite IHbarg_refines2; eauto.
-    erewrite IHbarg_refines1. 2: eapply H5.
-    all: eauto.
-Qed.
-
-Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
+  unfold bargs_refines; intros GFS lhsv lsv H lhsv' lsv' H' H0.
+  erewrite <- H, H0.
+Admitted.
+
+Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv':
   (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
-  list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv ->
-  forall lhsv' lsv',
-  list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' ->
-  barg_list_proj lhsv = barg_list_proj lhsv' ->
-  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
+  sval_refines ge sp rs m hsv sv ->
+  sval_refines ge' sp rs m hsv' sv' ->
+  hsval_proj hsv = hsval_proj hsv' ->
+  seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m.
 Proof.
-  induction 2; rename H into GFS.
-  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
-    inv H. simpl. reflexivity.
-  - simpl. intros. destruct lhsv'; try discriminate.
-    simpl in H2. inv H2. destruct lsv'; [inv H|].
-    inv H. simpl.
-    erewrite barg_proj_refines_eq_single; eauto.
-    erewrite IHlist_forall2; eauto.
+  intros GFS REF REF' PROJ.
+  rewrite <- REF, PROJ.
+  erewrite <- seval_preserved; eauto.
 Qed.
 
-
 Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
   hfinal_simu_core dm f opc1 opc2 hf1 hf2 ->
   hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 ->
@@ -1762,8 +1823,35 @@ Proof.
       constructor.
     + destruct res0; try discriminate. destruct osv0; inv H1. constructor.
 Qed.
+
+
+(** ** Specification of the simulation test on [hsstate].
+       It is motivated by [hsstate_simu_core_correct theorem] below
 *)
 
+Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
+     hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
+  /\ hfinal_simu_core dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2).
+
+Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
+  forall st1 st2,
+  hsstate_refines hst1 st1 ->
+  hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.
+
+Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
+  hsstate_simu_core dm f hst1 hst2 ->
+  hsstate_simu dm f hst1 hst2 ctx.
+Proof.
+  intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2.
+  destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2).
+  assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE.
+  eapply hsistate_simu_core_correct in SCORE.
+  eapply hfinal_simu_core_correct in FSIMU; eauto.
+  constructor; [apply SCORE; auto|]. 1-2: eassumption.
+  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
+  eapply FSIMU.
+Qed.
+
 (** * Implementing the simulation test with concrete hash-consed symbolic execution *)
 
 Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
@@ -1959,6 +2047,18 @@ Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   | _, _ => FAILWITH "revmap_check_list: lists have different lengths"
   end.
 
+Lemma revmap_check_list_correct dm: forall lpc lpc',
+  WHEN revmap_check_list dm lpc lpc' ~> _ THEN
+  ptree_get_list dm lpc' = Some lpc.
+Proof.
+  induction lpc.
+  - destruct lpc'; wlp_simplify.
+  - destruct lpc'; wlp_simplify. try_simplify_someHyps.
+Qed.
+Global Opaque revmap_check_list.
+Hint Resolve revmap_check_list_correct: wlp.
+
+
 Definition svos_simu_check (svos1 svos2: hsval + ident) :=
   match svos1, svos2 with
   | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
@@ -1966,18 +2066,51 @@ Definition svos_simu_check (svos1 svos2: hsval + ident) :=
   | _, _ => FAILWITH "svos_simu_check: type mismatch"
   end.
 
+Lemma svos_simu_check_correct svos1 svos2:
+  WHEN svos_simu_check svos1 svos2 ~> _ THEN
+  svos1 = svos2.
+Proof.
+  destruct svos1; destruct svos2; wlp_simplify.
+Qed.
+Global Opaque svos_simu_check.
+Hint Resolve svos_simu_check_correct: wlp.
+
+
 Fixpoint builtin_arg_simu_check (bs bs': builtin_arg hsval) :=
-  match bs, bs' with
-  | BA sv, BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
-  | BA_splitlong lo hi, BA_splitlong lo' hi' => 
-      builtin_arg_simu_check lo lo';;
-      builtin_arg_simu_check hi hi'
-  | BA_addptr b1 b2, BA_addptr b1' b2' => 
-      builtin_arg_simu_check b1 b1';;
-      builtin_arg_simu_check b2 b2'
-  | _, _ => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
+  match bs with
+  | BA sv =>
+    match bs' with
+    | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
+    | _ => FAILWITH "builtin_arg_simu_check: BA mismatch"
+    end
+  | BA_splitlong lo hi =>
+    match bs' with
+    | BA_splitlong lo' hi' =>
+        builtin_arg_simu_check lo lo';;
+        builtin_arg_simu_check hi hi'
+    | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch"
+    end
+  | BA_addptr b1 b2 =>
+    match bs' with
+    | BA_addptr b1' b2' =>
+        builtin_arg_simu_check b1 b1';;
+        builtin_arg_simu_check b2 b2'
+    | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch"
+    end
+  | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
   end.
 
+Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
+  WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN
+  builtin_arg_map hsval_proj bs1 = builtin_arg_map hsval_proj bs2.
+Proof.
+  induction bs1.
+  all: try (wlp_simplify; subst; reflexivity).
+  all: destruct bs2; wlp_simplify; congruence.
+Qed.
+Global Opaque builtin_arg_simu_check.
+Hint Resolve builtin_arg_simu_check_correct: wlp.
+
 Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
   match lbs1, lbs2 with
   | nil, nil => RET tt
@@ -1987,6 +2120,15 @@ Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
   | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
   end.
 
+Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2,
+  WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> _ THEN
+  List.map (builtin_arg_map hsval_proj) lbs1 = List.map (builtin_arg_map hsval_proj) lbs2.
+Proof.
+  induction lbs1; destruct lbs2; wlp_simplify. congruence.
+Qed.
+Global Opaque list_builtin_arg_simu_check.
+Hint Resolve list_builtin_arg_simu_check_correct: wlp.
+
 Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) :=
   match fv1, fv2 with
   | HSnone, HSnone => revmap_check_single dm pc1 pc2
@@ -2013,10 +2155,28 @@ Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: n
   | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
   end.
 
+Lemma sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
+  WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> _ THEN
+  hfinal_simu_core dm f opc1 opc2 fv1 fv2.
+Proof.
+  unfold hfinal_simu_core; destruct fv1; destruct fv2; wlp_simplify; try congruence.
+Qed.
+Hint Resolve sfval_simu_check_correct: wlp.
+Global Opaque sfval_simu_check.
+
 Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
   hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
   sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
+Lemma hsstate_simu_check_correct dm f hst1 hst2:
+  WHEN hsstate_simu_check dm f hst1 hst2 ~> _ THEN
+  hsstate_simu_core dm f hst1 hst2.
+Proof.
+  unfold hsstate_simu_core; wlp_simplify.
+Qed.
+Hint Resolve hsstate_simu_check_correct: wlp.
+Global Opaque hsstate_simu_check. 
+
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
   let (pc2, pc1) := m in
   (* creating the hash-consing tables *)
@@ -2035,6 +2195,12 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
 Lemma simu_check_single_correct dm tf f pc1 pc2:
   WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
   sexec_simu dm f tf pc1 pc2.
+Proof.
+  unfold sexec_simu; wlp_simplify.
+  exploit H2; clear H2. 1-3: wlp_simplify.
+  intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
+  exploit H3; clear H3. 1-3: wlp_simplify.
+  
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index dcdc54b5..3573ddbb 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -1716,7 +1716,8 @@ Proof.
       constructor; eauto. congruence.
 Qed.
 
-Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with
+Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
+  match bsv with
   | BA sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Some (BA v)
   | BA_splitlong sv1 sv2 =>
       SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
@@ -1736,7 +1737,8 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with
   | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
   end.
 
-Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := match lbsv with
+Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 :=
+  match lbsv with
   | nil => Some nil
   | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN
                  SOME lv <- seval_list_builtin_sval ge sp lbsv rs0 m0 IN