diff options
| author | Brian Campbell | 2019-04-16 17:11:53 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-16 17:47:36 +0100 |
| commit | 41d2b4fec5e904b6a1d336ceed0adf4474d90279 (patch) | |
| tree | d36affa7380e362b271bff24128eef41faed0690 /lib | |
| parent | 70c1ab20b8b5539f4efedff84bea68f7683d1aec (diff) | |
Coq: add specialised shifts
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 17 |
2 files changed, 19 insertions, 2 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 6ddc58aa..af814c81 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size)) ``` THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` */ -val _shl8 = {c: "shl_mach_int", _: "shl_int"} : +val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} : forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)} /*! Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` */ -val _shl32 = {c: "shl_mach_int", _: "shl_int"} : +val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} : forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)} val _shl_int = "shl_int" : (int, int) -> int 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. |