From 14d1a795f3ab054374c4fbe8f25c2a388047f2bc Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 14 Feb 2022 20:40:21 +0100
Subject: fp_divs32_correct

---
 kvx/FPDivision32.v | 137 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 137 insertions(+)

(limited to 'kvx')

diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v
index c920d22a..edbcbe12 100644
--- a/kvx/FPDivision32.v
+++ b/kvx/FPDivision32.v
@@ -616,3 +616,140 @@ Proof.
   rewrite Int.mul_commut.
   reflexivity.
 Qed.
+
+Definition e_is_neg a := Eop (Ocmp (Ccompimm Clt Int.zero)) (a ::: Enil).
+Definition e_xorw a b := Eop Oxor (a ::: b ::: Enil).
+Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
+Definition e_neg a := Eop Oneg (a ::: Enil).
+Definition e_abs a := Eop (Oabsdiffimm Int.zero) (a ::: Enil).
+
+Definition fp_divs32 a b :=
+  Elet a (Elet (lift b)
+    (Elet (fp_divu32 (e_abs (Eletvar (1%nat))) (e_abs (Eletvar (0%nat))))
+          (e_ite Tint (Ccompu0 Cne) (e_xorw (e_is_neg (Eletvar 2%nat))
+                                            (e_is_neg (Eletvar 1%nat)))
+                 (e_neg (Eletvar 0%nat)) (Eletvar 0%nat)))).
+
+Lemma nonneg_signed_unsigned:
+  forall x (x_NONNEG : Int.signed x >= 0),
+    (Int.signed x) = (Int.unsigned x).
+Proof.
+  intros.
+  pose proof (Int.unsigned_range x).
+  unfold Int.signed in *.
+  destruct zlt. reflexivity.
+  change Int.modulus with 4294967296%Z in *.
+  change Int.half_modulus with 2147483648%Z in *.
+  lia.
+Qed.
+
+Lemma int_min_signed_unsigned :
+  (- Int.min_signed < Int.max_unsigned)%Z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma int_divs_divu :
+  forall a b
+    (b_NOT0 : Int.signed b <> 0),
+    Int.divs a b = if xorb (Int.lt a Int.zero)
+                           (Int.lt b Int.zero)
+                   then Int.neg (Int.divu (ExtValues.int_abs a)
+                                          (ExtValues.int_abs b))
+                   else Int.divu (ExtValues.int_abs a) (ExtValues.int_abs b).
+Proof.
+  intros.
+  unfold Int.divs, Int.divu, Int.lt, ExtValues.int_abs.
+  pose proof (Int.signed_range a) as a_RANGE.
+  pose proof (Int.signed_range b) as b_RANGE.
+  change (Int.signed Int.zero) with 0%Z.
+  destruct zlt.
+  - cbn. rewrite (Z.abs_neq (Int.signed a)) by lia.
+    rewrite (Int.unsigned_repr (- Int.signed a)); cycle 1.
+    { pose proof int_min_signed_unsigned. lia. }
+
+    destruct zlt.
+    + rewrite (Z.abs_neq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof int_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int.signed b)) at 1.
+      rewrite Z.quot_opp_r by lia.
+      rewrite <- (Z.opp_involutive (Int.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 (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof Int.max_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int.signed a)) at 1.
+      rewrite Z.quot_opp_l by lia.
+      rewrite Z.quot_div_nonneg by lia.
+      rewrite Int.neg_repr.
+      reflexivity.
+    
+  - cbn. rewrite (Z.abs_eq (Int.signed a)) by lia.
+    rewrite (Int.unsigned_repr (Int.signed a)); cycle 1.
+    { pose proof Int.max_signed_unsigned. lia. }
+    destruct zlt.
+    + rewrite (Z.abs_neq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof int_min_signed_unsigned. lia. }
+      rewrite Int.neg_repr.
+      rewrite <- (Z.opp_involutive (Int.signed b)) at 1.
+      rewrite Z.quot_opp_r by lia.
+      rewrite Z.quot_div_nonneg by lia.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof Int.max_signed_unsigned. lia. }
+      rewrite Z.quot_div_nonneg by lia.
+      reflexivity.
+Qed.
+
+Lemma nonzero_unsigned_signed :
+  forall b, Int.unsigned b > 0 -> Int.signed b <> 0.
+Proof.
+  intros b GT EQ.
+  rewrite Int.unsigned_signed in GT.
+  unfold Int.lt in GT.
+  rewrite Int.signed_zero in GT.
+  destruct zlt in GT; lia.
+Qed.
+
+Theorem fp_divs32_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_divs32 expr_a expr_b)
+            (Vint (Int.divs a b)).
+Proof.
+  intros.
+  unfold fp_divs32.
+  Local Opaque fp_divu32.
+  repeat (econstructor + apply eval_lift + eassumption).
+  apply fp_divu32_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_divs_divu ; 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; destruct zlt; reflexivity.
+Qed.
-- 
cgit