11 files changed, 84 insertions, 9 deletions

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index a4d1a0b1..6953264f 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -77,14 +77,14 @@ val bitvector_update = {
   lem: "update_vec_dec",
   coq: "update_vec_dec",
   c: "vector_update"
-} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n)
+} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n)
 
 val plain_vector_update = {
   ocaml: "update",
   lem: "update_list_dec",
   coq: "vec_update_dec",
   c: "vector_update"
-} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m), 'a) -> vector('n, dec, 'a)
 
 overload vector_update = {bitvector_update, plain_vector_update}
 
@@ -117,7 +117,7 @@ val vector_update_subrange = {
   lem: "update_subrange_vec_dec",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_dec"
-} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 // Some ARM specific builtins
 
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index 042a6324..581dded7 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -77,14 +77,14 @@ val bitvector_update = {
   lem: "update_vec_inc",
   coq: "update_vec_inc",
   c: "vector_update"
-} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n)
+} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n)
 
 val plain_vector_update = {
   ocaml: "update",
   lem: "update_list_inc",
   coq: "update_list_inc",
   c: "vector_update"
-} : forall 'n ('a : Type). (vector('n, inc, 'a), int, 'a) -> vector('n, inc, 'a)
+} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, inc, 'a), atom('m), 'a) -> vector('n, inc, 'a)
 
 overload vector_update = {bitvector_update, plain_vector_update}
 
@@ -113,7 +113,7 @@ val vector_update_subrange = {
   lem: "update_subrange_vec_inc",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_inc"
-} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+} : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 // Some ARM specific builtins
 
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index 1e1f391c..d0a14586 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -52,7 +52,7 @@ val slice_slice : forall 'n 'm 'o 'p, 0 <= 'p <= 'm <= 'o & 'o - 'p < 'n.
 function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
 
 /* We can update a bitvector from another bitvector or a slice */
-val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice (v, stop, start, update) = {
@@ -61,7 +61,7 @@ function _set_slice (v, stop, start, update) = {
   (*v) = v2;
 }
 
-val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n.
+val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
index 078e266b..21911b15 100644
--- a/test/typecheck/pass/vec_length.sail
+++ b/test/typecheck/pass/vec_length.sail
@@ -4,5 +4,6 @@ $include <vector_dec.sail>
 function main () : unit -> unit = {
   let x : bits(8) = 0xff;
   let y = x[3];
+  let z = [x with 5 = y];
   ()
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
new file mode 100644
index 00000000..7ce8fd99
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1_inc.sail b/test/typecheck/pass/vec_length/v1_inc.sail
new file mode 100644
index 00000000..b72738d1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.sail
@@ -0,0 +1,8 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
new file mode 100644
index 00000000..d123cabd
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2.sail b/test/typecheck/pass/vec_length/v2.sail
new file mode 100644
index 00000000..4df62e81
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
new file mode 100644
index 00000000..e7d2b52f
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2_inc.sail b/test/typecheck/pass/vec_length/v2_inc.sail
new file mode 100644
index 00000000..3f75fee1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length_inc.sail b/test/typecheck/pass/vec_length_inc.sail
new file mode 100644
index 00000000..a8dd707f
--- /dev/null
+++ b/test/typecheck/pass/vec_length_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}