Solving the hok problem

1 files changed, 14 insertions, 31 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index f25143fd..e55cd461 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -194,9 +194,8 @@ Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
 
 Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop :=
    hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext)
-   /\ (hsok_exit ge sp rs0 m0 hext -> 
-        seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem_get (hsi_elocal hext)) rs0 m0 
-         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0).
+   /\ seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem_get (hsi_elocal hext)) rs0 m0
+         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0.
 
 Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
   hsiexit_refines_stat hse1 se1 ->
@@ -226,11 +225,9 @@ Qed.
 
 Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx:
   hsiexit_simu_core dm f hse1 hse2 ->
-  hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
   hsiexit_simu dm f ctx hse1 hse2.
 Proof.
-  intros SIMUC HOK1 st1 st2 HREF1 HREF2 HDYN1 HDYN2.
-  exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2.
+  intros SIMUC (* HOK1 *) st1 st2 HREF1 HREF2 HDYN1 HDYN2.
   assert (SEVALC:
     seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) 
   (the_rs0 ctx) (the_m0 ctx) =
@@ -241,8 +238,11 @@ Proof.
     destruct SIMUC as (_ & _ & CONDEQ & ARGSEQ & LSIMU). destruct LSIMU as (_ & _ & _ & MEMEQ).
     rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- seval_condition_preserved; eauto.
     eapply ctx. }
-  constructor; [assumption|].
-  intros is1 SSEME.
+  constructor; [assumption|]. intros is1 SSEME.
+  assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). {
+    unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML.
+    destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
+  exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2.
   exists (mk_istate (icontinue is1) (si_ifso st2) (irs is1) (imem is1)). simpl. constructor.
   - constructor; [|constructor].
     + rewrite <- SEVALC. destruct SSEME as (SCOND & _ & _). assumption.
@@ -273,13 +273,6 @@ Proof.
   auto.
 Qed.
 
-Inductive hsok_exits ge sp rs m: list hsistate_exit -> Prop :=
-  | hsok_exits_nil: hsok_exits ge sp rs m nil
-  | hsok_exits_cons: forall he lhe,
-      hsok_exits ge sp rs m lhe ->
-      hsok_exit ge sp rs m he ->
-      hsok_exits ge sp rs m (he::lhe).
-
 Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop :=
   list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2.
 
@@ -329,11 +322,10 @@ Admitted.
 
 Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx:
   hsiexits_simu_core dm f lhse1 lhse2 ->
-  hsok_exits (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 ->
   hsiexits_simu dm f ctx lhse1 lhse2.
 Proof.
   induction 1; [constructor|].
-  intros HOKS. inv HOKS. constructor; [|apply IHlist_forall2; assumption].
+  constructor; [|apply IHlist_forall2; assumption].
   apply hsiexit_simu_core_correct; assumption.
 Qed.
 
@@ -374,10 +366,6 @@ Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f):
   hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
   sistate_simu dm f st1 st2 ctx.
 
-Definition hsok ge sp rs m hst := 
-     hsok_exits ge sp rs m (hsi_exits hst)
-  /\ hsok_local ge sp rs m (hsi_local hst).
-
 Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
   siexits_simu dm f lse1 lse2 ctx ->
   all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) ->
@@ -471,13 +459,12 @@ Qed.
 
 Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx:
   hsistate_simu_core dm f hst1 hst2 ->
-  hsok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
   hsistate_simu dm f hst1 hst2 ctx.
 Proof.
-  intros SIMUC HOK st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI.
+  intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI.
   destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2).
   destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2).
-  destruct SIMUC as (PCSIMU & ESIMU & LSIMU). destruct HOK as (EOK1 & LOK1).
+  destruct SIMUC as (PCSIMU & ESIMU & LSIMU).
   exploit hsiexits_simu_core_correct; eauto. intro HESIMU.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
   - destruct SEMI as (SSEML & PCEQ & ALLFU).
@@ -604,8 +591,6 @@ Theorem hsstate_simu_coreb_correct dm f hst1 hst2:
 Proof.
 Admitted.
 
-Definition hok ge sp rs m hst := hsok ge sp rs m (hinternal hst).
-
 Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
   forall st1 st2,
   hsstate_refines hst1 st1 ->
@@ -613,13 +598,12 @@ Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
 
 Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
   hsstate_simu_core dm f hst1 hst2 ->
-  hok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
   hsstate_simu dm f hst1 hst2 ctx.
 Proof.
-  intros (SCORE & FSIMU) HOK1. intros st1 st2 HREF1 HREF2.
+  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; [|eassumption].
+  eapply hsistate_simu_core_correct in SCORE.
   eapply hfinal_simu_core_correct in FSIMU; eauto.
   constructor; [apply SCORE; auto|].
   destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
@@ -1532,8 +1516,7 @@ Proof.
   eexists; split; eauto.
   intros ctx. eapply hsstate_simu_coreb_correct in H.
   eapply hsstate_simu_core_correct; eauto.
-  (* TODO - Needs a sok in _theory.v, and a sok -> hok lemma *)
-Admitted.
+Qed.
 
 Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
   match lm with