diff options
| -rw-r--r-- | kvx/FPDivision64.v | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 38eb6c1b..2c6a49c5 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2320,3 +2320,39 @@ Proof. rewrite Int64.repr_unsigned. reflexivity. Qed. + +Open Scope cminorsel_scope. +Definition e_invfs a := Eop Oinvfs (a ::: Enil). +Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil). +Definition e_single_of_longu a := Eop Osingleoflongu (a ::: Enil). +Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil). +Definition e_longu_of_float_ne a := Eop Olonguoffloat_ne (a ::: Enil). +Definition e_mulf a b := Eop Omulf (a ::: b ::: Enil). + +Definition a_var1 := Eletvar (4%nat). +Definition a_d_var1 := Eletvar (3%nat). +Definition b_var1 := Eletvar (2%nat). +Definition b_d_var1 := Eletvar (1%nat). +Definition binv_d_var1 := Eletvar (0%nat). + +Definition e_setup1 a b rest := + Elet a (Elet (e_float_of_longu (Eletvar 0%nat)) + (Elet (lift (lift b)) (Elet (e_float_of_longu (Eletvar 0%nat)) + (Elet (e_float_of_single (e_invfs (e_single_of_longu (Eletvar 1%nat)))) + rest)))). +Definition e_step1 := e_longu_of_float_ne (e_mulf a_d_var1 binv_d_var1). + +Lemma e_step1_correct : + forall (ge : genv) (sp: val) cmenv memenv (le : letenv) + (expr_a : expr) (a : int64) (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vlong a)) + (expr_b : expr) (b : int64) (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vlong b)), + (eval_expr ge sp cmenv memenv le (e_setup1 expr_a expr_b (e_step1)) + (step1_div_longu (Vlong a) (Vlong b))). +Proof. + intros. + unfold e_setup1, step1_div_longu. + repeat econstructor. + { eassumption. } + { cbn. apply eval_lift. apply eval_lift. eassumption. } +Qed. + |