diff --git a/src/cache/file_cache.zig b/src/cache/file_cache.zig
index 449bca0..399a3a8 100644
--- a/src/cache/file_cache.zig
+++ b/src/cache/file_cache.zig
@@ -83,6 +83,15 @@ pub const FileCache = struct {
         return z.fixedArrayLen(node) catch null;
     }
 
+    /// Comptime-known non-negative value of `node`, or null when not
+    /// comptime-resolvable / engine unavailable.  A comptime index can't cause a
+    /// runtime underflow/OOB (it would be a compile error), so a non-null result
+    /// means the access is comptime-verified safe.
+    pub fn comptimeIntValueOf(self: *FileCache, node: std.zig.Ast.Node.Index) ?u64 {
+        const z = self.zls orelse return null;
+        return z.comptimeIntValue(node) catch null;
+    }
+
     /// For a type-name reference node `T`: whether `T` denotes a pointer/
     /// optional type (true), a value type (false), or couldn't resolve (null).
     /// Null when the type engine is unavailable.
@@ -98,6 +107,14 @@ pub const FileCache = struct {
         return z.intInfo(node) catch null;
     }
 
+    /// Whether `node`'s type resolves to a floating-point type.  False when the
+    /// type engine is unavailable or the type isn't a float.  Floats are not
+    /// containers, so `typeNameOfNode` can't report them — use this instead.
+    pub fn isFloatType(self: *FileCache, node: std.zig.Ast.Node.Index) bool {
+        const z = self.zls orelse return false;
+        return z.isFloatType(node) catch false;
+    }
+
     /// For `x.ptr` (x a slice): whether x's element is byte-sized (align 1) —
     /// true=byte slice, false=wider element, null=unresolved/unknown.  Null
     /// when the type engine is unavailable.
diff --git a/src/flow/cfg.zig b/src/flow/cfg.zig
index 69c1e85..fcea727 100644
--- a/src/flow/cfg.zig
+++ b/src/flow/cfg.zig
@@ -15,9 +15,14 @@
 //!   - `return EXPR;` (function exit)
 //!   - `if/else`, `while`, `for`, `switch` branching (real CFG edges)
 //!   - `defer` / `errdefer` (replayed at function-exit / return sites)
+//!   - `try` / `catch` (error-exit sinks + catch-arm forks; errdefers
+//!     replayed on error returns, including `return error.X` and
+//!     `return <error-capture>` from `catch |err|` / `else |err|`)
 //!
 //! What we DON'T model (yet):
-//!   - `try` / `catch` (error-path forking + error-set tracking)
+//!   - error-UNION returns (`return foo()` yielding `!T`): the success
+//!     vs error path isn't forked, so errdefers are not replayed there
+//!     (sound: a residual false-negative, never a false-positive)
 //!   - generics / comptime
 //!   - for-loop iteration variable origin (treated as .plain)
 //!   - switch-case pattern bindings (treated as .plain)
@@ -328,6 +333,12 @@ pub const LocalInfo = struct {
     /// treated as a borrow source.  Set at registerLocalFull from
     /// the same classifier that produces the .decl's init_kind.
     init_hint: InitHint = .other,
+    /// True iff this local is the error-value capture of a `catch |err|`
+    /// or `else |err|` arm.  Such a value is *definitely* an error, so a
+    /// `return <this>` fires errdefers (Zig only runs errdefers on error
+    /// returns).  Lets lowerReturn replay errdefers at `return err`,
+    /// closing the errdefer-double-free-on-error-return false negative.
+    is_error_capture: bool = false,
     /// If this local was declared from a bare identifier that names
     /// a fn in our annotation DB, the name of that fn.  Lets call
     /// sites `local(args)` resolve through the binding to the
diff --git a/src/flow/cfg_builder.zig b/src/flow/cfg_builder.zig
index 9eaf6ce..94931c6 100644
--- a/src/flow/cfg_builder.zig
+++ b/src/flow/cfg_builder.zig
@@ -666,7 +666,14 @@ const Builder = struct {
     /// the body now resolve via name_to_local rather than falling
     /// through to .unknown identifier classification.
     fn registerCaptures(self: *Builder, payload_token: Ast.TokenIndex) !void {
-        _ = try self.registerCapturesWith(payload_token, null);
+        _ = try self.registerCapturesImpl(payload_token, null, false);
+    }
+
+    /// Error-capture variant of `registerCaptures`: each registered
+    /// capture is marked `is_error_capture` so `return <cap>` is treated
+    /// as an error return.  Used for `catch |err|`.
+    fn registerErrorCaptures(self: *Builder, payload_token: Ast.TokenIndex) !void {
+        _ = try self.registerCapturesImpl(payload_token, null, true);
     }
 
     /// Heuristic: when an `if (<Type>.fromJS(...))` scrutinee
@@ -792,6 +799,19 @@ const Builder = struct {
     }
 
     fn registerCapturesWith(self: *Builder, payload_token: Ast.TokenIndex, reset_into: ?BlockId) !void {
+        _ = try self.registerCapturesImpl(payload_token, reset_into, false);
+    }
+
+    /// Error-capture variant of `registerCapturesWith`: marks each
+    /// registered capture `is_error_capture`.  Used for `else |err|`.
+    fn registerErrorCapturesWith(self: *Builder, payload_token: Ast.TokenIndex, reset_into: ?BlockId) !void {
+        _ = try self.registerCapturesImpl(payload_token, reset_into, true);
+    }
+
+    /// Shared body for the capture-registration wrappers.  When
+    /// `mark_error` is set, every registered capture local gets
+    /// `is_error_capture = true` (see LocalInfo).
+    fn registerCapturesImpl(self: *Builder, payload_token: Ast.TokenIndex, reset_into: ?BlockId, mark_error: bool) !void {
         const tree = self.tree;
         const tags = tree.tokens.items(.tag);
         var t: Ast.TokenIndex = payload_token;
@@ -802,6 +822,7 @@ const Builder = struct {
                     const name = tree.tokenSlice(t);
                     if (std.mem.eql(u8, name, "_")) continue;
                     const lid = try self.registerLocal(name, self.posOfToken(t));
+                    if (mark_error) self.locals.items[@intFromEnum(lid)].is_error_capture = true;
                     if (reset_into) |blk| {
                         try self.appendStmt(blk, .{
                             .kind = .{ .reset_capture = .{ .local = lid } },
@@ -1098,7 +1119,7 @@ const Builder = struct {
         // Lower the else branch if present.  `else |err|` payload is
         // in scope for the else-body only.
         if (else_block) |eb| {
-            if (if_data.error_token) |et| try self.registerCapturesWith(et, eb);
+            if (if_data.error_token) |et| try self.registerErrorCapturesWith(et, eb);
             var else_cur = eb;
             try self.lowerStmt(if_data.ast.else_expr.unwrap().?, &else_cur);
             try self.addEdge(else_cur, merge_block);
@@ -2069,7 +2090,7 @@ const Builder = struct {
         // `catch |err| BODY` — payload is `main_token + 2` when the
         // token immediately following `catch` is `|`.  Scope: body only.
         if (self.catchPayloadToken(catch_node)) |pt| {
-            try self.registerCaptures(pt);
+            try self.registerErrorCaptures(pt);
         }
 
         var catch_cur = catch_block;
@@ -2715,20 +2736,24 @@ const Builder = struct {
 
         // Now flush defers — fires after the .use's, before the .ret.
         //
-        // `return error.X` (or `return .{...}` resolving to an error-only
-        // path) returns an error value, so Zig fires errdefers too.
-        // Detect the syntactic `error.X` shape and use the error-path
-        // flush; everything else uses the normal-only flush.  This is
-        // conservative — `return foo()` where `foo()` returns an error
-        // also fires errdefers, but we can't tell that from the AST
-        // without callee resolution.  Catching the literal case is the
-        // common bug shape (`errdefer free(p); return error.X` after an
-        // explicit free of `p` is a textbook double-free).
-        const value_is_literal_error = if (value_opt) |expr|
-            isLiteralErrorReturn(tree, expr)
+        // Zig fires errdefers only on returns that yield an ERROR value.
+        // `returnExprIsError` recognises the statically-decidable error
+        // shapes — a literal `error.X` and a returned error-capture
+        // identifier (`catch |err| { ...; return err; }`) — and uses the
+        // error-path flush for them; everything else uses normal-only.
+        //
+        // This is a sound under-approximation: `return foo()` where
+        // `foo()` returns an error UNION (`!T`) may or may not be an
+        // error at runtime, so it is NOT classified here — flushing
+        // errdefers unconditionally would false-positive on the success
+        // path, and deciding it needs callee return-type resolution.
+        // Both caught shapes are common double-free sources, e.g.
+        // `errdefer free(p); something() catch |err| { free(p); return err; }`.
+        const value_is_error = if (value_opt) |expr|
+            self.returnExprIsError(expr)
         else
             false;
-        if (value_is_literal_error) {
+        if (value_is_error) {
             try self.flushErrAndNormalDefers(cur);
         } else {
             try self.flushDefers(cur);
@@ -4551,6 +4576,26 @@ const Builder = struct {
         }
     }
 
+    /// True iff the returned expression is statically known to be an
+    /// error value, so Zig fires errdefers on this return.  Covers:
+    ///   - literal `error.X` (and `try`-wrapped) — `isLiteralErrorReturn`
+    ///   - a bare identifier naming an in-scope error capture
+    ///     (`catch |err|` / `else |err|`), marked `is_error_capture`.
+    /// Sound under-approximation: returns of error UNIONS (`return foo()`
+    /// yielding `!T`) are deliberately NOT classified here — see the
+    /// rationale at the call site in `lowerReturn`.
+    fn returnExprIsError(self: *const Builder, expr: Ast.Node.Index) bool {
+        const tree = self.tree;
+        if (isLiteralErrorReturn(tree, expr)) return true;
+        if (tree.nodeTag(expr) == .identifier) {
+            const name = tree.tokenSlice(tree.nodeMainToken(expr));
+            if (self.name_to_local.get(name)) |lid| {
+                return self.locals.items[@intFromEnum(lid)].is_error_capture;
+            }
+        }
+        return false;
+    }
+
     fn isConstructorName(name: []const u8) bool {
         const list = [_][]const u8{
             "init", "create", "new", "open",
diff --git a/src/flow/cfg_tests.zig b/src/flow/cfg_tests.zig
index 063f1f4..0dbe3b8 100644
--- a/src/flow/cfg_tests.zig
+++ b/src/flow/cfg_tests.zig
@@ -281,6 +281,78 @@ test "plain defer DOES fire on return — kill visible before ret stmt" {
     try std.testing.expect(saw_kill);
 }
 
+test "errdefer DOES fire on `return err` from a catch capture" {
+    // `errdefer arena.deinit()` must be replayed when the function
+    // returns an error value — here `return err` re-raises the captured
+    // error from `catch |err|`.  Before the fix, only literal
+    // `return error.X` was recognised, so this `.arena_kill` was
+    // silently dropped (the errdefer-double-free-on-error-return FN).
+    const gpa = std.testing.allocator;
+    var result = try parseAndLower(gpa,
+        \\pub fn foo() !void {
+        \\    var arena = Arena.init(0);
+        \\    errdefer arena.deinit();
+        \\    sideEffect() catch |err| {
+        \\        return err;
+        \\    };
+        \\    return;
+        \\}
+        \\const Arena = struct {
+        \\    pub fn init(_: u32) Arena { return .{}; }
+        \\    pub fn deinit(_: *Arena) void {}
+        \\};
+        \\pub fn sideEffect() !void {}
+        \\
+    );
+    defer result.deinit(gpa);
+    const cfg = result.cfg.?;
+
+    // The errdefer's `arena.deinit()` (→ .arena_kill) must be replayed
+    // on the `return err` path.  The trailing `return;` is a success
+    // return and must NOT replay it — so exactly one kill appears.
+    var kill_count: usize = 0;
+    for (cfg.blocks) |b| {
+        for (b.stmts) |s| {
+            if (s.kind == .arena_kill) kill_count += 1;
+        }
+    }
+    try std.testing.expectEqual(@as(usize, 1), kill_count);
+}
+
+test "errdefer does NOT fire on a non-error `return` from a catch arm" {
+    // Symmetric guard against a false positive: a catch arm that
+    // returns a NON-error value (a literal here) is a success return,
+    // so the errdefer must stay silent — no `.arena_kill` anywhere.
+    const gpa = std.testing.allocator;
+    var result = try parseAndLower(gpa,
+        \\pub fn foo() !u32 {
+        \\    var arena = Arena.init(0);
+        \\    errdefer arena.deinit();
+        \\    const v: u32 = compute() catch |err| {
+        \\        _ = err;
+        \\        return 0;
+        \\    };
+        \\    return v;
+        \\}
+        \\const Arena = struct {
+        \\    pub fn init(_: u32) Arena { return .{}; }
+        \\    pub fn deinit(_: *Arena) void {}
+        \\};
+        \\pub fn compute() !u32 { return 1; }
+        \\
+    );
+    defer result.deinit(gpa);
+    const cfg = result.cfg.?;
+
+    var saw_kill = false;
+    for (cfg.blocks) |b| {
+        for (b.stmts) |s| {
+            if (s.kind == .arena_kill) saw_kill = true;
+        }
+    }
+    try std.testing.expect(!saw_kill);
+}
+
 test "try at statement position creates error-exit sink with defers replayed" {
     // `try call();` — adds an error-exit block reachable from cur.
     // The sink should contain whatever defers were active (here:
diff --git a/src/flow/value_range.zig b/src/flow/value_range.zig
index 7e26c5d..4b0eb26 100644
--- a/src/flow/value_range.zig
+++ b/src/flow/value_range.zig
@@ -38,6 +38,7 @@
 const std = @import("std");
 const Ast = std.zig.Ast;
 const file_cache_mod = @import("../cache/file_cache.zig");
+const fn_summary = @import("../model/fn_summary.zig");
 
 /// A set of string keys (source slices, stable for the tree's lifetime).
 const KeySet = struct {
@@ -85,18 +86,39 @@ const DiffAlias = struct {
     sub_node: Ast.Node.Index, // AST node of the subtrahend (for provablyNonneg check)
 };
 
+/// A `const LOCAL = <field-path>` binding (e.g. `const bit_length = self.bit_length`):
+/// LOCAL and the path hold the same value.  Lets a guard on the simple local
+/// (`if (bit_length == 0) return;`) establish that a later use of the path
+/// (`numMasks(self.bit_length)`) sees a non-zero argument.  Dropped when LOCAL is
+/// rebound or anything touches the path's root.
+const ValueAlias = struct {
+    local: []const u8,
+    path: []const u8,
+};
+
+/// `scalar` is known to equal the comptime constant `val` on this path (e.g.
+/// inside `switch (scalar) { K => … }` arm K, or after `const scalar = K`).
+const ScalarVal = struct {
+    name: []const u8,
+    val: u64,
+};
+
 /// Abstract state: two fact sets + len-alias bindings + diff-alias bindings.
 const State = struct {
     scalars: KeySet = .{}, // locals known != 0
     containers: KeySet = .{}, // container paths known non-empty
     aliases: std.ArrayListUnmanaged(Alias) = .empty, // n == c.len
     diff_aliases: std.ArrayListUnmanaged(DiffAlias) = .empty, // n = A - B
+    value_aliases: std.ArrayListUnmanaged(ValueAlias) = .empty, // local == path
+    scalar_vals: std.ArrayListUnmanaged(ScalarVal) = .empty, // scalar == const K
 
     fn deinit(self: *State, gpa: std.mem.Allocator) void {
         self.scalars.deinit(gpa);
         self.containers.deinit(gpa);
         self.aliases.deinit(gpa);
         self.diff_aliases.deinit(gpa);
+        self.value_aliases.deinit(gpa);
+        self.scalar_vals.deinit(gpa);
     }
     fn clone(self: *const State, gpa: std.mem.Allocator) !State {
         var out: State = .{};
@@ -105,6 +127,8 @@ const State = struct {
         try out.containers.keys.appendSlice(gpa, self.containers.keys.items);
         try out.aliases.appendSlice(gpa, self.aliases.items);
         try out.diff_aliases.appendSlice(gpa, self.diff_aliases.items);
+        try out.value_aliases.appendSlice(gpa, self.value_aliases.items);
+        try out.scalar_vals.appendSlice(gpa, self.scalar_vals.items);
         return out;
     }
     fn intersectWith(self: *State, other: *const State) void {
@@ -119,16 +143,28 @@ const State = struct {
         while (j < self.diff_aliases.items.len) {
             if (other.hasDiffAlias(self.diff_aliases.items[j])) j += 1 else _ = self.diff_aliases.swapRemove(j);
         }
+        var k: usize = 0;
+        while (k < self.value_aliases.items.len) {
+            if (other.hasValueAlias(self.value_aliases.items[k])) k += 1 else _ = self.value_aliases.swapRemove(k);
+        }
+        var m: usize = 0;
+        while (m < self.scalar_vals.items.len) {
+            if (other.hasScalarVal(self.scalar_vals.items[m])) m += 1 else _ = self.scalar_vals.swapRemove(m);
+        }
     }
     fn replaceWith(self: *State, gpa: std.mem.Allocator, src: *const State) !void {
         self.scalars.keys.clearRetainingCapacity();
         self.containers.keys.clearRetainingCapacity();
         self.aliases.clearRetainingCapacity();
         self.diff_aliases.clearRetainingCapacity();
+        self.value_aliases.clearRetainingCapacity();
+        self.scalar_vals.clearRetainingCapacity();
         try self.scalars.keys.appendSlice(gpa, src.scalars.keys.items);
         try self.containers.keys.appendSlice(gpa, src.containers.keys.items);
         try self.aliases.appendSlice(gpa, src.aliases.items);
         try self.diff_aliases.appendSlice(gpa, src.diff_aliases.items);
+        try self.value_aliases.appendSlice(gpa, src.value_aliases.items);
+        try self.scalar_vals.appendSlice(gpa, src.scalar_vals.items);
     }
     fn hasAlias(self: *const State, a: Alias) bool {
         for (self.aliases.items) |e|
@@ -171,6 +207,51 @@ const State = struct {
             } else i += 1;
         }
     }
+    fn hasValueAlias(self: *const State, va: ValueAlias) bool {
+        for (self.value_aliases.items) |e|
+            if (std.mem.eql(u8, e.local, va.local) and std.mem.eql(u8, e.path, va.path)) return true;
+        return false;
+    }
+    fn addValueAlias(self: *State, gpa: std.mem.Allocator, va: ValueAlias) !void {
+        if (self.hasValueAlias(va)) return;
+        try self.value_aliases.append(gpa, va);
+    }
+    /// Drop value_aliases whose local or whose path *starts with* `root` (so a
+    /// rebind of the local, or a mutation of the path's root identifier,
+    /// invalidates the equality).
+    fn dropValueAliasesByRoot(self: *State, root: []const u8) void {
+        var i: usize = 0;
+        while (i < self.value_aliases.items.len) {
+            const va = self.value_aliases.items[i];
+            const path_root_match = std.mem.startsWith(u8, va.path, root) and
+                (va.path.len == root.len or va.path[root.len] == '.' or va.path[root.len] == '[');
+            if (std.mem.eql(u8, va.local, root) or path_root_match) {
+                _ = self.value_aliases.swapRemove(i);
+            } else i += 1;
+        }
+    }
+    fn hasScalarVal(self: *const State, sv: ScalarVal) bool {
+        for (self.scalar_vals.items) |e|
+            if (std.mem.eql(u8, e.name, sv.name) and e.val == sv.val) return true;
+        return false;
+    }
+    fn setScalarVal(self: *State, gpa: std.mem.Allocator, name: []const u8, val: u64) !void {
+        self.dropScalarValsByName(name);
+        try self.scalar_vals.append(gpa, .{ .name = name, .val = val });
+    }
+    fn scalarVal(self: *const State, name: []const u8) ?u64 {
+        for (self.scalar_vals.items) |e|
+            if (std.mem.eql(u8, e.name, name)) return e.val;
+        return null;
+    }
+    fn dropScalarValsByName(self: *State, name: []const u8) void {
+        var i: usize = 0;
+        while (i < self.scalar_vals.items.len) {
+            if (std.mem.eql(u8, self.scalar_vals.items[i].name, name)) {
+                _ = self.scalar_vals.swapRemove(i);
+            } else i += 1;
+        }
+    }
 };
 
 const Flow = struct {
@@ -178,7 +259,7 @@ const Flow = struct {
     diverged: bool = false,
 };
 
-const Query = enum { nonzero_scalar, nonempty_container };
+const Query = enum { nonzero_scalar, nonempty_container, min_len_container };
 
 const Oracle = struct {
     gpa: std.mem.Allocator,
@@ -186,6 +267,8 @@ const Oracle = struct {
     query: Query,
     target: []const u8,
     use_token: Ast.TokenIndex,
+    /// For `min_len_container`: the threshold N — is `target.len >= N`?
+    min_n: u64 = 0,
     /// Optional type engine, used only to confirm a comparison operand is an
     /// UNSIGNED integer (so `key > operand` soundly implies `key >= 1`).  Null
     /// in unit tests → the type-gated `>` generalization simply doesn't apply.
@@ -205,6 +288,16 @@ const Oracle = struct {
         return switch (self.query) {
             .nonzero_scalar => st.scalars.contains(self.target),
             .nonempty_container => st.containers.contains(self.target),
+            // `target.len >= min_n`: proven via a slice-length alias
+            // (`target.len == scalar`) whose scalar has a known value >= min_n
+            // (e.g. from a `switch (scalar)` arm).
+            .min_len_container => {
+                for (st.aliases.items) |a| {
+                    if (!std.mem.eql(u8, a.container, self.target)) continue;
+                    if (st.scalarVal(a.scalar)) |v| if (v >= self.min_n) return true;
+                }
+                return false;
+            },
         };
     }
 };
@@ -219,7 +312,7 @@ pub fn provesNonzero(
     use_token: Ast.TokenIndex,
     cache: ?*file_cache_mod.FileCache,
 ) bool {
-    return run(gpa, tree, body_node, .nonzero_scalar, target, use_token, cache);
+    return run(gpa, tree, body_node, .nonzero_scalar, target, use_token, 0, cache);
 }
 
 /// Is container `target` (a source-spelling like "arr" or "self.items")
@@ -232,7 +325,23 @@ pub fn provesNonempty(
     use_token: Ast.TokenIndex,
     cache: ?*file_cache_mod.FileCache,
 ) bool {
-    return run(gpa, tree, body_node, .nonempty_container, target, use_token, cache);
+    return run(gpa, tree, body_node, .nonempty_container, target, use_token, 0, cache);
+}
+
+/// Is container `target` provably of length >= `n` at `use_token`?  Proven via a
+/// slice-length alias (`target = base[0..S]` ⟹ `target.len == S`) whose scalar
+/// `S` has a known constant value >= n (e.g. from an enclosing `switch (S)` arm).
+/// Covers the wyhash-style `switch (rem_len) { K => rem_key[N..] }` family.
+pub fn provesMinLen(
+    gpa: std.mem.Allocator,
+    tree: *const Ast,
+    body_node: Ast.Node.Index,
+    target: []const u8,
+    n: u64,
+    use_token: Ast.TokenIndex,
+    cache: ?*file_cache_mod.FileCache,
+) bool {
+    return run(gpa, tree, body_node, .min_len_container, target, use_token, n, cache);
 }
 
 fn run(
@@ -242,6 +351,7 @@ fn run(
     query: Query,
     target: []const u8,
     use_token: Ast.TokenIndex,
+    min_n: u64,
     cache: ?*file_cache_mod.FileCache,
 ) bool {
     var oracle: Oracle = .{
@@ -250,6 +360,7 @@ fn run(
         .query = query,
         .target = target,
         .use_token = use_token,
+        .min_n = min_n,
         .cache = cache,
     };
     var st: State = .{};
@@ -267,14 +378,33 @@ fn analyzeNode(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemory}!
             return analyzeSeq(o, blockStmts(tree, node, &buf), st);
         },
         .@"if", .if_simple => return analyzeIf(o, node, st),
+        .@"switch", .switch_comma => return analyzeSwitch(o, node, st),
         .@"while", .while_simple, .while_cont => return analyzeLoop(o, node, st, .while_),
         .@"for", .for_simple => return analyzeLoop(o, node, st, .for_),
         .simple_var_decl, .local_var_decl, .aligned_var_decl => return analyzeVarDecl(o, node, st),
         .assign => return analyzeAssign(o, node, st),
         .assign_add => return analyzeCompoundAdd(o, node, st),
+        // Short-circuit operators refine their RHS: in `A and B`, A is true while
+        // B evaluates; in `A or B`, A is false while B evaluates.  Covers the
+        // canonical guarded last-element idioms `c.len > 0 and c[c.len-1]` and
+        // `c.len == 0 or c[c.len-1]` (endsWith/startsWith), where the bounds
+        // proof lives in the same expression rather than an enclosing `if`.
+        .bool_and => return analyzeShortCircuit(o, node, st, true),
+        .bool_or => return analyzeShortCircuit(o, node, st, false),
         .@"return", .@"break", .@"continue", .unreachable_literal => {
             var flow: Flow = .{ .diverged = true };
-            if (o.tokenInNode(node)) flow.answer = o.answerAt(st);
+            if (o.tokenInNode(node)) {
+                // Descend into a `return <expr>;` operand so short-circuit
+                // refinement (bool_and/bool_or) applies before answering.
+                const operand: ?Ast.Node.Index = if (tree.nodeTag(node) == .@"return")
+                    tree.nodeData(node).opt_node.unwrap()
+                else
+                    null;
+                if (operand) |e| {
+                    const sub = try analyzeNode(o, e, st);
+                    flow.answer = sub.answer orelse o.answerAt(st);
+                } else flow.answer = o.answerAt(st);
+            }
             return flow;
         },
         else => {
@@ -318,10 +448,32 @@ fn analyzeVarDecl(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemor
     dropContainersRootedAt(st, name);
     st.dropAliasesByScalar(name);
     st.dropDiffAliasesByName(name);
+    st.dropValueAliasesByRoot(name);
+    st.dropScalarValsByName(name);
+    // Record a `const name = <field-path>` value alias (e.g.
+    // `const bit_length = self.bit_length`): name and the path are equal, so a
+    // guard on `name` later proves the path non-zero (see argProvablyNonzero).
+    if (fieldPathSrc(o, init_node)) |psrc| {
+        try st.addValueAlias(o.gpa, .{ .local = name, .path = psrc });
+    }
+    // Cross-fn: `const name = callee(arg)` where `callee` provably returns a
+    // non-zero value given a non-zero argument (e.g. ceil-division `numMasks`),
+    // and `arg` is proven non-zero here.  Then `name` is non-zero.
+    if (callResultNonzero(o, init_node, st)) try st.scalars.add(o.gpa, name);
     // Record a `const/var name = <c>.len` length-snapshot alias.
     if (lenContainerPath(o, init_node)) |cpath| {
         try st.addAlias(o.gpa, .{ .scalar = name, .container = cpath });
     }
+    // Record a `const/var name = base[0..N]` slice alias: name.len == N (same
+    // semantics as a `.len` snapshot, scalar=N container=name).  So a nonzero N
+    // ⟹ name non-empty, making `name[name.len - 1]` safe.  Restricted to a `0`
+    // start so the length is exactly the single scalar N.
+    if (sliceLenScalarName(o, init_node)) |nname| {
+        try st.addAlias(o.gpa, .{ .scalar = nname, .container = name });
+        // Immediate propagation: if N is already proven nonzero (e.g. a prior
+        // `if (N == 0) return` guard), `name` is non-empty right now.
+        if (st.scalars.contains(nname)) try st.containers.add(o.gpa, name);
+    }
     // Record a `const/var name = MINUEND - SUBTRAHEND` diff alias.
     // Used to propagate: when `name` is proven nonzero AND the subtrahend
     // is provably >= 0 (non-negative literal, .len, or unsigned by type engine),
@@ -344,6 +496,14 @@ fn analyzeAssign(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemory
     const data = tree.nodeData(node).node_and_node;
     const lhs = data[0];
     const rhs = data[1];
+    // The use may be in the LHS index expression of a subscript write
+    // (`buf[idx - 1] = …`).  The index is READ before the store, so answer the
+    // query against the current state — otherwise a provably-nonzero index on
+    // the write side is never resolved and the rule false-positives.
+    if (o.tokenInNode(lhs)) {
+        const flow = try analyzeNode(o, lhs, st);
+        if (flow.answer != null) return flow;
+    }
     if (o.tokenInNode(rhs)) {
         const flow = try analyzeNode(o, rhs, st);
         if (flow.answer != null) return flow;
@@ -357,16 +517,35 @@ fn analyzeAssign(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemory
         dropContainersRootedAt(st, name);
         st.dropAliasesByScalar(name);
         st.dropDiffAliasesByName(name);
+        st.dropValueAliasesByRoot(name);
+    st.dropScalarValsByName(name);
         // A re-bind to `c.len` re-establishes the alias.
         if (lenContainerPath(o, rhs)) |cpath| try st.addAlias(o.gpa, .{ .scalar = name, .container = cpath });
     } else {
         // Assignment through a field/index (`c.items = ...`) — conservatively
         // drop container facts whose path the LHS could alter.
         killMutatedContainers(o, node, st);
+        // A field write (`self.bit_length = …`) invalidates value-aliases whose
+        // path is rooted at the written path's head identifier.
+        if (lhsRootIdent(o, lhs)) |root| st.dropValueAliasesByRoot(root);
     }
     return .{};
 }
 
+/// Root identifier of an assignment LHS path (`self` from `self.bit_length`,
+/// `arr` from `arr[i].x`), or null.
+fn lhsRootIdent(o: *Oracle, lhs: Ast.Node.Index) ?[]const u8 {
+    const tree = o.tree;
+    var n = lhs;
+    while (true) switch (tree.nodeTag(n)) {
+        .identifier => return tree.tokenSlice(tree.nodeMainToken(n)),
+        .field_access => n = tree.nodeData(n).node_and_token[0],
+        .array_access => n = tree.nodeData(n).node_and_node[0],
+        .deref => n = tree.nodeData(n).node,
+        else => return null,
+    };
+}
+
 /// `x += <expr>` (non-wrapping).  For an unsigned `x`, addition never
 /// decreases the value, so:
 ///   - `x += <positive literal>` establishes `x >= 1` (x_old >= 0 + >=1).
@@ -380,6 +559,11 @@ fn analyzeCompoundAdd(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfM
     const data = tree.nodeData(node).node_and_node;
     const lhs = data[0];
     const rhs = data[1];
+    // Use may be in the LHS subscript (`buf[idx - 1] += …`) — answer first.
+    if (o.tokenInNode(lhs)) {
+        const flow = try analyzeNode(o, lhs, st);
+        if (flow.answer != null) return flow;
+    }
     if (o.tokenInNode(rhs)) {
         const flow = try analyzeNode(o, rhs, st);
         if (flow.answer != null) return flow;
@@ -391,6 +575,8 @@ fn analyzeCompoundAdd(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfM
         dropContainersRootedAt(st, name);
         st.dropAliasesByScalar(name);
         st.dropDiffAliasesByName(name);
+        st.dropValueAliasesByRoot(name);
+    st.dropScalarValsByName(name);
     } else {
         killMutatedContainers(o, node, st);
     }
@@ -437,6 +623,59 @@ fn analyzeIf(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemory}!Fl
     return .{};
 }
 
+/// `A and B` / `A or B` as a (sub)expression.  When the use token is inside the
+/// RHS, evaluate it under the short-circuit refinement of the LHS: for `and`,
+/// the LHS's THEN-facts hold (A is true); for `or`, the LHS's ELSE-facts hold
+/// (A is false).  Sound because Zig `and`/`or` only evaluate B when A is
+/// true/false respectively.
+fn analyzeShortCircuit(o: *Oracle, node: Ast.Node.Index, st: *State, is_and: bool) error{OutOfMemory}!Flow {
+    const tree = o.tree;
+    const d = tree.nodeData(node).node_and_node;
+    const lhs = d[0];
+    const rhs = d[1];
+    if (o.tokenInNode(rhs)) {
+        var refine: Refinement = .{};
+        collectRefinement(o, lhs, &refine);
+        var rhs_st = try st.clone(o.gpa);
+        defer rhs_st.deinit(o.gpa);
+        const scalar = if (is_and) refine.then_scalar else refine.else_scalar;
+        const container = if (is_and) refine.then_container else refine.else_container;
+        try applyRefine(o, &rhs_st, scalar, container);
+        return try analyzeNode(o, rhs, &rhs_st);
+    }
+    if (o.tokenInNode(lhs)) return try analyzeNode(o, lhs, st);
+    if (o.tokenInNode(node)) return .{ .answer = o.answerAt(st) };
+    return .{};
+}
+
+/// `switch (scrutinee) { K => arm, … }`.  When the use is in an arm whose single
+/// label is an integer literal `K` and the scrutinee is a simple scalar, record
+/// `scrutinee == K` (and nonzero if K != 0) for that arm — so a slice whose
+/// length aliases the scrutinee is known to have length K inside the arm.
+fn analyzeSwitch(o: *Oracle, node: Ast.Node.Index, st: *State) error{OutOfMemory}!Flow {
+    const tree = o.tree;
+    const sw = tree.fullSwitch(node) orelse return .{};
+    if (o.tokenInNode(sw.ast.condition)) return .{ .answer = o.answerAt(st) };
+    const scrut = identName(tree, sw.ast.condition);
+    for (sw.ast.cases) |case_node| {
+        const sc = tree.fullSwitchCase(case_node) orelse continue;
+        const body = sc.ast.target_expr;
+        if (!o.tokenInNode(body)) continue;
+        var arm_st = try st.clone(o.gpa);
+        defer arm_st.deinit(o.gpa);
+        if (scrut) |sn| {
+            if (sc.ast.values.len == 1) {
+                if (intLiteralVal(tree, sc.ast.values[0])) |k| {
+                    try arm_st.setScalarVal(o.gpa, sn, k);
+                    if (k != 0) try arm_st.scalars.add(o.gpa, sn);
+                }
+            }
+        }
+        return try analyzeNode(o, body, &arm_st);
+    }
+    return .{};
+}
+
 const LoopKind = enum { while_, for_ };
 
 fn analyzeLoop(o: *Oracle, node: Ast.Node.Index, st: *State, kind: LoopKind) error{OutOfMemory}!Flow {
@@ -453,7 +692,11 @@ fn analyzeLoop(o: *Oracle, node: Ast.Node.Index, st: *State, kind: LoopKind) err
         .while_ => if (tree.fullWhile(node)) |w| w.ast.cond_expr else null,
         .for_ => null,
     };
-    if (cond_node) |c| if (o.tokenInNode(c)) return .{ .answer = o.answerAt(st) };
+    // Use inside the loop condition itself: descend so short-circuit refinement
+    // applies (`while (tmp > beg and self.text[tmp-1] == …)` — the `and`'s LHS
+    // guards its RHS).  analyzeNode handles bool_and/bool_or; a plain comparison
+    // falls through to answerAt.
+    if (cond_node) |c| if (o.tokenInNode(c)) return try analyzeNode(o, c, st);
     if (body_node) |b| {
         if (o.tokenInNode(b)) {
             var body_st = try st.clone(o.gpa);
@@ -676,11 +919,17 @@ fn dropLoopMutated(o: *Oracle, loop_node: Ast.Node.Index, st: *State) void {
     const first = tree.firstToken(loop_node);
     const last = tree.lastToken(loop_node);
     const tags = tree.tokens.items(.tag);
-    // Scalars: any `NAME <assign-op>` inside the loop.
+    // Scalars: drop a nonzero fact only when the loop mutates the name
+    // NON-monotonically.  `NAME += …` on an unsigned can only grow the value
+    // (the safe/panic-on-overflow build never wraps to 0), so a scalar that is
+    // nonzero before the loop and *only* `+=`-mutated stays nonzero on every
+    // iteration — keep it.  Any other assign op (`=`, `-=`, `*=`, …) can reach
+    // 0, so drop.  Covers `var p: usize = 1; while (…) { …a[p-1]…; p += 1; }`.
     var t = first;
     while (t < last) : (t += 1) {
         if (tags[t] != .identifier) continue;
-        if (isAssignOp(tags[t + 1])) st.scalars.remove(tree.tokenSlice(t));
+        if (!isAssignOp(tags[t + 1])) continue;
+        if (tags[t + 1] != .plus_equal) st.scalars.remove(tree.tokenSlice(t));
     }
     dropContainersMutatedInTokens(tree, first, last, st);
 }
@@ -797,6 +1046,17 @@ fn identName(tree: *const Ast, node: Ast.Node.Index) ?[]const u8 {
     return tree.tokenSlice(tree.nodeMainToken(node));
 }
 
+/// For a slice expression `base[0..N]` (start literal 0, end an identifier),
+/// return N's name — the slice's length equals N.  Null for non-slices,
+/// non-zero starts, open-ended slices, or non-identifier ends.
+fn sliceLenScalarName(o: *Oracle, node: Ast.Node.Index) ?[]const u8 {
+    const tree = o.tree;
+    const sl = tree.fullSlice(node) orelse return null;
+    if (!isIntLiteralValue(tree, sl.ast.start, 0)) return null;
+    const end = sl.ast.end.unwrap() orelse return null;
+    return identName(tree, end);
+}
+
 fn isAssignOp(tag: std.zig.Token.Tag) bool {
     return switch (tag) {
         .equal,
@@ -840,6 +1100,150 @@ fn nodeSrc(tree: *const Ast, node: Ast.Node.Index) []const u8 {
     return tree.source[start..end];
 }
 
+fn unwrapGrouped(tree: *const Ast, node: Ast.Node.Index) Ast.Node.Index {
+    var n = node;
+    while (tree.nodeTag(n) == .grouped_expression) n = tree.nodeData(n).node_and_token[0];
+    return n;
+}
+
+/// True iff `node` is a pure field-access chain rooted at an identifier
+/// (`self.bit_length`, `a.b.c`) — no calls, no subscripts.
+fn isPureFieldPath(tree: *const Ast, node: Ast.Node.Index) bool {
+    return switch (tree.nodeTag(node)) {
+        .identifier => true,
+        .field_access => isPureFieldPath(tree, tree.nodeData(node).node_and_token[0]),
+        else => false,
+    };
+}
+
+/// Source spelling of a pure field-access path with at least one `.`, else null.
+fn fieldPathSrc(o: *Oracle, node: Ast.Node.Index) ?[]const u8 {
+    const tree = o.tree;
+    if (tree.nodeTag(node) != .field_access) return null;
+    if (!isPureFieldPath(tree, node)) return null;
+    return nodeSrc(tree, node);
+}
+
+/// Is the call argument `arg` provably non-zero in `st`?  A simple identifier is
+/// looked up in the nonzero set; a field-path is matched against a value-alias
+/// (`const local = path`) whose local is non-zero.
+fn argProvablyNonzero(o: *Oracle, st: *const State, arg: Ast.Node.Index) bool {
+    const tree = o.tree;
+    if (identName(tree, arg)) |nm| return st.scalars.contains(nm);
+    if (fieldPathSrc(o, arg)) |psrc| {
+        if (st.scalars.contains(psrc)) return true;
+        for (st.value_aliases.items) |va|
+            if (std.mem.eql(u8, va.path, psrc) and st.scalars.contains(va.local)) return true;
+    }
+    return false;
+}
+
+/// Cross-fn: is `init` a call `callee(arg)` whose result is provably non-zero?
+/// True when `callee` is an in-file single-return function whose return is
+/// non-zero given its first parameter non-zero (e.g. ceil-division), AND `arg`
+/// is proven non-zero at the call.  Single-argument callees only (v1).
+fn callResultNonzero(o: *Oracle, init: Ast.Node.Index, st: *const State) bool {
+    const tree = o.tree;
+    var buf: [1]Ast.Node.Index = undefined;
+    const call = tree.fullCall(&buf, init) orelse return false;
+    const callee = identName(tree, call.ast.fn_expr) orelse return false;
+    if (call.ast.params.len != 1) return false;
+    if (!argProvablyNonzero(o, st, call.ast.params[0])) return false;
+    return calleeReturnsNonzeroGivenArg(o, callee);
+}
+
+/// Every in-file function (top-level or method) named `name` has a single
+/// `return EXPR` whose value is provably non-zero given its first parameter
+/// non-zero.  Conservative: false if no such function is found, or ANY same-named
+/// function fails (so it holds whichever overload is actually called).
+fn calleeReturnsNonzeroGivenArg(o: *Oracle, name: []const u8) bool {
+    const tree = o.tree;
+    var found = false;
+    var ni: u32 = 0;
+    while (ni < tree.nodes.len) : (ni += 1) {
+        const fnode: Ast.Node.Index = @enumFromInt(ni);
+        if (tree.nodeTag(fnode) != .fn_decl) continue;
+        const fdata = tree.nodeData(fnode).node_and_node;
+        var pbuf: [1]Ast.Node.Index = undefined;
+        const proto = tree.fullFnProto(&pbuf, fdata[0]) orelse continue;
+        const nt = proto.name_token orelse continue;
+        if (!std.mem.eql(u8, tree.tokenSlice(nt), name)) continue;
+        found = true;
+        const ret = fn_summary.singleReturnExpr(tree, fdata[1]) orelse return false;
+        var it = proto.iterate(tree);
+        const p0 = it.next() orelse return false;
+        const pname = if (p0.name_token) |t| tree.tokenSlice(t) else return false;
+        if (!exprNonzeroPostcond(o, ret, pname)) return false;
+    }
+    return found;
+}
+
+/// Is `expr` provably non-zero assuming the single parameter `pname` is non-zero?
+/// Handles: positive literals, the parameter itself, unsigned addition (either
+/// operand non-zero), and ceil-division `(A + C) / D` with A non-zero and
+/// comptime constants `C >= D - 1` (⟹ `A + C >= D` ⟹ quotient >= 1).
+fn exprNonzeroPostcond(o: *Oracle, expr: Ast.Node.Index, pname: []const u8) bool {
+    const tree = o.tree;
+    const e = unwrapGrouped(tree, expr);
+    switch (tree.nodeTag(e)) {
+        .number_literal => return isPositiveIntLiteral(tree, e),
+        .identifier => return std.mem.eql(u8, tree.tokenSlice(tree.nodeMainToken(e)), pname),
+        .add, .add_wrap, .add_sat => {
+            const d = tree.nodeData(e).node_and_node;
+            return exprNonzeroPostcond(o, d[0], pname) or exprNonzeroPostcond(o, d[1], pname);
+        },
+        .div => {
+            const d = tree.nodeData(e).node_and_node;
+            const div_node = d[1];
+            const num = unwrapGrouped(tree, d[0]);
+            if (tree.nodeTag(num) != .add) return false;
+            const ad = tree.nodeData(num).node_and_node;
+            return ceilDivBase(o, ad[0], ad[1], div_node, pname) or
+                ceilDivBase(o, ad[1], ad[0], div_node, pname);
+        },
+        else => return false,
+    }
+}
+
+/// `(base + addend) / divisor` is non-zero when `base` is non-zero and
+/// `addend >= divisor - 1` (⟹ `base + addend >= divisor` ⟹ quotient >= 1).
+/// The bound is proven two ways: (1) comptime values `C >= D - 1`; (2) STRUCTURAL
+/// — `addend` is syntactically `divisor - 1` (e.g. ceil-div idiom
+/// `(x + (@bitSizeOf(T) - 1)) / @bitSizeOf(T)`), which holds for ANY value of the
+/// divisor even when the engine can't evaluate it (`@bitSizeOf` isn't a literal).
+fn ceilDivBase(o: *Oracle, base: Ast.Node.Index, addend: Ast.Node.Index, div_node: Ast.Node.Index, pname: []const u8) bool {
+    if (!exprNonzeroPostcond(o, base, pname)) return false;
+    if (comptimeValOf(o, div_node)) |dval| {
+        if (dval != 0) {
+            if (comptimeValOf(o, addend)) |cval| {
+                if (cval + 1 >= dval) return true;
+            }
+        }
+    }
+    return addendIsDivisorMinusOne(o, addend, div_node);
+}
+
+/// True iff `addend` is syntactically `<X> - 1` where `<X>` has the same source
+/// spelling as `div_node` — so `addend == divisor - 1` exactly, regardless of
+/// the (possibly engine-opaque) value.
+fn addendIsDivisorMinusOne(o: *Oracle, addend: Ast.Node.Index, div_node: Ast.Node.Index) bool {
+    const tree = o.tree;
+    const a = unwrapGrouped(tree, addend);
+    if (tree.nodeTag(a) != .sub) return false;
+    const sd = tree.nodeData(a).node_and_node;
+    if (!isIntLiteralValue(tree, sd[1], 1)) return false;
+    const left = unwrapGrouped(tree, sd[0]);
+    const div = unwrapGrouped(tree, div_node);
+    return std.mem.eql(u8, nodeSrc(tree, left), nodeSrc(tree, div));
+}
+
+/// Comptime value of `node` via the type engine, or null (also null without a
+/// resolver — keeps the cross-fn check sound in token-only mode).
+fn comptimeValOf(o: *Oracle, node: Ast.Node.Index) ?u64 {
+    const cache = o.cache orelse return null;
+    return cache.comptimeIntValueOf(unwrapGrouped(o.tree, node));
+}
+
 fn blockStmts(
     tree: *const Ast,
     block_node: Ast.Node.Index,
diff --git a/src/flow/value_range_tests.zig b/src/flow/value_range_tests.zig
index 82f554b..71c4f66 100644
--- a/src/flow/value_range_tests.zig
+++ b/src/flow/value_range_tests.zig
@@ -200,6 +200,126 @@ test "nonzero: guard in while condition refines body" {
     , "i", "buf"));
 }
 
+test "nonzero: use on LHS of a subscript write (buf[i-1] = …)" {
+    // Regression: analyzeAssign only inspected the RHS for the use token, so a
+    // provably-nonzero index on the WRITE side (`buf[i-1] = 0`) was never
+    // resolved and the rule false-positived. `.len` guard needs no type engine.
+    try std.testing.expect(try proveAt(
+        \\fn f(i: usize, buf: []u8, other: []const u8) void {
+        \\    if (i > other.len) {
+        \\        buf[i - 1] = 0;
+        \\    }
+        \\}
+        \\
+    , "i", "buf"));
+}
+
+test "nonzero: LHS subscript write under a bare (no-block) if" {
+    try std.testing.expect(try proveAt(
+        \\fn f(i: usize, buf: []u8, other: []const u8) void {
+        \\    if (i > other.len) buf[i - 1] = 0;
+        \\}
+        \\
+    , "i", "buf"));
+}
+
+test "nonzero: no false-negative — unguarded LHS write still unproven" {
+    try std.testing.expect(!try proveAt(
+        \\fn f(i: usize, buf: []u8) void {
+        \\    buf[i - 1] = 0;
+        \\}
+        \\
+    , "i", "buf"));
+}
+
+test "nonzero: cross-fn ceil-div postcondition (numMasks) with guarded arg" {
+    // `m = numMasks(k)` where numMasks is `(x + (D-1)) / D` (ceil-div, structural
+    // D-1 == D-1), and k is guarded non-zero ⟹ m non-zero. Caller listed first so
+    // `proveAt` analyzes it; the callee scan finds `numMasks` regardless of order.
+    try std.testing.expect(try proveAt(
+        \\fn f(a: []u8, k: usize) u8 {
+        \\    if (k == 0) return 0;
+        \\    const m = numMasks(k);
+        \\    return a[m - 1];
+        \\}
+        \\fn numMasks(x: usize) usize {
+        \\    return (x + (64 - 1)) / 64;
+        \\}
+    , "m", "a"));
+}
+
+test "nonzero: cross-fn — unguarded arg leaves result UNPROVEN (no false-negative)" {
+    try std.testing.expect(!try proveAt(
+        \\fn f(a: []u8, k: usize) u8 {
+        \\    const m = numMasks(k);
+        \\    return a[m - 1];
+        \\}
+        \\fn numMasks(x: usize) usize {
+        \\    return (x + (64 - 1)) / 64;
+        \\}
+    , "m", "a"));
+}
+
+test "nonzero: cross-fn via field-path value-alias (const L = s.len guards s.len arg)" {
+    try std.testing.expect(try proveAt(
+        \\fn f(s: S, a: []u8) u8 {
+        \\    const L = s.len;
+        \\    if (L == 0) return 0;
+        \\    const m = numMasks(s.len);
+        \\    return a[m - 1];
+        \\}
+        \\fn numMasks(x: usize) usize {
+        \\    return (x + (64 - 1)) / 64;
+        \\}
+    , "m", "a"));
+}
+
+test "nonempty: `s = base[0..n]` with n guarded nonzero ⟹ s non-empty" {
+    try std.testing.expect(try proveNonemptyAt(
+        \\fn f(buf: []u8, n: usize) u8 {
+        \\    if (n == 0) return 0;
+        \\    const s = buf[0..n];
+        \\    return s[s.len - 1];
+        \\}
+    , "s", "s"));
+}
+
+test "nonempty: `s = base[0..n]` with n unguarded is UNPROVEN (no false-negative)" {
+    try std.testing.expect(!try proveNonemptyAt(
+        \\fn f(buf: []u8, n: usize) u8 {
+        \\    const s = buf[0..n];
+        \\    return s[s.len - 1];
+        \\}
+    , "s", "s"));
+}
+
+test "nonempty: short-circuit `c.len > 0 and c[c.len-1]` (endsWith idiom)" {
+    try std.testing.expect(try proveNonemptyAt(
+        \\fn endsWith(self: []const u8, ch: u8) bool {
+        \\    return self.len > 0 and self[self.len - 1] == ch;
+        \\}
+        \\
+    , "self", "self"));
+}
+
+test "nonempty: short-circuit `c.len == 0 or c[c.len-1]` (or-form)" {
+    try std.testing.expect(try proveNonemptyAt(
+        \\fn endsWithOrEmpty(self: []const u8, ch: u8) bool {
+        \\    return self.len == 0 or self[self.len - 1] == ch;
+        \\}
+        \\
+    , "self", "self"));
+}
+
+test "nonempty: no false-negative — unguarded access in same fn still unproven" {
+    try std.testing.expect(!try proveNonemptyAt(
+        \\fn last(self: []const u8) u8 {
+        \\    return self[self.len - 1];
+        \\}
+        \\
+    , "self", "self"));
+}
+
 test "nonzero: and-chain guard (i > 0 and c)" {
     try std.testing.expect(try proveAt(
         \\fn f(i: usize, c: bool, buf: []const u8) u8 {
@@ -246,6 +366,52 @@ fn proveNonemptyAt(src: [:0]const u8, container: []const u8, arr: []const u8) !b
     return value_range.provesNonempty(gpa, &tree, body, container, lbracket, null);
 }
 
+/// Query `provesMinLen(container, n)` at the `[` token after identifier `arr`.
+fn proveMinLenAt(src: [:0]const u8, container: []const u8, n: u64, arr: []const u8) !bool {
+    const gpa = std.testing.allocator;
+    var tree = try Ast.parse(gpa, src, .zig);
+    defer tree.deinit(gpa);
+    const body = firstFnBody(&tree) orelse return error.NoFnBody;
+    const lbracket = subscriptLBracket(&tree, arr) orelse return error.NoSubscript;
+    return value_range.provesMinLen(gpa, &tree, body, container, n, lbracket, null);
+}
+
+test "minlen: switch-arm bounds a slice-from-range length (k.len >= 16 in arm 20)" {
+    try std.testing.expect(try proveMinLenAt(
+        \\fn f(b: []const u8) u8 {
+        \\    const n = b.len;
+        \\    const k = b[0..n];
+        \\    return switch (n) {
+        \\        20 => k[16],
+        \\        else => 0,
+        \\    };
+        \\}
+    , "k", 16, "k"));
+}
+
+test "minlen: switch arm BELOW threshold is UNPROVEN (no false-negative)" {
+    try std.testing.expect(!try proveMinLenAt(
+        \\fn f(b: []const u8) u8 {
+        \\    const n = b.len;
+        \\    const k = b[0..n];
+        \\    return switch (n) {
+        \\        10 => k[16],
+        \\        else => 0,
+        \\    };
+        \\}
+    , "k", 16, "k"));
+}
+
+test "minlen: no switch ⟹ unproven (no false-negative)" {
+    try std.testing.expect(!try proveMinLenAt(
+        \\fn f(b: []const u8) u8 {
+        \\    const n = b.len;
+        \\    const k = b[0..n];
+        \\    return k[16];
+        \\}
+    , "k", 16, "k"));
+}
+
 test "nonempty: bare arr.len-1 is unknown (fires)" {
     try std.testing.expect(!try proveNonemptyAt(
         \\fn f(arr: []const u8) u8 {
@@ -518,3 +684,28 @@ test "diff-alias: rebinding end clears diff fact" {
         \\
     , "end_mut", "buf"));
 }
+
+test "nonzero: loop var only `+=`'d keeps its positive init (monotonic)" {
+    try std.testing.expect(try proveAt(
+        \\fn f(buf: []u8) void {
+        \\    var p: usize = 1;
+        \\    while (p < buf.len) {
+        \\        buf[p - 1] = 0;
+        \\        p += 1;
+        \\    }
+        \\}
+    , "p", "buf"));
+}
+
+test "nonzero: loop var reset to 0 then accessed is UNPROVEN (no false-negative)" {
+    try std.testing.expect(!try proveAt(
+        \\fn f(buf: []u8) void {
+        \\    var p: usize = 1;
+        \\    while (p < buf.len) {
+        \\        p = 0;
+        \\        buf[p - 1] = 0;
+        \\        p += 1;
+        \\    }
+        \\}
+    , "p", "buf"));
+}
diff --git a/src/rules/misc/forced_unwrap_iterator_next.zig b/src/rules/misc/forced_unwrap_iterator_next.zig
index da948cd..aebb90e 100644
--- a/src/rules/misc/forced_unwrap_iterator_next.zig
+++ b/src/rules/misc/forced_unwrap_iterator_next.zig
@@ -194,12 +194,24 @@ fn isFirstNextOnSplitIterator(
     }
     const decl_tok = decl orelse return false;
 
-    // The RHS (decl .. semicolon) must name a `split*` constructor.
+    // The RHS (decl .. semicolon) must name an iterator constructor whose first
+    // `.next()` is guaranteed non-null: a `split*` constructor, or a
+    // `std.process.args()` / `argsWithAllocator()` ArgIterator (argv[0], the
+    // program name, is always present).
     var has_split = false;
     var j = decl_tok + 1;
     while (j < next_period and tags[j] != .semicolon) : (j += 1) {
         if (tags[j] != .identifier) continue;
-        if (isSplitConstructor(tree.tokenSlice(j))) {
+        const nm = tree.tokenSlice(j);
+        // `argsWithAllocator` is distinctive; bare `args` only counts when it is
+        // the `process.args` method (preceded by `process .`) to avoid matching
+        // unrelated `.args` fields.
+        if (isSplitConstructor(nm) or
+            std.mem.eql(u8, nm, "argsWithAllocator") or
+            (std.mem.eql(u8, nm, "args") and j >= 2 and
+                tags[j - 1] == .period and tags[j - 2] == .identifier and
+                std.mem.eql(u8, tree.tokenSlice(j - 2), "process")))
+        {
             has_split = true;
             break;
         }
@@ -418,3 +430,26 @@ test "forced-unwrap-iterator-next: fn not starting with test still fires" {
         \\
     );
 }
+
+test "forced-unwrap-iterator-next: first next on std.process.args suppressed" {
+    try testing.expectNoFire(check,
+        \\fn run() void {
+        \\    var args = std.process.args();
+        \\    const exe = args.next().?;
+        \\    _ = exe;
+        \\}
+        \\
+    );
+}
+
+test "forced-unwrap-iterator-next: second next on args still fires" {
+    try testing.expectFires(check, R,
+        \\fn run() void {
+        \\    var args = std.process.args();
+        \\    _ = args.next();
+        \\    const second = args.next().?;
+        \\    _ = second;
+        \\}
+        \\
+    );
+}
diff --git a/src/rules/misc/index_minus_one_without_zero_guard.zig b/src/rules/misc/index_minus_one_without_zero_guard.zig
index 83ccdd9..7507e1b 100644
--- a/src/rules/misc/index_minus_one_without_zero_guard.zig
+++ b/src/rules/misc/index_minus_one_without_zero_guard.zig
@@ -219,10 +219,26 @@ pub fn check(
     if (!config_mod.isEnabled(config, .index_minus_one_without_zero_guard)) return;
     var ctx = try FileCtx.build(gpa, tree);
     defer ctx.deinit(gpa);
+
+    // Map identifier-reference nodes by main token so the type engine can
+    // resolve an index operand to a comptime value (`bytes[max_inline_len-1]`).
+    // Empty when the engine is absent.
+    var ident_nodes: std.AutoHashMapUnmanaged(Ast.TokenIndex, Ast.Node.Index) = .empty;
+    defer ident_nodes.deinit(gpa);
+    {
+        var ni: u32 = 0;
+        while (ni < tree.nodes.len) : (ni += 1) {
+            const node: Ast.Node.Index = @enumFromInt(ni);
+            if (tree.nodeTag(node) == .identifier) {
+                try ident_nodes.put(gpa, tree.nodeMainToken(node), node);
+            }
+        }
+    }
+
     var proto_buf: [1]Ast.Node.Index = undefined;
     var fns = tokens.iterFnDecls(tree);
     while (fns.next(&proto_buf)) |fn_entry| {
-        try checkBody(gpa, tree, fn_entry.body, problems, &ctx, cache);
+        try checkBody(gpa, tree, fn_entry.body, problems, &ctx, cache, &ident_nodes);
     }
 }
 
@@ -233,6 +249,7 @@ fn checkBody(
     problems: *std.ArrayListUnmanaged(Problem),
     ctx: *const FileCtx,
     cache: *file_cache_mod.FileCache,
+    ident_nodes: *const std.AutoHashMapUnmanaged(Ast.TokenIndex, Ast.Node.Index),
 ) !void {
     const tags = tree.tokens.items(.tag);
     const first = tree.firstToken(body);
@@ -271,6 +288,14 @@ fn checkBody(
             tags[t + 4] == .r_bracket)
         {
             const idx_name = tree.tokenSlice(t + 1);
+            // Semantic: a comptime-known index can't underflow at RUNTIME — a
+            // `CONST - 1` with `CONST == 0`, or an out-of-range constant
+            // subscript, is a COMPILE error.  Resolve the operand's value;
+            // any successful resolution ⇒ comptime-verified safe.  Covers
+            // `bytes[max_inline_len - 1]` (max_inline_len a const usize).
+            if (ident_nodes.get(t + 1)) |opnode| {
+                if (cache.comptimeIntValueOf(opnode) != null) continue;
+            }
             if (hasAndGuard(tags, tree, t, &.{idx_name})) continue;
             if (hasOrGuard(tags, tree, t, &.{idx_name})) continue;
             if (isInGuardedRange(guarded.items, t, &.{idx_name})) continue;
diff --git a/src/rules/misc/midpoint_addition_overflow.zig b/src/rules/misc/midpoint_addition_overflow.zig
index 79af18c..c5b83b5 100644
--- a/src/rules/misc/midpoint_addition_overflow.zig
+++ b/src/rules/misc/midpoint_addition_overflow.zig
@@ -83,19 +83,19 @@ pub fn check(
     }
 }
 
-/// True iff the identifier at `tok` resolves to a float type via the type engine.
+/// True iff the identifier at `tok` resolves to a float type via the type
+/// engine.  Floats are `simple_type`s, not containers, so `typeNameOfNode`
+/// (container-only) can never report them — `isFloatType` inspects the
+/// resolved type's InternPool key directly.  Resolves through local-variable
+/// initializers (`const start_y = metrics.face_y + …` ⇒ f64), so float
+/// midpoints written over derived locals are suppressed.
 fn operandIsFloat(
     cache: *file_cache_mod.FileCache,
     ident_nodes: *const std.AutoHashMapUnmanaged(Ast.TokenIndex, Ast.Node.Index),
     tok: Ast.TokenIndex,
 ) bool {
     const node = ident_nodes.get(tok) orelse return false;
-    const tyname = cache.typeNameOfNode(node) orelse return false;
-    return std.mem.eql(u8, tyname, "f16") or
-        std.mem.eql(u8, tyname, "f32") or
-        std.mem.eql(u8, tyname, "f64") or
-        std.mem.eql(u8, tyname, "f128") or
-        std.mem.eql(u8, tyname, "f80");
+    return cache.isFloatType(node);
 }
 
 fn report(
@@ -223,6 +223,13 @@ test "midpoint-addition-overflow: variable divisor does not fire" {
     );
 }
 
+// NOTE: the type-engine float suppression (`operandIsFloat` → `isFloatType`)
+// is validated live against the corpus, not here: the unit-test harness runs
+// token-only (no resolver), so f64-typed locals can't be distinguished from
+// integers without the engine.  The `hasFloatDecl` syntactic fallback is what
+// the tests below exercise.  Regression covered live by ghostty font/face.zig
+// (`(start_y + end_y) / 2`, start_y/end_y inferred f64 → suppressed).
+
 test "midpoint-addition-overflow: f32 pixel operands do not fire" {
     try testing.expectNoFire(check,
         \\fn encode(rgba: []const u8) void {
diff --git a/src/rules/misc/return_arraylist_items.zig b/src/rules/misc/return_arraylist_items.zig
index 0e96557..f6d0eb5 100644
--- a/src/rules/misc/return_arraylist_items.zig
+++ b/src/rules/misc/return_arraylist_items.zig
@@ -83,10 +83,51 @@ pub fn check(
             if (found_capacity) continue;
         }
 
+        // Suppress when `recv` is a POINTER parameter (`recv: *ArrayList(T)`):
+        // the caller owns the list it passed in and will `deinit` it, so the
+        // returned `.items` is an intentional borrow into the caller's own
+        // allocation — there is no orphaned backing buffer to leak.  (A by-value
+        // param could leak a post-append realloc, so only pointer params qualify.)
+        if (recvIsPointerParam(tree, t, recv)) continue;
+
         try report(gpa, problems, tree, t);
     }
 }
 
+/// True iff `recv` is a pointer-typed parameter of the function enclosing `tok`.
+fn recvIsPointerParam(tree: *const Ast, tok: Ast.TokenIndex, recv: []const u8) bool {
+    // Innermost fn_decl containing `tok` (largest firstToken).  Keep only the
+    // proto NODE — `fullFnProto` stores params in a local buf that must outlive
+    // the iteration, so resolve the proto here, not in a helper that returns it.
+    var best_proto: ?Ast.Node.Index = null;
+    var best_first: Ast.TokenIndex = 0;
+    var ni: u32 = 0;
+    while (ni < tree.nodes.len) : (ni += 1) {
+        const node: Ast.Node.Index = @enumFromInt(ni);
+        if (tree.nodeTag(node) != .fn_decl) continue;
+        const ft = tree.firstToken(node);
+        if (tok < ft or tok > tree.lastToken(node)) continue;
+        if (best_proto == null or ft > best_first) {
+            best_proto = tree.nodeData(node).node_and_node[0];
+            best_first = ft;
+        }
+    }
+    const proto_node = best_proto orelse return false;
+    var buf: [1]Ast.Node.Index = undefined;
+    const proto = tree.fullFnProto(&buf, proto_node) orelse return false;
+    var it = proto.iterate(tree);
+    while (it.next()) |p| {
+        const nt = p.name_token orelse continue;
+        if (!std.mem.eql(u8, tree.tokenSlice(nt), recv)) continue;
+        const te = p.type_expr orelse return false;
+        return switch (tree.nodeTag(te)) {
+            .ptr_type, .ptr_type_aligned, .ptr_type_bit_range, .ptr_type_sentinel => true,
+            else => false,
+        };
+    }
+    return false;
+}
+
 fn report(
     gpa: std.mem.Allocator,
     problems: *std.ArrayListUnmanaged(Problem),
@@ -175,3 +216,22 @@ test "return-arraylist-items: no capacity check still fires" {
         \\
     );
 }
+
+test "return-arraylist-items: pointer param (caller-owned) suppresses" {
+    try testing.expectNoFire(check,
+        \\fn collect(out: *std.ArrayList(u8)) []u8 {
+        \\    out.append(1) catch {};
+        \\    return out.items;
+        \\}
+        \\
+    );
+}
+
+test "return-arraylist-items: by-value param still fires (post-append realloc leaks)" {
+    try testing.expectFires(check, R,
+        \\fn collect(list: std.ArrayList(u8)) []u8 {
+        \\    return list.items;
+        \\}
+        \\
+    );
+}
diff --git a/src/rules/misc/slice_from_fixed_offset_without_len_check.zig b/src/rules/misc/slice_from_fixed_offset_without_len_check.zig
index 46f0c57..d0c038e 100644
--- a/src/rules/misc/slice_from_fixed_offset_without_len_check.zig
+++ b/src/rules/misc/slice_from_fixed_offset_without_len_check.zig
@@ -68,6 +68,7 @@ const file_cache_mod = @import("../../cache/file_cache.zig");
 
 const tokens = @import("../../ast/tokens.zig");
 const testing = @import("../../testing.zig");
+const value_range = @import("../../flow/value_range.zig");
 
 const skipNestedFn = tokens.skipNestedFn;
 
@@ -497,6 +498,11 @@ fn checkBody(
         // (Generalises the old `buf[0]`-for-offset-1 check to any offset.)
         if (offsetValue(offset_str)) |off| {
             if (provenMinLenBefore(tree, tags, first, t, buf_name) >= off) continue;
+            // Value-range oracle: `buf.len >= off` proven via a slice-length alias
+            // whose scalar has a known value (e.g. an enclosing `switch (rem_len)`
+            // arm K bounds `rem_key = b[0..rem_len]` to len K). Covers the wyhash
+            // hash-tail family `switch (rem_len) { K => rem_key[N..] }` (K >= N).
+            if (value_range.provesMinLen(gpa, tree, body, buf_name, off, t, cache)) continue;
         }
 
         // Suppression: a prefix-check guard `startsWith*/hasPrefix*(…, buf,
diff --git a/src/type_engine/analysis.zig b/src/type_engine/analysis.zig
index 4013ca7..4346dcc 100644
--- a/src/type_engine/analysis.zig
+++ b/src/type_engine/analysis.zig
@@ -1466,7 +1466,7 @@ fn resolveInternPoolValue(analyser: *Analyser, options: ResolveOptions) Error!?I
     }
 }
 
-fn resolveIntegerLiteral(analyser: *Analyser, comptime T: type, options: ResolveOptions) Error!?T {
+pub fn resolveIntegerLiteral(analyser: *Analyser, comptime T: type, options: ResolveOptions) Error!?T {
     const ip_index = try analyser.resolveInternPoolValue(options) orelse return null;
     return analyser.ip.toInt(ip_index, T);
 }
diff --git a/src/type_engine/engine.zig b/src/type_engine/engine.zig
index 95a0760..1e01b33 100644
--- a/src/type_engine/engine.zig
+++ b/src/type_engine/engine.zig
@@ -12,6 +12,7 @@
 //!                the per-file arena and Analyser.
 
 const std = @import("std");
+const builtin = @import("builtin");
 const Ast = std.zig.Ast;
 
 const DocumentStore = @import("document_store.zig");
@@ -184,7 +185,25 @@ pub const TypeResolver = struct {
         self.arena = std.heap.ArenaAllocator.init(gpa);
         errdefer self.arena.deinit();
 
-        const handle_uri: Uri = try .fromPath(self.arena.allocator(), file_path);
+        // `@import` resolution joins the imported path against the *handle's*
+        // URI, so the handle URI must be absolute.  A relative `file_path`
+        // (e.g. `find … | xargs zbc` yields CWD-relative paths) would become
+        // `file:///<relative>` → filesystem root → every relative import fails
+        // to load → cross-file types silently never resolve.  Canonicalize to
+        // an absolute path first so imports resolve regardless of CWD/argv form.
+        // Canonicalize via libc `realpath(3)`: it resolves relative inputs
+        // against CWD and follows symlinks.  `std.fs.path.resolve` does NEITHER
+        // in this Zig version (only normalises `./`/`../`), so it can't be used.
+        const aa = self.arena.allocator();
+        const abs_path: []const u8 = blk: {
+            if (std.fs.path.isAbsolute(file_path)) break :blk file_path;
+            const z = aa.dupeSentinel(u8, file_path, 0) catch break :blk file_path;
+            var resolved_buf: [std.fs.max_path_bytes]u8 = undefined;
+            const got = std.c.realpath(z.ptr, &resolved_buf) orelse break :blk file_path;
+            const len = std.mem.indexOfSentinel(u8, 0, got);
+            break :blk aa.dupe(u8, resolved_buf[0..len]) catch file_path;
+        };
+        const handle_uri: Uri = try .fromPath(aa, abs_path);
         try ctx.store.openLspSyncedDocument(handle_uri, source);
         self.handle = ctx.store.getHandle(handle_uri) orelse return error.HandleMissing;
 
@@ -279,6 +298,26 @@ pub const TypeResolver = struct {
         }
     }
 
+    /// True iff `node`'s type resolves to a floating-point type (f16/f32/f64/
+    /// f80/f128 or c_longdouble).  Floats are `simple_type`s in the InternPool,
+    /// not containers, so `typeNameOfNode` (container-only) can never report
+    /// them — rules needing "is this a float?" must use this query.  Used e.g.
+    /// to suppress integer-overflow rules on float operands (`(a + b) / 2` on
+    /// f64 cannot overflow in the integer sense).
+    pub fn isFloatType(self: *TypeResolver, node: Ast.Node.Index) !bool {
+        const ty = (try self.analyser.resolveTypeOfNode(.of(node, self.handle))) orelse return false;
+        return switch (ty.data) {
+            .ip_index => |payload| switch (self.ctx.ip.indexToKey(payload.type)) {
+                .simple_type => |st| switch (st) {
+                    .f16, .f32, .f64, .f80, .f128, .c_longdouble => true,
+                    else => false,
+                },
+                else => false,
+            },
+            else => false,
+        };
+    }
+
     pub const IntInfo = struct { signed: bool, bits: u16 };
 
     /// Signedness and bit-width of `node`'s type when it resolves to an integer
@@ -286,13 +325,20 @@ pub const TypeResolver = struct {
     /// can't "wrap to a huge value") from unsigned underflow.
     pub fn intInfo(self: *TypeResolver, node: Ast.Node.Index) !?IntInfo {
         const ty = (try self.analyser.resolveTypeOfNode(.of(node, self.handle))) orelse return null;
-        return switch (ty.data) {
-            .ip_index => |payload| switch (self.ctx.ip.indexToKey(payload.type)) {
-                .int_type => |i| .{ .signed = i.signedness == .signed, .bits = i.bits },
-                else => null,
-            },
-            else => null,
+        const idx = switch (ty.data) {
+            .ip_index => |payload| payload.type,
+            else => return null,
         };
+        // `ip.intInfo` resolves usize/isize/c_int/… (which are `simple_type`s,
+        // NOT `int_type`) plus packed-struct/enum tag widths — but it is
+        // `unreachable` on non-integers, so gate on the .int type tag first.
+        // (The earlier `.int_type`-only match returned null for usize, silently
+        // breaking every unsigned-operand query — e.g. the value-range oracle's
+        // `i > usize_var ⟹ i != 0` generalization.)
+        const tag = self.ctx.ip.zigTypeTag(idx) orelse return null;
+        if (tag != .int) return null;
+        const info = self.ctx.ip.intInfo(idx, builtin.target);
+        return .{ .signed = info.signedness == .signed, .bits = info.bits };
     }
 
     /// For `x.ptr` where `x`'s type resolves to a slice / many-pointer:
@@ -356,6 +402,15 @@ pub const TypeResolver = struct {
         return self.fixedArrayLenOfType(ty, 0);
     }
 
+    /// If `node` resolves to a comptime-known non-negative integer, return its
+    /// value, else null.  A comptime-known index can never cause a *runtime*
+    /// underflow/OOB: `CONST - 1` with `CONST == 0`, or an out-of-range constant
+    /// subscript, is a COMPILE error (never ships).  So any successful
+    /// resolution here means the access is comptime-verified safe.
+    pub fn comptimeIntValue(self: *TypeResolver, node: Ast.Node.Index) !?u64 {
+        return self.analyser.resolveIntegerLiteral(u64, .of(node, self.handle));
+    }
+
     fn fixedArrayLenOfType(self: *TypeResolver, ty: Analyser.Type, depth: u8) ?u64 {
         if (depth > 4) return null;
         return switch (ty.data) {