[DanielLuning]

What changed

Defk.Facts now owns the range-facts scope. Before, the compiler kept i64 facts twice (on the binding and in env.atoms), and the provers read the compiler's env: env.atoms for i64 atoms and a scan of env.vars for array lengths.

• The scope: Facts.scope/0, bind/2, narrow/3 (a relation in) and facts_of/2. The scope keeps each i64 and array binding's facts by C variable. The env carries it under one key, env.facts.
• The provers: check/4, fits_i64?/2 and residual/5 take the scope instead of the env. env.atoms, atom_facts/2 and the fake carrier for Facts.narrow are gone. holds/2 and the per-atom narrowing are now private.
• Binding writes: put_var/3, the two array-copy sites, the kernel entry and the inline env each bind once into the scope. A nested block hands its scope out with its bindings.
• Range arithmetic: the arithmetic of the overflow check and the bitwise operators moves behind Facts (add_range/2, sub_range/2, bnot_facts/1, u64_bsr_facts/2). add, neg and bnot are private.
• The compiler's narrow/3: it calls Facts.narrow/3, then gives each binding whose entry changed the scope's facts. This keeps a binding's facts the same as its scope entry. These 15 lines stay in the compiler next to relation/3 and guarded/4, because only the compiler knows env.vars.
• The tests: the linear, condition and product facts tests read the access decision from the report (TestKit.bounds_proven?/2: there are bounds notes, and all are :dropped) where they read the C with a regex. One end-to-end C check stays per file (mix2, rolling_diff, scores). facts_test gains three scope tests: binding by C variable, a relation narrowing its newest atom so that the prover sees it, and a product narrowing its newer factor.
• The compiler map: the "range facts" row and the Facts bullet are updated.

Results

• mix dump_c of all 108 modules is byte-identical to main at 68c82a0. The only difference is the known path-hashed /* defk:loop scale_keep/2 */ key in Defk.ReportTest.Gen.c.
• No kernel's C changed, so no example was checked or measured.

How it was checked

• mix ci on the laptop (macOS) passed: 2297 tests, Credo found no issues, Dialyzer reported 0 errors. After that run, only a comment changed (format and compile checked again).

• mix dump_c without cc on an untouched main checkout and on the branch, compared with diff -r -I '^#define DEFK_HEADER_HASH '.

• Touches a promised surface? No: Defk.Facts is internal (@moduledoc false). No CHANGELOG.md entry.

• Touches test/stability/? No.