hfinal_refines depend on ge, sp, rs0, m0

1 files changed, 81 insertions, 17 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 5009a91b..c2baa880 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1168,12 +1168,75 @@ Definition hfinal_proj hfv := match hfv with
   | HSreturn oh => Sreturn (option_hsval_proj oh)
   end.
 
-Definition hfinal_refines (hfv: hsfval) (fv: sfval) := (hfinal_proj hfv) = fv.
+Section HFINAL_REFINES.
+
+Variable ge: RTL.genv.
+Variable sp: val.
+Variable rs0: regset.
+Variable m0: mem.
+
+Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0.
+
+Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
+  match hsi, si with
+  | inl hv, inl sv => sval_refines hv sv
+  | inr id, inr id' => id = id'
+  | _, _ => False
+  end.
+
+Inductive list_refines: hlist_sval -> list_sval -> Prop :=
+  | hsnil_ref: forall h, list_refines (HSnil h) Snil
+  | hscons_ref: forall lhv lsv hv sv h,
+      list_refines lhv lsv ->
+      sval_refines hv sv ->
+      list_refines (HScons hv lhv h) (Scons sv lsv).
+
+Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop :=
+  | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv)
+  | hba_splitlong: forall bha1 bha2 ba1 ba2,
+      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
+      barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2)
+  | hba_addptr: forall bha1 bha2 ba1 ba2,
+      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
+      barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2)
+  | hba_int: forall i, barg_refines (BA_int i) (BA_int i)
+  | hba_long: forall l, barg_refines (BA_long l) (BA_long l)
+  | hba_float: forall f, barg_refines (BA_float f) (BA_float f)
+  | hba_single: forall s, barg_refines (BA_single s) (BA_single s)
+  | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr)
+  | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr)
+  | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr)
+  | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr).
+
+Definition option_refines ohsv osv :=
+  match ohsv, osv with
+  | Some hsv, Some sv => sval_refines hsv sv
+  | None, None => True
+  | _, _ => False
+  end.
+
+Inductive hfinal_refines: hsfval -> sfval -> Prop :=
+  | hsnone_ref: hfinal_refines HSnone Snone
+  | hscall_ref: forall hros ros hargs args s r pc,
+      sum_refines hros ros ->
+      list_refines hargs args ->
+      hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc)
+  | hstailcall_ref: forall hros ros hargs args s,
+      sum_refines hros ros ->
+      list_refines hargs args ->
+      hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args)
+  | hsbuiltin_ref: forall ef lbha lba br pc,
+      list_forall2 barg_refines lbha lba ->
+      hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc)
+  | hsjumptable_ref: forall hsv sv lpc,
+      sval_refines hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc)
+  | hsreturn_ref: forall ohsv osv,
+      option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv).
 
 Remark hfinal_refines_snone: hfinal_refines HSnone Snone.
-Proof.
-  reflexivity.
-Qed.
+Proof. constructor. Qed.
+
+End HFINAL_REFINES.
 
 Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop :=
   match f1 with
@@ -1216,12 +1279,13 @@ 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 hf1 f1 ->
-  hfinal_refines hf2 f2 ->
+  hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 ->
+  hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 ->
   sfval_simu dm f opc1 opc2 ctx f1 f2.
 Proof.
   intros CORE FREF1 FREF2.
-  rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *)
+Admitted. (* TODO - prove it *)
+(*   rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *)
   destruct hf1.
   (* Snone *)
   - destruct hf2; try contradiction. simpl. inv CORE. constructor. assumption.
@@ -1243,7 +1307,7 @@ Proof.
     erewrite <- seval_preserved; [| eapply ctx]. constructor.
   (* Sreturn *)
   - destruct hf2; inv CORE. simpl. rewrite H0. constructor.
-Qed.
+Qed. *)
 
 Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := 
   match i with
@@ -1269,16 +1333,15 @@ Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval :=
   | _ => RET (HSnone)
   end.
 
-(** TODO - figure out how to prove that stuff *)
-Lemma hsexec_final_correct hsl sl i:
-  (forall ge sp rs0 m0, hsilocal_refines ge sp rs0 m0 hsl sl) ->
+Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
   WHEN hsexec_final i hsl ~> hsf THEN
-  hfinal_refines hsf (sexec_final i sl).
+  hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
 Proof.
-  destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
+(*   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. unfold hfinal_refines. simpl.
+    apply mayRet_ret in HSF. subst. unfold hfinal_refines. simpl. *)
     
 (* 
     + intro. inv H. constructor; auto.
@@ -1371,8 +1434,9 @@ Global Opaque hfinal_simu_core.
 
 Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
    hsistate_refines_stat (hinternal hst) (internal st)
-  /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st))
-  /\ hfinal_refines (hfinal hst) (final st).
+  /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st)
+                        /\ hfinal_refines ge sp rs0 m0 (hfinal hst) (final st))
+.
 
 Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
      hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
@@ -1392,7 +1456,7 @@ Proof.
   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|].
+  constructor; [apply SCORE; auto|]. 1-2: eassumption.
   destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
   eapply FSIMU.
 Qed.