Enforce that bitvectors have non-negative indices always

This requires some refactoring to the typing context, so now we always
check that unexpanded types are well-formed.

CHANGELOG.md

@@ -1,6 +1,27 @@
 Changelog
 =========
 
+Sail 0.19
+---------
+
+##### Stricter bitvector type indexing
+
+Stricter indexing for bitvector types. Previous versions of Sail
+treated `bitvector('n)` as uninhabited if `'n < 0`, but otherwise
+permitted such bitvector types in signatures. Now the type
+`bitvector('n)` is only well-formed if `'n >= 0`. This is a breaking
+change, as some previously permitted definitions are now rejected
+without additional constraints. However Sail has a new kind `Nat`
+which allows it to infer these `>= 0` constraints when explicit type
+variables are ommited, so in a function signature
+```
+val foo : forall 'n. bits('n) -> bool
+```
+the `'n` type variable will be inferred as:
+```
+val foo : forall ('n : Nat). bits('n) -> bool
+```
+
 Sail 0.18
 ---------
 

lib/concurrency_interface/read_write.sail

@@ -107,7 +107,7 @@ union Access_kind('arch_ak : Type) = {
 $option -lem_extern_type Mem_read_request
 $option -coq_extern_type Mem_read_request
 struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                        'arch_ak: Type), 'n > 0 = {
+                        'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   // There may not always be a virtual address, e.g. when translation is off.
   // Additionally, translate reads don't have a (VA, PA) pair in the
@@ -203,7 +203,7 @@ with
 $option -lem_extern_type Mem_write_request
 $option -coq_extern_type Mem_write_request
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                         'arch_ak : Type), 'n > 0 = {
+                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   va : option(bits('vasize)),
   pa : 'pa,

lib/vector.sail

@@ -74,7 +74,7 @@ $endif
 
 $include <flow.sail>
 
-type bits('n : Int) = bitvector('n)
+type bits('n) = bitvector('n)
 
 val eq_bits = pure {
   ocaml: "eq_list",
@@ -150,7 +150,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail
 
 overload operator ^ = {sail_mask}
 
-val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall 'n 'm.
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -337,7 +337,7 @@ val slice = pure "slice_inc" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm.
   (bits('m), int('o), int('n)) -> bits('n)
 $endif
 
-val replicate_bits = pure "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
+val replicate_bits = pure "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), int('m)) -> bits('n * 'm)
 
 val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n)
 function slice_mask(n,i,l) =

src/lib/ast_util.ml

@@ -809,6 +809,12 @@ let quant_map_items f = function
   | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
   | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
 
+let quant_fold_map_items f acc = function
+  | TypQ_aux (TypQ_no_forall, l) -> (acc, TypQ_aux (TypQ_no_forall, l))
+  | TypQ_aux (TypQ_tq qis, l) ->
+      let acc, qis = Util.fold_left_map f acc qis in
+      (acc, TypQ_aux (TypQ_tq qis, l))
+
 let is_quant_kopt = function QI_aux (QI_id _, _) -> true | _ -> false
 
 let is_quant_constraint = function QI_aux (QI_constraint _, _) -> true | _ -> false

src/lib/ast_util.mli

@@ -435,6 +435,7 @@ val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
 val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
+val quant_fold_map_items : ('acc -> quant_item -> 'acc * quant_item) -> 'acc -> typquant -> 'acc * typquant
 
 val is_quant_kopt : quant_item -> bool
 val is_quant_constraint : quant_item -> bool

src/lib/chunk_ast.ml

@@ -481,7 +481,7 @@ let pop_trailing_comment ?space:(n = 0) comments chunks line_num =
     end
 
 let string_of_kind (K_aux (k, _)) =
-  match k with K_type -> "Type" | K_int -> "Int" | K_order -> "Order" | K_bool -> "Bool"
+  match k with K_type -> "Type" | K_int -> "Int" | K_nat -> "Nat" | K_order -> "Order" | K_bool -> "Bool"
 
 (* Right now, let's just assume we never break up kinded-identifiers *)
 let chunk_of_kopt (KOpt_aux (KOpt_kind (special, vars, kind, _), l)) =