RFC-6: full words for clause keywords, and the effect row on the arrow

[maxinelevesque]

A rename and a reorder, proposed as a draft RFC. It adds no expressive power, no
obligation, no type, and no metatheory. Every existing program keeps its meaning,
and every one of them changes.

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 a fixed clause order, conjunct blocks as a clause body, and requires nothing.

The argument

Thermite is designed to be 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 or inventory. 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 here: the guar/ens collision that consumed
several design cycles happened because both were abbreviated.

Evidence attached

Counted by the pinned lexer rather than by a regex, on a git archive export of
84d276e7, so a word in a comment cannot be mistaken for a keyword:

• 547 clause sites across the 67 .th files, and 1,527 more inside Rust
  string literals across 111 test files. Three quarters of the migration is in
  the test suite.
• The compiler change is 63 insertions and 62 deletions across five files in
  thermite-syntax, built as a spike rather than estimated.
• 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. map_kv.th exits 1 in both directions, for an
  ens true that §7.1(a) rejects as EnsIsTrivial.
• The migration is driven by the front end: parse gives item boundaries,
  tokenize gives every offset, and the rewrite splices at spans. It reaches 66
  of 67 .th files with no clause keyword surviving, plus 450 embedded fragments.

Depends on #127

This targets rfc/process-and-migration rather than main, because RFC-6 needs
.design/rfcs/ to exist. GitHub will retarget it to main when #127 merges.

Six requirements join the registry, all not_started, since this is proposed
rather than accepted. .design/tooling/req-registry.md is re-pinned for the
governed-file change.

Gates run locally under Python 3.11: rfc-check, req-registry --check,
doc-drift, spec-discipline and anti-pattern-gate all exit 0.

What this asks

A review and a CI run. The judgement that matters is on keeps and measures,
which are not Verus's words and so carry the weight of the clause-grammar rule
that chose them.

This comes from outside the project, written while porting a kernel subsystem to
Thermite, where the clause vocabulary was a repeated source of misreading. That
buys evidence rather than standing.

Per RFC-5's own convention, this PR should not be squash-merged, or the review
history collapses and the RFC's revision count stops deriving.

🤖 Generated with Claude Code