exec_final_correct proved

1 files changed, 122 insertions, 22 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 1831b3fc..ac3fbf27 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1,8 +1,4 @@
-(** Implementation and refinement of the symbolic execution
-
-* a JUNK VERSION WITHOUT ANY FORMAL PROOF !!!
-
- *)
+(** Implementation and refinement of the symbolic execution *)
 
 Require Import Coqlib Maps Floats.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
@@ -219,18 +215,21 @@ Variable hC_hsval: hashinfo hsval -> ?? hsval.
 Hypothesis hC_hsval_correct: forall hs rhsv,
   hC_hsval hs ~~> rhsv ->
   (hsval_proj (hdata hs)) = (hsval_proj rhsv).
+Local Hint Resolve hC_hsval_correct: wlp.
 
 Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval.
 
 Hypothesis hC_hlist_sval_correct: forall hs rhsv,
   hC_hlist_sval hs ~~> rhsv ->
   (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv).
+Local Hint Resolve hC_hlist_sval_correct: wlp.
 
 Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
 
 Hypothesis hC_hsmem_correct: forall hs rhsv,
   hC_hsmem hs ~~> rhsv ->
   (hsmem_proj (hdata hs)) = (hsmem_proj rhsv).
+Local Hint Resolve hC_hsmem_correct: wlp.
 
 (* First, we wrap constructors for hashed values !*)
 
@@ -1523,6 +1522,112 @@ Proof.
   rewrite sval_refines_local_get; eauto.
 Qed.
 
+Lemma hSnil_correct:
+  WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil.
+Proof.
+  wlp_simplify. unfold hSnil in Hexta. apply hC_hlist_sval_correct in Hexta.
+  simpl in *. symmetry. assumption.
+Qed.
+Global Opaque hSnil.
+Hint Resolve hSnil_correct: wlp.
+
+Lemma hScons_correct: forall lhsv hsv,
+  WHEN hScons hsv lhsv ~> lhsv' THEN
+  hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv).
+Proof.
+  destruct lhsv; wlp_simplify.
+  - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta.
+    simpl in *. congruence.
+  - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta. simpl in *. congruence.
+Qed.
+Global Opaque hScons.
+Hint Resolve hScons_correct: wlp.
+
+Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  WHEN hsi_sreg_get hsl r ~> hsv THEN
+  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
+Proof.
+  intros HOK HREF. wlp_intros hsv HGET. destruct HREF as (_ & _ & A & _).
+  unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption.
+  rewrite A by assumption. reflexivity.
+Qed.
+
+Lemma hsval_list_proj_correct ge sp rs m lsv: forall lhsv,
+  list_refines ge sp rs m lhsv lsv ->
+  forall lhsv', hsval_list_proj lhsv' = hsval_list_proj lhsv ->
+  list_refines ge sp rs m lhsv' lsv.
+Proof.
+  induction 1.
+  - intro. simpl. intros. destruct lhsv'; try discriminate. constructor.
+  - intros. simpl in H1. destruct lhsv'; try discriminate.
+    simpl in H1. inv H1. apply IHlist_refines in H4.
+    constructor; [assumption|].
+    unfold sval_refines. unfold seval_hsval. rewrite H3. assumption.
+Qed.
+Hint Resolve hsval_list_proj_correct: wlp.
+
+Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  WHEN hsi_sreg_get hsl r ~> hsv' THEN
+  hsval_proj hsv = hsval_proj hsv' ->
+  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
+Proof.
+  intros HOK HREF. wlp_intros hsv' HGET. intros PROJ.
+  unfold sval_refines. unfold seval_hsval.
+  rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity].
+  erewrite hsi_sreg_get_refines; eauto.
+Qed.
+Global Opaque hsval_proj.
+Hint Resolve hsval_proj_correct: wlp.
+
+Lemma hlist_args_correct ge sp rs0 m0 hsl sl:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  forall lr, WHEN hlist_args hsl lr ~> shv THEN
+  list_refines ge sp rs0 m0 shv (list_sval_inj (List.map (si_sreg sl) lr)).
+Proof.
+  intros HOK HREF. induction lr.
+  - simpl. wlp_simplify. destruct exta; try discriminate. constructor.
+  - simpl. wlp_step_bind v V. wlp_step_bind hlsv HLSV. wlp_simplify.
+    apply IHlr in HLSV. clear IHlr.
+    destruct exta; try discriminate. simpl in H. inv H. constructor.
+    + eapply hsval_list_proj_correct; eauto.
+    + eapply hsval_proj_correct; eauto.
+Qed.
+Global Opaque hsval_list_proj.
+Global Opaque hlist_args.
+Hint Resolve hlist_args_correct: wlp.
+
+Lemma hbuiltin_arg_correct ge sp rs0 m0 hsl sl:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  forall br,
+  WHEN hbuiltin_arg hsl br ~> bhsv THEN
+  barg_refines ge sp rs0 m0 bhsv (builtin_arg_map (si_sreg sl) br).
+Proof.
+  intros HOK HREF.
+  induction br.
+  all: try (wlp_simplify; constructor; auto; fail).
+  (* BA *)
+  - simpl. wlp_step_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
+Qed.
+
+Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  forall lbr,
+  WHEN hbuiltin_args hsl lbr ~> lbhsv THEN
+  list_forall2 (barg_refines ge sp rs0 m0) lbhsv (List.map (builtin_arg_map (si_sreg sl)) lbr).
+Proof.
+  intros HOK HREF.
+  induction lbr; [wlp_simplify; constructor|].
+  simpl. wlp_step_bind ha HA. wlp_step_bind hl HL. wlp_simplify.
+  constructor; [|auto]. eapply hbuiltin_arg_correct; eauto.
+Qed.
+
 Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
   hsok_local ge sp rs0 m0 hsl ->
   hsilocal_refines ge sp rs0 m0 hsl sl ->
@@ -1532,28 +1637,23 @@ Proof.
   intro HOK.
   destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
   (* Scall *)
-  - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_intros hsf HSF.
-    apply mayRet_ret in HSF. subst. constructor.
+  - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor.
     + eapply hsum_left_correct; eauto.
-    + Search list_refines. admit.
-    
-(* 
-    + intro. inv H. constructor; auto.
-      ++ erewrite <- sfind_function_conserves; eauto.
-      ++ erewrite <- seval_list_sval_refines; eauto.
-    + intro. inv H. constructor; auto.
-      ++ erewrite sfind_function_conserves; eauto.
-      ++ erewrite seval_list_sval_refines; eauto.
+    + eapply hlist_args_correct; eauto.
   (* Stailcall *)
-  - admit.
+  - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor.
+    + eapply hsum_left_correct; eauto.
+    + eapply hlist_args_correct; eauto.
   (* Sbuiltin *)
-  - admit.
+  - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto.
   (* Sjumptable *)
-  - admit.
+  - wlp_step_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
   (* Sreturn *)
-  - admit.
- *)Admitted.
-
+  - destruct o.
+    -- wlp_step_bind sv HGET. wlp_simplify. constructor. simpl.
+       eapply hsi_sreg_get_refines; eauto.
+    -- wlp_simplify. repeat constructor.
+Qed.
 
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with