begin work on fp division

1 files changed, 43 insertions, 0 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
new file mode 100644
index 00000000..7fae685f
--- /dev/null
+++ b/kvx/FPDivision.v
@@ -0,0 +1,43 @@
+Require Archi.
+Require Import Coqlib.
+Require Import Compopts.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Op.
+Require Import CminorSel.
+Require Import OpHelpers.
+Require Import ExtValues ExtFloats.
+Require Import DecBoolOps.
+Require Import Chunks.
+Require Import Builtins.
+Require Import Values Globalenvs.
+Require Compopts.
+
+Local Open Scope cminorsel_scope.
+
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Definition approx_inv b :=
+  let invb_s := Eop Oinvfs ((Eop Osingleofintu ((Eletvar 0%nat):::Enil)):::Enil) in
+  let invb_d := Eop Ofloatofsingle (invb_s ::: Enil) in
+  let b_d := Eop Ofloatoflongu ((Eop Ocast32unsigned ((Eletvar 1%nat):::Enil)):::Enil) in
+  let invb_d_var := Eletvar (0%nat) in
+  let one := Eop (Ofloatconst ExtFloat.one) Enil in
+  let alpha := Eop Ofmsubf (one ::: invb_d_var ::: b_d ::: Enil) in
+  let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in
+  Elet b (Elet invb_d x).
+
+Theorem approx_inv_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv
+         (le : letenv) (expr_b : expr) b
+         (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)),
+    eval_expr ge sp cmenv memenv le (approx_inv expr_b)
+              (Vfloat ExtFloat.one).
+Proof.
+  intros. unfold approx_inv.
+  repeat econstructor.
+  { eassumption. }
+  cbn.
+Abort.