diff options
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index a374ec54..658bf0b3 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1883,6 +1883,9 @@ Proof. destruct v2; simpl; trivial. Qed. + +Require FPDivision32. + Theorem eval_platform_builtin: forall bf al a vl v le, platform_builtin bf al = Some a -> @@ -1903,7 +1906,29 @@ Proof. - cbn in *; destruct vl; trivial. destruct vl; trivial. destruct v0; try discriminate; - cbn; rewrite H0; reflexivity. + cbn; rewrite H0; reflexivity. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int.eq in EVAL. + change (Int.unsigned Int.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vint (Int.divu i i0)). split. + { + apply FPDivision32.fp_divu32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. Qed. End CMCONSTR. |