defk-rt2.11: the rest of the typing stays twice (ADR-0008 extended); drop Elixir mode's dead ctx write

docs/adr/0006-public-api-surface.md

@@ -65,7 +65,7 @@ above.
 | `Defk.Test.reason/1` | `@doc` in hidden module | tests 9 | **public** | what "same reason" means in agreement; users need it to assert a raise. Rename candidate |
 | `Defk.Case.in_both_modes/1` (macro) | hidden module | tests 2 | **hidden** | see open question 4 |
 | `Defk.ElixirMode.with_mode/2` | `@doc` | tests 6, 1 example, README, `language.md` | **public** | the documented per-process switch |
-| `Defk.ElixirMode.setup!/4`, `native_name/1`, `process_mode_key/0`, `definitions/3`, `fun_name/1` | `@doc false` | `Defk` at compile time | **hidden** | |
+| `Defk.ElixirMode.setup!/4`, `native_name/1`, `process_mode_key/0`, `definitions/2`, `fun_name/1` | `@doc false` | `Defk` at compile time | **hidden** | |
 | `Defk.Bits.wrap64/1`, `mulhi/2`, `clz/1`, `ctz/1`, `popcount/1`, `rotl64/2`, `rotr64/2`, `clz/2`, `ctz/2`, `rotl/3`, `rotr/3`, `f64_to_u64/1` (12) | `@doc`, `@spec`, doctests | Elixir mode, tests, `language.md` | **public** | each is a kernel builtin's meaning; renaming one is a language change |
 | `Defk.Report.print/1` | `@doc`, `@spec` | 1 test, 1 example, README, `performance.md`, `fast-path-report.md` | **public** | the way to read the report |
 | `Defk.Report.format/1` | `@doc`, `@spec` | `print/1` | **public** | the same text as a string (for tests and tools) |

docs/adr/0008-builtin-typing-shared-semantics-twice.md

@@ -1,7 +1,8 @@
 # ADR-0008: Builtin typing is shared data; builtin semantics are written twice on purpose
 
 - Date: 2026-10-12
-- Status: accepted (2026-10-12, maintainer, architecture review grilling)
+- Status: accepted (2026-10-12, maintainer, architecture review grilling);
+  extended 2026-10-20 (the rest of the typing, below)
 - Source: /improve-codebase-architecture session 2026-10-12; evidence in the
   review of `Defk.Compiler.builtin/4` and `Defk.ElixirMode.builtin/4`
 
@@ -45,3 +46,42 @@ remains defined as same exception module for the same reason.)
   exist and agree.
 - Anyone proposing to generate the Elixir emissions (or `Ops` bodies) from
   the table should be pointed here: it would silently retire the oracle.
+
+## Extension (2026-10-20): the rest of the typing also stays twice
+
+- Status: accepted (2026-10-20, maintainer)
+- Source: the spike `defk-rt2.11` (its ticket comment has the numbers)
+
+Beyond the builtins, Elixir mode types every node again: `expr/2`
+returns `{quoted, type}`, and the u64 accumulator inference
+(`settle_accs/3`, `note_u64_mix/3`) is a hand copy of the compiler's
+`u64_accs/2`. The spike asked whether the compiler could hand Elixir mode
+its node types, so that Elixir mode only emits.
+
+The seam exists. The compiler runs first, on the same desugared kernels,
+and a unique id stamped into each node's meta keys a node (a line and a
+column do not: a kernel built by a macro has no columns). The stamp left
+the C of every test and example module byte-identical, and 99.2% of
+Elixir mode's 58,361 keyed node typings equalled the compiler's own. The
+rest are four special cases: `bitstring` and `[u8]` naming, nodes the
+compiler types twice (u64 retries, `in` guards), float trees that do not
+pass `lower_expr`, and helpers that are only inlined.
+
+Decision: Elixir mode keeps its own typing. Two reasons:
+
+- The u64 accumulator inference is semantics, not typing: it decides the
+  result. `3 - 5` on a u64 accumulator raises, on an i64 one it is `-2`.
+  Shared, an inference error in the compiler would pass every agreement
+  test, which is what the decision above forbids.
+- Without that part the gain is about 20 lines (`body_type/3`, the
+  `leaf_types` look ahead). `expr/2`'s types and `trial/1` stay in any
+  case, as the emission and the write discovery use them. The cost is a
+  stamping step, type records in several lowering paths, the four special
+  cases, and an Elixir mode that depends on the compiler's lowering
+  instead of the AST.
+
+## How to revisit
+
+A proposal to share node types with Elixir mode answers both reasons: an
+independent check of the u64 accumulator inference, and a gain larger than
+the four special cases and the coupling.

docs/agents/compiler-map.md

@@ -120,7 +120,7 @@ of rows the lowering declares as it emits; defk-ch4), not from the C text.
   Its translation state (binding counter, writes log, look-ahead leaf
   types, u64 candidates and hits) is one process-dictionary key, `:defk_em`,
   holding one `Defk.ElixirMode.State`, fresh per kernel and deleted when
-  `definitions/3` returns; the `env` map (vars, sigs) is threaded
+  `definitions/2` returns; the `env` map (vars, sigs) is threaded
   explicitly. `lib/defk/elixir_mode/guard.ex` evaluates a case guard that
   can fail.
 - `lib/defk/inline_size.ex`: the code-size warning (defk-6ag).

lib/defk.ex

@@ -458,7 +458,7 @@ defmodule Defk do
     sigs = Enum.reject(all_sigs, &Defk.Bitstring.helper?/1)
 
     elixir_mode =
-      if elixir?, do: Defk.ElixirMode.definitions(kernels, all_sigs, env.file), else: []
+      if elixir?, do: Defk.ElixirMode.definitions(kernels, all_sigs), else: []
 
     Defk.Generated.defs(
       placement: placement,

lib/defk/elixir_mode.ex

@@ -146,20 +146,16 @@ defmodule Defk.ElixirMode do
 
   @doc false
   # Quoted definitions: `__defk_elixir__/2` and one private function per kernel.
-  def definitions(raw_kernels, sigs, file) do
-    # the compiler's ctx keeps the file for the rejections this translation
-    # raises (err! reads it); the translation's own state is `@state`, gone
-    # when this returns
-    Defk.Compiler.Ctx.set(:file, file)
+  # The translation's state is `@state`, gone when this returns; it never
+  # reads the compiler's ctx (a rejection reaching it raises plainly,
+  # raise_form!/4).
+  def definitions(raw_kernels, sigs) do
+    by_key = Map.new(sigs, &{{&1.name, &1.arity}, &1})
 
-    try do
-      by_key = Map.new(sigs, &{{&1.name, &1.arity}, &1})
-
-      Enum.zip_with(raw_kernels, sigs, fn raw, sig -> kernel(raw.body, sig, by_key) end)
-      |> definitions_of(sigs)
-    after
-      Process.delete(@state)
-    end
+    Enum.zip_with(raw_kernels, sigs, fn raw, sig -> kernel(raw.body, sig, by_key) end)
+    |> definitions_of(sigs)
+  after
+    Process.delete(@state)
   end
 
   defp definitions_of(kernels, sigs) do
@@ -204,7 +200,7 @@ defmodule Defk.ElixirMode do
   # holding one struct (as the compiler's :defk_ctx): the binding counter,
   # the writes log (write tracking), the leaf types a reduce_while look
   # ahead collects, and the u64 candidates and hits of settle_accs/3. Fresh
-  # per kernel, deleted when definitions/3 returns. The `env` map (vars,
+  # per kernel, deleted when definitions/2 returns. The `env` map (vars,
   # sigs) is threaded explicitly; this is the rest.
 
   defmodule State do

test/compiler_ctx_test.exs

@@ -34,8 +34,8 @@ defmodule Defk.CompilerCtxTest do
 
   # Elixir mode's translation keeps its own state the same way, in one key
   # (:defk_em) holding one struct, fresh per kernel and gone when
-  # definitions/3 returns: no translation state outlives a compile either.
-  test "after ElixirMode.definitions/3, the ctx is still the only defk-prefixed key" do
+  # definitions/2 returns: no translation state outlives a compile either.
+  test "after ElixirMode.definitions/2, the ctx is still the only defk-prefixed key" do
     for k <- defk_keys(), do: Process.delete(k)
 
     kernel = %{
@@ -55,7 +55,7 @@ defmodule Defk.CompilerCtxTest do
     }
 
     {_c, sigs, _report} = Defk.Compiler.compile(Defk.CompilerCtxTest.E, [kernel], nil)
-    defs = Defk.ElixirMode.definitions([kernel], sigs, "ctx_test.ex")
+    defs = Defk.ElixirMode.definitions([kernel], sigs)
 
     assert match?([_ | _], defs)
     assert defk_keys() == [:defk_ctx]