is_exp and bcond proof

1 files changed, 35 insertions, 18 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index efc22eb6..ac9cb8d8 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -1,4 +1,4 @@
-Require Import Coqlib Maps.
+Require Import Coqlib Maps Lia.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad BTL.
 
@@ -6,12 +6,10 @@ Require Import Errors Linking RTLtoBTL.
 
 Require Import Linking.
 
-(* TODO: remplacer "right_assoc" par "expand" ci-dessous *)
-
 Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
-  code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry);
+  code_expand: forall pc ib, (fn_code tf)!pc=Some ib -> is_expand ib.(entry);
   preserv_fnsig: fn_sig tf = RTL.fn_sig f;
   preserv_fnparams: fn_params tf = RTL.fn_params f;
   preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
@@ -33,7 +31,7 @@ Lemma verify_function_correct dupmap f f' tt:
   fn_sig f' = RTL.fn_sig f ->
   fn_params f' = RTL.fn_params f ->
   fn_stacksize f' = RTL.fn_stacksize f ->
-  (forall pc ib, (fn_code f')!pc=Some ib -> is_right_assoc ib.(entry)) ->
+  (forall pc ib, (fn_code f')!pc=Some ib -> is_expand ib.(entry)) ->
   match_function dupmap f f'.
 Proof.
   unfold verify_function; intro VERIF. monadInv VERIF.
@@ -48,7 +46,7 @@ Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
   eexists; eapply verify_function_correct; simpl; eauto.
-  eapply right_assoc_code_correct; eauto.
+  eapply expand_code_correct; eauto.
 Qed.
 
 Lemma transf_fundef_correct f f':
@@ -112,7 +110,7 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
       (ATpc0: (fn_code f')!pcB0 = Some ib0)
       (DUPLIC: dupmap!pcB0 = Some pcR0)
       (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
-      (RIGHTA: is_right_assoc ib)
+      (IS_EXPD: is_expand ib)
       (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
       : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
@@ -245,6 +243,12 @@ Definition omeasure (oib: option iblock): nat :=
  | Some ib => measure ib
  end.
 
+Lemma measure_pos: forall ib,
+  measure ib > 0.
+Proof.
+  induction ib; simpl; auto; lia.
+Qed.
+
 Lemma opt_simu_intro
   sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1'
   (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
@@ -253,7 +257,7 @@ Lemma opt_simu_intro
   (ATpc0 : (fn_code f') ! pcB0 = Some ib0)
   (DUPLIC : dupmap ! pcB0 = Some pcR0)
   (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
-  (RIGHTA : is_right_assoc ib)
+  (IS_EXPD : is_expand ib)
   (RTL_RUN : star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0
               (RTL.State st f sp pcR1 rs m))
   (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 =
@@ -280,12 +284,12 @@ Proof.
     + (* Bnop *)
       inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *)
       exists (Some b2); right; repeat (split; auto).
-      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      econstructor; eauto. inv IS_EXPD; auto; discriminate.
       eapply star_right; eauto.
     + (* Bop *)
       inversion STEP; subst; try_simplify_someHyps.
       exists (Some b2); right; repeat (split; auto).
-      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      econstructor; eauto. inv IS_EXPD; auto; discriminate.
       eapply star_right; eauto.
       erewrite eval_operation_preserved in H10.
       erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
@@ -293,7 +297,7 @@ Proof.
     + (* Bload *)
       inversion STEP; subst; try_simplify_someHyps.
       exists (Some (b2)); right; repeat (split; auto).
-      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      econstructor; eauto. inv IS_EXPD; auto; discriminate.
       eapply star_right; eauto.
       erewrite eval_addressing_preserved in H10.
       erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
@@ -301,17 +305,30 @@ Proof.
     + (* Bstore *)
       inversion STEP; subst; try_simplify_someHyps.
       exists (Some b2); right; repeat (split; auto).
-      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      econstructor; eauto. inv IS_EXPD; auto; discriminate.
       eapply star_right; eauto.
       erewrite eval_addressing_preserved in H10.
       erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
       intros; rewrite <- symbols_preserved; trivial.
     + (* Absurd case *)
-      inv RIGHTA. inv H4. inv H.
-    + (* Bcond *)
-      admit.
+      inv IS_EXPD. inv H4. inv H.
+    + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *)
+      inv IS_EXPD; discriminate.
   - (* mib_cond *)
-    admit.
+    inversion STEP; subst; try_simplify_someHyps.
+    intros; rewrite H12 in BTL_RUN. destruct b.
+    * (* Ifso *)
+      exists (Some bso); right; repeat (split; eauto).
+      simpl; assert (measure bnot > 0) by apply measure_pos; lia.
+      inv H2; econstructor; eauto.
+      1,3: inv IS_EXPD; auto; discriminate.
+      all: eapply star_right; eauto.
+    * (* Ifnot *)
+      exists (Some bnot); right; repeat (split; eauto).
+      simpl; assert (measure bso > 0) by apply measure_pos; lia.
+      inv H2; econstructor; eauto.
+      1,3: inv IS_EXPD; auto; discriminate.
+      all: eapply star_right; eauto.
 Admitted.
 
 Theorem opt_simu s1 t s1' oib s2:
@@ -338,7 +355,7 @@ Proof.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
       * econstructor; eauto.
-        eapply code_right_assoc; eauto.
+        eapply code_expand; eauto.
         all: erewrite preserv_fnparams; eauto.
         constructor.
     + (* External function *)
@@ -356,7 +373,7 @@ Proof.
     eexists; left; eexists; split.
     + eapply exec_return.
     + econstructor; eauto.
-      eapply code_right_assoc; eauto.
+      eapply code_expand; eauto.
       constructor.
 Qed.