hfinal_simu_core

1 files changed, 70 insertions, 1 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 965f8578..bfa66d8b 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -468,7 +468,7 @@ Qed.
 (* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s',
   ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *)
 
-(* FIXME - too strong let's change it later.. *)
+(* FIXME - might be too strong, let's change it later.. *)
 Definition hfinal_refines (hfv fv: sfval) := hfv = fv.
 
 Remark hfinal_refines_snone: hfinal_refines Snone Snone.
@@ -476,6 +476,75 @@ Proof.
   reflexivity.
 Qed.
 
+Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval): Prop :=
+  match hf1 with
+  | Scall sig1 svos1 lsv1 res1 pc1 =>
+      match hf2 with
+      | Scall sig2 svos2 lsv2 res2 pc2 =>
+          dm ! pc2 = Some pc1 /\ sig1 = sig2 /\ svos1 = svos2 /\ lsv1 = lsv2 /\ res1 = res2
+      | _ => False
+      end
+  | Sbuiltin ef1 lbs1 br1 pc1 =>
+      match hf2 with
+      | Sbuiltin ef2 lbs2 br2 pc2 =>
+          dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2
+      | _ => False
+      end
+  | Sjumptable sv1 lpc1 =>
+      match hf2 with
+      | Sjumptable sv2 lpc2 =>
+          ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2
+      | _ => False
+      end
+  (* Snone, Stailcall, Sreturn *)
+  | _ => hf1 = hf2
+  end.
+
+Definition hfinal_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval) := OK tt. (* TODO *)
+
+Theorem hfinal_simu_coreb_correct dm f hf1 hf2:
+  hfinal_simu_coreb dm f hf1 hf2 = OK tt ->
+  hfinal_simu_core dm f hf1 hf2.
+Proof.
+Admitted.
+
+Lemma svident_simu_refl f ctx s:
+  svident_simu f ctx s s.
+Proof.
+  destruct s; constructor; [| reflexivity].
+  erewrite <- seval_preserved; [| eapply ctx]. constructor.
+Qed.
+
+Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
+  hfinal_simu_core dm f hf1 hf2 ->
+  hfinal_refines hf1 f1 ->
+  hfinal_refines hf2 f2 ->
+  dm ! opc2 = Some opc1 ->
+  sfval_simu dm f opc1 opc2 ctx f1 f2.
+Proof.
+  intros CORE FREF1 FREF2 OPCEQ.
+  rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *)
+  destruct hf1.
+  (* Snone *)
+  - simpl in CORE. rewrite <- CORE. constructor. assumption.
+  (* Scall *)
+  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
+    constructor; [assumption | apply svident_simu_refl|].
+    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
+  (* Stailcall *)
+  - simpl in CORE. rewrite <- CORE. constructor; [apply svident_simu_refl|].
+    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
+  (* Sbuiltin *)
+  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst.
+    constructor; [assumption | reflexivity].
+  (* Sjumptable *)
+  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ?). subst.
+    constructor; [assumption|].
+    erewrite <- seval_preserved; [| eapply ctx]. constructor.
+  (* Sreturn *)
+  - simpl in CORE. subst. constructor.
+Qed.
+
 Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
 
 Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=