diff options
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 17 |
1 files changed, 17 insertions, 0 deletions
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. |