From 2ff1da88da6b948f5827480bafbcd999a5a5d1e1 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 11:43:41 +0700 Subject: [PATCH 1/7] A slice can be read-only: bytes-view answers a [const u8], and a store through one is refused at compile time --- TODO.org | 17 +- calc-me.flan | 4 +- docs/BUILT.md | 22 +-- emacs/flan-mode.el | 6 +- emacs/test-flan-mode.el | 2 + examples/text-rectangle-bounds.flan | 2 +- lib/ast.ml | 2 +- lib/check.ml | 294 +++++++++++++++++++--------- lib/cimport.ml | 3 +- lib/emit.ml | 18 +- lib/js.ml | 4 +- lib/load.ml | 4 +- lib/parse.ml | 19 +- lib/prelude.ml | 117 +++++------ lib/render.ml | 8 +- lib/session.ml | 14 +- lib/types.ml | 34 +++- lib/x86.ml | 6 +- runtime/flan_dev.c | 2 +- spike/x86/p4-convention.flan | 2 +- spike/x86/survey.sh | 31 +-- test/programs/algorithms.flan | 2 +- test/programs/bounds-condition.flan | 2 +- test/programs/bytes-view-write.flan | 18 +- test/programs/const-slice.flan | 49 +++++ test/programs/dev-segv.flan | 15 +- test/programs/edn.flan | 4 +- test/programs/pkg-return.flan | 2 +- test/programs/utf8.flan | 4 +- test/programs/vec-new-shadow.flan | 2 +- test/programs/vec-new-type.flan | 4 +- test/test_acceptance.ml | 45 +++-- test/test_dev.ml | 9 +- test/test_flan.ml | 81 +++++++- test/test_sanitize.ml | 2 +- vendor/edn/edn.flan | 10 +- vendor/edn/provide.flan | 20 +- vendor/edn/read.flan | 4 +- vendor/json/json.flan | 10 +- vendor/json/provide.flan | 18 +- vendor/raylib/raylib.flan | 4 +- web/examples/structs.flan | 2 +- web/index.html | 10 +- 43 files changed, 581 insertions(+), 347 deletions(-) create mode 100644 test/programs/const-slice.flan diff --git a/TODO.org b/TODO.org index 081c65c5..0d77b3b9 100644 --- a/TODO.org +++ b/TODO.org @@ -944,20 +944,9 @@ blocker it was, since =(array 4 T)= answers the case that raised it. plan.org's rule is "annotate function signatures, infer locals", so a general annotation is a deliberate absence. -** NEXT A read-only slice type -Decided 2026-09-25: =[const u8]=, Zig's spelling in Flan's brackets. =bytes-view= answers one and a =set= through it is a compile error; a =[T]= converts to =[const T]= and not back, and the prelude's read-only functions take it. =const= is reserved as a name, since =[n T]= accepts a constant's name for =n=. -=bytes-view= is read-only by convention only — the type system cannot say a =[u8]= -may not be stored through, so a trap on read-only memory is the enforcement. A -read-only slice type, or provenance, is what would move that refusal to compile -time. - -** NEXT Writing through a string literal -Decided 2026-09-25: closed by the read-only slice type above. -=(let [s (bytes-view "Hi")] (set (at s 0) \h))= stores into read-only memory at -=-O0= and is deleted as undefined at =-O2= — same source, and which way it fails -depends on a flag. Narrowed when =(bytes s)= started copying, so the common -spelling no longer reaches the edge. Emitting literals as mutable globals is not a -fix: it moves which flag misbehaves and costs their read-only placement. +** DONE A read-only slice type +CLOSED: [2026-09-25] +=[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused. ** TODO (slice d 1) over a dyn string is refused where (at d i) works The typed and dyn spaces disagree about a spelling, which the standing rule diff --git a/calc-me.flan b/calc-me.flan index 0af5019c..78d66745 100644 --- a/calc-me.flan +++ b/calc-me.flan @@ -20,7 +20,7 @@ ;; ── one by pointer. `addr` takes the address of a local; the pointer never ;; ── outlives the frame, so no allocator is involved. (defstruct Cursor - [src [u8] ; non-owning slice into argv — calc-me never owns a byte + [src [const u8] ; non-owning slice into argv — calc-me never owns a byte pos i32]) ; no initialiser means zeroed (defn peek [c (Ptr Cursor)] u8 @@ -105,7 +105,7 @@ (Some lhs))) ;; ── Whole input, or nothing. Trailing junk is an error, not ignored. ── -(defn evaluate [src [u8]] (Option f64) +(defn evaluate [src [const u8]] (Option f64) (let [c (Cursor {.src src})] ; pos omitted: zeroed (let [v (some (parse-expr (addr c) 1))] (skip-spaces (addr c)) diff --git a/docs/BUILT.md b/docs/BUILT.md index 02803ee5..35e3289f 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -950,7 +950,7 @@ the only two under which a mark and a sweep run at all. `dev_segv` sits beside t program that faults cannot be compared against an unsanitized run — that build's handler parks in the break loop, and the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a weak `__asan_init` and declines to install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's -line, built at `-O0` because at `-O2` the write through a bytes-view of a literal does not fault at all. That yield had +line, built at `-O0` because at `-O2` the write through a pointer to a literal's bytes does not fault at all. That yield had never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm. What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own path and has no `--sanitize` to pass it. @@ -2794,7 +2794,7 @@ fires. | `(clone v)` / `(clone v a)` | the only copy; assignment moves | | `(free v)` | consumes its argument | | `(bytes s)` / `(bytes s a)` | a writable copy of a string's bytes, against the context or a named allocator — an allocating operation like `vec-new`: StorageExhausted with retry, a registry note in dev builds. The answer is a `[u8]` view of the block, so nothing can `free` it through the slice; it lives until its allocator's `free-all` or destroy | -| `(bytes-view s)` | the string's own storage as a `[u8]`, costing nothing — the old `(bytes s)` reinterpret, renamed. Read-only by convention: a literal's view points into `.rodata` and a store through it traps | +| `(bytes-view s)` | the string's own storage as a `[const u8]`, costing nothing — the old `(bytes s)` reinterpret, renamed. A store through it is a compile error, because a literal's view points into `.rodata` | ### A view of a `Vec` goes stale at the `push`, and nothing checks it @@ -3881,7 +3881,7 @@ held at once; these copy out of that buffer before returning, so the hazard ends many numbers as it likes. `strings.flan` puts two integers and a float on one line, which is the case that could not be written before. -### `split` answers a `(Vec [u8])`, and the owning shape is unrepresentable +### `split` answers a `(Vec [const u8])`, and the owning shape is unrepresentable The fields are slices *of the input*. That was not a performance choice when this was written: `(Vec (Vec u8))` was **refused outright**, so there was no owning shape to have chosen instead. That refusal has since been narrowed — see @@ -3895,7 +3895,7 @@ The rule is `split-on-byte`'s, unchanged: n separators always yield n+1 fields, field and a trailing separator yields a trailing empty one. That is Odin's allocating `strings.split` and not Odin's `split_by_byte_iterator`, which disagree with each other on exactly that input. -Constructing it needed a one-line `(defn slices-new [] (Vec [u8]) (vec-new))`, because `check.ml`'s `vec_new_elem` +Constructing it needed a one-line `(defn slices-new [] (Vec [const u8]) (vec-new))`, because `check.ml`'s `vec_new_elem` takes the element type as a single bare symbol and `[u8]` is not one — so a `(Vec [u8])` can only be made where the *context* names the type, and a return type is a context while a `let` is not. Written down in TODO.org, "(vec-new [u8]) is refused", as a compiler gap rather than worked around silently. @@ -4538,7 +4538,7 @@ and the rule is easier to state and to trust with one construct in it. ## Assets are baked in, and the reason it is a compiler feature -TODO.org, "Assets are embedded at compile time". `(embed "brush.png")` is a `[u8]`, `(embed "brush.png" string)` is a `string`, and +TODO.org, "Assets are embedded at compile time". `(embed "brush.png")` is a `[const u8]`, `(embed "brush.png" string)` is a `string`, and `(embed-dir "assets")` is a `[n EmbedFile]` sorted by name. Odin's `#load` and `#load_directory` are the model (`src/parser.cpp`, and `check_load_directive` / `check_load_directory_directive` in `src/check_builtin.cpp`); Odin's `#` is not imported, because an s-expression language already has a head position for a name and these resolve as @@ -4551,12 +4551,12 @@ so a program can never be a package: the single file doing `(rl/load-texture "br with **no link channel at all**. The web lane found that hole and did not invent a flag for it. Embedding has no such hole, because there is nothing to tell the linker. -**It costs nothing at run time.** The bytes reach the program as a `Tast.Str` node typed `[u8]`, which emit.ml turns +**It costs nothing at run time.** The bytes reach the program as a `Tast.Str` node typed `[const u8]`, which emit.ml turns into the same `private unnamed_addr constant` every string literal already becomes, and its `escape` is byte-exact across the whole 0–255 range, so a PNG survives the round trip through the `.ll`. Bound with `defconst` at top level an `embed-dir` is an LLVM constant outright, through emit.ml's `const`. -**A `Str` node typed `[u8]`, not a `Bytes` prim over a `string`.** This is the one non-obvious choice. `Bytes` is +**A `Str` node typed `[const u8]`, not a `Bytes` prim over a `string`.** This is the one non-obvious choice. `Bytes` is identity — emit.ml lowers `Types.String` and `Types.Slice _` to the same `%slice` — but wrapping the literal in a prim makes the node non-constant, and `const` then refuses an `embed-dir` in a `defconst` with *a global's value must be a compile-time constant*. Both of emit.ml's string emitters take the bytes and ignore the node's type, so it is the same @@ -4583,11 +4583,9 @@ the call reads `(embed-find (slice assets 0 (length assets)) "brush.png")`. Entr order is filesystem-dependent and an unsorted embed would make two builds of identical sources emit different `.ll`. Non-recursive, files only — Odin again. -**The sharp edge, inherited and not widened.** The slice points into `.rodata`, so a store through it segfaults at -`-O0` and is deleted as undefined behaviour at `-O2` — the same trap the prelude's ASCII-case note measures for -`(bytes "Hi")`, and the same one TODO.org tracks as "Writing through a string literal". Nothing here makes it worse and -nothing here fixes it; provenance is what would. **To get a mutable copy, clone the bytes into a `Vec`.** It is worth -saying loudly because an embedded asset is precisely the thing someone will try to decode in place. +**Read-only, and the type says so.** The slice points into `.rodata`, where a store would segfault at `-O0` and be +deleted as undefined behaviour at `-O2`, so it is a `[const u8]` and a store through it is refused at compile time. +To decode an asset in place, copy the bytes into a `Vec` first. **What this does not do.** `sand.flan` still calls `(rl/load-texture "brush.png")`, which hands raylib a path for raylib to open. Pointing raylib at embedded bytes needs `LoadImageFromMemory` and `LoadTextureFromImage` in place of diff --git a/emacs/flan-mode.el b/emacs/flan-mode.el index f5a45fac..8edc20c6 100644 --- a/emacs/flan-mode.el +++ b/emacs/flan-mode.el @@ -238,7 +238,9 @@ reason and is the odd one — it is legal only as the last item of a `def' or a ;; resolves and the two function types, `Fn' and `CFn'. `dyn' is ;; lowercase on purpose — it is a primitive beside `i64' and `bool', not ;; a container over something. - ;; `int' and `float' are builtin aliases for `i32' and `f32'. + ;; `int' and `float' are builtin aliases for `i32' and `f32'. `const' + ;; is the reserved word of the read-only slice type, `[const u8]', and is + ;; drawn as part of the type it spells. ;; ;; `Unit' is deliberately absent, though `Types.primitive_names' has it. ;; The resolver answers to the name because `Cimport' builds one for C's @@ -246,7 +248,7 @@ reason and is the odd one — it is legal only as the last item of a `def' or a ;; word outright — unit is spelled `()'. Drawing it as a valid type would ;; advertise a spelling the parser rejects, which is the same reason ;; `find-restart' and `await' are left out of `flan--special'. - ("\\_<\\(?:[iu]\\(?:8\\|16\\|32\\|64\\)\\|f\\(?:32\\|64\\)\\|bool\\|string\\|dyn\\|int\\|float\\|Never\\|Allocator\\|Ptr\\|Option\\|Vec\\|Map\\|C?Fn\\)\\_>" + ("\\_<\\(?:[iu]\\(?:8\\|16\\|32\\|64\\)\\|f\\(?:32\\|64\\)\\|bool\\|string\\|dyn\\|const\\|int\\|float\\|Never\\|Allocator\\|Ptr\\|Option\\|Vec\\|Map\\|C?Fn\\)\\_>" . font-lock-type-face) ;; A type variable, `$t', which is what a generic `defn' names its ;; parameter types with and what `{:where (ordered? $t)}' constrains. diff --git a/emacs/test-flan-mode.el b/emacs/test-flan-mode.el index be9d1761..0640f967 100644 --- a/emacs/test-flan-mode.el +++ b/emacs/test-flan-mode.el @@ -489,6 +489,8 @@ "a package alias") ("(defn f [x int] float 1.0)" "int" font-lock-type-face "int, the builtin alias") + ("(defn f [s [const u8]] 1)" "const" font-lock-type-face + "const, in a read-only slice type") ;; Constants that stand for themselves. ("(set done true)" "true" font-lock-constant-face "true") ("(= o None)" "None" font-lock-constant-face "None") diff --git a/examples/text-rectangle-bounds.flan b/examples/text-rectangle-bounds.flan index fc4f7e81..8061a228 100644 --- a/examples/text-rectangle-bounds.flan +++ b/examples/text-rectangle-bounds.flan @@ -63,7 +63,7 @@ ;; from here they are ordinary slices, bounds-checked like any other, and the ;; index comes from raylib's own get-glyph-index so it is in range by ;; construction. -(defn draw-text-boxed [font rl/Font text [u8] rec rl/Rectangle +(defn draw-text-boxed [font rl/Font text [const u8] rec rl/Rectangle font-size f32 spacing f32 word-wrap? bool tint rl/Color] () (let [glyphs (rl/font-glyphs font) diff --git a/lib/ast.ml b/lib/ast.ml index 41708a09..c507c66f 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -14,7 +14,7 @@ type texpr = { t : texpr_kind; tloc : Loc.t } and texpr_kind = | Tname of string (* i32 bool Cursor string *) - | Tslice of texpr (* [u8] ptr+len *) + | Tslice of bool * texpr (* [u8] [const u8] ptr+len *) | Tarray of len * texpr (* [4 f32] [rows [cols u32]] *) | Tmap of texpr * texpr (* (Map string i32) *) | Tapp of string * texpr list (* (Ptr Cursor) (Option f64) *) diff --git a/lib/check.ml b/lib/check.ml index e5106991..652612ad 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1137,7 +1137,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t = let loc = t.Ast.tloc in match t.Ast.t with | Ast.Tname n -> resolve_name env ~seen loc n - | Ast.Tslice e -> Types.Slice (resolve env ~seen e) + | Ast.Tslice (c, e) -> + Types.Slice ((if c then Types.Const else Types.Mut), resolve env ~seen e) | Ast.Tarray (l, e) -> let e = resolve env ~seen e in no_zeroed_fn loc "a fixed array's element" e; @@ -1660,7 +1661,7 @@ let rec bracket_value_element env values (t : Ast.texpr) = | _ -> bracket_value_element env values e in match t.Ast.t with - | Ast.Tslice e -> elem e + | Ast.Tslice (_, e) -> elem e | Ast.Tarray (_, e) -> elem e | _ -> None @@ -1734,7 +1735,7 @@ let signature_tyvars (fn : Ast.fn) = let rec ty (t : Ast.texpr) = match t.Ast.t with | Ast.Tname n -> name t.Ast.tloc n - | Ast.Tslice e -> ty e + | Ast.Tslice (_, e) -> ty e | Ast.Tarray (_, e) -> ty e | Ast.Tmap (k, v) -> ty k; ty v (* The head of an application is a constructor — [Ptr], [Option], [Vec] — @@ -1752,24 +1753,30 @@ let signature_tyvars (fn : Ast.fn) = and with the same rule: a variable already bound must match what it is bound to, so [(pair 1 2.0)] over [a $t b $t] is a refusal and not a second instantiation. *) -let rec bind_ty ?(widen = false) subst (pat : Types.t) (arg : Types.t) = +(* [ro] is whether a [[T]] argument may meet a [[const $t]] pattern here: at + the top of an argument's type, and under a const slice, which is exactly + where [Types.const_widens] lets [expect] convert the value afterwards. *) +let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t) + (arg : Types.t) = + let inner = bind_ty ~ro:false subst in match pat, arg with | Types.Var v, a -> (match List.assoc_opt v !subst with | None -> subst := (v, a) :: !subst; true | Some b -> Types.equal a b) - | Types.Slice p, Types.Slice a + | Types.Slice (m, p), Types.Slice (m', a) + when m = m' || (ro && m = Types.Const) -> + bind_ty ~ro:(m = Types.Const) subst p a | Types.Ptr p, Types.Ptr a | Types.Vec p, Types.Vec a - | Types.Option p, Types.Option a -> bind_ty subst p a - | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && bind_ty subst p a - | Types.Map (k, v), Types.Map (k', v') -> - bind_ty subst k k' && bind_ty subst v v' + | Types.Option p, Types.Option a -> inner p a + | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && inner p a + | Types.Map (k, v), Types.Map (k', v') -> inner k k' && inner v v' (* Each function type against its own. *) | Types.Fn (ps, r), Types.Fn (ps', r') | Types.CFn (ps, r), Types.CFn (ps', r') -> List.length ps = List.length ps' - && List.for_all2 (bind_ty subst) ps ps' && bind_ty subst r r' + && List.for_all2 inner ps ps' && inner r r' (* And the widening between them, which is admitted at the top of an argument's type and nowhere inside it. [(Fn [$t] $t)] against a [(CFn [i32] i32)] is the shape every caller of @@ -1796,7 +1803,7 @@ let rec bind_ty ?(widen = false) subst (pat : Types.t) (arg : Types.t) = argument. *) | Types.Fn (ps, r), Types.CFn (ps', r') when widen -> List.length ps = List.length ps' - && List.for_all2 (bind_ty subst) ps ps' && bind_ty subst r r' + && List.for_all2 inner ps ps' && inner r r' (* Nothing generic left on the pattern side: this is ordinary type equality, and [Never] fits anywhere exactly as it does elsewhere. *) | p, a -> Types.fits ~expected:p ~actual:a @@ -1804,7 +1811,7 @@ let rec bind_ty ?(widen = false) subst (pat : Types.t) (arg : Types.t) = let rec subst_ty subst (t : Types.t) = match t with | Types.Var v -> (match List.assoc_opt v subst with Some c -> c | None -> t) - | Types.Slice e -> Types.Slice (subst_ty subst e) + | Types.Slice (m, e) -> Types.Slice (m, subst_ty subst e) | Types.Array (n, e) -> Types.Array (n, subst_ty subst e) | Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v) | Types.Ptr e -> Types.Ptr (subst_ty subst e) @@ -1819,7 +1826,7 @@ let rec subst_ty subst (t : Types.t) = let rec generic_ty (t : Types.t) = match t with | Types.Var _ -> true - | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e | Types.Option e -> generic_ty e | Types.Map (k, v) -> generic_ty k || generic_ty v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -1833,7 +1840,7 @@ let rec generic_ty (t : Types.t) = let rec reaches_dyn (t : Types.t) = match t with | Types.Dyn -> true - | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e | Types.Option e -> reaches_dyn e | Types.Map (k, v) -> reaches_dyn k || reaches_dyn v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -1873,7 +1880,8 @@ let unconstrained env loc op ~needs (t : Types.t) = let rec mangle_ty (t : Types.t) = match t with | Types.Unit -> "unit" - | Types.Slice e -> "slice-" ^ mangle_ty e + | Types.Slice (Types.Mut, e) -> "slice-" ^ mangle_ty e + | Types.Slice (Types.Const, e) -> "cslice-" ^ mangle_ty e | Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (mangle_ty e) | Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v) | Types.Ptr e -> "ptr-" ^ mangle_ty e @@ -1917,7 +1925,7 @@ let rec occurs_in ~needle (t : Types.t) = Types.equal needle t || match t with - | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e | Types.Option e -> occurs_in ~needle e | Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -2229,7 +2237,7 @@ let num_bytes = 64L let to_bytes ctx loc pr (x : Tast.expr) = let bty = Types.Array (num_bytes, Types.Int Types.U8) in - let bslice = Types.Slice (Types.Int Types.U8) in + let bslice = Types.Slice (Types.Mut, (Types.Int Types.U8)) in let s = fresh_slot ctx bty in mk loc bslice (Tast.Let @@ -2551,7 +2559,16 @@ let box loc (e : Tast.expr) : Tast.expr = | Some k -> if not (permanent_root e) then view_not_permanent loc e.Tast.ty else dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ]) - | Types.Slice elem -> + (* A dyn view is written through by (set (at d i) x), and nothing on the + dyn side can tell a read-only one apart, so a [[const T]] does not + cross. *) + | Types.Slice (Types.Const, elem) -> + no_dyn_yet loc ~into:true e.Tast.ty + (Printf.sprintf + ": a dyn view can be written through, and a [const %s] can only be \ + read. A dyn view is taken of the writable storage it came from" + (Types.to_string elem)) + | Types.Slice (Types.Mut, elem) -> (match view_elem elem with | None -> view_not_yet loc e.Tast.ty elem | Some k -> @@ -2849,7 +2866,8 @@ let rec thick_enc (t : Types.t) = | Types.Named n -> "n" ^ atom n | Types.Enum n -> "e" ^ atom n | Types.Var v -> "y" ^ atom v - | Types.Slice e -> "s" ^ thick_enc e + | Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e + | Types.Slice (Types.Const, e) -> "k" ^ thick_enc e | Types.Ptr e -> "p" ^ thick_enc e | Types.Vec e -> "v" ^ thick_enc e | Types.Option e -> "o" ^ thick_enc e @@ -2911,6 +2929,27 @@ let numeric_note ~(want : Types.t) ~(got : Types.t) = (%s x)" (Types.to_string want) +(* The rest of the sentence when a read-only slice meets a writable one. Both + copies it names compile today: [string] reads any byte slice and [bytes] + copies a string, and [into] pushes any slice's elements into a Vec that + [slice] then views. *) +let const_note ~(want : Types.t) ~(got : Types.t) = + match want, got with + | Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e') + when Types.equal e e' -> + let copy = + match e with + | Types.Int Types.U8 -> "(bytes (string v))" + | _ -> Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e) + in + Printf.sprintf + " — a %s can only be read, and never becomes a %s that can be written \ + through. %s copies v into a %s of its own; where nothing writes \ + through it, the %s can be declared %s instead" + (Types.to_string got) (Types.to_string want) copy (Types.to_string want) + (Types.to_string want) (Types.to_string got) + | _ -> "" + let expect ctx loc ~want (got : Tast.expr) = match want with | None -> got @@ -2958,6 +2997,12 @@ let expect ctx loc ~want (got : Tast.expr) = | Types.Fn (ps, r), Types.CFn (ps', r') when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) -> mk loc w (Tast.Thicken (thick_thunk ctx.env loc ps r, got)) + (* 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. *) + | Types.Slice (Types.Const, _), _ + when Types.const_widens ~from:got.Tast.ty ~into:w -> + { got with Tast.ty = w } | _ -> got in if Types.fits ~expected:w ~actual:got.Tast.ty then got @@ -2971,9 +3016,10 @@ let expect ctx loc ~want (got : Tast.expr) = numbers, and it is on this message rather than beside it because a reader who has just been told i64 and i32 are different types needs to be told, in the same breath, which direction needed nothing. *) - Loc.failk "check/type-mismatch" loc "expected %s, found %s%s" + Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s" (Types.to_string w) (Types.to_string got.Tast.ty) (numeric_note ~want:w ~got:got.Tast.ty) + (const_note ~want:w ~got:got.Tast.ty) (* Something a [break] may not jump out of, named so the refusal can say which. See [lentry]: it is a barrier and not a blanket refusal, so a loop written @@ -5474,7 +5520,7 @@ and check_arr ctx ~want loc items = let elem_want = match want with | Some (Types.Array (_, t)) -> Some t - | Some (Types.Slice t) -> Some t + | Some (Types.Slice (_, t)) -> Some t | _ -> None in (* With nothing outside saying what the elements are, the first one says: @@ -6117,7 +6163,44 @@ 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" -and check_place ctx loc (p : Ast.place) : Tast.place * Types.t = +(* 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 + other way across: [load-image-from-memory] over an [embed] is the case. So + the address of a read-only element may be taken, and it is a store that is + refused. *) +and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t = match p with | Ast.Pvar name -> (* Scope first, and the capture refusal only where scope did not settle @@ -6167,7 +6250,9 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t = | None -> Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname) "%s has no field %s" sname name - | Some i -> Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty) + | Some i -> + if store then Option.iter (refuse_const_place loc) (const_reached target); + Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty) | Ast.Pindex (target, idx) -> let target = check ctx target in (match target.Tast.ty with @@ -6179,7 +6264,7 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t = let p, ty = vec_at ctx loc target idx in Tast.Pderef p, ty | _ -> - let idx, ty = indexed ~place:loc ctx target idx in + let idx, ty = indexed ~place:loc ~store ctx target idx in Tast.Pindex (target, idx), ty) | Ast.Pderef target -> let target = check ctx target in @@ -6239,13 +6324,18 @@ and index_expr ctx (e : Ast.expr) = at *every* dimension rather than once about the target: [(at g 0 0)] over a [[2 string]] reaches a string at the last step and nowhere before it, so a question asked only of [g] would miss it. *) -and indexed ?place ctx (target : Tast.expr) (idx : Ast.expr list) = +and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list) = + (match place with + | Some l when store -> + Option.iter (refuse_const_place l) + (const_steps (const_reached target) target.Tast.ty (List.length idx)) + | _ -> ()); let rec go ty = function | [] -> [], ty | i :: rest -> let elem = match ty with - | Types.Array (_, t) | Types.Slice t -> t + | Types.Array (_, t) | Types.Slice (_, t) -> t (* A string indexes to its bytes, and only to read them. *) | Types.String -> Option.iter (fun l -> refuse_string_place l ty) place; @@ -6370,7 +6460,7 @@ and not_numeric name what (a : Tast.expr) = let text = match a.Tast.ty with | Types.String -> true - | Types.Slice (Types.Int Types.U8) -> true + | Types.Slice (_, (Types.Int Types.U8)) -> true | _ -> false in let where = a.Tast.loc in @@ -6784,7 +6874,10 @@ and type_of_expr (e : Ast.expr) : Ast.texpr option = in match e.Ast.e with | Ast.TypeArg t -> Some t - | Ast.Arr [ x ] -> Option.map (fun t -> mk (Ast.Tslice t)) (inner x) + (* Before the [[n T]] arm below, which would read [const] as a length. *) + | Ast.Arr [ { Ast.e = Ast.Var "const"; _ }; x ] -> + Option.map (fun t -> mk (Ast.Tslice (true, t))) (inner x) + | Ast.Arr [ x ] -> Option.map (fun t -> mk (Ast.Tslice (false, t))) (inner x) | Ast.Arr [ { Ast.e = Ast.Int n; _ }; x ] -> Option.map (fun t -> mk (Ast.Tarray (Ast.Lint n, t))) (inner x) | Ast.Arr [ { Ast.e = Ast.Var n; _ }; x ] -> @@ -6940,17 +7033,17 @@ and vec_slice ctx ~want loc (target : Tast.expr) elem (bounds : Ast.expr list) = lo, hi | _ -> assert false in - let out = fresh_slot ctx (Types.Slice elem) in + let out = fresh_slot ctx (Types.Slice (Types.Mut, elem)) in let fill = rt loc Types.Unit "flan_vec_as_slice" - [ target; addr_of loc (mk loc (Types.Slice elem) (Tast.Local out)); + [ target; addr_of loc (mk loc (Types.Slice (Types.Mut, elem)) (Tast.Local out)); lo; hi; size_of loc elem; here loc ] in expect ctx loc ~want - (mk loc (Types.Slice elem) - (Tast.Let ([ (out, mk loc (Types.Slice elem) - (Tast.Zero (Types.Slice elem))) ], - [ fill; mk loc (Types.Slice elem) (Tast.Local out) ]))) + (mk loc (Types.Slice (Types.Mut, elem)) + (Tast.Let ([ (out, mk loc (Types.Slice (Types.Mut, elem)) + (Tast.Zero (Types.Slice (Types.Mut, elem)))) ], + [ fill; mk loc (Types.Slice (Types.Mut, elem)) (Tast.Local out) ]))) (* Every arm below is a name an editor can be asked about and no program ever wrote down, so each one needs a line in [builtins] further down this file. @@ -7908,7 +8001,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = | [ s ] -> let s = check ctx s in (match s.Tast.ty with - | Types.String | Types.Slice (Types.Int Types.U8) -> + | Types.String | Types.Slice (_, (Types.Int Types.U8)) -> expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_kw" [ s ]) | other -> fail loc "keyword takes a string or a [u8], found %s" @@ -8073,13 +8166,10 @@ and named_call ?(qualified = false) ctx ~want loc name args = the round trip through the .ll. Bound with [defconst], an [embed-dir] becomes an LLVM constant outright (emit.ml's [const]). - The one sharp edge, and it is not new: the slice this hands back points - into .rodata, so a store through it either segfaults at -O0 or is deleted - at -O2 — the same measured trap the prelude's ASCII-case note describes - for (bytes-view "Hi"). Copy the bytes — (bytes s) does exactly that for a - string — for a mutable buffer. Nothing here widens that hole; it inherits - it, and read-only slice types are what would close it (TODO.org, "A - read-only slice type"). *) + The slice this hands back points into .rodata, so it is a [const u8]: a + store through it would segfault at -O0 and be deleted at -O2, and the + type refuses it at compile time instead. Copy the bytes for a writable + buffer. *) | "embed" -> (match args with | [ p ] | [ p; _ ] -> @@ -8091,17 +8181,17 @@ and named_call ?(qualified = false) ctx ~want loc name args = | [ _; { Ast.e = Ast.Var "string"; _ } ] | [ _ ] -> () | [ _; t ] -> fail t.Ast.loc - "embed's second argument is string, or nothing for a [u8]" + "embed's second argument is string, or nothing for a [const u8]" | _ -> ()); let data = read_embed_file (embed_path loc p) p.Ast.loc in let as_string () = mk loc Types.String (Tast.Str data) in - (* A [Str] node typed [u8] rather than a [Bytes] prim over one. [Bytes] + (* A [Str] node typed [const u8] rather than a [Bytes] prim over one. [Bytes] is identity — emit.ml lowers String and Slice _ to the same %slice — and the prim would make the node non-constant, so an (embed-dir) in a defconst could not be an LLVM constant. Both of emit.ml's string emitters take the bytes and ignore the node's type, so this is the same constant either way, and it is one a global can hold. *) - let as_bytes () = mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Str data) in + let as_bytes () = mk loc (Types.Slice (Types.Const, Types.Int Types.U8)) (Tast.Str data) in (* Two spellings rather than one that changes type with its context. Odin threads a type_hint everywhere and can afford (embed "p") to mean a string here and a []u8 there; with structural equality and a @@ -8118,7 +8208,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = | _ -> expect ctx loc ~want (as_bytes ()))) | _ -> fail loc - "embed is (embed \"path\") for a [u8], or (embed \"path\" string)") + "embed is (embed \"path\") for a [const u8], or (embed \"path\" string)") (* ── What a macro says when it has to refuse ─────────────────── The one thing a macro could not do, written down in the prelude where [unless] settles for it: "a macro has no error facility: it runs inside @@ -8166,7 +8256,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (Tast.Make ("EmbedFile", [ mk loc Types.String (Tast.Str nm); - mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Str data) ]))) + mk loc (Types.Slice (Types.Const, Types.Int Types.U8)) (Tast.Str data) ]))) entries in expect ctx loc ~want @@ -8246,11 +8336,11 @@ and named_call ?(qualified = false) ctx ~want loc name args = let path = check ctx ~want:Types.String path in let data = byte_slice ctx data in let ps = fresh_slot ctx Types.String in - let ds = fresh_slot ctx (Types.Slice (Types.Int Types.U8)) in + let ds = fresh_slot ctx (Types.Slice (Types.Const, Types.Int Types.U8)) in let steps try_ = [ try_ (rt loc (Types.Int Types.I8) "flan_file_write" [ mk loc Types.String (Tast.Local ps); - mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Local ds) ]) ] + mk loc (Types.Slice (Types.Const, Types.Int Types.U8)) (Tast.Local ds) ]) ] in (* Both operands are bound before the loop so that a retry re-attempts the write and not the expressions that produced it — the same rule @@ -8420,7 +8510,8 @@ and named_call ?(qualified = false) ctx ~want loc name args = calling it a byte slice would hand out a writable-looking view of storage the program does not own. *) let result = match ty with - | Types.Array (_, t) | Types.Slice t -> Types.Slice t + | Types.Array (_, t) -> Types.Slice (Types.Mut, t) + | Types.Slice (m, t) -> Types.Slice (m, t) | Types.String -> Types.String | other -> fail loc @@ -8545,7 +8636,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = fail n_loc "slice-from-ptr length %Ld is negative" k | _ -> ()); - prim Tast.SliceFromPtr (Types.Slice elem) [ target; n ] + prim Tast.SliceFromPtr (Types.Slice (Types.Mut, elem)) [ target; n ] | _ -> assert false) (* ── pointers ──────────────────────────────────────────────────── *) @@ -8558,7 +8649,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = "addr takes the address of a place — a name, (.field x), (at a i) \ or (deref p)" | Some p -> - let p, ty = check_place ctx a.Ast.loc p in + let p, ty = check_place ~store:false ctx a.Ast.loc p in expect ctx loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p))) | "deref" -> arity ctx loc name 1 args; @@ -8600,17 +8691,17 @@ and named_call ?(qualified = false) ctx ~want loc name args = expect ctx loc ~want (mk loc (Types.Option a.Tast.ty) (Tast.Some_ a)) (* ── the milestone-2 host primitives (plan.org) ────────────────── *) - (* (bytes-view s): the string's own storage seen as a [u8], costing nothing. - This is what (bytes s) used to be, renamed for what it is: a *view*. The - slice aliases the string — a literal's view points into .rodata and a - store through it traps at -O0 on either backend — so it is read-only by - convention until the type system can say so (TODO.org, "A read-only - slice type"). + (* (bytes-view s): the string's own storage seen as a [const u8], costing + nothing. The slice aliases the string, and a literal's bytes are in + read-only memory — a store through them would trap at -O0 and be deleted + as undefined at -O2 — so the view is one that can only be read, and a + store through it is refused here rather than at run time. (bytes s) is + the writable copy. Reading through it is the whole use: bytes=?, split, index-of-bytes and every other comparison walks a string's bytes without copying them. *) | "bytes-view" -> arity ctx loc name 1 args; - prim Tast.Bytes (Types.Slice (Types.Int Types.U8)) + prim Tast.Bytes (Types.Slice (Types.Const, Types.Int Types.U8)) [ check ctx ~want:Types.String (List.hd args) ] (* (bytes s) / (bytes s a): a *writable copy* of the string's bytes, from @@ -8641,7 +8732,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = the string. Same rule as [push]'s element. *) let sv = fresh_slot ctx Types.String in let v = fresh_slot ctx (Types.Vec u8) in - let out = fresh_slot ctx (Types.Slice u8) in + let out = fresh_slot ctx (Types.Slice (Types.Mut, u8)) in let attempt = rt loc (Types.Int Types.I8) "flan_bytes_dup" [ mk loc (Types.Vec u8) (Tast.Local v); a; @@ -8650,23 +8741,23 @@ and named_call ?(qualified = false) ctx ~want loc name args = let fill = rt loc Types.Unit "flan_vec_as_slice" [ mk loc (Types.Vec u8) (Tast.Local v); - addr_of loc (mk loc (Types.Slice u8) (Tast.Local out)); + addr_of loc (mk loc (Types.Slice (Types.Mut, u8)) (Tast.Local out)); mk loc index_ty (Tast.Int (0L, Types.I32)); mk loc index_ty (Tast.Int (-1L, Types.I32)); size_of loc u8; here loc ] in expect ctx loc ~want - (mk loc (Types.Slice u8) + (mk loc (Types.Slice (Types.Mut, u8)) (Tast.Let ([ (sv, s); (v, mk loc (Types.Vec u8) (Tast.Zero (Types.Vec u8))); - (out, mk loc (Types.Slice u8) (Tast.Zero (Types.Slice u8))) ], + (out, mk loc (Types.Slice (Types.Mut, u8)) (Tast.Zero (Types.Slice (Types.Mut, u8)))) ], [ with_note loc (alloc_guard ctx loc attempt) (reg_note loc "flan_dev_reg_note_vec" (mk loc (Types.Vec u8) (Tast.Local v)) [ size_of loc u8 ] u8); fill; - mk loc (Types.Slice u8) (Tast.Local out) ]))) + mk loc (Types.Slice (Types.Mut, u8)) (Tast.Local out) ]))) | _ -> fail loc "bytes is (bytes s) or (bytes s allocator)") (* (string b): a [u8] seen as a string. The mirror of (bytes-view s), @@ -8695,12 +8786,8 @@ and named_call ?(qualified = false) ctx ~want loc name args = would be the only enforcement point in the language — a claim the rest of it does not make. - 2. It does not widen the literal-write hole (TODO.org, "Writing through a - string literal"). That hole is the other direction: (bytes-view "Hi") - hands you a writable-looking slice over constant data — narrowed since - (bytes s) became a copy, and closable only by read-only slice types - (TODO.org, "A read-only slice type"). This direction only loses the - ability to write — a string + 2. It takes a [const u8], so a [u8] and a (bytes-view s) are both + accepted. This direction only loses the ability to write — a string is read-only everywhere — so the result of (string b) can reach strictly fewer stores than b could. @@ -8812,7 +8899,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = if List.exists (fun a -> generic_ty a.Tast.ty) checked then mk loc Types.Unit Tast.Unit else - let bslice = Types.Slice (Types.Int Types.U8) in + let bslice = Types.Slice (Types.Mut, (Types.Int Types.U8)) in let write x = mk loc Types.Unit (Tast.Prim (Tast.WriteStdout, [ x ])) in (* One frame slot per conversion the printer emits, which is what [to_bytes] is for. The printer writes each number out before making the @@ -8836,7 +8923,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = let rc = render_ctx ctx emitter in let render_one a = match a.Tast.ty with - | Types.String | Types.Slice (Types.Int Types.U8) -> + | Types.String | Types.Slice (_, (Types.Int Types.U8)) -> [ write (mk loc bslice (Tast.Prim (Tast.Bytes, [ a ]))) ] | _ -> Render.render rc 0 a in @@ -8884,7 +8971,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = if generic_ty v.Tast.ty then mk loc Types.Unit Tast.Unit else begin let unit_rt sym args = mk loc Types.Unit (Tast.Prim (Tast.Rt sym, args)) in - let bslice = Types.Slice (Types.Int Types.U8) in + let bslice = Types.Slice (Types.Mut, (Types.Int Types.U8)) in let emitter : Render.emitter = { Render.ebytes = (fun x -> unit_rt "flan_dev_watch_emit" [ x ]); estr = (fun x -> unit_rt "flan_dev_watch_emit_str" [ x ]); @@ -8943,7 +9030,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = prim Tast.Exit Types.Never [ check ctx ~want:index_ty (List.hd args) ] | "argv" -> arity ctx loc name 0 args; - prim Tast.Argv (Types.Slice Types.String) [] + prim Tast.Argv (Types.Slice (Types.Mut, Types.String)) [] (* ── casts: (i32 x), (f64 x), and an enum both ways ──────────────── @@ -9428,7 +9515,7 @@ and generic_call ctx ~want loc name vars pats pret args = let rec mentions v (t : Types.t) = match t with | Types.Var u -> String.equal u v - | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e | Types.Option e -> mentions v e | Types.Map (k, w) -> mentions v k || mentions v w | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -9537,8 +9624,16 @@ and generic_call ctx ~want loc name vars pats pret args = (* [~widen]: this is the top of an argument's type, which is the one place a widening thunk can be built around it. See [bind_ty]. *) if (not handled) && not (bind_ty ~widen:true subst p a.Tast.ty) then - fail a.Tast.loc "%s expects %s here, found %s" name - (Types.to_string p) (Types.to_string a.Tast.ty); + fail a.Tast.loc "%s expects %s here, found %s%s" name + (Types.to_string p) (Types.to_string a.Tast.ty) + (match p, a.Tast.ty with + | Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) -> + Printf.sprintf + " — %s takes a slice it may write through, and a %s can \ + only be read. (slice (into v (vec-new %s))) copies v into \ + one that can be written" + name (Types.to_string a.Tast.ty) (Types.to_string e) + | _ -> ""); a) pats args in @@ -9792,7 +9887,7 @@ and is_cast name = Types.ikind_of_name name <> None || Types.fkind_of_name name <> None and byte_slice ctx (a : Ast.expr) = - check ctx ~want:(Types.Slice (Types.Int Types.U8)) a + check ctx ~want:(Types.Slice (Types.Const, Types.Int Types.U8)) a and numeric_want want = match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None @@ -10211,13 +10306,13 @@ let builtins : (string * string * string) list = It is what a defgeneric dispatches on, so a class dispatcher is this \ call over the first argument and a defmulti whose body is (class-of x) \ is the same generic function written the other way."); - ("keyword", "keyword [string|[u8]] dyn", + ("keyword", "keyword [string|[const u8]] dyn", "The interned dyn keyword named by the bytes, for a name that only \ exists at run time — a reader building :texture-path out of a token's \ text. A literal :foo is already one."); (* assets, embedded at compile time *) - ("embed", "embed [\"path\" string?] [u8]", + ("embed", "embed [\"path\" string?] [const u8]", "The file's bytes, read at compile time and baked in as a constant; \ (embed \"p\" string) reads it as a string instead. The path is \ relative to the file the form is written in, and the slice points into \ @@ -10235,7 +10330,7 @@ let builtins : (string * string * string) list = "Reads a whole file. No Result and no out-parameter: a failure to read \ signals FileError under retry and use-value, and a failure to allocate \ signals StorageExhausted."); - ("barf", "barf [string [u8]] ()", + ("barf", "barf [string [const u8]] ()", "Writes a whole file. On the web target it signals FileError every \ time, with the path — there is no conditional compilation, so the \ program decides rather than the build."); @@ -10289,17 +10384,17 @@ let builtins : (string * string * string) list = StorageExhausted with retry — and the block lives until its \ allocator's free-all or destroy. For reading without a copy, \ bytes-view."); - ("bytes-view", "bytes-view [string] [u8]", - "The string's own storage seen as a byte slice. It costs nothing — both \ - are a ptr and a length at run time — and it decodes nothing. \ - Read-only by convention: a literal's bytes are constant data, so the \ - slice looks writable and a store through it traps."); - ("string", "string [[u8]] string", + ("bytes-view", "bytes-view [string] [const u8]", + "The string's own storage seen as a read-only byte slice. It costs \ + nothing — both are a ptr and a length at run time — and it decodes \ + nothing. A store through it is a compile error; bytes is the writable \ + copy."); + ("string", "string [[const u8]] string", "A byte slice seen as a string, and free at run time. It does not check \ UTF-8, because `string` does not claim UTF-8 — valid-utf8? is an \ ordinary function you call when you care."); - ("bytes->f64", "bytes->f64 [[u8]] f64", "Parses a float out of the bytes."); - ("bytes->i64", "bytes->i64 [[u8]] i64", + ("bytes->f64", "bytes->f64 [[const u8]] f64", "Parses a float out of the bytes."); + ("bytes->i64", "bytes->i64 [[const u8]] i64", "Parses an integer out of the bytes."); ("f64->bytes", "f64->bytes [f64] [u8]", "The number's text, in a frame slot belonging to this call site — so \ @@ -10308,7 +10403,7 @@ let builtins : (string * string * string) list = ("i64->bytes", "i64->bytes [i64] [u8]", "The number's text, in a frame slot belonging to this call site; it \ does not survive the frame."); - ("write-stdout", "write-stdout [[u8]] ()", + ("write-stdout", "write-stdout [[const u8]] ()", "Writes the bytes to standard output exactly as given: no newline and \ no formatting."); ("print", "print [T ...] ()", @@ -10479,6 +10574,15 @@ let collect env (decls : Ast.decl list) = spelled with it reaches the compiler's builtins and never a \ declaration — nothing could call this one" n builtin_prefix + (* [[const u8]] is a read-only slice only because no constant can be + named [const]: [[n T]] takes a constant's name for [n], and a + declaration of that name would make the brackets mean two things. + A local cannot be an array length, so only a declaration is + refused. *) + | Some "const" -> + Loc.failk "check/reserved-const" d.Ast.dloc + "const cannot be declared: it is reserved for the read-only slice \ + type, [const T]. Choose another name" | _ -> ()) decls; let claimed = Hashtbl.create 64 in @@ -11501,7 +11605,7 @@ let check_main env decls = let ok_params = match params with | [] -> true - | [ Types.Slice Types.String ] -> true + | [ Types.Slice (_, Types.String) ] -> true | _ -> false in if not ok_params then @@ -11750,7 +11854,7 @@ let rec dyn_reach ~through p seen (t : Types.t) = | Types.Dyn -> true | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e | Types.Map (k, v) -> go k || go v - | Types.Ptr e | Types.Slice e -> through && go e + | Types.Ptr e | Types.Slice (_, e) -> through && go e | Types.Fn _ -> false | Types.Named n when not (List.mem n seen) -> let seen = n :: seen in @@ -11805,7 +11909,7 @@ let rec dyn_behind_pointer p seen (t : Types.t) = It still terminates. This walk's own [seen] guards its own [Named] recursion, and each crossing starts a separate finite walk of its own. *) - | Types.Ptr e | Types.Slice e -> dyn_through p [] e + | Types.Ptr e | Types.Slice (_, e) -> dyn_through p [] e | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e | Types.Map (k, v) -> go k || go v | Types.Dyn | Types.Fn _ -> false @@ -11880,7 +11984,7 @@ let rec hidden_dyn p seen (t : Types.t) : Types.t option = if dyn_anywhere p seen k || dyn_anywhere p seen v then Some t else None (* A pointer and a slice are views of storage something else roots; see the note above. What they point at is checked where it is declared. *) - | Types.Ptr e | Types.Slice e -> hidden_dyn p seen e + | Types.Ptr e | Types.Slice (_, e) -> hidden_dyn p seen e | Types.Fn _ -> None | Types.Named n when not (List.mem n seen) -> let seen = n :: seen in @@ -12029,7 +12133,7 @@ let dyn_descriptors (p : Tast.program) = foreign parameter of pointer or slice type receives is the address of a place. Below it the question is [dyn_behind_pointer]'s again. *) let below (t : Types.t) = - match t with Types.Ptr e | Types.Slice e -> e | t -> t + match t with Types.Ptr e | Types.Slice (_, e) -> e | t -> t in List.iteri (fun i t -> diff --git a/lib/cimport.ml b/lib/cimport.ml index 0e4823c9..7e0d5871 100644 --- a/lib/cimport.ml +++ b/lib/cimport.ml @@ -408,7 +408,8 @@ let rec ty_source (t : Ast.texpr) = | Ast.Tname n -> n | Ast.Tapp (n, args) -> Printf.sprintf "(%s %s)" n (String.concat " " (List.map ty_source args)) - | Ast.Tslice e -> Printf.sprintf "[%s]" (ty_source e) + | Ast.Tslice (c, e) -> + Printf.sprintf "[%s%s]" (if c then "const " else "") (ty_source e) | Ast.Tarray (Ast.Lint n, e) -> Printf.sprintf "[%Ld %s]" n (ty_source e) | Ast.Tarray (Ast.Lname n, e) -> Printf.sprintf "[%s %s]" n (ty_source e) | Ast.Tmap (k, v) -> diff --git a/lib/emit.ml b/lib/emit.ml index 800e4a71..c2b3c8e2 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -765,7 +765,7 @@ let rec dty m d (t : Types.t) : int = | Types.String -> composite "string" [ ("ptr", Types.Ptr (Types.Int Types.U8)); ("len", Types.Int Types.I64) ] - | Types.Slice e -> + | Types.Slice (_, e) -> composite (Types.to_string t) [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64) ] | Types.Option e -> @@ -2488,7 +2488,7 @@ and element_addr f (target : Tast.expr) idx = same way, bounds check included. *) | Types.Slice _ | Types.String -> let elem = - match ty with Types.Slice e -> e | _ -> Types.Int Types.U8 in + match ty with Types.Slice (_, e) -> e | _ -> Types.Int Types.U8 in (* A slice is ptr+len, so step through the pointer it holds. *) let s = load f ptr ty in let base = fresh f in @@ -3328,7 +3328,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) = ins f "%s = getelementptr inbounds %s, ptr %s, i64 0, i64 %s" p (ll target.Tast.ty) a lo64; p - | Types.Slice elem -> + | Types.Slice (_, elem) -> let v = value f target in let q = fresh f in ins f "%s = extractvalue %%slice %s, 0" q v; @@ -3434,9 +3434,9 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) = term f "unreachable"; "zeroinitializer" | Tast.Argv, [] -> - let tmp = alloca f (Types.Slice Types.String) in + let tmp = alloca f (Types.Slice (Types.Mut, Types.String)) in ins f "call void @flan_argv(ptr %s)" tmp; - load f tmp (Types.Slice Types.String) + load f tmp (Types.Slice (Types.Mut, Types.String)) (* One arm for every runtime entry point the allocator and container runtime has. The result type is the node's own and the argument types are the arguments' own, so nothing here has to know which symbol it is calling. *) @@ -3538,17 +3538,17 @@ and shim_in f name ret x = and shim_out f name (x : Tast.expr) (buf : Tast.expr) = let v = value f x in let b = value f buf in - let tmp = alloca f (Types.Slice (Types.Int Types.U8)) in + let tmp = alloca f (Types.Slice (Types.Mut, (Types.Int Types.U8))) in ins f "call void %s(%s %s, ptr %s, ptr %s)" name (ll x.Tast.ty) v b tmp; - load f tmp (Types.Slice (Types.Int Types.U8)) + load f tmp (Types.Slice (Types.Mut, (Types.Int Types.U8))) (* Slice in, slice out: [shim_in] returns a scalar and [shim_out] takes one, so a shim that transforms bytes into bytes is neither. *) and shim_in_out f name (x : Tast.expr) = let p, n = explode f x in - let tmp = alloca f (Types.Slice (Types.Int Types.U8)) in + let tmp = alloca f (Types.Slice (Types.Mut, (Types.Int Types.U8))) in ins f "call void %s(ptr %s, i64 %s, ptr %s)" name p n tmp; - load f tmp (Types.Slice (Types.Int Types.U8)) + load f tmp (Types.Slice (Types.Mut, (Types.Int Types.U8))) and cast f ~guard (x : Tast.expr) target = let v = value f x in diff --git a/lib/js.ml b/lib/js.ml index c687f59b..221faf9e 100644 --- a/lib/js.ml +++ b/lib/js.ml @@ -219,7 +219,7 @@ let rec refuse_ty loc (t : Types.t) = match t with | Types.Int _ | Types.Float _ | Types.Bool | Types.String | Types.Unit | Types.Never | Types.Named _ | Types.Enum _ -> () - | Types.Slice t | Types.Array (_, t) | Types.Option t -> refuse_ty loc t + | Types.Slice (_, t) | Types.Array (_, t) | Types.Option t -> refuse_ty loc t | Types.Vec t -> refuse_ty loc t | Types.Fn (ps, r) | Types.CFn (ps, r) -> List.iter (refuse_ty loc) ps; refuse_ty loc r @@ -654,7 +654,7 @@ let struct_of m loc (t : Types.t) = let elem_ty loc (t : Types.t) = match t with - | Types.Slice e | Types.Array (_, e) -> e + | Types.Slice (_, e) | Types.Array (_, e) -> e | Types.String -> Types.Int Types.U8 | t -> at loc "indexing %s is not in the JS dialect" (Types.to_string t) diff --git a/lib/load.ml b/lib/load.ml index a3f28a9b..beae5abd 100644 --- a/lib/load.ml +++ b/lib/load.ml @@ -198,7 +198,7 @@ let rec rename_texpr owned alias (t : Ast.texpr) : Ast.texpr = match t.Ast.t with | Ast.Tname n when List.mem n owned -> Ast.Tname (qualify alias n) | Ast.Tname _ as k -> k - | Ast.Tslice e -> Ast.Tslice (rename_texpr owned alias e) + | Ast.Tslice (c, e) -> Ast.Tslice (c, rename_texpr owned alias e) (* The length too: [rows] in [[rows [cols u32]]] is an ordinary compile-time constant of the package, not part of the type syntax. *) | Ast.Tarray (l, e) -> @@ -742,7 +742,7 @@ let exported n = not (String.equal n "main") let rec texpr_uses acc (t : Ast.texpr) = match t.Ast.t with | Ast.Tname n -> acc := (n, t.Ast.tloc) :: !acc - | Ast.Tslice e -> texpr_uses acc e + | Ast.Tslice (_, e) -> texpr_uses acc e | Ast.Tarray (l, e) -> (match l with Ast.Lname n -> acc := (n, t.Ast.tloc) :: !acc | Ast.Lint _ -> ()); texpr_uses acc e diff --git a/lib/parse.ml b/lib/parse.ml index c380830b..9002c5bf 100644 --- a/lib/parse.ml +++ b/lib/parse.ml @@ -89,10 +89,23 @@ let rec texpr (f : Form.t) : Ast.texpr = emitter go on speaking. *) | Sym "Unit" -> fail f "unit is written (), not Unit" | Sym s -> mk (Ast.Tname s) - | Vec [ elem ] -> mk (Ast.Tslice (texpr elem)) + (* [const T] is matched before [n T], which it would otherwise be: [const] + is a reserved name exactly so that no constant can be called that and + make the two spellings mean the same brackets. *) + | Vec [ { v = Sym "const"; _ } ] -> + fail f "[const] names no element type — a read-only slice is [const T]" + | Vec [ { v = Sym "const"; _ }; elem ] -> mk (Ast.Tslice (true, texpr elem)) + | Vec [ elem ] -> mk (Ast.Tslice (false, texpr elem)) | Vec [ n; elem ] -> mk (Ast.Tarray (len n, texpr elem)) + | Vec items when List.exists (fun (i : Form.t) -> i.v = Sym "const") items -> + fail f + "a read-only slice is written [const T], and a fixed array [n T] has no \ + read-only form — take a read-only view of one with (slice a) where a \ + [const T] is wanted" | Vec _ -> - fail f "a type in brackets is [T] for a slice or [n T] for a fixed array" + fail f + "a type in brackets is [T] for a slice, [const T] for a read-only \ + slice or [n T] for a fixed array" (* Braces are not a type. [{K V}] used to spell [(Map K V)] and the two resolved to the same thing; the brace spelling is withdrawn, and the refusal names the surviving one rather than letting the form fall through @@ -1805,7 +1818,7 @@ let rec decl (f : Form.t) : Ast.decl = what keeps the compiler's own parameter out of the way of every name the author might bind. Same trick as [gensym]. *) params = [ { Ast.fname = macro_args; - fty = { Ast.t = Ast.Tslice form_t; tloc = ps.loc }; + fty = { Ast.t = Ast.Tslice (false, form_t); tloc = ps.loc }; floc = ps.loc } ]; (* Written out, not deferred: a macro takes [[Form]] and returns a [Form], and neither half of that is the user's to diff --git a/lib/prelude.ml b/lib/prelude.ml index dee1d391..1b67f283 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -274,7 +274,7 @@ let source = {flan| ;; One family per element type, because there are no generics: each of these ;; is a *copy* per element type, and the set below is i32 (what indices, ids ;; and tile values are), f32 (what positions, velocities and weights are) and -;; [u8] (what a field coming out of `split` is). +;; [const u8] (what a field coming out of `split` is). ;; ;; A slice is ptr+len and non-owning, so these mutate the storage they were ;; handed: sorting (slice grid 4 9) sorts those five elements of grid and @@ -389,7 +389,7 @@ let source = {flan| ;; The first index holding x. None rather than -1, because Option is what the ;; language has and a sentinel index is the bug this avoids. -(defn index-of [s [$t] x $t] (Option i32) +(defn index-of [s [const $t] x $t] (Option i32) {:where (equal? $t)} (dotimes [i (length s)] (when (= (at s i) x) @@ -406,7 +406,7 @@ let source = {flan| ;; or more numbers, and a defn cannot shadow a builtin: nothing shadows [+] ;; either. These reduce a slice, which is a different operation with a ;; different arity, so the different name is honest rather than a workaround. -(defn min-of [s [$t]] (Option $t) +(defn min-of [s [const $t]] (Option $t) {:where (ordered? $t)} (if (= (length s) 0) None @@ -415,7 +415,7 @@ let source = {flan| (set m (min m (at s i)))) (Some m)))) -(defn max-of [s [$t]] (Option $t) +(defn max-of [s [const $t]] (Option $t) {:where (ordered? $t)} (if (= (length s) 0) None @@ -500,7 +500,7 @@ let source = {flan| ;; The general fold, of which sum-i32 is the special case with the + written ;; in. The accumulator comes first in the step, which is the order that reads ;; as (f acc x) and the order Odin's slice.reduce uses. -(defn reduce [s [$t] init $t f (Fn [$t $t] $t)] $t +(defn reduce [s [const $t] init $t f (Fn [$t $t] $t)] $t (let [acc init] (dotimes [i (length s)] (set acc (f acc (at s i)))) @@ -513,7 +513,7 @@ let source = {flan| ;; allocates — (vec-new t), push, returns (Vec t) — and the type-erased Vec ;; runtime needed no change at all, because SizeOf and AlignOf are computed at ;; the instantiation site, where the element type is concrete. -(defn filter [s [$t] keep? (Fn [$t] bool)] (Vec $t) +(defn filter [s [const $t] keep? (Fn [$t] bool)] (Vec $t) (let [v (vec-new t)] (dotimes [i (length s)] (when (keep? (at s i)) @@ -577,7 +577,7 @@ let source = {flan| ;; total silently wraps. The per-element (i64 ...) would happen on its own now; ;; it is written to keep the accumulator's type visible at the line that feeds ;; it. -(defn sum-i32 [s [i32]] i64 +(defn sum-i32 [s [const i32]] i64 (let [t (i64 0)] (dotimes [i (length s)] (set t (+ t (i64 (at s i))))) @@ -590,7 +590,7 @@ let source = {flan| ;; is silently short rather than obviously wrong. An f64 accumulator has 29 ;; more bits of mantissa and pushes that failure out of reach of any array a ;; game holds. -(defn sum-f32 [s [f32]] f64 +(defn sum-f32 [s [const f32]] f64 (let [t 0.0] (dotimes [i (length s)] (set t (+ t (f64 (at s i))))) @@ -598,12 +598,12 @@ let source = {flan| ;; ── Bytes ───────────────────────────────────────────────────────────── ;; -;; Over [u8] and not over string, so (bytes-view s) is what a caller writes and one -;; copy of each serves strings and byte slices both — which is as close to a +;; Over [const u8] and not over string, so (bytes-view s) is what a caller writes +;; and one copy of each serves strings and byte slices both, writable or not — which is as close to a ;; generic as a language without them gets. Nothing here allocates: every ;; result is a bool, an index, or a number. -(defn bytes=? [a [u8] b [u8]] bool +(defn bytes=? [a [const u8] b [const u8]] bool (if (!= (length a) (length b)) false (do @@ -615,11 +615,11 @@ let source = {flan| ;; The length test comes first and `and` short-circuits, so the slice is only ;; built once it is known to be in bounds — otherwise a prefix longer than the ;; string would trap rather than answer false. -(defn starts-with? [s [u8] p [u8]] bool +(defn starts-with? [s [const u8] p [const u8]] bool (and (<= (length p) (length s)) (bytes=? (slice s 0 (length p)) p))) -(defn ends-with? [s [u8] p [u8]] bool +(defn ends-with? [s [const u8] p [const u8]] bool (and (<= (length p) (length s)) (bytes=? (slice s (- (length s) (length p)) (length s)) p))) @@ -630,7 +630,7 @@ let source = {flan| ;; libc-dependent, and a parser in the language gives the same answer on ;; wasm32 as on native for the same reason rand does. ;; Overflow wraps, as all arithmetic here does; it is not reported. -(defn parse-i64 [s [u8]] (Option i64) +(defn parse-i64 [s [const u8]] (Option i64) (let [i 0 n (i64 0) neg false] @@ -1221,7 +1221,7 @@ let source = {flan| ;; ;; Naive, O(n·m), and that is the deliberate choice: Boyer–Moore wants a skip ;; table, which is an array sized by the needle, which is an allocation. -(defn index-of-bytes [s [u8] p [u8]] (Option i32) +(defn index-of-bytes [s [const u8] p [const u8]] (Option i32) (when (> (length p) (length s)) (return None)) (let [last (- (length s) (length p)) @@ -1240,7 +1240,7 @@ let source = {flan| ;; The two loops both test (< lo hi), so an all-whitespace input walks lo up ;; to hi and stops there, and the result is the empty slice. Without that test ;; lo would pass hi and (slice s lo hi) would be a reversed range, which traps. -(defn trim [s [u8]] [u8] +(defn trim [s [const u8]] [const u8] (let [lo 0 hi (length s)] (while (and (< lo hi) (space? (at s lo))) @@ -1268,7 +1268,7 @@ let source = {flan| ;; 511 cap is flan_bytes_to_f64's buffer: past it the shim truncates, and a ;; validator that said yes to 600 digits would be approving a different ;; number than the one strtod reads. -(defn parse-f64 [s [u8]] (Option f64) +(defn parse-f64 [s [const u8]] (Option f64) (let [i 0 digits 0] (when (or (= (length s) 0) (> (length s) 511)) @@ -1350,7 +1350,7 @@ let source = {flan| (defn rune-start? [b u8] bool (!= (bit-and b 0xc0) 0x80)) -(defn decode-rune [s [u8]] Rune +(defn decode-rune [s [const u8]] Rune (when (= (length s) 0) (return (Rune {.code 0 .width 0 .ok false}))) (let [b0 (at s 0)] @@ -1406,7 +1406,7 @@ let source = {flan| ;; Decode at a byte offset. None when the offset is not on a rune boundary or ;; the bytes there are malformed, which is stricter than Odin's rune_at — that ;; one hands back RUNE_ERROR and the caller carries on with a wrong character. -(defn rune-at [s [u8] i i32] (Option i32) +(defn rune-at [s [const u8] i i32] (Option i32) (if (or (< i 0) (>= i (length s))) None (let [r (decode-rune (slice s i (length s)))] @@ -1419,7 +1419,7 @@ let source = {flan| ;; ;; A malformed byte counts as one, which is what a replacement-character ;; renderer would draw, so this agrees with what the screen shows. -(defn rune-count [s [u8]] i32 +(defn rune-count [s [const u8]] i32 (let [i 0 n 0] (while (< i (length s)) @@ -1428,7 +1428,7 @@ let source = {flan| (set n (+ n 1)))) n)) -(defn valid-utf8? [s [u8]] bool +(defn valid-utf8? [s [const u8]] bool (let [i 0] (while (< i (length s)) (let [r (decode-rune (slice s i (length s)))] @@ -1507,12 +1507,12 @@ let source = {flan| ;; empty field, and `rest` is exhausted only after the last one is taken. That ;; is the rule you can state without exceptions, and the one a caller counting ;; comma-separated columns needs. -(defstruct Split [rest [u8] sep u8 more bool]) +(defstruct Split [rest [const u8] sep u8 more bool]) -(defn split-on-byte [s [u8] sep u8] Split +(defn split-on-byte [s [const u8] sep u8] Split (Split {.rest s .sep sep .more true})) -(defn split-next [it (Ptr Split)] (Option [u8]) +(defn split-next [it (Ptr Split)] (Option [const u8]) (when (not (.more it)) (return None)) (match (index-of (.rest it) (.sep it)) @@ -1534,25 +1534,11 @@ let source = {flan| ;; the ones in the building section below; these are the forms that allocate ;; nothing, and they stay the right call when a copy is not wanted — folding a ;; comparison over two inputs beats lowering both and comparing. What is *not* -;; on offer is the third shape, lowering a [u8] in place, and it is worth -;; saying why rather than shipping it. A string -;; literal is emitted `private unnamed_addr constant` (emit.ml), so (bytes-view -;; "Hello") is a [u8] pointing straight into read-only memory. An in-place -;; lower-ascii type checks against that slice, and what happens next depends -;; on the optimiser — which is the worst of the available answers. Measured, -;; with (set (at (bytes-view "Hi") 0) \h): -;; -;; -O0 the store is emitted against the constant and the program takes -;; SIGSEGV. -;; -O2 LLVM deletes the store as undefined behaviour and the program -;; carries on and prints "Hi". -;; -;; So the same source either dies or silently does nothing depending on a -;; flag, and the -O2 half is the quiet-wrongness class this file keeps -;; refusing elsewhere. (bytes s) answers a writable copy now for exactly this -;; reason; these byte functions stay the right call when no copy is wanted, -;; and a caller that really does own its buffer writes the two-line loop -;; itself over storage it can see the declaration of. +;; on offer is the third shape, lowering a [u8] in place: the text a caller +;; has is most often a (bytes-view s), which is a [const u8] because a string +;; literal's bytes are in read-only memory, and an in-place lower could not +;; take it. (bytes s) is the writable copy; a caller that owns its buffer +;; writes the two-line loop itself. ;; ;; ASCII only, and only the 26 letters: case outside ASCII is not a byte ;; operation at all — it is per-code-point, it is not length-preserving (ß @@ -1567,7 +1553,7 @@ let source = {flan| ;; Case-insensitive comparison as a fold over both inputs, which is the useful ;; half of to_lower and needs no storage at all: comparing two lowered copies ;; is what a caller wanted, and this is that answer without either copy. -(defn bytes-ci=? [a [u8] b [u8]] bool +(defn bytes-ci=? [a [const u8] b [const u8]] bool (if (!= (length a) (length b)) false (do @@ -1579,7 +1565,7 @@ let source = {flan| ;; ── Ordering byte slices, and sorting them ──────────────────────────── ;; ;; The third element type the slice family covers, and the one a caller of -;; `split` actually has: a [[u8]] of fields, wanting to come out in order. +;; `split` actually has: a [[const u8]] of fields, wanting to come out in order. ;; ;; The order is bytewise-lexicographic — memcmp's, and the one every sane ;; sorted format uses. It is explicitly *not* alphabetical and not a collation: @@ -1596,7 +1582,7 @@ let source = {flan| ;; A prefix sorts before what extends it — "ab" before "abc" — which falls out ;; of running to the shorter length and then comparing lengths, and is the case ;; a loop written to (length a) alone reads off the end for. -(defn bytes i 0) @@ -1696,24 +1683,21 @@ let source = {flan| (append (addr b) (at parts i))) b)) -(defn repeat-bytes [s [u8] n i32] (Vec u8) +(defn repeat-bytes [s [const u8] n i32] (Vec u8) (let [b (vec-new u8)] (dotimes [i n] (append (addr b) s)) b)) ;; The allocating halves of the ASCII case pair. The note above lower-ascii -;; explains why lowering a [u8] *in place* is a trap — a string literal is -;; emitted into .rodata, so the store either segfaults at -O0 or is deleted at -;; -O2 — and this is the shape that has no such hole: the bytes it writes are -;; its own. -(defn to-lower [s [u8]] (Vec u8) +;; says why there is no in-place one; these write only bytes of their own. +(defn to-lower [s [const u8]] (Vec u8) (let [b (vec-new u8)] (dotimes [i (length s)] (push b (lower-ascii (at s i)))) b)) -(defn to-upper [s [u8]] (Vec u8) +(defn to-upper [s [const u8]] (Vec u8) (let [b (vec-new u8)] (dotimes [i (length s)] (push b (upper-ascii (at s i)))) @@ -1732,7 +1716,7 @@ let source = {flan| ;; choice: returning a Vec *moves* it, and the move analysis is a dead set over ;; the whole function, so a `return b` on one branch kills the binding for the ;; `b` at the foot of the other. One exit, one move. -(defn replace-bytes [s [u8] from [u8] to [u8]] (Vec u8) +(defn replace-bytes [s [const u8] from [const u8] to [const u8]] (Vec u8) (let [b (vec-new u8) i 0] (if (= (length from) 0) @@ -1757,7 +1741,7 @@ let source = {flan| ;; the other way. A return type does say it. That is a compiler gap rather than ;; a language decision, and it is written down in TODO.org, "(vec-new [u8]) is ;; refused". -(defn slices-new [] (Vec [u8]) (vec-new)) +(defn slices-new [] (Vec [const u8]) (vec-new)) ;; split, which the file used to refuse by name. The fields are slices *of the ;; input* and not copies, so nothing here owns bytes and the result dies with @@ -1769,7 +1753,7 @@ let source = {flan| ;; always yield n+1 fields, so the empty input yields one empty field and a ;; trailing separator yields a trailing empty one. That is Odin's allocating ;; strings.split and not Odin's iterator, which disagree with each other. -(defn split [s [u8] sep u8] (Vec [u8]) +(defn split [s [const u8] sep u8] (Vec [const u8]) (let [v (slices-new) it (split-on-byte s sep) going true] @@ -1929,10 +1913,9 @@ let source = {flan| ;; ;; `data` points into the program's own .rodata, exactly as a string literal ;; does, so an embed costs nothing at run time and nothing at startup. It is -;; also read-only, and the same trap the ASCII-case note above measures applies -;; here: a store through it either segfaults at -O0 or is deleted at -O2. To -;; get a mutable copy, clone the bytes into a Vec. -(defstruct EmbedFile [name string data [u8]]) +;; also read-only, so `data` is a [const u8] and a store through it is refused +;; at compile time. To get a writable copy, copy the bytes into a Vec. +(defstruct EmbedFile [name string data [const u8]]) ;; A linear scan, deliberately. A directory embed is tens of entries, the scan ;; is over names already in cache-warm .rodata, and the alternative — a @@ -1943,7 +1926,7 @@ let source = {flan| ;; It takes a slice rather than the array (embed-dir) answers, because an array ;; length is part of its type and there are no generics: write ;; (embed-find (slice assets 0 (length assets)) "brush.png"). -(defn embed-find [files [EmbedFile] name string] (Option [u8]) +(defn embed-find [files [EmbedFile] name string] (Option [const u8]) (dotimes [i (length files)] (when (bytes=? (bytes-view (.name (at files i))) (bytes-view name)) (return (Some (.data (at files i)))))) diff --git a/lib/render.ml b/lib/render.ml index f1cb9667..d45251b6 100644 --- a/lib/render.ml +++ b/lib/render.ml @@ -110,7 +110,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis let cast t x = { Tast.e = Tast.Prim (Tast.Cast t, [ x ]); ty = t; loc } in let bytes_of s = { Tast.e = Tast.Prim (Tast.Bytes, [ { Tast.e = Tast.Str s; ty = Types.String; loc } ]); - ty = Types.Slice (Types.Int Types.U8); loc } + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } in let lit s = c.emit.ebytes (bytes_of s) in let int64 n = { Tast.e = Tast.Int (n, Types.I64); ty = Types.Int Types.I64; loc } in @@ -152,10 +152,10 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis | Types.String -> [ c.emit.estr { Tast.e = Tast.Prim (Tast.Bytes, [ e ]); - ty = Types.Slice (Types.Int Types.U8); loc } ] + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } ] (* Bytes are almost always text, and escaping makes the case where they are not readable rather than a mess. *) - | Types.Slice (Types.Int Types.U8) -> [ c.emit.estr e ] + | Types.Slice (_, (Types.Int Types.U8)) -> [ c.emit.estr e ] (* An enum's members are erased to i32 before the backend sees them, so the name has to be recovered here, from the checker's table, as a chain of comparisons. Falling through to the number is not a failure: a value @@ -355,7 +355,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis (* A slice's length is not known until it runs, so this is the one case that needs a loop. The slice goes into a slot first: the expression it came from must not be evaluated once per element. *) - | Types.Slice t -> + | Types.Slice (_, t) -> let sv = c.alloc e.Tast.ty and iv = c.alloc (Types.Int Types.I32) in let local i ty = { Tast.e = Tast.Local i; ty; loc } in let len = diff --git a/lib/session.ml b/lib/session.ml index 00a4c241..2e172e5b 100644 --- a/lib/session.ml +++ b/lib/session.ml @@ -1074,8 +1074,8 @@ let eval ?(origin = "") ?pause t src : change = type emitter = { ename : string; ety : Types.t } -let emit_bytes = { ename = "flan/dev-emit"; ety = Types.Slice (Types.Int Types.U8) } -let emit_str = { ename = "flan/dev-emit-str"; ety = Types.Slice (Types.Int Types.U8) } +let emit_bytes = { ename = "flan/dev-emit"; ety = Types.Slice (Types.Mut, (Types.Int Types.U8)) } +let emit_str = { ename = "flan/dev-emit-str"; ety = Types.Slice (Types.Mut, (Types.Int Types.U8)) } let emit_i64 = { ename = "flan/dev-emit-i64"; ety = Types.Int Types.I64 } let emit_u64 = { ename = "flan/dev-emit-u64"; ety = Types.Int Types.U64 } let emit_f64 = { ename = "flan/dev-emit-f64"; ety = Types.Float Types.F64 } @@ -1289,7 +1289,7 @@ let render_locals ?(origin = "") t ~frame ~(fn : Tast.fn) ~bound let bytes_of str = { Tast.e = Tast.Prim (Tast.Bytes, [ { Tast.e = Tast.Str str; ty = Types.String; loc } ]); - ty = Types.Slice (Types.Int Types.U8); loc } + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } in let lit str = c.Render.emit.Render.ebytes (bytes_of str) in let refused = ref [] in @@ -1401,7 +1401,7 @@ let render_condition t ~(st : Tast.structure) : change * (string * string) list let bytes_of str = { Tast.e = Tast.Prim (Tast.Bytes, [ { Tast.e = Tast.Str str; ty = Types.String; loc } ]); - ty = Types.Slice (Types.Int Types.U8); loc } + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } in let lit str = c.Render.emit.Render.ebytes (bytes_of str) in let refused = ref [] in @@ -1520,7 +1520,7 @@ let step_into t (v : Tast.expr) (s : step) : (Tast.expr, string) result = { Tast.e = Tast.Int (Int64.of_int i, Types.I32); ty = Types.Int Types.I32; loc } ]); ty = el; loc } - | Types.Slice el -> + | Types.Slice (_, el) -> (* A slice's length is not in its type, so this is the one step whose range cannot be settled here. It is checked in the program, like every other index in a dev build. *) @@ -1708,7 +1708,7 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path Tast.Prim (Tast.Bytes, [ { Tast.e = Tast.Str "\n"; ty = Types.String; loc } ]); - ty = Types.Slice (Types.Int Types.U8); loc } + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } in dev_emitter.Render.ei64 addr :: dev_emitter.Render.ebytes newline :: parts @@ -2062,7 +2062,7 @@ let render_globals ?(origin = "") t ~(globals : Tast.global list) let bytes_of str = { Tast.e = Tast.Prim (Tast.Bytes, [ { Tast.e = Tast.Str str; ty = Types.String; loc } ]); - ty = Types.Slice (Types.Int Types.U8); loc } + ty = Types.Slice (Types.Mut, (Types.Int Types.U8)); loc } in let lit str = c.Render.emit.Render.ebytes (bytes_of str) in let nullary n = { Tast.e = Tast.Call (n, []); ty = Types.Unit; loc } in diff --git a/lib/types.ml b/lib/types.ml index 42a309bd..c6bc9ae7 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -18,6 +18,17 @@ type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64 type fkind = F32 | F64 +(* Whether a slice may be stored through. [[const T]] is a view that can only + be read: [bytes-view] answers one, because its bytes are a string's and a + string literal's are in read-only memory. A [[T]] converts to a + [[const T]] implicitly and never back — see [const_widens] at the bottom of + this file — so every writable view is also a readable one, and a + read-only one cannot be laundered into a writable one. The const is + shallow: a [[const [u8]]] may not have its elements replaced, but each + element is a writable [[u8]] of its own. Both are the same two words at + run time; only the checker reads the flag. *) +type access = Mut | Const + type t = | Int of ikind | Float of fkind @@ -29,7 +40,7 @@ type t = (* A C enum: an i32 at run time, but its own type, so a keyword at a call site has something to resolve against and a plain integer does not fit. *) | Enum of string - | Slice of t (* [T] ptr+len, non-owning *) + | Slice of access * t (* [T] [const T] ptr+len, non-owning *) | Array of int64 * t (* [n T] inline, a value, copies *) | Map of t * t (* (Map K V) *) | Ptr of t (* (Ptr T) *) @@ -179,7 +190,7 @@ let rec equal a b = one dyn type the way there is one string type. *) | Bool, Bool | String, String | Unit, Unit | Never, Never | Dyn, Dyn -> true | Named x, Named y | Enum x, Enum y -> String.equal x y - | Slice x, Slice y -> equal x y + | Slice (a, x), Slice (b, y) -> a = b && equal x y | Array (n, x), Array (m, y) -> Int64.equal n m && equal x y | Map (k, v), Map (k', v') -> equal k k' && equal v v' | Ptr x, Ptr y -> equal x y @@ -204,7 +215,8 @@ let rec to_string = function | Unit -> "()" | Never -> "Never" | Named n | Enum n -> n - | Slice t -> "[" ^ to_string t ^ "]" + | Slice (Mut, t) -> "[" ^ to_string t ^ "]" + | Slice (Const, t) -> "[const " ^ to_string t ^ "]" | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t) | Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v) | Ptr t -> "(Ptr " ^ to_string t ^ ")" @@ -318,3 +330,19 @@ let join a b = else if widens_to ~from:a ~into:b then Some b else if widens_to ~from:b ~into:a then Some a else None + +(* The one conversion between the two slice types, and it goes one way: a + [[T]] may be seen as a [[const T]], because a view that can only be read + asks less of its bytes than one that can be written. Under a const slice + the same holds one level down — [[[u8]]] reads as [[const [const u8]]] — + because nothing can be stored through the outer view to put a read-only + slice where the writable original expects a writable one. Under a writable + slice it does not: a [[[u8]]] seen as [[[const u8]]] could have a + read-only slice stored into it and read back out as a [[u8]]. Like + [widens_to] this is a predicate and not a loosening of [equal]; the + caller is [Check.expect], which retypes the value — the two words are the + same at run time. *) +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 diff --git a/lib/x86.ml b/lib/x86.ml index 9d6f15a3..f971a0b2 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -2540,7 +2540,7 @@ and elements f (base : loc) (ty : Types.t) (is : Tast.expr list) : loc = | i :: rest -> let elem = match ty with - | Types.Array (_, el) | Types.Slice el | Types.Ptr el -> el + | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el | Types.String -> Types.Int Types.U8 | t -> unsupported "index into %s" (Types.to_string t) in @@ -2838,7 +2838,7 @@ and check_cast f (loc : Loc.t) (src : Types.fkind) (k : Types.ikind) = and element f (base : loc) (ty : Types.t) (i : Tast.expr) : loc = let elem = match ty with - | Types.Array (_, el) | Types.Slice el | Types.Ptr el -> el + | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el | Types.String -> Types.Int Types.U8 | t -> unsupported "index into %s" (Types.to_string t) in @@ -3212,7 +3212,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst = | Tast.Slice, [ a; lo; hi ] -> let elem = match a.Tast.ty with - | Types.Array (_, el) | Types.Slice el -> el + | Types.Array (_, el) | Types.Slice (_, el) -> el | Types.String -> Types.Int Types.U8 | ty -> unsupported "slice of %s" (Types.to_string ty) in diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c index bbd914eb..8fb65c7c 100644 --- a/runtime/flan_dev.c +++ b/runtime/flan_dev.c @@ -2074,7 +2074,7 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) { } { static const char why[] = - "\nflan: a write through a read-only slice (bytes-view of a literal), " + "\nflan: a write through a pointer into read-only memory, " "a null, or a stack overflow\n"; crash_puts(why, sizeof why - 1); } diff --git a/spike/x86/p4-convention.flan b/spike/x86/p4-convention.flan index 47ad249e..89372936 100644 --- a/spike/x86/p4-convention.flan +++ b/spike/x86/p4-convention.flan @@ -13,7 +13,7 @@ (defn eight [a i64 b i64 c i64 d i64 e i64 f i64 g i64 h i64] i64 (+ (+ (+ a b) (+ c d)) (+ (+ e f) (+ g h)))) -(defn taglen [s [u8]] i64 +(defn taglen [s [const u8]] i64 (i64 (length s))) (defn main [] i32 diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index da96bf72..c6b9a598 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -94,30 +94,15 @@ forever="dev-loop dev-watch dev-chatty agent-auto" # in the epilogue that every exit already went through. The five are in the # sweep now and they are five of the MATCHes. -# The ones whose whole point is a fault, and which therefore cannot be compared -# at this sweep's optimisation level. Both write through a bytes-view of a -# string literal, which is a store into .rodata: measured here, LLVM exits 0 -# having printed the unmodified literal and this backend exits 139, because the -# store is undefined and the optimiser deleted it on one side and there is no -# optimiser on the other. That is not a lowering disagreement. At -O0 the two -# agree exactly -- 139, no output, both backends -- and test_acceptance.ml's -# dies_segv rows pin precisely that, on both backends, which is the coverage -# this sweep would otherwise be duplicating at the one level where, as that -# file's own comment puts it, there is nothing left to pin but the UB. -# -# Excluded by name rather than by building these two at -O0 here, and the -# reason is the coverage and not the counts: a per-name -O0 list would move the -# counts exactly as much as this does, so that is no argument at all. The -# argument is that dies_segv already builds both of them at -O0, on both -# backends, and asserts the exit status and the empty output -- everything this -# sweep would check, in the file where the ruling is written down. -# -# One more thing about dev-segv, which is a reason to keep it out of the -# comparison rather than a reason for this list: it calls agent/start, so it +# The one whose whole point is a fault, and which therefore cannot be compared +# at this sweep's optimisation level. dev-segv stores through a pointer to a +# string literal's bytes, which is a store into .rodata: LLVM at -O2 deletes it +# as undefined and exits 0, and this backend has no optimiser and exits 139. +# That is not a lowering disagreement. test_dev.ml builds it in a dev session, +# where the fault is the thing asserted. It also calls agent/start, so it # leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks -# in the break loop instead of dying -- which is a forever-list problem, met -# here by a program that was never going to be compared anyway. -faults="bytes-view-write dev-segv" +# in the break loop instead of dying. +faults="dev-segv" TIMEOUT=${TIMEOUT:-20} diff --git a/test/programs/algorithms.flan b/test/programs/algorithms.flan index 33d339c1..9f4aabea 100644 --- a/test/programs/algorithms.flan +++ b/test/programs/algorithms.flan @@ -13,7 +13,7 @@ (print " ")) (println "")) -(defn show-fields [s [[u8]]] () +(defn show-fields [s [[const u8]]] () (dotimes [i (length s)] (print (string (at s i))) (print " ")) diff --git a/test/programs/bounds-condition.flan b/test/programs/bounds-condition.flan index 646032ff..6f394c56 100644 --- a/test/programs/bounds-condition.flan +++ b/test/programs/bounds-condition.flan @@ -85,7 +85,7 @@ (set frames (+ frames 1))) (continue [] (set skipped (+ skipped 1))))) -(defn slice-frame [s [u8] lo i32 hi i32] () +(defn slice-frame [s [const u8] lo i32 hi i32] () (restart-case (do (show "slice" (i64 (length (slice s lo hi)))) (set frames (+ frames 1))) diff --git a/test/programs/bytes-view-write.flan b/test/programs/bytes-view-write.flan index 23bfc59a..68184fc6 100644 --- a/test/programs/bytes-view-write.flan +++ b/test/programs/bytes-view-write.flan @@ -1,19 +1,11 @@ -;;;; A store through (bytes-view "literal") lands in the string constant's -;;;; own storage, which both backends emit read-only — LLVM as a `constant` -;;;; global, x86 in .rodata — so the write traps where it happens instead of -;;;; corrupting the literal. Pinned at -O0 on both backends, where the store -;;;; is really emitted; at -O2 LLVM deletes it as undefined behaviour, which -;;;; is why this program has no -O2 row. The trap itself (SIGSEGV on a -;;;; read-only page) is the defined consequence of the emission, not a bet on -;;;; anything further. -;;;; -;;;; If this ever exits 0, string data has become writable somewhere and the -;;;; read-only-by-convention story of bytes-view is silently gone. +;;;; A store through (bytes-view "literal") is refused at compile time: +;;;; bytes-view answers a [const u8], because a string literal's bytes are in +;;;; read-only memory, where the store would trap at -O0 and be deleted as +;;;; undefined at -O2. test_acceptance.ml asserts the refusal; nothing here is +;;;; ever built. (defn main [] i32 (let [v (bytes-view "INSERTIONSORT")] (set (at v 0) \Z) - ;; Never reached: the store above traps. Printing anyway makes a failure - ;; loud — output where none was expected. (print (string v)) 0)) diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan new file mode 100644 index 00000000..3d83ebde --- /dev/null +++ b/test/programs/const-slice.flan @@ -0,0 +1,49 @@ +;;;; [const T]: a slice that can only be read. bytes-view answers one, a [T] +;;;; converts to one wherever one is wanted, and slicing one keeps it +;;;; read-only. Nothing about it exists at run time, so this prints the same +;;;; on every backend and at every level. + +(defn total [s [const i32]] i64 + (let [t (i64 0)] + (dotimes [i (length s)] + (set t (+ t (at s i)))) + t)) + +;; A generic over a read-only slice takes a writable one too. +(defn first-of [s [const $t]] $t (at s 0)) + +(defn widths [parts [const [const u8]]] i32 + (let [n 0] + (dotimes [i (length parts)] + (set n (+ n (length (at parts i))))) + n)) + +(defn main [] i32 + (let [xs [3 1 2] + w (slice xs) + r (bytes-view "hello, world") + head (slice r 0 5) + tail (slice r 7) + names (vec-new [const u8])] + (sort w) + (println (total w) (total (slice w 1))) + (println (first-of w) (first-of (bytes-view "z"))) + (println (string head) (string tail) (length head)) + (println (bytes=? head (bytes-view "hello")) (starts-with? r head)) + (push names head) + (push names tail) + (println (widths (slice names))) + ;; A writable [[u8]] meets [const [const u8]] too: the outer view is + ;; read-only, so nothing can put a read-only slice into it. + (let [a (bytes "ab") + b (bytes "cde") + both [a b]] + (println (widths (slice both))) + (set (at a 0) \A) + (println (string a))) + (let [f (split (bytes-view "b,a,c") \,)] + (sort-bytes (slice f)) + (println (string (slice (join (slice f) (bytes-view "-")))))) + (println (at r 0)) + (free names)) + 0) diff --git a/test/programs/dev-segv.flan b/test/programs/dev-segv.flan index 528263cf..1ea5ca31 100644 --- a/test/programs/dev-segv.flan +++ b/test/programs/dev-segv.flan @@ -1,17 +1,22 @@ -;;;; The dogfooding crash, replayed on purpose: a write through a bytes-view -;;;; of a string literal lands in read-only memory and takes SIGSEGV. In a -;;;; dev session that used to kill the whole process — daemon, compiler and +;;;; The dogfooding crash, replayed on purpose: a store through a pointer to +;;;; a string literal's bytes lands in read-only memory and takes SIGSEGV. In +;;;; a dev session that used to kill the whole process — daemon, compiler and ;;;; socket together, with no message at all. The dev build's crash handler ;;;; turns it into the same park the no-channel traps take: one line naming ;;;; the address and the frame, then the break loop, with the daemon alive ;;;; and answering behind it. There is no restart to list — a faulting ;;;; instruction has nowhere to resume at — which is the same empty-list ;;;; shape dev-trap-null-alloc.flan pins for free-all. +;;;; +;;;; Through a pointer, because a store through the [const u8] itself is +;;;; refused at compile time; a (Ptr T) is the C boundary, where nothing is +;;;; checked. (import agent "vendor:agent") (defn main [] i32 (agent/start "/tmp/flan-dev-segv-fallback.sock") - (let [v (bytes-view "INSERTIONSORT")] - (set (at v 0) \Z) + (let [v (bytes-view "INSERTIONSORT") + p (addr (at v 0))] + (set (deref p) \Z) (print (string v)) 0)) diff --git a/test/programs/edn.flan b/test/programs/edn.flan index 9b39d880..10757311 100644 --- a/test/programs/edn.flan +++ b/test/programs/edn.flan @@ -70,11 +70,11 @@ ;; ── The worked example: a struct read by hand ─────────────────────── -;; `name` is a [u8] and not a copy of one, so an Enemy is only valid while the +;; `name` is a [const u8] and not a copy of one, so an Enemy is only valid while the ;; buffer it was read out of is. That is the lifetime contract from the package ;; header, and it is what a struct reader inherits by using slices. (defstruct Enemy - [name [u8] + [name [const u8] hp i32 speed f32 boss? bool]) diff --git a/test/programs/pkg-return.flan b/test/programs/pkg-return.flan index 6e76be68..22654d82 100644 --- a/test/programs/pkg-return.flan +++ b/test/programs/pkg-return.flan @@ -13,7 +13,7 @@ (defstruct Local [n i32]) ;;; The case that used to fail: a package struct as the declared return type. -(defn fresh [src [u8]] edn/Cursor (edn/cursor src)) +(defn fresh [src [const u8]] edn/Cursor (edn/cursor src)) ;;; And the one that must keep working: a lowercase qualified name in the same ;;; position is an expression, not a type. diff --git a/test/programs/utf8.flan b/test/programs/utf8.flan index 4ecbd325..799d12e3 100644 --- a/test/programs/utf8.flan +++ b/test/programs/utf8.flan @@ -50,7 +50,7 @@ ;; code/width/ok, so a wrong answer names which of the three it got wrong ;; rather than just failing. -(defn show-dec [s [u8]] () +(defn show-dec [s [const u8]] () (let [r (decode-rune s)] (print (.code r)) (print "/") (print (.width r)) (print "/") @@ -78,7 +78,7 @@ (print x) (print " ")) -(defn show-split [s [u8] sep u8] () +(defn show-split [s [const u8] sep u8] () (let [it (split-on-byte s sep) going true] (while going diff --git a/test/programs/vec-new-shadow.flan b/test/programs/vec-new-shadow.flan index 9be6e154..cc368677 100644 --- a/test/programs/vec-new-shadow.flan +++ b/test/programs/vec-new-shadow.flan @@ -6,7 +6,7 @@ (defn main [] i32 (let [x 7 - v (builtin/vec-new [u8])] + v (builtin/vec-new [const u8])] (println (vec-new [x])) (push v (bytes-view "ab")) (println (length (at v 0))) diff --git a/test/programs/vec-new-type.flan b/test/programs/vec-new-type.flan index 5d338a70..a809bd26 100644 --- a/test/programs/vec-new-type.flan +++ b/test/programs/vec-new-type.flan @@ -5,11 +5,11 @@ (defn main [] i32 (let [a (arena-new 4096) - words (vec-new [u8]) + words (vec-new [const u8]) pairs (vec-new [2 i32]) ptrs (vec-new (Ptr i32)) opts (vec-new (Option i64) a) - m (map-new string [u8]) + m (map-new string [const u8]) x (i32 7)] (push words (bytes-view "ab")) (push words (bytes-view "cde")) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 6ced8956..b01c1ca5 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -840,26 +840,33 @@ let () = "programs/bytes-copy.flan" bytes_copy_out; outputs ~x86:true "bytes copies, bytes-view aliases, --x86" "programs/bytes-copy.flan" bytes_copy_out; - (* The other half of the same ruling: a store through a bytes-view of a - literal traps, identically on both backends, because both emit string - data read-only. -O0 only — at -O2 LLVM deletes the store as UB, so - there is nothing there to pin except the UB itself. 139 is the shell's - 128+SIGSEGV. *) - let dies_segv name path ~x86 = - let exe = compile ~opt:"-O0" ~x86 path in - let code, text = run exe None in - if code <> 139 || text <> "" then begin - incr failures; - Printf.printf - "FAIL %s\n got: %S (exit %d)\n wanted: %S (exit 139)\n" - name text code "" - end; - (try Sys.remove exe with Sys_error _ -> ()) + (* The other half of the same ruling: a store through a bytes-view is + refused before anything is built, because bytes-view answers a + [const u8]. It used to compile and trap at -O0 on both backends, and be + deleted as undefined at -O2. *) + (let path = "programs/bytes-view-write.flan" in + match + Check.program (Load.program ~file:path (Reader.read_file path)).Load.decls + with + | _ -> + incr failures; + Printf.printf "FAIL a write through bytes-view is refused\n" + | exception Loc.Error { Loc.dmsg = m; _ } -> + if not (contains m "this writes through a [const u8]") then begin + incr failures; + Printf.printf + "FAIL a write through bytes-view is refused\n said: %S\n" m + end); + (* [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" in - dies_segv "a write through bytes-view traps, -O0" - "programs/bytes-view-write.flan" ~x86:false; - dies_segv "a write through bytes-view traps, --x86" - "programs/bytes-view-write.flan" ~x86:true; + outputs "const slices" "programs/const-slice.flan" const_slice_out; + outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan" + const_slice_out; + outputs ~x86:true "const slices, --x86" "programs/const-slice.flan" + const_slice_out; (* (string b). The conversion emits nothing — String and Slice _ are the same %slice — so the rows are about length and ownership rather than arithmetic: a number round-tripped, an empty slice, sub-views whose diff --git a/test/test_dev.ml b/test/test_dev.ml index 169a2eee..803e8104 100644 --- a/test/test_dev.ml +++ b/test/test_dev.ml @@ -442,7 +442,7 @@ let () = [Rune] also pins the spelling — the types read exactly as [defs] spells a signature, because both go through [Types.to_string]. *) let r = request c "(:op \"layout\" :type \"Split\")" in - if fields r <> [ "rest [u8]"; "sep u8"; "more bool" ] then + if fields r <> [ "rest [const u8]"; "sep u8"; "more bool" ] then fail "Split's fields: %s" (String.concat ", " (fields r)); let r = request c "(:op \"layout\" :type \"Nonesuch\")" in @@ -1922,7 +1922,7 @@ let () = if refault then begin let faulting = "(:op \"eval-expr\" :code \ - \"(let [v (bytes-view \\\"refault\\\")] (set (at v 0) 90) 1)\" \ + \"(let [v (bytes-view \\\"refault\\\") p (addr (at v 0))] (set (deref p) 90) 1)\" \ :file \"/tmp/buf.flan\")" in (match ask faulting with _ -> () | exception _ -> ()); @@ -2028,8 +2028,9 @@ let () = word. The dev build's crash handler (flan_dev_crash_enable) enters the same trap hook the six no-channel refusals use, so everything trap_park asserts for them holds here too: stopped and describable, an eval still - answered, a resume refused. The program writes through bytes-view, - which is the surviving spelling of that crash. *) + answered, a resume refused. The program writes through a pointer to + a literal's bytes, which is the surviving spelling of that crash: a + store through the bytes-view itself no longer compiles. *) trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" []; (* ── The locals of a stopped frame ─────────────────────────────── *) diff --git a/test/test_flan.ml b/test/test_flan.ml index d7857883..1bc8d222 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -468,7 +468,23 @@ let () = | { d = Defn { praw = Some [ Pname ("x", _); Ptype t ]; _ }; _ } -> t.t | _ -> failwith "bad type test" in - (match ty "[u8]" with Tslice _ -> () | _ -> check "[T] is a slice" false); + (match ty "[u8]" with + | Tslice (false, _) -> () | _ -> check "[T] is a slice" false); + (* [const] is reserved, so this is never [n T] with a length named const. *) + (match ty "[const u8]" with + | Tslice (true, { t = Tname "u8"; _ }) -> () + | _ -> check "[const T] is a read-only slice" false); + (match ty "[const [const u8]]" with + | Tslice (true, { t = Tslice (true, _); _ }) -> () + | _ -> check "[const [const T]] nests" false); + (match ty "[const]" with + | exception Loc.Error { Loc.dmsg; _ } + when contains dmsg "[const] names no element type" -> () + | _ -> check "[const] alone is refused" false); + (match ty "[const 4 u8]" with + | exception Loc.Error { Loc.dmsg; _ } + when contains dmsg "has no read-only form" -> () + | _ -> check "[const 4 u8] is refused" false); (match ty "[4 f32]" with | Tarray (Lint 4L, _) -> () | _ -> check "[n T] is an array" false); (match ty "[rows [cols u32]]" with @@ -568,7 +584,7 @@ let () = (match (parse_decl "(defmacro m [& args] (at args 0))").d with | Defn { name = "m"; params = [ p ]; ret = Some r; _ } -> (match p.fty.t, r.t with - | Tslice { t = Tname "Form"; _ }, Tname "Form" -> () + | Tslice (false, { t = Tname "Form"; _ }), Tname "Form" -> () | _ -> check "defmacro is [Form] -> Form" false) | _ -> check "defmacro parses as a defn" false); @@ -578,7 +594,7 @@ let () = (match (parse_decl "(defmacro m [[a b] c & rest] (at rest 0))").d with | Defn { name = "m"; params = [ p ]; ret = Some r; _ } -> (match p.fty.t, r.t with - | Tslice { t = Tname "Form"; _ }, Tname "Form" -> () + | Tslice (false, { t = Tname "Form"; _ }), Tname "Form" -> () | _ -> check "a parameter list is still [Form] -> Form" false) | _ -> check "a macro with a parameter list parses as a defn" false); @@ -1052,7 +1068,7 @@ let () = runs no passes over it. *) infers "array-fill of nothing" "(array-fill [0] 1)" "[0 i32]"; infers "bytes of a string" "(bytes \"hi\")" "[u8]"; - infers "bytes-view of a string" "(bytes-view \"hi\")" "[u8]"; + infers "bytes-view of a string" "(bytes-view \"hi\")" "[const u8]"; infers "length is i32" "(length (bytes \"hi\"))" "i32"; infers "slice of a slice" "(slice (bytes \"hi\") 0 1)" "[u8]"; infers "slice of the whole" "(slice (bytes \"hi\"))" "[u8]"; @@ -2197,6 +2213,63 @@ let () = "(defn g [b [u8]] i32 (length b)) (defn f [s string] i32 (g (slice s)))" ~needle:"expected [u8], found string"; + (* [const T]: a view that can only be read. Every route to a store through + one is refused, and none of the reads is. *) + infers "a const slice slices to a const slice" + "(slice (bytes-view \"hello\") 1 3)" "[const u8]"; + infers "vec-new reads [const u8] as a type" "(vec-new [const u8])" + "(Vec [const u8])"; + infers "map-new reads [const u8] as a type" "(map-new string [const u8])" + "(Map string [const u8])"; + rejects_check "set through a const slice" + "(defn f [s [const u8]] () (set (at s 0) 65))" + ~needle:"this writes through a [const u8]"; + rejects_check "set through bytes-view" + "(defn f [] () (let [v (bytes-view \"Hi\")] (set (at v 0) \\h)))" + ~needle:"this writes through a [const u8]"; + rejects_check "set through a const slice, two indices" + "(defn f [s [const [2 i32]]] () (set (at s 0 1) 5))" + ~needle:"this writes through a [const [2 i32]]"; + rejects_check "set through an array element of a const slice" + "(defn f [s [const [2 i32]]] () (set (at (at s 0) 1) 5))" + ~needle:"this writes through a [const [2 i32]]"; + rejects_check "replace an array element of a const slice whole" + "(defn f [s [const [2 i32]]] () (set (at s 0) [1 2]))" + ~needle:"this writes through a [const [2 i32]]"; + rejects_check "set a field of a const slice's element" + "(defstruct P [x i32]) (defn f [s [const P]] () (set (.x (at s 0)) 5))" + ~needle:"this writes through a [const P]"; + rejects_check "a const slice is not a writable one" + "(defn g [b [u8]] () (set (at b 0) 1)) (defn f [s [const u8]] () (g s))" + ~needle:"expected [u8], found [const u8]"; + rejects_check "and the refusal names the copy" + "(defn g [b [u8]] () (set (at b 0) 1)) (defn f [s [const u8]] () (g s))" + ~needle:"(bytes (string v)) copies v"; + rejects_check "a generic writer does not take a const slice" + "(defn f [s [const i32]] () (sort s))" + ~needle:"sort takes a slice it may write through"; + rejects_check "a const slice does not cross into dyn" + "(defn f [s [const i64]] dyn s)" + ~needle:"a [const i64] can only be read"; + 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 "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]. *) + accepts "store through an element of a const slice of slices" + "(defn f [s [const [u8]]] () (set (at (at s 0) 1) 5))"; + accepts "a writable slice is a const one" + "(defn g [b [const u8]] u8 (at b 0)) (defn f [s [u8]] u8 (g s))"; + accepts "and so is a string's bytes, at a prelude reader" + "(defn f [s string] bool (bytes=? (bytes-view s) (bytes-view \"x\")))"; + accepts "under a const slice the element converts too" + "(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))"; + accepts "the address of a const element, for C" + "(defn f [s [const u8]] (Ptr u8) (addr (at s 0)))"; + accepts "a generic reader takes both" + "(defn f [a [const i32] b [i32]] i64 (+ (sum-i32 a) (sum-i32 b)))"; + (* (slice-from-ptr p n). The one form in the language whose central claim the compiler cannot check — whether n is the truth about what p addresses — so what it does check is worth pinning: the argument really is a pointer, the diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index e5829224..fbf1563e 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -440,7 +440,7 @@ let dev_sweep () = handler's line, and that is the assertion. And it has to be built at -O0. At the sweep's -O2 the write through a - bytes-view of a string literal does not fault at all — measured, both + pointer to a string literal's bytes does not fault at all — measured, both builds print the unmodified string — so a case that is about what happens on a fault has to be compiled where the fault happens. Same family as the -O0/-O2 split [unchecked_controls] records for bounds.flan. diff --git a/vendor/edn/edn.flan b/vendor/edn/edn.flan index e7cb7058..a9f14590 100644 --- a/vendor/edn/edn.flan +++ b/vendor/edn/edn.flan @@ -1,4 +1,4 @@ -;;;; An EDN tokenizer, in Flan, over a [u8]. +;;;; An EDN tokenizer, in Flan, over a [const u8]. ;;;; ;;;; This is the bottom layer of a reader. It answers one question — "what is ;;;; the next token, and where" — and it answers it without allocating @@ -161,7 +161,7 @@ ;; usable underline position even though `text` is narrower than the token. (defstruct Token [kind i32 - text [u8] + text [const u8] pos i32]) ;; The cursor owns no storage either: `src` is the caller's buffer. @@ -171,7 +171,7 @@ ;; left to a parser, because `[1 2}` is malformed in a way only the tokenizer ;; has the position for. (defstruct Cursor - [src [u8] + [src [const u8] pos i32 err i32 err-pos i32 @@ -180,7 +180,7 @@ ;; ── Construction ──────────────────────────────────────────────────── -(defn cursor [src [u8]] Cursor +(defn cursor [src [const u8]] Cursor (Cursor {.src src .pos 0 .err err-none .err-pos 0 .depth 0})) (defn ok? [c (Ptr Cursor)] bool @@ -266,7 +266,7 @@ ;; text of their own — eof, error, and every delimiter. It is still a slice of ;; the input rather than a slice of nothing, so `text` has one meaning for all ;; token kinds. -(defn- empty-at [c (Ptr Cursor) p i32] [u8] +(defn- empty-at [c (Ptr Cursor) p i32] [const u8] (slice (.src c) p p)) (defn- token [c (Ptr Cursor) kind i32 lo i32 hi i32 p i32] Token diff --git a/vendor/edn/provide.flan b/vendor/edn/provide.flan index f9456dc6..ab7b5c80 100644 --- a/vendor/edn/provide.flan +++ b/vendor/edn/provide.flan @@ -80,7 +80,7 @@ ;; buffer costs nothing to produce. A person reading a refusal wants a line and ;; a column, so the newlines before the offset are counted here — once per ;; refusal, which is as often as this is ever called. -(defn- where [src [u8] pos i32] string +(defn- where [src [const u8] pos i32] string (let [line (i64 1) col (i64 1) i (i32 0)] @@ -212,7 +212,7 @@ ;; One value, from the cursor's current position, consumed. `name` is what a ;; struct here would be called; `src` is the whole buffer, for the positions a ;; refusal names. -(defn- derive [c (Ptr Cursor) name string src [u8]] Derived +(defn- derive [c (Ptr Cursor) name string src [const u8]] Derived (let [t (next c)] (when (not (ok? c)) (return (derived-bad @@ -242,7 +242,7 @@ ;; decides; every one after it is compared against that decision and both ;; positions are named when they disagree, because "heterogeneous" without ;; saying where sends someone to read the whole file. -(defn- derive-vec [c (Ptr Cursor) name string at-pos i32 src [u8]] Derived +(defn- derive-vec [c (Ptr Cursor) name string at-pos i32 src [const u8]] Derived (when (at-byte? c \]) (return (derived-bad (joined3 "the empty vector at " (where src at-pos) @@ -291,7 +291,7 @@ ;; A set becomes `(Map T bool)`, so its elements are map keys. `derive-key` is ;; where that constraint is enforced and said. -(defn- derive-set [c (Ptr Cursor) name string at-pos i32 src [u8]] Derived +(defn- derive-set [c (Ptr Cursor) name string at-pos i32 src [const u8]] Derived (when (at-byte? c \}) (return (derived-bad (joined3 "the empty set at " (where src at-pos) @@ -326,7 +326,7 @@ ;; fixed array, which is one where a Vec is not; anything else is refused here ;; rather than at the `(Map ...)` the caller would build out of it, because a ;; map-key refusal names a type nobody wrote. -(defn- derive-key [c (Ptr Cursor) name string src [u8]] Derived +(defn- derive-key [c (Ptr Cursor) name string src [const u8]] Derived (when (at-byte? c \[) (return (derive-array c name src))) (let [d (derive c name src)] @@ -342,7 +342,7 @@ ;; of the set has to be the same length as well as the same shape — which falls ;; out of the type comparison the caller already makes, since the length is in ;; the type it compares. -(defn- derive-array [c (Ptr Cursor) name string src [u8]] Derived +(defn- derive-array [c (Ptr Cursor) name string src [const u8]] Derived (let [open (next c)] (when (at-byte? c \]) (return (derived-bad @@ -379,7 +379,7 @@ (expect c tok-vec-close) arr))))))) -(defn- disagreement [what string src [u8] at-pos i32 n i64 +(defn- disagreement [what string src [const u8] at-pos i32 n i64 first Form second Form] string (joined3 (joined3 "the " what " at ") (where src at-pos) @@ -400,7 +400,7 @@ ;; differently is the two arms a hand-written reader had no reason to have — a ;; key that is not a field of the struct, and a field the file did not have. ;; Both signal SchemaDrift. See the note over that type. -(defn- derive-map [c (Ptr Cursor) name string at-pos i32 src [u8]] Derived +(defn- derive-map [c (Ptr Cursor) name string at-pos i32 src [const u8]] Derived (when (at-byte? c \}) (return (derived-bad (joined3 "the empty map at " (where src at-pos) @@ -543,7 +543,7 @@ _ (refuse "defedn's first argument is the name of the struct to declare, written as a name")) _ (refuse "defedn's second argument is the path to the data file, written as a string literal — the file is read while this is being compiled, so there is nothing here to compute a path from")))) -(defn- provide [name string path string src [u8]] Form +(defn- provide [name string path string src [const u8]] Form (let [cur (cursor src) d (derive (addr cur) name src)] (if (bad? d) @@ -560,7 +560,7 @@ ;; fields are built in, because a string field is a copy and a Vec ;; field is an allocation — spec-memory's rule, and the reason the ;; destination is never implicit. - (defn ~bname [b [u8] a Allocator] ~sname + (defn ~bname [b [const u8] a Allocator] ~sname (let [c (cursor b) out (~rname (addr c) a)] ;; The cursor is made and dropped here, so this is the only diff --git a/vendor/edn/read.flan b/vendor/edn/read.flan index 1a8b0a1d..e09fb45d 100644 --- a/vendor/edn/read.flan +++ b/vendor/edn/read.flan @@ -65,7 +65,7 @@ ;; dropped here on purpose. Nothing individually owns a block in a region — ;; free-all owns all of them — so keeping the header around to free through ;; would be keeping a handle for an operation that never happens. -(defn copy-text [s [u8]] string +(defn copy-text [s [const u8]] string (let [b (vec-new u8)] (append (addr b) s) (string (slice b)))) @@ -136,7 +136,7 @@ ;; The whole document, from a byte slice. nil when the input was malformed — ;; the header says what that conflates and what to do when it matters. -(defn read [src [u8]] dyn +(defn read [src [const u8]] dyn (let [c (cursor src) t (next (addr c)) v (read-value (addr c) t)] diff --git a/vendor/json/json.flan b/vendor/json/json.flan index 57f2b4bb..647648f5 100644 --- a/vendor/json/json.flan +++ b/vendor/json/json.flan @@ -1,4 +1,4 @@ -;;;; A JSON tokenizer, in Flan, over a [u8]. +;;;; A JSON tokenizer, in Flan, over a [const u8]. ;;;; ;;;; The shape is vendor/edn's, deliberately: a Cursor over a caller's buffer, ;;;; one `next` that answers a Token, errors accumulated on the cursor with the @@ -205,7 +205,7 @@ ;; underline position even where `text` is narrower than the token. (defstruct Token [kind i32 - text [u8] + text [const u8] pos i32]) ;; The cursor owns no storage: `src` is the caller's buffer. @@ -214,7 +214,7 @@ ;; each one waits for, so that {"a": [1} fails at the brace with a position ;; rather than confusing a reader two levels up. (defstruct Cursor - [src [u8] + [src [const u8] pos i32 err i32 err-pos i32 @@ -223,7 +223,7 @@ ;; ── Construction ──────────────────────────────────────────────────── -(defn cursor [src [u8]] Cursor +(defn cursor [src [const u8]] Cursor (Cursor {.src src .pos 0 .err err-none .err-pos 0 .depth 0})) (defn ok? [c (Ptr Cursor)] bool @@ -313,7 +313,7 @@ ;; An empty slice of src, positioned at p. Used for the tokens that have no ;; text of their own — eof, error, and every delimiter — so that `text` has one ;; meaning for every token kind and not two. -(defn- empty-at [c (Ptr Cursor) p i32] [u8] +(defn- empty-at [c (Ptr Cursor) p i32] [const u8] (slice (.src c) p p)) (defn- token [c (Ptr Cursor) kind i32 lo i32 hi i32 p i32] Token diff --git a/vendor/json/provide.flan b/vendor/json/provide.flan index 8d85892b..c8e99c3b 100644 --- a/vendor/json/provide.flan +++ b/vendor/json/provide.flan @@ -63,7 +63,7 @@ ;; The tokenizer answers byte offsets. A person reading a refusal wants a line ;; and a column, so the newlines before the offset are counted here — once per ;; refusal, which is as often as this is ever called. -(defn- where [src [u8] pos i32] string +(defn- where [src [const u8] pos i32] string (let [line (i64 1) col (i64 1) i (i32 0)] @@ -173,7 +173,7 @@ ;; ── Deriving ──────────────────────────────────────────────────────── -(defn- derive [c (Ptr Cursor) name string src [u8]] Derived +(defn- derive [c (Ptr Cursor) name string src [const u8]] Derived (let [t (next c)] (when (not (ok? c)) (return (derived-bad @@ -202,7 +202,7 @@ ;; every one after it is compared against that, and both positions are named ;; when they disagree — "heterogeneous" on its own sends someone to read the ;; whole file. -(defn- derive-array [c (Ptr Cursor) name string at-pos i32 src [u8]] Derived +(defn- derive-array [c (Ptr Cursor) name string at-pos i32 src [const u8]] Derived (when (at-byte? c \]) (return (derived-bad (joined3 "the empty array at " (where src at-pos) @@ -248,7 +248,7 @@ ;; ── An object, which is a struct ──────────────────────────────────── -(defn- derive-object [c (Ptr Cursor) name string at-pos i32 src [u8]] Derived +(defn- derive-object [c (Ptr Cursor) name string at-pos i32 src [const u8]] Derived (when (at-byte? c \}) (return (derived-bad (joined3 "the empty object at " (where src at-pos) @@ -349,7 +349,7 @@ (defn key=? [t Token s string] bool (bytes=? (.text t) (bytes-view s))) -(defn- has-escape? [s [u8]] bool +(defn- has-escape? [s [const u8]] bool (dotimes [i (length s)] (when (= (at s i) \\) (return true))) @@ -358,7 +358,7 @@ ;; What a field name may be made of. Deliberately narrower than what the reader ;; would accept: this is the set a *person* would recognise as a name, and a ;; member called "a b" or "x.y" has no field it could become. -(defn- name-like? [s [u8]] bool +(defn- name-like? [s [const u8]] bool (when (= (length s) 0) (return false)) (dotimes [i (length s)] @@ -372,7 +372,7 @@ ;; A copy of a token's raw text as a string. The Vec header is dropped here on ;; purpose: this runs inside the compiler, where an expansion is bounded by the ;; size of the program being compiled. -(defn- copy-of [s [u8]] string +(defn- copy-of [s [const u8]] string (let [b (vec-new u8)] (append (addr b) s) (string (slice b)))) @@ -424,7 +424,7 @@ _ (refuse "defjson's first argument is the name of the struct to declare, written as a name")) _ (refuse "defjson's second argument is the path to the data file, written as a string literal — the file is read while this is being compiled, so there is nothing here to compute a path from")))) -(defn- provide [name string path string src [u8]] Form +(defn- provide [name string path string src [const u8]] Form (let [cur (cursor src) d (derive (addr cur) name src)] (if (bad? d) @@ -441,7 +441,7 @@ ;; built in: a string field is a copy and a Vec field is an ;; allocation, and spec-memory's rule is that the destination is ;; never implicit. - (defn ~bname [b [u8] a Allocator] ~sname + (defn ~bname [b [const u8] a Allocator] ~sname (let [c (cursor b) out (~rname (addr c) a)] ;; The cursor is made and dropped here, so this is the only diff --git a/vendor/raylib/raylib.flan b/vendor/raylib/raylib.flan index 1c6a5d29..8eb234c3 100644 --- a/vendor/raylib/raylib.flan +++ b/vendor/raylib/raylib.flan @@ -811,7 +811,7 @@ ;; false for it either way, so a caller that checks sees the same thing. (defonce no-image Image) -(defn load-image-from-memory [file-type string data [u8]] Image +(defn load-image-from-memory [file-type string data [const u8]] Image (if (= (length data) 0) no-image (load-image-from-memory-raw file-type (addr (at data 0)) (length data)))) @@ -1606,7 +1606,7 @@ ;; before it and `codepoint-size` is that one's length in bytes, so the ;; previous offset is `offset` minus what comes back through the pointer. At ;; offset 0 there is nothing behind it and raylib is not asked. -(defn get-codepoint-previous [text [u8] offset i32 codepoint-size (Ptr i32)] i32 +(defn get-codepoint-previous [text [const u8] offset i32 codepoint-size (Ptr i32)] i32 (if (<= offset 0) (do (set (deref codepoint-size) 0) 0) (get-codepoint-previous-raw (addr (at text offset)) codepoint-size))) diff --git a/web/examples/structs.flan b/web/examples/structs.flan index e9c58d8c..7b8dd6ae 100644 --- a/web/examples/structs.flan +++ b/web/examples/structs.flan @@ -1,5 +1,5 @@ (defstruct Cursor - [src [u8] ; a non-owning slice + [src [const u8] ; a read-only, non-owning slice pos i32]) ; no initialiser means zeroed (defn peek [c (Ptr Cursor)] u8 diff --git a/web/index.html b/web/index.html index 7584f36e..89ebd5fc 100644 --- a/web/index.html +++ b/web/index.html @@ -384,7 +384,8 @@ described.

  • Fixed arrays are values. [n T] is inline storage and copies on assignment and on pass-by-value.
  • Slices are views. [T] is ptr+len and owns nothing. - Copying a slice copies the view, never the elements.
    • + Copying a slice copies the view, never the elements. [const T] is the + same view with no stores through it.
  • Pointers are visible. (addr x) takes the address of any assignable place and gives (Ptr T). It does not extend anything's lifetime, and keeping one past its frame is your contract to honour — there is no @@ -518,6 +519,7 @@ notation reads as exactly one data item.

    booli1 stringa byte slice with no NULptr + len [T]slice, non-owningptr + len +[const T]read-only slice: a [T] converts to one, never the reverseptr + len [n T]fixed array, a valuen inline items (Vec T)growable, owning — copies as its header, so the copies alias one bufferptr + len + cap + its allocator (Map K V)open addressing, owning, copies the same way. The only map spelling: braces in type position are not a typedata + len + log2cap + its allocator @@ -800,7 +802,7 @@ code on every target, which is what makes the collector work there.

    its fields, and omitted fields are zeroed.

    (defstruct Cursor
-  [src [u8]      ; a non-owning slice
+  [src [const u8] ; a read-only, non-owning slice
    pos i32])     ; no initialiser means zeroed
 
 (defn peek [c (Ptr Cursor)] u8
@@ -829,8 +831,8 @@ its bytes.
    
 
 
    There are two ways to see a string's bytes and the difference is whether anything
 is allocated. (bytes-view s) is the string's own storage seen as a
-[u8] and costs nothing; it aliases the string, so a literal's view points
-into .rodata and writing through it traps. (bytes s) and
+[const u8] and costs nothing; it aliases the string, and a store through
+it is a compile error. (bytes s) and
 (bytes s allocator) make a writable copy through the allocator — never a
 hidden malloc, which is the rule every allocating operation follows. The
 example above wants a view and takes one.
    

From 7cf57eb8ba10d715396df549832005ea1951845d Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 11:49:17 +0700
Subject: [PATCH 2/7] A read-only slice refuses a dyn view without promising
 one later, and taking a read-only element's address is recorded as an open
 decision

---
 TODO.org     |  3 +++
 lib/check.ml | 10 +++++-----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/TODO.org b/TODO.org
index 0d77b3b9..7a48a077 100644
--- a/TODO.org
+++ b/TODO.org
@@ -948,6 +948,9 @@ deliberate absence.
 CLOSED: [2026-09-25]
 =[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused.
 
+** TODO The address of a read-only element is taken without complaint
+=(addr (at v i))= over a =[const T]= answers a writable =(Ptr T)=, so =slice-from-ptr= launders one back into a =[T]=; a string's byte refuses the same =addr=. Allowed because raylib's =load-image-from-memory= and =get-codepoint-previous= have no other way to hand a =[const u8]= to C. Decision needed: a const pointer type, or a refusal plus another route to C.
+
 ** TODO (slice d 1) over a dyn string is refused where (at d i) works
 The typed and dyn spaces disagree about a spelling, which the standing rule
 forbids. A dyn slice should exist.
diff --git a/lib/check.ml b/lib/check.ml
index 652612ad..89648d89 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2563,11 +2563,11 @@ let box loc (e : Tast.expr) : Tast.expr =
      dyn side can tell a read-only one apart, so a [[const T]] does not
      cross. *)
   | Types.Slice (Types.Const, elem) ->
-    no_dyn_yet loc ~into:true e.Tast.ty
-      (Printf.sprintf
-         ": a dyn view can be written through, and a [const %s] can only be \
-          read. A dyn view is taken of the writable storage it came from"
-         (Types.to_string elem))
+    Loc.failk "check/dyn-const-view" loc
+      "%s does not cross into dyn: a dyn view can be written through, and a \
+       [const %s] can only be read. A dyn view is taken of the writable \
+       storage it came from"
+      (Types.to_string e.Tast.ty) (Types.to_string elem)
   | Types.Slice (Types.Mut, elem) ->
     (match view_elem elem with
      | None -> view_not_yet loc e.Tast.ty elem

From c0b4b2235754920c49bc1972d2b682a8eb57546b Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 12:10:47 +0700
Subject: [PATCH 3/7] 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                   | 89 +++++++++++++++++++++-------------
 lib/types.ml                   | 13 +++++
 test/programs/const-slice.flan |  9 ++++
 test/test_acceptance.ml        |  2 +-
 test/test_flan.ml              | 31 ++++++++++++
 5 files changed, 110 insertions(+), 34 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index c1bf23c0..e22d0889 100644
--- a/lib/check.ml
+++ b/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
diff --git a/lib/types.ml b/lib/types.ml
index c6bc9ae7..7ef1cd4d 100644
--- a/lib/types.ml
+++ b/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)
diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan
index 3d83ebde..6ab1db0f 100644
--- a/test/programs/const-slice.flan
+++ b/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)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 7b1b65c5..4ef0165a 100644
--- a/test/test_acceptance.ml
+++ b/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"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index c4fc6f18..77abd557 100644
--- a/test/test_flan.ml
+++ b/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]. *)

From d8945ae4ae4ca4f8d08db418e16a274bb52910f1 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 12:43:04 +0700
Subject: [PATCH 4/7] The address of read-only storage is a (Ptr const T),
 which nothing is written through and which a C const T * parameter takes

---
 lib/check.ml                   | 166 +++++++++++++++++++++++----------
 lib/cimport.ml                 |  65 ++++++++-----
 lib/dev.ml                     |   8 +-
 lib/emit.ml                    |  14 +--
 lib/render.ml                  |   2 +-
 lib/session.ml                 |  38 ++++----
 lib/shim.ml                    |   2 +
 lib/types.ml                   |  10 +-
 lib/x86.ml                     |  18 ++--
 runtime/flan_dev.c             |   2 +-
 spike/x86/survey.sh            |   8 +-
 test/programs/const-slice.flan |   7 ++
 test/programs/dev-segv.flan    |  33 ++++---
 test/test_acceptance.ml        |   2 +-
 test/test_dev.ml               |   7 +-
 test/test_flan.ml              |  67 +++++++++++--
 test/test_sanitize.ml          |   5 +-
 vendor/raylib/generated.flan   |  54 +++++------
 vendor/raylib/raylib.flan      |  26 +++---
 19 files changed, 335 insertions(+), 199 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index e22d0889..dfd97c60 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1172,6 +1172,10 @@ let tyvar_in_scope env n =
 let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
   let loc = t.Ast.tloc in
   match t.Ast.t with
+  | Ast.Tname "const" ->
+    fail loc
+      "const is not a type on its own — it marks one that can only be read, \
+       as in [const u8] or (Ptr const u8)"
   | Ast.Tname n -> resolve_name env ~seen loc n
   | Ast.Tslice (c, e) ->
     Types.Slice ((if c then Types.Const else Types.Mut), resolve env ~seen e)
@@ -1209,9 +1213,16 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
     if env' then Types.Fn (ps, r) else Types.CFn (ps, r)
   | Ast.Tapp (name, args) ->
     (match name, args with
-     | "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
+     | "Ptr", [ a ] -> Types.Ptr (Types.Mut, resolve env ~seen a)
+     (* The pointer beside [[const T]]: nothing is written through it, and a
+        (Ptr T) converts to one. [const] cannot name a type, so this reading
+        is the only one the two arguments have. *)
+     | "Ptr", [ { Ast.t = Ast.Tname "const"; _ }; a ] ->
+       Types.Ptr (Types.Const, resolve env ~seen a)
      | "Option", [ a ] -> Types.Option (resolve env ~seen a)
-     | ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
+     | "Ptr", _ -> fail loc "a pointer type is (Ptr T), or (Ptr const T) for one \
+                            nothing is written through"
+     | "Option", _ -> fail loc "(Option T) takes exactly one type"
      | "Vec", [ a ] ->
        let e = resolve env ~seen a in
        (* A Vec of a Vec used to be refused here, and the refusal named two
@@ -1865,7 +1876,9 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
   | Types.Slice (m, p), Types.Slice (m', a)
     when m = m' || (ro && m = Types.Const) ->
     bind_ty ~ro:(m = Types.Const) subst p a
-  | Types.Ptr p, Types.Ptr a
+  | Types.Ptr (m, p), Types.Ptr (m', a)
+    when m = m' || (ro && m = Types.Const) ->
+    bind_ty ~ro:(m = Types.Const) subst p a
   | Types.Vec p, Types.Vec a
   | Types.Option p, Types.Option a -> inner p a
   | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && inner p a
@@ -1912,7 +1925,7 @@ let rec subst_ty subst (t : Types.t) =
   | Types.Slice (m, e) -> Types.Slice (m, subst_ty subst e)
   | Types.Array (n, e) -> Types.Array (n, subst_ty subst e)
   | Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v)
-  | Types.Ptr e -> Types.Ptr (subst_ty subst e)
+  | Types.Ptr (m, e) -> Types.Ptr (m, subst_ty subst e)
   | Types.Vec e -> Types.Vec (subst_ty subst e)
   | Types.Option e -> Types.Option (subst_ty subst e)
   | Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r)
@@ -1924,7 +1937,7 @@ let rec subst_ty subst (t : Types.t) =
 let rec generic_ty (t : Types.t) =
   match t with
   | Types.Var _ -> true
-  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
   | Types.Option e -> generic_ty e
   | Types.Map (k, v) -> generic_ty k || generic_ty v
   | Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -1938,7 +1951,7 @@ let rec generic_ty (t : Types.t) =
 let rec reaches_dyn (t : Types.t) =
   match t with
   | Types.Dyn -> true
-  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
   | Types.Option e -> reaches_dyn e
   | Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
   | Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -1982,7 +1995,8 @@ let rec mangle_ty (t : Types.t) =
   | Types.Slice (Types.Const, e) -> "cslice-" ^ mangle_ty e
   | Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (mangle_ty e)
   | Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v)
-  | Types.Ptr e -> "ptr-" ^ mangle_ty e
+  | Types.Ptr (Types.Mut, e) -> "ptr-" ^ mangle_ty e
+  | Types.Ptr (Types.Const, e) -> "cptr-" ^ mangle_ty e
   | Types.Vec e -> "vec-" ^ mangle_ty e
   | Types.Option e -> "opt-" ^ mangle_ty e
   | Types.Fn (ps, r) ->
@@ -2023,7 +2037,7 @@ let rec occurs_in ~needle (t : Types.t) =
   Types.equal needle t
   ||
   match t with
-  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
   | Types.Option e -> occurs_in ~needle e
   | Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
   | Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -2164,11 +2178,11 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
     in
     Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields };
     let ety = Types.Named ename in
-    let eslot = fresh_slot fctx (Types.Ptr ety) in
+    let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in
     let binds =
       List.mapi
         (fun i (_, ((b : binding), slot)) ->
-           let p = mk loc (Types.Ptr ety) (Tast.Local eslot) in
+           let p = mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Local eslot) in
            (slot, mk loc b.bty (Tast.Field (mk loc ety (Tast.Deref p), i))))
         caught
     in
@@ -2183,7 +2197,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
                       caught))
     in
     prefix, Some eslot, Some (mslot, make),
-    Some (mk loc (Types.Ptr ety) (Tast.Addr (Tast.Plocal mslot)))
+    Some (mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Addr (Tast.Plocal mslot)))
 
 (* A source location as a value, for a runtime trap that has to name the site
    rather than the runtime. The bounds and slice traps get theirs from [Emit],
@@ -2202,6 +2216,8 @@ let rec const_reached (e : Tast.expr) =
   | Tast.Prim (Tast.At, target :: idx) ->
     const_steps (const_reached target) target.Tast.ty (List.length idx)
   | Tast.Field (target, _) -> const_reached target
+  | Tast.Deref p ->
+    (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
   | _ -> None
 
 (* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
@@ -2214,14 +2230,27 @@ and const_steps ro (ty : Types.t) n =
     | Types.Array (_, t) -> const_steps ro t (n - 1)
     | _ -> ro
 
-(* A store, or an [addr], through a read-only view. *)
+(* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
 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)
+  match view with
+  | Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
+    Loc.failk "check/store-through-const" loc
+      "this changes the %s behind a %s, which can only be read through. A \
+       container that has to change is handed over as a (Ptr %s)"
+      (Types.to_string t) (Types.to_string view) (Types.to_string t)
+  | Types.Ptr (_, t) ->
+    Loc.failk "check/store-through-const" loc
+      "this writes through a %s, which can only be read, so what it points at \
+       is a value and not a place. (deref p) copies the %s out, and the copy \
+       can be written"
+      (Types.to_string view) (Types.to_string 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
@@ -2358,7 +2387,7 @@ let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []
 (* The address of an expression, place or not: the type-erased runtime takes
    the element [push] copies by pointer. *)
 let addr_of loc (e : Tast.expr) =
-  mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
+  mk loc (Types.Ptr (Types.Mut, e.Tast.ty)) (Tast.Prim (Tast.AddrOf, [ e ]))
 
 (* ── Where a rendered number's bytes live ──────────────────────────────
 
@@ -3015,7 +3044,8 @@ let rec thick_enc (t : Types.t) =
   | Types.Var v -> "y" ^ atom v
   | Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e
   | Types.Slice (Types.Const, e) -> "k" ^ thick_enc e
-  | Types.Ptr e -> "p" ^ thick_enc e
+  | Types.Ptr (Types.Mut, e) -> "p" ^ thick_enc e
+  | Types.Ptr (Types.Const, e) -> "q" ^ thick_enc e
   | Types.Vec e -> "v" ^ thick_enc e
   | Types.Option e -> "o" ^ thick_enc e
   | Types.Array (n, e) -> Printf.sprintf "a%Ld-%s" n (thick_enc e)
@@ -3060,7 +3090,7 @@ let thick_thunk env loc ps r =
    that never reads it costs one store the optimiser drops. *)
 let declare_env ctx = function
   | Some _ as s -> s
-  | None -> Some (fresh_slot ctx (Types.Ptr Types.Unit))
+  | None -> Some (fresh_slot ctx (Types.Ptr (Types.Mut, Types.Unit)))
 
 let numeric_note ~(want : Types.t) ~(got : Types.t) =
   if not (Types.is_numeric want && Types.is_numeric got) then ""
@@ -3095,6 +3125,14 @@ let const_note ~(want : Types.t) ~(got : Types.t) =
        through it, the %s can be declared %s instead"
       (Types.to_string got) (Types.to_string want) copy (Types.to_string want)
       (Types.to_string want) (Types.to_string got)
+  | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
+    when Types.equal e e' ->
+    Printf.sprintf
+      " — a %s can only be read through, and never becomes a %s that can be \
+       written through. Copy the %s out with (deref p) and point at the copy; \
+       where nothing writes through it, the %s can be declared %s instead"
+      (Types.to_string got) (Types.to_string want) (Types.to_string e)
+      (Types.to_string want) (Types.to_string got)
   | _ -> ""
 
 let expect ctx loc ~want (got : Tast.expr) =
@@ -3152,7 +3190,7 @@ let expect ctx loc ~want (got : Tast.expr) =
       (* 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. *)
-      | Types.Slice (Types.Const, _), _
+      | (Types.Slice (Types.Const, _) | Types.Ptr (Types.Const, _)), _
         when Types.const_widens ~from:got.Tast.ty ~into:w ->
         { got with Tast.ty = w }
       | _ -> got
@@ -3239,8 +3277,8 @@ let invented_ctx env ret =
 
 (* The address of field [i] of the struct the pointer in slot [p] points at. *)
 let field_addr_of loc sty fty p i =
-  let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr sty) (Tast.Local p))) in
-  mk loc (Types.Ptr fty) (Tast.Addr (Tast.Pfield (target, i)))
+  let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr (Types.Mut, sty)) (Tast.Local p))) in
+  mk loc (Types.Ptr (Types.Mut, fty)) (Tast.Addr (Tast.Pfield (target, i)))
 
 (* The pointer form is what a Map_Info holds; the direct form is what an
    emitted hasher calls. See flan_rt.c on why they are two symbols. *)
@@ -3337,8 +3375,8 @@ and struct_key_pair env loc n =
       fail loc
         "%s has no fields, so it is not a map key — every value of it would \
          be the same key" n;
-    let hparams = [ Types.Ptr sty; hash_ty; Types.Int Types.I64 ] in
-    let eparams = [ Types.Ptr sty; Types.Ptr sty; Types.Int Types.I64 ] in
+    let hparams = [ Types.Ptr (Types.Mut, sty); hash_ty; Types.Int Types.I64 ] in
+    let eparams = [ Types.Ptr (Types.Mut, sty); Types.Ptr (Types.Mut, sty); Types.Int Types.I64 ] in
     (* Registered before the fields are walked, so a struct reached twice
        through two different fields emits one pair and not two. A struct cannot
        contain itself by value, so there is no cycle to break — only sharing.
@@ -3358,7 +3396,7 @@ and struct_key_pair env loc n =
        hashes its bytes and a nested struct hashes field by field. Padding is
        never reached, because nothing here addresses anything but a field. *)
     let hctx = invented_ctx env hash_ty in
-    let kp = fresh_slot ~name:"key" hctx (Types.Ptr sty) in
+    let kp = fresh_slot ~name:"key" hctx (Types.Ptr (Types.Mut, sty)) in
     let seed = fresh_slot ~name:"seed" hctx hash_ty in
     ignore (fresh_slot ~name:"size" hctx (Types.Int Types.I64));
     let acc = fresh_slot ~name:"h" hctx hash_ty in
@@ -3395,8 +3433,8 @@ and struct_key_pair env loc n =
        field that differs, which for a struct with a string field is the
        difference between one memcmp and two. *)
     let ectx = invented_ctx env (Types.Int Types.I8) in
-    let ap = fresh_slot ~name:"a" ectx (Types.Ptr sty) in
-    let bp = fresh_slot ~name:"b" ectx (Types.Ptr sty) in
+    let ap = fresh_slot ~name:"a" ectx (Types.Ptr (Types.Mut, sty)) in
+    let bp = fresh_slot ~name:"b" ectx (Types.Ptr (Types.Mut, sty)) in
     ignore (fresh_slot ~name:"size" ectx (Types.Int Types.I64));
     let i8 v = mk loc (Types.Int Types.I8) (Tast.Int (v, Types.I8)) in
     let checks =
@@ -3648,7 +3686,7 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
       List.filter_map
         (fun i ->
            match List.nth_opt args i with
-           | Some ({ Tast.ty = Types.Ptr t; _ } as p) when res_pure p ->
+           | Some ({ Tast.ty = Types.Ptr (_, t); _ } as p) when res_pure p ->
              Some (mk loc t (Tast.Deref p), t)
            | _ -> None)
         tr.Shim.rekey
@@ -4600,7 +4638,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
             pointer is a hidden parameter and the name is a slot loaded from
             it — a handler that passed [c] to something expecting the struct
             would otherwise be handed an address. *)
-         let pslot = fresh_slot hctx (Types.Ptr ty) in
+         let pslot = fresh_slot hctx (Types.Ptr (Types.Mut, ty)) in
          let cslot = bind hctx c.Ast.hname ty ~assignable:false in
          let hbody = map_lr (fun e -> check hctx e) c.Ast.hbody in
          let hbody =
@@ -4609,7 +4647,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
                   ([ (cslot,
                       mk c.Ast.hloc ty
                         (Tast.Deref
-                           (mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ],
+                           (mk c.Ast.hloc (Types.Ptr (Types.Mut, ty)) (Tast.Local pslot)))) ],
                    hbody)) ]
          in
          (* Named after the function it came out of, and numbered within it:
@@ -4642,7 +4680,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
             clause matched, and it cannot know which of them captured. *)
          let fenv = declare_env hctx fenv in
          ctx.env.lifted <-
-           { Tast.name = fname; params = [ Types.Ptr ty ];
+           { Tast.name = fname; params = [ Types.Ptr (Types.Mut, ty) ];
              slots = Array.of_list (List.rev hctx.slot_tys);
              snames = Array.of_list (List.rev hctx.slot_names);
              ret = Types.Unit; body = prefix hbody; fdefers = [];
@@ -6362,7 +6400,7 @@ and unknown_name : 'a. ?setting:bool -> ctx -> Loc.t -> string -> 'a =
     let sname =
       match ty with
       | Some (Types.Named n) when fields_named ctx.env n <> None -> Some n
-      | Some (Types.Ptr (Types.Named n)) when fields_named ctx.env n <> None -> Some n
+      | Some (Types.Ptr (_, (Types.Named n))) when fields_named ctx.env n <> None -> Some n
       | _ -> None
     in
     match sname, ty with
@@ -6455,13 +6493,13 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string =
   let has n = fields_named ctx.env n <> None in
   match t.Tast.ty with
   | Types.Named n when has n -> t, n
-  | Types.Ptr (Types.Named n) when has n ->
+  | Types.Ptr (_, (Types.Named n)) when has n ->
     mk t.Tast.loc (Types.Named n) (Tast.Deref t), n
   (* A data type's fields belong to one case, and which case it is holding is
      only known after the tag has been read. [.field] would have to be a read
      that might be reading something else, so it is not one: [match] is how a
      data type is opened, and it binds the fields it has proved are there. *)
-  | (Types.Named n | Types.Ptr (Types.Named n))
+  | (Types.Named n | Types.Ptr (_, Types.Named n))
     when Hashtbl.mem ctx.env.datas n ->
     fail target.Ast.loc
       "%s is a data type, and its fields belong to a case — reach them with \
@@ -6508,6 +6546,26 @@ and refuse_string_place loc (ty : Types.t) =
    other way across: [load-image-from-memory] over an [embed] is the case. So
    the address of a read-only element may be taken, and it is a store that is
    refused. *)
+(* Whether a checked place is read-only storage: reached through a
+   [[const T]] or a (Ptr const T), or a byte of a string. Its address is a
+   (Ptr const T). *)
+and place_const (p : Tast.place) =
+  match p with
+  | Tast.Plocal _ | Tast.Pglobal _ -> false
+  | Tast.Pfield (t, _) -> const_reached t <> None
+  | Tast.Pderef t ->
+    (match t.Tast.ty with Types.Ptr (Types.Const, _) -> true | _ -> false)
+  | Tast.Pindex (t, idx) ->
+    let rec through_string ty n =
+      n > 0
+      && (match ty with
+          | Types.String -> true
+          | Types.Array (_, e) | Types.Slice (_, e) -> through_string e (n - 1)
+          | _ -> false)
+    in
+    const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
+    || through_string t.Tast.ty (List.length idx)
+
 and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
   match p with
   | Ast.Pvar name ->
@@ -6577,7 +6635,9 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
   | Ast.Pderef target ->
     let target = check ctx target in
     (match target.Tast.ty with
-     | Types.Ptr t -> Tast.Pderef target, t
+     | Types.Ptr (Types.Const, _) as view when store ->
+       refuse_const_place loc view
+     | Types.Ptr (_, t) -> Tast.Pderef target, t
      | other ->
        fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
 
@@ -6646,7 +6706,7 @@ and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list
         | Types.Array (_, t) | Types.Slice (_, t) -> t
         (* A string indexes to its bytes, and only to read them. *)
         | Types.String ->
-          Option.iter (fun l -> refuse_string_place l ty) place;
+          if store then Option.iter (fun l -> refuse_string_place l ty) place;
           Types.Int Types.U8
         | other ->
           fail i.Ast.loc "%s cannot be indexed" (Types.to_string other)
@@ -7290,7 +7350,7 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
   match idx with
   | [ i ] ->
     let i = index_expr ctx i in
-    rt loc (Types.Ptr elem) "flan_vec_at"
+    rt loc (Types.Ptr (Types.Mut, elem)) "flan_vec_at"
       [ target; i; size_of loc elem; here loc ], elem
   | _ ->
     fail loc
@@ -8414,9 +8474,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | [ target; cur; k; v ] ->
        let target = check ctx target in
        let kt, vt = map_kv loc "map-next" target.Tast.ty in
-       let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in
-       let k = check ctx ~want:(Types.Ptr kt) k in
-       let v = check ctx ~want:(Types.Ptr vt) v in
+       let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
+       let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
+       let v = check ctx ~want:(Types.Ptr (Types.Mut, vt)) v in
        let found =
          rt loc (Types.Int Types.I8) "flan_map_next"
            [ target; cur; k; v; size_of loc kt; size_of loc vt; here loc ]
@@ -8951,7 +9011,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        let target = check ctx target in
        let elem =
          match target.Tast.ty with
-         | Types.Ptr t -> t
+         | Types.Ptr (_, t) -> t
          | other ->
            fail loc
              "slice-from-ptr takes a (Ptr T) and the number of elements behind \
@@ -8967,7 +9027,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           fail n_loc
             "slice-from-ptr length %Ld is negative" k
         | _ -> ());
-       prim Tast.SliceFromPtr (Types.Slice (Types.Mut, elem)) [ target; n ]
+       (* A read-only pointer gives a read-only slice, or [slice-from-ptr]
+          would undo the const [addr] put there. *)
+       let m = match target.Tast.ty with Types.Ptr (m, _) -> m | _ -> Types.Mut in
+       prim Tast.SliceFromPtr (Types.Slice (m, elem)) [ target; n ]
      | _ -> assert false)
 
   (* ── pointers ──────────────────────────────────────────────────── *)
@@ -8981,12 +9044,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           or (deref p)"
      | Some p ->
        let p, ty = check_place ~store:false ctx a.Ast.loc p in
-       expect ctx loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p)))
+       let m = if place_const p then Types.Const else Types.Mut in
+       expect ctx loc ~want (mk loc (Types.Ptr (m, ty)) (Tast.Addr p)))
   | "deref" ->
     arity ctx loc name 1 args;
     let a = check ctx (List.hd args) in
     (match a.Tast.ty with
-     | Types.Ptr t -> expect ctx loc ~want (mk loc t (Tast.Deref a))
+     | Types.Ptr (_, t) -> expect ctx loc ~want (mk loc t (Tast.Deref a))
      | other -> fail loc "deref takes a (Ptr T), found %s"
                   (Types.to_string other))
 
@@ -9857,7 +9921,7 @@ and generic_call ctx ~want loc name vars pats pret args =
   let rec mentions v (t : Types.t) =
     match t with
     | Types.Var u -> String.equal u v
-    | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+    | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
     | Types.Option e -> mentions v e
     | Types.Map (k, w) -> mentions v k || mentions v w
     | Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -12197,7 +12261,7 @@ let rec dyn_reach ~through p seen (t : Types.t) =
   | Types.Dyn -> true
   | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
   | Types.Map (k, v) -> go k || go v
-  | Types.Ptr e | Types.Slice (_, e) -> through && go e
+  | Types.Ptr (_, e) | Types.Slice (_, e) -> through && go e
   | Types.Fn _ -> false
   | Types.Named n when not (List.mem n seen) ->
     let seen = n :: seen in
@@ -12252,7 +12316,7 @@ let rec dyn_behind_pointer p seen (t : Types.t) =
 
      It still terminates. This walk's own [seen] guards its own [Named]
      recursion, and each crossing starts a separate finite walk of its own. *)
-  | Types.Ptr e | Types.Slice (_, e) -> dyn_through p [] e
+  | Types.Ptr (_, e) | Types.Slice (_, e) -> dyn_through p [] e
   | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
   | Types.Map (k, v) -> go k || go v
   | Types.Dyn | Types.Fn _ -> false
@@ -12327,7 +12391,7 @@ let rec hidden_dyn p seen (t : Types.t) : Types.t option =
     if dyn_anywhere p seen k || dyn_anywhere p seen v then Some t else None
   (* A pointer and a slice are views of storage something else roots; see the
      note above. What they point at is checked where it is declared. *)
-  | Types.Ptr e | Types.Slice (_, e) -> hidden_dyn p seen e
+  | Types.Ptr (_, e) | Types.Slice (_, e) -> hidden_dyn p seen e
   | Types.Fn _ -> None
   | Types.Named n when not (List.mem n seen) ->
     let seen = n :: seen in
@@ -12476,7 +12540,7 @@ let dyn_descriptors (p : Tast.program) =
           foreign parameter of pointer or slice type receives is the address
           of a place. Below it the question is [dyn_behind_pointer]'s again. *)
        let below (t : Types.t) =
-         match t with Types.Ptr e | Types.Slice (_, e) -> e | t -> t
+         match t with Types.Ptr (_, e) | Types.Slice (_, e) -> e | t -> t
        in
        List.iteri
          (fun i t ->
diff --git a/lib/cimport.ml b/lib/cimport.ml
index d72a954b..6d5d067c 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -556,6 +556,13 @@ let param_ty env (s : string) : Ast.texpr =
         "char * is a parameter C may write through, and a Flan string crosses \
          as a NUL-terminated copy — the writes would be lost. const char * is \
          a string; this one needs a declare-c saying (Ptr u8)"
+    (* [const T *] is the one pointer C promises not to write through, so it
+       takes a (Ptr const T) — and with it the address of a read-only
+       element, which a (Ptr T) parameter would refuse. *)
+    | _ when is_const ->
+      (match (value_ty env s).Ast.t with
+       | Ast.Tapp ("Ptr", [ e ]) -> ty (Ast.Tapp ("Ptr", [ tname "const"; e ]))
+       | _ -> value_ty env s)
     | _ -> value_ty env s
   end
   else value_ty env s
@@ -949,33 +956,41 @@ let c_pointee (s : string) : string option =
     Some (String.trim (String.sub s 0 (String.length s - 1)))
   else None
 
+let ptr_agrees_elem env ~inner (elem : Ast.texpr) =
+  (* [void *] agrees with a pointer to anything, and this is the judgement
+     call of the arm. C's [void *] is opaque about *what it points at* — that
+     is the whole of what the spelling means — so there is no element type in
+     the header to disagree with, and a check that reported one would be
+     reporting [value_ty]'s guess of [u8] back at the author as if the header
+     had said it. What is *not* given up is that it is a pointer at all: the
+     match above requires [(Ptr _)] on the Flan side, so an [i32] or a
+     [string] declared against a [void *] is still a finding. That
+     asymmetry is the point — raylib spells thirty-odd parameters [void *]
+     and none of them is a scalar. *)
+  let b = bare inner in
+  if String.equal b "void" then true
+  else (
+    match (try Some (value_ty env inner) with Refused _ -> None) with
+    | None ->
+      (* A pointee this cannot render says nothing, exactly as an
+         unrenderable field type says nothing in [check_structs]. *)
+      false
+    | Some want ->
+      let a = ty_source want and b = ty_source elem in
+      (* [agrees] and not [String.equal], so a [(Ptr Key)] against the
+         header's [(Ptr int)] lands on the enum arm. The four bytes are the
+         same four bytes through a pointer as they are beside one. *)
+      agrees env want elem || (byte a && byte b))
+
 let ptr_agrees env ~(c : string) (t : Ast.texpr) =
   match (c_pointee c, t.Ast.t) with
-  | Some inner, Ast.Tapp ("Ptr", [ elem ]) ->
-    (* [void *] agrees with a pointer to anything, and this is the judgement
-       call of the arm. C's [void *] is opaque about *what it points at* — that
-       is the whole of what the spelling means — so there is no element type in
-       the header to disagree with, and a check that reported one would be
-       reporting [value_ty]'s guess of [u8] back at the author as if the header
-       had said it. What is *not* given up is that it is a pointer at all: the
-       match above requires [(Ptr _)] on the Flan side, so an [i32] or a
-       [string] declared against a [void *] is still a finding. That
-       asymmetry is the point — raylib spells thirty-odd parameters [void *]
-       and none of them is a scalar. *)
-    let b = bare inner in
-    if String.equal b "void" then true
-    else (
-      match (try Some (value_ty env inner) with Refused _ -> None) with
-      | None ->
-        (* A pointee this cannot render says nothing, exactly as an
-           unrenderable field type says nothing in [check_structs]. *)
-        false
-      | Some want ->
-        let a = ty_source want and b = ty_source elem in
-        (* [agrees] and not [String.equal], so a [(Ptr Key)] against the
-           header's [(Ptr int)] lands on the enum arm. The four bytes are the
-           same four bytes through a pointer as they are beside one. *)
-        agrees env want elem || (byte a && byte b))
+  (* A (Ptr const T) promises C will not write, so the header has to promise
+     it too: over a [T *] without const, C may write through storage Flan
+     holds read-only. *)
+  | Some inner, Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; elem ]) ->
+    strip_prefix "const " inner <> None
+    && ptr_agrees_elem env ~inner elem
+  | Some inner, Ast.Tapp ("Ptr", [ elem ]) -> ptr_agrees_elem env ~inner elem
   | _ -> false
 
 (* The two together, for the one caller that still has the C spelling. A
diff --git a/lib/dev.ml b/lib/dev.ml
index dfe19dda..7170de14 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -2726,7 +2726,7 @@ let type_of_spelling t spelling : (Types.t, string) result =
 let addr_extern : Tast.extern =
   { Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr";
     eparams = [ Types.Int Types.I64 ];
-    eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown }
+    eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown }
 
 (* Renders the value [(Ptr ty)] holding [addr], in the program.
 
@@ -2761,7 +2761,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
         extra := ty :: !extra;
         i) }
   in
-  let pty = Types.Ptr ty in
+  let pty = Types.Ptr (Types.Mut, ty) in
   let root =
     { Tast.e =
         Tast.Prim
@@ -2771,7 +2771,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
                    ("flan/dev-addr",
                     [ { Tast.e = Tast.Int (Int64.of_int addr, Types.I64);
                         ty = Types.Int Types.I64; loc } ]);
-               ty = Types.Ptr (Types.Int Types.U8); loc } ]);
+               ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } ]);
       ty = pty; loc }
   in
   match Render.render c 0 root with
@@ -2935,7 +2935,7 @@ let inspect_addr t ~addr ~want_type =
                    | Ok v ->
                      ok
                        ([ Printf.sprintf ":addr %d" addr;
-                          ":type " ^ Wire.quote (Types.to_string (Types.Ptr ty));
+                          ":type " ^ Wire.quote (Types.to_string (Types.Ptr (Types.Mut, ty)));
                           ":value " ^ Wire.quote v; ":live " ^ live ]
                         @ told @ where))))))
 
diff --git a/lib/emit.ml b/lib/emit.ml
index a8ccfff7..3e229510 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -791,7 +791,7 @@ let rec dty m d (t : Types.t) : int =
       | Types.Bool -> basic "bool" 8 "DW_ATE_boolean"
       | Types.Enum e -> basic e 32 "DW_ATE_signed"
       | Types.Unit | Types.Never -> composite (Types.to_string t) []
-      | Types.Ptr e ->
+      | Types.Ptr (_, e) ->
         let id = dalloc d in
         Hashtbl.replace d.dtys key id;
         (* [(Ptr Unit)] and [(Ptr Never)] are the opaque pointer, and a DWARF
@@ -817,10 +817,10 @@ let rec dty m d (t : Types.t) : int =
          capacity, so two members are the whole truth about a slice. *)
       | Types.String ->
         composite "string"
-          [ ("ptr", Types.Ptr (Types.Int Types.U8)); ("len", Types.Int Types.I64) ]
+          [ ("ptr", Types.Ptr (Types.Mut, (Types.Int Types.U8))); ("len", Types.Int Types.I64) ]
       | Types.Slice (_, e) ->
         composite (Types.to_string t)
-          [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64) ]
+          [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64) ]
       | Types.Option e ->
         composite (Types.to_string t)
           [ ("tag", Types.Int Types.U8); ("value", e) ]
@@ -888,7 +888,7 @@ let rec dty m d (t : Types.t) : int =
          would put the reader's offsets out by one. *)
       | Types.Vec e ->
         composite (Types.to_string t)
-          [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64);
+          [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64);
             ("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
             ("epoch", Types.Int Types.I64) ]
       (* Five fields again, and shown as five for the same reason: a debugger
@@ -898,7 +898,7 @@ let rec dty m d (t : Types.t) : int =
          describing a field that is not there. *)
       | Types.Map (k, v) ->
         composite (Types.to_string t)
-          [ ("data", Types.Ptr (Types.Int Types.U8));
+          [ ("data", Types.Ptr (Types.Mut, (Types.Int Types.U8)));
             ("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64);
             ("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
         |> fun n -> ignore k; ignore v; n
@@ -913,7 +913,7 @@ let rec dty m d (t : Types.t) : int =
          locals, where they are under the names the source gave them. *)
       | Types.Fn _ ->
         composite (Types.to_string t)
-          [ ("code", Types.Ptr Types.Unit); ("env", Types.Ptr Types.Unit) ]
+          [ ("code", Types.Ptr (Types.Mut, Types.Unit)); ("env", Types.Ptr (Types.Mut, Types.Unit)) ]
       (* And the bare one is what it always was: a pointer to code, and lldb
          is told exactly that and no more. DWARF has DW_TAG_subroutine_type
          for the signature behind it, and spelling one out would buy a reader
@@ -2568,7 +2568,7 @@ and place f (p : Tast.place) : string * Types.t =
   | Tast.Pindex (target, idx) -> element_addr f target idx
   | Tast.Pderef target ->
     let t = match target.Tast.ty with
-      | Types.Ptr t -> t | t -> internal "deref of %s" (Types.to_string t)
+      | Types.Ptr (_, t) -> t | t -> internal "deref of %s" (Types.to_string t)
     in
     value f target, t
 
diff --git a/lib/render.ml b/lib/render.ml
index d45251b6..c5cf9f6d 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -193,7 +193,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis
        An address the registry never saw is neither: it prints []. That
        is a stack local, a global, or a pointer from C, and the shadow stack
        and the static type table already answer for the first two by name. *)
-    | Types.Ptr t ->
+    | Types.Ptr (_, t) ->
       (match c.ptrs with
        | None -> [ lit "" ]
        | Some pt ->
diff --git a/lib/session.ml b/lib/session.ml
index b86df0e4..2aba91a8 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -1202,12 +1202,12 @@ let externs : Tast.extern list =
        is. See [render_locals]. *)
     { Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot";
       eparams = [ Types.Int Types.I64; Types.Int Types.I64 ];
-      eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown };
+      eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown };
     (* The condition the stopped program is holding, same contract: the agent
        resolves it against the snapshot on top when the thunk runs, and NULL
        when there is none. See [render_condition]. *)
     { Tast.ename = "flan/dev-cond"; esym = "flan_agent_condition";
-      eparams = []; eret = Types.Ptr (Types.Int Types.U8);
+      eparams = []; eret = Types.Ptr (Types.Mut, (Types.Int Types.U8));
       eloc = Loc.unknown };
     (* The character beside a rendered byte. See [Render.pointers]. *)
     { Tast.ename = "flan/dev-emit-u8-char"; esym = "flan_dev_emit_u8_char";
@@ -1232,10 +1232,10 @@ let externs : Tast.extern list =
        written" is already the right rendering for an address the registry
        never saw. *)
     { Tast.ename = "flan/reg-live"; esym = "flan_dev_reg_live";
-      eparams = [ Types.Ptr (Types.Int Types.U8) ];
+      eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ];
       eret = Types.Int Types.I32; eloc = Loc.unknown };
     { Tast.ename = "flan/reg-emit"; esym = "flan_dev_reg_emit";
-      eparams = [ Types.Ptr (Types.Int Types.U8) ];
+      eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ];
       eret = Types.Int Types.I32; eloc = Loc.unknown } ]
 
 (* The REPL's emitter. Each piece is one extern call: the dev runtime already
@@ -1264,8 +1264,8 @@ let dev_pointers : Render.pointers =
   let ask name (p : Tast.expr) : Tast.expr =
     let loc = p.Tast.loc in
     let byte =
-      { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Int Types.U8)), [ p ]);
-        ty = Types.Ptr (Types.Int Types.U8); loc }
+      { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, (Types.Int Types.U8))), [ p ]);
+        ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
     in
     { Tast.e = Tast.Call (name, [ byte ]); ty = i32; loc }
   in
@@ -1405,11 +1405,11 @@ let render_locals ?(origin = "") t ~frame ~(fn : Tast.fn) ~bound
     in
     let address =
       { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx i ]);
-        ty = Types.Ptr (Types.Int Types.U8); loc }
+        ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
     in
     let typed =
-      { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
-        ty = Types.Ptr ty; loc }
+      { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+        ty = Types.Ptr (Types.Mut, ty); loc }
     in
     let v = { Tast.e = Tast.Deref typed; ty; loc } in
     match Render.render c 0 v with
@@ -1513,11 +1513,11 @@ let render_condition t ~(st : Tast.structure) : change * (string * string) list
   let cty = Types.Named st.Tast.sname in
   let address =
     { Tast.e = Tast.Call ("flan/dev-cond", []);
-      ty = Types.Ptr (Types.Int Types.U8); loc }
+      ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
   in
   let typed =
-    { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr cty), [ address ]);
-      ty = Types.Ptr cty; loc }
+    { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, cty)), [ address ]);
+      ty = Types.Ptr (Types.Mut, cty); loc }
   in
   let root = { Tast.e = Tast.Deref typed; ty = cty; loc } in
   let one i (f : Tast.field) =
@@ -1770,11 +1770,11 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
       let ty = fn.Tast.slots.(slot) in
       let address =
         { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
-          ty = Types.Ptr (Types.Int Types.U8); loc }
+          ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
       in
       let typed =
-        { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
-          ty = Types.Ptr ty; loc }
+        { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+          ty = Types.Ptr (Types.Mut, ty); loc }
       in
       let root = { Tast.e = Tast.Deref typed; ty; loc } in
       let rec walk v = function
@@ -1805,7 +1805,7 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
                       Tast.Prim
                         (Tast.Cast (Types.Int Types.I64),
                          [ { Tast.e = Tast.Prim (Tast.AddrOf, [ v ]);
-                             ty = Types.Ptr v.Tast.ty; loc } ]);
+                             ty = Types.Ptr (Types.Mut, v.Tast.ty); loc } ]);
                     ty = Types.Int Types.I64; loc }
                 in
                 let newline =
@@ -1985,11 +1985,11 @@ let write_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
       let ty = fn.Tast.slots.(slot) in
       let address =
         { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
-          ty = Types.Ptr (Types.Int Types.U8); loc }
+          ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
       in
       let typed =
-        { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
-          ty = Types.Ptr ty; loc }
+        { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+          ty = Types.Ptr (Types.Mut, ty); loc }
       in
       let root = { Tast.e = Tast.Deref typed; ty; loc } in
       let rec walk v = function
diff --git a/lib/shim.ml b/lib/shim.ml
index 2c590440..e185d325 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -221,6 +221,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
        else
          fail loc "%s is %s, which is not a type this shim generator knows" what n)
   | Ast.Tapp ("Ptr", [ e ]) -> cty env ~needed ~loc ~what e ^ " *"
+  | Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; e ]) ->
+    "const " ^ cty env ~needed ~loc ~what e ^ " *"
   | Ast.Tapp ("Option", _) ->
     fail loc
       "%s is an Option, which C has no shape for — declare what C returns and \
diff --git a/lib/types.ml b/lib/types.ml
index 7ef1cd4d..bccd930a 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -43,7 +43,7 @@ type t =
   | Slice  of access * t              (* [T] [const T]  ptr+len, non-owning *)
   | Array  of int64 * t               (* [n T]   inline, a value, copies *)
   | Map    of t * t                   (* (Map K V) *)
-  | Ptr    of t                       (* (Ptr T) *)
+  | Ptr    of access * t              (* (Ptr T) (Ptr const T) *)
   (* [Allocator]: a builtin opaque type, the way [string] is a builtin
      ptr+len. It is a [Types.t] case with no user-writable constructor, which
      is what lets spec-memory.md's "procedure plus an opaque data pointer" be
@@ -193,7 +193,7 @@ let rec equal a b =
   | Slice (a, x), Slice (b, y) -> a = b && equal x y
   | Array (n, x), Array (m, y) -> Int64.equal n m && equal x y
   | Map (k, v), Map (k', v') -> equal k k' && equal v v'
-  | Ptr x, Ptr y -> equal x y
+  | Ptr (a, x), Ptr (b, y) -> a = b && equal x y
   | Alloc, Alloc -> true
   | Vec x, Vec y -> equal x y
   | Option x, Option y -> equal x y
@@ -219,7 +219,8 @@ let rec to_string = function
   | Slice (Const, t) -> "[const " ^ to_string t ^ "]"
   | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t)
   | Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v)
-  | Ptr t -> "(Ptr " ^ to_string t ^ ")"
+  | Ptr (Mut, t) -> "(Ptr " ^ to_string t ^ ")"
+  | Ptr (Const, t) -> "(Ptr const " ^ to_string t ^ ")"
   | Alloc -> "Allocator"
   | Vec t -> "(Vec " ^ to_string t ^ ")"
   | Option t -> "(Option " ^ to_string t ^ ")"
@@ -344,7 +345,8 @@ let join a b =
    same at run time. *)
 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
+  | Slice (_, a), Slice (Const, b) | Ptr (_, a), Ptr (Const, b) ->
+    equal a b || const_widens ~from:a ~into:b
   | _ -> false
 
 (* A function of one signature standing where another is wanted, when the
diff --git a/lib/x86.ml b/lib/x86.ml
index 7b1f5521..fd80d5f8 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -1554,7 +1554,7 @@ type arg =
    move-only container by address. *)
 let classify_c (l : loc) (t : Types.t) =
   match t with
-  | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ]
+  | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr (Types.Mut, Types.Unit)); Alen l ]
   | Types.Unit | Types.Never -> []
   | Types.Vec _ | Types.Map _ -> [ Aptr l ]
   (* A fixed array crossing into a dyn view (M2 item 3) needs its address for
@@ -1816,7 +1816,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
     store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8;
     (match env with
      | None -> xor_rr f.b ~dst:rax ~src:rax
-     | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr Types.Unit));
+     | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit)));
     store_int f.b ~src:rax ~mm:(lmem f (shift dst 8) ~scratch:r11) ~size:8
   | Tast.FnAddr r ->
     fnaddr_at f ~loc:e.Tast.loc ~reg:rax r;
@@ -1844,7 +1844,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
     let c = eval f callee in
     let env =
       match callee.Tast.ty with
-      | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr Types.Unit))
+      | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr (Types.Mut, Types.Unit)))
       | _ -> None
     in
     call_flan f ?env ~target:(`Loc c) ~args ~rty:t dst
@@ -2059,7 +2059,7 @@ and emit_handled f frames body dst t =
          (match h.Tast.henv with
           | Some ev ->
             let l = scoped f (fun () -> eval f ev) in
-            load_loc f ~reg:rax l (Types.Ptr Types.Unit)
+            load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit))
           | None -> xor_rr f.b ~dst:rax ~src:rax);
          store_int f.b ~src:rax ~mm:(Frame (slot + h_env)) ~size:8;
          lea f.b ~dst:rdi ~mm:(Frame slot);
@@ -2573,7 +2573,7 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t =
 and field_loc f (base : loc) (ty : Types.t) i =
   match ty with
   | Types.Named sn -> shift base (List.nth (field_offsets f sn) i)
-  | Types.Ptr (Types.Named sn) ->
+  | Types.Ptr (_, (Types.Named sn)) ->
     shift (Lp (off_of base, 0)) (List.nth (field_offsets f sn) i)
   | Types.String | Types.Slice _ -> shift base (if i = 0 then 0 else 8)
   | Types.Option el -> let ot, ov = option_lay f el in
@@ -2606,7 +2606,7 @@ and elements f (base : loc) (ty : Types.t) (is : Tast.expr list) : loc =
   | i :: rest ->
     let elem =
       match ty with
-      | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el
+      | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el
       | Types.String -> Types.Int Types.U8
       | t -> unsupported "index into %s" (Types.to_string t)
     in
@@ -2904,7 +2904,7 @@ and check_cast f (loc : Loc.t) (src : Types.fkind) (k : Types.ikind) =
 and element f (base : loc) (ty : Types.t) (i : Tast.expr) : loc =
   let elem =
     match ty with
-    | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el
+    | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el
     | Types.String -> Types.Int Types.U8
     | t -> unsupported "index into %s" (Types.to_string t)
   in
@@ -2966,7 +2966,7 @@ and call_flan f ?env ~target ~args ~rty dst =
   in
   (* The channel is this frame's own: a callee that transfers writes through
      the pointer we were handed, so one cell serves the whole chain. *)
-  let chan = [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] in
+  let chan = [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] in
   (* And the environment last of all, on exactly one kind of call: one through
      a [(Fn ...)] value, which cannot know whether the body it reaches
      declared one. Every other call passes what it always passed — this is
@@ -3074,7 +3074,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
       args
   in
   let flat = List.concat_map (fun (l, ty) -> classify_c l ty) vals in
-  let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] else flat in
+  let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] else flat in
   let nsse = emit_args f flat in
   (* [al] is how many SSE registers were used, which a variadic callee reads.
      Harmless on a fixed one, and a [declare] does not say which it is. *)
diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c
index ec4e0e3f..82c1120c 100644
--- a/runtime/flan_dev.c
+++ b/runtime/flan_dev.c
@@ -2325,7 +2325,7 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) {
   }
   {
     static const char why[] =
-      "\nflan: a write through a pointer into read-only memory, "
+      "\nflan: a write into read-only memory, "
       "a null, or a stack overflow\n";
     crash_puts(why, sizeof why - 1);
   }
diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh
index c6b9a598..c0c58015 100755
--- a/spike/x86/survey.sh
+++ b/spike/x86/survey.sh
@@ -95,10 +95,10 @@ forever="dev-loop dev-watch dev-chatty agent-auto"
 # sweep now and they are five of the MATCHes.
 
 # The one whose whole point is a fault, and which therefore cannot be compared
-# at this sweep's optimisation level. dev-segv stores through a pointer to a
-# string literal's bytes, which is a store into .rodata: LLVM at -O2 deletes it
-# as undefined and exits 0, and this backend has no optimiser and exits 139.
-# That is not a lowering disagreement. test_dev.ml builds it in a dev session,
+# at this sweep's optimisation level. dev-segv stores through a null pointer,
+# which is undefined: what LLVM at -O2 does with it is its own business, and
+# this backend has no optimiser and exits 139. That is not a lowering
+# disagreement. test_dev.ml builds it in a dev session,
 # where the fault is the thing asserted. It also calls agent/start, so it
 # leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks
 # in the break loop instead of dying.
diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan
index 6ab1db0f..3c64505f 100644
--- a/test/programs/const-slice.flan
+++ b/test/programs/const-slice.flan
@@ -18,6 +18,9 @@
       (set n (+ n (length (at parts i)))))
     n))
 
+;; A (Ptr const T) is what the address of read-only storage is.
+(defn peek [p (Ptr const u8)] u8 (deref p))
+
 ;; 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))
@@ -54,5 +57,9 @@
       (println (string (slice (join (slice f) (bytes-view "-"))))))
     (println (at r 0))
     (println (call-rd rd) (call-bare rd) (call-mk mk))
+    (let [b (bytes "q")]
+      (println (peek (addr (at r 1))) (peek (addr (at "abc" 2)))
+               (peek (addr (at b 0)))
+               (string (slice-from-ptr (addr (at r 7)) 5))))
     (free names))
   0)
diff --git a/test/programs/dev-segv.flan b/test/programs/dev-segv.flan
index 1ea5ca31..95ce1f54 100644
--- a/test/programs/dev-segv.flan
+++ b/test/programs/dev-segv.flan
@@ -1,22 +1,21 @@
-;;;; The dogfooding crash, replayed on purpose: a store through a pointer to
-;;;; a string literal's bytes lands in read-only memory and takes SIGSEGV. In
-;;;; a dev session that used to kill the whole process — daemon, compiler and
-;;;; socket together, with no message at all. The dev build's crash handler
-;;;; turns it into the same park the no-channel traps take: one line naming
-;;;; the address and the frame, then the break loop, with the daemon alive
-;;;; and answering behind it. There is no restart to list — a faulting
-;;;; instruction has nowhere to resume at — which is the same empty-list
-;;;; shape dev-trap-null-alloc.flan pins for free-all.
+;;;; A hardware fault, taken on purpose: a store through a null pointer takes
+;;;; SIGSEGV. In a dev session that used to kill the whole process — daemon,
+;;;; compiler and socket together, with no message at all. The dev build's
+;;;; crash handler turns it into the same park the no-channel traps take: one
+;;;; line naming the address and the frame, then the break loop, with the
+;;;; daemon alive and answering behind it. There is no restart to list — a
+;;;; faulting instruction has nowhere to resume at — which is the same
+;;;; empty-list shape dev-trap-null-alloc.flan pins for free-all.
 ;;;;
-;;;; Through a pointer, because a store through the [const u8] itself is
-;;;; refused at compile time; a (Ptr T) is the C boundary, where nothing is
-;;;; checked.
+;;;; The crash that first raised this was a write through a bytes-view of a
+;;;; string literal, which no longer compiles; a zeroed pointer is the
+;;;; surviving way to fault.
 (import agent "vendor:agent")
 
+(defonce nowhere (Ptr u8))
+
 (defn main [] i32
   (agent/start "/tmp/flan-dev-segv-fallback.sock")
-  (let [v (bytes-view "INSERTIONSORT")
-        p (addr (at v 0))]
-    (set (deref p) \Z)
-    (print (string v))
-    0))
+  (set (deref nowhere) \Z)
+  (println "not reached")
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 4ef0165a..f06512f6 100644
--- a/test/test_acceptance.ml
+++ b/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\n3 4 2\n"
+      "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n101 99 113 world\n"
     in
     outputs "const slices" "programs/const-slice.flan" const_slice_out;
     outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 7701bb2d..46af004a 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -1922,7 +1922,7 @@ let () =
           if refault then begin
             let faulting =
               "(:op \"eval-expr\" :code \
-               \"(let [v (bytes-view \\\"refault\\\") p (addr (at v 0))] (set (deref p) 90) 1)\" \
+               \"(do (set (deref nowhere) 90) 1)\" \
                :file \"/tmp/buf.flan\")"
             in
             (match ask faulting with _ -> () | exception _ -> ());
@@ -2028,9 +2028,8 @@ let () =
        word. The dev build's crash handler (flan_dev_crash_enable) enters the
        same trap hook the six no-channel refusals use, so everything trap_park
        asserts for them holds here too: stopped and describable, an eval still
-       answered, a resume refused. The program writes through a pointer to
-       a literal's bytes, which is the surviving spelling of that crash: a
-       store through the bytes-view itself no longer compiles. *)
+       answered, a resume refused. The program stores through a null
+       pointer: the bytes-view write that first crashed no longer compiles. *)
     trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" [];
 
     (* ── The locals of a stopped frame ─────────────────────────────── *)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 77abd557..adc0a418 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2238,12 +2238,10 @@ let () =
   rejects_check "set through a string's slice"
     "(defn f [s string] () (set (at (slice s 1) 0) 65))"
     ~needle:"not a place";
-  (* The address of one is the same question and gets the same answer, so
-     the message has to fit a reader who asked for a pointer and not a
-     store. *)
-  rejects_check "the address of a string's byte"
+  (* The address of one is a (Ptr const u8), so it is not a (Ptr u8). *)
+  rejects_check "the address of a string's byte is read-only"
     "(defn f [s string] (Ptr u8) (addr (at s 0)))"
-    ~needle:"(at s i) is a value and not a place";
+    ~needle:"expected (Ptr u8), found (Ptr const u8)";
   (* And a string is still not a [u8]: slicing one does not smuggle a byte
      slice out of it. *)
   rejects_check "a string slice is not a byte slice"
@@ -2322,6 +2320,47 @@ let () =
     "(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])";
+  (* (Ptr const T): the pointer beside [const T]. *)
+  infers "the address of a const element" "(addr (at (bytes-view \"hi\") 0))"
+    "(Ptr const u8)";
+  infers "the address of a string's byte" "(addr (at \"hi\" 0))"
+    "(Ptr const u8)";
+  infers "a const pointer slices to a const slice"
+    "(slice-from-ptr (addr (at (bytes-view \"hi\") 0)) 2)" "[const u8]";
+  rejects_check "a store through a const pointer"
+    "(defn f [p (Ptr const i32)] () (set (deref p) 1))"
+    ~needle:"this writes through a (Ptr const i32)";
+  rejects_check "a store through the address of a const element"
+    "(defn f [v [const u8]] () (set (deref (addr (at v 0))) 1))"
+    ~needle:"this writes through a (Ptr const u8)";
+  rejects_check "a store through the address of a string's byte"
+    "(defn f [s string] () (set (deref (addr (at s 0))) 1))"
+    ~needle:"this writes through a (Ptr const u8)";
+  rejects_check "a field store through a const pointer"
+    "(defstruct P [x i32]) (defn f [p (Ptr const P)] () (set (.x p) 1))"
+    ~needle:"this writes through a (Ptr const P)";
+  rejects_check "a push through a const pointer"
+    "(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))"
+    ~needle:"behind a (Ptr const (Vec i32))";
+  rejects_check "a const pointer is not a writable one"
+    "(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))"
+    ~needle:"expected (Ptr u8), found (Ptr const u8)";
+  rejects_check "slice-from-ptr keeps the const"
+    "(defn f [v [const u8]] [u8] (slice-from-ptr (addr (at v 0)) 1))"
+    ~needle:"expected [u8], found [const u8]";
+  rejects_check "const alone is not a type" "(defn f [p (Ptr const)] i32 0)"
+    ~needle:"const is not a type on its own";
+  rejects_check "no conversion under a writable pointer"
+    "(defn f [p (Ptr (Ptr i32))] (Ptr (Ptr const i32)) p)"
+    ~needle:"expected (Ptr (Ptr const i32)), found (Ptr (Ptr i32))";
+  accepts "a writable pointer is a const one"
+    "(defn f [p (Ptr i32)] (Ptr const i32) p)";
+  accepts "and under a const pointer, one level down"
+    "(defn f [p (Ptr (Ptr i32))] (Ptr const (Ptr const i32)) p)";
+  accepts "a generic const pointer binds from a writable one"
+    "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
+  accepts "vec-new reads (Ptr const u8) as a type"
+    "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
   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]. *)
@@ -2334,7 +2373,7 @@ let () =
   accepts "under a const slice the element converts too"
     "(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))";
   accepts "the address of a const element, for C"
-    "(defn f [s [const u8]] (Ptr u8) (addr (at s 0)))";
+    "(defn f [s [const u8]] (Ptr const u8) (addr (at s 0)))";
   accepts "a generic reader takes both"
     "(defn f [a [const i32]  b [i32]] i64 (+ (sum-i32 a) (sum-i32 b)))";
 
@@ -4503,8 +4542,9 @@ let () =
      something different in a parameter than it does anywhere else. *)
   emits "const char * as a string parameter"
     "(declare-c name-length [text string] i32 \"name_length\")";
-  emits "a pointer parameter"
-    "(declare-c count-at [values (Ptr i32)  n i32] i32 \"count_at\")";
+  (* const int * is a pointer C promises not to write through. *)
+  emits "a const pointer parameter"
+    "(declare-c count-at [values (Ptr const i32)  n i32] i32 \"count_at\")";
   (* struct Pair is both Pair and Point in the header and the package
      describes it once, so both names have to land on the one defstruct —
      raylib does exactly this with Texture2D and TextureCubemap. *)
@@ -5140,6 +5180,10 @@ let () =
     "(declare-c name-length [text string] i32 \"name_length\")";
   agreed "a pointer that matches the header exactly"
     "(declare-c count-at [values (Ptr i32)  n i32] i32 \"count_at\")";
+  agreed "a const pointer that matches the header exactly"
+    "(declare-c count-at [values (Ptr const i32)  n i32] i32 \"count_at\")";
+  agreed "a const pointer where the header says const void *"
+    "(declare-c blit [dst (Ptr Pair)  src (Ptr const Shade)  n i32] \"blit\")";
   (* void * is opaque about what it points at, so there is no element type in
      the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *)
   agreed "any pointer where the header says void *"
@@ -5155,12 +5199,17 @@ let () =
      name the disagreement. *)
   differs "a pointer to the wrong named type"
     "(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")"
-    "parameter p is (Ptr Shade) and the header says (Ptr Pair)";
+    "parameter p is (Ptr Shade) and the header says (Ptr const Pair)";
   differs "a pointer to the wrong width"
     "(declare-c count-at [values (Ptr f64)  n i32] i32 \"count_at\")"
     "parameter values is (Ptr f64)";
   (* void * gives up the element type and nothing else. It is still a pointer,
      and a scalar declared against one is still a finding. *)
+  (* A (Ptr const T) promises C will not write, and the header has to say so
+     too. *)
+  differs "a const pointer where the header may write"
+    "(declare-c blit [dst (Ptr const u8)  src (Ptr u8)  n i32] \"blit\")"
+    "parameter dst is (Ptr const u8)";
   differs "a scalar where the header says void *"
     "(declare-c blit [dst i64  src (Ptr u8)  n i32] \"blit\")"
     "parameter dst is i64";
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index b381a2fe..fad8cea3 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -441,9 +441,8 @@ let dev_sweep () =
    sanitized run must produce ASan's report and must NOT produce the
    handler's line, and that is the assertion.
 
-   And it has to be built at -O0. At the sweep's -O2 the write through a
-   pointer to a string literal's bytes does not fault at all — measured, both
-   builds print the unmodified string — so a case that is about what happens
+   And it has to be built at -O0. At the sweep's -O2 a store through a null
+   pointer is undefined and need not fault — so a case that is about what happens
    on a fault has to be compiled where the fault happens. Same family as the
    -O0/-O2 split [unchecked_controls] records for bounds.flan.
 
diff --git a/vendor/raylib/generated.flan b/vendor/raylib/generated.flan
index 7ff58dbd..2ce0d70f 100644
--- a/vendor/raylib/generated.flan
+++ b/vendor/raylib/generated.flan
@@ -78,7 +78,7 @@
 (declare-c load-file-data [file-name string  data-size (Ptr i32)] (Ptr u8) "LoadFileData")
 (declare-c unload-file-data [data (Ptr u8)] "UnloadFileData")
 (declare-c save-file-data [file-name string  data (Ptr u8)  data-size i32] bool "SaveFileData")
-(declare-c export-data-as-code [data (Ptr u8)  data-size i32  file-name string] bool "ExportDataAsCode")
+(declare-c export-data-as-code [data (Ptr const u8)  data-size i32  file-name string] bool "ExportDataAsCode")
 (declare-c file-exists [file-name string] bool "FileExists")
 (declare-c directory-exists [dir-path string] bool "DirectoryExists")
 (declare-c file-extension? [file-name string  ext string] bool "IsFileExtension")
@@ -95,9 +95,9 @@
 (declare-c path-file? [path string] bool "IsPathFile")
 (declare-c file-name-valid? [file-name string] bool "IsFileNameValid")
 (declare-c file-dropped? [] bool "IsFileDropped")
-(declare-c compress-data [data (Ptr u8)  data-size i32  comp-data-size (Ptr i32)] (Ptr u8) "CompressData")
-(declare-c decompress-data [comp-data (Ptr u8)  comp-data-size i32  data-size (Ptr i32)] (Ptr u8) "DecompressData")
-(declare-c decode-data-base-64 [data (Ptr u8)  output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64")
+(declare-c compress-data [data (Ptr const u8)  data-size i32  comp-data-size (Ptr i32)] (Ptr u8) "CompressData")
+(declare-c decompress-data [comp-data (Ptr const u8)  comp-data-size i32  data-size (Ptr i32)] (Ptr u8) "DecompressData")
+(declare-c decode-data-base-64 [data (Ptr const u8)  output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64")
 (declare-c compute-crc32 [data (Ptr u8)  data-size i32] u32 "ComputeCRC32")
 (declare-c compute-md5 [data (Ptr u8)  data-size i32] (Ptr u32) "ComputeMD5")
 (declare-c compute-sha1 [data (Ptr u8)  data-size i32] (Ptr u32) "ComputeSHA1")
@@ -117,7 +117,7 @@
 (declare-c set-mouse-scale [scale-x f32  scale-y f32] "SetMouseScale")
 (declare-c get-mouse-wheel-move-v [] Vector2 "GetMouseWheelMoveV")
 (declare-c update-camera-pro [camera (Ptr Camera3D)  movement Vector3  rotation Vector3  zoom f32] "UpdateCameraPro")
-(declare-c draw-line-strip-raw [points (Ptr Vector2)  point-count i32  color Color] "DrawLineStrip")
+(declare-c draw-line-strip-raw [points (Ptr const Vector2)  point-count i32  color Color] "DrawLineStrip")
 (declare-c draw-line-bezier [start-pos Vector2  end-pos Vector2  thick f32  color Color] "DrawLineBezier")
 (declare-c draw-circle-sector [center Vector2  radius f32  start-angle f32  end-angle f32  segments i32  color Color] "DrawCircleSector")
 (declare-c draw-circle-sector-lines [center Vector2  radius f32  start-angle f32  end-angle f32  segments i32  color Color] "DrawCircleSectorLines")
@@ -126,16 +126,16 @@
 (declare-c draw-rectangle-gradient-v [pos-x i32  pos-y i32  width i32  height i32  top Color  bottom Color] "DrawRectangleGradientV")
 (declare-c draw-rectangle-gradient-h [pos-x i32  pos-y i32  width i32  height i32  left Color  right Color] "DrawRectangleGradientH")
 (declare-c draw-rectangle-gradient-ex [rec Rectangle  top-left Color  bottom-left Color  top-right Color  bottom-right Color] "DrawRectangleGradientEx")
-(declare-c draw-triangle-fan-raw [points (Ptr Vector2)  point-count i32  color Color] "DrawTriangleFan")
-(declare-c draw-triangle-strip-raw [points (Ptr Vector2)  point-count i32  color Color] "DrawTriangleStrip")
+(declare-c draw-triangle-fan-raw [points (Ptr const Vector2)  point-count i32  color Color] "DrawTriangleFan")
+(declare-c draw-triangle-strip-raw [points (Ptr const Vector2)  point-count i32  color Color] "DrawTriangleStrip")
 (declare-c draw-poly [center Vector2  sides i32  radius f32  rotation f32  color Color] "DrawPoly")
 (declare-c draw-poly-lines [center Vector2  sides i32  radius f32  rotation f32  color Color] "DrawPolyLines")
 (declare-c draw-poly-lines-ex [center Vector2  sides i32  radius f32  rotation f32  line-thick f32  color Color] "DrawPolyLinesEx")
-(declare-c draw-spline-linear-raw [points (Ptr Vector2)  point-count i32  thick f32  color Color] "DrawSplineLinear")
-(declare-c draw-spline-basis-raw [points (Ptr Vector2)  point-count i32  thick f32  color Color] "DrawSplineBasis")
-(declare-c draw-spline-catmull-rom-raw [points (Ptr Vector2)  point-count i32  thick f32  color Color] "DrawSplineCatmullRom")
-(declare-c draw-spline-bezier-quadratic-raw [points (Ptr Vector2)  point-count i32  thick f32  color Color] "DrawSplineBezierQuadratic")
-(declare-c draw-spline-bezier-cubic-raw [points (Ptr Vector2)  point-count i32  thick f32  color Color] "DrawSplineBezierCubic")
+(declare-c draw-spline-linear-raw [points (Ptr const Vector2)  point-count i32  thick f32  color Color] "DrawSplineLinear")
+(declare-c draw-spline-basis-raw [points (Ptr const Vector2)  point-count i32  thick f32  color Color] "DrawSplineBasis")
+(declare-c draw-spline-catmull-rom-raw [points (Ptr const Vector2)  point-count i32  thick f32  color Color] "DrawSplineCatmullRom")
+(declare-c draw-spline-bezier-quadratic-raw [points (Ptr const Vector2)  point-count i32  thick f32  color Color] "DrawSplineBezierQuadratic")
+(declare-c draw-spline-bezier-cubic-raw [points (Ptr const Vector2)  point-count i32  thick f32  color Color] "DrawSplineBezierCubic")
 (declare-c draw-spline-segment-linear [p-1 Vector2  p-2 Vector2  thick f32  color Color] "DrawSplineSegmentLinear")
 (declare-c draw-spline-segment-basis [p-1 Vector2  p-2 Vector2  p-3 Vector2  p-4 Vector2  thick f32  color Color] "DrawSplineSegmentBasis")
 (declare-c draw-spline-segment-catmull-rom [p-1 Vector2  p-2 Vector2  p-3 Vector2  p-4 Vector2  thick f32  color Color] "DrawSplineSegmentCatmullRom")
@@ -148,7 +148,7 @@
 (declare-c get-spline-point-bezier-cubic [p-1 Vector2  c-2 Vector2  c-3 Vector2  p-4 Vector2  t f32] Vector2 "GetSplinePointBezierCubic")
 (declare-c load-image-raw [file-name string  width i32  height i32  format i32  header-size i32] Image "LoadImageRaw")
 (declare-c load-image-anim [file-name string  frames (Ptr i32)] Image "LoadImageAnim")
-(declare-c load-image-anim-from-memory [file-type string  file-data (Ptr u8)  data-size i32  frames (Ptr i32)] Image "LoadImageAnimFromMemory")
+(declare-c load-image-anim-from-memory [file-type string  file-data (Ptr const u8)  data-size i32  frames (Ptr i32)] Image "LoadImageAnimFromMemory")
 (declare-c load-image-from-texture [texture Texture2D] Image "LoadImageFromTexture")
 (declare-c load-image-from-screen [] Image "LoadImageFromScreen")
 (declare-c export-image-to-memory [image Image  file-type string  file-size (Ptr i32)] (Ptr u8) "ExportImageToMemory")
@@ -171,7 +171,7 @@
 (declare-c image-alpha-mask [image (Ptr Image)  alpha-mask Image] "ImageAlphaMask")
 (declare-c image-alpha-premultiply [image (Ptr Image)] "ImageAlphaPremultiply")
 (declare-c image-blur-gaussian [image (Ptr Image)  blur-size i32] "ImageBlurGaussian")
-(declare-c image-kernel-convolution [image (Ptr Image)  kernel (Ptr f32)  kernel-size i32] "ImageKernelConvolution")
+(declare-c image-kernel-convolution [image (Ptr Image)  kernel (Ptr const f32)  kernel-size i32] "ImageKernelConvolution")
 (declare-c image-resize-canvas [image (Ptr Image)  new-width i32  new-height i32  offset-x i32  offset-y i32  fill Color] "ImageResizeCanvas")
 (declare-c image-mipmaps [image (Ptr Image)] "ImageMipmaps")
 (declare-c image-dither [image (Ptr Image)  r-bpp i32  g-bpp i32  b-bpp i32  a-bpp i32] "ImageDither")
@@ -211,8 +211,8 @@
 (declare-c image-draw-text [dst (Ptr Image)  text string  pos-x i32  pos-y i32  font-size i32  color Color] "ImageDrawText")
 (declare-c image-draw-text-ex [dst (Ptr Image)  font Font  text string  position Vector2  font-size f32  spacing f32  tint Color] "ImageDrawTextEx")
 (declare-c load-texture-cubemap [image Image  layout i32] Texture2D "LoadTextureCubemap")
-(declare-c update-texture [texture Texture2D  pixels (Ptr u8)] "UpdateTexture")
-(declare-c update-texture-rec [texture Texture2D  rec Rectangle  pixels (Ptr u8)] "UpdateTextureRec")
+(declare-c update-texture [texture Texture2D  pixels (Ptr const u8)] "UpdateTexture")
+(declare-c update-texture-rec [texture Texture2D  rec Rectangle  pixels (Ptr const u8)] "UpdateTextureRec")
 (declare-c gen-texture-mipmaps [texture (Ptr Texture2D)] "GenTextureMipmaps")
 (declare-c set-texture-wrap [texture Texture2D  wrap i32] "SetTextureWrap")
 (declare-c color-is-equal [col-1 Color  col-2 Color] bool "ColorIsEqual")
@@ -229,13 +229,13 @@
 (declare-c set-pixel-color [dst-ptr (Ptr u8)  color Color  format i32] "SetPixelColor")
 (declare-c get-pixel-data-size [width i32  height i32  format i32] i32 "GetPixelDataSize")
 (declare-c load-font-from-image [image Image  key Color  first-char i32] Font "LoadFontFromImage")
-(declare-c load-font-from-memory [file-type string  file-data (Ptr u8)  data-size i32  font-size i32  codepoints (Ptr i32)  codepoint-count i32] Font "LoadFontFromMemory")
-(declare-c load-font-data [file-data (Ptr u8)  data-size i32  font-size i32  codepoints (Ptr i32)  codepoint-count i32  type i32] (Ptr GlyphInfo) "LoadFontData")
-(declare-c gen-image-font-atlas [glyphs (Ptr GlyphInfo)  glyph-recs (Ptr (Ptr Rectangle))  glyph-count i32  font-size i32  padding i32  pack-method i32] Image "GenImageFontAtlas")
+(declare-c load-font-from-memory [file-type string  file-data (Ptr const u8)  data-size i32  font-size i32  codepoints (Ptr i32)  codepoint-count i32] Font "LoadFontFromMemory")
+(declare-c load-font-data [file-data (Ptr const u8)  data-size i32  font-size i32  codepoints (Ptr i32)  codepoint-count i32  type i32] (Ptr GlyphInfo) "LoadFontData")
+(declare-c gen-image-font-atlas [glyphs (Ptr const GlyphInfo)  glyph-recs (Ptr (Ptr Rectangle))  glyph-count i32  font-size i32  padding i32  pack-method i32] Image "GenImageFontAtlas")
 (declare-c unload-font-data [glyphs (Ptr GlyphInfo)  glyph-count i32] "UnloadFontData")
 (declare-c export-font-as-code [font Font  file-name string] bool "ExportFontAsCode")
 (declare-c draw-text-pro [font Font  text string  position Vector2  origin Vector2  rotation f32  font-size f32  spacing f32  tint Color] "DrawTextPro")
-(declare-c draw-text-codepoints [font Font  codepoints (Ptr i32)  codepoint-count i32  position Vector2  font-size f32  spacing f32  tint Color] "DrawTextCodepoints")
+(declare-c draw-text-codepoints [font Font  codepoints (Ptr const i32)  codepoint-count i32  position Vector2  font-size f32  spacing f32  tint Color] "DrawTextCodepoints")
 (declare-c set-text-line-spacing [spacing i32] "SetTextLineSpacing")
 (declare-c load-codepoints [text string  count (Ptr i32)] (Ptr i32) "LoadCodepoints")
 (declare-c unload-codepoints [codepoints (Ptr i32)] "UnloadCodepoints")
@@ -246,7 +246,7 @@
 (declare-c text-is-equal [text-1 string  text-2 string] bool "TextIsEqual")
 (declare-c text-length [text string] u32 "TextLength")
 (declare-c text-subtext [text string  position i32  length i32] string "TextSubtext")
-(declare-c text-join [text-list (Ptr (Ptr i8))  count i32  delimiter string] string "TextJoin")
+(declare-c text-join [text-list (Ptr const (Ptr i8))  count i32  delimiter string] string "TextJoin")
 (declare-c text-split [text string  delimiter i8  count (Ptr i32)] (Ptr (Ptr i8)) "TextSplit")
 (declare-c text-find-index [text string  find string] i32 "TextFindIndex")
 (declare-c text-to-upper [text string] string "TextToUpper")
@@ -260,7 +260,7 @@
 (declare-c draw-point-3d [position Vector3  color Color] "DrawPoint3D")
 (declare-c draw-circle-3d [center Vector3  radius f32  rotation-axis Vector3  rotation-angle f32  color Color] "DrawCircle3D")
 (declare-c draw-triangle-3d [v-1 Vector3  v-2 Vector3  v-3 Vector3  color Color] "DrawTriangle3D")
-(declare-c draw-triangle-strip-3d-raw [points (Ptr Vector3)  point-count i32  color Color] "DrawTriangleStrip3D")
+(declare-c draw-triangle-strip-3d-raw [points (Ptr const Vector3)  point-count i32  color Color] "DrawTriangleStrip3D")
 (declare-c draw-cube-wires-v [position Vector3  size Vector3  color Color] "DrawCubeWiresV")
 (declare-c draw-sphere-ex [center-pos Vector3  radius f32  rings i32  slices i32  color Color] "DrawSphereEx")
 (declare-c draw-cylinder [position Vector3  radius-top f32  radius-bottom f32  height f32  slices i32  color Color] "DrawCylinder")
@@ -286,7 +286,7 @@
 (declare-c draw-billboard-rec [camera Camera3D  texture Texture2D  source Rectangle  position Vector3  size Vector2  tint Color] "DrawBillboardRec")
 (declare-c draw-billboard-pro [camera Camera3D  texture Texture2D  source Rectangle  position Vector3  up Vector3  size Vector2  origin Vector2  rotation f32  tint Color] "DrawBillboardPro")
 (declare-c upload-mesh [mesh (Ptr Mesh)  dynamic bool] "UploadMesh")
-(declare-c update-mesh-buffer [mesh Mesh  index i32  data (Ptr u8)  data-size i32  offset i32] "UpdateMeshBuffer")
+(declare-c update-mesh-buffer [mesh Mesh  index i32  data (Ptr const u8)  data-size i32  offset i32] "UpdateMeshBuffer")
 (declare-c unload-mesh [mesh Mesh] "UnloadMesh")
 (declare-c get-mesh-bounding-box [mesh Mesh] BoundingBox "GetMeshBoundingBox")
 (declare-c gen-mesh-tangents [mesh (Ptr Mesh)] "GenMeshTangents")
@@ -312,14 +312,14 @@
 (declare-c get-ray-collision-mesh [ray Ray  mesh Mesh  transform Matrix] RayCollision "GetRayCollisionMesh")
 (declare-c get-ray-collision-triangle [ray Ray  p-1 Vector3  p-2 Vector3  p-3 Vector3] RayCollision "GetRayCollisionTriangle")
 (declare-c get-ray-collision-quad [ray Ray  p-1 Vector3  p-2 Vector3  p-3 Vector3  p-4 Vector3] RayCollision "GetRayCollisionQuad")
-(declare-c load-wave-from-memory [file-type string  file-data (Ptr u8)  data-size i32] Wave "LoadWaveFromMemory")
-(declare-c update-sound [sound Sound  data (Ptr u8)  sample-count i32] "UpdateSound")
+(declare-c load-wave-from-memory [file-type string  file-data (Ptr const u8)  data-size i32] Wave "LoadWaveFromMemory")
+(declare-c update-sound [sound Sound  data (Ptr const u8)  sample-count i32] "UpdateSound")
 (declare-c export-wave-as-code [wave Wave  file-name string] bool "ExportWaveAsCode")
-(declare-c load-music-stream-from-memory [file-type string  data (Ptr u8)  data-size i32] Music "LoadMusicStreamFromMemory")
+(declare-c load-music-stream-from-memory [file-type string  data (Ptr const u8)  data-size i32] Music "LoadMusicStreamFromMemory")
 (declare-c load-audio-stream [sample-rate u32  sample-size u32  channels u32] AudioStream "LoadAudioStream")
 (declare-c audio-stream-valid? [stream AudioStream] bool "IsAudioStreamValid")
 (declare-c unload-audio-stream [stream AudioStream] "UnloadAudioStream")
-(declare-c update-audio-stream [stream AudioStream  data (Ptr u8)  frame-count i32] "UpdateAudioStream")
+(declare-c update-audio-stream [stream AudioStream  data (Ptr const u8)  frame-count i32] "UpdateAudioStream")
 (declare-c audio-stream-processed? [stream AudioStream] bool "IsAudioStreamProcessed")
 (declare-c play-audio-stream [stream AudioStream] "PlayAudioStream")
 (declare-c pause-audio-stream [stream AudioStream] "PauseAudioStream")
diff --git a/vendor/raylib/raylib.flan b/vendor/raylib/raylib.flan
index cba15d63..702129ba 100644
--- a/vendor/raylib/raylib.flan
+++ b/vendor/raylib/raylib.flan
@@ -582,10 +582,10 @@
 ;; out-of-bounds read, and raylib answers false for a polygon with no points
 ;; anyway.
 (declare-c collision-point-poly?-raw
-  [point Vector2  points (Ptr Vector2)  count i32] bool
+  [point Vector2  points (Ptr const Vector2)  count i32] bool
   "CheckCollisionPointPoly")
 
-(defn collision-point-poly? [point Vector2  points [Vector2]] bool
+(defn collision-point-poly? [point Vector2  points [const Vector2]] bool
   (if (= (length points) 0)
     false
     (collision-point-poly?-raw point (addr (at points 0)) (length points))))
@@ -801,7 +801,7 @@
 ;; which integer type a C count parameter is. The Flan wrapper below takes the
 ;; slice apart, which is where that idiom lives everywhere else in this file.
 (declare-c load-image-from-memory-raw
-  [file-type string  file-data (Ptr u8)  data-size i32] Image
+  [file-type string  file-data (Ptr const u8)  data-size i32] Image
   "LoadImageFromMemory")
 
 ;; Empty is answered here rather than passed on, exactly as in
@@ -1015,42 +1015,42 @@
 ;; Each -raw below is a generated declaration whose name moved aside; see the
 ;; `name` lines at the foot of `bindings`.
 
-(defn draw-line-strip [points [Vector2]  color Color] ()
+(defn draw-line-strip [points [const Vector2]  color Color] ()
   (when (> (length points) 0)
     (draw-line-strip-raw (addr (at points 0)) (length points) color)))
 
-(defn draw-triangle-fan [points [Vector2]  color Color] ()
+(defn draw-triangle-fan [points [const Vector2]  color Color] ()
   (when (> (length points) 0)
     (draw-triangle-fan-raw (addr (at points 0)) (length points) color)))
 
-(defn draw-triangle-strip [points [Vector2]  color Color] ()
+(defn draw-triangle-strip [points [const Vector2]  color Color] ()
   (when (> (length points) 0)
     (draw-triangle-strip-raw (addr (at points 0)) (length points) color)))
 
-(defn draw-triangle-strip-3d [points [Vector3]  color Color] ()
+(defn draw-triangle-strip-3d [points [const Vector3]  color Color] ()
   (when (> (length points) 0)
     (draw-triangle-strip-3d-raw (addr (at points 0)) (length points) color)))
 
 ;; The five spline drawers. raylib reads the same point array five different
 ;; ways; the only difference between these wrappers is which one it calls.
-(defn draw-spline-linear [points [Vector2]  thick f32  color Color] ()
+(defn draw-spline-linear [points [const Vector2]  thick f32  color Color] ()
   (when (> (length points) 0)
     (draw-spline-linear-raw (addr (at points 0)) (length points) thick color)))
 
-(defn draw-spline-basis [points [Vector2]  thick f32  color Color] ()
+(defn draw-spline-basis [points [const Vector2]  thick f32  color Color] ()
   (when (> (length points) 0)
     (draw-spline-basis-raw (addr (at points 0)) (length points) thick color)))
 
-(defn draw-spline-catmull-rom [points [Vector2]  thick f32  color Color] ()
+(defn draw-spline-catmull-rom [points [const Vector2]  thick f32  color Color] ()
   (when (> (length points) 0)
     (draw-spline-catmull-rom-raw (addr (at points 0)) (length points) thick color)))
 
-(defn draw-spline-bezier-quadratic [points [Vector2]  thick f32  color Color] ()
+(defn draw-spline-bezier-quadratic [points [const Vector2]  thick f32  color Color] ()
   (when (> (length points) 0)
     (draw-spline-bezier-quadratic-raw
       (addr (at points 0)) (length points) thick color)))
 
-(defn draw-spline-bezier-cubic [points [Vector2]  thick f32  color Color] ()
+(defn draw-spline-bezier-cubic [points [const Vector2]  thick f32  color Color] ()
   (when (> (length points) 0)
     (draw-spline-bezier-cubic-raw
       (addr (at points 0)) (length points) thick color)))
@@ -1595,7 +1595,7 @@
 ;; half no longer carries the string-faced version at all — a binding that is
 ;; wrong for the only direction it reads in is worse than no binding.
 (declare-c get-codepoint-previous-raw
-  [text (Ptr u8)  codepoint-size (Ptr i32)] i32
+  [text (Ptr const u8)  codepoint-size (Ptr i32)] i32
   "GetCodepointPrevious")
 
 ;; The face a caller wants: the bytes and an offset into them, rather than an

From 37e577d5e165f6358b89e9a27846fb30574b7ad8 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 12:46:07 +0700
Subject: [PATCH 5/7] (Ptr const T) is documented beside [const T], and the
 TODO entries for it are closed

---
 TODO.org       | 10 +---------
 web/index.html |  1 +
 2 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/TODO.org b/TODO.org
index cce2e0a9..545df224 100644
--- a/TODO.org
+++ b/TODO.org
@@ -975,10 +975,7 @@ deliberate absence.
 
 ** DONE A read-only slice type
 CLOSED: [2026-09-25]
-=[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused.
-
-** TODO The address of a read-only element is taken without complaint
-=(addr (at v i))= over a =[const T]= answers a writable =(Ptr T)=, so =slice-from-ptr= launders one back into a =[T]=; a string's byte refuses the same =addr=. Allowed because raylib's =load-image-from-memory= and =get-codepoint-previous= have no other way to hand a =[const u8]= to C. Decision needed: a const pointer type, or a refusal plus another route to C.
+=[const T]= and =(Ptr const T)=; a =[T]= or =(Ptr T)= converts at the top of a type or under another const one, never inside a writable one. The const is shallow: an element of a =[const [u8]]= and a Vec's buffer are writable. The address of read-only storage, a string's byte included, is a =(Ptr const T)=, and a C =const T *= parameter takes one.
 
 ** TODO (slice d 1) over a dyn string is refused where (at d i) works
 The typed and dyn spaces disagree about a spelling, which the standing rule
@@ -1089,11 +1086,6 @@ Decided 2026-09-25: the type-limit constants as a form taking a type, Odin's
 max(T), valid at any numeric type or a numeric?-bounded variable. For a float,
 min-of is the most negative finite value.
 
-** NEXT (Ptr const T), the pointer beside [const T]
-Decided 2026-09-25: addr through a read-only slice gives a (Ptr const T), which
-nothing writes through; (Ptr T) widens to it and never back; a C parameter
-declared const T* takes one. Closes the addr hole in [const T].
-
 * Backends
 
 ** DONE The x86 backend tracks LLVM at -O0
diff --git a/web/index.html b/web/index.html
index 67ffbe3f..a232e51b 100644
--- a/web/index.html
+++ b/web/index.html
@@ -526,6 +526,7 @@ notation reads as exactly one data item.
    
 (Pool T)generational slab storage, owning, copies the same wayitems + slots + its allocator
 (Handle T)a reference into a pool that reports a dead referentindex and generation packed into an i64
 (Ptr T)raw pointera pointer
+(Ptr const T)a pointer nothing is written through: the address of read-only storage, and what a C const T * takes. A (Ptr T) converts to one, never the reversea pointer
 (Option T)Some / Nonetag byte + T
 (Fn [T ...] R)a function value, which may have captureda code address and an environment pointer
 (CFn [T ...] R)a function value that cannot capture — the C is what a C function pointer would need, not a way to reach C todaya pointer

From 1e5be63a1ad46e9849d148086d7398b023ce6d89 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 13:08:29 +0700
Subject: [PATCH 6/7] An array reached through read-only storage slices to a
 [const T], a Vec or Map copied out of one stays read-only through lets, and
 an if's const and writable branches meet at const in either order

---
 docs/BUILT.md     |   2 +-
 lib/check.ml      | 142 ++++++++++++++++++++++++++++++++--------------
 lib/types.ml      |   8 +++
 test/test_flan.ml |  56 +++++++++++++++---
 4 files changed, 157 insertions(+), 51 deletions(-)

diff --git a/docs/BUILT.md b/docs/BUILT.md
index 9974edcd..5050d0a2 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -1043,7 +1043,7 @@ the only two under which a mark and a sweep run at all. `dev_segv` sits beside t
 program that faults cannot be compared against an unsanitized run — that build's handler parks in the break loop, and
 the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a weak `__asan_init` and declines to
 install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's
-line, built at `-O0` because at `-O2` the write through a pointer to a literal's bytes does not fault at all. That yield had
+line, built at `-O0` because at `-O2` a store through a zeroed `(Ptr u8)` is undefined and need not fault. That yield had
 never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm.
 What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own
 path and has no `--sanitize` to pass it.
diff --git a/lib/check.ml b/lib/check.ml
index dfd97c60..4be7ddf2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -556,6 +556,8 @@ type ctx = {
      the outer scope is a list and the names on it were not all written for
      this body's sake. *)
   mutable caught : (string * (binding * int)) list;
+  (* Locals bound from read-only storage, and the view each came through. *)
+  mutable const_locals : (int * Types.t) list;
   (* The context this body was lifted out of, so that capture can be
      transitive: an [fn] inside an [fn] naming a local of the function both
      were written in is captured by the middle one and then by the inner one
@@ -2211,11 +2213,12 @@ let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
    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) =
+let rec const_reached ?(local = fun (_ : int) -> None) (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
+    const_steps (const_reached ~local target) target.Tast.ty (List.length idx)
+  | Tast.Field (target, _) -> const_reached ~local target
+  | Tast.Local s -> local s
   | Tast.Deref p ->
     (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
   | _ -> None
@@ -2230,6 +2233,15 @@ and const_steps ro (ty : Types.t) n =
     | Types.Array (_, t) -> const_steps ro t (n - 1)
     | _ -> ro
 
+(* A copy of a read-only slice's elements that can be written, spelled so it
+   compiles. Only for elements that own nothing: an element holding a Vec or
+   a Map — directly or inside a struct — would copy only its header, and the
+   copy would share the original's block. *)
+let const_copy (e : Types.t) =
+  match e with
+  | Types.Vec _ | Types.Map _ | Types.Named _ -> None
+  | _ -> Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
+
 (* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
 let refuse_const_place loc (view : Types.t) =
   match view with
@@ -2248,30 +2260,19 @@ 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
+       value and not a place. %s"
+      (Types.to_string view)
+      (match const_copy elem with
+       | Some c ->
+         Printf.sprintf
+           "Write into a slice that can be written: %s copies v's elements \
+            into one" c
+       | None ->
+         Printf.sprintf "Where it has to be written, take it as a [%s] instead"
+           (Types.to_string elem))
 
 (* A runtime call, with the result type spelled at the site. *)
-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))
+let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
 
 (* ── The allocation registry's note ──────────────────────────────────
 
@@ -3116,14 +3117,19 @@ let const_note ~(want : Types.t) ~(got : Types.t) =
     when Types.equal e e' ->
     let copy =
       match e with
-      | Types.Int Types.U8 -> "(bytes (string v))"
-      | _ -> Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e)
+      | Types.Int Types.U8 -> Some "(bytes (string v))"
+      | _ -> const_copy e
     in
     Printf.sprintf
       " — a %s can only be read, and never becomes a %s that can be written \
-       through. %s copies v into a %s of its own; where nothing writes \
-       through it, the %s can be declared %s instead"
-      (Types.to_string got) (Types.to_string want) copy (Types.to_string want)
+       through. %sWhere nothing writes through it, the %s can be declared %s \
+       instead"
+      (Types.to_string got) (Types.to_string want)
+      (match copy with
+       | Some c ->
+         Printf.sprintf "%s copies v into a %s of its own. " c
+           (Types.to_string want)
+       | None -> "")
       (Types.to_string want) (Types.to_string got)
   | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
     when Types.equal e e' ->
@@ -3271,7 +3277,7 @@ let hash_ty = Types.Int Types.U64
    would share a slot counter. *)
 let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
-    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
+    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
     owner = "" }
 
@@ -5019,6 +5025,13 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
             | _ -> ());
            (* Locals are assignable places; parameters are not. *)
            let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
+           (* A Vec or Map header copied out of read-only storage still
+              shares its block with the original, so a push through the copy
+              is a push through the original. The local remembers where it
+              came from, for [refuse_const_change]. *)
+           Option.iter
+             (fun view -> ctx.const_locals <- (slot, view) :: ctx.const_locals)
+             (const_reached ~local:(const_local ctx) v);
            (slot, v))
         bs
     in
@@ -5478,10 +5491,18 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
     (* With no expectation the then-branch supplies one for the else-branch,
        unless it diverges, in which case the else-branch decides. *)
+    (* A slice or a pointer from the then-branch is not the else-branch's
+       want: the two may differ only in const, and they meet at the
+       read-only one whichever side it is on — [Types.const_join]. *)
+    let free_join =
+      want = None
+      && (match t.Tast.ty with Types.Slice _ | Types.Ptr _ -> true | _ -> false)
+    in
     let ewant =
       match want with
       | Some _ -> want
-      | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
+      | None ->
+        if t.Tast.ty = Types.Never || free_join then None else Some t.Tast.ty
     in
     (* [(and a b c)] is [(let [t a] (if t (let [u b] (if u c u)) t))], so the
        *last* operand of an [and] is the then arm and the sentinel that carries
@@ -5514,6 +5535,13 @@ and check_if ctx ?(tail = false) ?want loc c t e =
            one type — this operand is %s, and false is a bool"
           (Types.to_string t.Tast.ty)
     in
+    let t, e =
+      match free_join, Types.const_join t.Tast.ty e.Tast.ty with
+      | true, Some j when e.Tast.ty <> Types.Never ->
+        expect ctx t.Tast.loc ~want:(Some j) t,
+        expect ctx e.Tast.loc ~want:(Some j) e
+      | _ -> t, e
+    in
     let ty =
       if t.Tast.ty = Types.Never then e.Tast.ty
       else if e.Tast.ty = Types.Never then t.Tast.ty
@@ -6540,12 +6568,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"
 
-(* [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
-   other way across: [load-image-from-memory] over an [embed] is the case. So
-   the address of a read-only element may be taken, and it is a store that is
-   refused. *)
 (* Whether a checked place is read-only storage: reached through a
    [[const T]] or a (Ptr const T), or a byte of a string. Its address is a
    (Ptr const T). *)
@@ -6566,6 +6588,28 @@ and place_const (p : Tast.place) =
     const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
     || through_string t.Tast.ty (List.length idx)
 
+and const_local ctx slot = List.assoc_opt slot ctx.const_locals
+
+(* Growing, shrinking or freeing a Vec or a Map that is read-only storage, or
+   a copy of one. The backends hand the runtime the container's address, and
+   the header's block is shared with every copy, so this is the 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 refuse_const_change ctx loc (target : Tast.expr) =
+  match const_reached ~local:(const_local ctx) target with
+  | None -> ()
+  | Some view ->
+    let t = Types.to_string target.Tast.ty in
+    let holder =
+      match view with Types.Slice (_, e) | Types.Ptr (_, e) -> e | t -> t
+    in
+    Loc.failk "check/store-through-const" loc
+      "this changes a %s reached through a %s, which can only be read. Where \
+       it has to change, take the %s it lives in as a [%s] or a (Ptr %s) \
+       instead"
+      t (Types.to_string view) (Types.to_string holder)
+      (Types.to_string holder) (Types.to_string holder)
+
 and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
   match p with
   | Ast.Pvar name ->
@@ -8059,6 +8103,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     (match args with
      | [ target; x ] ->
        let target = check ctx target in
+       refuse_const_change ctx loc target;
        (* A push into a dyn container is a call and nothing else: no allocation
           guard, no restart, no region check. The dyn runtime owns the storage
           and answers a failure to grow it on its own terms — the guard and the
@@ -8099,6 +8144,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     (match args with
      | [ target; n ] ->
        let target = check ctx target in
+       refuse_const_change ctx loc target;
        let n = check ctx ~want:index_ty n in
        let n64 =
          mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
@@ -8142,6 +8188,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
   | "free" ->
     arity ctx loc name 1 args;
     let target = check ctx (List.hd args) in
+    refuse_const_change ctx loc target;
     (* A container of owning elements is refused here, and a reader will
        assume the opposite — that [free] recurses — so this says why it does
        not and what does.
@@ -8311,6 +8358,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     (match args with
      | [ target; k; v ] ->
        let target = check ctx target in
+       refuse_const_change ctx loc target;
        (* A put into a dyn map is a call and nothing else, the way a push into
           a dyn vec is: the runtime owns the storage, so there is no guard, no
           restart and no region check. An equal key's value is replaced. *)
@@ -8436,6 +8484,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     (match args with
      | [ target; k ] ->
        let target = check ctx target in
+       refuse_const_change ctx loc target;
        let kt, vt = map_kv loc "map-remove" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred exactly as [get] is, and with [None] for the same reason:
@@ -8901,6 +8950,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           calling it a byte slice would hand out a writable-looking view of
           storage the program does not own. *)
        let result = match ty with
+         (* An array reached through a [[const T]] or a (Ptr const T) is
+            read-only storage, and so is a view of it. *)
+         | Types.Array (_, t) when const_reached target <> None ->
+           Types.Slice (Types.Const, t)
          | Types.Array (_, t) -> Types.Slice (Types.Mut, t)
          | Types.Slice (m, t) -> Types.Slice (m, t)
          | Types.String -> Types.String
@@ -10036,9 +10089,12 @@ and generic_call ctx ~want loc name vars pats pret args =
               | Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) ->
                 Printf.sprintf
                   " — %s takes a slice it may write through, and a %s can \
-                   only be read. (slice (into v (vec-new %s))) copies v into \
-                   one that can be written"
-                  name (Types.to_string a.Tast.ty) (Types.to_string e)
+                   only be read%s"
+                  name (Types.to_string a.Tast.ty)
+                  (match const_copy e with
+                   | Some c ->
+                     Printf.sprintf ". %s copies v into one that can be written" c
+                   | None -> "")
               | _ -> "");
          a)
       pats args
@@ -10395,7 +10451,7 @@ and trial ctx f =
      resource failure into a wrong answer. *)
   let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
                        defers; defer_slot; defer_ok; defer_block; outer = _;
-                       outer_what; caught; envslot; parent = _;
+                       outer_what; caught; const_locals; envslot; parent = _;
                        in_frames; loops; tail; in_defer;
                        owner = _ } = ctx in
   match f () with
@@ -10406,7 +10462,7 @@ and trial ctx f =
     ctx.defers <- defers; ctx.defer_slot <- defer_slot;
     ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
     ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
-    ctx.caught <- caught; ctx.envslot <- envslot;
+    ctx.caught <- caught; ctx.const_locals <- const_locals; ctx.envslot <- envslot;
     ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
     Error d
 
diff --git a/lib/types.ml b/lib/types.ml
index bccd930a..eefb0bbf 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -355,6 +355,14 @@ let rec const_widens ~(from : t) ~(into : t) =
    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. *)
+(* The one type two branches of an [if] meet at when they differ only in
+   const: the read-only one, whichever branch it came from. *)
+let const_join a b =
+  if equal a b then Some a
+  else if const_widens ~from:a ~into:b then Some b
+  else if const_widens ~from:b ~into:a then Some a
+  else None
+
 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'
diff --git a/test/test_flan.ml b/test/test_flan.ml
index adc0a418..31722fd1 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2291,22 +2291,22 @@ let () =
     ~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)]";
+    ~needle:"reached 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)]";
+    ~needle:"reached 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)]";
+    ~needle:"reached 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)]";
+    ~needle:"reached 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)]";
+    ~needle:"reached 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]";
+    ~needle:"reached 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"
@@ -2341,7 +2341,7 @@ let () =
     ~needle:"this writes through a (Ptr const P)";
   rejects_check "a push through a const pointer"
     "(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))"
-    ~needle:"behind a (Ptr const (Vec i32))";
+    ~needle:"this changes a (Vec i32) reached through a (Ptr const (Vec i32))";
   rejects_check "a const pointer is not a writable one"
     "(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))"
     ~needle:"expected (Ptr u8), found (Ptr const u8)";
@@ -2361,6 +2361,48 @@ let () =
     "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
   accepts "vec-new reads (Ptr const u8) as a type"
     "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
+  (* A Vec header copied out of read-only storage shares its block, so the
+     copy is as read-only as the original, through any number of lets. *)
+  rejects_check "push through a let-bound copy of a const element"
+    "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))"
+    ~needle:"reached through a [const (Vec i32)]";
+  rejects_check "reserve through a copy of a copy"
+    "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))"
+    ~needle:"reached through a [const (Vec i32)]";
+  rejects_check "put through a let-bound copy of a const element"
+    "(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))"
+    ~needle:"reached through a [const (Map string i32)]";
+  rejects_check "push into a field of a let-bound copy"
+    "(defstruct P [v (Vec i32)]) \
+     (defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))"
+    ~needle:"take the P it lives in as a [P]";
+  rejects_check "no copy of Vec headers is suggested"
+    "(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
+    ~needle:"take it as a [(Vec i32)] instead";
+  (* A fixed array reached through read-only storage slices to a read-only
+     view. *)
+  rejects_check "slice of an array element of a const slice"
+    "(defn f [cs [const [4 u8]]] () (let [s (slice (at cs 0))] (set (at s 0) 9)))"
+    ~needle:"this writes through a [const u8]";
+  rejects_check "slice of an array behind a const pointer"
+    "(defn f [p (Ptr const [4 u8])] () (let [s (slice (deref p))] (set (at s 0) 9)))"
+    ~needle:"this writes through a [const u8]";
+  rejects_check "slice of an array field reached through a const slice"
+    "(defstruct B [buf [4 u8]]) \
+     (defn f [cs [const B]] () (let [s (slice (.buf (at cs 0)))] (set (at s 0) 9)))"
+    ~needle:"this writes through a [const u8]";
+  infers "a local array still slices to a writable slice"
+    "(let [a [1 2]] (slice a))" "[i32]";
+  (* The branches of an if meet at the read-only type, in either order. *)
+  accepts "if: writable then read-only"
+    "(defn f [c bool  cs [const u8]  ms [u8]] i32 (length (if c ms cs)))";
+  accepts "if: read-only then writable"
+    "(defn f [c bool  cs [const u8]  ms [u8]] i32 (length (if c cs ms)))";
+  rejects_check "and the join is read-only"
+    "(defn f [c bool  cs [const u8]  ms [u8]] () (set (at (if c ms cs) 0) 1))"
+    ~needle:"this writes through a [const u8]";
+  accepts "if over pointers joins the same way"
+    "(defn f [c bool  a (Ptr const i32)  b (Ptr i32)] i32 (deref (if c b a)))";
   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]. *)

From c6ad71dc5bdc5da0ffee9415c2177288b8989f1b Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 13:30:47 +0700
Subject: [PATCH 7/7] A value that owns storage is never copied out of
 read-only storage, and two arguments at one type variable meet at const

---
 lib/check.ml                   | 173 ++++++++++++++++++++++-----------
 lib/types.ml                   |  17 ++--
 test/programs/const-owned.flan |  39 ++++++++
 test/test_acceptance.ml        |   6 ++
 test/test_flan.ml              |  90 ++++++++++++++---
 5 files changed, 247 insertions(+), 78 deletions(-)
 create mode 100644 test/programs/const-owned.flan

diff --git a/lib/check.ml b/lib/check.ml
index e42e90ab..60c3244a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -556,8 +556,11 @@ type ctx = {
      the outer scope is a list and the names on it were not all written for
      this body's sake. *)
   mutable caught : (string * (binding * int)) list;
-  (* Locals bound from read-only storage, and the view each came through. *)
-  mutable const_locals : (int * Types.t) list;
+  (* Whether the form being checked is the target of a place — indexed,
+     sliced, a field read, its address taken — rather than a value. Granted by
+     [check_target] to the one form it checks and withdrawn at the top of
+     [check]. See [refuse_owned_copy]. *)
+  mutable place_ok : bool;
   (* The context this body was lifted out of, so that capture can be
      transitive: an [fn] inside an [fn] naming a local of the function both
      were written in is captured by the middle one and then by the inner one
@@ -1859,7 +1862,16 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
   | Types.Var v, a ->
     (match List.assoc_opt v !subst with
      | None -> subst := (v, a) :: !subst; true
-     | Some b -> Types.equal a b)
+     | Some b when Types.equal a b -> true
+     (* Two arguments that differ only in const bind the variable to the
+        read-only one, whichever came first — the same meeting an [if]'s two
+        branches have. [expect] converts the writable argument afterwards. *)
+     | Some b when ro ->
+       (match Types.const_join a b with
+        | Some j ->
+          subst := (v, j) :: List.remove_assoc v !subst; true
+        | None -> false)
+     | Some _ -> false)
   | Types.Slice (m, p), Types.Slice (m', a)
     when m = m' || (ro && m = Types.Const) ->
     bind_ty ~ro:(m = Types.Const) subst p a
@@ -2198,12 +2210,11 @@ let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
    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 ?(local = fun (_ : int) -> None) (e : Tast.expr) =
+let rec const_reached (e : Tast.expr) =
   match e.Tast.e with
   | Tast.Prim (Tast.At, target :: idx) ->
-    const_steps (const_reached ~local target) target.Tast.ty (List.length idx)
-  | Tast.Field (target, _) -> const_reached ~local target
-  | Tast.Local s -> local s
+    const_steps (const_reached target) target.Tast.ty (List.length idx)
+  | Tast.Field (target, _) -> const_reached target
   | Tast.Deref p ->
     (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
   | _ -> None
@@ -2222,13 +2233,12 @@ and const_steps ro (ty : Types.t) n =
    compiles. Only for elements that own nothing: an element holding a Vec or
    a Map — directly or inside a struct — would copy only its header, and the
    copy would share the original's block. *)
-let const_copy (e : Types.t) =
-  match e with
-  | Types.Vec _ | Types.Map _ | Types.Named _ -> None
-  | _ -> Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
+let const_copy env (e : Types.t) =
+  if owning env e then None
+  else Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
 
 (* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
-let refuse_const_place loc (view : Types.t) =
+let refuse_const_place env loc (view : Types.t) =
   match view with
   | Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
     Loc.failk "check/store-through-const" loc
@@ -2247,7 +2257,7 @@ let refuse_const_place loc (view : Types.t) =
       "this writes through a %s, which can only be read, so the element is a \
        value and not a place. %s"
       (Types.to_string view)
-      (match const_copy elem with
+      (match const_copy env elem with
        | Some c ->
          Printf.sprintf
            "Write into a slice that can be written: %s copies v's elements \
@@ -3096,14 +3106,14 @@ let numeric_note ~(want : Types.t) ~(got : Types.t) =
    copies it names compile today: [string] reads any byte slice and [bytes]
    copies a string, and [into] pushes any slice's elements into a Vec that
    [slice] then views. *)
-let const_note ~(want : Types.t) ~(got : Types.t) =
+let const_note env ~(want : Types.t) ~(got : Types.t) =
   match want, got with
   | Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e')
     when Types.equal e e' ->
     let copy =
       match e with
       | Types.Int Types.U8 -> Some "(bytes (string v))"
-      | _ -> const_copy e
+      | _ -> const_copy env e
     in
     Printf.sprintf
       " — a %s can only be read, and never becomes a %s that can be written \
@@ -3200,7 +3210,7 @@ let expect ctx loc ~want (got : Tast.expr) =
       Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
         (Types.to_string w) (Types.to_string got.Tast.ty)
         (numeric_note ~want:w ~got:got.Tast.ty)
-        (const_note ~want:w ~got:got.Tast.ty)
+        (const_note ctx.env ~want:w ~got:got.Tast.ty)
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -3262,7 +3272,7 @@ let hash_ty = Types.Int Types.U64
    would share a slot counter. *)
 let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
-    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
+    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
     owner = "" }
 
@@ -3701,7 +3711,51 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
   | [], [] -> call
   | pre, post -> mk loc ret (Tast.Do (pre @ [ call ] @ post))
 
+(* Every expression goes through here, and [check_value] is the one that
+   knows the forms. What this adds is [refuse_owned_copy], asked of whatever
+   came back unless the form was checked as the target of a place. *)
 let rec check ctx ?want (e : Ast.expr) : Tast.expr =
+  let place = ctx.place_ok in
+  ctx.place_ok <- false;
+  let r = check_value ctx ?want e in
+  if not place then refuse_owned_copy ctx r;
+  r
+
+(* A form checked as the target of a place: indexed, sliced, a field read,
+   measured, its address taken, or handed to a builtin that works on the
+   container where it stands. *)
+and check_target ctx (e : Ast.expr) =
+  ctx.place_ok <- true;
+  check ctx e
+
+(* Decision 81 (2026-09-25). A value that owns storage — a Vec, a Map, or an
+   array, Option or struct holding one — reached through a [[const T]] or a
+   (Ptr const T) is not copied out as a value. Its header shares its block
+   with the original, so a copy that could be grown, freed or handed on as
+   writable would be the original written through. It is used where it
+   stands instead: indexed, sliced (to a [[const T]]), its fields read when
+   they own nothing, or its address taken as a (Ptr const T). Refusing at the
+   source is the whole rule; there is no tracking of where a copy went. *)
+and refuse_owned_copy ctx (r : Tast.expr) =
+  match const_reached r with
+  | Some view when owning ctx.env r.Tast.ty ->
+    let t = Types.to_string r.Tast.ty in
+    let fix =
+      match r.Tast.ty with
+      | (Types.Vec _ | Types.Map _) when not (region_only ctx.env r.Tast.ty) ->
+        Printf.sprintf "(clone v) copies it into a %s of its own" t
+      (* TODO.org, "(clone slice)": once clone copies any value that owns
+         storage, this should say (clone v) too. *)
+      | _ -> Printf.sprintf "(addr v) gives a (Ptr const %s) to read it through" t
+    in
+    Loc.failk "check/const-owned-copy" r.Tast.loc
+      "this copies a %s out of a %s, which can only be read, and the copy \
+       would share its storage with the original. Use it where it stands — \
+       index it, slice it or read its fields — or %s"
+      t (Types.to_string view) fix
+  | _ -> ()
+
+and check_value ctx ?want (e : Ast.expr) : Tast.expr =
   let loc = e.Ast.loc in
   (* Read the permission this form was given and withdraw it in the same
      breath, so that nothing reached from here inherits it. The two callers
@@ -3928,7 +3982,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
      than once — nothing in this milestone builds one — still falls to the
      ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *)
   | Ast.Set (Ast.Pindex (target, [ idx ]), v) ->
-    let target = check ctx target in
+    let target = check_target ctx target in
     if target.Tast.ty = Types.Dyn then
       let i = check ctx ~want:Types.Dyn idx in
       let v = check ctx ~want:Types.Dyn v in
@@ -5010,13 +5064,6 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
             | _ -> ());
            (* Locals are assignable places; parameters are not. *)
            let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
-           (* A Vec or Map header copied out of read-only storage still
-              shares its block with the original, so a push through the copy
-              is a push through the original. The local remembers where it
-              came from, for [refuse_const_change]. *)
-           Option.iter
-             (fun view -> ctx.const_locals <- (slot, view) :: ctx.const_locals)
-             (const_reached ~local:(const_local ctx) v);
            (slot, v))
         bs
     in
@@ -6502,7 +6549,7 @@ and fields_named env n : Tast.structure option =
    pointer to one. The auto-deref is inserted here as a real node, so no
    backend re-derives it. *)
 and struct_target ctx (target : Ast.expr) : Tast.expr * string =
-  let t = check ctx target in
+  let t = check_target ctx target in
   let has n = fields_named ctx.env n <> None in
   match t.Tast.ty with
   | Types.Named n when has n -> t, n
@@ -6573,15 +6620,13 @@ and place_const (p : Tast.place) =
     const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
     || through_string t.Tast.ty (List.length idx)
 
-and const_local ctx slot = List.assoc_opt slot ctx.const_locals
-
-(* Growing, shrinking or freeing a Vec or a Map that is read-only storage, or
-   a copy of one. The backends hand the runtime the container's address, and
-   the header's block is shared with every copy, so this is the 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 refuse_const_change ctx loc (target : Tast.expr) =
-  match const_reached ~local:(const_local ctx) target with
+(* Growing, shrinking or freeing a Vec or a Map that is read-only storage.
+   The backends hand the runtime the container's address, so this is the
+   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 refuse_const_change _ctx loc (target : Tast.expr) =
+  match const_reached target with
   | None -> ()
   | Some view ->
     let t = Types.to_string target.Tast.ty in
@@ -6646,10 +6691,10 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
        Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
          "%s has no field %s" sname name
      | Some i ->
-       if store then Option.iter (refuse_const_place loc) (const_reached target);
+       if store then Option.iter (refuse_const_place ctx.env loc) (const_reached target);
        Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
   | Ast.Pindex (target, idx) ->
-    let target = check ctx target in
+    let target = check_target ctx target in
     (match target.Tast.ty with
      (* The same bounds and epoch check the value form gets, through the same
         helper: an element of a Vec is a place because a Vec element is
@@ -6665,7 +6710,7 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
     let target = check ctx target in
     (match target.Tast.ty with
      | Types.Ptr (Types.Const, _) as view when store ->
-       refuse_const_place loc view
+       refuse_const_place ctx.env loc view
      | Types.Ptr (_, t) -> Tast.Pderef target, t
      | other ->
        fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
@@ -6724,7 +6769,7 @@ and index_expr ctx (e : Ast.expr) =
 and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list) =
   (match place with
    | Some l when store ->
-     Option.iter (refuse_const_place l)
+     Option.iter (refuse_const_place ctx.env l)
        (const_steps (const_reached target) target.Tast.ty (List.length idx))
    | _ -> ());
   let rec go ty = function
@@ -8087,7 +8132,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 2 args;
     (match args with
      | [ target; x ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        refuse_const_change ctx loc target;
        (* A push into a dyn container is a call and nothing else: no allocation
           guard, no restart, no region check. The dyn runtime owns the storage
@@ -8128,7 +8173,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 2 args;
     (match args with
      | [ target; n ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        refuse_const_change ctx loc target;
        let n = check ctx ~want:index_ty n in
        let n64 =
@@ -8172,7 +8217,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      is a thing you write, and writing it twice is yours to not do. *)
   | "free" ->
     arity ctx loc name 1 args;
-    let target = check ctx (List.hd args) in
+    let target = check_target ctx (List.hd args) in
     refuse_const_change ctx loc target;
     (* A container of owning elements is refused here, and a reader will
        assume the opposite — that [free] recurses — so this says why it does
@@ -8227,7 +8272,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (* Checked once, then dispatched on what it turned out to be: checking
           it inside a guard as well would allocate the target's slots twice and
           evaluate whatever it was written as twice. *)
-       let target = check ctx target in
+       let target = check_target ctx target in
        let a = allocator_arg ctx loc rest in
        (match target.Tast.ty with
         (* The refusal that did *not* come down with the type-level ones, and
@@ -8342,7 +8387,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 3 args;
     (match args with
      | [ target; k; v ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        refuse_const_change ctx loc target;
        (* A put into a dyn map is a call and nothing else, the way a push into
           a dyn vec is: the runtime owns the storage, so there is no guard, no
@@ -8393,7 +8438,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        (* A dyn map's absence is nil, not None: the typed map can promise an
           (Option V) because V was written down, and a dyn map has nothing to
           write. nil is an ordinary dyn value the caller compares against —
@@ -8468,7 +8513,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        refuse_const_change ctx loc target;
        let kt, vt = map_kv loc "map-remove" target.Tast.ty in
        let k = check ctx ~want:kt k in
@@ -8506,7 +8551,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 4 args;
     (match args with
      | [ target; cur; k; v ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        let kt, vt = map_kv loc "map-next" target.Tast.ty in
        let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
        let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
@@ -8530,7 +8575,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     arity ctx loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        (* The dyn map's question, one word with the typed one. It exists on
           the dyn side because absence there is nil, and a map can also store
           nil under a key — (get m k) answering nil cannot tell the two
@@ -8849,7 +8894,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
   | "length" ->
     arity ctx loc name 1 args;
     let target = List.hd args in
-    let a = check ctx target in
+    let a = check_target ctx target in
     (match a.Tast.ty with
      | Types.Array _ | Types.Slice _ | Types.String ->
        prim Tast.Len index_ty [ a ]
@@ -8876,7 +8921,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
   | "at" ->
     (match args with
      | target :: idx when idx <> [] ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        (match target.Tast.ty with
         | Types.Vec _ ->
           let p, elem = vec_at ctx loc target idx in
@@ -8923,7 +8968,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          "slice is (slice a), (slice a lo) or (slice a lo hi) — given %d \
           arguments" (List.length args)
      | target :: bounds ->
-       let target = check ctx target in
+       let target = check_target ctx target in
        let ty = target.Tast.ty in
        match ty with
        (* A Vec leaves here: everything below is written around a length the
@@ -10004,8 +10049,19 @@ and generic_call ctx ~want loc name vars pats pret args =
            | Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ -> true
            | _ -> false
          in
+         (* A bare [$t] an earlier argument bound to a slice or a pointer:
+            this argument may differ from it only in const, and the two meet
+            at the read-only one ([Types.const_join]), whichever came first.
+            So it is checked on its own terms rather than against the
+            binding. *)
+         let bound_view =
+           match pat, p with
+           | Types.Var v, (Types.Slice _ | Types.Ptr _)
+             when not (generic_ty p || bound_exactly v) -> Some v
+           | _ -> None
+         in
          let a =
-           if generic_ty p then check ctx a
+           if generic_ty p || bound_view <> None then check ctx a
            else if bound_scalar <> None && not untyped_literal then
              (* On its own terms first. A form that has no type without a want
                 — [(zeroed)] is the one that matters — refuses here and is
@@ -10038,6 +10094,11 @@ and generic_call ctx ~want loc name vars pats pret args =
             bound to i64 is an ordinary mismatch and gets the ordinary
             refusal below. *)
          let handled =
+           match bound_view, Types.const_join p a.Tast.ty with
+           | Some v, Some j ->
+             subst := (v, j) :: List.remove_assoc v !subst;
+             true
+           | _ ->
            match bound_scalar with
            | Some v
              when (not (Types.equal p a.Tast.ty))
@@ -10076,7 +10137,7 @@ and generic_call ctx ~want loc name vars pats pret args =
                   " — %s takes a slice it may write through, and a %s can \
                    only be read%s"
                   name (Types.to_string a.Tast.ty)
-                  (match const_copy e with
+                  (match const_copy ctx.env e with
                    | Some c ->
                      Printf.sprintf ". %s copies v into one that can be written" c
                    | None -> "")
@@ -10126,6 +10187,8 @@ and generic_call ctx ~want loc name vars pats pret args =
                    && Types.is_numeric a.Tast.ty
                    && Types.widens_to ~from:a.Tast.ty ~into:f ->
               widen a.Tast.loc f a
+            | Some f when Types.const_widens ~from:a.Tast.ty ~into:f ->
+              { a with Tast.ty = f }
             | _ -> a)
          (* And the other widening, for the same reason and at the same
             moment: a [CFn] argument against an [(Fn [$t] $t)] parameter.
@@ -10436,7 +10499,7 @@ and trial ctx f =
      resource failure into a wrong answer. *)
   let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
                        defers; defer_slot; defer_ok; defer_block; outer = _;
-                       outer_what; caught; const_locals; envslot; parent = _;
+                       outer_what; caught; place_ok; envslot; parent = _;
                        in_frames; loops; tail; in_defer;
                        owner = _ } = ctx in
   match f () with
@@ -10447,7 +10510,7 @@ and trial ctx f =
     ctx.defers <- defers; ctx.defer_slot <- defer_slot;
     ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
     ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
-    ctx.caught <- caught; ctx.const_locals <- const_locals; ctx.envslot <- envslot;
+    ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot;
     ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
     Error d
 
diff --git a/lib/types.ml b/lib/types.ml
index eefb0bbf..d2dff244 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -349,20 +349,21 @@ let rec const_widens ~(from : t) ~(into : t) =
     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. *)
-(* The one type two branches of an [if] meet at when they differ only in
-   const: the read-only one, whichever branch it came from. *)
+(* The one type two branches of an [if], or two arguments at one type
+   variable, meet at when they differ only in const: the read-only one,
+   whichever came first. *)
 let const_join a b =
   if equal a b then Some a
   else if const_widens ~from:a ~into:b then Some b
   else if const_widens ~from:b ~into:a then Some a
   else None
 
+(* 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'
diff --git a/test/programs/const-owned.flan b/test/programs/const-owned.flan
new file mode 100644
index 00000000..60f2d142
--- /dev/null
+++ b/test/programs/const-owned.flan
@@ -0,0 +1,39 @@
+;;;; A Vec reached through a [const (Vec T)] or a (Ptr const (Vec T)) is used
+;;;; where it stands — indexed, measured, sliced, its address taken — and never
+;;;; copied out as a value; (clone v) is the copy. The refusals are in
+;;;; test_flan.ml; this is the half that compiles, on both backends.
+
+(defstruct Bag [items (Vec i32)  n i32])
+
+(defn total [vs [const (Vec i32)]] i32
+  (let [t 0]
+    (dotimes [i (length vs)]
+      (dotimes [j (length (at vs i))]
+        (set t (+ t (at (at vs i) j)))))
+    t))
+
+(defn first-len [p (Ptr const (Vec i32))] i32 (length (deref p)))
+
+(defn bag-n [bs [const Bag]] i32 (+ (.n (at bs 0)) (length (.items (at bs 0)))))
+
+(defn pick [c bool  a $t  b $t] $t (if c a b))
+
+(defn main [] i32
+  (let [a (vec-new i32)
+        b (vec-new i32)]
+    (push a 1) (push a 2)
+    (push b 30)
+    (let [vs [a b]
+          cv (the-const (slice vs))
+          w (clone (at cv 0))
+          bags [(Bag {.items b .n 4})]]
+      (push w 99)
+      ;; The shallow rule: the Vec's own buffer is writable through the view.
+      (set (at (at cv 1) 0) 31)
+      (println (total cv) (length w) (length (at cv 0)))
+      (println (first-len (addr (at cv 0))) (bag-n (slice bags)))
+      (println (length (pick true (bytes-view "abc") (bytes "de")))
+               (length (pick false (bytes "de") (bytes-view "abc"))))))
+  0)
+
+(defn the-const [s [const (Vec i32)]] [const (Vec i32)] s)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 6aa6fc54..47b9cdda 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -879,6 +879,12 @@ let () =
       const_slice_out;
     outputs ~x86:true "const slices, --x86" "programs/const-slice.flan"
       const_slice_out;
+    let const_owned_out = "34 3 2\n2 5\n3 3\n" in
+    outputs "const owned" "programs/const-owned.flan" const_owned_out;
+    outputs ~opt:"-O0" "const owned, -O0" "programs/const-owned.flan"
+      const_owned_out;
+    outputs ~x86:true "const owned, --x86" "programs/const-owned.flan"
+      const_owned_out;
     (* (string b). The conversion emits nothing — String and Slice _ are the
        same %slice — so the rows are about length and ownership rather than
        arithmetic: a number round-tripped, an empty slice, sub-views whose
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 3624a82b..a0c8c6ca 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2361,21 +2361,81 @@ let () =
     "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
   accepts "vec-new reads (Ptr const u8) as a type"
     "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
-  (* A Vec header copied out of read-only storage shares its block, so the
-     copy is as read-only as the original, through any number of lets. *)
-  rejects_check "push through a let-bound copy of a const element"
-    "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))"
-    ~needle:"reached through a [const (Vec i32)]";
-  rejects_check "reserve through a copy of a copy"
-    "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))"
-    ~needle:"reached through a [const (Vec i32)]";
-  rejects_check "put through a let-bound copy of a const element"
-    "(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))"
-    ~needle:"reached through a [const (Map string i32)]";
-  rejects_check "push into a field of a let-bound copy"
-    "(defstruct P [v (Vec i32)]) \
-     (defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))"
-    ~needle:"take the P it lives in as a [P]";
+  (* Decision 81: a value that owns storage, reached through read-only
+     storage, is used where it stands and never copied out. Every route a
+     copy could take is refused at the copy. *)
+  let copied = "this copies a (Vec i32) out of a [const (Vec i32)]" in
+  List.iter
+    (fun (name, src) -> rejects_check ("no copy out: " ^ name) src ~needle:copied)
+    [ "let", "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))";
+      "loop binding",
+      "(defn f [cs [const (Vec i32)]] () (loop [v (at cs 0)] (push v 1)))";
+      "if value",
+      "(defn f [c bool  cs [const (Vec i32)]] () \
+       (let [v (if c (at cs 0) (at cs 1))] (push v 1)))";
+      "do value",
+      "(defn f [cs [const (Vec i32)]] () (let [v (do (at cs 0))] (push v 1)))";
+      "set into a local",
+      "(defn f [cs [const (Vec i32)]] () \
+       (let [v (vec-new i32)] (set v (at cs 0)) (push v 1)))";
+      "match binding",
+      "(defn f [cs [const (Vec i32)]] i32 \
+       (match (Some (at cs 0)) (Some v) (do (push v 1) 0) None 0))";
+      "array destructure",
+      "(defn f [cs [const (Vec i32)]] () \
+       (let [[a b] [(at cs 0) (at cs 1)]] (push a 1)))";
+      "closure capture",
+      "(defn app [g (Fn [] ())] () (g)) (defn f [cs [const (Vec i32)]] () \
+       (let [v (at cs 0)] (app (fn [] (push v 1)))))";
+      "passed by value",
+      "(defn pusher [v (Vec i32)] () (push v 1)) \
+       (defn f [cs [const (Vec i32)]] () (pusher (at cs 0)))";
+      "returned by value",
+      "(defn g [cs [const (Vec i32)]] (Vec i32) (at cs 0))";
+      "through a generic",
+      "(defn id [x $t] $t x) (defn f [cs [const (Vec i32)]] () (push (id (at cs 0)) 1))" ];
+  rejects_check "no copy out through a const pointer"
+    "(defn f [p (Ptr const (Vec i32))] () (let [v (deref p)] (push v 1)))"
+    ~needle:"this copies a (Vec i32) out of a (Ptr const (Vec i32))";
+  rejects_check "and the copy that is allowed is named"
+    "(defn f [cs [const (Vec i32)]] (Vec i32) (at cs 0))"
+    ~needle:"(clone v) copies it into a (Vec i32) of its own";
+  rejects_check "a struct holding a Vec is not copied out either"
+    "(defstruct P [v (Vec i32)]) (defn f [cs [const P]] P (at cs 0))"
+    ~needle:"(addr v) gives a (Ptr const P) to read it through";
+  rejects_check "nor an array of them"
+    "(defn f [cs [const [2 (Vec i32)]]] [2 (Vec i32)] (at cs 0))"
+    ~needle:"this copies a [2 (Vec i32)] out of a [const [2 (Vec i32)]]";
+  rejects_check "nor an Option of one"
+    "(defn f [cs [const (Option (Vec i32))]] (Option (Vec i32)) (at cs 0))"
+    ~needle:"this copies a (Option (Vec i32)) out";
+  rejects_check "nor a field that owns storage"
+    "(defstruct P [v (Vec i32)]) (defn f [cs [const P]] (Vec i32) (.v (at cs 0)))"
+    ~needle:"this copies a (Vec i32) out of a [const P]";
+  accepts "used where it stands"
+    "(defstruct P [v (Vec i32)  n i32]) \
+     (defn f [cs [const (Vec i32)]  ps [const P]  p (Ptr const (Vec i32))] i32 \
+       (+ (at (at cs 0) 1) (length (at cs 0)) (length (slice (at cs 0))) \
+          (.n (at ps 0)) (length (.v (at ps 0))) (length (deref p)) \
+          (length (deref (addr (at cs 0)))) (length (clone (at cs 0)))))";
+  accepts "a copy of a scalar element is still a copy"
+    "(defn f [cs [const i32]] i32 (let [x (at cs 0)] (set x 5) x))";
+  (* The header copy is suggested only for elements that own nothing. *)
+  rejects_check "no header copy suggested for an array of Vecs"
+    "(defn f [cs [const [2 (Vec i32)]]] () (set (at cs 0) (at cs 1)))"
+    ~needle:"take it as a [[2 (Vec i32)]] instead";
+  rejects_check "nor for an Option of a Vec"
+    "(defn f [cs [const (Option (Vec i32))]] () (set (at cs 0) None))"
+    ~needle:"take it as a [(Option (Vec i32))] instead";
+  (* Two arguments at one type variable meet at const, either order. *)
+  accepts "a generic's arguments join at const"
+    "(defn pick [c bool  a $t  b $t] $t (if c a b)) \
+     (defn f [c bool  cs [const u8]  ms [u8]] i32 (+ (length (pick c ms cs)) \
+       (length (pick c cs ms))))";
+  rejects_check "and the join is read-only"
+    "(defn pick [c bool  a $t  b $t] $t (if c a b)) \
+     (defn f [c bool  cs [const u8]  ms [u8]] () (set (at (pick c ms cs) 0) 1))"
+    ~needle:"this writes through a [const u8]";
   rejects_check "no copy of Vec headers is suggested"
     "(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
     ~needle:"take it as a [(Vec i32)] instead";