defk-o08.5: the report's hint search runs only under report: :full; DEFK_DUMP_C dumps each module's report

CHANGELOG.md

@@ -87,8 +87,9 @@
   the body of a range that runs, and after a raising guard,
   `if w < 1, do: raise(ArgumentError, "...")`. docs/language.md now
   recommends raising guards for what a kernel needs of its arguments. When
-  a check stays, the fast-path report names a small fact that would drop
-  it: `nothing proves i - w < length(x) (it would follow from w >= 0)`. An
+  a check stays, the fast-path report of a module with `report: :full`
+  names a small fact that would drop it:
+  `nothing proves i - w < length(x) (it would follow from w >= 0)`. An
   `if` value whose arm relies on its condition to drop a check is a branch,
   not a select. Results are unchanged.
 - Faster: a row-major index with a runtime row length, `m[r * dim + j]`,

docs/adr/0007-symbolic-bounds.md

@@ -87,7 +87,10 @@ Replace the fact model with one representation:
   The compiler is at about +29% of its time before step 1, past the
   ceiling; the next step cuts first. The copy analysis's one pass per arm
   (`defk-o08.3`, 6.39) took 9% off: +17.6% of the work before step 1, still
-  past the ceiling.
+  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%).
 - **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/agents/runs.md

@@ -12,7 +12,12 @@ no more.
   `dev/dump_c.exs`): the kernels compile, their C goes to `<dir>`, and no
   library is built (`DEFK_NO_CC=1`, set by the alias). Every test file and
   example took 68 s on 2026-10-19 with a cold library cache; named files take
-  seconds. Diff two dumps to see which modules' C changed.
+  seconds. Diff two dumps to see which modules' C changed. Beside each
+  `<Module>.c` the dump writes `<Module>.report`, the compiler's report notes
+  (`__defk_report__/0` without `report: :full`'s clang part), so the same
+  diff shows a change to the report; its notes name absolute paths only for
+  a note in another file, so dump both sides from the same directory when a
+  report diff matters.
 - **An example's check** (`mix defk.examples --only a,b`): builds the
   libraries and runs the example's `:check`, defk against Elixir. No timing.
 - **`mix test`, `mix ci`**: before the PR, as `AGENTS.md` says.

docs/fast-path-report.md

@@ -40,10 +40,11 @@ next_sum/1  test/report_test.exs:16
   20 |   end
 ```
 
-When one small fact about the kernel's values would prove the missing
-half, the note names it. Here a raising guard `if w < 1, do: raise(...)`
-before the loop (docs/language.md, "Preconditions: raising guards") would
-drop both checks:
+With `use Defk, report: :full` (below), when one small fact about the
+kernel's values would prove the missing half, the note names it. Here a
+raising guard `if w < 1, do: raise(...)` before the loop
+(docs/language.md, "Preconditions: raising guards") would drop both
+checks:
 
 ```text
   6 |       n -> if x[i] > x[i - w], do: n + 1, else: n  # x[i]: bounds check kept; nothing proves 0 <= i (it would follow from w >= 0)
@@ -52,7 +53,9 @@ drop both checks:
 
 The fact is a hint: the residual with the fewest terms that the proof
 search reached, when it has at most two variables or lengths and a small
-constant. Another fact could also do.
+constant. Another fact could also do. The search runs once per kept check,
+so a module asks for it with `report: :full`; without it the note ends at
+what nothing proves.
 
 An `if`, `cond` or `case` value whose arms are pure arithmetic becomes a
 select, which computes every arm. An arm that dropped a check only because
@@ -88,7 +91,7 @@ it before the loop and clearing each pass) and `:vectorize`.
 defk's own facts are noted while the kernel is lowered. They cost no extra
 compiler pass and nothing at run time.
 
-## Vectorisation: `report: :full`
+## Hints and vectorisation: `report: :full`
 
 ```elixir
 defmodule Stats do
@@ -97,7 +100,8 @@ defmodule Stats do
 end
 ```
 
-This adds a `{:vectorize, verdict, text}` fact to each loop, taken from
+This names the fact that would drop a kept bounds check, as shown above,
+and adds a `{:vectorize, verdict, text}` fact to each loop, taken from
 clang's `-Rpass=loop-vectorize`, `-Rpass-missed=loop-vectorize` and
 `-Rpass-analysis=loop-vectorize` remarks. The verdict is `:vectorized`,
 `:missed` (with clang's reasons), `:partial` (some of the loop's C forms,

docs/language.md

@@ -1229,7 +1229,8 @@ lengths, through:
 It does not use products of three variables (`(y * w + x) * ch`), a `!=`
 or an `or` that holds, or `case` guards yet: such an index keeps its check, and the
 fast-path report says which half (`0 <= i` or `i < length(a)`) nothing
-proves, and, when one small fact would prove it, that fact:
+proves, and, with `use Defk, report: :full`, when one small fact would
+prove it, that fact:
 `nothing proves i - w < length(x) (it would follow from w >= 0)`. That
 is a hint, not a promise: another fact could also do.
 
@@ -2156,7 +2157,8 @@ iex> M.rises(<<1::64-native>>, 0)
 `x[i]` and `x[i - w]` have no bounds check: `i >= w` from the range and
 `w >= 1` from the guard give `0 <= i - w` and `0 <= i`, and
 `i <= length(x) - 1` gives the rest. Without the guard both keep their
-checks, and the fast-path report names the fact they lack:
+checks, and the fast-path report (with `use Defk, report: :full`) names
+the fact they lack:
 `x[i - w]: bounds check kept; nothing proves i - w < length(x) (it would
 follow from w >= 0)`. The guard costs one compare per call; a check in the
 loop costs one per element and may keep clang from vectorising it.

docs/performance.md

@@ -2577,6 +2577,62 @@ else: 0))`; it now says `if first < 0 and n > 0, do: raise(ArgumentError,
 - **Source:** `defk-o08.3`; `test/copies_test.exs`.
 - **Status:** measured, provisional.
 
+### 6.40 Each statement's reads walked once: another -9% of the compiler's work
+
+- **Numbers:** entering a statement computed its reads three times: in
+  `Copies.live_after/1` (`stmt_reads/1`), in the compiler's `hoist/3` and
+  in `Copies.enter_stmt/4` (`reads/1`, the same set: `read_counts/1` skips a
+  match's left side as `stmt_reads/1` does). `Copies.block_liveness/1` keeps
+  each statement's reads beside its live set, and `enter/3` hands them on.
+  Over the 108 modules of `mix dump_c`, two rounds each, interleaved with
+  main: 125.9 -> 115.0 M reductions (-8.6%, the same without
+  `SatEx.Kernels`), 987 -> 934 ms (-5.4%); `HashChain.Kernels` and its
+  Elixir-mode twin -2.2 M reductions each, `SatEx.Kernels` -3.6 M. Against
+  the compiler before step 1 (6.38's baseline, by reductions): +7.4%
+  (-1.0% without `SatEx.Kernels`), from +17.6%: under ADR-0007's ceiling.
+- **Same C:** `mix dump_c` byte-identical for all 108 modules; a property
+  test checks `reads/1 == stmt_reads/1` and that `block_liveness/1` agrees
+  with `live_after/1` on generated blocks.
+- **Not done:** a statement nested d blocks deep is still walked once per
+  enclosing statement (its reads are part of theirs); building a
+  statement's reads from its blocks' would need the walk to follow the
+  lowering's order.
+- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run.
+- **Source:** `defk-o08.4`; `test/copies_test.exs`.
+- **Status:** measured, provisional.
+
+### 6.41 The report's hint search runs only under `report: :full`: -3.6% of the compiler's work
+
+- **Numbers:** the search for "it would follow from ..." (`Facts.residual/5`
+  for every kept bounds check) took about 2.4% of the compiler's time, 6% on
+  `SatEx.Kernels`. It now runs only in a module with `use Defk, report:
+  :full` (maintainer's call, 2026-10-20). Over the 108 modules of `mix
+  dump_c`, two rounds each, interleaved with 6.40's state: 114.9 -> 110.8 M
+  reductions (-3.6%; -1.2% without `SatEx.Kernels`, which alone saves
+  3.2 M), 932 -> 922 ms (-1.1%, within drift). Same C (but for the path-hashed
+  loop markers of the two test modules that took `report: :full`); every
+  report the same less its hints, and two notes of `HashChain.Kernels` that
+  differed only by their hints now kept once (a note made twice is kept
+  once). Against the compiler before step 1 (6.38's baseline, by
+  reductions): +3.5% (-2.2% without `SatEx.Kernels`).
+- **Tried first, not adopted** (both keep every report the same, checked
+  with `mix dump_c`'s `.report` files, two rounds interleaved against
+  main):
+  - A text made only when the note survives (a closure, rendered in
+    `report/0`, so a lowering that is undone and redone drops its notes
+    unrendered): -1.5% of the work (reductions), all on `SatEx.Kernels`
+    (-1.85 M; no other module redoes a lowering), but +9.0% time (+4.3%
+    without `SatEx.Kernels`, both rounds): every kept note's closure holds
+    the env and the facts scope of its moment until the compile ends, and
+    the collector copies them. Not adopted.
+  - A smaller `@hint_budget`: 8 drops the hints of two notes (a kernel of
+    `{:load, 9}`) for -0.5% of the work, 4 drops hints in four modules for
+    -0.9%. Not adopted: 16 stays.
+- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run.
+- **Source:** `defk-o08.5`; `test/condition_facts_test.exs` (a kernel with and
+  without `report: :full`).
+- **Status:** measured, provisional.
+
 ---
 
 ## 7. When a hand-written or wrapper NIF is still the answer
@@ -2884,4 +2940,4 @@ example or close a workload ticket, add its entries and its line here.
   `defk-sve`, `defk-sve.1` ([`state-copy-cost.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/state-copy-cost.md)), `defk-ulk`, `defk-ulk.1` ([`simd.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/simd.md)), `defk-33b`,
   `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.2`, `defk-o08.3`, `defk-o08.4`, `defk-o08.5`.

lib/defk.ex

@@ -47,8 +47,10 @@ defmodule Defk do
       `Mix.install` script, for instance). The kernels' own functions still
       run natively. Default `false`. See `Defk.ElixirMode`.
     * `report: :full` adds the C compiler's vectorisation of each loop to the
-      [fast-path report](`Defk.Report`), at the cost of a second C compile.
-      What it adds is unstable.
+      [fast-path report](`Defk.Report`), at the cost of a second C compile,
+      and names, for a kept bounds check, a small fact that would drop it,
+      at the cost of a proof search per kept check. What it adds is
+      unstable.
     * `adaptive_slice: false` turns off the short first slice on a crowded
       run queue. By default a yielding kernel's function reads
       `:erlang.statistics(:total_run_queue_lengths)` (about 9 ns) and, when
@@ -444,15 +446,16 @@ defmodule Defk do
           nif_name: nif_name,
           fault_hooks: fault_hooks?,
           adaptive_slice: adaptive?,
-          max_owned_bytes: max_owned_bytes!(env.module)
+          max_owned_bytes: max_owned_bytes!(env.module),
+          hints: Module.get_attribute(env.module, :defk_report) == :full
         )
       end)
 
     # a yielding kernel's NIF takes the run-queue hint: it is
     # renamed, and the kernel's function passes the hint
     all_sigs = Enum.map(all_sigs, &Map.update!(&1, :yields, fn y -> adaptive? and y end))
 
-    if dump = System.get_env("DEFK_DUMP_C"), do: dump_c!(dump, env.module, c_src)
+    if dump = System.get_env("DEFK_DUMP_C"), do: dump_c!(dump, env.module, c_src, report)
 
     {report, placement} = library(env, c_src, report)
 
@@ -514,12 +517,19 @@ defmodule Defk do
   end
 
   # DEFK_DUMP_C=<dir>: every module compiled while it is set writes its
-  # generated C to <dir>/<Module>.c — the byte-identical gate for compiler
-  # refactors (dev/dump_c.exs). A pure side channel: the build
-  # and the module are unchanged.
-  defp dump_c!(dir, module, c_src) do
+  # generated C to <dir>/<Module>.c, and the compiler's report notes (the
+  # fast-path report before `report: :full` adds clang's) to
+  # <dir>/<Module>.report — the byte-identical gate for compiler refactors
+  # (dev/dump_c.exs). A pure side channel: the build and the module are
+  # unchanged.
+  defp dump_c!(dir, module, c_src, report) do
     File.mkdir_p!(dir)
     File.write!(Path.join(dir, "#{inspect(module)}.c"), c_src)
+
+    File.write!(
+      Path.join(dir, "#{inspect(module)}.report"),
+      Enum.map(report, &[inspect(&1, limit: :infinity, printable_limit: :infinity), "\n"])
+    )
   end
 
   # DEFK_COMPILE_TIME=<file>: every module compiled while it is set appends

lib/defk/compiler.ex

@@ -104,9 +104,15 @@ defmodule Defk.Compiler do
   #       adaptive_slice - a yielding kernel's NIF is `__defk_native_<name>__`
   #         with the run-queue hint as an extra last argument (default false);
   #       max_owned_bytes - the byte budget of a call's owned buffers (DEFK_MAX_OWNED
-  #         in priv/defk_runtime.h; default nil: half of physical memory)
+  #         in priv/defk_runtime.h; default nil: half of physical memory);
+  #       hints - a kept bounds check's note names the fact that would drop
+  #         it (note_bounds/4: a proof search per kept check; default false,
+  #         `report: :full` turns it on)
   def compile(module, raw_kernels, file, opts \\ []) do
-    Process.put(@ctx, Ctx.new(file, module, source_lines(file)))
+    Process.put(@ctx, %{
+      Ctx.new(file, module, source_lines(file))
+      | hints: Keyword.get(opts, :hints, false)
+    })
 
     kernels =
       raw_kernels
@@ -369,7 +375,8 @@ defmodule Defk.Compiler do
     case Code.string_to_quoted(src) do
       # the statements are lowered in the block of the statement env is at
       {:ok, ast} ->
-        probe(fn -> stmt_list(exprs(ast), Copies.live_after(exprs(ast)), env) end) != :error
+        probe(fn -> stmt_list(exprs(ast), Copies.block_liveness(exprs(ast)), env) end) !=
+          :error
 
       _ ->
         false
@@ -906,7 +913,7 @@ defmodule Defk.Compiler do
   defp lower_block_env(ast, env) do
     es = exprs(ast)
     {init, [last]} = Enum.split(es, -1)
-    lives = Copies.live_after(es)
+    lives = Copies.block_liveness(es)
     {s1, env} = stmt_list(init, lives, nested(env, ast))
 
     {s2, v, env} =
@@ -957,10 +964,11 @@ defmodule Defk.Compiler do
   # A block evaluated only for effect, nested like lower_block's.
   defp lower_stmts(ast, env) do
     es = exprs(ast)
-    stmt_list(es, Copies.live_after(es), nested(env, ast))
+    stmt_list(es, Copies.block_liveness(es), nested(env, ast))
   end
 
-  # statements `es` of one block; `lives` has the names read after each
+  # statements `es` of one block; `lives` has, for each, the names read after
+  # it and the names it reads (Copies.block_liveness/1)
   defp stmt_list(es, lives, env) do
     Enum.zip(AllocZeroing.mark(es), lives)
     |> Enum.reduce({[], env}, fn {e, live}, {acc, env} ->
@@ -1349,12 +1357,13 @@ defmodule Defk.Compiler do
   defp array_ids({:arr, _}), do: %{id: make_ref(), buf: make_ref(), fin: false, depth: 1}
   defp array_ids(_t), do: %{}
 
-  # Before statement `e` of a block, `live` the names read after it: copy
-  # what its nested writes need (hoist/3), then note what is live.
-  defp enter(e, live, env) do
+  # Before statement `e` of a block, `live` the names read after it and
+  # `reads` those it reads: copy what its nested writes need (hoist/4), then
+  # note what is live.
+  defp enter(e, {live, reads}, env) do
     names = Copies.live_names(e, live)
-    {sh, env} = hoist(e, names, env)
-    {sh, %{env | scope: Copies.enter_stmt(env.scope, e, names, env.vars)}}
+    {sh, env} = hoist(e, names, reads, env)
+    {sh, %{env | scope: Copies.enter_stmt(env.scope, e, names, reads, env.vars)}}
   end
 
   # A variable bound outside the branches and loop bodies of `e` and written
@@ -1363,8 +1372,8 @@ defmodule Defk.Compiler do
   # only binding of an owned buffer, so its writes are in place, and a loop
   # copies once. An input array written in a branch is copied even when the
   # branch is not taken.
-  defp hoist(e, names, env) do
-    seen = MapSet.union(names, Copies.reads(e))
+  defp hoist(e, names, reads, env) do
+    seen = MapSet.union(names, reads)
 
     Enum.reduce(Copies.nested_writes(e), {[], env}, fn n, {acc, env} ->
       case env.vars do
@@ -5099,7 +5108,7 @@ defmodule Defk.Compiler do
   defp lower_tail(ast, env, leaf) do
     es = exprs(ast)
     {init, [last]} = Enum.split(es, -1)
-    lives = Copies.live_after(es)
+    lives = Copies.block_liveness(es)
     {s, env} = stmt_list(init, lives, nested(env, ast))
 
     [
@@ -6287,9 +6296,10 @@ defmodule Defk.Compiler do
   # a[i], or the word load u64_le(bytes, i), of width w: its bounds check
   # dropped, or kept with the facts that would drop it. `proof` is the
   # access's own (Facts.check/4), which names the half that fails, so what
-  # is named is what the proof would accept. A failing half names the fact
-  # it would follow from when that is small (Facts.residual/5): a value `a`
-  # indexed by `i`, in `env`.
+  # is named is what the proof would accept. Under `report: :full` (ctx
+  # hints), a failing half also names the fact it would follow from when
+  # that is small (Facts.residual/5, a search per kept check, so not for
+  # every compile): a value `a` indexed by `i`, in `env`.
   defp note_bounds(node, w, proof, {a, i, env}) do
     {text, arr, idx} =
       case node do
@@ -6304,10 +6314,14 @@ defmodule Defk.Compiler do
       {:unproven, half} ->
         {arr, idx} = {src_text(arr), src_text(idx)}
 
+        hints? = ctx(:hints)
+
         named = fn h, what ->
-          case Facts.residual(a, i, w, h, env.facts) |> hint_text(env) do
-            nil -> what
-            fact -> "#{what} (it would follow from #{fact})"
+          with true <- hints?,
+               fact when fact != nil <- Facts.residual(a, i, w, h, env.facts) |> hint_text(env) do
+            "#{what} (it would follow from #{fact})"
+          else
+            _ -> what
           end
         end
 

lib/defk/compiler/ctx.ex

@@ -15,6 +15,7 @@ defmodule Defk.Compiler.Ctx do
             broken: MapSet.new(),
             statics: %{},
             report: [],
+            hints: false,
             bits_names: %{},
             lowering: nil
 

lib/defk/copies.ex

@@ -177,10 +177,17 @@ defmodule Defk.Copies do
   def stmt_reads(e), do: reads(e)
 
   # for each statement of a block, the names read after it in the block
-  def live_after(es) do
+  def live_after(es), do: es |> block_liveness() |> Enum.map(&elem(&1, 0))
+
+  # for each statement of a block, {the names read after it in the block,
+  # the names it reads}: what entering it needs (enter_stmt/5), from one
+  # walk of it. stmt_reads/1 is reads/1 of the statement: read_counts/1
+  # skips a match's left side as stmt_reads/1 does.
+  def block_liveness(es) do
     {lives, _} =
       List.foldr(es, {[], MapSet.new()}, fn e, {acc, live} ->
-        {[live | acc], live |> MapSet.difference(binds(e)) |> MapSet.union(stmt_reads(e))}
+        reads = stmt_reads(e)
+        {[{live, reads} | acc], live |> MapSet.difference(binds(e)) |> MapSet.union(reads)}
       end)
 
     lives
@@ -289,9 +296,12 @@ defmodule Defk.Copies do
   # with `vars` the bindings after the copies hoisted before `e`: what is
   # live after `e`, and for the blocks nested in it (which also see what `e`
   # reads, as a later iteration or a later arm does).
-  def enter_stmt(%Scope{} = s, e, names, vars) do
+  # `reads` is reads(e), when the caller has it (block_liveness/1).
+  def enter_stmt(%Scope{} = s, e, names, vars), do: enter_stmt(s, e, names, reads(e), vars)
+
+  def enter_stmt(%Scope{} = s, e, names, reads, vars) do
     live = MapSet.union(pairs(vars, names), s.out)
-    nest = MapSet.union(live, pairs(vars, reads(e)))
+    nest = MapSet.union(live, pairs(vars, reads))
     %{s | stmt: e, live: live, live_names: names, nest: nest}
   end