From 0fef148ea767281afc3fb8248bee0420f431f9aa Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 3 Sep 2020 11:51:14 +0200
Subject: More proofs

---
 kvx/lib/RTLpathSE_impl.v | 40 ++++++++++++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 8 deletions(-)

(limited to 'kvx')

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index e7efa3ec..e173aa6c 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -1235,9 +1235,12 @@ Lemma hsiexec_inst_correct_stat i hst hst' st:
   exists st', siexec_inst i st = Some st'
   /\ (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st').
 Proof.
- destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto.
- (* TODO *)
-Admitted.
+  destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto.
+  intros HREF. constructor; [simpl; reflexivity|]. simpl.
+  destruct HREF as (PCEQ & EXREF).
+  constructor; [|assumption]. clear EXREF.
+  constructor.
+Qed.
 
 Lemma refines_okargs ge sp rs0 m0 hst st l: 
  hsistate_refines_dyn ge sp rs0 m0 hst st ->
@@ -1312,22 +1315,43 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate
     hsiexec_path p f hst1
   end.
 
-Lemma hsiexec_path_correct_stat ps f hst hst' st:
+Lemma hsiexec_path_correct_stat f ps: forall hst hst',
   hsiexec_path ps f hst = Some hst' -> 
-  hsistate_refines_stat hst st ->
+  forall st, hsistate_refines_stat hst st ->
   exists st', siexec_path ps f st = Some st' /\ hsistate_refines_stat hst' st'.
 Proof.
-Admitted.
+  induction ps.
+  - simpl. intros. inv H. repeat (econstructor; eauto).
+  - simpl. intros hst hst' EPATH st HREF.
+    destruct HREF as (PCREF & EXREF). rewrite <- PCREF.
+    destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate].
+    destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate].
+    eapply (hsiexec_inst_correct_stat _ _ _ st) in HSI. destruct HSI as (st' & SI' & HREF').
+    lapply HREF'; [|constructor; assumption]. clear HREF'. intro HREF'.
+    eapply IHps in EPATH; eauto. destruct EPATH as (st'' & SIPATH & HREF'').
+    exists st''. constructor; [|assumption].
+    rewrite SI'. assumption.
+Qed.
 
-Lemma hsiexec_path_correct_dyn ge sp rs0 m0 ps f hst hst' st st':
+Lemma hsiexec_path_correct_dyn ge sp rs0 m0 f: forall ps hst hst',
   hsiexec_path ps f hst = Some hst' -> 
+  forall st st',
   siexec_path ps f st = Some st' ->
   hsistate_refines_stat hst st ->
   hsistate_refines_stat hst' st' ->
   hsistate_refines_dyn ge sp rs0 m0 hst st 
   -> hsistate_refines_dyn ge sp rs0 m0 hst' st'.
 Proof.
-Admitted.
+  induction ps; [simpl; intros; congruence|].
+  intros hst hst' HPATH st st' SPATH HSTAT HSTAT' HDYN.
+  simpl in *. destruct HSTAT as (PCREF & EXREF). rewrite <- PCREF in SPATH.
+  destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate].
+  destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate].
+  exploit hsiexec_inst_correct_stat; eauto. intros (s & SI & HREF).
+  lapply HREF; [|constructor; eassumption]. clear HREF. intro HREF.
+  rewrite SI in SPATH.
+  eapply hsiexec_inst_correct_dyn in HSI; eauto.
+Qed.
 
 
 Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
-- 
cgit