diff --git a/.design/reqs/registry.toml b/.design/reqs/registry.toml index 88854549..04a59a06 100644 --- a/.design/reqs/registry.toml +++ b/.design/reqs/registry.toml @@ -17757,3 +17757,99 @@ note = "registry reader" kind = "file" target = ".design/reqs/registry.toml" note = "the registry the link resolves against" + +[[requirement]] +id = "REQ-SYNTAX-CLAUSE-FULL-WORDS" +title = "Clause keywords are full words" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "req/ens/inv/dec are spelled requires/ensures/keeps/measures, so a clause keyword carries the pretraining prior its meaning deserves." +remaining_scope = "Rename five entries in keyword_kind, keeping the TokKind variant names so downstream references do not move, and rename the clause names carried as strings in parser diagnostics. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the proposal, with the rename table and the clause-grammar rule that chose keeps and measures" + +[[requirement]] +id = "REQ-SYNTAX-EFFECT-ROW-LEADING" +title = "The effect row leads the contract, spelled `!`" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "fx E becomes ! E at the head of the contract, marking the row as part of the arrow rather than a claim about behaviour." +remaining_scope = "Accept the row first in parse_contract and drop fx as a keyword; `!` already lexes as TokKind::Bang, so no new token is needed. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the position argument, and the measurement that 142 lines open with a row and none open with a `!` that is not one" + +[[requirement]] +id = "REQ-SYNTAX-CLAUSE-ORDER" +title = "Clause order: row, bare clauses, measures last" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "The contract is ordered the effect row, then the bare clauses, then measures, and one or more requires is accepted to match ensures." +remaining_scope = "Reorder the parse_contract state machine. Today it enforces req x1, ens x1+, fx x1, with a recursive fn carrying dec after the row. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the ordering rule, checkable without knowing anything semantic" + +[[requirement]] +id = "REQ-SYNTAX-CLAUSE-CONJUNCTS" +title = "A clause body may be a block of conjuncts" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "requires { a; b; } desugars to repeated clauses, with the bare single-expression form as sugar, so a per-obligation proof hint has somewhere to attach." +remaining_scope = "Add the production and desugar it in the parser; nothing downstream of the AST needs to know about it. This is the only part of RFC-6 that adds a production rather than renaming a token. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the production, and why it belongs in a syntax-only change" + +[[requirement]] +id = "REQ-SYNTAX-CLAUSE-TRIVIAL" +title = "`requires nothing` for a trivial clause" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "requires nothing is clause-level sugar for requires true, leaving true legal inside expressions." +remaining_scope = "Accept the keyword in clause position. Adoption across the 100 existing req true sites is a second pass rather than a correctness condition, since a naive rewriter emits requires true and that stays legal. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the sugar, and the note that ensures nothing parses and is then refused by 7.1(a) as EnsIsTrivial" + +[[requirement]] +id = "REQ-SYNTAX-ADDRESS-CLAUSE-SEGMENTS" +title = "Address segments follow the clause rename" +owner = ".design/rfcs" +status = "not_started" +scope = "syntax" +summary = "validate_segments matches the renamed clause keywords, keeping a semantic address and a clause keyword the same word." +remaining_scope = "Rename the segments in the two fixed allowlists in address.rs. This is also why a clause keyword must be one word: a space-bearing segment is rejected as malformed before any lookup. Proposed by RFC-6; not accepted." +contributors = [".design/rfcs/0006-full-words.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "doc" +target = ".design/rfcs/0006-full-words.md" +note = "the allowlist lines, and the address-segment constraint that ruled out `terminates by`" diff --git a/.design/reqs/status.md b/.design/reqs/status.md index a02da26e..a54e2f36 100644 --- a/.design/reqs/status.md +++ b/.design/reqs/status.md @@ -441,6 +441,7 @@ Source: `.design/reqs/registry.toml` | REQ-STRING-SUBSTRING-PREDICATES | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_search_conformance.rs` | lower | String substring predicates | symbol: `emit_string_search_methods` - substring predicate method emitter
symbol: `emit_string_search_defs` - substring predicate spec emitter
test: `forge/tests/string_search_conformance.rs` - substring predicate conformance | | | REQ-STRING-TRIM | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_search_conformance.rs` | lower | String trim operation | symbol: `emit_string_search_methods` - trim method emitter
symbol: `GENERATED_SPEC_FNS` - validator admits `is_space`
test: `forge/tests/string_search_conformance.rs` - trim conformance | | | REQ-STRING-U64-TO-STRING | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_format_conformance.rs`, `forge/tests/divergence_numfmt_display_order.rs` | lower | u64 decimal formatting with round-trip contract | symbol: `emit_numfmt_defs` - decimal formatter and round-trip spec emitter
symbol: `GENERATED_SPEC_FNS` - validator admits generated parse/format spec functions
test: `forge/tests/string_format_conformance.rs` - formatting L3 conformance
test: `forge/tests/divergence_numfmt_display_order.rs` - MSB-first display regression tooth | | +| REQ-SYNTAX-ADDRESS-CLAUSE-SEGMENTS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Address segments follow the clause rename | doc: `.design/rfcs/0006-full-words.md` - the allowlist lines, and the address-segment constraint that ruled out `terminates by` | Rename the segments in the two fixed allowlists in address.rs. This is also why a clause keyword must be one word: a space-bearing segment is rejected as malformed before any lookup. Proposed by RFC-6; not accepted. | | REQ-SYNTAX-ADDRESS-DEC | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address dec segment | symbol: `emit_loop` - emits dec address entries
symbol: `AddrKind::Dec` - dec address kind
test: `thermite-syntax/tests/conformance.rs` - semantic address oracle | | | REQ-SYNTAX-ADDRESS-DETERMINISTIC-RESOLVE | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address bidirectional resolution | symbol: `resolve` - address-to-node resolver
symbol: `AddressError` - structured resolution error
test: `thermite-syntax/tests/conformance.rs` - bidirectional address conformance | | | REQ-SYNTAX-ADDRESS-GRAMMAR | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address grammar | symbol: `AddressEntry` - address entry carrier
symbol: `validate_segments` - address segment grammar validator
test: `thermite-syntax/tests/conformance.rs` - semantic address conformance | | @@ -468,7 +469,12 @@ Source: `.design/reqs/registry.toml` | REQ-SYNTAX-AST-PATTERN-TYPE-EFFECT | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/parser.rs` | syntax | Pattern, type, and effect AST nodes | symbol: `Pattern` - pattern AST enum
symbol: `EffectRow` - effect row AST enum | | | REQ-SYNTAX-AST-SLAG | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/parser.rs` | syntax | Slag attribute AST node | symbol: `SlagAttr` - slag attribute node
symbol: `parse_slag_body` - slag parser arm | | | REQ-SYNTAX-AST-SPANS | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/address.rs` | syntax | Span-bearing AST boundary stability | symbol: `Span` - source span type
symbol: `Clause` - span and verbatim text carrier | | +| REQ-SYNTAX-CLAUSE-CONJUNCTS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | A clause body may be a block of conjuncts | doc: `.design/rfcs/0006-full-words.md` - the production, and why it belongs in a syntax-only change | Add the production and desugar it in the parser; nothing downstream of the AST needs to know about it. This is the only part of RFC-6 that adds a production rather than renaming a token. Proposed by RFC-6; not accepted. | +| REQ-SYNTAX-CLAUSE-FULL-WORDS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Clause keywords are full words | doc: `.design/rfcs/0006-full-words.md` - the proposal, with the rename table and the clause-grammar rule that chose keeps and measures | Rename five entries in keyword_kind, keeping the TokKind variant names so downstream references do not move, and rename the clause names carried as strings in parser diagnostics. Proposed by RFC-6; not accepted. | +| REQ-SYNTAX-CLAUSE-ORDER | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Clause order: row, bare clauses, measures last | doc: `.design/rfcs/0006-full-words.md` - the ordering rule, checkable without knowing anything semantic | Reorder the parse_contract state machine. Today it enforces req x1, ens x1+, fx x1, with a recursive fn carrying dec after the row. Proposed by RFC-6; not accepted. | +| REQ-SYNTAX-CLAUSE-TRIVIAL | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | `requires nothing` for a trivial clause | doc: `.design/rfcs/0006-full-words.md` - the sugar, and the note that ensures nothing parses and is then refused by 7.1(a) as EnsIsTrivial | Accept the keyword in clause position. Adoption across the 100 existing req true sites is a second pass rather than a correctness condition, since a naive rewriter emits requires true and that stays legal. Proposed by RFC-6; not accepted. | | REQ-SYNTAX-COLLECTIONS-VEC | shipped | `thermite-syntax/src/ast.rs` | `.design/basis/04-collections.md`, `thermite-syntax/src/parser.rs`, `thermite-lower/tests/collections_conformance.rs` | syntax | Vec type surface AST | symbol: `Type::Vec` - Vec type node
test: `thermite-lower/tests/collections_conformance.rs` - collection conformance | | +| REQ-SYNTAX-EFFECT-ROW-LEADING | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | The effect row leads the contract, spelled `!` | doc: `.design/rfcs/0006-full-words.md` - the position argument, and the measurement that 142 lines open with a row and none open with a `!` that is not one | Accept the row first in parse_contract and drop fx as a keyword; `!` already lexes as TokKind::Bang, so no new token is needed. Proposed by RFC-6; not accepted. | | REQ-SYNTAX-ERGONOMICS-FOR | shipped | `thermite-syntax/src/parser.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/ast.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | For-loop desugar | symbol: `parse_for` - for-loop parser desugar
test: `forge/tests/ergonomics_conformance.rs` - for-loop conformance | | | REQ-SYNTAX-ERGONOMICS-IF-WHILE-LET | shipped | `thermite-syntax/src/parser.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/ast.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | If-let and while-let desugars | symbol: `parse_if_let` - if-let parser desugar
symbol: `parse_while_let` - while-let parser desugar
test: `forge/tests/ergonomics_conformance.rs` - if-let and while-let conformance | | | REQ-SYNTAX-ERGONOMICS-MATCH-GUARD | shipped | `thermite-syntax/src/ast.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/parser.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | Match guard surface AST | symbol: `MatchArm.guard` - optional match guard
test: `forge/tests/ergonomics_conformance.rs` - match guard conformance | | diff --git a/.design/rfcs/0006-full-words.md b/.design/rfcs/0006-full-words.md new file mode 100644 index 00000000..c7caaea9 --- /dev/null +++ b/.design/rfcs/0006-full-words.md @@ -0,0 +1,312 @@ +--- +rfc: 6 +title: Full words for clause keywords, and the effect row on the arrow +status: draft +supersedes: [] +introduces: + - REQ-SYNTAX-CLAUSE-FULL-WORDS + - REQ-SYNTAX-CLAUSE-ORDER + - REQ-SYNTAX-CLAUSE-CONJUNCTS + - REQ-SYNTAX-CLAUSE-TRIVIAL + - REQ-SYNTAX-EFFECT-ROW-LEADING + - REQ-SYNTAX-ADDRESS-CLAUSE-SEGMENTS +--- + +# Full words for clause keywords, and the effect row on the arrow + +Kind: rename and reorder. This RFC adds no expressive power, no obligation, no +type, and no metatheory. Every existing program keeps its meaning, and every one +of them changes. + +## The change + +| from | to | +|---|---| +| `req P` | `requires P` | +| `ens P` | `ensures P` | +| `inv P` | `keeps P` | +| `dec E` | `measures E` | +| `fx E` | `! E`, moved to the head of the contract | + +Plus three things that follow from those. + +**Clause order becomes** the effect row, then the bare clauses, then `measures` +last. Today `parse_contract` enforces `req` ×1, `ens` ×1+, `fx` ×1, and a +recursive `fn` carries its `dec` after the row. + +**A clause body may be a block of conjuncts**, with the bare single-expression +form as sugar: + +```thermite +requires { + cpu < 64; + (s.expected >> cpu) & 1 == 1; +} +``` + +**`requires nothing`** is sugar for `requires true`. + +That is the entire proposal. + +## Why + +Thermite is designed to be written principally by language models. That makes +**semantic overlap with pretraining worth more than token economy**. + +The failure mode of abbreviation is not that a model cannot learn it. It is that +abbreviations misdirect: `fx` reads as audio/visual effects, `dec` as +declare/decimal/decrement, `inv` as inverse or inventory. Those are wrong priors +rather than absent ones. In a language where a misread clause yields a vacuous +proof rather than a compile error, that is a safety property rather than an +ergonomic one. + +**The evidence is already paid, in this repository.** A `guar`/`ens` collision +consumed several design cycles in a proposal for this language, and it happened +because both were abbreviated. `guarantees` and `ensures` do not collide. The +abbreviation destroyed the information that would have prevented the clash. + +The current spelling is also a departure from both parents. Verus uses full words +heavily — in vstd, `ensures` 804, `requires` 465, `decreases` 161, `invariant` +117. Rust is mixed, abbreviating only its most ubiquitous tokens: `fn`, `mut`, +`pub`. `req`/`ens`/`fx`/`inv`/`dec` is neither. + +The counter-argument, that idiosyncrasy makes fine-tuning more specifying, is +real. It is judged to lose against the loss of semantic overlap. + +## Why these particular words + +`requires` and `ensures` are Verus's, and need no defence. + +`keeps` and `measures` are not, so they do: + +> **Every clause is a third-person-singular verb whose subject is the item.** A +> clause is a sentence with the subject elided, and the item supplies it. + +``` +f requires n < 100 +f ensures result == n * 2 +f measures p.count +the loop keeps acked & !expected == 0 +Grant keeps base + len <= MAX_PHYS +``` + +`requires` and `ensures` already obey this. `inv` is a noun in a verb slot, which +is why it never sat right beside them, and `dec` names the expression's property +rather than the clause's purpose. + +`measures` also fixes a mechanical problem. A clause keyword is a +semantic-address segment, and `validate_segments` matches a fixed allowlist after +splitting on `.`, so a clause keyword must be one word. A two-word spelling such +as `terminates by` is rejected as malformed before any lookup: + +``` +double.ens → no such address (segment well-formed) +double.terminates by → malformed address (rejected before lookup) +``` + +## Why the row moves + +`fx E` is a noun phrase sitting among verb phrases, and it is not a claim about +behaviour. It is part of the type: `() ! pure` and `() ! write(shootdown)` are +different types to the prover, so the row belongs to the arrow. `!` follows +Koka's `-> B ! e`. + +```thermite +fn allocate(pages: u64) -> Result + ! write(heap) + requires pages > 0 && pages <= 1024 + ensures ... +``` + +The line the position draws is worth stating, because it is the one that decides +where a future feature belongs: + +> An effect propagates up the call graph by construction. A clause is proved at +> the item. + +`!` needs no new token: it already lexes as `TokKind::Bang`. The row is +unambiguous by position, checked rather than assumed. Migrating the corpus and +scanning every line gives **142 lines opening with a row and zero lines opening +with `!` that are not one**. The remaining three of the lexer's 145 `fx` tokens +are accounted for: one row sits inline in `conformance/review/vacuous.th`, and +two are in `conformance/parse/recover_per_item.th`, which does not parse by +design. Clause expressions that open with a negation are unaffected, because +there the `!` follows a keyword and never opens a line. + +## An argument the migration turned up + +After the rename, Thermite's `requires` and Verus's `requires` are the same word, +so **lowering becomes identity rather than translation** for four of the five +clauses. Emitted Verus reads against its Thermite source directly, and a reader +comparing the two no longer holds a mapping in their head. + +That was not why the change was proposed, and it is a real argument for it. + +## Scope + +Measured by the pinned lexer across the 67 `.th` files tracked at `84d276e7`. A +`req` token is a clause and an identifier spelled `req` is not, which is the +distinction a textual count cannot make. + +| | sites | +|---|---| +| `ens` | 205 | +| `req` | 152 | +| `fx` | 145 | +| `dec` | 26 | +| `inv` | 19 | +| **total** | **547**, across 144 contracts | +| `req true` | 100 | +| `ens true` | 2 | + +The volume is not there. **1,527 further clause sites live inside Rust string +literals**, across 450 `.th` fragments in 111 test files. Three quarters of the +migration is in the test suite. + +## The compiler change + +Scoped against the tree at `84d276e7` rather than estimated, and built as a spike +to check the estimate. + +| | | +|---|---| +| `keyword_kind` entries (`lexer.rs:217`) | 5 | +| `TokKind` variants | 5, keeping their names, so 53 downstream references do not move | +| `parse_contract` (`parser.rs:1420`) | accept the row first, one or more `requires`, `measures` last | +| `validate_segments` (`address.rs:331`, `:347`) | 2 lines | +| clause names in diagnostic strings | several in `parser.rs`, user-facing | + +**The spike measured 63 insertions and 62 deletions across five files** in +`thermite-syntax` — lexer, parser, addresses, AST and lib. `fx` is removed as a +keyword entirely, since the row is `!` and `Bang` already lexed. + +Conjunct blocks are the one part that adds a production rather than renaming a +token. They desugar to repeated clauses, so nothing downstream of the AST needs +to know about them, which is the argument for including them here. + +**Correcting a claim in this proposal's own history:** `fx` is not last today. A +recursive function carries `dec` after it — `examples/editor/editor.th` reads +`ens … fx pure … dec end - i` — so the new order is a genuine move rather than a +no-op. + +## Migration + +**It is mechanical.** A rename plus a fixed reorder is a deterministic +source-to-source rewrite: nothing about it depends on what a program means. The +rewriter edits spans rather than reprinting files, so comments, blank lines, +expression text and alignment survive untouched. A formatter would produce a diff +nobody can review, and this change does not need one. + +**The front end drives it, so the hard case is exact.** The hard case is a +contract written on one line, which is most of the test corpus: + +```thermite +fn id(x: u32) -> u32 req true ens result == x fx pure { x } +``` + +Moving the row to the front means knowing where the contract ends and the body +begins, and that is parsing rather than matching. A rewriter linking +`thermite-syntax` takes item boundaries from `parse` and every offset from +`tokenize`; two facts from the grammar then settle it. A clause keyword is a +reserved token, so `TokKind::Req` is a clause and an identifier spelled `req` +cannot be one. And `parse_effect_row` is a closed grammar containing no brace, so +the row ends at the first token that cannot continue it and the body's `{` is +whatever follows. + +Measured on a `git archive` export of the pin: + +| | | +|---|---| +| `.th` corpus | **66 of 67 migrate**, with no clause keyword surviving | +| the one decline | `conformance/parse/recover_per_item.th`, whose purpose is to not parse | +| `.th` fragments in Rust literals | **450 migrate**, carrying 1,527 clause sites | +| declined, carrying no clause keyword | 340, where declining costs nothing | +| declined and clause-bearing | **43**: `format!` templates, assertion prose, and fixtures invalid on purpose | + +Those 43 are a hand-reviewable list rather than a residue, and they are listed in +the implementation PR rather than here. + +**A note on checking, because it generalises.** An earlier rewriter matched a +clause keyword at the head of a line and proved itself by round-trip — +`to_v2(to_v3(x)) == x`, byte for byte, on 382 of 382 files. That check is silent +about text a tool never touches, because untouched text is restored perfectly, +and the silence hid every one-line contract and 17 `@bv`-tagged clauses across 10 +files. A migrated corpus would have carried `ens@bv64` into a front end with no +`ens` keyword. Reversibility is worth having and does not measure coverage. +Parsing both sides and comparing ASTs is the replacement, and it checks meaning +rather than text. + +**The one non-mechanical part is optional.** A naive rewriter emits +`requires true` rather than `requires nothing`. That stays legal, since `true` +remains legal inside expressions and the sugar is clause-level only, so adopting +it is a second pass over 100 sites rather than a correctness condition. + +**Certificates survive**, and this was checked rather than assumed. The +`.cert.json` oracle subset is `item` / `level` / `tautology` / +`vacuous_precondition` / `effects` / `slag`. Clause names appear nowhere in it, so +no oracle is invalidated and the migration is source-only. + +**And the migrated corpus certifies identically**, which is the check a +round-trip cannot make. Baseline is `forge check` at `84d276e7` on the unmigrated +file; migrated is the patched front end on the rewriter's output: + +| file | items at L3, before | after | exit, before / after | +|---|---|---|---| +| `parse_u64.th` | 1 | 1 | 0 / 0 | +| `list_sum.th` | 2 | 2 | 0 / 0 | +| `option_result.th` | 5 | 5 | 0 / 0 | +| `multi_adt.th` | 5 | 5 | 0 / 0 | +| `map_kv.th` | 1 of 4 | 1 of 4 | 1 / 1 | +| `bytes_eq_demo.th` | 4 | 4 | 0 / 0 | + +Eighteen items at L3, same levels and the same exit status on every file, against +Verus `0.2026.05.24.ecee80a`. `map_kv.th` exits 1 in both directions: it carries +an `ens true` that §7.1(a) rejects as `EnsIsTrivial`, before the rename and after +it. The rename preserves meaning to the prover rather than only information in +the text. + +## What is not in this proposal + +Everything that would add capability, listed so that this one can be short: + +``` +survives · interleaves { asks / promises } · resource · forget / forgets(r) +opaque · by unfold(…) · shared declarations and checked effect rows +lock / owns / holding · protocol types · ensures on spec fn · blocks · cost(E) +handlers { } · an effect algebra +``` + +Each of those adds an obligation, a type, or a check. + +**Two abbreviations are deliberately left alone.** `alloc` and `rand` are +abbreviations the principle above would rename. They are untouched because a +plausible later proposal turns them into `write(heap)` and `write(entropy)` +anyway, and renaming the same token twice is churn. Flagged so it reads as a +decision rather than an oversight. + +## What this asks + +A review and a CI run. The corpus certifies before and after, the migration is a +tool rather than a hand edit, and no proof obligation anywhere changes. + +The migration and the parser change land as **one PR rather than two**, because +no front end accepts the new surface until the parser moves, so a migrated corpus +cannot certify on its own. + +It is also a **version-number event**, which makes it a concrete test case for +[RFC-4](0004-versioning.md): a breaking change to every source file, with an +automated migration, and no change to what any program proves. + +## Provenance + +This proposal comes from outside the project. It was written while porting a +kernel subsystem to Thermite, where the clause vocabulary was a repeated source +of misreading, and the counts above come from measuring this repository at +`84d276e7` rather than from reading its documentation. The spike, the migration +tooling and the certification table are attached to the implementation PR. + +Every gap that motivated it was found by attempting something rather than by +reading the reference, and several contradicted the documentation in both +directions. That buys evidence rather than standing: the proposal earns its way +on the design and the reproduction, and a maintainer's judgement on `keeps` and +`measures` is the deciding one. diff --git a/.design/tooling/req-registry.md b/.design/tooling/req-registry.md index b0d783e1..22c1e888 100644 --- a/.design/tooling/req-registry.md +++ b/.design/tooling/req-registry.md @@ -4,7 +4,7 @@ tier: 3-component status: draft audited-sha: f09f8ca376257cc1e2543b8ebc9fb771bffd04df (content-sha256 re-pinned 2026-07-29 for stage-3 REQ-1..REQ-9 / gate G3 (#80, crosslink #351): the registry and generated status view carry the fixed-width reconstruction requirements and verified evidence; req-registry.py --check is clean (462 requirements, 119 views). The legacy commit pin remains the f09f8ca3 stable-main ancestor; the active content digest tracks the governed files. prior: 2026-06-21 stage-2 REQ-10 / AC-10 (#332), the pin battery and final gate G2 increment) -audited-content-sha256: 68d2b71dc3764885450afa985b710f40840a6fe7c48b35c7e8d1bab8474f3505 (re-pinned 2026-08-06 for the RFC process (#127): three RFC requirements join the registry and the generated status view, and the tools declare their interpreter floor, described under Interpreter floor. req-registry.py --check is clean (527 requirements, 125 views); the RFC gate carries test evidence. prior: 2026-08-01 after replacing generated-image evidence with the tracked kernel-image CI gate) +audited-content-sha256: ab7f72c4e6f31a1ebdf032d87f095ae0b5afd2082e7d74379aa0a621983e1b41 (re-pinned 2026-08-06 for the full-words anchor (RFC-6): six syntax requirements join the registry and the generated status view, all not_started, since the clause rename is proposed rather than accepted. req-registry.py --check is clean (533 requirements, 125 views). prior: 2026-08-06 for the RFC process (#127), three RFC requirements and the interpreter floor) governs: - .design/reqs/registry.toml - .design/reqs/status.md