diff --git a/FIX.org b/FIX.org
index efd0249..c3d4e47 100644
--- a/FIX.org
+++ b/FIX.org
@@ -4782,14 +4782,44 @@ the target, nothing computed that was not computed before. The Vec had no
 two-argument spelling only because the name it had was not the name that grew
 the arities.
 
-*A Vec a call returned is refused, at every arity*, and for a different reason
-than the array. [(slice (mk))] over an array dangles: the view outlives a
-temporary the frame reuses. [(slice (make-vec))] does not dangle — the storage
-a returned Vec owns lives until its allocator's free-all or destroy. What is
-lost is the *owner*: the header is a temporary, so nothing can ever free that
-block, and the program has written a leak it cannot spell the fix for. The
-refusal says that rather than borrowing the array's sentence, and names the
-[let] that keeps the owner.
+*A Vec a call returned is accepted*, where an array a call returned is
+refused. This lane first refused it, the review pushed back, and the author
+ruled:
+
+#+begin_quote
+we're purposely doing manual memory management for the static side, so whatever
+#+end_quote
+
+[(slice (mk))] over an array dangles: the view outlives a temporary the frame
+reuses, and the dangle is the whole reason that refusal exists.
+[(slice (make-vec))] does not dangle — the storage a returned Vec owns lives
+until its allocator's free-all or destroy, so the view reads what it says it
+reads. What a returned Vec loses is the *owner*, and losing an owner is a
+leak, which this language has already ruled is defined behaviour:
+spec-memory.md on overwriting a global Vec says it "overwrites the first block
+and leaks it; there is no drop", and programs/strings.flan says "leaking is
+defined behaviour" out loud.
+
+So the refusal singled out one of three operations that lose the same owner.
+[(len (mk))] and [(at (mk) 0)] compile and leak the identical block, and
+refusing only the third would have been a rule about a spelling rather than
+about a hazard. It also broke code [as-slice] accepted, including the case
+where there is nothing to leak at all:
+[(with-allocator context/temp (println (len (slice (mk)))))] — the arena takes
+the block back whatever anyone does with the header. Dropped, and check.ml
+says why beside the array refusal it sits next to, so that the asymmetry reads
+as deliberate rather than as an oversight.
+
+*The array refusal stays, and the line between the two is the point.* They
+look alike and they are not. A view into a returned array points at bytes the
+frame has already handed to something else, so it answers a number that was
+never in the array — a wrong answer, silently, on both backends, with nothing
+to trap on. A view into a returned Vec answers exactly the elements it says it
+does; the cost is a block nobody can free. Wrong answers are the compiler's
+business and leaks are the program's, which is the whole of why one refusal is
+kept and the other is gone. BUILT.md and spec-memory.md both say it, because a
+reader meeting one of the two forms will assume the other behaves the same
+way.
 
 The refusal for the name itself is in [ordinary_call], after every table, so a
 program that defines an [as-slice] of its own still reaches its own. It reads
@@ -4840,6 +4870,39 @@ first one is sufficient on its own.
 What was built instead is the sentence, in the two places a reader meets the
 operation that breaks the view.
 
+The independent review sharpened the argument and reached the same place. The
+reserve witness kills the cheap per-push flag. The refined version — flag a
+push only when no reserve on *that* Vec came between — has to know which Vec a
+view was taken from and what happened to it in between, across calls and
+control flow, which is the static flow tracking repealed on 2026-09-18.
+Witness kills the cheap check; repeal kills the sound one.
+
+** Two forks closed on review, and one refusal dropped
+Found by the independent review of this branch and fixed here.
+
+*The -1 sentinel was reachable from user syntax.* [(slice v 0 -1)] answered
+the whole Vec and [(slice v 1 -1)] the tail, on both backends, while
+[(slice a 0 -1)] over an array was refused as a negative bound — the same
+builtin giving the same literal opposite meanings. The refusal now runs on the
+bounds the reader *wrote*, before the implicit hi is built, which is the only
+order that works: the sentinel is itself a -1, so a check on the finished pair
+would refuse [(slice v)] itself. [(slice v -1)] is a compile error now, in the
+same words an array gets. The backwards-pair check moved into the branch where
+both ends are bounds somebody wrote, so it no longer has to step around a
+value nobody wrote.
+
+*The bounds fork is closed toward [index_expr].* The array path expected an
+i32 outright and the Vec path used [index_expr], so with a u32 in hand
+[(slice v c)] compiled and [(slice a c)] did not. The tiebreaker is not which
+half is older but what every other subscript in the language does: [indexed]
+and [vec_at] both take their index through [index_expr], so [(at a c)]
+compiled where [(slice a c)] did not — the fork was between [slice] and [at]
+as much as between two targets. A bound is a subscript; it takes the subscript
+rule. Nothing is loosened that the bounds check does not still catch, and i64
+and u64 are still refused by name on both paths.
+
+*The returned-Vec refusal is dropped*, as above.
+
 ** Swept
 Every spelling in the repo: lib/ (check.ml, prelude.ml, render.ml, shim.ml),
 runtime/flan_rt.c comments, test/ (test_flan.ml, test_acceptance.ml,
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 283d7c5..3c7a469 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -2441,6 +2441,14 @@ memory; writing through it writes to memory the program no longer owns. **The co
 not tell you.** That is `spec-memory.md`'s explicit Zig/Odin contract, chosen instead of a borrow checker, and it is
 one rule: take the view again after the `push`.
 
+One thing it is *not*: a dangle. `(slice (make-vec))` is legal, and the view it answers reads what it says it reads —
+the storage a returned `Vec` owns outlives the expression. What does not survive is the header, which was a
+temporary, and it was the only handle `free` could have taken, so that block is leaked unless the allocator reclaims
+it wholesale at `free-all` or destroy. That is the same leak `(len (mk))` and `(at (mk) 0)` already write, and the
+same one `spec-memory.md` names when a global `Vec` is overwritten: manual memory management, and the program's
+business. `(slice (mk))` over a fixed **array** is refused, and the difference is worth being exact about — that one
+is a view into a frame that is gone, so it answers whatever the frame was reused for. A wrong answer is not a leak.
+
 It is stated here, beside `push`, rather than at `slice`, because the `slice` is not the moment anything goes wrong —
 the `push` is. There used to be a second name, `as-slice`, for taking a view of a `Vec`, on the theory that a
 different word at that call site was the warning. It was not one. The value handed to `slice` already decides what
diff --git a/lib/check.ml b/lib/check.ml
index fb5acd0..a104795 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -6025,42 +6025,54 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
 
    No slot and no length read at any arity: -1 is the runtime's "to the end",
    so the short forms pass a constant where an array passes its length, and
-   the target appears exactly once in all three. *)
+   the target appears exactly once in all three.
+
+   A Vec a *call* returned is accepted, where an array a call returned is
+   refused a screen down. The array is a dangle — the view outlives a
+   temporary the frame reuses — and this is not: the storage a returned Vec
+   owns lives to its allocator's free-all or destroy, so the view reads what
+   it says it reads. What a returned Vec loses is the owner, and losing the
+   owner is a leak, which this language has already decided is defined
+   behaviour (spec-memory.md on overwriting a global Vec: "overwrites the
+   first block and leaks it; there is no drop"). [(len (mk))] and
+   [(at (mk) 0)] lose exactly the same owner and are accepted; refusing the
+   third of those three would be a rule about one spelling rather than about
+   a hazard, and under a region allocator there is nothing to leak at all. *)
 and vec_slice ctx ~want loc (target : Tast.expr) elem (bounds : Ast.expr list) =
-  (* The mirror of the array rule one screen down, for a different reason. An
-     array a call returned is storage the frame reuses, so the view dangles;
-     a Vec a call returned owns storage that outlives the expression, and what
-     is lost is the owner — the header is a temporary, so nothing can ever
-     [free] it and the block lives to the allocator's free-all or destroy. A
-     [let] keeps the owner, so that is what the refusal names. *)
-  (match target.Tast.e with
-   | Tast.Call _ | Tast.CallPtr _ ->
-     fail loc
-       "this slices a Vec a call returned, and the header a call answers is a \
-        temporary — the view outlives it, and the storage it names can no \
-        longer be freed, because there is no Vec left to free it through. \
-        Bind it first: (let [v (…)] (slice v …))"
-   | _ -> ());
   let int k = mk loc index_ty (Tast.Int (k, Types.I32)) in
-  (* -1 is "to the end". A Vec's length is not static, so unlike an array
-     there is no constant to fold and the runtime reads the length word it is
-     carrying anyway. *)
+  (* Every bound the reader wrote goes through here, and the -1 below does
+     not: a negative literal is refused exactly as it is on an array, in the
+     same words, and that refusal has to happen on the bounds a person wrote
+     rather than on the pair that comes out of this — the sentinel *is* a -1,
+     and checking afterwards would refuse (slice v) itself. There is no static
+     length to check the other direction against. *)
+  let bound (b : Ast.expr) =
+    let v = index_expr ctx b in
+    (match literal v with
+     | Some k ->
+       static_index b.Ast.loc (Types.Vec elem) ~past_end:true "slice bound" k
+     | None -> ());
+    v
+  in
+  (* -1 is the runtime's "to the end". A Vec's length is not static, so unlike
+     an array there is no constant to fold and the runtime reads the length
+     word the header is carrying anyway. *)
   let to_end () = int (-1L) in
   let lo, hi =
     match bounds with
     | [] -> int 0L, to_end ()
-    | [ lo ] -> index_expr ctx lo, to_end ()
-    | [ lo; hi ] -> index_expr ctx lo, index_expr ctx hi
+    | [ lo ] -> bound lo, to_end ()
+    | [ lo; hi ] ->
+      let lo = bound lo and hi = bound hi in
+      (* The same refusal the other targets get, and it is asked only here,
+         where both ends are bounds somebody wrote. *)
+      (match literal lo, literal hi with
+       | Some a, Some b when a > b ->
+         fail loc "slice [%Ld %Ld) runs backwards — lo must not exceed hi" a b
+       | _ -> ());
+      lo, hi
     | _ -> assert false
   in
-  (* The same refusal the other targets get. There is no static length to
-     check a single bound against, but a literal pair that runs backwards is
-     wrong without one — and [hi] here may be the -1 sentinel, which is not a
-     bound anybody wrote. *)
-  (match literal lo, literal hi with
-   | Some a, Some b when b >= 0L && a > b ->
-     fail loc "slice [%Ld %Ld) runs backwards — lo must not exceed hi" a b
-   | _ -> ());
   let out = fresh_slot ctx (Types.Slice elem) in
   let fill =
     rt loc Types.Unit "flan_vec_as_slice"
@@ -7578,14 +7590,22 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          | Types.Array (n, _) -> int n
          | _ -> mk loc index_ty (Tast.Prim (Tast.Len, [ src () ]))
        in
+       (* [index_expr] and not an [i32] expectation, which is what this used
+          to be. One builtin cannot answer two ways about the same bound, and
+          the question is settled by what every *other* subscript in the
+          language already does: [indexed] and [vec_at] both take their index
+          through here, so [(at a c)] over a [u32] compiles and [(slice a c)]
+          used to not. A bound is a subscript; it takes the subscript rule.
+          Nothing is loosened by it that a bounds check does not still catch —
+          [index_expr] admits an integer narrower than 32 bits and a u32,
+          whose out-of-range values truncate to a negative i32 the unsigned
+          comparison rejects, and refuses i64 and u64 by name. *)
        let lo_loc, lo, hi_loc, hi =
          match bounds with
          | [] -> loc, int 0L, loc, whole_len ()
-         | [ lo ] ->
-           lo.Ast.loc, check ctx ~want:index_ty lo, loc, whole_len ()
+         | [ lo ] -> lo.Ast.loc, index_expr ctx lo, loc, whole_len ()
          | [ lo; hi ] ->
-           lo.Ast.loc, check ctx ~want:index_ty lo,
-           hi.Ast.loc, check ctx ~want:index_ty hi
+           lo.Ast.loc, index_expr ctx lo, hi.Ast.loc, index_expr ctx hi
          | _ -> assert false
        in
        (* A bound may sit one past the end, so the length is checked against
diff --git a/spec-memory.md b/spec-memory.md
index 9ced367..358ad33 100644
--- a/spec-memory.md
+++ b/spec-memory.md
@@ -107,6 +107,11 @@ region" for the rule that stands in its place and for what it costs.
   and a view holds the old address and the old length. This is the whole of the
   contract: the view goes stale at the `push`, not at the `slice`, and it is
   the program's business to take the view again afterwards.
+- A view of a `Vec` a call returned is legal and does not dangle — the storage
+  outlives the expression — but the header was the only handle `free` could
+  have taken, so that block is leaked unless its allocator reclaims it
+  wholesale. Same leak as `(len (mk))`, same rule as overwriting a global
+  `Vec`: manual memory management, and the program's business.
 - **The first implementation follows Zig/Odin's explicit model, not Rust's
   borrow checker.** Dev builds carry a generation word on `Vec` and trap on use
   of a stale slice. `Ptr` is the explicit lower-level escape hatch and has the
diff --git a/test/programs/algorithms.flan b/test/programs/algorithms.flan
index d86f288..3135821 100644
--- a/test/programs/algorithms.flan
+++ b/test/programs/algorithms.flan
@@ -107,14 +107,14 @@
   ;; which an in-place byte sort could not, since a literal lives in .rodata.
   (let [f (split (bytes-view "pear,apple,Fig,apple,banana") \,)]
     (sort-bytes (slice f))
-    (show-fields (slice f))          ; Fig apple apple banana pear
+    (show-fields (slice f))             ; Fig apple apple banana pear
     (free f))
 
   ;; And the round trip the whole second tier is for: split, sort, join.
   (let [f (split (bytes-view "delta,alpha,charlie,bravo") \,)]
     (sort-bytes (slice f))
     (let [j (join (slice f) (bytes-view " < "))]
-      (println (string (slice j)))   ; alpha < bravo < charlie < delta
+      (println (string (slice j)))      ; alpha < bravo < charlie < delta
       (free j))
     (free f))
   0)
diff --git a/test/programs/format.flan b/test/programs/format.flan
index dfec99b..c042c9a 100644
--- a/test/programs/format.flan
+++ b/test/programs/format.flan
@@ -95,6 +95,6 @@
     (let [f (format-f64 0.0166667 4)]
       (append (addr b) (slice f))
       (free f))
-    (println (string (slice b)))     ; fps 59.9 / frame 0.0167
+    (println (string (slice b)))        ; fps 59.9 / frame 0.0167
     (free b))
   0)
diff --git a/test/programs/into.flan b/test/programs/into.flan
index 34aad46..136fbde 100644
--- a/test/programs/into.flan
+++ b/test/programs/into.flan
@@ -46,20 +46,20 @@
   ;; No transforms: a copy into the destination named in the form.
   (let [xs [7 8 9]
         v (into xs (vec-new i32))]
-    (show (slice v))                          ; 7 8 9
+    (show (slice v))                             ; 7 8 9
     (free v))
 
   ;; map then filter.
   (let [xs [1 2 3 4 5 6]
         v (into xs (vec-new i32) (map double) (filter even?))]
-    (show (slice v))                          ; 2 4 6 8 10 12
+    (show (slice v))                             ; 2 4 6 8 10 12
     (free v))
 
   ;; filter then map, over the same source: a different answer, because the
   ;; stages are in the order they were written.
   (let [xs [1 2 3 4 5 6]
         v (into xs (vec-new i32) (filter even?) (map double))]
-    (show (slice v))                          ; 4 8 12
+    (show (slice v))                             ; 4 8 12
     (free v))
 
   ;; One pass and no intermediate collection. The two chains above pulled
@@ -69,8 +69,8 @@
   ;; A name as the source is read, not moved: src is still alive here.
   (let [src (into [3 1 2] (vec-new i32))
         v (into src (vec-new i32) (map double))]
-    (show (slice v))                          ; 6 2 4
-    (show (slice src))                        ; 3 1 2
+    (show (slice v))                             ; 6 2 4
+    (show (slice src))                           ; 3 1 2
     (free v)
     (free src))
 
@@ -88,7 +88,7 @@
   ;; elements come out of it.
   (let [xs [1 2 3 4]
         v (into (source (slice xs 0 4)) (vec-new i32) (filter even?))]
-    (show (slice v))                          ; 2 4
+    (show (slice v))                             ; 2 4
     (free v))
   (print builds) (println "")                    ; 1
   0)
diff --git a/test/programs/slurp.flan b/test/programs/slurp.flan
index f07f1e2..7aa4022 100644
--- a/test/programs/slurp.flan
+++ b/test/programs/slurp.flan
@@ -29,7 +29,7 @@
   ;; ── The happy path ────────────────────────────────────────────────
   (let [v (slurp "programs/assets/a.txt")]
     (println (len v))                   ; 13
-    (print (string (slice v)))       ; hello from a
+    (print (string (slice v)))          ; hello from a
     (free v))
 
   ;; Byte-exact, the same as an embed: nothing here decodes anything.
@@ -52,7 +52,7 @@
        (invoke-restart 'use-value "programs/assets/b.bin"))]
     (let [v (slurp "programs/assets/does-not-exist")]
       (println (len v))                 ; 3
-      (println (string (slice v)))   ; BBB
+      (println (string (slice v)))      ; BBB
       (free v)))
   (println seen)                        ; 1
   (println (= last-reason file-missing)) ; true
@@ -65,7 +65,7 @@
   (barf "slurp-out.txt" (bytes-view "round trip\n"))
   (let [v (slurp "slurp-out.txt")]
     (println (len v))                   ; 11
-    (print (string (slice v)))       ; round trip
+    (print (string (slice v)))          ; round trip
     (free v))
 
   ;; barf's own failure signals the same condition with op = write. A directory
@@ -80,7 +80,7 @@
   (println seen)                        ; 1
   (println (= last-op file-op-write))   ; true
   (let [v (slurp "slurp-out.txt")]
-    (print (string (slice v)))       ; second
+    (print (string (slice v)))          ; second
     (free v))
 
   ;; ── retry: the file was not there, so the handler makes it ────────
@@ -96,7 +96,7 @@
        (barf "slurp-made.txt" (bytes-view "made by the handler\n"))
        (invoke-restart 'retry))]
     (let [v (slurp "slurp-made.txt")]
-      (print (string (slice v)))     ; made by the handler
+      (print (string (slice v)))        ; made by the handler
       (free v)))
   (println seen)                        ; 1
   (println (= last-reason file-missing)) ; true
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 56bbc35..2aa15d3 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1350,6 +1350,11 @@ let () =
     outputs "vec" "programs/vec.flan" vec_out;
     outputs ~opt:"-O0" "vec, -O0" "programs/vec.flan" vec_out;
     outputs ~dev:true "vec, dev" "programs/vec.flan" vec_out;
+    (* The x86 row, added when [slice] took the Vec over: the three arities
+       are one checker path and the runtime call underneath is the one
+       [as-slice] made, so agreement is by construction — and a row that says
+       so is what turns "by construction" into something CI knows. *)
+    outputs ~x86:true "vec, --x86" "programs/vec.flan" vec_out;
     (* The prelude's second tier: the functions that return new storage, every
        one of which the prelude used to refuse by name for want of an
        allocator. The cases are the ones that separate a correct version from a
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5fbf903..949f098 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1978,16 +1978,26 @@ let () =
     ~needle:"runs backwards";
   rejects_check "slice of a Vec of four"
     (vec ^ "[i32] (slice v 0 1 2))") ~needle:"given 4 arguments";
-  (* The mirror of the returned-array refusal, for a different loss. The
-     storage a returned Vec owns outlives the expression, so the view does not
-     dangle — what is gone is the owner, and with it any way to free the
-     block. *)
-  rejects_check "slice of a returned Vec"
-    "(defn mk [] (Vec i32) (vec-new i32)) (defn f [] [i32] (slice (mk)))"
-    ~needle:"the header a call answers is a temporary";
-  rejects_check "slice of a returned Vec, three arguments"
-    "(defn mk [] (Vec i32) (vec-new i32)) (defn f [] [i32] (slice (mk) 0 1))"
-    ~needle:"the header a call answers is a temporary";
+  (* A negative bound reads the same on a Vec as on an array, and it has to be
+     asked of what the reader wrote: the implicit hi the short forms pass *is*
+     a -1, so a check on the finished pair would refuse (slice v) itself. The
+     one-argument form is the case that proves it runs in the right place. *)
+  rejects_check "negative Vec tail"   (vec ^ "[i32] (slice v -1))")
+    ~needle:"is negative";
+  rejects_check "negative Vec lo"     (vec ^ "[i32] (slice v -1 2))")
+    ~needle:"is negative";
+  rejects_check "the sentinel is not a bound anybody may write"
+    (vec ^ "[i32] (slice v 0 -1))") ~needle:"is negative";
+  (* A Vec a call returned is *accepted*, where an array a call returned is
+     not. The array dangles; this does not — the storage outlives the
+     expression — and what it loses is the owner, which is a leak, which is
+     defined behaviour here. (len (mk)) and (at (mk) 0) lose the same owner
+     and compile, so refusing only the third would be a rule about a spelling
+     rather than about a hazard. *)
+  accepts "slice of a returned Vec"
+    "(defn mk [] (Vec i32) (vec-new i32)) (defn f [] [i32] (slice (mk)))";
+  accepts "slice of a returned Vec, three arguments"
+    "(defn mk [] (Vec i32) (vec-new i32)) (defn f [] [i32] (slice (mk) 0 1))";
   (* There is no [as-slice]: one word takes the view and what it is given says
      what the view is. The refusal names [slice] and writes the call back out,
      because a reader meeting it has no reason to know there was ever a second
@@ -2017,6 +2027,20 @@ let () =
     ~needle:"a returned array is a temporary";
   accepts "slice of an array literal"
     "(defn f [] [i32] (slice [7 8 9]))";
+  (* One builtin, one answer about a bound. A slice bound is a subscript and
+     goes through [index_expr] like every other one, so a u32 is admitted on
+     an array exactly as it always was on a Vec, and an i64 is refused by name
+     on both. The array path used to expect an i32 outright, which made
+     (at a c) compile and (slice a c) not. *)
+  accepts "a u32 bound over an array"
+    (arr ^ "(defn f [c u32] [i32] (slice a c))");
+  accepts "a u32 bound over a Vec"
+    "(defn f [v (Vec i32) c u32] [i32] (slice v c))";
+  rejects_check "an i64 bound over an array"
+    (arr ^ "(defn f [c i64] [i32] (slice a c))") ~needle:"an index is an i32";
+  rejects_check "an i64 bound over a Vec"
+    "(defn f [v (Vec i32) c i64] [i32] (slice v c))"
+    ~needle:"an index is an i32";
 
   (* A string indexes and slices, and neither is a place: it is a view of
      bytes the program does not own — a literal's are in constant storage —