Add full constraints for vector updates

Also fix a test with an insufficient constraint

2 files changed, 6 insertions, 6 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