hsiexec_inst_correct_dyn proof of Iop

1 files changed, 42 insertions, 1 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index e55055fa..0c2af325 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1947,6 +1947,45 @@ Proof.
   destruct H1 as (A & B & C & D). rewrite <- B; eauto.
 Qed.
 
+Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr:
+  hsok_local ge sp rs0 m0 hst ->
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  WHEN hlist_args hst lr ~> lhsv THEN
+  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0.
+Proof.
+  intros OKL HLREF. wlp_simplify.
+  destruct lr.
+  - simpl in *. inv H. reflexivity.
+  - inv H. simpl. unfold seval_list_hsval. simpl. rewrite H4. erewrite seval_list_sval_proj; eauto.
+Qed.
+
+Lemma seval_list_sval_none ge sp (srs: reg -> sval) rs0 m0: forall lr,
+  (forall r, seval_sval ge sp (srs r) rs0 m0 <> None) ->
+  seval_list_sval ge sp (list_sval_inj (List.map srs lr)) rs0 m0 <> None.
+Proof.
+  induction lr.
+  - simpl. discriminate.
+  - intro SR. simpl. destruct (seval_sval _ _ _ _ _) eqn:V.
+    2: { apply SR in V. inv V. }
+    destruct (seval_list_sval _ _ _ _ _) eqn:LV.
+    2: { apply IHlr in SR. assumption. }
+    discriminate.
+Qed.
+
+Lemma refines_okargs ge sp rs0 m0 hst st lr: 
+  hsistate_refines_dyn ge sp rs0 m0 hst st ->
+  hok_args ge sp rs0 m0 (hsi_local hst) lr.
+Proof.
+  unfold hok_args.
+  intros (_ & HLREF & _). wlp_intro lhsv LHSV. intros OK.
+  exploit hlist_args_correct; eauto. intro LREF.
+  erewrite seval_list_hsval_refines; eauto.
+  destruct HLREF as (OKEQ & _ & _).
+  rewrite <- OKEQ in OK.
+  destruct OK as (_ & _ & OK).
+  apply seval_list_sval_none. assumption.
+Qed.
+
 (* Local Hint Resolve refines_okargs: core. *)
 Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
   WHEN hsiexec_inst i hst ~> ohst' THEN
@@ -1962,7 +2001,7 @@ Proof.
     eapply hsist_set_local_correct_dyn; eauto.
     + destruct H1 as (A & B & C).
       eapply hslocal_set_sreg_correct; eauto.
-      { admit. (* refines_okargs *) }
+      { eapply refines_okargs. repeat (econstructor; eauto). }
       simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV.
       eapply hlist_args_correct in LHSV; eauto.
       erewrite hSop_correct; eauto. simpl. reflexivity.
@@ -1988,6 +2027,8 @@ Proof.
   - admit.
 Admitted.
 
+
+
 (* PROOF from RTLpathSE_impl.v
   destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1;
     inversion_clear STEP2; discriminate || (intro REF; eauto).