diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-10 22:48:26 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-10 22:48:26 +0100 |
| commit | b45d9ac4b98ed9ce095a1ad64a4192fea89f7b5f (patch) | |
| tree | 3fcf0320de8dfb46ba275178b45db57d1854869b /kvx | |
| parent | 6bd3c44a582d3d1f23fe4ed99dec8b59893e3a85 (diff) | |
| download | compcert-kvx-b45d9ac4b98ed9ce095a1ad64a4192fea89f7b5f.tar.gz compcert-kvx-b45d9ac4b98ed9ce095a1ad64a4192fea89f7b5f.zip | |
fp_divu64_correct
Diffstat (limited to 'kvx')
| -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. |