progress on hsexec_inst_correct_dyn

1 files changed, 140 insertions, 39 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index dce66a5f..04e8d559 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -372,6 +372,27 @@ Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop
   /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st)
   /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
 
+Lemma hsistate_refines_dyn_exits ge sp rs0 m0 hst st:
+  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st).
+Proof.
+  unfold hsistate_refines_dyn; intuition.
+Qed.
+Local Hint Resolve hsistate_refines_dyn_exits: core.
+
+Lemma hsistate_refines_dyn_local ge sp rs0 m0 hst st:
+  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
+Proof.
+  unfold hsistate_refines_dyn; intuition.
+Qed.
+Local Hint Resolve hsistate_refines_dyn_local: core.
+
+Lemma hsistate_refines_dyn_nested ge sp rs0 m0 hst st:
+  hsistate_refines_dyn ge sp rs0 m0 hst st -> nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
+Proof.
+  unfold hsistate_refines_dyn; intuition.
+Qed.
+Local Hint Resolve hsistate_refines_dyn_nested: core.
+
 
 (** * Implementation of symbolic execution *)
 Section CanonBuilding.
@@ -428,13 +449,13 @@ Definition hSop (op:operation) (lhsv: list_hsval)  (hsm: hsmem): ?? hsval :=
    hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}.
 
 Lemma hSop_correct op lhsv hsm:
-  WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm,
-    list_sval_refines ge sp rs0 m0 lhsv lsv ->
-    smem_refines ge sp rs0 m0 hsm sm ->
+  WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm
+    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
+    (MR: smem_refines ge sp rs0 m0 hsm sm),
     sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
 Proof.
   wlp_simplify.
-  rewrite <- H0, <- H1.
+  rewrite <- LR, <- MR.
   auto.
 Qed.
 Global Opaque hSop.
@@ -453,13 +474,13 @@ Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr
    hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}.
 
 Lemma hSload_correct hsm trap chunk addr lhsv:
-  WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm,
-    list_sval_refines ge sp rs0 m0 lhsv lsv ->
-    smem_refines ge sp rs0 m0 hsm sm ->
+  WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm
+    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
+    (MR: smem_refines ge sp rs0 m0 hsm sm),
     sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv).
 Proof.
   wlp_simplify.
-  rewrite <- H0, <- H1.
+  rewrite <- LR, <- MR.
   auto.
 Qed.
 Global Opaque hSload.
@@ -481,13 +502,13 @@ Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval :=
    hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}.
 
 Lemma hScons_correct hsv lhsv:
-  WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv,
-    sval_refines ge sp rs0 m0 hsv sv ->
-    list_sval_refines ge sp rs0 m0 lhsv lsv ->
+  WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv
+    (VR: sval_refines ge sp rs0 m0 hsv sv)
+    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
     list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv).
 Proof.
   wlp_simplify.
-  rewrite <- H0, <- H1.
+  rewrite <- VR, <- LR.
   auto.
 Qed.
 Global Opaque hScons.
@@ -516,14 +537,14 @@ Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv:
    hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}.
 
 Lemma hSstore_correct hsm chunk addr lhsv hsv:
-  WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv,
-    list_sval_refines ge sp rs0 m0 lhsv lsv ->
-    smem_refines ge sp rs0 m0 hsm sm ->
-    sval_refines ge sp rs0 m0 hsv sv ->
+  WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv
+    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
+    (MR: smem_refines ge sp rs0 m0 hsm sm)
+    (VR: sval_refines ge sp rs0 m0 hsv sv),
     smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv).
 Proof.
   wlp_simplify.
-  rewrite <- H0, <- H1, <- H2.
+  rewrite <- LR, <- MR, <- VR.
   auto.
 Qed.
 Global Opaque hSstore.
@@ -536,13 +557,11 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    end.
 
 Lemma hsi_sreg_get_correct hst r:
-  WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval),
-    (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) ->
+  WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval)
+    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
     sval_refines ge sp rs0 m0 hsv (f r).
 Proof.
-  unfold hsi_sreg_eval; wlp_simplify.
-  + rewrite <- H0, H. auto.
-  + rewrite <- H1, H. auto.
+  unfold hsi_sreg_eval; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
 Qed.
 Global Opaque hsi_sreg_get.
 Local Hint Resolve hsi_sreg_get_correct: wlp.
@@ -556,10 +575,9 @@ Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
     hScons v lhsv
   end.
 
-
 Lemma hlist_args_correct hst l:
-  WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval),
-    (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) ->
+  WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval)
+    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
     list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)).
 Proof.
   induction l; wlp_simplify.
@@ -625,8 +643,8 @@ Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_
    RET (hslocal_set_smem hst hm).
 
 Lemma hslocal_store_correct hst chunk addr args src:
-  WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st,
-    hsilocal_refines ge sp rs0 m0 hst st ->
+  WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st
+    (REF: hsilocal_refines ge sp rs0 m0 hst st),
     hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src).
 Proof.
   wlp_simplify.
@@ -688,15 +706,15 @@ Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval :=
   .
 
 Lemma hSop_hSinit_correct op lhsv:
-  WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m,
-   seval_smem ge sp sm rs0 m0 = Some m -> 
-   (forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
-   list_sval_refines ge sp rs0 m0 lhsv lsv ->
+  WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m
+   (MEM: seval_smem ge sp sm rs0 m0 = Some m)
+   (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+   (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
    sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
 Proof.
   wlp_simplify.
   erewrite H0; [ idtac | eauto | eauto ].
-  rewrite H, H1.
+  rewrite H, MEM.
   destruct (seval_list_sval _ _ lsv _); try congruence.
   eapply op_valid_pointer_eq; eauto.
 Qed.
@@ -711,9 +729,9 @@ Definition root_happly (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?
   end.
 
 Lemma root_happly_correct (rsv: root_sval) lr hst:
-  WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st,
-    hsilocal_refines ge sp rs0 m0 hst st ->
-    hsok_local ge sp rs0 m0 hst -> 
+  WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st
+    (REF:hsilocal_refines ge sp rs0 m0 hst st)
+    (OK:hsok_local ge sp rs0 m0 hst),
     sval_refines ge sp rs0 m0 hv' (rsv lr st).
 Proof.
    unfold hsilocal_refines, root_apply, root_happly; destruct rsv; wlp_simplify.
@@ -785,10 +803,10 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
   end.
 
 Lemma simplify_correct rsv lr hst:
-  WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st,
-    hsilocal_refines ge sp rs0 m0 hst st ->
-    hsok_local ge sp rs0 m0 hst ->
-    seval_sval ge sp (rsv lr st) rs0 m0 <> None ->
+  WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st
+    (REF: hsilocal_refines ge sp rs0 m0 hst st)
+    (OK0: hsok_local ge sp rs0 m0 hst)
+    (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None),
     sval_refines ge sp rs0 m0 hv (rsv lr st).
 Proof.
   destruct rsv; simpl; auto.
@@ -835,6 +853,23 @@ Proof.
   - rewrite PTree.gro, PTree.gso; simpl; auto.
 Qed.
 
+(* TODO: a revoir --- simplifier! 
+Lemma sok_local_set_sreg ge sp rs0 m0 st r (rsv:root_sval) lr sv':
+ (sok_local ge sp rs0 m0 st -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lr st) rs0 m0) ->
+  sok_local ge sp rs0 m0 (slocal_set_sreg st r sv')
+  <-> (sok_local ge sp rs0 m0 st /\ seval_sval ge sp sv' rs0 m0 <> None).
+Proof.
+  unfold slocal_set_sreg, sok_local; simpl; intro SV'; split.
+  + intros ((SVAL0 & PRE) & SMEM & SVAL).
+    repeat (split; try tauto).
+    - intros r0; generalize (SVAL r0); clear SVAL; destruct (Pos.eq_dec r r0); try congruence.
+    - generalize (SVAL r); clear SVAL; destruct (Pos.eq_dec r r); try congruence.
+  + intros ((PRE & SMEM & SVAL0) & SVAL).
+    repeat (split; try tauto; eauto).
+    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+Qed.
+*)
+
 Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
   DO ok_lhsv <~
    (if may_trap rsv lr
@@ -847,6 +882,25 @@ Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr:
          hsi_ok_lsval := ok_lhsv;
          hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.
 
+
+Lemma hslocal_set_sreg_correct hst r rsv lr:
+  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st
+    (REF: hsilocal_refines ge sp rs0 m0 hst st),
+    hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)).
+Proof.
+  wlp_simplify.
+  + assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
+               hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := exta :: hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta0 hst |}).
+   { admit . }
+   unfold hsilocal_refines; split; auto.
+   
+   
+Admitted.
+Global Opaque hslocal_set_sreg.
+Local Hint Resolve hslocal_set_sreg_correct: wlp.
+
+
+
 (** ** Execution of one instruction *)
 
 Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := 
@@ -870,6 +924,53 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
   | _ => RET None (* TODO jumptable ? *)
   end.
 
+Lemma seval_condition_refines hst st ge sp cond hargs args rs m:
+  hsok_local ge sp rs m hst -> 
+  hsilocal_refines ge sp rs m hst st ->
+  list_sval_refines ge sp rs m hargs args ->
+  hseval_condition ge sp cond hargs (hsi_smem hst) rs m
+  = seval_condition ge sp cond args (si_smem st) rs m.
+ Proof.
+  intros HOK (_ & MEMEQ & _) LR. unfold hseval_condition, seval_condition.
+  rewrite LR, <- MEMEQ; auto.
+Qed.
+
+Lemma hsiexec_inst_correct_dyn i hst:
+  WHEN hsiexec_inst i hst ~> o THEN forall ge sp rs0 m0 st hst' st'
+    (EQo: o = Some hst')
+    (SIEXEC: siexec_inst i st = Some st')
+    (REF: hsistate_refines_dyn ge sp rs0 m0 hst st),
+    hsistate_refines_dyn ge sp rs0 m0 hst' st'.
+Proof.
+  destruct i; simpl; wlp_simplify; try_simplify_someHyps.
+  - (* Iop *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    unfold sok_local; simpl; intros (PRE & MEM & REG).
+    intuition.
+    generalize (REG r0); clear REG.
+    destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
+  - (* Iload *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    unfold sok_local; simpl; intros (PRE & MEM & REG).
+    intuition.
+    generalize (REG r0); clear REG.
+    destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
+  - (* Istore *)
+    eapply hsist_set_local_correct_dyn; eauto.
+    unfold sok_local; simpl; intuition.
+  - (* Icond *)
+    destruct REF as (EXREF & LREF & NEST).
+    split.
+    + constructor; simpl; auto.
+      constructor; simpl; auto.
+      intros; erewrite seval_condition_refines; eauto.
+    + split; simpl; auto.
+      destruct NEST as [|st0 se lse TOP NEST];
+      econstructor; simpl; auto; constructor; auto.
+Qed.
+Global Opaque hsiexec_inst.
+Local Hint Resolve hsiexec_inst_correct_dyn: wlp.
+
 Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
   match o with
   | Some x => RET x