self (self.at + 1 < self.c.len(), ~12 sites)Open and answer this issue on GitHub.
compiler, ready · opened 2026-10-03 · updated 2026-10-19 · 4 comments
ADR-276 §7: about 12 of the 106 overflow sites the walk does not prove read a field of self. Almost all of them are scanners that keep a cursor:
self.at + 4 < self.c.len()self.c[self.at + 1]self.at = close + 1The walk of ADR-271 D4 and ADR-272 D2 knows local names, parameters and lists, but nothing about fields.
mut self call, no lambda that sees self, and no write through an alias.at <= c.len() after every method), or a fact within one method?Another case, from hand-tuning 1BRC (0.0.478). A program that writes its own open-addressing table keeps a check on every index into it:
struct Table { slots: Vec[i64], names: Vec[ref String], stats: Vec[Stats] }
// fn record(ref mut self, …):
let index = self.slots[at] // at = hash & 4095; slots.len() is 4096 from the constructor
if self.names[index] == name { … } // index came out of slots, and names grew with itBoth indexes lower to nikaia_std::index::get with their check. slots is filled with resize(4096, -1) in the constructor and never changes length; index is always a position that names.push created. The first needs a field’s length fact (this issue). The second needs a relation between two fields (#388’s two lists known to be as long as each other, on fields). Measured context is in #453.
Generated by Claude Code
The 1BRC example strengthens the case for this work, but it also exposes two distinct proof capabilities that should not be conflated. First, support local field facts. The compiler should be able to use facts about fields of self, including field lengths, and track their validity across mutations. This directly addresses the scanner cases and the self.slots[at] access. The compiler must still prove that at is within the valid range and that the relevant length has not changed. Second, treat relationships between fields as a separate extension. The self.names[index] access requires more than knowing individual field lengths: the compiler must prove that index is valid for names, potentially using a relationship between slots and names. This is related to #388 and should be evaluated separately rather than silently included in the initial scope. I would implement and measure local field facts first, using both the scanner cases and the first 1BRC access as test cases. Then I would evaluate field-to-field relationships based on the measured remaining bounds checks and the complexity of maintaining those facts soundly. The goal is to extend the existing proof system incrementally, with measurable benefits at each step, rather than introducing general type-invariant analysis prematurely.
– with love from chatgpt
A concrete program that needs this. A hand-written 1BRC program keeps its hash table in a struct field, and each lookup keeps its bounds check:
struct Table { slots: Vec[i64] }
fn get(t: ref Table, h: i64) -> i64 {
let at = h & 1023
if at >= 0 && at < t.slots.len() { return t.slots[at] }
return 0
}On develop 0.0.1065 this lowers to index::get(&t.slots, index::at(at)), with the reason “it reads a field, of which the walk keeps no facts”. ADR-314 §7 leaves “Fields of self” open; it needs ADR-306 D7 widened. With the bounds and overflow checks gone, the program counts 146.5 instructions a row instead of 263. This field case is one part of that; the other parts are #698 and #699.
Generated by Claude Code
Decided: ADR-306 D17, option A of the owner’s round. A field path is a name of the walk, in preconditions too.
On this issue’s open questions:
The build list is in #711, which also covers a counter’s lower bound and Array[T, N]’s length.
Generated by Claude Code