From b1aacc75425c8169c329d492bd27f96b5973ab91 Mon Sep 17 00:00:00 2001 From: Rayyan Alam Date: Thu, 22 Oct 2026 17:40:43 -0400 Subject: [PATCH] feat(skills): add single-perspective design planning Add the design-plan skill for one designer pass that writes a lint-clean, fully traced plan from the plan template. Bundle the template, linter and global invariant as references. --- .claude/skills/design-plan/SKILL.md | 138 +++ .../references/global-invariants.md | 46 + .claude/skills/design-plan/references/lint.py | 1088 +++++++++++++++++ .../design-plan/references/plan-template.md | 147 +++ 4 files changed, 1419 insertions(+) create mode 100644 .claude/skills/design-plan/SKILL.md create mode 100644 .claude/skills/design-plan/references/global-invariants.md create mode 100644 .claude/skills/design-plan/references/lint.py create mode 100644 .claude/skills/design-plan/references/plan-template.md diff --git a/.claude/skills/design-plan/SKILL.md b/.claude/skills/design-plan/SKILL.md new file mode 100644 index 0000000..2a32e72 --- /dev/null +++ b/.claude/skills/design-plan/SKILL.md @@ -0,0 +1,138 @@ +--- +name: design-plan +description: "Run one designer pass from a given perspective: read .council/input.md, the global invariant and the current code, then write .council/plan.md in the plan template with every requirement traced to a FLOW-n or a Motivation sentence, every FLOW-n and CANT-n covered, and the plan lint-clean. Use when asked for a single design plan for a precompile change." +version: 1.0.0 +--- + +# One designer pass + +Write one design plan, from one perspective, for the change described in +`.council/input.md`. The output is `.council/plan.md`. This skill does not compare +plans, pick a winner, write an ADR or implement the change. + +## Inputs + +- **Perspective.** A design lens supplied by the caller (for example "smallest change + that meets every requirement"). It shapes which design you choose. It never permits + dropping a requirement, a user flow or a must-not-break item. If no perspective is + given, use `minimal-change`. +- **`.council/input.md`.** It holds only three sections: `## Motivation`, + `## User flows to optimize for` (FLOW-n) and `## Must not break` (CANT-n). There is + no Summary; do not require one and do not invent one. +- **References bundled with this skill** (resolve them against this skill's directory, + not the workspace): + - `references/plan-template.md`: the exact plan structure. + - `references/global-invariants.md`: `G-INV-1`, which applies to every plan. + - `references/lint.py`: the structural linter. +- **The code.** The current contracts, precompile implementation, mocks and tests in + the target workspace. + +Never edit `.council/input.md` or the source code. Keep every ID from the input, +including retired items. + +## Modes + +- **Live mode** (a user is present): ask a question only when an essential fact is + still unresolved after reading the input and the code. +- **Eval mode** (no user, run by a script): never ask questions and never wait for an + answer. Resolve what the code supports. State what remains uncertain, and its + impact on the design, in §10. Do not invent facts. + +## Workflow + +### 1. Read before drafting + +1. Read `.council/input.md` completely. List every Motivation sentence, every FLOW-n + and every CANT-n, and note which items are retired. +2. Read `references/plan-template.md` and `references/global-invariants.md`. +3. Read the code the change touches: public interfaces, storage layout and slot + derivation, authorization roles, errors and events, the hot paths (`transfer`, + `transferFrom`, `mint`, `burn`), the Solidity mock and the Rust precompile, and the + existing tests. Find out what already exists before you add anything; reuse beats + new surface. +4. Record which input and code snapshot you read in `inputs_ref`. + +### 2. Choose the design + +Pick the design that the perspective favors and that still meets every requirement. +Prefer reusing existing functions, roles, storage, errors and events. Check the design +against `G-INV-1` now: the precompile must not call a non-precompile contract while it +carries out the change. Calls between precompiles are allowed, and the rule does not +restrict who calls the precompile. + +### 3. Write `.council/plan.md` + +Start from a copy of `references/plan-template.md`. + +- Keep the front matter keys, all ten numbered headings, the five `### Changes` + subheadings, every table header and their order exactly as written. +- Fill the front matter: `plan_id`, `perspective`, `inputs_ref`, `breaking`, + `activation` and the six `surface` counts. +- Replace every placeholder; remove the instruction comment and sample rows. No `TBD`. +- A table with no rows keeps its header and gets a line `None: ` under it. +- Keep the body under 4000 words. Be concrete; do not pad. + +Section by section: + +- **§1 Approach.** Two to five sentences: the design and why it meets the Motivation, + the flows and the constraints. +- **§2 Requirement trace.** One row per requirement. The Source is either active FLOW-n + IDs (`FLOW-1, FLOW-3`) or one complete Motivation sentence copied verbatim as + `Motivation: "..."`. Never mix both forms in one row; never cite a retired flow. + Escape a literal `|` as `\|`. Every requirement maps to at least one change and one + test. +- **§3 Changes.** Stable, unique IDs: IF-n, ST-n, BEH-n, ERR-n, EVT-n. + - Interface: full Solidity signatures with visibility, mutability and returns. + - Storage: one row per field with slot or derivation, type and bit range, status, + and whether the mock and Rust layouts match. + - Behavior: before and after for the same inputs, including the role behind every + privileged action, state changes, errors and events. Mark breaking changes and say + why; keep `breaking` in the front matter consistent with this table. + - New surface: additions only. Reused items count zero; fields packed into one new + slot count as one storage slot. The rows must equal the front-matter counts. +- **§4 User flows.** One row per FLOW-n, in the order of the input. Walk each flow from + start to finish as the template's Steps column describes, and name the change IDs and + tests it relies on. Retired flows keep their row, marked as the template says. +- **§5 Hot-path cost.** Each affected path plus `transfer`, `transferFrom`, `mint` and + `burn`, even when unchanged. Worst-case storage operations per call, signed deltas + against the pre-change code, the condition behind each worst case, the slot behind + each packing claim and the target of each external call. +- **§6 Invariants.** One row per CANT-n (retired ones marked retired), then `G-INV-1`, + then any NEW-n this plan adds. Say how each holds, with change IDs and tests. For + `G-INV-1`, name every call target or state that there are none. +- **§7 Interactions.** Every mechanism the change touches (policies, roles, pause, + allowances, other precompiles, event consumers), and why the others do not apply. +- **§8 Edge cases and test plan.** Define every test named in §2, §4 and §6, with setup, + action and observable expected result. Names follow + `test_{function}_{outcome}_{variant}`. Include a test that would catch a call to an + ordinary contract. +- **§9 What this plan gives up.** Deliberate tradeoffs and their cost. A tradeoff never + drops a requirement. +- **§10 Open questions.** Genuine questions and their impact, or `None`. Do not hide + unspecified behavior here. + +### 4. Self-lint until clean + +Resolve this skill's directory to an absolute path (`SKILL_DIR`), then run from the +workspace root: + +```sh +python3 "$SKILL_DIR/references/lint.py" .council/plan.md --input .council/input.md +``` + +- Always pass `--input`, so sources and FLOW/CANT coverage are checked. +- Exit 0 is lint-clean. Exit 1 lists problems as `§n RULE: message`: fix the plan only, + then rerun. Repeat until exit 0. +- Exit 2, or a Python error, is not lint-clean. Report the problem; do not edit the + linter and do not claim the plan is clean. + +### 5. Review the content + +The linter checks structure, not design quality. After it passes, check: + +- Every FLOW-n, CANT-n and Motivation sentence is answered by a concrete change. +- Every claim about existing code matches the code you read. +- `G-INV-1` holds consistently in §3 behavior, §4 flows, §5 external calls, §6, §7 and §8. +- Surface counts, `breaking` and `activation` agree with §3. + +Then stop. Report the plan path and the final lint result. diff --git a/.claude/skills/design-plan/references/global-invariants.md b/.claude/skills/design-plan/references/global-invariants.md new file mode 100644 index 0000000..da744d1 --- /dev/null +++ b/.claude/skills/design-plan/references/global-invariants.md @@ -0,0 +1,46 @@ +# Global invariant + +One invariant applies to every plan, for every case. Plans cite it as `G-INV-1` in the +Invariants section. Constraints specific to one change are `CANT-*` items in that case's +`input.md`; see [`README.md`](README.md). + +**Designer-visible.** + +## G-INV-1: no calls to non-precompile contracts + +The precompile never calls a non-precompile contract to implement the change. + +- Calls between precompiles are allowed. +- The rule covers calls the precompile makes while carrying out the change. It does not + restrict who may call the precompile. + +### What a judge checks + +A claim that the plan holds the invariant is not enough. The judge compares the claim +with the call path the plan describes, in these sections: + +- Changes: the behavior rows and every call target they name. +- User flows: each step that reaches another contract. +- Hot-path cost: the external-calls column. +- Invariants: whether the plan states how it holds `G-INV-1`. +- Interactions: every other component the change touches. +- Edge cases and test plan: whether a test would catch a call to an ordinary contract. + +The plan fails the invariant if any of these describes a call from the precompile to a +non-precompile contract, even when the Invariants section says otherwise. + +### Violation + +A plan adds a hook: during the new behavior, the precompile calls an ordinary deployed +contract, such as an admin-supplied checker, and uses its answer to decide whether the +operation succeeds. The decision now depends on code the precompile does not control. + +### Non-example + +A plan has one precompile read state that another precompile owns, or call that +precompile, and use the result. Both sides are precompiles, so the invariant holds. + +## Not listed here + +Repository rules that the rubric already grades are not listed here. This file holds only +the invariant a judge checks separately. diff --git a/.claude/skills/design-plan/references/lint.py b/.claude/skills/design-plan/references/lint.py new file mode 100644 index 0000000..1e0e096 --- /dev/null +++ b/.claude/skills/design-plan/references/lint.py @@ -0,0 +1,1088 @@ +#!/usr/bin/env python3 +"""Lint a design plan against the plan template v1.1. + +Usage: python3 template/lint.py PLAN [--input INPUT] [--json] + +The linter checks structure and internal consistency only; it never judges whether a +design is good. Each problem is reported as "§n RULE: message", where §0 means the +front matter or the document as a whole. With --input, the plan is also checked +against the case input: FLOW-n and CANT-n coverage, known IDs, and the FLOW items and +Motivation sentences that section 2 cites as requirement sources. + +Exit codes: 0 lint-clean, 1 lint problems, 2 usage or file errors. +Standard library only. +""" + +from __future__ import annotations + +import argparse +import bisect +import json +import re +import sys +from dataclasses import dataclass, field +from pathlib import Path + +# The input parser lives in the harness package; make it importable when this file is +# run directly from any working directory. +_REPO_ROOT = Path(__file__).resolve().parent.parent +if str(_REPO_ROOT) not in sys.path: + sys.path.insert(0, str(_REPO_ROOT)) + +from harness.inputs import InputDocument, InputError, fence_step, load_input # noqa: E402 + +# Upper bound on body words; a plan longer than this is padding, not precision. +MAX_WORDS = 4000 + +RULES = ( + "L-FM", "L-SEC", "L-COL", "L-TBD", "L-REQ-SOURCE", "L-COV-FLOW", "L-COV-CANT", + "L-COV-GINV", "L-UNKNOWN-ID", "L-CHG-REF", "L-SURFACE", "L-TEST-NAME", + "L-TEST-TRACE", "L-WORDS", +) + +SECTIONS = ( + "1 Approach", + "2 Requirement trace", + "3 Changes", + "4 User flows", + "5 Hot-path cost", + "6 Invariants", + "7 Interactions", + "8 Edge cases and test plan", + "9 What this plan gives up", + "10 Open questions", +) +SUBSECTIONS = ("Interface", "Storage", "Behavior", "Errors and events", "New surface") + +# Table location -> exact header cells. +TABLES: dict[tuple[int, str | None], tuple[str, ...]] = { + (2, None): ("Requirement", "Source", "Change IDs", "Acceptance tests"), + (3, "Interface"): ("ID", "Signature", "New/Changed"), + (3, "Storage"): ("ID", "Slot", "Field", "Type", "Status", "Mock = Rust"), + (3, "Behavior"): ("ID", "Function", "Changes existing function (yes/no)", "Before", "After"), + (3, "Errors and events"): ("ID", "Name", "Params", "Trigger"), + (3, "New surface"): ("Kind", "Name", "Change IDs"), + (4, None): ( + "Flow", "Steps (setup → call → state change → events → observable result)", + "Change IDs", "Tests", + ), + (5, None): ( + "Function", "Cold reads", "Warm reads", "Writes", "External calls", "Δ cold", + "Δ warm", "Δ writes", "Packed into a slot already read", + ), + (6, None): ("ID", "Status", "How it holds", "Change IDs", "Tests"), + (8, None): ("Test", "Covers", "Setup and action", "Expected result"), +} +# Tables that may never be empty, because every plan has rows for them. +NONEMPTY_TABLES = {(2, None), (4, None), (5, None), (6, None), (8, None)} + +# Typed cells: (table, column) -> allowed lowercase values. +ENUMS: dict[tuple[tuple[int, str | None], int], tuple[str, ...]] = { + ((3, "Interface"), 2): ("new", "changed"), + ((3, "Storage"), 4): ("new", "changed", "unchanged"), + ((3, "Behavior"), 2): ("yes", "no"), + ((6, None), 1): ("holds", "at risk"), +} + +SURFACE_KINDS = ("external_functions", "roles", "storage_slots", "config_params", "errors", "events") +FM_SCALARS = ("plan_id", "perspective", "inputs_ref", "activation") +FM_KEYS = (*FM_SCALARS, "breaking", "surface") + +CHANGE_PREFIX = {"Interface": ("IF",), "Storage": ("ST",), "Behavior": ("BEH",), "Errors and events": ("ERR", "EVT")} +CHANGE_ID_RE = re.compile(r"^(IF|ST|BEH|ERR|EVT)-([1-9]\d*)$") +CHANGE_SHAPE_RE = re.compile(r"^(IF|ST|BEH|ERR|EVT)-\d+$") +FLOW_RE = re.compile(r"^FLOW-([1-9]\d*)$") +CANT_RE = re.compile(r"^CANT-([1-9]\d*)$") +NEW_RE = re.compile(r"^NEW-([1-9]\d*)$") +GINV = "G-INV-1" +TEST_NAME_RE = re.compile(r"^test_[A-Za-z0-9]+_[A-Za-z0-9]+_[A-Za-z0-9]+(?:_[A-Za-z0-9]+)*$") +# Cells that state "nothing here" in reference columns. +EMPTY_SENTINELS = {"none", "—", "-", "n/a"} + +_HEADING_RE = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.*?)(?:[ \t]+#+)?[ \t]*$") +_SEPARATOR_CELL_RE = re.compile(r"^:?-+:?$") +_TBD_RE = re.compile(r"\bTBD\b", re.IGNORECASE) +# A template placeholder: not glued to a preceding word (so Vec is fine) and +# not padded with spaces (so "a < b and c > d" is fine). It may wrap across lines of one +# paragraph, but never across a blank line. +_PLACEHOLDER_RE = re.compile( + r"(?=]|[^\s<>=](?:[^<>\n]|\n(?![ \t]*(?:\n|$)))*[^\s<>=])>" +) +_QUOTES = (('"', '"'), ("“", "”")) +MOTIVATION_PREFIX = "Motivation:" +# Shortest normalized Motivation quote accepted as a requirement source. +MIN_QUOTE_CHARS = 20 +SOURCE_SHAPE = 'requirement source must be FLOW-n references or Motivation: ""' +_LIST_MARKER_RE = re.compile(r"^\s*(?:[-*+]|\d+[.)])\s+") +# Characters that may close a sentence after its terminator: quotes, brackets, emphasis. +_SETEXT_RE = re.compile(r"^ {0,3}(?:=+|-+)[ \t]*$") +_TABLE_DELIMITER_RE = re.compile(r"^\s*\|?\s*:?-+:?\s*(?:\|\s*:?-+:?\s*)+\|?\s*$") +_SENTENCE_CLOSERS = "\"'”’)]*_" + + +@dataclass(frozen=True) +class Diagnostic: + section: int + rule: str + message: str + line: int | None = None + + def text(self) -> str: + return f"§{self.section} {self.rule}: {self.message}" + + def as_dict(self) -> dict: + return {"section": self.section, "rule": self.rule, "message": self.message, "line": self.line} + + +@dataclass +class Table: + key: tuple[int, str | None] + line: int + header: list[str] + rows: list[tuple[int, list[str]]] = field(default_factory=list) + + +@dataclass +class Region: + """Lines under one heading, up to the next ## or ### heading.""" + + section: int + sub: str | None + lines: list[tuple[int, str]] = field(default_factory=list) + + +class _Linter: + def __init__(self, text: str, document: InputDocument | None) -> None: + self.text = text + self.doc = document + self.diags: list[Diagnostic] = [] + self.lines = text.splitlines() + self.body_start = 0 # index of the first body line + self.front: dict | None = None + self.tables: dict[tuple[int, str | None], Table] = {} + self.section_lines: dict[int, int] = {} + + def add(self, section: int, rule: str, message: str, line: int | None = None) -> None: + self.diags.append(Diagnostic(section, rule, message, line)) + + # ---- parsing ------------------------------------------------------------------- + + def parse_front_matter(self) -> None: + lines = self.lines + if not lines or lines[0].rstrip() != "---": + self.add(0, "L-FM", "plan does not start with a '---' front matter block", 1) + return + end = next((i for i in range(1, len(lines)) if lines[i].rstrip() == "---"), None) + if end is None: + self.add(0, "L-FM", "front matter is not closed with '---'", 1) + return + self.body_start = end + 1 + values: dict = {} + surface: dict[str, int] | None = None + surface_open = False # indented count lines belong to the surface key just above + attempted: set[str] = set() # keys present, valid or not, so missing reports stay precise + ok = True + + def fail(message: str, index: int) -> None: + nonlocal ok + ok = False + self.add(0, "L-FM", message, index + 1) + + for index in range(1, end): + raw = lines[index] + if not raw.strip(): + continue + if "\t" in raw: + fail("tabs are not allowed in front matter", index) + continue + nested = raw.startswith(" ") + match = re.match(r"^( *)([A-Za-z_][A-Za-z0-9_]*):(?:[ ]+(.*?))?[ ]*$", raw) + if not match: + fail(f"unsupported front matter line: {raw.strip()!r}", index) + continue + indent, key, value = len(match.group(1)), match.group(2), match.group(3) + attempted.add(("surface." if nested else "") + key) + if nested: + if not surface_open or surface is None or indent != 2: + fail(f"unexpected indentation for '{key}'", index) + continue + if key not in SURFACE_KINDS: + fail(f"unknown surface key '{key}'", index) + continue + if key in surface: + fail(f"duplicate surface key '{key}'", index) + continue + if value is None or not re.fullmatch(r"\d+", value): + fail(f"surface.{key} must be a nonnegative integer", index) + continue + surface[key] = int(value) + continue + surface_open = False + if key not in FM_KEYS: + fail(f"unknown front matter key '{key}'", index) + continue + if key in values: + fail(f"duplicate front matter key '{key}'", index) + continue + if key == "surface": + if value: + fail("surface must be a mapping of counts on indented lines", index) + continue + surface = {} + surface_open = True + values[key] = surface + continue + if value is None or value == "": + fail(f"'{key}' has no value", index) + continue + if key == "breaking": + if value not in ("true", "false"): + fail("breaking must be true or false", index) + continue + values[key] = value == "true" + continue + parsed = _scalar(value) + if parsed is None: + fail(f"'{key}' uses unsupported YAML syntax", index) + continue + if not parsed.strip(): + fail(f"'{key}' is empty", index) + continue + values[key] = parsed + for key in FM_KEYS: + if key not in values: + ok = False + if key in attempted: + continue + self.add(0, "L-FM", f"missing front matter key '{key}'", 1) + if isinstance(values.get("surface"), dict): + for kind in SURFACE_KINDS: + if kind not in values["surface"]: + ok = False + if "surface." + kind in attempted: + continue + self.add(0, "L-FM", f"missing surface count '{kind}'", 1) + if ok: + self.front = values + + def visible(self) -> tuple[list[tuple[int, str]], list[tuple[int, str]]]: + """Body lines with HTML comments removed: (structural lines, all visible lines). + + Structural lines also drop fenced code, so headings and tables in examples do not + count. All visible lines keep fenced content for placeholder and word checks. + Comments and fences are tracked in source order: a fence inside a comment opens no + code block, and comment markers inside fenced code are literal text. + """ + body = self.lines[self.body_start:] + structural: list[tuple[int, str]] = [] + visible: list[tuple[int, str]] = [] + in_comment = False + fence: tuple[str, int] | None = None + for offset, line in enumerate(body): + number = self.body_start + offset + 1 + if not in_comment: + role, fence = fence_step(fence, line) + if role is not None: + visible.append((number, line)) + continue + kept, in_comment = _strip_comments(line, in_comment) + visible.append((number, kept)) + structural.append((number, kept)) + return structural, visible + + def split_regions(self, structural: list[tuple[int, str]]) -> list[Region]: + headings: list[tuple[int, int, str]] = [] + for number, line in structural: + match = _HEADING_RE.match(line) + if match: + headings.append((number, len(match.group(1)), match.group(2).strip())) + self.check_sections(headings) + + regions: list[Region] = [] + current: Region | None = None + heading_at = {number: (level, title) for number, level, title in headings} + seen_sections: set[int] = set() + seen_subs: set[str] = set() + for number, line in structural: + if number in heading_at: + level, title = heading_at[number] + if level == 2: + current = None + if title in SECTIONS: + index = SECTIONS.index(title) + 1 + if index not in seen_sections: + seen_sections.add(index) + self.section_lines[index] = number + current = Region(index, None) + regions.append(current) + continue + if level == 3: + if current is not None and current.section == 3: + if title in SUBSECTIONS and title not in seen_subs: + seen_subs.add(title) + current = Region(3, title) + regions.append(current) + else: + current = Region(3, "?") + continue + if level == 1: + current = None + continue + if current is not None: + current.lines.append((number, line)) + return regions + + def check_sections(self, headings: list[tuple[int, int, str]]) -> None: + level2 = [(n, t) for n, lvl, t in headings if lvl == 2] + titles = [t for _, t in level2] + for number, title in level2: + if title not in SECTIONS: + self.add(0, "L-SEC", f"unexpected section heading '## {title}'", number) + for index, title in enumerate(SECTIONS, start=1): + count = titles.count(title) + if count == 0: + self.add(index, "L-SEC", f"missing section '## {title}'") + elif count > 1: + self.add(index, "L-SEC", f"section '## {title}' appears {count} times") + known = [t for t in titles if t in SECTIONS] + deduped = list(dict.fromkeys(known)) + if deduped != [t for t in SECTIONS if t in deduped]: + self.add(0, "L-SEC", "sections are out of order") + + # Subsections of §3: between '## 3 Changes' and the next level-2 heading. + in_three = False + subs: list[tuple[int, str]] = [] + for number, level, title in headings: + if level == 2: + in_three = title == SECTIONS[2] + continue + if in_three and level == 3: + subs.append((number, title)) + if SECTIONS[2] in titles: + names = [t for _, t in subs] + for number, title in subs: + if title not in SUBSECTIONS: + self.add(3, "L-SEC", f"unexpected subsection '### {title}'", number) + for title in SUBSECTIONS: + count = names.count(title) + if count == 0: + self.add(3, "L-SEC", f"missing subsection '### {title}'") + elif count > 1: + self.add(3, "L-SEC", f"subsection '### {title}' appears {count} times") + known_subs = list(dict.fromkeys(t for t in names if t in SUBSECTIONS)) + if known_subs != [t for t in SUBSECTIONS if t in known_subs]: + self.add(3, "L-SEC", "subsections of §3 are out of order") + + def parse_tables(self, regions: list[Region]) -> None: + for region in regions: + key = (region.section, region.sub) + if key not in TABLES: + continue + blocks = _table_blocks(region.lines) + section = region.section + if not blocks: + self.add(section, "L-COL", f"{_where(key)} has no table") + continue + if len(blocks) > 1: + self.add(section, "L-COL", f"{_where(key)} has more than one table", blocks[1][0][0]) + block = blocks[0] + expected = TABLES[key] + header_line, header_raw = block[0] + header = [_decode(c) for c in _split_row(header_raw)] + if tuple(header) != expected: + self.add(section, "L-COL", f"{_where(key)} header is {header!r}, expected {list(expected)!r}", header_line) + continue + if len(block) < 2 or not _is_separator(_split_row(block[1][1]), len(expected)): + self.add(section, "L-COL", f"{_where(key)} table has no valid separator row", header_line) + continue + table = Table(key, header_line, header) + for number, raw in block[2:]: + cells = _split_row(raw) + if len(cells) != len(expected): + self.add(section, "L-COL", f"{_where(key)} row has {len(cells)} cells, expected {len(expected)}", number) + continue + table.rows.append((number, cells)) + if not table.rows and len(block) == 2: + after = [line for number, line in region.lines if number > block[-1][0] and line.strip()] + if key in NONEMPTY_TABLES: + self.add(section, "L-COL", f"{_where(key)} table has no rows", header_line) + elif not after or not after[0].strip().startswith("None:"): + self.add(section, "L-COL", f"{_where(key)} table is empty without a 'None:' reason", header_line) + for (table_key, column), allowed in ENUMS.items(): + if table_key != key: + continue + for number, cells in table.rows: + value = _plain(cells[column]).lower() + if key == (6, None) and _is_retired_row(cells[2]) and value == "retired": + continue + if value not in allowed: + self.add(section, "L-COL", f"{_where(key)} '{expected[column]}' is '{_plain(cells[column])}', expected one of {', '.join(allowed)}", number) + self.tables[key] = table + + # ---- rules ---------------------------------------------------------------------- + + def check_placeholders(self, visible: list[tuple[int, str]]) -> None: + for index in range(0, self.body_start): + self._scan_placeholders(0, index + 1, self.lines[index]) + starts = sorted((line, sec) for sec, line in self.section_lines.items()) + + def section_of(number: int) -> int: + section = 0 + for start, sec in starts: + if number >= start: + section = sec + return section + + for number, line in visible: + if _TBD_RE.search(line): + self.add(section_of(number), "L-TBD", f"line {number}: contains TBD", number) + # Placeholders may wrap, so scan the visible body as one text and report the opening line. + offsets: list[int] = [] + position = 0 + for _, line in visible: + offsets.append(position) + position += len(line) + 1 + text = "\n".join(line for _, line in visible) + for match in _PLACEHOLDER_RE.finditer(text): + number = visible[bisect.bisect_right(offsets, match.start()) - 1][0] + shown = _short(_collapse(match.group(0))) + self.add(section_of(number), "L-TBD", f"line {number}: unfilled placeholder '{shown}'", number) + + def _scan_placeholders(self, section: int, number: int, line: str) -> None: + if _TBD_RE.search(line): + self.add(section, "L-TBD", f"line {number}: contains TBD", number) + for match in _PLACEHOLDER_RE.finditer(line): + self.add(section, "L-TBD", f"line {number}: unfilled placeholder '{match.group(0)}'", number) + + def check_words(self, visible: list[tuple[int, str]]) -> None: + count = sum( + 1 for _, line in visible for token in line.split() if any(ch.isalnum() for ch in token) + ) + if count > MAX_WORDS: + self.add(0, "L-WORDS", f"plan body has {count} words, maximum is {MAX_WORDS}") + + def collect_changes(self) -> dict[str, tuple[str, list[str]]]: + """Return change ID -> (subsection, cells) for every §3 declaration.""" + declared: dict[str, tuple[str, list[str]]] = {} + for sub, prefixes in CHANGE_PREFIX.items(): + table = self.tables.get((3, sub)) + if table is None: + continue + for number, cells in table.rows: + change_id = _plain(cells[0]) + match = CHANGE_ID_RE.match(change_id) + if not match or match.group(1) not in prefixes: + self.add(3, "L-CHG-REF", f"'{change_id}' is not a valid ID for ### {sub} (expected {' or '.join(p + '-n' for p in prefixes)})", number) + continue + if change_id in declared: + self.add(3, "L-CHG-REF", f"duplicate change ID {change_id}", number) + continue + declared[change_id] = (sub, cells) + return declared + + def check_change_cell(self, section: int, number: int, cell: str, declared: dict, required: bool, what: str) -> list[str]: + tokens = _tokens(cell) + if tokens is None: + if required: + self.add(section, "L-CHG-REF", f"{what} cites no change IDs", number) + return [] + good: list[str] = [] + for token in tokens: + if not CHANGE_SHAPE_RE.match(token): + self.add(section, "L-UNKNOWN-ID", f"{what} cites '{token}', which is not a change ID", number) + elif not CHANGE_ID_RE.match(token): + self.add(section, "L-UNKNOWN-ID", f"{what} cites non-canonical ID '{token}'", number) + elif token not in declared: + self.add(section, "L-CHG-REF", f"{what} cites {token}, which is not defined in §3", number) + else: + good.append(token) + return good + + def check_tests_cell(self, section: int, number: int, cell: str, tests: dict, required: bool, what: str, row_id: str | None) -> None: + tokens = _tokens(cell) + if tokens is None: + if required: + self.add(section, "L-TEST-TRACE", f"{what} cites no tests", number) + return + for token in tokens: + if not TEST_NAME_RE.match(token): + self.add(section, "L-TEST-NAME", f"{what} cites '{token}', which does not follow test_{{function}}_{{outcome}}_{{variant}}", number) + continue + if token not in tests: + self.add(section, "L-TEST-TRACE", f"{what} cites {token}, which is not defined in §8", number) + continue + if row_id is not None and row_id not in tests[token]: + self.add(section, "L-TEST-TRACE", f"{what} cites {token}, whose Covers does not include {row_id}", number) + + def run(self) -> list[Diagnostic]: + self.parse_front_matter() + structural, visible = self.visible() + regions = self.split_regions(structural) + self.parse_tables(regions) + self.check_placeholders(visible) + self.check_words(visible) + + declared = self.collect_changes() + flow_ids, cant_ids, retired = self.source_ids() + new_ids = self.check_invariants(cant_ids, retired, declared) + self.check_flows(flow_ids, retired, declared) + tests = self.collect_tests(flow_ids, cant_ids, new_ids, declared) + self.check_trace(declared, tests, flow_ids, retired) + self.check_flow_and_invariant_tests(tests, retired) + self.check_surface(declared) + return self.diags + + def source_ids(self) -> tuple[list[str] | None, list[str] | None, set[str]]: + """FLOW and CANT IDs from the input, or None without input. Also retired IDs.""" + if self.doc is None: + return None, None, set() + retired = {item.id for item in (*self.doc.flows, *self.doc.cants) if _is_retired_item(item.text)} + return [i.id for i in self.doc.flows], [i.id for i in self.doc.cants], retired + + def check_flows(self, flow_ids: list[str] | None, retired: set[str], declared: dict) -> None: + table = self.tables.get((4, None)) + if table is None: + return + seen: list[str] = [] + for number, cells in table.rows: + row_id = _plain(cells[0]) + if not FLOW_RE.match(row_id): + self.add(4, "L-COV-FLOW", f"'{row_id}' is not a FLOW-n ID", number) + continue + if row_id in seen: + self.add(4, "L-COV-FLOW", f"duplicate row for {row_id}", number) + continue + seen.append(row_id) + marked = _is_retired_row(cells[1]) + if flow_ids is not None: + if row_id not in flow_ids: + self.add(4, "L-UNKNOWN-ID", f"{row_id} is not in the input", number) + continue + if marked and row_id not in retired: + self.add(4, "L-COV-FLOW", f"{row_id} is active in the input but marked retired", number) + if row_id in retired and not marked: + self.add(4, "L-COV-FLOW", f"{row_id} is retired in the input; write 'retired: ...' in Steps", number) + is_retired = marked if flow_ids is None else row_id in retired + self.check_change_cell(4, number, cells[2], declared, not is_retired, row_id) + if flow_ids is not None: + missing = [i for i in flow_ids if i not in seen] + if missing: + self.add(4, "L-COV-FLOW", f"missing rows for {', '.join(missing)}") + present = [i for i in seen if i in flow_ids] + if not missing and present != flow_ids: + self.add(4, "L-COV-FLOW", "FLOW rows are not in input order") + elif seen != sorted(seen, key=lambda s: int(s.split("-")[1])): + self.add(4, "L-COV-FLOW", "FLOW rows are not in order") + + def check_invariants(self, cant_ids: list[str] | None, retired: set[str], declared: dict) -> set[str]: + table = self.tables.get((6, None)) + if table is None: + return set() + cants: list[str] = [] + news: list[str] = [] + ginv_rows = 0 + phase = 0 # 0 CANT rows, 1 after G-INV-1 + for number, cells in table.rows: + row_id = _plain(cells[0]) + marked = _is_retired_row(cells[2]) + if CANT_RE.match(row_id): + if phase: + self.add(6, "L-COV-CANT", f"{row_id} comes after {GINV}; CANT rows come first", number) + if row_id in cants: + self.add(6, "L-COV-CANT", f"duplicate row for {row_id}", number) + continue + cants.append(row_id) + if cant_ids is not None: + if row_id not in cant_ids: + self.add(6, "L-UNKNOWN-ID", f"{row_id} is not in the input", number) + continue + if marked and row_id not in retired: + self.add(6, "L-COV-CANT", f"{row_id} is active in the input but marked retired", number) + if row_id in retired and not marked: + self.add(6, "L-COV-CANT", f"{row_id} is retired in the input; write 'retired: ...' in How it holds", number) + elif row_id == GINV: + ginv_rows += 1 + if ginv_rows > 1: + self.add(6, "L-COV-GINV", f"duplicate row for {GINV}", number) + phase = 1 + if marked: + self.add(6, "L-COV-GINV", f"{GINV} cannot be retired", number) + elif NEW_RE.match(row_id): + if not phase: + self.add(6, "L-COV-GINV", f"{row_id} comes before {GINV}; NEW rows come last", number) + if row_id in news: + self.add(6, "L-UNKNOWN-ID", f"duplicate invariant ID {row_id}", number) + continue + news.append(row_id) + else: + self.add(6, "L-UNKNOWN-ID", f"'{row_id}' is not a CANT-n, {GINV} or NEW-n ID", number) + continue + # Invariants may hold without any change touching them, so change IDs are optional. + self.check_change_cell(6, number, cells[3], declared, False, row_id) + if ginv_rows == 0: + self.add(6, "L-COV-GINV", f"missing row for {GINV}") + if cant_ids is not None: + missing = [i for i in cant_ids if i not in cants] + if missing: + self.add(6, "L-COV-CANT", f"missing rows for {', '.join(missing)}") + present = [i for i in cants if i in cant_ids] + if not missing and present != cant_ids: + self.add(6, "L-COV-CANT", "CANT rows are not in input order") + elif cants != sorted(cants, key=lambda s: int(s.split("-")[1])): + self.add(6, "L-COV-CANT", "CANT rows are not in order") + return set(news) + + def collect_tests(self, flow_ids, cant_ids, new_ids: set[str], declared: dict) -> dict[str, set[str]]: + table = self.tables.get((8, None)) + if table is None: + return {} + if flow_ids is None: + flow_ids = self._local_ids((4, None), FLOW_RE) + if cant_ids is None: + cant_ids = self._local_ids((6, None), CANT_RE) + known = set(flow_ids) | set(cant_ids) | new_ids | {GINV} | set(declared) + tests: dict[str, set[str]] = {} + for number, cells in table.rows: + name = _plain(cells[0]) + if not TEST_NAME_RE.match(name): + self.add(8, "L-TEST-NAME", f"'{name}' does not follow test_{{function}}_{{outcome}}_{{variant}}", number) + continue + if name in tests: + self.add(8, "L-TEST-NAME", f"duplicate test {name}", number) + continue + covers = _tokens(cells[1]) or [] + if not covers: + self.add(8, "L-TEST-TRACE", f"{name} has an empty Covers cell", number) + for token in covers: + if token not in known: + self.add(8, "L-UNKNOWN-ID", f"{name} covers unknown ID '{token}'", number) + for column in (2, 3): + if not _plain(cells[column]): + self.add(8, "L-TEST-TRACE", f"{name} has an empty '{TABLES[(8, None)][column]}' cell", number) + tests[name] = set(covers) + return tests + + def _local_ids(self, key, pattern) -> list[str]: + table = self.tables.get(key) + if table is None: + return [] + return [_plain(c[0]) for _, c in table.rows if pattern.match(_plain(c[0]))] + + def check_trace(self, declared: dict, tests: dict, flow_ids: list[str] | None, retired: set[str]) -> None: + table = self.tables.get((2, None)) + if table is None: + return + flows, retired_flows, where = self.citable_flows(flow_ids, retired) + sentences = _motivation_sentences(self.doc.motivation) if self.doc is not None else None + for number, cells in table.rows: + statement = _decode(cells[0]).strip() + if not statement or statement.lower() in EMPTY_SENTINELS: + self.add(2, "L-REQ-SOURCE", "requirement statement is empty", number) + problem = _source_problem(cells[1], flows, retired_flows, where, sentences) + if problem is not None: + self.add(2, "L-REQ-SOURCE", problem, number) + self.check_change_cell(2, number, cells[2], declared, True, "requirement") + self.check_tests_cell(2, number, cells[3], tests, True, "requirement", None) + + def citable_flows(self, flow_ids: list[str] | None, retired: set[str]) -> tuple[set[str] | None, set[str], str]: + """FLOW IDs a requirement may cite, retired ones, and where they come from. + + The input is authoritative when given; otherwise §4 stands in for it. Without + either, FLOW references are checked for form only. + """ + if flow_ids is not None: + return set(flow_ids), retired & set(flow_ids), "the input" + table = self.tables.get((4, None)) + if table is None: + return None, set(), "§4" + flows: set[str] = set() + marked: set[str] = set() + for _, cells in table.rows: + row_id = _plain(cells[0]) + if FLOW_RE.match(row_id): + flows.add(row_id) + if _is_retired_row(cells[1]): + marked.add(row_id) + return flows, marked, "§4" + + def check_flow_and_invariant_tests(self, tests: dict, retired: set[str]) -> None: + for key, section, text_col in (((4, None), 4, 1), ((6, None), 6, 2)): + table = self.tables.get(key) + if table is None: + continue + for number, cells in table.rows: + row_id = _plain(cells[0]) + is_retired = row_id in retired if self.doc is not None else _is_retired_row(cells[text_col]) + self.check_tests_cell(section, number, cells[-1], tests, not is_retired, row_id, row_id) + + def check_surface(self, declared: dict) -> None: + table = self.tables.get((3, "New surface")) + if table is None: + return + counts = {kind: 0 for kind in SURFACE_KINDS} + seen: set[tuple[str, str]] = set() + # New IF ID -> external_functions rows citing it; each new function has exactly one row. + cited_new_if: dict[str, list[int]] = {} + for number, cells in table.rows: + kind, name = _plain(cells[0]), _plain(cells[1]) + if kind not in SURFACE_KINDS: + self.add(3, "L-SURFACE", f"unknown kind '{kind}' (expected one of {', '.join(SURFACE_KINDS)})", number) + continue + if not name: + self.add(3, "L-SURFACE", f"{kind} row has no name", number) + continue + if (kind, name) in seen: + self.add(3, "L-SURFACE", f"{kind} '{name}' is listed twice", number) + continue + seen.add((kind, name)) + counts[kind] += 1 + refs = self.check_change_cell(3, number, cells[2], declared, True, f"{kind} '{name}'") + if not refs: + continue + new_ifs = [r for r in refs if r.startswith("IF-") and _plain(declared[r][1][2]).lower() == "new"] + if kind == "external_functions": + for change_id in new_ifs: + cited_new_if.setdefault(change_id, []).append(number) + if len(new_ifs) > 1: + self.add(3, "L-SURFACE", f"{kind} '{name}' cites {len(new_ifs)} new IF rows ({', '.join(new_ifs)}); list one function per row", number) + need = { + "external_functions": (new_ifs, "a new IF row"), + "errors": ([r for r in refs if r.startswith("ERR-")], "an ERR row"), + "events": ([r for r in refs if r.startswith("EVT-")], "an EVT row"), + "storage_slots": ( + [r for r in refs if r.startswith("ST-") and _plain(declared[r][1][4]).lower() == "new"], + "a new ST row", + ), + }.get(kind) + if need is not None and not need[0]: + self.add(3, "L-SURFACE", f"{kind} '{name}' does not cite {need[1]}", number) + for change_id, (sub, cells) in declared.items(): + if sub != "Interface" or _plain(cells[2]).lower() != "new": + continue + rows = cited_new_if.get(change_id, []) + if not rows: + self.add(3, "L-SURFACE", f"{change_id} is a new function but no external_functions row cites it") + elif len(rows) > 1: + self.add(3, "L-SURFACE", f"{change_id} is cited by {len(rows)} external_functions rows; expected one", rows[1]) + if self.front is not None: + for kind in SURFACE_KINDS: + claimed = self.front["surface"][kind] + if claimed != counts[kind]: + self.add(3, "L-SURFACE", f"front matter surface.{kind} is {claimed} but §3 New surface lists {counts[kind]}") + + +# ---- helpers ---------------------------------------------------------------------------- + + +def _scalar(value: str) -> str | None: + """Parse a restricted YAML scalar: quoted, or plain text without YAML indicators.""" + if value[0] in "\"'": + quote = value[0] + if len(value) < 2 or value[-1] != quote: + return None + inner = value[1:-1] + if quote == "'": + if re.search(r"(?%@`,#" or " #" in value or value.startswith("- "): + return None + # A colon followed by a space (or ending the value) starts a mapping, which a plain scalar cannot hold. + if ": " in value or value.endswith(":"): + return None + return value + + +def _strip_comments(line: str, in_comment: bool) -> tuple[str, bool]: + out = [] + i = 0 + while i < len(line): + if in_comment: + end = line.find("-->", i) + if end < 0: + return "".join(out), True + i = end + 3 + in_comment = False + else: + start = line.find(" + +## 1 Approach + + + +## 2 Requirement trace + + + +| Requirement | Source | Change IDs | Acceptance tests | +| --- | --- | --- | --- | +| | | | | +| | | | | + +## 3 Changes + + + +### Interface + + + +| ID | Signature | New/Changed | +| --- | --- | --- | +| IF-1 | | | + +### Storage + + + +| ID | Slot | Field | Type | Status | Mock = Rust | +| --- | --- | --- | --- | --- | --- | +| ST-1 | | | | | | + +### Behavior + + + +| ID | Function | Changes existing function (yes/no) | Before | After | +| --- | --- | --- | --- | --- | +| BEH-1 | | | | | + +### Errors and events + +| ID | Name | Params | Trigger | +| --- | --- | --- | --- | +| ERR-1 | | <(type name)> | | +| EVT-1 | | <(type indexed name, type name)> | | + +### New surface + + + +| Kind | Name | Change IDs | +| --- | --- | --- | +| | | | + +## 4 User flows + + + +| Flow | Steps (setup → call → state change → events → observable result) | Change IDs | Tests | +| --- | --- | --- | --- | +| FLOW-1 | | | | + +## 5 Hot-path cost + + + +| Function | Cold reads | Warm reads | Writes | External calls | Δ cold | Δ warm | Δ writes | Packed into a slot already read | +| --- | --- | --- | --- | --- | --- | --- | --- | --- | +| | | | | | <+0> | <+0> | <+0> | | + +## 6 Invariants + + + +| ID | Status | How it holds | Change IDs | Tests | +| --- | --- | --- | --- | --- | +| CANT-1 | | | | | +| G-INV-1 | | | | | +| NEW-1 | | | | | + +## 7 Interactions + + + +## 8 Edge cases and test plan + + + +| Test | Covers | Setup and action | Expected result | +| --- | --- | --- | --- | +| | | | | + +## 9 What this plan gives up + + + +## 10 Open questions + +