Growing, shrinking or freeing a container reached through a [const T] is refused, and a function that only reads a slice stands where one that may write it is wanted

lib/check.ml

@@ -2192,8 +2192,57 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
    crosses as ptr+len like any other. *)
 let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
 
+(* The read-only slice a value's storage is reached through, if there is one:
+   an element of a [[const T]], a field of such an element, or an element of
+   an array that is. The last slice stepped through decides, because the
+   const is shallow — an element of a [[const [u8]]] is itself a writable
+   [[u8]], and what it views is not the outer slice's to protect. *)
+let rec const_reached (e : Tast.expr) =
+  match e.Tast.e with
+  | Tast.Prim (Tast.At, target :: idx) ->
+    const_steps (const_reached target) target.Tast.ty (List.length idx)
+  | Tast.Field (target, _) -> const_reached target
+  | _ -> None
+
+(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
+and const_steps ro (ty : Types.t) n =
+  if n = 0 then ro
+  else
+    match ty with
+    | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1)
+    | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1)
+    | Types.Array (_, t) -> const_steps ro t (n - 1)
+    | _ -> ro
+
+(* A store, or an [addr], through a read-only view. *)
+let refuse_const_place loc (view : Types.t) =
+  let elem = match view with Types.Slice (_, t) -> t | t -> t in
+  Loc.failk "check/store-through-const" loc
+    "this writes through a %s, which can only be read, so the element is a \
+     value and not a place. Write into a slice that can be written: \
+     (slice (into v (vec-new %s))) copies v's elements into one"
+    (Types.to_string view) (Types.to_string elem)
+
+(* The runtime entry points that change a Vec or a Map, which the backends
+   hand the container's address. An element of a [[const (Vec T)]], or a field
+   reached through one, is storage the view may not write, so growing,
+   shrinking or freeing it there is the same store [check_place] refuses —
+   made through the header instead of through a [set]. Writing into the
+   Vec's own buffer is not refused: the const is shallow, and the buffer is
+   not the slice's storage. *)
+let changes_container = function
+  | "flan_vec_push" | "flan_vec_reserve" | "flan_vec_free"
+  | "flan_map_put" | "flan_map_remove" | "flan_map_reserve" | "flan_map_free" ->
+    true
+  | _ -> false
+
 (* A runtime call, with the result type spelled at the site. *)
-let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
+let rt loc ty sym args =
+  (if changes_container sym then
+     match args with
+     | target :: _ -> Option.iter (refuse_const_place loc) (const_reached target)
+     | [] -> ());
+  mk loc ty (Tast.Prim (Tast.Rt sym, args))
 
 (* ── The allocation registry's note ──────────────────────────────────
 
@@ -3093,8 +3142,13 @@ let expect ctx loc ~want (got : Tast.expr) =
          [CFn] has nowhere to put one — so the reverse falls through to the
          ordinary refusal, which names both types and is the right sentence. *)
       | Types.Fn (ps, r), Types.CFn (ps', r')
-        when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) ->
+        when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) ->
         mk loc w (Tast.Thicken (thick_thunk ctx.env loc ps r, got))
+      (* The same signature up to const, which [Types.fn_accepts] defines. *)
+      | Types.Fn (ps, r), Types.Fn (ps', r')
+      | Types.CFn (ps, r), Types.CFn (ps', r')
+        when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) ->
+        { got with Tast.ty = w }
       (* A writable view seen as a read-only one. The two are the same two
          words, so the value is only retyped; the reverse is refused below,
          with [const_note] naming the copy that would make it writable. *)
@@ -6448,37 +6502,6 @@ and refuse_string_place loc (ty : Types.t) =
       "a string is read-only, so (at s i) is a value and not a place. Copy \
        the bytes into a buffer you own and write that"
 
-(* The read-only slice a value's storage is reached through, if there is one:
-   an element of a [[const T]], a field of such an element, or an element of
-   an array that is. The last slice stepped through decides, because the
-   const is shallow — an element of a [[const [u8]]] is itself a writable
-   [[u8]], and what it views is not the outer slice's to protect. *)
-and const_reached (e : Tast.expr) =
-  match e.Tast.e with
-  | Tast.Prim (Tast.At, target :: idx) ->
-    const_steps (const_reached target) target.Tast.ty (List.length idx)
-  | Tast.Field (target, _) -> const_reached target
-  | _ -> None
-
-(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
-and const_steps ro (ty : Types.t) n =
-  if n = 0 then ro
-  else
-    match ty with
-    | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1)
-    | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1)
-    | Types.Array (_, t) -> const_steps ro t (n - 1)
-    | _ -> ro
-
-(* A store, or an [addr], through a read-only view. *)
-and refuse_const_place loc (view : Types.t) =
-  let elem = match view with Types.Slice (_, t) -> t | t -> t in
-  Loc.failk "check/store-through-const" loc
-    "this writes through a %s, which can only be read, so the element is a \
-     value and not a place. Write into a slice that can be written: \
-     (slice (into v (vec-new %s))) copies v's elements into one"
-    (Types.to_string view) (Types.to_string elem)
-
 (* [store] is false for [addr] alone. A (Ptr T) is the C boundary, where the
    program is already trusted — [slice-from-ptr] and [declare-c] take its word
    — and a [[const u8]] handed to a C function that takes a [const T *] has no

lib/types.ml

@@ -346,3 +346,16 @@ let rec const_widens ~(from : t) ~(into : t) =
   match from, into with
   | Slice (_, a), Slice (Const, b) -> equal a b || const_widens ~from:a ~into:b
   | _ -> false
+
+(* A function of one signature standing where another is wanted, when the
+   two differ only in const. A parameter may be more permissive than asked —
+   a function that takes a [[const T]] only reads what it is handed, so a
+   caller handing it a [[T]] loses nothing — and a result may be less so: a
+   [[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
+   two words are the same either way, so [Check.expect] only retypes. *)
+let fn_accepts ~(from : t list * t) ~(into : t list * t) =
+  let ps', r' = from and ps, r = into in
+  List.length ps = List.length ps'
+  && List.for_all2
+       (fun p p' -> equal p p' || const_widens ~from:p ~into:p') ps ps'
+  && (equal r r' || const_widens ~from:r' ~into:r)

test/programs/const-slice.flan

@@ -18,6 +18,14 @@
       (set n (+ n (length (at parts i)))))
     n))
 
+;; A function that only reads stands where one that may write is wanted, and
+;; one returning a writable slice where a read-only one is wanted.
+(defn rd [s [const u8]] i32 (length s))
+(defn call-rd [f (Fn [[u8]] i32)] i32 (f (bytes "abc")))
+(defn call-bare [f (CFn [[u8]] i32)] i32 (f (bytes "abcd")))
+(defn mk [] [u8] (bytes "xy"))
+(defn call-mk [f (Fn [] [const u8])] i32 (length (f)))
+
 (defn main [] i32
   (let [xs [3 1 2]
         w (slice xs)
@@ -45,5 +53,6 @@
       (sort-bytes (slice f))
       (println (string (slice (join (slice f) (bytes-view "-"))))))
     (println (at r 0))
+    (println (call-rd rd) (call-bare rd) (call-mk mk))
     (free names))
   0)

test/test_acceptance.ml

@@ -872,7 +872,7 @@ let () =
     (* [const T]: the checker's alone, so the three builds agree and every
        row is about which values reach which parameters. *)
     let const_slice_out =
-      "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n"
+      "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n"
     in
     outputs "const slices" "programs/const-slice.flan" const_slice_out;
     outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"

test/test_flan.ml

@@ -2291,6 +2291,37 @@ let () =
   rejects_check "no conversion under a writable slice"
     "(defn g [p [[const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))"
     ~needle:"expected [[const u8]], found [[u8]]";
+  rejects_check "push through a const slice of Vecs"
+    "(defn f [s [const (Vec i32)]] () (push (at s 0) 5))"
+    ~needle:"this writes through a [const (Vec i32)]";
+  rejects_check "put through a const slice of maps"
+    "(defn f [s [const (Map string i32)]] () (put (at s 0) \"a\" 5))"
+    ~needle:"this writes through a [const (Map string i32)]";
+  rejects_check "map-remove through a const slice of maps"
+    "(defn f [s [const (Map string i32)]] bool (map-remove (at s 0) \"a\"))"
+    ~needle:"this writes through a [const (Map string i32)]";
+  rejects_check "reserve through a const slice of Vecs"
+    "(defn f [s [const (Vec i32)]] () (reserve (at s 0) 10))"
+    ~needle:"this writes through a [const (Vec i32)]";
+  rejects_check "free through a const slice of Vecs"
+    "(defn f [s [const (Vec i32)]] () (free (at s 0)))"
+    ~needle:"this writes through a [const (Vec i32)]";
+  rejects_check "push into a field reached through a const slice"
+    "(defstruct P [v (Vec i32)]) (defn f [s [const P]] () (push (.v (at s 0)) 1))"
+    ~needle:"this writes through a [const P]";
+  accepts "a Vec's own buffer is not the const slice's storage"
+    "(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))";
+  accepts "a reading function where a writing one is wanted"
+    "(defn rd [s [const u8]] i32 0) (defn c [f (Fn [[u8]] i32)] i32 0) \
+     (defn m [] i32 (c rd))";
+  rejects_check "not a writing function where a reading one is wanted"
+    "(defn wr [s [u8]] i32 0) (defn c [f (Fn [[const u8]] i32)] i32 0) \
+     (defn m [] i32 (c wr))"
+    ~needle:"expected (Fn [[const u8]] i32), found (CFn [[u8]] i32)";
+  rejects_check "nor a read-only result where a writable one is wanted"
+    "(defn mk [] [const u8] (bytes-view \"a\")) \
+     (defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))"
+    ~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])";
   rejects_check "const is not a name a constant can have"
     "(defconst const 4)" ~needle:"const cannot be declared";
   (* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)