From 867b74d57fc2b834cc19176b650dc62a1e4e0fd2 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 16 Feb 2022 09:14:01 +0100
Subject: simpler mod

---
 kvx/FPDivision32.v | 37 +++++++++++++++++++++++++++++++++----
 kvx/FPDivision64.v | 35 +++++++++++++++++++++++++++++++----
 2 files changed, 64 insertions(+), 8 deletions(-)

diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v
index 48e4bbbc..5a7b536f 100644
--- a/kvx/FPDivision32.v
+++ b/kvx/FPDivision32.v
@@ -812,23 +812,23 @@ Proof.
       reflexivity.
 Qed.
 
-Definition fp_mods32 a b :=
+Definition fp_mods32z a b :=
   Elet a (Elet (lift b)
     (Elet (fp_modu32 (e_abs (Eletvar (1%nat))) (e_abs (Eletvar (0%nat))))
           (e_ite Tint (Ccomp0 Clt) (Eletvar 2%nat)
                  (e_neg (Eletvar 0%nat)) (Eletvar 0%nat)))).
 
-Theorem fp_mods32_correct :
+Theorem fp_mods32z_correct :
   forall (ge : genv)  (sp: val) cmenv memenv
          (le : letenv) (expr_a expr_b : expr) (a b : int)
          (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vint a))
          (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b))
          (b_nz : (Int.unsigned b > 0)%Z),
-  eval_expr ge sp cmenv memenv le (fp_mods32 expr_a expr_b)
+  eval_expr ge sp cmenv memenv le (fp_mods32z expr_a expr_b)
             (Vint (Int.mods a b)).
 Proof.
   intros.
-  unfold fp_mods32.
+  unfold fp_mods32z.
   Local Opaque fp_modu32.
   repeat (econstructor + apply eval_lift + eassumption).
   apply fp_modu32_correct.
@@ -852,3 +852,32 @@ Proof.
   repeat rewrite Z.sub_0_r.
   destruct zlt; reflexivity. 
 Qed.
+
+Definition e_msub a b c := Eop Omsub (a ::: b ::: c ::: Enil).
+
+Definition fp_mods32 a b :=
+  Elet a (Elet (lift b)
+    (Elet (fp_divs32 (Eletvar (1%nat)) (Eletvar (0%nat)))
+          (e_msub (Eletvar 2%nat) (Eletvar 1%nat) (Eletvar 0%nat)))).
+
+Theorem fp_mods32_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv
+         (le : letenv) (expr_a expr_b : expr) (a b : int)
+         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vint a))
+         (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b))
+         (b_nz : (Int.unsigned b > 0)%Z),
+  eval_expr ge sp cmenv memenv le (fp_mods32 expr_a expr_b)
+            (Vint (Int.mods a b)).
+Proof.
+  intros.
+  rewrite Int.mods_divs.
+  unfold fp_mods32.
+  Local Opaque fp_divs32.
+  repeat (econstructor + apply eval_lift + eassumption).
+  { apply fp_divs32_correct;
+    repeat (econstructor + apply eval_lift + eassumption).
+  }
+  cbn.
+  rewrite Int.mul_commut.
+  reflexivity.
+Qed.
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 113bf07a..298831a0 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2601,23 +2601,23 @@ Proof.
       reflexivity.
 Qed.
 
-Definition fp_mods64 a b :=
+Definition fp_mods64z a b :=
   Elet a (Elet (lift b)
     (Elet (fp_modu64 (e_absl (Eletvar (1%nat))) (e_absl (Eletvar (0%nat))))
           (e_ite Tlong (Ccompl0 Clt) (Eletvar 2%nat)
                  (e_negl (Eletvar 0%nat)) (Eletvar 0%nat)))).
 
-Theorem fp_mods64_correct :
+Theorem fp_mods64z_correct :
   forall (ge : genv)  (sp: val) cmenv memenv
          (le : letenv) (expr_a expr_b : expr) (a b : int64)
          (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vlong a))
          (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vlong b))
          (b_nz : (Int64.unsigned b > 0)%Z),
-  eval_expr ge sp cmenv memenv le (fp_mods64 expr_a expr_b)
+  eval_expr ge sp cmenv memenv le (fp_mods64z expr_a expr_b)
             (Vlong (Int64.mods a b)).
 Proof.
   intros.
-  unfold fp_mods64.
+  unfold fp_mods64z.
   Local Opaque fp_modu64.
   repeat (econstructor + apply eval_lift + eassumption).
   apply fp_modu64_correct.
@@ -2641,3 +2641,30 @@ Proof.
   repeat rewrite Z.sub_0_r.
   destruct zlt; reflexivity. 
 Qed.
+
+Definition fp_mods64 a b :=
+  Elet a (Elet (lift b)
+    (Elet (fp_divs64 (Eletvar (1%nat)) (Eletvar (0%nat)))
+          (e_msubl (Eletvar 2%nat) (Eletvar 1%nat) (Eletvar 0%nat)))).
+
+Theorem fp_mods64_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv
+         (le : letenv) (expr_a expr_b : expr) (a b : int64)
+         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vlong a))
+         (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vlong b))
+         (b_nz : (Int64.unsigned b > 0)%Z),
+  eval_expr ge sp cmenv memenv le (fp_mods64 expr_a expr_b)
+            (Vlong (Int64.mods a b)).
+Proof.
+  intros.
+  rewrite Int64.mods_divs.
+  unfold fp_mods64.
+  Local Opaque fp_divs64.
+  repeat (econstructor + apply eval_lift + eassumption).
+  { apply fp_divs64_correct;
+    repeat (econstructor + apply eval_lift + eassumption).
+  }
+  cbn.
+  rewrite Int64.mul_commut.
+  reflexivity.
+Qed.
-- 
cgit