From 7fa462ec791789cfec4327e03531efed56252937 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 7 Sep 2020 14:44:37 +0200
Subject: hsexec_final_correct progress

---
 kvx/lib/RTLpathSE_impl_junk.v | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 1edfa53d..1831b3fc 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1500,15 +1500,42 @@ Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval :=
   | _ => RET (HSnone)
   end.
 
+Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  WHEN hsi_sreg_get hsl r ~> hsv THEN
+  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
+Proof.
+  intros HOK HREF. wlp_intros hsv HSV. unfold sval_refines.
+  erewrite <- hsi_sreg_eval_correct; eauto.
+  destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption].
+  reflexivity.
+Qed.
+
+Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros:
+  hsok_local ge sp rs0 m0 hsl ->
+  hsilocal_refines ge sp rs0 m0 hsl sl ->
+  WHEN hsum_left hsl ros ~> svos THEN
+  sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros).
+Proof.
+  intros HOK HREF. destruct ros; [| wlp_simplify].
+  wlp_step_bind hr HGET. wlp_simplify. unfold sval_refines.
+  rewrite sval_refines_local_get; eauto.
+Qed.
+
 Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
+  hsok_local ge sp rs0 m0 hsl ->
   hsilocal_refines ge sp rs0 m0 hsl sl ->
   WHEN hsexec_final i hsl ~> hsf THEN
   hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
 Proof.
-(*   destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
+  intro HOK.
+  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. constructor.
+    + eapply hsum_left_correct; eauto.
+    + Search list_refines. admit.
     
 (* 
     + intro. inv H. constructor; auto.
@@ -1527,6 +1554,7 @@ Proof.
   - admit.
  *)Admitted.
 
+
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with
   | nil, nil => RET tt
-- 
cgit