some progress in canonbuilding

1 files changed, 106 insertions, 14 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index a2b5cc43..25819ffa 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -474,6 +474,8 @@ Proof.
   - intros X; inversion REF.
     erewrite H1; eauto.
 Qed.
+Global Opaque hrexec_store.
+Local Hint Resolve hrexec_store_correct: wlp.
 
 (** ** Assignment of registers *)
 
@@ -786,9 +788,103 @@ Qed.
 Global Opaque hrs_sreg_set.
 Local Hint Resolve hrs_sreg_set_correct: wlp.
 
+(* transfer *)
+
+Lemma ok_hrset_red_sreg ctx r rsv hrs:
+  ris_ok ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs))
+  <-> (ris_ok ctx hrs).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+Qed.
+
+Lemma hrset_red_reg_correct ctx r rsv sv hrs sis:
+  ris_refines ctx hrs sis ->
+  (ris_ok ctx hrs -> eval_sval ctx rsv <> None) ->
+  (ris_ok ctx hrs -> eval_sval ctx rsv = eval_sval ctx sv) ->
+  ris_refines ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs)) (set_sreg r sv sis).
+Proof.
+  destruct 1; intros.
+  econstructor; eauto.
+  + rewrite ok_set_sreg, ok_hrset_red_sreg; intuition congruence.
+  + rewrite ok_hrset_red_sreg; intuition eauto.
+  + rewrite ok_hrset_red_sreg. intros; unfold set_sreg; simpl;
+    erewrite red_PTree_set_refines; eauto.
+    econstructor; eauto.
+Qed.
+
+Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ristate :=
+  match inputs with
+  | nil =>   {| ris_smem := hrs.(ris_smem);
+                ris_input_init := false;
+                ok_rsval := hrs.(ok_rsval);
+                ris_sreg:= PTree.empty _
+             |}
+  | r::l =>
+      let hrs' := transfer_hrs l hrs in
+      ris_sreg_set hrs' (red_PTree_set r (ris_sreg_get hrs r) hrs')
+  end.
+
+Lemma ok_transfer_hrs ctx inputs hrs:
+  ris_ok ctx (transfer_hrs inputs hrs)
+  <-> (ris_ok ctx hrs).
+Proof.
+  induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto.
+  + rewrite ok_hrset_red_sreg. auto.
+Qed.
+
+Lemma transfer_hrs_correct ctx inputs hrs sis:
+  ris_refines ctx hrs sis ->
+  ris_refines ctx (transfer_hrs inputs hrs) (transfer_sis inputs sis).
+Proof.
+  destruct 1; intros.
+  induction inputs as [|r l].
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_hrs; eauto.
+    * erewrite ok_transfer_hrs; eauto.
+    * erewrite ok_transfer_hrs; simpl; unfold ris_sreg_get; simpl; eauto.
+      intros; rewrite PTree.gempty. simpl; auto.
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_hrs; eauto.
+    * erewrite ok_transfer_hrs; simpl.
+      intros; inversion IHl. erewrite MEM_EQ0.
+      - unfold transfer_sis; simpl; eauto.
+      - rewrite ok_transfer_hrs; simpl; eauto.
+    * erewrite ok_transfer_hrs; simpl.
+      intros H r0; inversion IHl.
+      erewrite red_PTree_set_refines; eauto.
+      - destruct (Pos.eq_dec); eauto.
+      - rewrite ok_transfer_hrs. auto.
+Qed.
+
+Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))).
+
+Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core.
+Local Opaque transfer_hrs.
+
+Lemma ok_tr_hrs ctx fi hrs:
+  ris_ok ctx (tr_hrs (cf ctx) fi hrs)
+  <-> (ris_ok ctx hrs).
+Proof.
+   destruct fi; simpl; eauto.
+Qed.
+
+Lemma hrs_ok_tr_okpreserv ctx fi hrs: ris_ok ctx (tr_hrs (cf ctx) fi hrs) -> ris_ok ctx hrs.
+Proof.
+  rewrite ok_tr_hrs; auto.
+Qed.
+
+Lemma tr_hrs_correct ctx fi hrs sis:
+  ris_refines ctx hrs sis ->
+  ris_refines ctx (tr_hrs (cf ctx) fi hrs) (tr_sis (cf ctx) fi sis).
+Proof.
+  intros REF. rewrite <- tr_sis_alt_def.
+  destruct fi; simpl; eauto.
+Qed.
+
 Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
   match ib with
-  | BF fin _ => RET (Rfinal (tr_ris f fin hrs) (sexec_final_sfv fin hrs))
+  | BF fin _ => RET (Rfinal (tr_hrs f fin hrs) (sexec_final_sfv fin hrs))
   (* basic instructions *)
   | Bnop _ => k hrs
   | Bop op args dst _ =>
@@ -817,6 +913,9 @@ Definition hrexec f ib :=
   DO init <~ hrs_init;;
   hrexec_rec f ib init (fun _ => RET Rabort).
 
+Local Hint Resolve exec_final_refpreserv tr_hrs_correct hrs_ok_tr_okpreserv: core.
+Local Hint Constructors rst_refines: core.
+
 Lemma hrexec_rec_correct1 ctx ib: 
   forall rk k
   (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
@@ -835,23 +934,16 @@ Lemma hrexec_rec_correct1 ctx ib:
   WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN
   rst_refines ctx rst st.
 Proof.
-  induction ib; wlp_simplify.
-  - admit.
-  - eapply CONT; eauto.
-  - autodestruct; try_simplify_someHyps; try congruence; intros; subst.
-(*
-    unfold sexec_load.
-    exploit hrs_sreg_set_correct; eauto.
-    eapply CONT; eauto.
-    destruct next.
-  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
+  induction ib; try (wlp_simplify; fail).
+  - wlp_simplify; eapply CONT; eauto.
+  - destruct trap; wlp_simplify.
   - (* seq *)
-    intros; subst.
-    eapply IHib1. 3-6: eauto.
+    wlp_simplify.
+    eapply IHib1. 3-7: eauto.
     + simpl. eapply sexec_rec_okpreserv; eauto.
     + intros; subst. eapply IHib2; eauto.
   - (* cond *)
-    intros rk k CONTh CONT hrs sis lsis sfv st REF EXEC OUT OK. subst.
+    simpl; intros; wlp_simplify.
     assert (rOK: ris_ok ctx hrs). {
       erewrite <- OK_EQUIV. 2: eauto.
       eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.