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

1 files changed, 32 insertions, 0 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index d826f139..d0c826a3 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -281,6 +281,12 @@ Definition transl_cbranch
   | CEbnew optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
+  | CEbequw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
+  | CEbneuw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
   | CEbltw optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k)
@@ -299,6 +305,12 @@ Definition transl_cbranch
   | CEbnel optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
+  | CEbequl optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k)
+  | CEbneul optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
   | CEbltl optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k)
@@ -768,6 +780,16 @@ Definition transl_op
       do rs1 <- ireg_of a1;
       do rs2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k)
+  | OEsequw optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k)
+  | OEsneuw optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k)
   | OEsltw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
@@ -806,6 +828,16 @@ Definition transl_op
       do rs1 <- ireg_of a1;
       do rs2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k)
+  | OEsequl optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k)
+  | OEsneul optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k)
   | OEsltl optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;