Avancement sur simu_check_single_correct

1 files changed, 50 insertions, 1 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 2a759ebb..6170318b 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1350,6 +1350,33 @@ Qed.
 Hint Resolve hsstate_simu_check_correct: wlp.
 Global Opaque hsstate_simu_core.
 
+(** Correctness of hsexec *)
+
+(* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct
+  hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *)
+
+Lemma hsexec_correct f pc:
+  WHEN hsexec f pc ~> hst THEN
+  exists st, sexec f pc = Some st /\ hsstate_refines hst st.
+Proof. Admitted.
+(*   unfold hsexec. intro. explore_hyp.
+  unfold sexec. 
+  rewrite EQ.
+  exploit hsiexec_path_correct_stat; eauto.
+  intros (st0 & SPATH & REF0).
+  generalize REF0; intros (PC0 & XREF0). rewrite SPATH.
+  erewrite <- PC0. rewrite EQ1.
+  destruct (hsiexec_inst i h) eqn:HINST.
+  + exploit hsiexec_inst_correct_stat; eauto.
+    intros (st1 & EQ2 & PC2 & REF2).
+    - split; eauto. 
+    - rewrite EQ2.
+      repeat (econstructor; simpl; eauto).
+  + erewrite hsiexec_inst_correct_None; eauto.
+    repeat (econstructor; simpl; eauto).
+    unfold hfinal_refines. simpl; eauto.
+Qed. *)
+
 End CanonBuilding.
 
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
@@ -1365,11 +1392,33 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   (* comparing the executions *)
   hsstate_simu_check dm f hst1 hst2.
 
+Ltac wlp_intros varname hname := apply wlp_unfold; intros varname hname.
+
+Ltac wlp_step_bind varname hname := apply wlp_bind; wlp_intros varname hname.
+
 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.
-  wlp_simplify. (* TODO *)
+  unfold simu_check_single.
+  wlp_step_bind hC_sval HSVAL. wlp_step_bind hC_hlist_sval HLSVAL.
+  wlp_step_bind hC_hsmem HSMEM. wlp_step_bind hst1 HSEXEC1. wlp_step_bind hst2 HSEXEC2.
+  wlp_intros u HSIMU.
+  unfold sexec_simu. intros st1 SEXEC. explore.
+  assert (TODO1: forall hs hsv rhsv, hdata hs = hsv -> hC hC_sval hs ~~> rhsv -> hsval_proj hsv = hsval_proj rhsv)
+    by admit.
+  assert (TODO2: forall hs hsv rhsv, hdata hs = hsv -> hC hC_hlist_sval hs ~~> rhsv -> hsval_list_proj hsv = hsval_list_proj rhsv)
+    by admit.
+  assert (TODO3: forall hs hsv rhsv, hdata hs = hsv -> hC hC_hsmem hs ~~> rhsv -> hsmem_proj hsv = hsmem_proj rhsv)
+    by admit.
+  exploit hsexec_correct; eauto.
+  intros (st2 & SEXEC2 & REF2).
+  exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto.
+  intros (st0 & SEXEC1 & REF1).
+  rewrite SEXEC1 in SEXEC. inv SEXEC.
+  eexists. split; eauto.
+  intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto.
+  eapply hsstate_simu_core_correct; eauto.
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.