[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof

1 files changed, 98 insertions, 26 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index c99c3b43..28760a72 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -51,14 +51,18 @@ Inductive condition : Type :=
   | Ccompfs (c: comparison)     (**r 32-bit floating-point comparison *)
   | Cnotcompfs (c: comparison)  (**r negation of a floating-point comparison *)
   (* Expansed branches *)
-  | CEbeqw (optR0: option bool)                      (**r branch-if-equal *)
+  | CEbeqw (optR0: option bool)                      (**r branch-if-equal signed *)
   | CEbnew (optR0: option bool)                      (**r branch-if-not-equal signed *)
+  | CEbequw (optR0: option bool)                     (**r branch-if-equal unsigned *)
+  | CEbneuw (optR0: option bool)                     (**r branch-if-not-equal unsigned *)
   | CEbltw (optR0: option bool)                      (**r branch-if-less signed *)
   | CEbltuw (optR0: option bool)                     (**r branch-if-less unsigned *)
   | CEbgew (optR0: option bool)                      (**r branch-if-greater-or-equal signed *)
   | CEbgeuw (optR0: option bool)                     (**r branch-if-greater-or-equal unsigned *)
-  | CEbeql (optR0: option bool)                      (**r branch-if-equal *)
+  | CEbeql (optR0: option bool)                      (**r branch-if-equal signed *)
   | CEbnel (optR0: option bool)                      (**r branch-if-not-equal signed *)
+  | CEbequl (optR0: option bool)                     (**r branch-if-equal unsigned *)
+  | CEbneul (optR0: option bool)                     (**r branch-if-not-equal unsigned *)
   | CEbltl (optR0: option bool)                      (**r branch-if-less signed *)
   | CEbltul (optR0: option bool)                     (**r branch-if-less unsigned *)
   | CEbgel (optR0: option bool)                      (**r branch-if-greater-or-equal signed *)
@@ -167,8 +171,10 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   (* Expansed conditions *)
-  | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
-  | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
+  | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
+  | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
+  | OEsequw (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneuw (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
   | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
@@ -176,8 +182,10 @@ Inductive operation : Type :=
   | OExoriw (n: int)                             (**r xor immediate *)
   | OEluiw (n: int)                              (**r load upper-immediate *)
   | OEaddiwr0 (n: int)                           (**r add immediate *)
-  | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
-  | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
+  | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
+  | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
+  | OEsequl (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneul (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltl (optR0: option bool)                  (**r set-less-than *)
   | OEsltul (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltil (n: int64)                           (**r set-less-than immediate *)
@@ -270,14 +278,18 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
   | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
   (* Expansed branches *)
-  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
-  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
+  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Ceq) v1 v2 zero32
+  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32
+  | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
+  | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
   | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32
   | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32
   | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32
   | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32
-  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
-  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
+  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Ceq) v1 v2 zero64
+  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64
+  | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
+  | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
   | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64
   | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64
   | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64
@@ -383,8 +395,10 @@ Definition eval_operation
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   (* Expansed conditions *)
-  | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
-  | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
+  | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32)
+  | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
+  | OEsneuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
   | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32)
   | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
@@ -392,8 +406,10 @@ Definition eval_operation
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
   | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12)))
   | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
-  | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
-  | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
+  | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
+  | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64))
+  | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
+  | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
   | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64))
   | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64))
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
@@ -469,12 +485,16 @@ Definition type_of_condition (c: condition) : list typ :=
   | Cnotcompfs _ => Tsingle :: Tsingle :: nil
   | CEbeqw _ => Tint :: Tint :: nil
   | CEbnew _ => Tint :: Tint :: nil
+  | CEbequw _ => Tint :: Tint :: nil
+  | CEbneuw _ => Tint :: Tint :: nil
   | CEbltw _ => Tint :: Tint :: nil
   | CEbltuw _ => Tint :: Tint :: nil
   | CEbgew _ => Tint :: Tint :: nil
   | CEbgeuw _ => Tint :: Tint :: nil
   | CEbeql _ => Tlong :: Tlong :: nil
   | CEbnel _ => Tlong :: Tlong :: nil
+  | CEbequl _ => Tlong :: Tlong :: nil
+  | CEbneul _ => Tlong :: Tlong :: nil
   | CEbltl _ => Tlong :: Tlong :: nil
   | CEbltul _ => Tlong :: Tlong :: nil
   | CEbgel _ => Tlong :: Tlong :: nil
@@ -578,6 +598,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocmp c => (type_of_condition c, Tint)
   | OEseqw _ => (Tint :: Tint :: nil, Tint)
   | OEsnew _ => (Tint :: Tint :: nil, Tint)
+  | OEsequw _ => (Tint :: Tint :: nil, Tint)
+  | OEsneuw _ => (Tint :: Tint :: nil, Tint)
   | OEsltw _ => (Tint :: Tint :: nil, Tint)
   | OEsltuw _ => (Tint :: Tint :: nil, Tint)
   | OEsltiw _ => (Tint :: nil, Tint)
@@ -587,6 +609,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEaddiwr0 _ => (nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsneul _ => (Tlong :: Tlong :: nil, Tint)
   | OEsltl _ => (Tlong :: Tlong :: nil, Tint)
   | OEsltul _ => (Tlong :: Tlong :: nil, Tint)
   | OEsltil _ => (Tlong :: nil, Tint)
@@ -808,9 +832,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
   (* OEseqw *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
+    destruct Val.cmp_bool... all: destruct b...
+  (* OEsnew *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
+    destruct Val.cmp_bool... all: destruct b...
+  (* OEsequw *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
     destruct Val.cmpu_bool... all: destruct b...
-  (* OEsnew *)
+  (* OEsneuw *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
     destruct Val.cmpu_bool... all: destruct b...
   (* OEsltw *)
@@ -831,9 +861,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEaddiwr0 *)
   - trivial.
   (* OEseql *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
+    destruct Val.cmpl_bool... all: destruct b...
+  (* OEsnel *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
+    destruct Val.cmpl_bool... all: destruct b...
+  (* OEsequl *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
     destruct Val.cmplu_bool... all: destruct b...
-  (* OEsnel *)
+  (* OEsneul *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
     destruct Val.cmplu_bool... all: destruct b...
   (* OEsltl *)
@@ -944,12 +980,16 @@ Definition negate_condition (cond: condition): condition :=
   | Cnotcompfs c => Ccompfs c
   | CEbeqw optR0 => CEbnew optR0
   | CEbnew optR0 => CEbeqw optR0
+  | CEbequw optR0 => CEbneuw optR0
+  | CEbneuw optR0 => CEbequw optR0
   | CEbltw optR0 => CEbgew optR0
   | CEbltuw optR0 => CEbgeuw optR0
   | CEbgew optR0 => CEbltw optR0
   | CEbgeuw optR0 => CEbltuw optR0
   | CEbeql optR0 => CEbnel optR0
   | CEbnel optR0 => CEbeql optR0
+  | CEbequl optR0 => CEbneul optR0
+  | CEbneul optR0 => CEbequl optR0
   | CEbltl optR0 => CEbgel optR0
   | CEbltul optR0 => CEbgeul optR0
   | CEbgel optR0 => CEbltl optR0
@@ -975,6 +1015,10 @@ Proof.
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.
 
   repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
   apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
   apply Val.negate_cmpu_bool.
@@ -987,6 +1031,10 @@ Proof.
   repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|];
   apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
   apply Val.negate_cmplu_bool.
   repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
   apply Val.negate_cmplu_bool.
@@ -1094,12 +1142,12 @@ Definition cond_depends_on_memory (cond : condition) : bool :=
   | Ccompuimm _ _ => negb Archi.ptr64
   | Ccomplu _ => Archi.ptr64
   | Ccompluimm _ _ => Archi.ptr64
-  | CEbeqw _ => negb Archi.ptr64
-  | CEbnew _ => negb Archi.ptr64
+  | CEbequw _ => negb Archi.ptr64
+  | CEbneuw _ => negb Archi.ptr64
   | CEbltuw _ => negb Archi.ptr64
   | CEbgeuw _ => negb Archi.ptr64
-  | CEbeql _ => Archi.ptr64
-  | CEbnel _ => Archi.ptr64
+  | CEbequl _ => Archi.ptr64
+  | CEbneul _ => Archi.ptr64
   | CEbltul _ => Archi.ptr64
   | CEbgeul _ => Archi.ptr64
   | _ => false
@@ -1108,12 +1156,12 @@ Definition cond_depends_on_memory (cond : condition) : bool :=
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp cmp => cond_depends_on_memory cmp
-  | OEseqw _ => negb Archi.ptr64
-  | OEsnew _ => negb Archi.ptr64
+  | OEsequw _ => negb Archi.ptr64
+  | OEsneuw _ => negb Archi.ptr64
   | OEsltiuw _ => negb Archi.ptr64
   | OEsltuw _ => negb Archi.ptr64
-  | OEseql _ => Archi.ptr64
-  | OEsnel _ => Archi.ptr64
+  | OEsequl _ => Archi.ptr64
+  | OEsneul _ => Archi.ptr64
   | OEsltul _ => Archi.ptr64
   | OEsltiul _ => Archi.ptr64
   | _ => false
@@ -1380,6 +1428,10 @@ Proof.
 - inv H3; inv H2; simpl in H0; inv H0; auto.
 - inv H3; inv H2; simpl in H0; inv H0; auto.
 - destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
   eapply eval_cmpu_bool_inj'; eauto.
 - destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
   eapply eval_cmpu_bool_inj'; eauto.
@@ -1392,6 +1444,10 @@ Proof.
 - destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
   eapply eval_cmpu_bool_inj'; eauto.
 - destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
   eapply eval_cmplu_bool_inj'; eauto.
 - destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
   eapply eval_cmplu_bool_inj'; eauto.
@@ -1612,8 +1668,16 @@ Proof.
     destruct b; simpl; constructor.
     simpl; constructor.
   (* OEseqw *)
-  - apply eval_cmpu_bool_inj_opt; auto.
+  - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
+    inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
   (* OEsnew *)
+  - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
+    inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
+  (* OEsequw *)
+  - apply eval_cmpu_bool_inj_opt; auto.
+  (* OEsneuw *)
   - apply eval_cmpu_bool_inj_opt; auto.
   (* OEsltw *)
   - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
@@ -1628,8 +1692,16 @@ Proof.
   (* OExoriw *)
   - inv H4; simpl; auto.
   (* OEseql *)
-  - apply eval_cmplu_bool_inj_opt; auto.
+  - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
+    inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
   (* OEsnel *)
+  - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
+    inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
+  (* OEsequl *)
+  - apply eval_cmplu_bool_inj_opt; auto.
+  (* OEsneul *)
   - apply eval_cmplu_bool_inj_opt; auto.
   (* OEsltl *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;