diff options
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 186 |
1 files changed, 186 insertions, 0 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 4ddf6ece..19393091 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1935,6 +1935,8 @@ Proof. constructor. Qed. +Require FPDivision32. + Theorem eval_platform_builtin: forall bf al a vl v le, platform_builtin bf al = Some a -> @@ -1948,6 +1950,190 @@ Proof. repeat (try econstructor; try eassumption)). - apply eval_fma; assumption. - apply eval_fmaf; assumption. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + cbn; rewrite H0; reflexivity. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + 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. + - 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 Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.divu i i0)). split. + { + apply FPDivision64.fp_divu64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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.modu i i0)). split. + { + apply FPDivision32.fp_modu32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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 Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.modu i i0)). split. + { + apply FPDivision64.fp_modu64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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.divs i i0)). split. + { + apply FPDivision32.fp_divs32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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 Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.divs i i0)). split. + { + apply FPDivision64.fp_divs64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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.mods i i0)). split. + { + apply FPDivision32.fp_mods32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - 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 Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.mods i i0)). split. + { + apply FPDivision64.fp_mods64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. - apply eval_abs; assumption. - apply eval_absl; assumption. Qed. |