defk-o08.2: compiler time measured warm in a fresh process; the chain measured again against its budget

dev/compile_time.exs

@@ -0,0 +1,107 @@
+# Compiler time: compare rounds of DEFK_COMPILE_TIME logs from two
+# checkouts. One round is one dump of every kernel, its log one line per
+# module, "<Module> <microseconds> <reductions>" of a compile measured in a
+# fresh process (Defk.__before_compile__):
+#
+#   DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c   # in the base checkout
+#   DEFK_COMPILE_TIME=tmp/new1.log  DEFK_DUMP_C=tmp/c_new  mix dump_c   # in the new one
+#   ... base2, new2, ..., interleaved so drift hits both sides ...
+#   elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log
+#   elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log
+#
+# Microseconds drift with the machine (a laptop's clock on battery moved a
+# whole round by about 25% between runs); reductions, the work the BEAM
+# counts, repeat to about 0.1% and are the figure to compare when the
+# change is the compiler's own work. Only the modules every log has are
+# compared, so kernels added between the two checkouts do not count as a
+# cost, but a kernel edited between them does: check that the examples and
+# test modules are unchanged. A module name compiled twice in one round
+# (two files) is summed. Each side's figure is the median of its rounds,
+# with and without SatEx.Kernels (examples/cdcl_sat.exs, thousands of kept
+# checks: it dominates any prover cost). With no `--`, the logs are one
+# side and only its medians are printed.
+
+{column, args} =
+  case System.argv() do
+    ["--reductions" | rest] -> {2, rest}
+    rest -> {1, rest}
+  end
+
+{base_paths, new_paths} =
+  case Enum.split_while(args, &(&1 != "--")) do
+    {base, ["--" | new]} -> {base, new}
+    {base, []} -> {base, []}
+  end
+
+if base_paths == [] do
+  IO.puts(
+    :stderr,
+    "usage: elixir dev/compile_time.exs [--reductions] <base logs> [-- <new logs>]"
+  )
+
+  System.halt(2)
+end
+
+read = fn path ->
+  for line <- File.read!(path) |> String.split("\n", trim: true),
+      [mod | figures] = String.split(line),
+      n = String.to_integer(Enum.at(figures, column - 1)),
+      reduce: %{},
+      do: (acc -> Map.update(acc, mod, n, &(&1 + n)))
+end
+
+{base, new} = {Enum.map(base_paths, read), Enum.map(new_paths, read)}
+
+common =
+  (base ++ new)
+  |> Enum.map(&MapSet.new(Map.keys(&1)))
+  |> Enum.reduce(&MapSet.intersection/2)
+
+median = fn xs ->
+  sorted = Enum.sort(xs)
+  n = length(sorted)
+  mid = div(n, 2)
+
+  if rem(n, 2) == 1,
+    do: Enum.at(sorted, mid),
+    else: div(Enum.at(sorted, mid - 1) + Enum.at(sorted, mid), 2)
+end
+
+total = fn round, mods -> mods |> Enum.map(&Map.fetch!(round, &1)) |> Enum.sum() end
+without_sat = MapSet.delete(common, "SatEx.Kernels")
+
+side = fn rs ->
+  {median.(Enum.map(rs, &total.(&1, common))), median.(Enum.map(rs, &total.(&1, without_sat)))}
+end
+
+show =
+  if column == 1,
+    do: fn us -> :erlang.float_to_binary(us / 1000, decimals: 1) <> " ms" end,
+    else: fn r -> :erlang.float_to_binary(r / 1.0e6, decimals: 2) <> "M reductions" end
+
+pct = fn a, b -> :erlang.float_to_binary(100 * (b - a) / a, decimals: 1) <> "%" end
+
+IO.puts(
+  "#{MapSet.size(common)} modules in every log; rounds: #{length(base)} base, #{length(new)} new"
+)
+
+{b_all, b_wo} = side.(base)
+IO.puts("base: #{show.(b_all)} (without SatEx.Kernels #{show.(b_wo)})")
+
+if new != [] do
+  {n_all, n_wo} = side.(new)
+  IO.puts("new:  #{show.(n_all)} (without SatEx.Kernels #{show.(n_wo)})")
+  IO.puts("change: #{pct.(b_all, n_all)} (without SatEx.Kernels #{pct.(b_wo, n_wo)})")
+
+  deltas =
+    for m <- common do
+      {m, median.(Enum.map(new, & &1[m])) - median.(Enum.map(base, & &1[m]))}
+    end
+
+  IO.puts("largest changes by module (median):")
+
+  deltas
+  |> Enum.sort_by(&(-abs(elem(&1, 1))))
+  |> Enum.take(5)
+  |> Enum.each(fn {m, d} -> IO.puts("  #{m} #{if d >= 0, do: "+", else: ""}#{show.(d)}") end)
+end

docs/adr/0007-symbolic-bounds.md

@@ -80,7 +80,12 @@ Replace the fact model with one representation:
   (products, `defk-pvt`) +1.7% (+0.9% without `SatEx.Kernels`) after
   cutting a second fact lookup per step and the ranking of one-term forms;
   the chain is at about +14%, under the ceiling, with about 1% left
-  (`docs/performance.md` 6.37).
+  (`docs/performance.md` 6.37). Measured again (2026-10-20) with a warm
+  compile in a fresh process (6.38; the method before included waiting
+  and heap noise): the chain cost +13.4% of the time but +20.8% of the
+  work (reductions), and the refactors after it another +13.5% / +7.3%.
+  The compiler is at about +29% of its time before step 1, past the
+  ceiling; the next step cuts first (the copy analysis, `defk-o08.3`).
 - **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

@@ -61,9 +61,23 @@ cores it uses.
 
 ## Compiler time
 
-The compiler-time rounds (a temporary `:timer.tc` around
-`Defk.Compiler.compile` in `Defk.__before_compile__`, interleaved `mix
-dump_c` rounds on both sides) measure defk's compile, not `cc`, so they run
-without `cc` too. Name the files when the change touches only some kernels,
-and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own: it
-dominates the prover's cost.
+The compiler-time rounds measure defk's compile, not `cc`, so they run
+without `cc` too. With `DEFK_COMPILE_TIME=<file>` set, every module compiles
+once more in a fresh process and logs that compile's microseconds and
+reductions (`Defk.__before_compile__`, `timed_compile/2`). Run interleaved
+rounds on both sides and compare them:
+
+    DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c   # base checkout
+    DEFK_COMPILE_TIME=tmp/new1.log  DEFK_DUMP_C=tmp/c_new  mix dump_c   # branch
+    ... base2, new2 ...
+    elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log
+    elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log
+
+Two rounds a side are enough for reductions, which repeat to about 0.1%;
+microseconds drift with the machine (about 25% between runs on a laptop
+on battery), so report them with the conditions. A full round takes about
+a minute and a half. Name the files when the change touches only some
+kernels, and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own:
+it dominates the prover's cost. Do not time a module's first compile: under
+`mix compile` it waits for the compiler's own modules (`docs/performance.md`
+6.38).

docs/performance.md

@@ -2514,6 +2514,48 @@ else: 0))`; it now says `if first < 0 and n > 0, do: raise(ArgumentError,
   the whole suite under AddressSanitizer.
 - **Status:** measured, provisional.
 
+### 6.38 Compiler time: measure a second compile in a fresh process; the chain and the refactors cost ~29% together
+
+- **The method before** (6.32-6.37) timed `Defk.Compiler.compile` once per
+  module under `mix dump_c`. That run is `compile --force`, so `lib` and
+  `test/support` compile in parallel, and the first kernel module
+  (`Examples.Kernels`) waited about 1 s for the compiler's own modules: of
+  a 2.5 s round, about 1.0 s was that wait (the module needs 13 ms warm).
+  A second compile in the same process was no better: `SatEx.Kernels`
+  then took either ~240 or ~510 ms on the same code (what the first
+  compile left on the heap), and a whole round moved by ~25% between two
+  runs on the laptop.
+- **The method now:** `DEFK_COMPILE_TIME=<file>` makes every module compile
+  once for its result and once more in a fresh process, which is measured:
+  microseconds and the process's reductions. `dev/compile_time.exs`
+  compares interleaved rounds of two checkouts on the modules both have.
+  Five compiles of `SatEx.Kernels`: 355-369 ms, 50.64-50.68 M reductions
+  (±2% and ±0.05%). Reductions are the figure to compare for a change to
+  the compiler's own work; time is the one a user feels.
+- **Numbers** (99 modules both checkouts have, two rounds each,
+  interleaved, medians): before step 1 (`23e27970`) 105.8 M reductions /
+  801 ms; after step 4 (`a371dcab`) 127.8 M / 909 ms; main (`b90ed0ff`)
+  137.1 M / 1,032 ms. The symbolic-bounds chain: +20.8% reductions, +13.4%
+  time (without `SatEx.Kernels` +6.8%, +3.9%). The readability refactors
+  after it (`x3a`, `rt2`): +7.3% reductions, +13.5% time (+6.7%, +3.3%).
+  Together +29.5% reductions, +28.8% time (+14.0%, +7.3%). `SatEx.Kernels`
+  alone went from ~150 to ~340 ms.
+- **What it means:** the chain's own +14% (6.37) holds for time but not for
+  work, and the compiler is about twice as far past its state before step
+  1 as the +15% ceiling of ADR-0007 allows, half of it from refactors no
+  budget covered. Where the time is (one warm round, 2026-10-20): the copy
+  analysis's per-statement walks ~16% (`Copies.nested/3` 9.7%), the
+  prover ~3.5%, the report's hint search 2.4%, the strip classifier 2.4%;
+  the rest is spread over the lowering.
+- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run
+  (`DEFK_NO_CC=1`; the baseline with the `DEFK_NO_CC` change applied, a
+  tooling change). A few examples and test kernels changed between the
+  checkouts (`hash_chain.exs` gained a raising guard), so the 99 modules are
+  not all identical; `SatEx.Kernels` (`cdcl_sat.exs`) is.
+- **Source:** `defk-o08.2`; `dev/compile_time.exs`; the harness in
+  `Defk.__before_compile__` (`timed_compile/2`).
+- **Status:** measured, provisional.
+
 ---
 
 ## 7. When a hand-written or wrapper NIF is still the answer
@@ -2820,4 +2862,5 @@ example or close a workload ticket, add its entries and its line here.
   `defk-l2g`, `defk-yzw`, `defk-dtw.2`, `defk-dtw.20`, `defk-dtw.21`,
   `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-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`,
+  `defk-o08.2`.

lib/defk.ex

@@ -439,12 +439,14 @@ defmodule Defk do
     adaptive? = Module.get_attribute(env.module, :defk_adaptive_slice)
 
     {c_src, all_sigs, report} =
-      Defk.Compiler.compile(env.module, kernels, env.file,
-        nif_name: nif_name,
-        fault_hooks: fault_hooks?,
-        adaptive_slice: adaptive?,
-        max_owned_bytes: max_owned_bytes!(env.module)
-      )
+      timed_compile(env.module, fn ->
+        Defk.Compiler.compile(env.module, kernels, env.file,
+          nif_name: nif_name,
+          fault_hooks: fault_hooks?,
+          adaptive_slice: adaptive?,
+          max_owned_bytes: max_owned_bytes!(env.module)
+        )
+      end)
 
     # a yielding kernel's NIF takes the run-queue hint: it is
     # renamed, and the kernel's function passes the hint
@@ -520,6 +522,48 @@ defmodule Defk do
     File.write!(Path.join(dir, "#{inspect(module)}.c"), c_src)
   end
 
+  # DEFK_COMPILE_TIME=<file>: every module compiled while it is set appends
+  # "<Module> <microseconds> <reductions>" to <file>, of a second compile
+  # run in a fresh process (dev/compile_time.exs). The first compile, whose
+  # result the module uses, is not measured: under `mix compile` it may wait
+  # for the compiler's own modules, compiled in parallel with the kernels,
+  # and that wait is not compiler work. A fresh process starts with a small
+  # heap, so the time does not depend on what the first compile left. Like
+  # DEFK_DUMP_C, a side channel: the module is unchanged.
+  defp timed_compile(module, compile) do
+    case System.get_env("DEFK_COMPILE_TIME") do
+      nil ->
+        compile.()
+
+      log ->
+        result = compile.()
+        {us, reductions} = measured(compile)
+        File.write!(log, "#{inspect(module)} #{us} #{reductions}\n", [:append])
+        result
+    end
+  end
+
+  defp measured(compile) do
+    parent = self()
+
+    {pid, mref} =
+      spawn_monitor(fn ->
+        {:reductions, r0} = Process.info(self(), :reductions)
+        {us, _} = :timer.tc(compile)
+        {:reductions, r1} = Process.info(self(), :reductions)
+        send(parent, {self(), us, r1 - r0})
+      end)
+
+    receive do
+      {^pid, us, reductions} ->
+        Process.demonitor(mref, [:flush])
+        {us, reductions}
+
+      {:DOWN, ^mref, :process, ^pid, reason} ->
+        raise "DEFK_COMPILE_TIME: the measured compile failed: #{inspect(reason)}"
+    end
+  end
+
   # `use Defk, max_owned_bytes: n`: a positive integer of bytes that fits in
   # a uint64 (DEFK_MAX_OWNED), or nil (the runtime's default)
   defp max_owned_bytes!(module) do