diff options
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/Asmgenproof1.v | 16 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 5 |
2 files changed, 11 insertions, 10 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 7f070c12..98d5bd33 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -16,7 +16,7 @@ (* *********************************************************************) Require Import Coqlib Errors Maps. -Require Import AST Integers Floats Values Memory Globalenvs. +Require Import AST Zbits Integers Floats Values Memory Globalenvs. Require Import Op Locations Mach Conventions. Require Import Asm Asmgen Asmgenproof0. @@ -33,16 +33,16 @@ Proof. predSpec Int.eq Int.eq_spec n lo. - auto. - set (m := Int.sub n lo). - assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). - assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0). + assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). + assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0). { replace 0 with (Int.unsigned n - Int.unsigned n) by omega. - auto using Int.eqmod_sub, Int.eqmod_refl. } - assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0). - { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto. - apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + auto using eqmod_sub, eqmod_refl. } + assert (C: eqmod (two_p 12) (Int.unsigned m) 0). + { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto. + apply eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. exists (two_p (32-12)); auto. } assert (D: Int.modu m (Int.repr 4096) = Int.zero). - { apply Int.eqmod_mod_eq in C. unfold Int.modu. + { apply eqmod_mod_eq in C. unfold Int.modu. change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. reflexivity. apply two_p_gt_ZERO; omega. } diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 90f077db..d12bd8af 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -20,6 +20,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Zbits. Require Import Integers. Require Import Floats. Require Import Values. @@ -372,7 +373,7 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)). - unfold Int.mulhs; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. assert (N1: 0 <= n < 64) by omega. @@ -400,7 +401,7 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)). - unfold Int.mulhu; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. assert (N1: 0 <= n < 64) by omega. |