fp_divs32_correct

1 files changed, 41 insertions, 0 deletions

diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v
index 4e9b2fb2..48e4bbbc 100644
--- a/kvx/FPDivision32.v
+++ b/kvx/FPDivision32.v
@@ -811,3 +811,44 @@ Proof.
       rewrite Z.rem_mod_nonneg by lia.
       reflexivity.
 Qed.
+
+Definition fp_mods32 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 :
+  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.
+  unfold fp_mods32.
+  Local Opaque fp_modu32.
+  repeat (econstructor + apply eval_lift + eassumption).
+  apply fp_modu32_correct.
+  all: repeat (econstructor + apply eval_lift + eassumption).
+  { unfold ExtValues.int_absdiff, ExtValues.Z_abs_diff.
+    rewrite Int.signed_zero. rewrite Z.sub_0_r.
+    rewrite Int.unsigned_repr.
+    { pose proof (nonzero_unsigned_signed b b_nz).
+      lia.
+    }
+    pose proof Int.max_signed_unsigned.
+    pose proof int_min_signed_unsigned.
+    pose proof (Int.signed_range b).
+    lia.
+  }
+  cbn.
+  rewrite int_mods_modu ; cycle 1.
+  { apply nonzero_unsigned_signed. assumption. }
+  unfold Int.lt, ExtValues.int_abs, ExtValues.int_absdiff, ExtValues.Z_abs_diff.
+  change (Int.signed Int.zero) with 0%Z.
+  repeat rewrite Z.sub_0_r.
+  destruct zlt; reflexivity. 
+Qed.