defk-w8r.3: rank parameters in declaration order, so a guard between two arguments bounds the later one

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

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

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

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)).

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