From 8c2fa417866f4c70fc5e4d17609a073e73c8ce71 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 20 Nov 2018 11:30:49 +0000
Subject: Add full constraints for vector updates Also fix a test with an
 insufficient constraint

---
 lib/vector_dec.sail | 6 +++---
 lib/vector_inc.sail | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'lib')

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