diff options
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 35 |
1 files changed, 31 insertions, 4 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 113bf07a..298831a0 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2601,23 +2601,23 @@ Proof. reflexivity. Qed. -Definition fp_mods64 a b := +Definition fp_mods64z a b := Elet a (Elet (lift b) (Elet (fp_modu64 (e_absl (Eletvar (1%nat))) (e_absl (Eletvar (0%nat)))) (e_ite Tlong (Ccompl0 Clt) (Eletvar 2%nat) (e_negl (Eletvar 0%nat)) (Eletvar 0%nat)))). -Theorem fp_mods64_correct : +Theorem fp_mods64z_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_mods64 expr_a expr_b) + eval_expr ge sp cmenv memenv le (fp_mods64z expr_a expr_b) (Vlong (Int64.mods a b)). Proof. intros. - unfold fp_mods64. + unfold fp_mods64z. Local Opaque fp_modu64. repeat (econstructor + apply eval_lift + eassumption). apply fp_modu64_correct. @@ -2641,3 +2641,30 @@ Proof. repeat rewrite Z.sub_0_r. destruct zlt; reflexivity. Qed. + +Definition fp_mods64 a b := + Elet a (Elet (lift b) + (Elet (fp_divs64 (Eletvar (1%nat)) (Eletvar (0%nat))) + (e_msubl (Eletvar 2%nat) (Eletvar 1%nat) (Eletvar 0%nat)))). + +Theorem fp_mods64_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_mods64 expr_a expr_b) + (Vlong (Int64.mods a b)). +Proof. + intros. + rewrite Int64.mods_divs. + unfold fp_mods64. + Local Opaque fp_divs64. + repeat (econstructor + apply eval_lift + eassumption). + { apply fp_divs64_correct; + repeat (econstructor + apply eval_lift + eassumption). + } + cbn. + rewrite Int64.mul_commut. + reflexivity. +Qed. |