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

1 files changed, 29 insertions, 21 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index ece28eff..581229c6 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -41,14 +41,18 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
   | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
   | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
-  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32
-  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32
+  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32
+  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32
+  | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32
+  | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32
   | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32
   | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32
   | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32
   | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32
-  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64
-  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64
+  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64
+  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64
+  | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64
+  | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64
   | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64
   | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64
   | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64
@@ -159,8 +163,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
-  | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32)
-  | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32)
+  | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32)
+  | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32)
+  | OEsneuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32)
   | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32)
   | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
@@ -168,8 +174,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OExoriw n, v1::nil => xor v1 (I n)
   | OEluiw n, nil => I (Int.shl n (Int.repr 12))
   | OEaddiwr0 n, nil => add (I n) zero32
-  | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
-  | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64)
+  | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
+  | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64)
+  | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
+  | OEsneul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64)
   | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64)
   | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64)
   | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
@@ -206,7 +214,7 @@ Proof.
   destruct cond; simpl; eauto with va.
   inv H2.
   destruct cond; simpl; eauto with va.
-  13: destruct cond; simpl; eauto with va.
+  17: destruct cond; simpl; eauto with va.
   all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0;
        unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va.
 Qed.
@@ -291,23 +299,23 @@ Proof.
   apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
 Qed.
 
-Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0,
+Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp,
   vmatch bc a1 b1 ->
   vmatch bc a0 b0 ->
-  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp Clt) a1 a0 Op.zero32)
-  (of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) b1 b0 zero32)).
+  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp cmp) a1 a0 Op.zero32)
+  (of_optbool (apply_bin_r0 optR0 (cmp_bool cmp) b1 b0 zero32)).
 Proof.
   intros.
   destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
   apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
 Qed.
 
-Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0,
+Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp,
   vmatch bc a1 b1 ->
   vmatch bc a0 b0 ->
   vmatch bc
-    (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl Clt) a1 a0 Op.zero64))
-    (of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) b1 b0 zero64)).
+    (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl cmp) a1 a0 Op.zero64))
+    (of_optbool (apply_bin_r0 optR0 (cmpl_bool cmp) b1 b0 zero64)).
 Proof.
   intros.
   destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
@@ -327,16 +335,16 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   
-  1,2,4: apply eval_cmpu_sound; auto.
-  apply eval_cmp_sound; auto.
+  3,4,6: apply eval_cmpu_sound; auto.
+  1,2,3: apply eval_cmp_sound; auto.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
   unfold Val.cmpu; apply of_optbool_sound; eauto with va.
-  unfold zero32; simpl. eauto with va.
-  1,2,4: apply eval_cmplu_sound; auto.
-  apply eval_cmpl_sound; auto.
+  unfold zero32; simpl; eauto with va.
+  3,4,6: apply eval_cmplu_sound; auto.
+  1,2,3: apply eval_cmpl_sound; auto.
   unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.
   unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va.
-  unfold zero64; simpl. eauto with va.
+  unfold zero64; simpl; eauto with va.
   all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.