diff --git a/bench/elixir_mode.exs b/bench/elixir_mode.exs
new file mode 100644
index 00000000..a040236d
--- /dev/null
+++ b/bench/elixir_mode.exs
@@ -0,0 +1,479 @@
+# Elixir mode at small sizes: could the generated Elixir ever be the fast
+# side of a kernel below the crossover? Each kernel is timed three ways at
+# 16 B to 1 KiB: the native kernel, its Elixir mode (`__defk_elixir__/2`)
+# and the optimised Elixir baseline of its example. Two read-only kernels
+# (xxh64 and SipHash-2-4 from examples/hashes.exs: no array writes, the
+# best case for Elixir mode) and one that allocates and writes its output
+# (ws_mask from examples/ws_masking.exs; a write is a binary copy in Elixir
+# mode). docs/performance.md 5.14.
+#
+#   mix run bench/elixir_mode.exs [rounds]
+#
+# Each row is the median over the rounds of (ns per call over n calls),
+# rounds interleaved; the three sides of a size run in the same round.
+# Other processes' CPU is printed before each block (Defk.Bench.other_cpu/0):
+# at most one core counts as quiet. Elixir mode's numbers are an
+# exploration, never a baseline (Defk.ElixirMode).
+rounds = String.to_integer(List.first(System.argv()) || "7")
+n = 20_000
+
+defmodule EM.Kernels do
+  use Defk, elixir_mode: true
+
+  # ---- xxh64 (examples/hashes.exs) ----------------------------------------
+  @xp1 Defk.Bits.wrap64(0x9E3779B185EBCA87)
+  @xp2 Defk.Bits.wrap64(0xC2B2AE3D27D4EB4F)
+  @xp3 0x165667B19E3779F9
+  @xp4 Defk.Bits.wrap64(0x85EBCA77C2B2AE63)
+  @xp5 0x27D4EB2F165667C5
+
+  defk(rotl1(x :: i64) :: i64, do: bor(wrap64(bsl(x, 1)), band(bsr(x, 63), 0x1)))
+  defk(rotl7(x :: i64) :: i64, do: bor(wrap64(bsl(x, 7)), band(bsr(x, 57), 0x7F)))
+  defk(rotl11(x :: i64) :: i64, do: bor(wrap64(bsl(x, 11)), band(bsr(x, 53), 0x7FF)))
+  defk(rotl12(x :: i64) :: i64, do: bor(wrap64(bsl(x, 12)), band(bsr(x, 52), 0xFFF)))
+  defk(rotl18(x :: i64) :: i64, do: bor(wrap64(bsl(x, 18)), band(bsr(x, 46), 0x3FFFF)))
+  defk(rotl23(x :: i64) :: i64, do: bor(wrap64(bsl(x, 23)), band(bsr(x, 41), 0x7FFFFF)))
+  defk(rotl27(x :: i64) :: i64, do: bor(wrap64(bsl(x, 27)), band(bsr(x, 37), 0x7FFFFFF)))
+  defk(rotl31(x :: i64) :: i64, do: bor(wrap64(bsl(x, 31)), band(bsr(x, 33), 0x7FFFFFFF)))
+  defk(rotl13(x :: i64) :: i64, do: bor(wrap64(bsl(x, 13)), band(bsr(x, 51), 0x1FFF)))
+  defk(rotl16(x :: i64) :: i64, do: bor(wrap64(bsl(x, 16)), band(bsr(x, 48), 0xFFFF)))
+  defk(rotl17(x :: i64) :: i64, do: bor(wrap64(bsl(x, 17)), band(bsr(x, 47), 0x1FFFF)))
+  defk(rotl21(x :: i64) :: i64, do: bor(wrap64(bsl(x, 21)), band(bsr(x, 43), 0x1FFFFF)))
+  defk(rotl32(x :: i64) :: i64, do: bor(wrap64(bsl(x, 32)), band(bsr(x, 32), 0xFFFFFFFF)))
+  defk(shr33(x :: i64) :: i64, do: band(bsr(x, 33), 0x7FFFFFFF))
+  defk(shr29(x :: i64) :: i64, do: band(bsr(x, 29), 0x7FFFFFFFF))
+  defk(shr32(x :: i64) :: i64, do: band(bsr(x, 32), 0xFFFFFFFF))
+
+  defk(xround(acc :: i64, lane :: i64) :: i64,
+    do: wrap64(rotl31(wrap64(acc + lane * @xp2)) * @xp1)
+  )
+
+  defk(xmerge(h :: i64, v :: i64) :: i64, do: wrap64(bxor(h, xround(0, v)) * @xp1 + @xp4))
+
+  defk xxh64(b :: [u8], seed :: i64) :: i64 do
+    n = length(b)
+    stop = n
+    body = n - rem(n, 32)
+
+    h =
+      if n >= 32 do
+        {v1, v2, v3, v4} =
+          for i <- 0..(body - 32)//32,
+              reduce: {wrap64(seed + @xp1 + @xp2), wrap64(seed + @xp2), seed, wrap64(seed - @xp1)} do
+            {v1, v2, v3, v4} ->
+              {xround(v1, u64_le(b, i)), xround(v2, u64_le(b, i + 8)),
+               xround(v3, u64_le(b, i + 16)), xround(v4, u64_le(b, i + 24))}
+          end
+
+        h = wrap64(rotl1(v1) + rotl7(v2) + rotl12(v3) + rotl18(v4))
+        xmerge(xmerge(xmerge(xmerge(h, v1), v2), v3), v4)
+      else
+        wrap64(seed + @xp5)
+      end
+
+    h = wrap64(h + n)
+    words = stop - rem(stop - body, 8)
+
+    h =
+      for i <- body..(words - 8)//8, reduce: h do
+        h -> wrap64(rotl27(bxor(h, xround(0, u64_le(b, i)))) * @xp1 + @xp4)
+      end
+
+    tail4 = stop - words >= 4
+
+    h =
+      if tail4,
+        do: wrap64(rotl23(bxor(h, wrap64(u32_le(b, words) * @xp1))) * @xp2 + @xp3),
+        else: h
+
+    p = if tail4, do: words + 4, else: words
+
+    h =
+      for i <- p..(stop - 1)//1, reduce: h do
+        h -> wrap64(rotl11(bxor(h, wrap64(b[i] * @xp5))) * @xp1)
+      end
+
+    h = wrap64(bxor(h, shr33(h)) * @xp2)
+    h = wrap64(bxor(h, shr29(h)) * @xp3)
+    bxor(h, shr32(h))
+  end
+
+  # ---- SipHash-2-4 (examples/hashes.exs) ----------------------------------
+  defk le_bytes(b :: [u8], from :: i64, to :: i64) :: i64 do
+    for i <- (to - 1)..from//-1, reduce: 0 do
+      acc -> bor(bsl(acc, 8), b[i])
+    end
+  end
+
+  defk siphash24(b :: [u8], k0 :: i64, k1 :: i64) :: i64 do
+    n = length(b)
+    words = n - rem(n, 8)
+    last = bor(wrap64(bsl(band(n, 255), 56)), le_bytes(b, words, n))
+
+    {v0, v1, v2, v3} =
+      for i <- 0..words//8,
+          reduce:
+            {bxor(k0, 0x736F6D6570736575), bxor(k1, 0x646F72616E646F6D),
+             bxor(k0, 0x6C7967656E657261), bxor(k1, 0x7465646279746573)} do
+        {v0, v1, v2, v3} ->
+          m = if i < words, do: u64_le(b, i), else: last
+          v3 = bxor(v3, m)
+          v0 = wrap64(v0 + v1)
+          v1 = bxor(rotl13(v1), v0)
+          v0 = rotl32(v0)
+          v2 = wrap64(v2 + v3)
+          v3 = bxor(rotl16(v3), v2)
+          v0 = wrap64(v0 + v3)
+          v3 = bxor(rotl21(v3), v0)
+          v2 = wrap64(v2 + v1)
+          v1 = bxor(rotl17(v1), v2)
+          v2 = rotl32(v2)
+          v0 = wrap64(v0 + v1)
+          v1 = bxor(rotl13(v1), v0)
+          v0 = rotl32(v0)
+          v2 = wrap64(v2 + v3)
+          v3 = bxor(rotl16(v3), v2)
+          v0 = wrap64(v0 + v3)
+          v3 = bxor(rotl21(v3), v0)
+          v2 = wrap64(v2 + v1)
+          v1 = bxor(rotl17(v1), v2)
+          v2 = rotl32(v2)
+          {bxor(v0, m), v1, v2, v3}
+      end
+
+    {v0, v1, v2, v3} =
+      for _ <- 1..4, reduce: {v0, v1, bxor(v2, 0xFF), v3} do
+        {v0, v1, v2, v3} ->
+          v0 = wrap64(v0 + v1)
+          v1 = bxor(rotl13(v1), v0)
+          v0 = rotl32(v0)
+          v2 = wrap64(v2 + v3)
+          v3 = bxor(rotl16(v3), v2)
+          v0 = wrap64(v0 + v3)
+          v3 = bxor(rotl21(v3), v0)
+          v2 = wrap64(v2 + v1)
+          v1 = bxor(rotl17(v1), v2)
+          {v0, v1, rotl32(v2), v3}
+      end
+
+    bxor(bxor(v0, v1), bxor(v2, v3))
+  end
+
+  # ---- no loop (bench/call_cost.exs, examples/poor_tiny_calls.exs) -------
+  defk add(a :: i64, b :: i64) :: i64 do
+    a + b
+  end
+
+  defk clamp(x :: f64, lo :: f64, hi :: f64) :: f64 do
+    min(max(x, lo), hi)
+  end
+
+  # ---- ws_mask (examples/ws_masking.exs): allocates and writes ------------
+  defk ws_mask(payload :: [u8], mask :: i64) :: [u8] do
+    if mask < 0 or mask > 0xFFFFFFFF do
+      raise ArgumentError, "mask must be a 32-bit unsigned integer"
+    end
+
+    k0 = band(bsr(mask, 24), 255)
+    k1 = band(bsr(mask, 16), 255)
+    k2 = band(bsr(mask, 8), 255)
+    k3 = band(mask, 255)
+    n = length(payload)
+    out = alloc(u8, n)
+
+    for i <- 0..(div(n, 4) - 1)//1 do
+      j = 4 * i
+      out[j] = bxor(payload[j], k0)
+      out[j + 1] = bxor(payload[j + 1], k1)
+      out[j + 2] = bxor(payload[j + 2], k2)
+      out[j + 3] = bxor(payload[j + 3], k3)
+    end
+
+    for j <- (n - rem(n, 4))..(n - 1)//1 do
+      out[j] = bxor(payload[j], band(bsr(mask, 24 - 8 * rem(j, 4)), 255))
+    end
+
+    out
+  end
+end
+
+# ---- the optimised Elixir baselines (examples/hashes.exs, ws_masking.exs) ---
+
+defmodule EM.XXH64 do
+  import Bitwise
+
+  @m 0xFFFFFFFFFFFFFFFF
+  @p1 0x9E3779B185EBCA87
+  @p2 0xC2B2AE3D27D4EB4F
+  @p3 0x165667B19E3779F9
+  @p4 0x85EBCA77C2B2AE63
+  @p5 0x27D4EB2F165667C5
+
+  @compile {:inline, rotl: 2, round: 2, merge: 2}
+
+  def hash(bin, seed) do
+    seed = band(seed, @m)
+    n = byte_size(bin)
+
+    {h, rest} =
+      if n >= 32 do
+        stripes(bin, band(seed + @p1 + @p2, @m), band(seed + @p2, @m), seed, band(seed - @p1, @m))
+      else
+        {band(seed + @p5, @m), bin}
+      end
+
+    h = tail(band(h + n, @m), rest)
+    h = band(bxor(h, h >>> 33) * @p2, @m)
+    h = band(bxor(h, h >>> 29) * @p3, @m)
+    bxor(h, h >>> 32)
+  end
+
+  defp stripes(
+         <<a::little-64, b::little-64, c::little-64, d::little-64, rest::binary>>,
+         v1,
+         v2,
+         v3,
+         v4
+       ),
+       do: stripes(rest, round(v1, a), round(v2, b), round(v3, c), round(v4, d))
+
+  defp stripes(rest, v1, v2, v3, v4) do
+    h = band(rotl(v1, 1) + rotl(v2, 7) + rotl(v3, 12) + rotl(v4, 18), @m)
+    {h |> merge(v1) |> merge(v2) |> merge(v3) |> merge(v4), rest}
+  end
+
+  defp tail(h, <<k::little-64, rest::binary>>),
+    do: tail(band(rotl(bxor(h, round(0, k)), 27) * @p1 + @p4, @m), rest)
+
+  defp tail(h, <<k::little-32, rest::binary>>),
+    do: tail(band(rotl(bxor(h, band(k * @p1, @m)), 23) * @p2 + @p3, @m), rest)
+
+  defp tail(h, <<k, rest::binary>>),
+    do: tail(band(rotl(bxor(h, band(k * @p5, @m)), 11) * @p1, @m), rest)
+
+  defp tail(h, <<>>), do: h
+
+  defp rotl(x, r), do: bor(band(x <<< r, @m), x >>> (64 - r))
+  defp round(acc, lane), do: band(rotl(band(acc + lane * @p2, @m), 31) * @p1, @m)
+  defp merge(h, v), do: band(bxor(h, round(0, v)) * @p1 + @p4, @m)
+end
+
+defmodule EM.SipHash do
+  import Bitwise
+
+  @m 0xFFFFFFFFFFFFFFFF
+
+  @compile {:inline, rotl: 2, sipround: 4}
+
+  def hash(k0, k1, bin) do
+    blocks(
+      bin,
+      byte_size(bin),
+      bxor(k0, 0x736F6D6570736575),
+      bxor(k1, 0x646F72616E646F6D),
+      bxor(k0, 0x6C7967656E657261),
+      bxor(k1, 0x7465646279746573)
+    )
+  end
+
+  defp blocks(<<m::little-64, rest::binary>>, n, v0, v1, v2, v3) do
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, bxor(v3, m))
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, v3)
+    blocks(rest, n, bxor(v0, m), v1, v2, v3)
+  end
+
+  defp blocks(tail, n, v0, v1, v2, v3) do
+    m = bor(band(n, 255) <<< 56, :binary.decode_unsigned(tail, :little))
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, bxor(v3, m))
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, v3)
+    {v0, v1, v2, v3} = sipround(bxor(v0, m), v1, bxor(v2, 0xFF), v3)
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, v3)
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, v3)
+    {v0, v1, v2, v3} = sipround(v0, v1, v2, v3)
+    bxor(bxor(v0, v1), bxor(v2, v3))
+  end
+
+  defp sipround(v0, v1, v2, v3) do
+    v0 = band(v0 + v1, @m)
+    v1 = bxor(rotl(v1, 13), v0)
+    v0 = rotl(v0, 32)
+    v2 = band(v2 + v3, @m)
+    v3 = bxor(rotl(v3, 16), v2)
+    v0 = band(v0 + v3, @m)
+    v3 = bxor(rotl(v3, 21), v0)
+    v2 = band(v2 + v1, @m)
+    v1 = bxor(rotl(v1, 17), v2)
+    {v0, v1, rotl(v2, 32), v3}
+  end
+
+  defp rotl(x, r), do: bor(band(x <<< r, @m), x >>> (64 - r))
+end
+
+defmodule EM.Ws do
+  import Bitwise
+
+  # ws_masking's baseline: the 32-bit loop (Bandit's shape) below 512 B,
+  # :crypto.exor/2 with a doubled key from there
+  @threshold 512
+  def hybrid(p, m) when byte_size(p) < @threshold, do: b32(p, m, <<>>)
+  def hybrid(p, m), do: :crypto.exor(p, key(<<m::32>>, byte_size(p)))
+
+  defp b32(<<h::32, r::binary>>, m, acc), do: b32(r, m, <<acc::binary, bxor(h, m)::32>>)
+  defp b32(<<>>, _, acc), do: acc
+  defp b32(rest, m, acc), do: <<acc::binary, tail(rest, m)::bitstring>>
+
+  defp tail(rest, m) do
+    s = bit_size(rest)
+    <<h::size(^s)>> = rest
+    <<mm::size(^s), _::bitstring>> = <<m::32>>
+    <<bxor(h, mm)::size(s)>>
+  end
+
+  defp key(k, n) when byte_size(k) >= n, do: binary_part(k, 0, n)
+  defp key(k, n), do: key(<<k::binary, k::binary>>, n)
+end
+
+# ---- the measurement ---------------------------------------------------------
+
+defmodule EM.Time do
+  def loop(_f, 0), do: :ok
+
+  def loop(f, k) do
+    f.()
+    loop(f, k - 1)
+  end
+
+  def ns(f, n) do
+    {us, _} = :timer.tc(fn -> loop(f, n) end)
+    us * 1000 / n
+  end
+
+  def median(l), do: Enum.at(Enum.sort(l), div(length(l), 2))
+
+  def fmt(ns) when ns < 10_000, do: :erlang.float_to_binary(ns * 1.0, decimals: 0) <> " ns"
+  def fmt(ns), do: :erlang.float_to_binary(ns / 1000, decimals: 1) <> " us"
+
+  # interleaved: each round runs every row of every size once
+  def block(title, sizes, rows, n, rounds) do
+    IO.puts("\n#{title}  (other CPU: #{Float.round(Defk.Bench.other_cpu() * 1.0, 2)} cores)")
+
+    IO.puts(
+      "  #{String.pad_trailing("size", 8)}#{Enum.map_join(rows, fn {name, _} -> String.pad_leading(name, 16) end)}   mode/kernel  mode/Elixir"
+    )
+
+    res =
+      for _ <- 1..rounds, {size, input} <- sizes, {name, f} <- rows, reduce: %{} do
+        acc ->
+          Map.update(
+            acc,
+            {size, name},
+            [ns(fn -> f.(input) end, n)],
+            &[ns(fn -> f.(input) end, n) | &1]
+          )
+      end
+
+    for {size, _} <- sizes do
+      meds = for {name, _} <- rows, do: median(res[{size, name}])
+      [kernel, mode, elixir] = meds
+
+      IO.puts(
+        "  #{String.pad_trailing(if(is_integer(size), do: "#{size} B", else: size), 8)}#{Enum.map_join(meds, &String.pad_leading(fmt(&1), 16))}   #{String.pad_leading(:erlang.float_to_binary(mode / kernel, decimals: 1) <> "x", 11)}  #{String.pad_leading(:erlang.float_to_binary(mode / elixir, decimals: 1) <> "x", 11)}"
+      )
+    end
+  end
+end
+
+:rand.seed(:exsss, {7, 8, 9})
+sizes = for s <- [1, 8, 16, 64, 256, 1024], do: {s, :crypto.strong_rand_bytes(s)}
+seed = 0x1234_5678
+k0 = 0x0706050403020100
+k1 = 0x0F0E0D0C0B0A0908
+mask = 0x37FA213D
+
+# agreement first: the three sides give the same answer on every input
+for {_, b} <- sizes do
+  u = &Bitwise.band(&1, 0xFFFFFFFFFFFFFFFF)
+  x = EM.Kernels.xxh64(b, seed)
+  ^x = EM.Kernels.__defk_elixir__(:xxh64, [b, seed])
+  true = u.(x) == EM.XXH64.hash(b, seed)
+  s = EM.Kernels.siphash24(b, k0, k1)
+  ^s = EM.Kernels.__defk_elixir__(:siphash24, [b, k0, k1])
+  true = u.(s) == EM.SipHash.hash(k0, k1, b)
+  w = EM.Kernels.ws_mask(b, mask)
+  ^w = EM.Kernels.__defk_elixir__(:ws_mask, [b, mask])
+  ^w = EM.Ws.hybrid(b, mask)
+end
+
+IO.puts("#{rounds} rounds x #{n} calls per cell, median; mode = the kernel's Elixir mode")
+
+EM.Time.block(
+  "xxh64 (read-only)",
+  sizes,
+  [
+    {"kernel", &EM.Kernels.xxh64(&1, seed)},
+    {"Elixir mode", &EM.Kernels.__defk_elixir__(:xxh64, [&1, seed])},
+    {"Elixir (opt.)", &EM.XXH64.hash(&1, seed)}
+  ],
+  n,
+  rounds
+)
+
+EM.Time.block(
+  "siphash24 (read-only)",
+  sizes,
+  [
+    {"kernel", &EM.Kernels.siphash24(&1, k0, k1)},
+    {"Elixir mode", &EM.Kernels.__defk_elixir__(:siphash24, [&1, k0, k1])},
+    {"Elixir (opt.)", &EM.SipHash.hash(k0, k1, &1)}
+  ],
+  n,
+  rounds
+)
+
+EM.Time.block(
+  "ws_mask (alloc + writes)",
+  sizes,
+  [
+    {"kernel", &EM.Kernels.ws_mask(&1, mask)},
+    {"Elixir mode", &EM.Kernels.__defk_elixir__(:ws_mask, [&1, mask])},
+    {"Elixir (opt.)", &EM.Ws.hybrid(&1, mask)}
+  ],
+  n,
+  rounds
+)
+
+# kernels without a loop: the call is the cost (docs/performance.md 5.13),
+# so this is where Elixir mode would have its best chance against the kernel
+defmodule EM.Scalar do
+  def add(a, b), do: a + b
+  def clamp(x, lo, hi), do: min(max(x, lo), hi)
+end
+
+7 = EM.Kernels.add(3, 4)
+7 = EM.Kernels.__defk_elixir__(:add, [3, 4])
+2.5 = EM.Kernels.clamp(2.5, 1.0, 3.0)
+2.5 = EM.Kernels.__defk_elixir__(:clamp, [2.5, 1.0, 3.0])
+
+EM.Time.block(
+  "no loop (scalars in, scalar out)",
+  [{"add", {3, 4}}, {"clamp", {2.5, 1.0, 3.0}}],
+  [
+    {"kernel",
+     fn
+       {a, b} -> EM.Kernels.add(a, b)
+       {x, lo, hi} -> EM.Kernels.clamp(x, lo, hi)
+     end},
+    {"Elixir mode",
+     fn
+       {a, b} -> EM.Kernels.__defk_elixir__(:add, [a, b])
+       {x, lo, hi} -> EM.Kernels.__defk_elixir__(:clamp, [x, lo, hi])
+     end},
+    {"Elixir (opt.)",
+     fn
+       {a, b} -> EM.Scalar.add(a, b)
+       {x, lo, hi} -> EM.Scalar.clamp(x, lo, hi)
+     end}
+  ],
+  n * 10,
+  rounds
+)
diff --git a/bench/gather_layer.exs b/bench/gather_layer.exs
new file mode 100644
index 00000000..41f452ba
--- /dev/null
+++ b/bench/gather_layer.exs
@@ -0,0 +1,114 @@
+# A gather loop: which runtime checks stay in its hot loop, and what each
+# costs. A sparse layer over an [f32] weight array, with the input index of
+# each term in an [i32] array: output r is the sum over t < k of
+# w[r * k + t] * x[base + idx[r * k + t]]. The fast-path report lists every
+# check the compiler kept in the loop and the fact that would drop it;
+# the timing gives the cost per output row. docs/performance.md 6.45.
+#
+#   mix run bench/gather_layer.exs [rounds]
+#
+# Each number is the best over the rounds of the us per output row over
+# one call (n rows of k terms); other processes' CPU is printed before
+# each block (Defk.Bench.other_cpu/0): at most one core counts as quiet.
+rounds = String.to_integer(List.first(System.argv()) || "9")
+
+defmodule Gather.Kernels do
+  use Defk, report: :full
+
+  # the shape from the arrays: n rows of k terms in w, one index per term
+  defk layer(w :: [f32], idx :: [i32], x :: [f32], k :: i64, base :: i64) :: [f32] do
+    n = div(length(w), k)
+    out = alloc(f32, n)
+
+    for r <- 0..(n - 1)//1 do
+      out[r] =
+        for t <- 0..(k - 1)//1, reduce: 0.0 do
+          acc -> acc + w[r * k + t] * x[base + idx[r * k + t]]
+        end
+    end
+
+    out
+  end
+
+  # the same with the shape and the base stated by raising guards
+  defk layer_guarded(w :: [f32], idx :: [i32], x :: [f32], k :: i64, base :: i64) :: [f32] do
+    if not (k > 0 and length(idx) == length(w) and base >= 0 and base <= length(x)),
+      do: raise(ArgumentError, "shape")
+
+    n = div(length(w), k)
+    out = alloc(f32, n)
+
+    for r <- 0..(n - 1)//1 do
+      out[r] =
+        for t <- 0..(k - 1)//1, reduce: 0.0 do
+          acc -> acc + w[r * k + t] * x[base + idx[r * k + t]]
+        end
+    end
+
+    out
+  end
+
+  # the NFA study's one fact: a product of two band(_, 1) values is 0 or 1
+  defk bit_product(a :: [i64], b :: [i64]) :: i64 do
+    n = min(length(a), length(b))
+
+    for i <- 0..(n - 1)//1, reduce: 0 do
+      acc ->
+        hit = band(a[i], 1)
+        ext = band(b[i], 1)
+        acc + hit * (1 - ext)
+    end
+  end
+end
+
+defmodule Gather.Elixir do
+  # the same sum in Elixir, as the agreement reference
+  def layer(w, idx, x, k, base) do
+    n = div(byte_size(w), 4 * k)
+
+    for r <- 0..(n - 1), into: <<>> do
+      acc =
+        Enum.reduce(0..(k - 1), 0.0, fn t, acc ->
+          j = r * k + t
+          <<wv::float-32-native>> = binary_part(w, 4 * j, 4)
+          <<iv::signed-32-native>> = binary_part(idx, 4 * j, 4)
+          <<xv::float-32-native>> = binary_part(x, 4 * (base + iv), 4)
+          acc + wv * xv
+        end)
+
+      <<acc::float-32-native>>
+    end
+  end
+end
+
+:rand.seed(:exsss, {4, 5, 6})
+n = 4096
+k = 16
+m = 1024
+base = 512
+w = for _ <- 1..(n * k), into: <<>>, do: <<:rand.uniform() * 2 - 1::float-32-native>>
+idx = for _ <- 1..(n * k), into: <<>>, do: <<:rand.uniform(m) - 1::signed-32-native>>
+x = for _ <- 1..(m + base), into: <<>>, do: <<:rand.uniform() * 2 - 1::float-32-native>>
+
+ref = Gather.Elixir.layer(w, idx, x, k, base)
+^ref = Gather.Kernels.layer(w, idx, x, k, base)
+^ref = Gather.Kernels.layer_guarded(w, idx, x, k, base)
+
+Defk.Report.print(Gather.Kernels)
+
+best = fn f ->
+  Enum.min(for _ <- 1..rounds, do: elem(:timer.tc(f), 0)) / n
+end
+
+IO.puts(
+  "\n#{n} rows x #{k} terms, best of #{rounds}  (other CPU: #{Float.round(Defk.Bench.other_cpu() * 1.0, 2)} cores)"
+)
+
+for {name, f} <- [
+      {"layer", fn -> Gather.Kernels.layer(w, idx, x, k, base) end},
+      {"layer_guarded", fn -> Gather.Kernels.layer_guarded(w, idx, x, k, base) end}
+    ] do
+  IO.puts(
+    "  #{String.pad_trailing(name, 16)} #{:erlang.float_to_binary(best.(f), decimals: 3)} us per row"
+  )
+end
diff --git a/docs/adr/0007-symbolic-bounds.md b/docs/adr/0007-symbolic-bounds.md
index 92e87adf..884b157d 100644
--- a/docs/adr/0007-symbolic-bounds.md
+++ b/docs/adr/0007-symbolic-bounds.md
@@ -26,7 +26,9 @@ Replace the fact model with one representation:
 
 - **Atoms** are the C variables of i64 bindings and the lengths of array
   bindings, ranked by binding order (`fresh/2`'s counter; parameters
-  first).
+  first, in declaration order, carried in the facts scope since
+  `defk-w8r.3`: before that they ranked by name, so a guard between two
+  parameters could land on the wrong one).
 - **Facts** are `q * x <= P` and `q * x >= P` for an atom or a product of
   two atoms `x`, with `q >= 1` and `P` a polynomial of degree at most 2 over
   atoms ranked below `x`, plus the constant `lo`/`hi` kept as they are.
@@ -90,7 +92,9 @@ Replace the fact model with one representation:
   past the ceiling. Each statement's reads walked once (`defk-o08.4`, 6.40)
   took 8.6% more off: +7.4% of the work before step 1 (-1.0% without
   `SatEx.Kernels`), under the ceiling again. The report's hint search only
-  under `report: :full` (`defk-o08.5`, 6.41): +3.5% (-2.2%).
+  under `report: :full` (`defk-o08.5`, 6.41): +3.5% (-2.2%). Parameters
+  ranked in declaration order instead of by name (`defk-w8r.3`, 6.45):
+  +0.5% (+0.3%); the chain at about +4.0% (-1.9%).
 - **Raising guards become the way to state facts about arguments** in a
   kernel, which the language docs would describe.
 - **Out of scope:** degree 3 and nested products, facts across loop
diff --git a/docs/language.md b/docs/language.md
index d4487cb2..a2791886 100644
--- a/docs/language.md
+++ b/docs/language.md
@@ -2171,6 +2171,14 @@ that does not raise says, by the rules for [conditions](#reading):
 `if n != len, do: raise(...)` gives `n == len`; `if a and b, do: raise(...)`
 gives nothing, as `not a or not b` names no single fact.
 
+A condition between two arguments bounds the one declared later by the
+earlier one. In `defk gather(idx :: [i32], x :: [f32], base :: i64)`, the
+guard `if base < 0 or base > length(x), do: raise(...)` bounds `base`, so
+`base + idx[i]` needs no overflow check (an `[i32]` element is within
+32 bits). Declared as `(base :: i64, x :: [f32])`, the same guard bounds
+the length of `x` by `base` instead, which proves nothing about `base`:
+declare an offset after the array it is compared with.
+
 ### Blocks
 
 Every block that needs a value ends in an expression; an empty block is
diff --git a/docs/performance.md b/docs/performance.md
index c24ee8a7..aa81d869 100644
--- a/docs/performance.md
+++ b/docs/performance.md
@@ -1553,6 +1553,69 @@ which the BEAM's own NIF call and the term decoding are 6.
 - **Source:** `defk-25s`, [`bench/call_cost.exs`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost.exs), [`bench/call_cost_nif.c`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost_nif.c); `defk_now_us` in [`priv/defk_runtime.h`](https://github.com/DanielLuning/defk/blob/main/priv/defk_runtime.h).
 - **Status:** measured.
 
+### 5.14 Elixir mode is never the fast side of a kernel: 7-110x the kernel at 1-16 B, and a 220-250 ns floor per call
+
+defk compiles each kernel to Elixir as well as C (Elixir mode, the test
+oracle), so could a call switch to that Elixir below the crossover size,
+where the kernel's call cost still outweighs its work? Measured once, to
+close the question: no. Elixir mode's per-call floor is 10x a kernel call,
+and its loops are slower than the optimised Elixir an example compares the
+kernel against. The rule stands: Elixir mode is never a fallback in
+production and never a baseline (`Defk.ElixirMode`, CONTEXT.md); these
+numbers are an exploration, not a baseline.
+
+- **Numbers** (ns per call, median of 7 interleaved rounds of 20,000 calls,
+  two runs; kernel / Elixir mode / optimised Elixir, then Elixir mode over
+  each):
+
+  | kernel | size | kernel | Elixir mode | Elixir (opt.) | mode/kernel | mode/Elixir |
+  |---|---|---|---|---|---|---|
+  | `xxh64` (read-only) | 1 B | 36 | 603 | 178 | 17x | 3.4x |
+  | | 16 B | 36 | 875 | 350 | 24x | 2.5x |
+  | | 256 B | 48 | 5,363 | 2,882 | 112x | 1.9x |
+  | | 1 KiB | 80 | 18,100 | 9,437 | 227x | 1.9x |
+  | `siphash24` (read-only) | 1 B | 40 | 3,002 | 1,717 | 76x | 1.7x |
+  | | 16 B | 42 | 4,745 | 2,913 | 112x | 1.6x |
+  | | 256 B | 110 | 32,800 | 20,500 | 298x | 1.6x |
+  | | 1 KiB | 345 | 125,700 | 77,700 | 364x | 1.6x |
+  | `ws_mask` (alloc + writes) | 1 B | 83 | 566 | 82 | 6.8x | 6.9x |
+  | | 16 B | 87 | 3,070 | 65 | 36x | 47x |
+  | | 256 B | 123 | 36,600 | 268 | 299x | 137x |
+  | | 1 KiB | 233 | 145,500 | 707 | 624x | 206x |
+  | `add` (no loop) | | 17 | 248 | 3 | 15x | 79x |
+  | `clamp` (no loop) | | 19 | 222 | 5 | 12x | 48x |
+
+  The second run repeats every cell within a few percent (`xxh64` 1 B: 35 /
+  623 / 190; `siphash24` 1 KiB: 353 / 125,900 / 76,000; `ws_mask` 1 KiB:
+  231 / 150,000 / 716; `add` 17 / 254 / 3). The sizes 8 and 64 B lie
+  between their neighbours in both runs.
+- **Where the time goes.** The floor is the entry: `__defk_elixir__/2`
+  checks every argument's type (`Ops.args!`), reads the native library's
+  owned-buffer budget through the `__defk_stats__` NIF, and runs the body
+  under a process-dictionary budget (`Ops.owned_call`); each integer
+  operation then goes through a range-checked helper (`Ops.add`). A loop
+  over a read-only array costs 1.6-3.4x the optimised Elixir: each element
+  read is a helper call with a bounds check, where the Elixir baseline
+  matches eight bytes at a time. A write is `Ops.put_u8(out, j, v)`: a new
+  binary per write, so a loop of n writes copies n bytes n times, and
+  `ws_mask` at 1 KiB is 206x the Elixir loop and 624x the kernel.
+- **The switch does not exist.** The ticket's test for a decision ticket
+  was Elixir mode within ~2x of the optimised Elixir at small sizes, which
+  the two read-only hashes meet from 64 B up (1.6-1.9x). But a size-based
+  switch would replace the kernel call, and the kernel is 7-17x faster than
+  Elixir mode at 1 B, 12-15x on a kernel with no loop at all, where the call
+  is the whole cost (5.13): there is no size at which the generated Elixir
+  is the fast side. No decision ticket is filed. What beats a kernel below
+  the crossover is the hand-written Elixir of the example, as before.
+- **Conditions:** M-series Mac, 12 schedulers, OTP 29, Elixir 1.20.2, on
+  battery; other processes at 0.3-0.9 cores before each block (one block of the
+  first run at 1.3, repeated at 0.9) (the ps
+  quiet test).
+- **Source:** `defk-vcx.2`, [`bench/elixir_mode.exs`](https://github.com/DanielLuning/defk/blob/main/bench/elixir_mode.exs) (the kernels and
+  baselines of `hashes.exs` and `ws_masking.exs`, and `bench/call_cost.exs`'
+  no-loop kernels); the rule: `defk-dtw.6`.
+- **Status:** measured.
+
 ---
 
 ## 6. Making a defk kernel fast
@@ -2893,6 +2956,83 @@ s[0] = a * b        # the write rounds to float32 (raises if the value does not
 p = s[0]            # read back the rounded value as f64
 ```
 
+### 6.45 Gather loops: a guard now bounds the parameter declared later, which drops the offset's overflow check; the rest of the checks are about contents
+
+A sparse layer gathers an input per term: `out[r] = sum of w[r * k + t] *
+x[base + idx[r * k + t]]` over an `[f32]` weight array, `[i32]` indices
+and an `[f32]` input (`bench/gather_layer.exs`, `layer/5`; the guarded
+twin states `k > 0`, `length(idx) == length(w)` and `0 <= base <=
+length(x)` as a raising guard). The handwired study (`defk-w8r.2`, 6.43 and 6.44; its
+prototype is deleted, and its numbers are the reference point only) had its layer at 0.378
+us per item against 0.069 us for the hand-written C float loop, and listed
+the checks in each term. Read again on today's compiler, most of that list
+was already gone, one proof was missing for a reason of ranking, and what
+stays is about array contents.
+
+- **The checks in the hot loop, per term** (the fast-path report, `use
+  Defk, report: :full`; the guarded kernel unless said otherwise):
+
+  | check | before | after | why |
+  |---|---|---|---|
+  | `r * k`, `r * k + t`: overflow | dropped | dropped | the loop bounds and the product rule (6.37) |
+  | `w[r * k + t]`: bounds | dropped | dropped | `n = div(length(w), k)` (6.37) |
+  | `idx[r * k + t]`: bounds | dropped with the guard (kept without: "it would follow from k * n <= length(idx)") | the same | `length(idx) == length(w)` |
+  | `base + idx[...]`: overflow | **kept**, with or without the guard | **dropped** with the guard | the guard's `base <= length(x)` now bounds `base`; an `[i32]` element is within 32 bits |
+  | `x[base + idx[...]]`: bounds | kept | kept | depends on `idx`'s contents; ADR-0007 states no facts about contents |
+  | `w[...]`, `x[...]`: finite read (`defk_in_f64`) | kept | kept | an input `[f32]` may hold inf or NaN bits |
+  | `w * x`, `acc + ...`: non-finite result | kept | kept | float values have no facts |
+  | `out[r] = acc`: f32 range (`defk_to_f32`), once per row | kept | kept | the same |
+  | `n - 1`, `k - 1`: overflow (loop headers, once) | dropped with the guard | the same | `k > 0`, `n = div(...)` |
+
+  The NFA study's one fact, a product of two `band(_, 1)` values: `hit *
+  (1 - ext)` had no overflow check before this change either (`band`'s
+  facts give 0..1, the product rule multiplies the ranges); the
+  accumulator's add keeps its check (facts across iterations are out of
+  ADR-0007's scope). The inner loop runs flagged in both kernels: every
+  kept check sets a flag tested once per strip (6.5), so each costs an
+  operation and an or, not a branch, and clang reports the loop as not
+  vectorised for its in-order float reduction, not for a check.
+- **What blocked the one proof.** Facts are stated on the newest atom of a
+  condition, and parameters ranked by their C names (`p_base` before
+  `p_x`), so `base <= length(x)` was stored as a lower bound on `length(x)`
+  and said nothing about `base`. Parameters now rank in declaration order
+  (the design's "parameters first, by position"), carried in the facts
+  scope, so the guard bounds `base` and `base + idx[j]` is within
+  `length(x) + 2^31`. The rule to know: a condition between two arguments
+  bounds the one declared later, so declare an offset after the array it
+  is compared with (docs/language.md, raising guards).
+- **The gate** (`mix dump_c` on both sides, 113 modules): one module's C
+  changed, `Defk.ProductFactsTest.K`, which lost one range-limit test on a
+  loop bound (`dim`, now bounded by its guard); no kernel gained a check.
+  The catalog's bounds (3,301) and overflow (6,050) call sites are
+  unchanged: no example kernel has a guard between two parameters in the
+  wrong name order. The report's hint for a product now names the factors
+  in declaration order (`n * dim <= length(m)`, was `dim * n`).
+- **Run time** (`bench/gather_layer.exs`, 4,096 rows of 16 terms, best of
+  9, us per row, two interleaved runs a side): the unguarded kernel, whose C
+  did not change, 0.018 / 0.018 on `main` (one first run 0.023) and 0.018
+  / 0.018 on the branch; the guarded kernel 0.018 / 0.014 on `main` and
+  0.012 / 0.012 on the branch, about 0.75 ns per term where it was
+  0.9-1.1. So the one dropped check is worth 15-30% of this loop, and the
+  loop is now 1.5x the unguarded one. Against the prototype's 0.378 us
+  per item (a different kernel on a loaded machine) nothing is comparable;
+  the hand-written C of that study is gone with it.
+- **Compiler time** (two interleaved `mix dump_c` rounds a side,
+  `dev/compile_time.exs`): +0.5% of
+  the compiler's work (reductions; +0.3% without `SatEx.Kernels`, which
+  dominates the prover's cost), +0.8% of its time (-0.3% without), with
+  `SatEx.Kernels` +0.29M reductions. The chain of ADR-0007 is at about
+  +4.0% of the work before step 1 (-1.9% without `SatEx.Kernels`), under
+  its ceiling.
+- **Conditions:** M-series Mac, on battery; other processes at 0.1-0.7 cores before
+  each timed run (the ps quiet test); the compiler-time rounds on the same
+  machine, one job at a time.
+- **Source:** `defk-w8r.3`, [`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs); the proof's
+  tests: `test/condition_facts_test.exs` ("a guard between two
+  parameters": the gather with both name orders, the extremes of the
+  dropped check, and the agreement properties).
+- **Status:** measured.
+
 ---
 
 ## 7. When a hand-written or wrapper NIF is still the answer
@@ -3169,6 +3309,7 @@ costs as much as the splits.
 | Tiling helps a matrix multiply kernel | no faster at 64 to 1024 | 6.9 |
 | Yielding costs throughput | ~0% after reducible resume (one loaded run disagrees) | 6.4 |
 | `-ffp-contract=off` makes float kernels slow | no measurable cost on dot, sum, mean_var | 6.6 |
+| The generated Elixir (Elixir mode) could serve calls below the crossover | 7-17x slower than the kernel at 1 B, 12-15x on a kernel with no loop; its entry alone is ~230 ns | 5.14 |
 
 ### 8.2 Open questions
 
@@ -3235,4 +3376,6 @@ example or close a workload ticket, add its entries and its line here.
   `defk-ulk.4`, `defk-52v.15` ([`cdcl_sat.exs`](https://github.com/DanielLuning/defk/blob/main/examples/cdcl_sat.exs)), `defk-tif`, `defk-gqk`, `defk-6ag`,
   `defk-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`,
   `defk-o08.2`, `defk-o08.3`, `defk-o08.4`, `defk-o08.5`, `defk-o08.6`,
-  `defk-w8r.2`, `defk-25s` ([`bench/call_cost.exs`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost.exs)).
+  `defk-w8r.2`, `defk-25s` ([`bench/call_cost.exs`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost.exs)),
+  `defk-vcx.2` ([`bench/elixir_mode.exs`](https://github.com/DanielLuning/defk/blob/main/bench/elixir_mode.exs)),
+  `defk-w8r.3` ([`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs)).
diff --git a/lib/defk/compiler.ex b/lib/defk/compiler.ex
index 42dd683b..138dee5e 100644
--- a/lib/defk/compiler.ex
+++ b/lib/defk/compiler.ex
@@ -718,9 +718,12 @@ defmodule Defk.Compiler do
         {p, Map.merge(val(c, t, c), array_ids(t))}
       end)
 
+    # the parameters rank in declaration order (Defk.Facts, the scope)
+    scope = Facts.scope(for {p, _} <- k.params, do: vars[p].c)
+
     env = %{
       vars: vars,
-      facts: Enum.reduce(vars, Facts.scope(), fn {_, b}, s -> Facts.bind(s, b) end),
+      facts: Enum.reduce(vars, scope, fn {_, b}, s -> Facts.bind(s, b) end),
       sigs: sigs,
       inlining: [{k.name, k.arity}],
       ret: k.ret,
@@ -2294,7 +2297,7 @@ defmodule Defk.Compiler do
       case op do
         :+ -> {"add", Facts.add_facts(va, vb), Facts.add_range(va, vb)}
         :- -> {"sub", Facts.sub_facts(va, vb), Facts.sub_range(va, vb)}
-        :* -> {"mul", Facts.mul_facts(va, vb), Facts.mul_range(va, vb)}
+        :* -> {"mul", Facts.mul_facts(va, vb, env.facts), Facts.mul_range(va, vb)}
       end
 
     v = Facts.put(val(nil, :i64), facts)
@@ -6358,7 +6361,7 @@ defmodule Defk.Compiler do
         nil
 
       map_size(d.t) == 1 ->
-        case Facts.narrowing(d) do
+        case Facts.narrowing(d, env.facts) do
           {x, :lo, b} -> "#{names[x]} >= #{b}"
           {x, :hi, b} -> "#{names[x]} <= #{b}"
         end
diff --git a/lib/defk/facts.ex b/lib/defk/facts.ex
index fe4b80d8..8d9136dc 100644
--- a/lib/defk/facts.ex
+++ b/lib/defk/facts.ex
@@ -111,9 +111,17 @@ defmodule Defk.Facts do
   # {:len, c}). The compiler's env carries it and it is lexical like the
   # env; a binding's value keeps the same facts as its entry. An entry
   # outlives a shadowing binding, as the C variable is assigned once where
-  # it is in scope.
+  # it is in scope. The scope also holds the kernel's parameter order under
+  # @order (the C names in declaration order, each with its position),
+  # which ranks the parameter atoms (rank/2): a condition between two
+  # parameters then states its fact on the later one, as it does for two
+  # bindings. A scope made with no parameters ranks them by name.
 
-  def scope, do: %{}
+  @order :order
+
+  def scope(params \\ []), do: %{@order => Map.new(Enum.with_index(params))}
+
+  defp order(scope), do: Map.get(scope, @order, %{})
 
   # the scope with binding v's facts
   def bind(scope, %{t: :i64, c: c} = v), do: Map.put(scope, c, facts(v))
@@ -129,7 +137,7 @@ defmodule Defk.Facts do
     rel
     |> holds(true?)
     |> Enum.reduce(scope, fn d, scope ->
-      {x, kind, b} = narrowing(d)
+      {x, kind, b} = narrowing(d, scope)
       c = binding_of(x)
       Map.put(scope, c, with_fact(facts_of(scope, c), x, kind, b))
     end)
@@ -310,11 +318,11 @@ defmodule Defk.Facts do
   defp negated_op(op),
     do: %{<: :>=, <=: :>, >: :<=, >=: :<, ==: :!=, ===: :!==, !=: :==, !==: :===}[op]
 
-  # D <= 0 as a fact on D's newest monomial x, over older ones only:
-  # {x, :lo | :hi, constant} when the rest of D is a constant, else
-  # {x, :lb | :ub, {q, form}}
-  def narrowing(%{t: t} = d) when map_size(t) > 0 do
-    {x, c} = newest(t)
+  # D <= 0 as a fact on D's newest monomial x (by the scope's ranking), over
+  # older ones only: {x, :lo | :hi, constant} when the rest of D is a
+  # constant, else {x, :lb | :ub, {q, form}}
+  def narrowing(%{t: t} = d, scope) when map_size(t) > 0 do
+    {x, c} = newest(t, order(scope))
     rest = %{d | t: Map.delete(t, x)}
     const? = map_size(rest.t) == 0
 
@@ -480,7 +488,7 @@ defmodule Defk.Facts do
          do: form,
          else: best
 
-    {x, c} = newest(form.t)
+    {x, c} = newest(form.t, lookup.(:order))
     rest = %{form | t: Map.delete(form.t, x)}
     {lo, hi, lbs, ubs, fx} = mono(x, lookup)
     stated = if state == :tainted, do: :tainted, else: :ok
@@ -509,8 +517,10 @@ defmodule Defk.Facts do
   # An atom's facts: array a's own (the one a proof is about), else its
   # binding's in scope, else none. A binding's exact form is never its own
   # atom (bound/1 records the value's), so it is a bound over older atoms.
+  # Asked :order, it gives the scope's parameter order (rank/2).
   defp lookup(scope, a) do
     fn
+      :order -> order(scope)
       {:len, c} when a != nil and c == a.c -> facts(a)
       {_, c} -> facts_of(scope, c)
     end
@@ -560,7 +570,7 @@ defmodule Defk.Facts do
   defp le?(_form, _lookup, 0, _support), do: {false, 0}
 
   defp le?(form, lookup, budget, support) do
-    {x, c} = newest(form.t)
+    {x, c} = newest(form.t, lookup.(:order))
     rest = %{form | t: Map.delete(form.t, x)}
     {lo, hi, lbs, ubs, _} = mono(x, lookup)
 
@@ -605,7 +615,7 @@ defmodule Defk.Facts do
 
   # a monomial's constant range and relative bounds, and an atom's facts:
   # {lo, hi, lbs, ubs, facts or nil}
-  defp mono({:mul, y, z}, lookup), do: product(y, z, lookup.(y), lookup.(z))
+  defp mono({:mul, y, z}, lookup), do: product(y, z, lookup.(y), lookup.(z), lookup.(:order))
 
   defp mono({:len, _} = x, lookup) do
     f = lookup.(x)
@@ -625,7 +635,7 @@ defmodule Defk.Facts do
   # product), y's stated constant bounds among them. A bound of y of degree
   # 2 would give degree 3 and is left out. The product's constant range is
   # the factors' multiplied.
-  defp product(y, z, fy, fz) do
+  defp product(y, z, fy, fz, order) do
     {zlo, zhi} = zr = monomial_range(z, fz)
     yr = monomial_range(y, fy)
     {ylbs, yubs} = monomial_bounds(y, fy)
@@ -635,8 +645,8 @@ defmodule Defk.Facts do
 
     {lbs, ubs} =
       cond do
-        zlo >= 0 -> {times(lows, z), times(highs, z)}
-        zhi <= 0 -> {times(highs, z), times(lows, z)}
+        zlo >= 0 -> {times(lows, z, order), times(highs, z, order)}
+        zhi <= 0 -> {times(highs, z, order), times(lows, z, order)}
         true -> {[], []}
       end
 
@@ -653,8 +663,8 @@ defmodule Defk.Facts do
   defp const_bound(k), do: [{1, form_const(k)}]
 
   # bounds {q, p} on y as bounds on y * z (the caller picks the direction)
-  defp times(bounds, z),
-    do: for({q, p} <- bounds, degree(p) <= 1, do: {q, form_mul(p, form_mono(z))})
+  defp times(bounds, z, order),
+    do: for({q, p} <- bounds, degree(p) <= 1, do: {q, form_mul(p, form_mono(z), order)})
 
   # a monomial's constant bounds: a length is always in 0..2^61 - 1, an i64
   # in -2^63..2^63 - 1
@@ -674,21 +684,21 @@ defmodule Defk.Facts do
   defp support_of({:mul, {_, a}, {_, b}}, support), do: [a, b | support]
   defp support_of({_, c}, support), do: [c | support]
 
-  # the newest monomial is replaced first: parameters are the oldest, then
-  # the bindings in fresh/2's order (their C names carry its counter); a
-  # product ranks with its newer factor, before that factor alone, then by
-  # its older factor
+  # the newest monomial is replaced first: parameters are the oldest, in
+  # declaration order (`order`, the scope's; by name in a scope that holds
+  # none), then the bindings in fresh/2's order (their C names carry its
+  # counter); a product ranks with its newer factor, before that factor
+  # alone, then by its older factor
   # the newest monomial of a form's terms and its coefficient (one term
   # needs no ranking)
-  defp newest(t) when map_size(t) == 1, do: hd(Map.to_list(t))
-  defp newest(t), do: Enum.max_by(t, fn {m, _} -> rank(m) end)
+  defp newest(t, _order) when map_size(t) == 1, do: hd(Map.to_list(t))
+  defp newest(t, order), do: Enum.max_by(t, fn {m, _} -> rank(m, order) end)
 
-  defp rank({:mul, x, y}), do: {atom_rank(x), 1, atom_rank(y)}
-  defp rank({_, "p_" <> _ = c}), do: {{0, c}, 0, 0}
-  defp rank({_, c}), do: {counter(c, byte_size(c), 0, 1), 0, 0}
+  defp rank({:mul, x, y}, order), do: {atom_rank(x, order), 1, atom_rank(y, order)}
+  defp rank(a, order), do: {atom_rank(a, order), 0, 0}
 
-  defp atom_rank({_, "p_" <> _ = c}), do: {0, c}
-  defp atom_rank({_, c}), do: counter(c, byte_size(c), 0, 1)
+  defp atom_rank({_, "p_" <> _ = c}, order), do: {0, Map.get(order, c, c)}
+  defp atom_rank({_, c}, _order), do: counter(c, byte_size(c), 0, 1)
 
   # the number after the last "_" of c, read from the end: {1, n}, or
   # {0, c} for a name without one
@@ -878,8 +888,8 @@ defmodule Defk.Facts do
   # a product: lo..hi from the operands' (nil when one is unbounded), and
   # for a constant k >= 1 times v, v's facts scaled by k; the exact form is
   # the operands' multiplied while it stays of degree 2 (`r * dim`,
-  # `(n - 1) * m`), none beyond
-  def mul_facts(a, b) do
+  # `(n - 1) * m`), none beyond; the scope ranks the product's factors
+  def mul_facts(a, b, scope \\ %{}) do
     {fa, fb} = {facts(a), facts(b)}
 
     f =
@@ -899,7 +909,7 @@ defmodule Defk.Facts do
       case {const(a), const(b)} do
         {k, _} when is_integer(k) -> (e = eq(b)) && form_scale(e, k)
         {_, k} when is_integer(k) -> (e = eq(a)) && form_scale(e, k)
-        _ -> both(eq(a), eq(b), &form_mul/2)
+        _ -> both(eq(a), eq(b), &form_mul(&1, &2, order(scope)))
       end
 
     %{f | eq: eq}
@@ -1113,15 +1123,16 @@ defmodule Defk.Facts do
     end)
   end
 
-  # the product of two forms, or nil when it would be of degree 3 or more
-  def form_mul(%{t: ta} = a, b) when map_size(ta) == 0, do: form_scale(b, a.k)
-  def form_mul(a, %{t: tb} = b) when map_size(tb) == 0, do: form_scale(a, b.k)
+  # the product of two forms, or nil when it would be of degree 3 or more;
+  # `order` ranks the factors of each product monomial
+  def form_mul(%{t: ta} = a, b, _order) when map_size(ta) == 0, do: form_scale(b, a.k)
+  def form_mul(a, %{t: tb} = b, _order) when map_size(tb) == 0, do: form_scale(a, b.k)
 
-  def form_mul(a, b) do
+  def form_mul(a, b, order) do
     if degree(a) + degree(b) <= 2 do
       cross =
         for {x, cx} <- a.t, {y, cy} <- b.t, reduce: form_const(0) do
-          acc -> form_add(acc, %{k: 0, t: %{mul_mono(x, y) => cx * cy}})
+          acc -> form_add(acc, %{k: 0, t: %{mul_mono(x, y, order) => cx * cy}})
         end
 
       form_add(form_scale(%{a | k: 0}, b.k), form_scale(%{b | k: 0}, a.k))
@@ -1131,7 +1142,8 @@ defmodule Defk.Facts do
   end
 
   # the product of two atoms, its newer factor first
-  defp mul_mono(x, y), do: if(atom_rank(x) >= atom_rank(y), do: {:mul, x, y}, else: {:mul, y, x})
+  defp mul_mono(x, y, order),
+    do: if(atom_rank(x, order) >= atom_rank(y, order), do: {:mul, x, y}, else: {:mul, y, x})
 
   def form_scale(form, 1), do: form
   def form_scale(_form, 0), do: form_const(0)
diff --git a/test/condition_facts_test.exs b/test/condition_facts_test.exs
index a2fb6a79..5532438f 100644
--- a/test/condition_facts_test.exs
+++ b/test/condition_facts_test.exs
@@ -138,6 +138,30 @@ defmodule Defk.ConditionFactsTest.K do
       acc -> if i + k >= 0 and i + k < length(x), do: acc + x[i + k], else: acc
     end
   end
+
+  # A guard between two parameters states its fact on the one declared
+  # later, whatever their names: base <= length(x) bounds base (declared
+  # after x), so base + idx[i], an i32 element, fits i64 with no check. The
+  # gather x[base + idx[i]] keeps its bounds check: it depends on the
+  # array's contents.
+  defk gather(idx :: [i32], x :: [f32], base :: i64) :: f64 do
+    if not (base >= 0 and base <= length(x)), do: raise(ArgumentError, "base")
+
+    for i <- 0..(length(idx) - 1)//1, reduce: 0.0 do
+      acc -> acc + x[base + idx[i]]
+    end
+  end
+
+  # the same with the offset's name sorting after the array's: the same
+  # proof (a guard bounds the parameter declared later, never the earlier
+  # one: declared before the array, `off` would keep its check)
+  defk gather_named(ia :: [i32], as :: [f32], off :: i64) :: f64 do
+    if not (off >= 0 and off <= length(as)), do: raise(ArgumentError, "off")
+
+    for i <- 0..(length(ia) - 1)//1, reduce: 0.0 do
+      acc -> acc + as[off + ia[i]]
+    end
+  end
 end
 
 # the same unguarded kernel without report: :full: its note names no fact
@@ -183,6 +207,7 @@ defmodule Defk.ConditionFactsTest do
   defp kept(kernel), do: kept_bounds(K, kernel)
 
   defp f64s(xs), do: G.pack(:f64, Enum.map(xs, &(&1 * 1.0)))
+  defp f32s(xs), do: G.pack(:f32, Enum.map(xs, &(&1 * 1.0)))
 
   describe "a raising guard and an if arm: a rolling window" do
     test "x[i - w] keeps no bounds check after a raise when w < 1" do
@@ -315,6 +340,39 @@ defmodule Defk.ConditionFactsTest do
     end
   end
 
+  describe "a guard between two parameters" do
+    @i32_max 0x7FFFFFFF
+    @i32_min -0x80000000
+
+    # the parameters rank in declaration order, so the guard's fact lands on
+    # the later one whichever name sorts first
+    for {kernel, sum} <- [{:gather, "base + idx[i]"}, {:gather_named, "off + ia[i]"}] do
+      test "#{kernel}: the offset plus an i32 element needs no overflow check" do
+        assert {:dropped, "#{unquote(sum)}: no overflow check"} in notes(unquote(kernel), :check)
+        # the gather itself depends on the indices: its check stays
+        assert [text] = kept(unquote(kernel))
+        assert text =~ "bounds check kept; nothing proves 0 <= #{unquote(sum)}"
+
+        x = f32s(Enum.to_list(1..8))
+
+        for idx <- [[], [0], [7, 0, 3], [-1], [8]], base <- [0, 1, 8] do
+          assert {_, _} = agrees(unquote(kernel), [G.pack(:i32, idx), x, base])
+        end
+
+        # the extremes of the dropped check: the sum fits, the access raises
+        for idx <- [@i32_max, @i32_min], base <- [0, 8] do
+          assert {:raise, %Enum.OutOfBoundsError{}} =
+                   agrees(unquote(kernel), [G.pack(:i32, [idx]), x, base])
+        end
+
+        for base <- [-1, 9, @i64_min, @i64_max] do
+          assert {:raise, %ArgumentError{}} =
+                   agrees(unquote(kernel), [G.pack(:i32, [0]), x, base])
+        end
+      end
+    end
+  end
+
   describe "flagged strips" do
     test "a guard on a value the strip computes with a check makes no access fixed" do
       c = kernel_c(K, "guarded_shift")
@@ -359,7 +417,9 @@ defmodule Defk.ConditionFactsTest do
     shift_add: [args: StreamData.fixed_list([G.array(:i64), G.array(:i64), G.i64(-3..20)])],
     shift_add_unguarded: [
       args: StreamData.fixed_list([G.array(:i64), G.array(:i64), G.i64(-3..20)])
-    ]
+    ],
+    gather: [args: StreamData.fixed_list([G.array(:i32), G.array(:f32), G.i64(-3..20)])],
+    gather_named: [args: StreamData.fixed_list([G.array(:i32), G.array(:f32), G.i64(-3..20)])]
   ])
 
   # ------------------------------------------------------ soundness --
diff --git a/test/product_facts_test.exs b/test/product_facts_test.exs
index cb22b504..3b7db531 100644
--- a/test/product_facts_test.exs
+++ b/test/product_facts_test.exs
@@ -207,7 +207,7 @@ defmodule Defk.ProductFactsTest do
     test "without the shape, the report names the product's bound" do
       assert kept(:unshaped) == [
                "m[r * dim + j]: bounds check kept; nothing proves r * dim + j < length(m) " <>
-                 "(it would follow from dim * n <= length(m))"
+                 "(it would follow from n * dim <= length(m))"
              ]
     end
   end