fp_modu32

1 files changed, 31 insertions, 1 deletions

diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v
index 5cda1077..c920d22a 100644
--- a/kvx/FPDivision32.v
+++ b/kvx/FPDivision32.v
@@ -585,4 +585,34 @@ Proof.
     rewrite Int64.unsigned_repr by (cbn; lia).
     reflexivity.
 Qed.
-    
+
+Definition e_msubl a b c := Eop Omsub (a ::: b ::: c ::: Enil).
+Definition fp_modu32 a b := Elet a (Elet (lift b) (e_msubl (Eletvar 1%nat) (Eletvar 0%nat)
+                                                    (fp_divu32 (Eletvar 1%nat) (Eletvar 0%nat)))).
+
+Theorem fp_modu32_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_modu32 expr_a expr_b)
+            (Vint (Int.modu a b)).
+Proof.
+  intros.
+  rewrite Int.modu_divu; cycle 1.
+  { intro Z.
+    subst.
+    rewrite Int.unsigned_zero in b_nz.
+    lia.
+  }
+  unfold fp_modu32.
+  Local Opaque fp_divu32.
+  repeat (econstructor + apply eval_lift + eassumption).
+  { apply fp_divu32_correct;
+    repeat (econstructor + apply eval_lift + eassumption).
+  }
+  cbn.
+  rewrite Int.mul_commut.
+  reflexivity.
+Qed.