From d042c17c7d7c3e98b7db4aae09aebd12d3ad5e62 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 03:04:43 -0700 Subject: [PATCH] RFC-6: full words for clause keywords, and the effect row on the arrow A rename and a reorder. req/ens/inv/dec become requires/ensures/keeps/measures, fx E becomes ! E at the head of the contract, and three things follow: a fixed clause order, conjunct blocks as a clause body, and `requires nothing`. No expressive power, no obligation, no type, no metatheory. The argument is that Thermite is written principally by language models, which makes semantic overlap with pretraining worth more than token economy. Abbreviations misdirect rather than merely failing to help: fx reads as audio/visual effects, dec as declare/decimal/decrement, inv as inverse. In a language where a misread clause yields a vacuous proof rather than a compile error, that is a safety property. The guar/ens collision that consumed several design cycles happened because both were abbreviated. Scope, counted by the pinned lexer rather than by a regex: 547 clause sites across the 67 .th files at 84d276e7, and 1,527 more inside Rust string literals across 111 test files, which is three quarters of the migration. The spike measured the compiler change at 63 insertions and 62 deletions across five files in thermite-syntax. The migrated corpus certifies identically against Verus 0.2026.05.24.ecee80a: 18 items at L3 over six conformance files, with the same exit status on each, including map_kv.th exiting 1 in both directions for an ens true that 7.1(a) rejects as EnsIsTrivial. Six requirements join the registry, all not_started, since this is proposed rather than accepted. The generated status view is regenerated and .design/tooling/req-registry.md is re-pinned for the governed-file change. Written from outside the project, while porting a kernel subsystem, where the clause vocabulary was a repeated source of misreading. The counts come from measuring this repository rather than reading its documentation. Co-Authored-By: Claude Opus 5 --- .design/reqs/registry.toml | 96 ++++++++++ .design/reqs/status.md | 6 + .design/rfcs/0006-full-words.md | 312 ++++++++++++++++++++++++++++++++ .design/tooling/req-registry.md | 2 +- 4 files changed, 415 insertions(+), 1 deletion(-) create mode 100644 .design/rfcs/0006-full-words.md 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