From 1308bdc1fd4785e37f00e4436b2cd9f4c8e8fad7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 29 May 2019 19:09:45 +0100
Subject: Coq: need a proof for _shr32

---
 lib/arith.sail         |  2 +-
 lib/coq/Sail2_values.v | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)

(limited to 'lib')

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.  
-- 
cgit v1.2.3