[DanielLuning]

What changed

Stacked on #79 (defk-vcx.2): merge #79 first.

A gather-loop bench, bench/gather_layer.exs, lists the runtime checks a sparse layer keeps per term (an [f32] weight array, [i32] indices, r * k + t indexing, base + idx gathers, one [f32] store per row), with and without a raising guard for the shape. Read on today's compiler, most of the handwired study's list was already proven away (product facts, 6.37). One check was not for a reason of ranking: a condition's fact lands on its newest atom, and parameters ranked by their C names, so base <= length(x) was stored on the length of x and said nothing about base; base + idx[j] kept its overflow check.

The facts scope now carries the parameters' declaration order (Defk.Facts.scope/1), and the ranking reads it: newest/2, the prover's le?/walk, the product's canonical form (form_mul/3, mul_facts/3) and narrowing/2. A scope without an order (the unit tests' scopes) still ranks by name. The design doc already said "parameters first, by position"; ADR-0007 now says so too. docs/language.md (raising guards) tells users the rule: a condition between two arguments bounds the one declared later, so declare an offset after the array it is compared with.

What stays in the gather loop is about array contents (the bounds check of the gather itself, the finite checks on [f32] reads, the non-finite checks on the float multiply and add, the f32 range check on the store), which ADR-0007 keeps out of scope; the loop runs flagged, so each is a flag update, not a branch. The table is in docs/performance.md 6.45.

Results

• The gate (mix dump_c both sides, 113 modules): one module's C changed, Defk.ProductFactsTest.K, which lost one range-limit test on a loop bound; no kernel gained a check; the catalog's bounds (3,301) and overflow (6,050) call sites are unchanged. The report's product hint now names the factors in declaration order (n * dim <= length(m), was dim * n); the one test that read it is updated.
• The guarded gather loop: 0.012 / 0.012 us per row of 16 terms on the branch against 0.018 / 0.014 on main (two interleaved runs a side, quiet, other CPU 0.1-0.7 cores), about 0.75 ns per term where it was 0.9-1.1. The unguarded kernel, whose C did not change, 0.018 on both.
• Compiler time (two interleaved mix dump_c rounds a side): +0.5% of the work (reductions; +0.3% without SatEx.Kernels), +0.8% of the time (-0.3% without). The ADR-0007 chain is at about +4.0% (-1.9% without SatEx.Kernels) of the work before step 1, under its ceiling.

How it was checked

mix ci on the M-series laptop: 2309 passed, 817 excluded. New tests in test/condition_facts_test.exs ("a guard between two parameters"): the gather with both name orders drops the overflow check and keeps the gather's bounds check, the extremes of the dropped check (an i32 extreme with the offset at 0 and at the length: the sum fits, the access raises), the guard's raises, and the agreement properties of both kernels. test/product_facts_test.exs: the hint text's factor order.

• Touches a promised surface? No: the kernel subset's meaning is unchanged (a check dropped by a proof raises nowhere it did before); the report's fact text grows, which docs/guides/stability.md allows. No CHANGELOG.md entry.
• Touches test/stability/? No.