Proofs finished for expansion

3 files changed, 68 insertions, 41 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 39b8f367..41a2227b 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
   insn
   :: (if normal' then
       Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
-     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *)
+     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info))
   :: k
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index f6d96d06..6a0297e9 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -1249,32 +1249,75 @@ Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
   seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
   seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
 Proof.
-  (*unfold target_cbranch_expanse, seval_condition; simpl.
+  unfold target_cbranch_expanse, seval_condition; simpl.
   intros H (LREF & SREF & SREG & SMEM) ?.
-  destruct c; try congruence.
-  all:
-    repeat (destruct l; simpl in H; try congruence).
-    inv H; simpl.
-    try erewrite !fsi_sreg_get_correct; eauto.
-
-  - simpl. 
-    destruct c; inv H; simpl.
+  destruct c; try congruence;
+  repeat (destruct l; simpl in H; try congruence).
+  1,2,5,6:
+    destruct c; inv H; simpl;
     try erewrite !fsi_sreg_get_correct; eauto;
+    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
     try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
     try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
-    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence).
-
-    try destruct (Int.eq n Int.zero) eqn: EQIMM;
-    try apply Int.same_if_eq in EQIMM;
-  all:
     try replace (Cle) with (swap_comparison Cge) by auto;
     try replace (Clt) with (swap_comparison Cgt) by auto;
     try rewrite Val.swap_cmp_bool; trivial;
     try rewrite Val.swap_cmpu_bool; trivial;
     try rewrite Val.swap_cmpl_bool; trivial;
-     try rewrite Val.swap_cmplu_bool; trivial.*)
-  all:admit.
-Admitted.
-(*Qed.*)
+    try rewrite Val.swap_cmplu_bool; trivial.
+  1,2,3,4:
+    try destruct (Int.eq n Int.zero) eqn: EQIMM;
+    try apply Int.same_if_eq in EQIMM;
+    try destruct (Int64.eq n Int64.zero) eqn: EQIMM;
+    try apply Int64.same_if_eq in EQIMM;
+    destruct c; inv H; simpl;
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
+    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
+    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
+    unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32;
+    unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64;
+    intros; try (specialize make_immed32_sound with (n);
+    destruct (make_immed32 n) eqn:EQMKI); intros; simpl;
+    intros; try (specialize make_immed64_sound with (n);
+    destruct (make_immed64 n) eqn:EQMKI); intros; simpl;
+    try rewrite EQLO; simpl;
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+    try apply Int.same_if_eq in EQLO; simpl; trivial;
+    try apply Int64.same_if_eq in EQLO; simpl; trivial;
+    unfold may_undef_int, may_undef_luil; 
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1; simpl; trivial;
+    try destruct v; try rewrite H;
+    try rewrite ltu_12_wordsize; try rewrite EQLO;
+    try rewrite Int.add_commut, Int.add_zero_l;
+    try rewrite Int64.add_commut, Int64.add_zero_l;
+    auto; simpl;
+    try rewrite H in EQIMM;
+    try rewrite EQLO in EQIMM;
+    try rewrite Int.add_commut, Int.add_zero_l in EQIMM;
+    try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM;
+    try rewrite EQIMM; simpl;
+    try destruct (Archi.ptr64); trivial.
+
+    1,2,3,4:
+    destruct c; inv H; simpl;
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
+    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
+    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
+    unfold zero32, zero64, Val.cmpf, Val.cmpfs;
+    destruct v, v0; simpl; trivial;
+    try rewrite Float.cmp_ne_eq;
+    try rewrite Float32.cmp_ne_eq;
+    try rewrite <- Float.cmp_swap; simpl;
+    try rewrite <- Float32.cmp_swap; simpl;
+    try destruct (Float.cmp _ _); simpl;
+    try destruct (Float32.cmp _ _); simpl;
+    try rewrite Int.eq_true; simpl;
+    try rewrite Int.eq_false; try apply Int.one_not_zero;
+    simpl; trivial.
+Qed.
 Global Opaque target_op_simplify.
 Global Opaque target_cbranch_expanse.
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 7b1df1ab..12aba56b 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -823,22 +823,6 @@ Proof.
 Global Opaque hslocal_set_sreg.
 Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
-(* TODO gourdinl MOVE ELSEWHERE Branch expansion *)
-
-(* TODO gourdinl NOT SURE IF THIS DEF IS NEEDED
- * SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE?
-Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval :=
-  if is_inv then
-   hlist_args prev*)
-
-(*
-
-
-
-  
-Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
- *)
-
 (** ** Execution of one instruction *)
 
 (* TODO gourdinl
@@ -871,13 +855,13 @@ Lemma cbranch_expanse_correct hst c l:
   (OK: hsok_local ge sp rs0 m0 hst),
   seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
   seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
-Proof. Admitted. (*
+Proof.
   unfold cbranch_expanse.
-  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
-  + destruct p as [c' l']; simpl.
-    exploit target_cbranch_expanse_correct; eauto.
-  + unfold seval_condition; erewrite H; eauto.
-                    Qed.*)
+  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
+  unfold seval_condition; erewrite <- H; eauto.
+  destruct p as [c' l']; simpl.
+  exploit target_cbranch_expanse_correct; eauto.
+Qed.
 Local Hint Resolve cbranch_expanse_correct: wlp.
 Global Opaque cbranch_expanse.