diff options
| -rw-r--r-- | mips/mips_extras.v | 10 | ||||
| -rw-r--r-- | mips/prelude.sail | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/mips/mips_extras.v b/mips/mips_extras.v index b9dd6138..94e4779c 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -138,6 +138,16 @@ Definition eq_bit (x : bitU) (y : bitU) : bool := | _,_ => false end. +Require Import Zeuclid. +Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. +refine (build_ex (ZEuclid.modulo m n)). +constructor. +destruct H. +assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. } +rewrite <- H at 3. +lapply (ZEuclid.mod_always_pos m n); omega. +Qed. + (* Override the more general version *) Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. diff --git a/mips/prelude.sail b/mips/prelude.sail index c411ad83..b3349799 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -104,7 +104,7 @@ overload operator / = {quotient_nat, quotient} val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) +val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) overload operator % = {modulus} |