Skip to content

defk-rt2.7: Defk.Facts owns the range-facts scope; the provers stop reading the compiler's env #65

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
DanielLuning merged 1 commit into from
Oct 20, 2026
Merged

defk-rt2.7: Defk.Facts owns the range-facts scope; the provers stop reading the compiler's env #65

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions docs/agents/compiler-map.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ One module, ordered by section dividers you can grep for
| reduce accumulators | `for ... reduce:` and `reduce_while`: carrying, facts across trips, halts | `lower_reduce`, `with_acc_facts/2`, `u64_accs/2` |
| tails and branches | a `reduce_while` body's tail, if/else chains | `lower_tail/3`, `branch_chain/3` |
| case | clause dispatch (multi-clause kernels); a case guard lowered with the guard as the error sink (`env.sink`), whose flags are locals made on first use, and every value carries the flags its C uses | `case_arms`, `guard_expr/2`, `guard_flag/1`, `guard_poison/4` |
| range facts | `Defk.Facts` holds ADR-0007's representation: forms over atoms (array lengths and i64 bindings), values' exact forms (`eq`), bounds `{q, form}`, one prover with a step budget; this file states facts through the module's sources (`len_value`, `len_from`, `len_like`, `between`, `bound`, the derivations), keeps i64 bindings' facts by C variable in `env.atoms` (`put_var/3`), and asks the proofs with the env as scope | `Facts.check`, `Facts.fits_i64?`, `range_limit` |
| range facts | `Defk.Facts` holds ADR-0007's representation: forms over atoms (array lengths and i64 bindings), values' exact forms (`eq`), bounds `{q, form}`, one prover with a step budget; this file states facts through the module's sources (`len_value`, `len_from`, `len_like`, `between`, `bound`, the derivations), binds each i64 and array binding into the facts scope `env.facts` (`put_var/3`, `Facts.bind/2`), narrows it by a condition's relation (`narrow/3`, `guarded/4`, `Facts.narrow/3`), and asks the proofs with that scope | `Facts.check`, `Facts.fits_i64?`, `range_limit` |
| element types | narrow loads/stores; the one element-access decision for a store, a load and a word load: prove it in bounds, record the strip row, note the verdict (`access/6`), the site keeps its C templates | `access/6`, `narrowed/2`, `int_stored/2` |
| emitting | C text: entries, init, frames, resume; what each safepoint spills, read from the lowering's locals table (`loop_locals/2` in the kernels section), never from the C | `emit_entry`, `safepoint_saves/2`, `resume_block/3`, `view_term/3` |
| report | fast-path notes, each made where the lowering decides (bounds, overflow and range checks, the branch verdict); one of `compile/4`'s results, never read back | `note/4`, `note_bounds/4`, `note_overflow/2`, `note_fit/3`, `note_branch/2` |
Expand Down Expand Up @@ -82,7 +82,9 @@ of rows the lowering declares as it emits; defk-ch4), not from the C text.
see `docs/agents/generated-docs.md`.
- `lib/defk/facts.ex`: the range-facts lattice (one opaque value under
`v.facts`; assert/derive in, `check`/`prove_i64`/`fits_i64?` with
support out). ADR-0007's representation lives here; its soundness nets
support out) and the facts scope the provers read (`bind/2`,
`narrow/3`, `facts_of/2`: each binding's facts by its C variable, carried
in `env.facts`). ADR-0007's representation lives here; its soundness nets
are `test/facts_test.exs`, `test/scaled_facts_test.exs`,
`test/linear_facts_test.exs`, `test/condition_facts_test.exs` and
`test/product_facts_test.exs`.
Expand Down
114 changes: 39 additions & 75 deletions lib/defk/compiler.ex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -713,6 +713,7 @@ defmodule Defk.Compiler do

env = %{
vars: vars,
facts: Enum.reduce(vars, Facts.scope(), fn {_, b}, s -> Facts.bind(s, b) end),
sigs: sigs,
inlining: [{k.name, k.arity}],
ret: k.ret,
Expand Down Expand Up @@ -921,7 +922,7 @@ defmodule Defk.Compiler do
# A nested plain block binds into the scope around it, as in Elixir: `env`
# is the block's env at its end, `outer` the env the block is nested in.
defp leave(env, outer),
do: %{outer | vars: Copies.leave_block(env.vars, env.scope, outer.scope)}
do: %{outer | vars: Copies.leave_block(env.vars, env.scope, outer.scope), facts: env.facts}

# a nested block's value, and the env with its bindings; any other expression
# binds nothing
Expand Down Expand Up @@ -1280,15 +1281,10 @@ defmodule Defk.Compiler do
end
end

# an i64 binding's facts are also kept by its C variable (env.atoms), where
# the prover finds an atom's (Defk.Facts); it outlives a shadowing
# binding, as the variable is assigned once where it is in scope
# a binding's facts are also in the facts scope, where the prover finds an
# atom's (Facts.bind/2)
defp put_var(env, name, v) do
env = %{env | vars: Map.put(env.vars, name, Map.put(v, :var, v.c))}

if v.t == :i64,
do: Map.put(env, :atoms, Map.put(env[:atoms] || %{}, v.c, Facts.facts(v))),
else: env
%{env | vars: Map.put(env.vars, name, Map.put(v, :var, v.c)), facts: Facts.bind(env.facts, v)}
end

defp tuple_items({a, b}), do: [a, b]
Expand Down Expand Up @@ -1395,7 +1391,7 @@ defmodule Defk.Compiler do

defp copy_var(name, b, env) do
{s, nb} = copied(b, name)
{s, %{env | vars: Map.put(env.vars, name, nb)}}
{s, %{env | vars: Map.put(env.vars, name, nb), facts: Facts.bind(env.facts, nb)}}
end

# {stmts, value}: array `a` copied into a buffer of the kernel's own, in
Expand Down Expand Up @@ -1518,7 +1514,7 @@ defmodule Defk.Compiler do

{s, b} = copied(a, n)
note(:copy, arr, :copied, "#{n} is copied before this write: #{copy_why(a)}")
{s, b, %{env | vars: Map.put(env.vars, n, b)}}
{s, b, %{env | vars: Map.put(env.vars, n, b), facts: Facts.bind(env.facts, b)}}

_ ->
{s, b} = copied(a, "arr")
Expand Down Expand Up @@ -2287,23 +2283,14 @@ defmodule Defk.Compiler do
defp i64_arith(op, va, vb, node, env) do
{fun, facts, {lo, hi}} =
case op do
:+ ->
{"add", Facts.add_facts(va, vb),
{Facts.add(Facts.lo_of(va), Facts.lo_of(vb)),
Facts.add(Facts.hi_of(va), Facts.hi_of(vb))}}

:- ->
{"sub", Facts.sub_facts(va, vb),
{Facts.add(Facts.lo_of(va), Facts.neg(Facts.hi_of(vb))),
Facts.add(Facts.hi_of(va), Facts.neg(Facts.lo_of(vb)))}}

:* ->
{"mul", Facts.mul_facts(va, vb), Facts.mul_range(va, vb)}
:+ -> {"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)}
end

v = Facts.put(val(nil, :i64), facts)

if Facts.prove_i64(lo, hi) or Facts.fits_i64?(v, env) do
if Facts.prove_i64(lo, hi) or Facts.fits_i64?(v, env.facts) do
note_overflow(node, :dropped)
%{v | c: "(#{va.c} #{op} #{vb.c})"}
else
Expand Down Expand Up @@ -2576,7 +2563,8 @@ defmodule Defk.Compiler do
{s, c}
end

# a condition's statements and C, and what it says (Facts.holds/2)
# a condition's statements and C, and what it says (its relation, which
# Facts.narrow/3 reads)
defp lower_test(cond, env) do
{s, v} = lower_expr(cond, env)
bool!(v, cond, "a condition")
Expand Down Expand Up @@ -3129,11 +3117,7 @@ defmodule Defk.Compiler do
end

defp bitwise_val(:bnot, [a], _args, _node, _env),
do:
Facts.assert(val("(~#{a.c})", :i64),
lo: Facts.bnot(Facts.hi(a)),
hi: Facts.bnot(Facts.lo(a))
)
do: Facts.put(val("(~#{a.c})", :i64), Facts.bnot_facts(a))

defp bitwise_val(f, [a, b], _args, node, _env) when f in [:band, :bor, :bxor] do
cop = %{band: "&", bor: "|", bxor: "^"}[f]
Expand All @@ -3151,10 +3135,7 @@ defmodule Defk.Compiler do

case int_literal(n) do
k when f == :bsr and is_integer(k) and k in 0..63 ->
Facts.assert(val("(#{a.c} >> #{k})", :u64),
lo: 0,
hi: Bitwise.bsr(Facts.hi(a) || @max_u64, k)
)
Facts.put(val("(#{a.c} >> #{k})", :u64), Facts.u64_bsr_facts(a, k))

_ ->
val("defk_#{f}_u64#{check(env, :ovf)}, #{a.c}, #{b.c})", :u64)
Expand Down Expand Up @@ -3615,19 +3596,16 @@ defmodule Defk.Compiler do
end)
|> Enum.unzip()

# The parameters' facts may name the caller's atoms, which stay in scope
# in the inlined body (env.atoms, see put_var/3).
atoms =
for {_, %{t: :i64, c: c} = b} <- vars, into: env[:atoms] || %{}, do: {c, Facts.facts(b)}

# The parameters' facts may name the caller's atoms, which stay in the
# facts scope in the inlined body (Facts.bind/2).
# The callee's declared return type and returned fors: a rejected for in
# the inlined body gets the hint the callee's own compile gives, since a
# caller lowered first records the rejection (one per code and position).
# The bindings the caller still reads after the call stay live in the
# callee (Copies.inline_call/3).
cenv = %{
vars: Map.new(vars),
atoms: atoms,
facts: Enum.reduce(vars, env.facts, fn {_, b}, s -> Facts.bind(s, b) end),
sigs: env.sigs,
inlining: [key | env.inlining],
ret: k.ret,
Expand Down Expand Up @@ -5648,10 +5626,11 @@ defmodule Defk.Compiler do
end

# ---------------------------------------------------------- range facts --
# The lattice lives in Defk.Facts: what a value is known to
# satisfy, the derivations, and the proofs (in_bounds?, in_i64?) that drop
# checks. This file creates facts and asks those questions; it holds no
# fact algebra of its own.
# The lattice lives in Defk.Facts: what a value is known to satisfy, the
# derivations, the facts scope (env.facts) and the proofs (check,
# fits_i64?) that drop checks. This file creates facts, binds them
# (put_var/3) and asks those questions; it holds no fact algebra of its
# own.

# A comparison's relation (Facts.relation/3), from i64 operands computed
# without a check: a flagged strip computes on past a failed check, so a
Expand All @@ -5672,39 +5651,24 @@ defmodule Defk.Compiler do
# through ctx (may_raise?/1)
defp check_free?(%{c: c} = v), do: not may_raise?(v) and not (c =~ "defk_")

# `env` where relation `rel` is `true?` (Facts.holds/2): each fact on its
# newest atom, in that atom's binding (env.atoms and the i64 binding for a
# C variable, the array binding for a length), so a read of the binding
# and the prover both see it. The env is lexical: the facts end with the
# branch, filter or loop body they were made for.
# `env` where relation `rel` is `true?` (Facts.narrow/3): the facts
# scope, and the bindings whose facts it narrowed, so a read of the
# binding and the prover both see them. The env is lexical: the facts end
# with the branch, filter or loop body they were made for.
defp narrow(env, rel, true?) do
rel
|> Facts.holds(true?)
|> Enum.reduce(env, fn d, env ->
{x, kind, b} = Facts.narrowing(d)
narrow_atom(env, x, kind, b)
end)
end
facts = Facts.narrow(env.facts, rel, true?)

# a product's fact goes on the binding of its newer factor
defp narrow_atom(env, {:mul, y, _} = x, kind, b), do: narrow_on(env, y, x, kind, b)
defp narrow_atom(env, x, kind, b), do: narrow_on(env, x, x, kind, b)

defp narrow_on(env, {:var, c}, x, kind, b) do
atoms = env[:atoms] || %{}
f = Facts.facts(Facts.narrow(%{facts: atoms[c] || Facts.none()}, x, kind, b))

Map.merge(env, %{atoms: Map.put(atoms, c, f), vars: narrow_vars(env.vars, c, x, kind, b)})
end
vars =
Map.new(env.vars, fn
{n, %{c: c} = v} = kv ->
f = Facts.facts_of(facts, c)
if f == Facts.facts_of(env.facts, c), do: kv, else: {n, Facts.put(v, f)}

defp narrow_on(env, {:len, c}, x, kind, b),
do: %{env | vars: narrow_vars(env.vars, c, x, kind, b)}
kv ->
kv
end)

defp narrow_vars(vars, c, x, kind, b) do
Map.new(vars, fn
{n, %{c: ^c} = v} -> {n, Facts.narrow(v, x, kind, b)}
kv -> kv
end)
%{env | facts: facts, vars: vars}
end

# A raising guard: the statements after `if c` see the condition of the
Expand Down Expand Up @@ -5760,7 +5724,7 @@ defmodule Defk.Compiler do
# records its strip row (srec_proven/4); either verdict is noted
# (note_bounds/4). The site keeps its own C templates for the two forms.
defp access(kind, node, a, i, w, env) do
proven = Facts.check(a, i, w, env)
proven = Facts.check(a, i, w, env.facts)
if match?({:proven, _}, proven), do: srec_proven(kind, a, i, proven)
note_bounds(node, w, proven, {a, i, env})
match?({:proven, _}, proven)
Expand Down Expand Up @@ -6341,7 +6305,7 @@ defmodule Defk.Compiler do
{arr, idx} = {src_text(arr), src_text(idx)}

named = fn h, what ->
case Facts.residual(a, i, w, h, env) |> hint_text(env) do
case Facts.residual(a, i, w, h, env.facts) |> hint_text(env) do
nil -> what
fact -> "#{what} (it would follow from #{fact})"
end
Expand Down
Loading