diff --git a/docs/agents/compiler-map.md b/docs/agents/compiler-map.md
index 0792bd18..10188b72 100644
--- a/docs/agents/compiler-map.md
+++ b/docs/agents/compiler-map.md
@@ -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` |
@@ -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`.
diff --git a/lib/defk/compiler.ex b/lib/defk/compiler.ex
index 702c7ab1..b5f3a66d 100644
--- a/lib/defk/compiler.ex
+++ b/lib/defk/compiler.ex
@@ -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,
@@ -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
@@ -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]
@@ -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
@@ -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")
@@ -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
@@ -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")
@@ -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]
@@ -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)
@@ -3615,11 +3596,8 @@ 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).
@@ -3627,7 +3605,7 @@ defmodule Defk.Compiler do
     # 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,
@@ -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
@@ -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
@@ -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)
@@ -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
diff --git a/lib/defk/facts.ex b/lib/defk/facts.ex
index 06fe6039..fe4b80d8 100644
--- a/lib/defk/facts.ex
+++ b/lib/defk/facts.ex
@@ -32,10 +32,9 @@ defmodule Defk.Facts do
   # wraps); a case guard's checked arithmetic flags and computes on, so the
   # compiler drops its exact form (inexact/1). An i64 value whose C is a C
   # variable is that atom (eq/1). An atom's facts are its binding's, found
-  # in the scope the compiler passes (its env: atoms for i64 bindings by C
-  # variable, vars for arrays): a binding is assigned in one place, or is a
-  # loop counter or an accumulator, whose facts hold wherever the binding is
-  # in scope, and an array never changes length. A fact whose atom is out of
+  # in the scope (bind/2): a binding is assigned in one place, or is a loop
+  # counter or an accumulator, whose facts hold wherever the binding is in
+  # scope, and an array never changes length. A fact whose atom is out of
   # scope finds no binding and proves nothing (sound, if weak).
   #
   # The prover (le?/4) decides `form <= 0` by replacing the newest monomial
@@ -61,6 +60,7 @@ defmodule Defk.Facts do
   @i64_min -0x8000000000000000
   @i64_max 0x7FFFFFFFFFFFFFFF
   @len_max 2 ** 61 - 1
+  @max_u64 0xFFFFFFFFFFFFFFFF
 
   # the prover's step budget per query (one step: one monomial replaced);
   # measured on the suite and the examples, see docs/performance.md
@@ -105,6 +105,39 @@ defmodule Defk.Facts do
   # flags an overflow and computes on
   def inexact(v), do: put(v, %{facts(v) | eq: nil})
 
+  # ----------------------------------------------------------- the scope --
+  # The provers' index of the bindings in scope: each i64 or array binding's
+  # facts by its C variable, which is what an atom names ({:var, c},
+  # {:len, c}). The compiler's env carries it and it is lexical like the
+  # env; a binding's value keeps the same facts as its entry. An entry
+  # outlives a shadowing binding, as the C variable is assigned once where
+  # it is in scope.
+
+  def scope, do: %{}
+
+  # the scope with binding v's facts
+  def bind(scope, %{t: :i64, c: c} = v), do: Map.put(scope, c, facts(v))
+  def bind(scope, %{t: {:arr, _}, c: c} = v), do: Map.put(scope, c, facts(v))
+  def bind(scope, _v), do: scope
+
+  def facts_of(scope, c), do: Map.get(scope, c, %__MODULE__{})
+
+  # the scope where relation rel is true? (holds/2): each fact on its
+  # newest atom, in that atom's binding (a product's, in its newer
+  # factor's)
+  def narrow(scope, rel, true?) do
+    rel
+    |> holds(true?)
+    |> Enum.reduce(scope, fn d, scope ->
+      {x, kind, b} = narrowing(d)
+      c = binding_of(x)
+      Map.put(scope, c, with_fact(facts_of(scope, c), x, kind, b))
+    end)
+  end
+
+  defp binding_of({:mul, {_, c}, _}), do: c
+  defp binding_of({_, c}), do: c
+
   # ------------------------------------------------------------- queries --
   # lo/hi/len_lo are the raw constant bounds; lo_of/hi_of fold the relative
   # bounds in, so they may know more. The split is load-bearing: a caller
@@ -254,13 +287,13 @@ defmodule Defk.Facts do
   # comparison, and both sides of an `and` that holds or an `or` that does
   # not. A disjunction and `!=` give nothing; a constant form (a test that
   # is always or never true) gives nothing either.
-  def holds(nil, _true?), do: []
-  def holds({:not, x}, true?), do: holds(x, not true?)
-  def holds({:and, x, y}, true), do: holds(x, true) ++ holds(y, true)
-  def holds({:or, x, y}, false), do: holds(x, false) ++ holds(y, false)
-  def holds({op, _, _}, _true?) when op in [:and, :or], do: []
+  defp holds(nil, _true?), do: []
+  defp holds({:not, x}, true?), do: holds(x, not true?)
+  defp holds({:and, x, y}, true), do: holds(x, true) ++ holds(y, true)
+  defp holds({:or, x, y}, false), do: holds(x, false) ++ holds(y, false)
+  defp holds({op, _, _}, _true?) when op in [:and, :or], do: []
 
-  def holds({:cmp, op, a, b}, true?) do
+  defp holds({:cmp, op, a, b}, true?) do
     op = if true?, do: op, else: negated_op(op)
 
     case op do
@@ -295,56 +328,41 @@ defmodule Defk.Facts do
     end
   end
 
-  # the carrier (a binding of atom x, or of a product's newer factor) with
+  # the facts f (of atom x's binding, or of a product's newer factor's) with
   # the fact `kind`, `b` added; a narrowed bound comes first, as it is the
   # one the branch is about
-  def narrow(carrier, {:mul, _, y}, kind, b) do
-    f = facts(carrier)
-
-    put(
-      carrier,
-      case kind do
-        :lo -> %{f | mlbs: cap([{y, {1, form_const(b)}} | f.mlbs])}
-        :hi -> %{f | mubs: cap([{y, {1, form_const(b)}} | f.mubs])}
-        :lb -> %{f | mlbs: cap([{y, b} | f.mlbs])}
-        :ub -> %{f | mubs: cap([{y, b} | f.mubs])}
-      end
-    )
+  defp with_fact(f, {:mul, _, y}, kind, b) do
+    case kind do
+      :lo -> %{f | mlbs: cap([{y, {1, form_const(b)}} | f.mlbs])}
+      :hi -> %{f | mubs: cap([{y, {1, form_const(b)}} | f.mubs])}
+      :lb -> %{f | mlbs: cap([{y, b} | f.mlbs])}
+      :ub -> %{f | mubs: cap([{y, b} | f.mubs])}
+    end
   end
 
-  def narrow(carrier, {:var, _}, kind, b) do
-    f = facts(carrier)
-
-    put(
-      carrier,
-      case kind do
-        :lo -> %{f | lo: either(f.lo, b, &max/2)}
-        :hi -> %{f | hi: either(f.hi, b, &min/2)}
-        :lb -> %{f | lbs: cap([b | f.lbs])}
-        :ub -> %{f | ubs: cap([b | f.ubs])}
-      end
-    )
+  defp with_fact(f, {:var, _}, kind, b) do
+    case kind do
+      :lo -> %{f | lo: either(f.lo, b, &max/2)}
+      :hi -> %{f | hi: either(f.hi, b, &min/2)}
+      :lb -> %{f | lbs: cap([b | f.lbs])}
+      :ub -> %{f | ubs: cap([b | f.ubs])}
+    end
   end
 
-  def narrow(carrier, {:len, _}, kind, b) do
-    f = facts(carrier)
-
-    put(
-      carrier,
-      case kind do
-        :lo -> %{f | len_lo: either(f.len_lo, b, &max/2)}
-        :hi -> %{f | len_ubs: cap([{1, form_const(b)} | f.len_ubs])}
-        :lb -> %{f | len_lbs: cap([b | f.len_lbs])}
-        :ub -> %{f | len_ubs: cap([b | f.len_ubs])}
-      end
-    )
+  defp with_fact(f, {:len, _}, kind, b) do
+    case kind do
+      :lo -> %{f | len_lo: either(f.len_lo, b, &max/2)}
+      :hi -> %{f | len_ubs: cap([{1, form_const(b)} | f.len_ubs])}
+      :lb -> %{f | len_lbs: cap([b | f.len_lbs])}
+      :ub -> %{f | len_ubs: cap([b | f.len_ubs])}
+    end
   end
 
   # ------------------------------------------------------------- proving --
   # The only functions whose answers may drop a check. A proof carries its
   # support: the C variables of the atoms it reasoned about, which the
-  # flagged-strip classifier must see (ADR-0007). `scope` is the compiler's
-  # env: where an atom's facts are (atom_facts/2).
+  # flagged-strip classifier must see (ADR-0007). `scope` is where an
+  # atom's facts are (bind/2).
 
   # a value within lo..hi needs no i64 overflow check
   def prove_i64(lo, hi),
@@ -494,21 +512,10 @@ defmodule Defk.Facts do
   defp lookup(scope, a) do
     fn
       {:len, c} when a != nil and c == a.c -> facts(a)
-      m -> atom_facts(scope, m)
+      {_, c} -> facts_of(scope, c)
     end
   end
 
-  # scope: the compiler's env, whose atoms map an i64 binding's C variable
-  # to its facts, and whose vars hold the array bindings
-  defp atom_facts(scope, {:var, c}), do: (scope[:atoms] || %{})[c] || %__MODULE__{}
-
-  defp atom_facts(scope, {:len, c}) do
-    Enum.find_value(scope[:vars] || %{}, %__MODULE__{}, fn
-      {_, %{c: ^c, t: {:arr, _}} = b} -> facts(b)
-      _ -> nil
-    end)
-  end
-
   # Prove c * v + rest <= 0 for a value v (c = 1 or -1): v is replaced by
   # each of its bounds in c's direction, then by its constant bound, then by
   # its exact form, and the form left is handed to the prover. Gives
@@ -908,7 +915,12 @@ defmodule Defk.Facts do
     }
   end
 
-  # every value of a * b, with the bounds the relative facts give (lo_of, hi_of)
+  # every value of a + b, a - b and a * b, with the bounds the relative
+  # facts give (lo_of, hi_of)
+  def add_range(a, b), do: {add(lo_of(a), lo_of(b)), add(hi_of(a), hi_of(b))}
+
+  def sub_range(a, b), do: {add(lo_of(a), neg(hi_of(b))), add(hi_of(a), neg(lo_of(b)))}
+
   def mul_range(a, b), do: mul_bounds({lo_of(a), hi_of(a)}, {lo_of(b), hi_of(b)})
 
   defp mul_bounds({a1, a2}, {b1, b2})
@@ -1031,16 +1043,22 @@ defmodule Defk.Facts do
     end
   end
 
+  # a u64 shifted right by a literal k in 0..63
+  def u64_bsr_facts(a, k), do: %__MODULE__{lo: 0, hi: Bitwise.bsr(hi(a) || @max_u64, k)}
+
+  # bnot reverses the order: ~x = -x - 1
+  def bnot_facts(a), do: %__MODULE__{lo: bnot(hi(a)), hi: bnot(lo(a))}
+
   # 2^k - 1 for the bit length k of h >= 0: every value of at most k bits
   defp ones(h), do: Bitwise.bsl(1, length(Integer.digits(h, 2))) - 1
 
-  def bnot(x) when is_integer(x), do: -x - 1
-  def bnot(_), do: nil
+  defp bnot(x) when is_integer(x), do: -x - 1
+  defp bnot(_), do: nil
 
-  def add(x, y), do: both(x, y, &+/2)
+  defp add(x, y), do: both(x, y, &+/2)
 
-  def neg(x) when is_integer(x), do: -x
-  def neg(_), do: nil
+  defp neg(x) when is_integer(x), do: -x
+  defp neg(_), do: nil
 
   # a value's exact form as a bound, when it has atoms (a constant one is
   # its lo and hi)
diff --git a/test/condition_facts_test.exs b/test/condition_facts_test.exs
index 6693575e..236e2adc 100644
--- a/test/condition_facts_test.exs
+++ b/test/condition_facts_test.exs
@@ -143,7 +143,14 @@ defmodule Defk.ConditionFactsTest do
   use Defk.Properties
 
   import Defk.TestKit,
-    only: [kernel_c: 2, bounds_check_free?: 2, kept_bounds: 2, eval_ops: 2, fits_i64?: 1]
+    only: [
+      kernel_c: 2,
+      bounds_check_free?: 2,
+      bounds_proven?: 2,
+      kept_bounds: 2,
+      eval_ops: 2,
+      fits_i64?: 1
+    ]
 
   alias Defk.ConditionFactsTest.K
 
@@ -161,8 +168,9 @@ defmodule Defk.ConditionFactsTest do
 
   describe "a raising guard and an if arm: a rolling window" do
     test "x[i - w] keeps no bounds check after a raise when w < 1" do
+      assert bounds_proven?(K, :rolling_diff)
+      # end to end: the C calls no checked access
       assert bounds_check_free?(K, "rolling_diff")
-      assert kept(:rolling_diff) == []
 
       for x <- [[], [1], [1, 2, 3], Enum.to_list(1..3000)], w <- [1, 2, 3, 5000, @i64_max] do
         assert {:ok, _} = agrees(:rolling_diff, [f64s(x), w])
@@ -186,7 +194,7 @@ defmodule Defk.ConditionFactsTest do
 
   describe "a range start and a raising guard: a shifted block" do
     test "acc[i - m], acc[i] and bufs[i] keep no bounds check with m >= 0" do
-      assert bounds_check_free?(K, "shift_add")
+      assert bounds_proven?(K, :shift_add)
 
       for {acc, bufs} <- [{[], []}, {[1, 2, 3], [4, 5]}, {Enum.to_list(1..3000), [7, 8, 9]}],
           m <- [0, 1, 2, 3, 4000, @i64_max] do
@@ -235,7 +243,7 @@ defmodule Defk.ConditionFactsTest do
 
   describe "conditions narrow" do
     test "the later arms of a cond, by the earlier conditions' negations" do
-      assert bounds_check_free?(K, "clamped_get")
+      assert bounds_proven?(K, :clamped_get)
       x = G.pack(:i64, [4, 5, 6])
 
       for k <- [@i64_min, -1, 0, 2, 3, @i64_max] do
@@ -244,7 +252,7 @@ defmodule Defk.ConditionFactsTest do
     end
 
     test "the rest of a for after its filters" do
-      assert bounds_check_free?(K, "filtered")
+      assert bounds_proven?(K, :filtered)
       x = G.pack(:i64, [1, 2, 3, 4])
 
       for w <- [@i64_min, -1, 0, 1, 4, 5, @i64_max] do
@@ -253,7 +261,7 @@ defmodule Defk.ConditionFactsTest do
     end
 
     test "the right side of an and" do
-      assert bounds_check_free?(K, "positive_at")
+      assert bounds_proven?(K, :positive_at)
       x = G.pack(:i64, [1, -2])
 
       for k <- [@i64_min, -1, 0, 1, 2, @i64_max] do
@@ -262,7 +270,7 @@ defmodule Defk.ConditionFactsTest do
     end
 
     test "the statements after an if whose else arm raises" do
-      assert bounds_check_free?(K, "checked_get")
+      assert bounds_proven?(K, :checked_get)
       x = G.pack(:i64, [1, -2])
 
       for k <- [0, 1], do: assert({:ok, _} = agrees(:checked_get, [x, k]))
@@ -273,7 +281,7 @@ defmodule Defk.ConditionFactsTest do
     end
 
     test "the body of a range that runs, by its start <= stop" do
-      assert bounds_check_free?(K, "first_sum")
+      assert bounds_proven?(K, :first_sum)
 
       for n <- [-1, 0, 1, 2, 300] do
         assert {:ok, _} = agrees(:first_sum, [n])
diff --git a/test/facts_test.exs b/test/facts_test.exs
index ee8773aa..b8dd2c43 100644
--- a/test/facts_test.exs
+++ b/test/facts_test.exs
@@ -289,6 +289,50 @@ defmodule Defk.FactsTest do
              Facts.prove_in_bounds(a, Facts.put(%{c: "v_op_14"}, Facts.add_facts(three_j, three)))
   end
 
+  # ---------------------------------------------------------- the scope ----
+
+  test "the scope keeps an i64 or array binding's facts by its C variable" do
+    n = Facts.assert(%{t: :i64, c: "v_n_1"}, lo: 0, hi: 9)
+    a = Facts.assert(%{t: {:arr, :i64}, c: "p_a"}, len_lo: 3)
+    x = Facts.assert(%{t: :f64, c: "v_x_2"}, lo: 0)
+    scope = Facts.scope() |> Facts.bind(n) |> Facts.bind(a) |> Facts.bind(x)
+
+    assert Facts.facts_of(scope, "v_n_1") == Facts.facts(n)
+    assert Facts.facts_of(scope, "p_a") == Facts.facts(a)
+    assert Facts.facts_of(scope, "v_x_2") == Facts.none()
+    assert Facts.facts_of(scope, "v_y_3") == Facts.none()
+  end
+
+  test "a relation narrows its newest atom's binding, where the prover finds it" do
+    a = %{t: {:arr, :i64}, c: "p_a"}
+    k = %{t: :i64, c: "v_k_1"}
+    zero = Facts.assert(%{t: :i64, c: "0"}, lo: 0, hi: 0)
+    len = Facts.len_value(%{t: :i64, c: "(int64_t)p_a_len"}, a, true)
+    scope = Facts.scope() |> Facts.bind(a) |> Facts.bind(k)
+    assert {:unproven, :both} = Facts.check(a, k, 1, scope)
+
+    # 0 <= k and k < length(a)
+    rel = {:and, Facts.relation(:>=, k, zero), Facts.relation(:<, k, len)}
+    narrowed = Facts.narrow(scope, rel, true)
+    assert {:proven, support} = Facts.check(a, k, 1, narrowed)
+    assert "v_k_1" in support
+    assert Facts.facts_of(narrowed, "p_a") == Facts.facts_of(scope, "p_a")
+
+    # the negation of an and is a disjunction: nothing
+    assert Facts.narrow(scope, rel, false) == scope
+  end
+
+  test "a product's relation narrows the binding of its newer factor" do
+    m = %{t: {:arr, :f32}, c: "p_m"}
+    {r, d} = {%{t: :i64, c: "v_r_1"}, %{t: :i64, c: "v_d_2"}}
+    rd = Facts.put(%{t: :i64, c: "v_op_3"}, Facts.mul_facts(r, d))
+    len = Facts.len_value(%{t: :i64, c: "(int64_t)p_m_len"}, m, true)
+    scope = Facts.narrow(Facts.scope(), Facts.relation(:<=, rd, len), true)
+
+    assert Facts.facts_of(scope, "v_d_2") != Facts.none()
+    assert Facts.facts_of(scope, "v_r_1") == Facts.none()
+  end
+
   # ------------------------------------------------- the carry protocol ----
 
   property "weaken drops exactly what carries? reports" do
diff --git a/test/linear_facts_test.exs b/test/linear_facts_test.exs
index d1c8689c..d3385999 100644
--- a/test/linear_facts_test.exs
+++ b/test/linear_facts_test.exs
@@ -104,7 +104,7 @@ defmodule Defk.LinearFactsTest do
   use ExUnit.Case, async: true
   use Defk.Properties
 
-  import Defk.TestKit, only: [kernel_c: 2, bounds_check_free?: 2]
+  import Defk.TestKit, only: [kernel_c: 2, bounds_check_free?: 2, bounds_proven?: 2]
 
   alias Defk.LinearFactsTest.K
 
@@ -113,14 +113,16 @@ defmodule Defk.LinearFactsTest do
   @i64_min -0x8000000000000000
   @i64_max 0x7FFFFFFFFFFFFFFF
 
-  defp check_free?(name), do: bounds_check_free?(K, name)
+  defp proven?(kernel), do: bounds_proven?(K, kernel)
 
   defp agrees(fun, args),
     do: Defk.Test.assert_agrees(K, fun, args, forced_yields: true)
 
   describe "alloc(e, n) has length n" do
     test "out[i], a[i] and b[i] keep no bounds check for n = min(length(a), length(b))" do
-      assert check_free?("mix2")
+      assert proven?(:mix2)
+      # end to end: the C calls no checked access
+      assert bounds_check_free?(K, "mix2")
 
       for {a, b} <- [{[], []}, {[2], []}, {[1, 3, -5], [3, 1]}, {Enum.to_list(1..3000), [7]}] do
         {a, b} = {G.pack(:i16, a), G.pack(:i16, b)}
@@ -131,7 +133,7 @@ defmodule Defk.LinearFactsTest do
 
   describe "a block at a variable offset" do
     test "bufs[base + i] and sums[i] keep no bounds check, and base + i no overflow check" do
-      assert check_free?("add_blocks")
+      assert proven?(:add_blocks)
       refute kernel_c(K, "add_blocks") =~ ~r/defk_add_i64\([^;]*v_base_\d+ *,/
       assert kernel_c(K, "add_blocks") =~ ~r/\(v_base_\d+ \+ v_i_\d+\)/
     end
@@ -153,7 +155,7 @@ defmodule Defk.LinearFactsTest do
 
   describe "a range counting down" do
     test "out[n - 1 - i] and a[i] keep no bounds check" do
-      assert check_free?("reverse")
+      assert proven?(:reverse)
 
       for a <- [[], [1], [1, 2, 3], Enum.to_list(1..3000)] do
         assert {:ok, _} = agrees(:reverse, [G.pack(:i64, a)])
@@ -161,7 +163,7 @@ defmodule Defk.LinearFactsTest do
     end
 
     test "a step of -2 from min(k, length(a) - 1) keeps no bounds check" do
-      assert check_free?("odd_down")
+      assert proven?(:odd_down)
       a = G.pack(:i64, [1, 2, 3, 4, 5])
 
       for k <- [@i64_min, -1, 0, 1, 2, 4, 5, 100, @i64_max] do
@@ -172,7 +174,7 @@ defmodule Defk.LinearFactsTest do
 
   describe "the value of a branch" do
     test "keeps the bound every arm shares" do
-      assert check_free?("head")
+      assert proven?(:head)
 
       for flag <- [0, 1], {a, b} <- [{[], []}, {[1, 2], [5]}, {[1, 2, 3], [4, 5, 6, 7]}] do
         assert {:ok, _} = agrees(:head, [G.pack(:i64, a), G.pack(:i64, b), flag])
@@ -194,7 +196,7 @@ defmodule Defk.LinearFactsTest do
 
   describe "an offset argument" do
     test "a[x + i] keeps no bounds check, and x + i no overflow check" do
-      assert check_free?("window")
+      assert proven?(:window)
       refute kernel_c(K, "window") =~ "defk_add_i64(ctx, v_x"
 
       for x <- [@i64_min, -1, 0, 1, 3, 7, 8, @i64_max] do
diff --git a/test/product_facts_test.exs b/test/product_facts_test.exs
index 05125750..d2800393 100644
--- a/test/product_facts_test.exs
+++ b/test/product_facts_test.exs
@@ -108,7 +108,14 @@ defmodule Defk.ProductFactsTest do
   use Defk.Properties
 
   import Defk.TestKit,
-    only: [bounds_check_free?: 2, eval_ops: 2, fits_i64?: 1, kernel_c: 2, kept_bounds: 2]
+    only: [
+      bounds_check_free?: 2,
+      bounds_proven?: 2,
+      eval_ops: 2,
+      fits_i64?: 1,
+      kernel_c: 2,
+      kept_bounds: 2
+    ]
 
   alias Defk.ProductFactsTest.K
 
@@ -128,8 +135,9 @@ defmodule Defk.ProductFactsTest do
 
   describe "a row-major index with a runtime row length" do
     test "the shape from div: no bounds or overflow check on m[r * dim + j]" do
+      assert bounds_proven?(K, :scores)
+      # end to end: the C calls no checked access
       assert bounds_check_free?(K, "scores")
-      assert kept(:scores) == []
       refute kernel_c(K, "scores") =~ ~r/defk_(add|mul)_i64\(ctx, v_r_/
 
       for {n, dim, extra} <- [{0, 1, 0}, {1, 1, 0}, {3, 4, 0}, {3, 4, 3}, {50, 7, 6}, {0, 5, 4}] do
@@ -146,7 +154,7 @@ defmodule Defk.ProductFactsTest do
     end
 
     test "the shape from a raising guard, length(m) == n * dim" do
-      assert bounds_check_free?(K, "scores_guarded")
+      assert bounds_proven?(K, :scores_guarded)
       refute kernel_c(K, "scores_guarded") =~ ~r/defk_(add|mul)_i64\(ctx, v_r_/
 
       for {n, dim} <- [{1, 1}, {3, 4}, {40, 9}] do
@@ -162,8 +170,7 @@ defmodule Defk.ProductFactsTest do
     end
 
     test "the PCM mixer's sum loop: no bounds check" do
-      assert bounds_check_free?(K, "sum_blocks")
-      assert kept(:sum_blocks) == []
+      assert bounds_proven?(K, :sum_blocks)
 
       for {n, m, held} <- [{1, 0, []}, {1, 3, [5]}, {4, 5, [1, 2]}, {3, 100, Enum.to_list(1..9)}],
           extra <- [0, 2] do
@@ -177,7 +184,7 @@ defmodule Defk.ProductFactsTest do
     end
 
     test "a divisor of either sign" do
-      assert bounds_check_free?(K, "row_sums")
+      assert bounds_proven?(K, :row_sums)
       m = G.pack(:i64, Enum.to_list(1..12))
 
       for d <- [@i64_min, -13, -5, -1, 1, 2, 5, 12, 13, @i64_max] do
@@ -188,7 +195,7 @@ defmodule Defk.ProductFactsTest do
     end
 
     test "column-major, through the product of the counter and the row count" do
-      assert bounds_check_free?(K, "col_sums")
+      assert bounds_proven?(K, :col_sums)
 
       for len <- [0, 1, 11, 12], d <- [1, 2, 5, 12, 13, 1000] do
         assert {:ok, _} = agrees(:col_sums, [G.pack(:i64, Enum.to_list(1..len//1)), d])
diff --git a/test/support/test_kit.ex b/test/support/test_kit.ex
index c6bc0f52..9e193dd5 100644
--- a/test/support/test_kit.ex
+++ b/test/support/test_kit.ex
@@ -122,6 +122,16 @@ defmodule Defk.TestKit do
   @doc "The texts of kernel `name`'s kept bounds checks."
   def kept_bounds(mod, name), do: for({:kept, text} <- notes(mod, name, :bounds), do: text)
 
+  @doc """
+  The prover dropped every bounds check of kernel `name` in `mod`: its
+  report has bounds notes, and each one is :dropped. The decision, where
+  bounds_check_free?/2 reads the C.
+  """
+  def bounds_proven?(mod, name) do
+    verdicts = for {verdict, _} <- notes(mod, name, :bounds), do: verdict
+    verdicts != [] and Enum.all?(verdicts, &(&1 == :dropped))
+  end
+
   # ------------------------------------------------ soundness properties --
   # The range-fact soundness properties compile generated kernels and check
   # each dropped check against the arithmetic, evaluated here.