fp_modu64_correct

1 files changed, 30 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 56170419..1d0fd2ee 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2376,3 +2376,33 @@ Proof.
   rewrite <- full2_div_longu_correct with (m := memenv) by lia.
   apply e_step7_correct; assumption.
 Qed.
+
+Definition fp_modu64 a b := Elet a (Elet (lift b) (e_msubl (Eletvar 1%nat) (Eletvar 0%nat)
+                                                    (fp_divu64 (Eletvar 1%nat) (Eletvar 0%nat)))).
+
+Theorem fp_modu64_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_modu64 expr_a expr_b)
+            (Vlong (Int64.modu a b)).
+Proof.
+  intros.
+  rewrite Int64.modu_divu; cycle 1.
+  { intro Z.
+    subst.
+    rewrite Int64.unsigned_zero in b_nz.
+    lia.
+  }
+  unfold fp_modu64.
+  Local Opaque fp_divu64.
+  repeat (econstructor + apply eval_lift + eassumption).
+  { apply fp_divu64_correct;
+    repeat (econstructor + apply eval_lift + eassumption).
+  }
+  cbn.
+  rewrite Int64.mul_commut.
+  reflexivity.
+Qed.