more on ternary

2 files changed, 149 insertions, 6 deletions

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 0dad482b..65364579 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -62,11 +62,11 @@ Section SELECT.
 Context {hf: helper_functions}.
 
 (** Stuff for select *)
-Definition is_zero_expr (vt : expr) : expr :=
+Definition is_zero (vt : expr) : expr :=
   Eop (Ocmp (Ccomp Ceq))
       (vt:::(Eop (Ointconst Int.zero) Enil):::Enil).
 
-Definition is_nonzero_expr (vt : expr) : expr :=
+Definition is_nonzero (vt : expr) : expr :=
   Eop (Ocmp (Ccomp Cne))
       (vt:::(Eop (Ointconst Int.zero) Enil):::Enil).
 
@@ -76,14 +76,14 @@ Definition bool_to_bitmask (et : expr) : expr :=
 Definition not_bool_to_bitmask (et : expr) : expr :=
   Eop Osub (et:::(Eop (Ointconst Int.one) Enil):::Enil).
 
-Definition ternary_expand (et e0 e1 : expr) : expr :=
+Definition ternary_expand (e0 e1 et : expr) : expr :=
   Eop Oor
     ((Eop Oand ((not_bool_to_bitmask et):::e1:::Enil)):::
      (Eop Oand ((bool_to_bitmask et):::e0:::Enil)):::
      Enil).
                      
-Definition select_or_expand (et e0 e1 : expr) : expr :=
-  ternary_expand (is_nonzero_expr et) e0 e1.
+Definition select_or_expand (e0 e1 et: expr) : expr :=
+  ternary_expand e0 e1 (is_zero et).
 
 (** ** Constants **)
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 89af39ee..0637256d 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -92,7 +92,7 @@ Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
-
+  
 (* Helper lemmas - from SplitLongproof.v *)
 
 Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
@@ -163,6 +163,149 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va
   eval_expr ge sp e m le b y ->
   exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.
 
+Definition is_zero_sem (vt : val) : val :=
+  match vt with
+  | Vint x => Vint (if Int.eq x Int.zero then Int.one else Int.zero)
+  | _ => Vundef
+  end.
+
+Theorem eval_is_zero: unary_constructor_sound is_zero is_zero_sem.
+Proof.
+  red; intros.
+  unfold is_zero_sem, is_zero; simpl.
+  TrivialExists.
+  - constructor.
+    + exact H.
+    + constructor; econstructor; constructor.
+  - simpl.
+    destruct x; simpl; try congruence.
+    unfold Vtrue, Vfalse.
+    predSpec Int.eq Int.eq_spec i Int.zero; reflexivity.
+Qed.
+
+Definition is_nonzero_sem (vt : val) : val :=
+  match vt with
+  | Vint x => Vint (if Int.eq x Int.zero then Int.zero else Int.one)
+  | _ => Vundef
+  end.
+
+Theorem eval_is_nonzero: unary_constructor_sound is_nonzero is_nonzero_sem.
+Proof.
+  red; intros.
+  unfold is_zero_sem, is_zero; simpl.
+  TrivialExists.
+  - constructor.
+    + exact H.
+    + constructor; econstructor; constructor.
+  - simpl.
+    destruct x; simpl; try congruence.
+    unfold Vtrue, Vfalse.
+    predSpec Int.eq Int.eq_spec i Int.zero; reflexivity.
+Qed.
+
+
+Definition ternary_constructor_sound (cstr: expr -> expr -> expr -> expr) (sem: val -> val -> val -> val) : Prop :=
+  forall le a x b y c z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  eval_expr ge sp e m le c z ->
+  exists v, eval_expr ge sp e m le (cstr a b c) v /\ Val.lessdef (sem x y z) v.
+
+Lemma int_eq_commut : forall x y,
+    Int.eq x y = Int.eq y x.
+Proof.
+  unfold Int.eq.
+  intros.
+  unfold zeq.
+  destruct (Z.eq_dec _ _);  destruct (Z.eq_dec _ _); congruence.
+Qed.
+
+Theorem eval_select_or_expand : ternary_constructor_sound select_or_expand select.
+Proof.
+  unfold ternary_constructor_sound, ternary_expand.
+  intros.
+  TrivialExists.
+  constructor.
+  - econstructor.
+    constructor.
+    econstructor.
+    constructor.
+    unfold is_zero.
+    econstructor.
+    constructor.
+    eassumption.
+    constructor.
+    econstructor.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    econstructor.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    eassumption.
+    constructor.
+    simpl.
+    reflexivity.
+  - constructor.
+    econstructor.
+    constructor.
+    econstructor.
+    constructor.
+    unfold is_zero.
+    econstructor.
+    constructor.
+    eassumption.
+    constructor.
+    econstructor.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+    eassumption.
+    constructor.
+    simpl.
+    reflexivity.
+    constructor.
+  - simpl.
+    unfold select.
+    destruct z; simpl; trivial.
+    destruct x; simpl; trivial; try (destruct (Int.eq i Int.zero); simpl; rewrite <- (Val.or_commut Vundef); simpl; reflexivity).
+    destruct y; simpl; trivial;
+    try (destruct (Int.eq i Int.zero); simpl; reflexivity).
+    rewrite int_eq_commut. predSpec Int.eq Int.eq_spec Int.zero i.
+    * simpl.
+      rewrite Int.sub_idem.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_commut.
+      rewrite Int.or_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      reflexivity.
+    * simpl.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_zero.
+      reflexivity.
+Qed.
+       
 Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.