Fix warnings and documentation for "at-most" constructs

doc/3d-lang.rst

@@ -374,8 +374,10 @@ A variation is:
 
 * ``T f[:byte-size-single-element-array-at-most n]``
 
-similar to the previous form, but where ``n`` is an upper bound on the
-size in bytes.
+which describes a field ``f`` that contains a single element of type
+``T`` occupying at most ``n`` bytes, followed by padding bytes to make
+up to ``n`` bytes. This construct thus always consumes exactly ``n``
+bytes.
 
 We expect to add several other kinds of variable-length array-like
 types in the uture.

src/3d/Ast.fst

@@ -457,7 +457,7 @@ let field_bitwidth_t = either (with_meta_t int) bitfield_attr
 type array_qualifier =
   | ByteArrayByteSize  //[
   | ArrayByteSize      //[:byte-size
-  | ArrayByteSizeAtMost //[:byte-size-at-most
+  | ArrayByteSizeAtMost //[:byte-size-single-element-array-at-most
   | ArrayByteSizeSingleElementArray //[:byte-size-single-element-array
 
 [@@ PpxDerivingYoJson ]
@@ -1114,11 +1114,11 @@ and print_atomic_field (f:atomic_field) : ML string =
       begin match q with
       | ByteArrayByteSize -> Printf.sprintf "[%s]" (print_expr e)
       | ArrayByteSize -> Printf.sprintf "[:byte-size %s]" (print_expr e)
-      | ArrayByteSizeAtMost -> Printf.sprintf "[:byte-size-at-most %s]" (print_expr e)
+      | ArrayByteSizeAtMost -> Printf.sprintf "[:byte-size-single-element-array-at-most %s]" (print_expr e)
       | ArrayByteSizeSingleElementArray -> Printf.sprintf "[:byte-size-single-element-array %s]" (print_expr e)
       end
     | FieldString None -> Printf.sprintf "[::zeroterm]"
-    | FieldString (Some sz) -> Printf.sprintf "[:zeroterm-b-te-size-at-most %s]" (print_expr sz)
+    | FieldString (Some sz) -> Printf.sprintf "[:zeroterm-byte-size-at-most %s]" (print_expr sz)
     | FieldConsumeAll -> Printf.sprintf "[:consume-all]"
   in
   let sf = f.v in

src/3d/TypeSizes.fst

@@ -169,7 +169,7 @@ let size_and_alignment_of_atomic_field (env:env_t) (f:atomic_field)
 
       | FieldArrayQualified (n, ByteArrayByteSize) ->
         if base_size <> Fixed 1
-        then warning "Expected a byte array; if the underlying array elements are larger than a byte, use the '[:byte-size' notation"
+        then error "Expected a byte array; if the underlying array elements are larger than a byte, use the '[:byte-size' notation"
                      f.range;
         let n = value_of_const_expr env n in
         begin

src/3d/ocaml/lexer.mll

@@ -153,7 +153,7 @@ rule token =
   | "]"                          { locate lexbuf RBRACK }
   | "[="           { deprecation_warning lexbuf "[:byte-size-single-element-array";
                      locate lexbuf LBRACK_EQ }
-  | "[<="          { deprecation_warning lexbuf "[:byte-size-at-most";
+  | "[<="          { deprecation_warning lexbuf "[:byte-size-single-element-array-at-most";
                      locate lexbuf LBRACK_LEQ }
   | "*"            { locate lexbuf STAR }
   | "/"            { locate lexbuf DIV }