Skip to content

[Spec audit] Bring spec/language.md up to date with Plan D + state-cell#124

Merged
boldfield merged 4 commits into
mainfrom
spec-audit-plan-d
May 10, 2026
Merged

[Spec audit] Bring spec/language.md up to date with Plan D + state-cell#124
boldfield merged 4 commits into
mainfrom
spec-audit-plan-d

Conversation

@boldfield
Copy link
Copy Markdown
Owner

Summary

Three-phase doc-only audit bringing spec/language.md and README.md into sync with Plan D + state-cell reality. Implements boldfield/designs/in-progress/2026-05-09-sigil-spec-audit-fixes.md (design at boldfield/designs/docs/plans/2026-05-09-sigil-spec-audit-fixes-design.md).

No language-surface change; no compiler change.

Phase 1 — README + §8.1 generics + §8.3 row-poly (233e78f)

  • README ship-status paragraph: rewrote to reflect Plans A1/A2/A3/B/B'/C/D shipped (was framing Plan D items as remaining work). v2 cluster (precise GC, profile-data, per-context CPS) named as the only remaining work.
  • §8.1: fixed bogus example signature fail: (E) -> Int (stdlib's actual shape is fail[A]: (E) -> A); added subsections for generic-effect declarations and per-op generic parameters with canonical examples sourced from std/raise.sigil. References E0143 + E0144.
  • §8.3: added a row-polymorphic-handlers subsection between the multi-shot worked example and the (untouched) eligible-body-shapes paragraph. Walks through catch[A, E]'s signature and the row-tail unification semantics. References E0137.

Phase 2 — §8.5 Continuation + §11 error codes (52722b5)

  • §8.5: expanded the Continuation[OpRet, Ret] section. Documents type-parameter semantics (OpRet = op return, Ret = handler return); the syntactic-sugar desugaring (let f: Continuation[…] = k is a typing-only annotation, no runtime indirection); and dynamic-extent enforcement via E0145.
  • §11: added a Recent additions table covering E0117, E0143, E0144, E0145, E0148, E0220. Each text matches what sigil explain <code> emits.

Phase 3 — cell-backed State + tuple arity + per-resume + verification (8a34e0d)

  • §13 cell-backed State: §13's std.state row at line 1525 already comprehensively covers the cell-backed encoding (allocation at run_state entry, get/set semantics, (value, final_state) return, composition with Raise[E] in either nesting order, E0148 cross-ref). No new edit needed — design Task 6 satisfied by existing coverage.
  • §6 tuple arity: documented MAX_TUPLE_ARITY = 31 (architectural: 32-bit pointer bitmap, one bit reserved for GC).
  • §8.3 conditional-k clarifier: appended a sentence after the per-resume worked example noting per-resume execution applies whether k is invoked unconditionally or conditionally.
  • Worked-example verification (E1..E17): extracted each to /tmp/spec-example-verify/E*.sigil and compiled against target/release/sigil. All 17 examples compile clean.
  • Bonus fix: §8 (E8 illustration block) showed effect Raise[E] { fail: (E) -> Int } — same outdated signature as §8.1. Updated to match std/raise.sigil.

Out of scope (per design doc)

Surfaced for follow-up

E0137 catalog/emit drift. compiler/src/errors/catalog.rs defines E0137 as "duplicate operation name in effect declaration" but typecheck.rs::e0137_unbound_row_var also emits E0137 for unbound row variables (Plan D Task 116 site). E0137 is intentionally omitted from the §11 table to avoid pinning an inaccurate description; either split the codes or update the catalog as a separate cleanup.

Test plan

  • All 17 worked examples compile clean (output: /tmp/spec-example-verify/results.txt)
  • cargo build --release clean
  • Each E-code text in §11 matches sigil explain <code> output
  • Stdlib references in §8.1, §8.3, §13 sourced from actual std/*.sigil files

🤖 Generated with Claude Code

boldfield and others added 3 commits May 9, 2026 17:34
Task 1 — README ship-status paragraph: rewrite to reflect Plans
A1/A2/A3/B/B'/C/D shipped (was framing Plan D items as remaining
work). Mention v2 cluster as the only remaining work.

Task 2 — §8.1: fix the bogus example signature `fail: (E) -> Int`
(stdlib's actual shape is `fail[A]: (E) -> A`); add subsections
for generic-effect declarations and per-op generic parameters with
canonical examples sourced from std/raise.sigil. Mention E0143
(row-arg arity) and E0144 (per-op shadow).

Task 3 — §8.3: add a row-polymorphic-handlers subsection between
the multi-shot worked example and the (untouched) eligible-body-
shapes paragraph. Walks through `catch[A, E]`'s signature and
the row-tail unification semantics. References E0137.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Task 4 — §8.5: expand the Continuation[OpRet, Ret] section. Cover
type-parameter semantics (OpRet = op return, Ret = handler return);
the syntactic-sugar desugaring (`let f: Continuation[…] = k` is a
typing-only annotation, no runtime indirection); and dynamic-extent
enforcement via E0145 (escape barrier — k cannot leave its handler
frame).

Task 5 — §11: add a Recent additions table covering E0117, E0143,
E0144, E0145, E0148, E0220. Each text matches what `sigil explain
<code>` emits (verified against compiler/src/errors/catalog.rs).
E0137 is intentionally omitted — the typecheck pass emits it for
both 'duplicate operation name in effect declaration' (catalog
text) and 'unbound row variable' (Plan D Task 116 site); spec
text would need to pick one. Surface as catalog/emit drift in PR
description for follow-up.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…erification

Task 6 — State cell-backed encoding note: §13's std.state row at
the existing line 1525 already covers the full cell-backed
encoding (allocation at run_state entry, get/set semantics, (value,
final_state) return, composition with Raise[E] in either nesting
order, E0148 cross-ref). §8.5's lambda-of-state subsection also
points readers to std/state.sigil. No new edit needed; existing
coverage is comprehensive.

Task 7 — Tuple arity in §6: documented MAX_TUPLE_ARITY = 31
(architectural: 32-bit pointer bitmap, one bit reserved for GC).

Task 8 — Conditional-k clarifier in §8.3: appended a sentence
after the per-resume worked example noting that per-resume
execution applies whether k is invoked unconditionally or
conditionally (cross-ref to the Conditional k-call subsection).

Task 9 — Worked-example verification (E1..E17): all 17 examples
extracted to /tmp/spec-example-verify/E*.sigil and compiled
against ./target/release/sigil. All passed. Output in
/tmp/spec-example-verify/results.txt.

Bonus fix discovered during Task 9: §8 (E8 illustration block)
showed `effect Raise[E] { fail: (E) -> Int }` — same outdated
signature §8.1 had. Updated to `fail[A]: (E) -> A` to match
std/raise.sigil reality.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Copy link
Copy Markdown
Owner Author

@boldfield boldfield left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review: spec-audit-plan-d

Cross-referenced every claim against the compiler source. The §11 table entries, stdlib signatures, tuple arity constant, and README status are all accurate. Two factual errors in the new prose:

Must-fix

1. §8.3 row-polymorphic handlers — row-variable binding claim is wrong.

The new text says:

e is a row variable, bound at catch's generic-param list alongside A and E.

e is NOT in the generic-param list. The actual signature (both in std/raise.sigil and earlier in the spec at line 764) is:

fn catch[A, E](body: () -> A ![Raise[E] | e]) -> Result[A, E] ![| e]

Only A and E are in the brackets. e is bound implicitly by the | e tail syntax in the effect row. typecheck.rs:25-41 explicitly documents that if someone writes [e] in the brackets, it's "redundant surface noise" that gets stripped — the row variable alone carries the polymorphism via effect_row_var, not through the generic-param list.

Suggested fix: something like "e is a row variable, introduced by the | e tail in the effect row — it is not listed in the [A, E] generic-param brackets."

2. §8.5 E0145 — wrong pass attribution.

The new text says:

The escape barrier is enforced statically by the codegen color pass

E0145 is emitted exclusively from typecheck.rs (6 emission sites: lines 3642, 3789, 3843, 4235, 4985, 5916). Zero occurrences in color.rs or codegen.rs. Should say "typecheck pass" or just drop the pass name and say "enforced statically."

Nit

3. E-code parentheticals are paraphrases styled as quotes. The inline references use parenthetical strings that look like direct quotes but don't match the catalog short field:

  • §8.1: ("Row-argument arity mismatch") — catalog: "row-site effect-arg arity does not match the effect-decl's generic-param count"
  • §8.1: ("Per-op generic param shadows effect-decl param") — catalog: "per-op generic parameter shadows an effect-decl generic parameter"

The §11 table entries use the exact catalog strings (good). These inline ones are abbreviated paraphrases in quote-style parens — could confuse someone grepping for the diagnostic text. Consider either matching the catalog verbatim or dropping the quotes to signal it's a summary.

Verified correct

  • §11 table: all six E-code short strings match catalog.rs verbatim
  • std/raise.sigil signature: fail[A]: (E) -> A matches source; catch[A, E] row-poly shape matches
  • MAX_TUPLE_ARITY = 31: matches header-constants/src/lib.rs:129
  • E0137 omission from §11 + surfaced drift: correct call given the dual-use (catalog says "duplicate op name"; typecheck also emits for unbound row vars)
  • README: plan completion status and stdlib/example inventory are accurate

Must-fix #1 (§8.3 row-poly): `e` is NOT in catch's [A, E]
generic-param brackets — it's introduced by the `| e` tail in
the effect row. Reword to match reality. Same fix applied to the
follow-up paragraph that incorrectly described row-var binding as
'bound by the generic-param list' — corrected to 'introduced by
the | <name> tail somewhere in the function's signature.'

Must-fix #2 (§8.5 E0145): the escape barrier is enforced by the
typecheck pass (typecheck.rs has 6 emission sites for E0145), not
the codegen color pass. Corrected.

Nit #3: dropped quoted paraphrases of E-code text from inline
references (E0137, E0143, E0144, E0145) since the §11 table
carries the verbatim catalog strings and the inline paraphrases
risked confusing grep readers. The E0137 inline reference was
also removed entirely given the catalog/emit drift surfaced in
the PR description — citing E0137 there would mislead readers
who run `sigil explain E0137` (catalog says 'duplicate operation
name').

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@boldfield boldfield merged commit be85c05 into main May 10, 2026
4 checks passed
@boldfield boldfield deleted the spec-audit-plan-d branch May 10, 2026 01:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant