mods 64

1 files changed, 235 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 1d0fd2ee..113bf07a 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2406,3 +2406,238 @@ Proof.
   rewrite Int64.mul_commut.
   reflexivity.
 Qed.
+
+Definition e_is_negl a := Eop (Ocmp (Ccomplimm Clt Int64.zero)) (a ::: Enil).
+Definition e_xorw a b := Eop Oxor (a ::: b ::: Enil).
+Definition e_negl a := Eop Onegl (a ::: Enil).
+Definition e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil).
+
+Definition fp_divs64 a b :=
+  Elet a (Elet (lift b)
+    (Elet (fp_divu64 (e_absl (Eletvar (1%nat))) (e_absl (Eletvar (0%nat))))
+          (e_ite Tlong (Ccompu0 Cne) (e_xorw (e_is_negl (Eletvar 2%nat))
+                                            (e_is_negl (Eletvar 1%nat)))
+                 (e_negl (Eletvar 0%nat)) (Eletvar 0%nat)))).
+
+Lemma nonneg_signed_unsigned:
+  forall x (x_NONNEG : (Int64.signed x >= 0)%Z),
+    (Int64.signed x) = (Int64.unsigned x).
+Proof.
+  intros.
+  pose proof (Int64.unsigned_range x).
+  unfold Int64.signed in *.
+  destruct zlt. reflexivity.
+  change Int64.modulus with 18446744073709551616%Z in *.
+  change Int64.half_modulus with 9223372036854775808%Z in *.
+  lia.
+Qed.
+
+Lemma long_min_signed_unsigned :
+  (- Int64.min_signed < Int64.max_unsigned)%Z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma long_divs_divu :
+  forall a b
+    (b_NOT0 : (Int64.signed b <> 0)%Z),
+    Int64.divs a b = if xorb (Int64.lt a Int64.zero)
+                           (Int64.lt b Int64.zero)
+                   then Int64.neg (Int64.divu (ExtValues.long_abs a)
+                                          (ExtValues.long_abs b))
+                   else Int64.divu (ExtValues.long_abs a) (ExtValues.long_abs b).
+Proof.
+  intros.
+  unfold Int64.divs, Int64.divu, Int64.lt, ExtValues.long_abs.
+  pose proof (Int64.signed_range a) as a_RANGE.
+  pose proof (Int64.signed_range b) as b_RANGE.
+  change (Int64.signed Int64.zero) with 0%Z.
+  destruct zlt.
+  - cbn. rewrite (Z.abs_neq (Int64.signed a)) by lia.
+    rewrite (Int64.unsigned_repr (- Int64.signed a)); cycle 1.
+    { pose proof long_min_signed_unsigned. lia. }
+
+    destruct zlt.
+    + rewrite (Z.abs_neq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof long_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int64.signed b)) at 1.
+      rewrite Z.quot_opp_r by lia.
+      rewrite <- (Z.opp_involutive (Int64.signed a)) at 1.
+      rewrite Z.quot_opp_l by lia.
+      rewrite Z.quot_div_nonneg by lia.
+      rewrite Z.opp_involutive.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof Int64.max_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int64.signed a)) at 1.
+      rewrite Z.quot_opp_l by lia.
+      rewrite Z.quot_div_nonneg by lia.
+      rewrite Int64.neg_repr.
+      reflexivity.
+    
+  - cbn. rewrite (Z.abs_eq (Int64.signed a)) by lia.
+    rewrite (Int64.unsigned_repr (Int64.signed a)); cycle 1.
+    { pose proof Int64.max_signed_unsigned. lia. }
+    destruct zlt.
+    + rewrite (Z.abs_neq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof long_min_signed_unsigned. lia. }
+      rewrite Int64.neg_repr.
+      rewrite <- (Z.opp_involutive (Int64.signed b)) at 1.
+      rewrite Z.quot_opp_r by lia.
+      rewrite Z.quot_div_nonneg by lia.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof Int64.max_signed_unsigned. lia. }
+      rewrite Z.quot_div_nonneg by lia.
+      reflexivity.
+Qed.
+
+Lemma nonzero_unsigned_signed :
+  forall b, (Int64.unsigned b > 0 -> Int64.signed b <> 0)%Z.
+Proof.
+  intros b GT EQ.
+  rewrite Int64.unsigned_signed in GT.
+  unfold Int64.lt in GT.
+  rewrite Int64.signed_zero in GT.
+  destruct zlt in GT; lia.
+Qed.
+
+Theorem fp_divs64_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_divs64 expr_a expr_b)
+            (Vlong (Int64.divs a b)).
+Proof.
+  intros.
+  unfold fp_divs64.
+  Local Opaque fp_divu64.
+  repeat (econstructor + apply eval_lift + eassumption).
+  apply fp_divu64_correct.
+  all: repeat (econstructor + apply eval_lift + eassumption).
+  { unfold ExtValues.long_absdiff, ExtValues.Z_abs_diff.
+    rewrite Int64.signed_zero. rewrite Z.sub_0_r.
+    rewrite Int64.unsigned_repr.
+    { pose proof (nonzero_unsigned_signed b b_nz).
+      lia.
+    }
+    pose proof Int64.max_signed_unsigned.
+    pose proof long_min_signed_unsigned.
+    pose proof (Int64.signed_range b).
+    lia.
+  }
+  cbn.
+  rewrite long_divs_divu ; cycle 1.
+  { apply nonzero_unsigned_signed. assumption. }
+  unfold Int64.lt, ExtValues.long_abs, ExtValues.long_absdiff, ExtValues.Z_abs_diff.
+  change (Int64.signed Int64.zero) with 0%Z.
+  repeat rewrite Z.sub_0_r.
+  destruct zlt; destruct zlt; reflexivity.
+Qed.
+
+Lemma long_mods_modu :
+  forall a b
+    (b_NOT0 : (Int64.signed b <> 0)%Z),
+    Int64.mods a b = if Int64.lt a Int64.zero
+                   then Int64.neg (Int64.modu (ExtValues.long_abs a)
+                                          (ExtValues.long_abs b))
+                   else Int64.modu (ExtValues.long_abs a) (ExtValues.long_abs b).
+Proof.
+  intros.
+  unfold Int64.mods, Int64.modu, Int64.lt, ExtValues.long_abs.
+  pose proof (Int64.signed_range a) as a_RANGE.
+  pose proof (Int64.signed_range b) as b_RANGE.
+  change (Int64.signed Int64.zero) with 0%Z.
+  destruct zlt.
+  - cbn. rewrite (Z.abs_neq (Int64.signed a)) by lia.
+    rewrite (Int64.unsigned_repr (- Int64.signed a)); cycle 1.
+    { pose proof long_min_signed_unsigned. lia. }
+
+    destruct (zlt (Int64.signed b) 0%Z).
+    + rewrite (Z.abs_neq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof long_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int64.signed b)) at 1.
+      rewrite Z.rem_opp_r by lia.
+      rewrite <- (Z.opp_involutive (Int64.signed a)) at 1.
+      rewrite Z.rem_opp_l by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      rewrite Int64.neg_repr.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof Int64.max_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int64.signed a)) at 1.
+      rewrite Z.rem_opp_l by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      rewrite Int64.neg_repr.
+      reflexivity.
+    
+  - cbn. rewrite (Z.abs_eq (Int64.signed a)) by lia.
+    rewrite (Int64.unsigned_repr (Int64.signed a)); cycle 1.
+    { pose proof Int64.max_signed_unsigned. lia. }
+    destruct (zlt (Int64.signed b) 0%Z).
+    + rewrite (Z.abs_neq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof long_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int64.signed b)) at 1.
+      rewrite Z.rem_opp_r by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int64.signed b)) by lia.
+      rewrite Int64.unsigned_repr ; cycle 1.
+      { pose proof Int64.max_signed_unsigned. lia. }
+      rewrite Z.rem_mod_nonneg by lia.
+      reflexivity.
+Qed.
+
+Definition fp_mods64 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 :
+  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.
+  unfold fp_mods64.
+  Local Opaque fp_modu64.
+  repeat (econstructor + apply eval_lift + eassumption).
+  apply fp_modu64_correct.
+  all: repeat (econstructor + apply eval_lift + eassumption).
+  { unfold ExtValues.long_absdiff, ExtValues.Z_abs_diff.
+    rewrite Int64.signed_zero. rewrite Z.sub_0_r.
+    rewrite Int64.unsigned_repr.
+    { pose proof (nonzero_unsigned_signed b b_nz).
+      lia.
+    }
+    pose proof Int64.max_signed_unsigned.
+    pose proof long_min_signed_unsigned.
+    pose proof (Int64.signed_range b).
+    lia.
+  }
+  cbn.
+  rewrite long_mods_modu ; cycle 1.
+  { apply nonzero_unsigned_signed. assumption. }
+  unfold Int64.lt, ExtValues.long_abs, ExtValues.long_absdiff, ExtValues.Z_abs_diff.
+  change (Int64.signed Int64.zero) with 0%Z.
+  repeat rewrite Z.sub_0_r.
+  destruct zlt; reflexivity. 
+Qed.