Coq: add specialised shifts

1 files changed, 17 insertions, 0 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index d1f1a768..9cff3f83 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1948,3 +1948,20 @@ Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
 Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
   build_ex (Z.max x y).
+
+Definition shl_int_8 (x y : Z) `{HE:ArithFact (x = 8)} `{HR:ArithFact (0 <= y <= 3)}: {z : Z & ArithFact (In z [8;16;32;64])}.
+refine (existT _ (shl_int x y) _).
+destruct HE as [HE].
+destruct HR as [HR].
+assert (H : y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega.
+constructor.
+intuition (subst; compute; auto).
+Defined.
+
+Definition shl_int_32 (x y : Z) `{HE:ArithFact (x = 32)} `{HR:ArithFact (In y [0;1])}: {z : Z & ArithFact (In z [32;64])}.
+refine (existT _ (shl_int x y) _).
+destruct HE as [HE].
+destruct HR as [[HR1 | [HR2 | []]]];
+subst; compute;
+auto using Build_ArithFact.
+Defined.