From b45d9ac4b98ed9ce095a1ad64a4192fea89f7b5f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 22:48:26 +0100 Subject: fp_divu64_correct --- kvx/FPDivision64.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index c08103b1..411865ba 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2528,3 +2528,20 @@ Proof. repeat f_equal. destruct (Int64.lt b Int64.zero); cbn; change (Int.eq Int.one Int.zero) with false; change (Int.eq Int.zero Int.zero) with true; cbn; reflexivity. Qed. + +Definition fp_divu64 a b := e_setup7 a b e_step7. + +Theorem fp_divu64_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_divu64 expr_a expr_b) + (Vlong (Int64.divu a b)). +Proof. + intros. + unfold Int64.divu. + rewrite <- full2_div_longu_correct with (m := memenv) by lia. + apply e_step7_correct; assumption. +Qed. -- cgit