Open and answer this issue on GitHub.
ready · opened 2026-10-31 · updated 2026-10-31 · 0 comments
agent: builder model: opus max_turns: 100 budget_usd: 20 — Facts: Where things live, Traps already met, Commands
Part of #1053 (claim (b), prover lane). The brief is written and tracked: docs/briefs/prover/p13-1053-sequence-counts.md (probe, locations, steps with tests, rules, report path). A builder starts on it as is; the probe there was run on the 2026-10-31 21:11 binary, so re-run it first.
A std ledger entry whose result is a Seq may carry ensures_count = [...] (facts over count, self.len() and the parameters). The bounds walk reads them where the count becomes a length: a collect() written right after the producer, .count() right after it, and the turns of a for over it, when no write to self stands between (as ensures_each, ADR-375 D5). Entries: str::split, str::rsplit ["1 <= count", "count <= self.len() + 1"]; String::chars ["count <= self.len()", "self.len() <= 4 * count"]; String::bytes ["count == self.len()"]; nothing for splitn.
fn h(path: String) -> String {
let parts: Vec[String] = path.split(".").collect()
return parts[0].to_string() // checked today; proved after
}
fn main() { println(h("x.y")) }nikaia check --bounds: parts[0] is checked: no fact bounds what it reads.
ensures_count parsed (ledger.nika), kept (ty.nika), written back (ledger_text.nika); the three entries in crates/nikaia-std/std.contracts.collect() / .count() (bounds_matched.nika, bounds_walk.nika bounding_built), and 3. at a for over the producer (D13 turns). Test tests/compiler/tests/sequence_count_facts.nika with .stdout, .bounds, .loops.bounds.lower-std --bounds --asserts + scripts/proved.nika), docs/formal-verification.md §2, Part III optimization paragraph sentence (in the brief).scripts/proved.nika stops counting a panic( inside a string literal (modules.nika :496): the figure reads 2 panics, not 3.As in docs/briefs/common.part. Report to docs/briefs/prover/p13-1053-sequence-counts.md.report.md.
Generated by Claude Code