diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 2 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 17 |
2 files changed, 18 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 1950080a..d04c7988 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -70,7 +70,7 @@ val _shl_int = "shl_int" : (int, int) -> int overload shl_int = {_shl8, _shl32, _shl_int} -val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} +val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} val _shr_int = "shr_int" : (int, int) -> int diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 4764cc9f..2150722c 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -2232,6 +2232,23 @@ subst; compute; auto using Build_ArithFact. Defined. +Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <= x <= 31)} `{HR:ArithFact (y = 1)}: {z : Z & ArithFact (0 <= z <= 15)}. +refine (existT _ (shr_int x y) _). +destruct HE as [HE]. +destruct HR as [HR]; +subst. +unfold shr_int. +rewrite <- Z.div2_spec. +constructor. +rewrite Z.div2_div. +specialize (Z.div_mod x 2). +specialize (Z.mod_pos_bound x 2). +generalize (Z.div x 2). +generalize (x mod 2). +intros. +nia. +Defined. + Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0. unfold shl_int. apply Z.le_ge. |