Issue #770: Invariants over every slot of a table: array smashing as a strategy of ADR-361 D5 (prepare decision)

Open and answer this issue on GitHub.

decision · opened 2026-10-20 · updated 2026-10-20 · 1 comment

How it came up

The check analysis of benches/brc/fast.nika (0.0.1150, topic 4 of the owner’s decision round on 0.0.1151–0.0.1153) found two overflow checks a row (2.0 instructions): count += 1 and sum += temp on fields of a slot in the program’s own table (self.slots[at].count). ADR-367 bounds counters only in a grammar fold’s accumulator. Proving these checks needs a fact about every slot, such as “each slot’s count is at most the position reached”, which neither the walk nor ADR-361’s strategies (closed forms, intervals) can state today.

The owner chose a ladder:

1. Now, with no compiler work: try in fast.nika a struct rule (ADR-369) assert(count <= 1 << 40) together with one length check per file (assert(buf.len() <= 1 << 40)). This should prove count + 1 and sum + temp, and leave one check (the rule’s) a row instead of two. If the prover does not use the rule for overflow goals, that is a defect to fix. Try it after #714 is complete.
2. This issue: prepare a decision on a strategy that finds such invariants itself, with nothing written by the program (ADR-361 D3).
3. Not pursued: quantified invariants and ghost variables written by the program, as in Dafny and SPARK.

What to prepare

1. How others do it, checked against their documentation:
   • Dafny: invariant forall i :: … plus ghost var, written by the user;
   • SPARK: pragma Loop_Invariant (for all …), generated frame conditions, bounded subtypes;
   • Astrée and Frama-C/EVA: array smashing with weak updates, found automatically;
   • array partitioning (Cousot, Cousot and Logozzo 2011) and its cost;
   • Clousot.
2. The strategy for Nikaia, as a D5 strategy under prove-through-loops:on (ADR-361 D10):
   • all elements of a Vec of structs are one summary per field;
   • a write to one element is a weak update (the summary holds the old value or the new);
   • the summary is related to the loop’s scalars, so that count - pos <= 0 is an octagon.

   sum needs |sum| <= 999 · pos, a linear relation with a coefficient (polyhedra or templates). Say which of the two is needed and what each costs.

3. The parallel case: the per-worker tables are merged at the end. A rule in the manner of ADR-367 is needed: the input length is compared once before the fold, and the pieces add up to at most the whole input.
4. Measurements:
   • What the strategy costs when lowering std and the tools (ADR-361 D8’s criterion: at most 5 % more instructions).
   • What it saves: fast.nika (2.0 a row), plus a histogram and a group-by over a Vec of structs written for the purpose.
5. Options, consequences, a recommendation, and a draft ADR (a new D in ADR-361, or its own record) for the owner’s round.

Depends on #767 (prove-through-loops). Nothing waits on it for 1BRC’s comparison; the motivation is the general pattern of counters and sums per key.

Comments

keywan-ghadami, 2026-10-20

State as of 0.0.1174:

• Decided: ADR-361 D11, extended to carry the summary across a fold’s step and merge.
• Built: a proved index is written without its check (0f20f5a). It gains nothing in fast.nika, because LLVM had already removed those checks.
• Where fast.nika stands: 107.5 instructions a row (16 units, x86-64), against fast-unsafe.nika at 104.0. The only difference is the overflow checks on sum += v and count += 1 in run; with overflow checks off, fast.nika counts 104.1.

Blocked: D11 over fast.nika’s hand-written Par::fold. Three questions are not settled by ADR-361 or ADR-367:

1. What a turn is. In a fold whose step is a method, a turn is a whole piece, and count grows inside run’s find_all loop. ADR-367 D1 defines a step count only for grammar folds.
2. The tail copy. scan runs run again over a zero-padded copy of up to n - cut + MARGIN bytes, and nothing bounds the number of pieces par_pieces makes. A bound taken from bytes can therefore exceed i64.
3. The sum. |v| <= 1023 times about 2^60 does not fit an i64. It needs ADR-367 D4’s length test before the fold, which is decided only for grammar folds.

The grammar-fold case, a step that does self.slots[k].count += 1, can be built without these answers: record element-field writes as sites in fold_bound.rs. It proves nothing in fast.nika. With the gap at 3.5 instructions a row, this waits.

---

Generated by Claude Code

Back to Open Issues