Autoformat input rules

Handle $ARGUMENTS. check, or no argument, runs the gate bound. deep runs --length=4 and compares its failures with Findings. lower runs --lower after a fix removes a known finding. typed <keys> runs --typed=<keys> to show one sequence's results. update brings the verification in line with changed code, as Coverage record says.

The property. Typed key by key into a paragraph between two others, every shorthand the kits declare gives its declared result whole: the substituted symbol, or the content with exactly its marks and no delimiter left. Inside a word, a mark shorthand stays literal, except subscript and superscript around a script token. No typed sequence changes the paragraphs above or below. When a keystroke fires a rule, one undo gives back the document from before that keystroke. Committed through a composition, as an input method commits it, the last keystroke gives the same document, caret and pending marks that typing it gives. Committed two letters into another author's struck text with the pending marks set to {}, it throws nothing, and when typing it there fires a rule, it gives what typing gives.

The harm. A user who types ==yellow==, ***both***, H~2~O or !>= from the docs gets symbols or stray delimiters instead of what the kit promises, and closing an inline-code backtick pulled the next paragraph into the current one until plate-private#13's fix. Each case is one string a test can check, but rules that share keys collide in sequences nobody wrote down, as five Beta bugs on the Autoformat demo showed. With Doubao IME on, typing !>= stopped after ! and threw points outside document root until plate-private#127's fix, because after a rule on a composed key deleted its source, the caret the view reported still pointed into the text from before the deletion.

What it checks

apps/www/scripts/autoformat-input-rules.ts types into real editors built from BasicMarksKit then AutoformatKit, the order EditorKit uses, with editor.update.text.insert once per key, as apps/www/src/__tests__/package-integration/autoformat/current-kit.spec.tsx does. It checks the TypeScript code itself, exhaustively up to a bound, not a model of it. No verifier runs on input rules, so the script enumerates the inputs. Each run starts from the paragraphs x, the caret paragraph and y, with the caret at the end of the caret paragraph.

1. It reads the declarations with the Babel parser, because the repository's TypeScript has no compiler API. From autoformat.tsx it takes every createTextSubstitutionInputRule constant in an inputRules list, with each pattern's format and match. From basic-marks.tsx it takes every <Mark>Rules.markdown() call in an inputRules list, with its variant or value. A value that is not a string literal, an inputRules value that is not a list literal, a rule of another shape or a file with no inputRules list exits 2. Each worker also counts the text input rules an editor of the two kits runs, through getPlateRuntime. The script exits 2 when that count differs from the number of rules it read, because a rule that reaches the editor another way would go untyped.
2. A mark rule's syntax comes from the script's EXPECTED_MARK_SYNTAX table, not from the factories in BaseMarkPlugins.ts, so a factory whose delimiters drift from the table fails. The table copies the Inline Mark Autoformat rules of docs/editor-behavior/markdown-editing-spec.md where they name a syntax: **, *, `, ~~, ==, ~, ^ and ***. The spec names only the opening runs __*, __** and ___*** of EDIT-PROFILE-AUTOFMT-MARK-003, so each combo's closing run mirrors its opening run, ___***a***___ for boldItalicUnderline. The spec names no syntax for the _ variants of bold and italic, the ≡ highlight variant or underline, so their rows hold CommonMark's __ and _ and what their factories type, ≡a≡ and __a__. A factory or variant the table lacks exits 2.
3. A declared character that no key types, such as ≤ in ≤= or ≯ in ≯=, is typed as the source of the rule that writes it, <= and !>, as a user would reach it.
4. Declared shorthands. Each substitution source is typed at a paragraph start, after the word w and after a bold w , and must give the context followed by its symbol; a smart quote is typed around a. Each mark rule is typed around a and around one character for each substitution rule whose source that character completes with the rule's opening or closing delimiter, such as ~=~ for equalityRule and ^o^ for superscriptSymbolsRule. It must give the content with the rule's marks, plus bold in the bold context. Subscript and superscript need a letter or a digit between their delimiters, as EDIT-PROFILE-AUTOFMT-MARK-002 says, so around other content, such as ~=~, they must leave no leaf with their marks. Typed right after w, a mark rule must leave no leaf with its marks, as EDIT-PROFILE-AUTOFMT-MARK-004 says, except subscript and superscript around a script token, ASCII letters or digits with an optional sign at either end, which must apply there, as EDIT-PROFILE-AUTOFMT-MARK-002 says. Around any other content, such as w~!~, they stay literal too. These are the autoformat-declared findings, owned by the kit file that declares the shorthand. The check judges the caret paragraph on its own. When a typed sequence joins y into it, the script drops that y before comparing, because the blocks rule already reports the join.
5. Sequences. Every sequence of up to three keys over a and the characters of the mark syntaxes and of the substitution sources that hold no letter or digit is typed at a paragraph start. That is 15 characters and 3,615 sequences. A run whose result holds other than three paragraphs, or changes x or y, is an autoformat-blocks finding, owned by createInputRules.ts.
6. Undo, on every run. The last keystroke fired a rule when the caret paragraph is no longer its old text plus the key, or its old characters changed marks, or the other paragraphs changed. Then one editor.api.history.undo() must give back the children from before that keystroke. Each shorter sequence is a run of its own, so every keystroke of every sequence is checked. These are the autoformat-undo findings, owned by InputRulesPlugin.ts.
7. Composition, on every run. A second editor types the same keys while a view of it holds the caret. It then commits the last key through that view with getUserTextLanding and dispatchUserText, as commitChromeCompositionEndFallback in composition-state.ts does when Chrome ends a composition. A target runtime reports the caret in the document the update started from, as the React view's does. The commit must give the children, caret and pending marks that typing gives. A throw or a difference is an autoformat-composition finding, owned by packages/plitejs/src/react/editable/mutation-controller.ts, whose dispatchUserText decides where the composed key and a rule's later write land. Each run then does this again in editors that add AuthoredPlugin, in a caret paragraph that ends with bob's struck gone. After the earlier keys, both editors move the caret two letters into gone and set the pending marks to {}, as turning a mark off does. Each command frame's accept-all projection hides struck text, so with no active pending mark the commit takes the stored landing and keeps the key inside gone, where typing puts it beside gone instead. There the commit must not throw. When typing the last key fires a rule, judged on the text outside gone, the commit must also give the children, caret and pending marks that typing gives. Such a finding's identity starts with struck.
8. It sorts the findings and compares them with apps/www/scripts/autoformat-input-rules-baseline.json through tooling/scripts/finding-baseline.mjs, the shrink-only baseline the decision-order and lint checks use. A finding's identity names the rule or sequence, the typed keys and the context, never the result.

Run it

Run every command from the repository root.

• pnpm check:autoformat-rules checks the gate bound, three keys. It makes 3,821 runs, each typed and composed in a plain paragraph and again inside struck text, and 241 declared checks in about 45 s on an 18-core M5 Max while other sessions load the machine. It prints one JSON summary line, then each finding the baseline does not list. pnpm check autoformat-rules runs the same step through the check runner, and pnpm check --affected runs it for a change to the script or its baseline, apps/www/src/registry/components/editor/, packages/platejs/src/, packages/plitejs/src/ or tooling/scripts/finding-baseline.mjs.
• --length=4 types every sequence of up to four keys: 54,446 runs in about 600 s on the same machine with 8 workers while other sessions load it. A bound other than the gate's skips the baseline and exits 1 on any finding, because the known findings repeat there in more sequences. Compare its counts with Findings. Run it after a change to how rules match or apply.
• --typed='<keys>' runs one typed sequence in each context the gate types it in, or at a start, after a word, after a bold word and inside a word when the gate has no such run, and prints every finding without reading the baseline.
• --jobs=<n> sets the number of worker processes. It defaults to the machine's cores, at most 8, because each worker holds its own editor runtime. Any other argument exits 2, and so does --init or --lower with --length or --typed.
• After a fix removes a known finding, the gate fails until you run pnpm check:autoformat-rules --lower, which drops the entries the tree no longer holds. The baseline never grows. --lower refuses a new entry, and finding-baseline.mjs refuses an entry its copy at the base commit lacks. --init seeds only a rule the baseline lacks.

Read a failure

A finding prints its rule and identity, then what each paragraph holds. A leaf is its text in quotes, followed by its marks, and | separates paragraphs:

autoformat-declared comparisonsRule "<=" at start
  expected "x" | "≤" | "y"
  got      "x" | "⇐" | "y"

autoformat-blocks "`a`" at start
  "x" | "`a" | "y"  then "`"  gives "x" | "a"⟨code⟩ "y"

autoformat-undo "->" at start
  "x" | "-" | "y"  then ">"  gives "x" | "→" | "y"
  one undo gives "x" | "" | "y" (applied)

The first is arrowsRule's <= firing as ⇐ before comparisonsRule sees the key. The second is the closing backtick joining y into the caret paragraph, as it did before plate-private#13's fix. The third is a planted history bug from What a pass proves, where one undo also takes back the - typed before the rule.

Tell a real bug from a modeling error before you change code:

• Real bug. The typed keys are what a user types for a shorthand the kit declares, or a sequence of real keys, and the result differs from the spec's or the declaration's. Fix the rule, the kit's rule order or the runtime, then run --lower. When two declarations share their keys, as __a__ does for BoldRules _ and UnderlineRules, the spec's first matching rule wins, so the later one never applies. Fix that by removing or changing a declaration, never by adding a baseline entry.
• Modeling error. EXPECTED_MARK_SYNTAX names a syntax the spec does not promise, the content the script picks makes the expected result ambiguous, or the difference is one no user sees, such as an empty leaf. The script compares leaves with empty text dropped and equal marks merged. Fix the table or the script with the spec rule it follows.
• Intended change. Changing what a shorthand gives changes its declaration in the kit, or the spec and EXPECTED_MARK_SYNTAX together, in the same change. Never weaken the property or add a baseline entry to get green.

Findings

The gate finds 25, all autoformat-declared, with no autoformat-blocks, autoformat-composition or autoformat-undo. --length=4 finds the same 25 and nothing else. Each class is one cause:

• <= gives ⇐, never ≤, because arrowsRule declares <= and runs before comparisonsRule, and arrowsRule's own ≤=, typed <==, gives ⇐= (t_dceb960e). 6 entries.
• ==!==, ==<== and ==>== give ==≢ and the like, because a substitution inside the span takes the first key of the closing == (t_c4407e94). 9 entries.
• __a__ gives bold, never underline, because BoldRules _ and UnderlineRules both match __ and bold comes first. 3 entries.
• ^o^ gives °^ and ~~=~~ gives ~≈~~, because ^o and ~= fire inside the span. 7 entries.

No run needs more than one undo. The undo check covers every keystroke of every sequence at a paragraph start up to the bound, and the last keystroke of each declared shorthand in its other contexts.

What a pass proves

The gate catches a shorthand that stops applying whole, a typed sequence that changes another paragraph, a rule step that undo no longer takes back on its own, and a composed key that leaves a different document, caret or pending marks than the typed key. At base 95a313df66 with this check copied in, bugs planted in a detached proof worktree gave:

• Keeping a substitution's end text, by turning if (match.end) in createTextSubstitutionInputRule's apply into if (!match.end), gives 293 autoformat-declared, 127 autoformat-blocks and 456 autoformat-undo findings against 86, 86 and 0. One is arrowsRule "->" at start, which gives -→.
• Merging every text batch in shouldMergeBatch of packages/plitejs/src/history/history-merge-policy.ts gives 456 autoformat-undo findings and leaves the other counts unchanged. One is the -> failure in Read a failure.
• Writing one pattern's match as String('->') exits 2, naming autoformat.tsx:7.
• Adding a plugin to AutoformatKit whose rules sit in Object.fromEntries([['inputRules', [arrowsRule]]]), which the reader cannot see, exits 2, because the editor runs 29 text input rules and the lists declare 28.
• After each plant was dropped, the gate matched the baseline again.

At fc9906287b with plate-private#127's fix, dispatchUserText points the implicit target at the caret the view holds before it lands a composed key there, at every landing. A rule's later write in the same update then lands at that caret, moved by the rule's own changes. Limiting that step to the selection landing again, as before the fix, gives 588 autoformat-composition findings, 270 in a plain paragraph and 318 inside struck text, and leaves the other counts unchanged. Each one throws points outside document root, such as "!>=" at start and struck "!>=" at start. Skipping it only for the stored landing, as the fix did until a review found the struck case, gives 318, all struck and each a throw. Restoring the fix brings the gate back to the baseline. Leaving bold pending after a composed key, by calling tx.marks.set({ bold: true }) after the composed insert in dispatchUserText, gives 4,179 autoformat-composition findings, which only the comparison of pending marks reports.

The code before plate-private#13's fix failed autoformat-blocks on its own, the code before plate-private#127's fix failed autoformat-composition, and the current code fails autoformat-declared, as Findings lists. So three of the four properties have failed on real bugs too.

Coverage record

Synced at fix(plitejs): apply input rules to a key an input method commits. The verification describes these files as they stand there:

To see whether the verification needs another look, find the sync commit with git log --oneline -1 --grep 'apply input rules to a key an input method commits', then run git log --oneline <that commit>..HEAD -- with the table's files and apps/www/scripts/autoformat-input-rules.ts. For each commit it lists, read the diff and confirm four things. The script still builds its editors from the kits the way EditorKit orders them. EXPECTED_MARK_SYNTAX still matches the spec's mark rules where they name a syntax. A new rule shape in either kit file still reaches the script, or exits 2. The script still commits the last key through getUserTextLanding and dispatchUserText the way commitChromeCompositionEndFallback in packages/plitejs/src/react/editable/composition-state.ts does. Move the sync commit in this file forward, naming its subject, only after that check and a run of pnpm check:autoformat-rules.

What it does not cover

• The other kits of EditorKit and their input rules: block shorthands such as # , lists, quotes, code fences, the horizontal rule and link automd. The demo pages use the full EditorKit.
• The browser: beforeinput, a real input method's composition events, mobile keyboards, paste and the caret the DOM shows. The script calls the model's insertText once per key. Its composition commit calls the functions the browser's commit calls, with a target runtime that reports a fixed caret instead of the DOM's and with no composition events. Only the last key of a run is composed. The stored landing is checked in Editing only, two letters into one struck run, with the pending marks set to {}. Suggesting, where typing records a suggestion of its own, goes unchecked. When no rule fires there, the check looks only for a throw and compares neither where the composed key lands nor its marks. A key composed there after bold text comes out bold, where typing gives a plain key. Base fc9906287b does the same. The stored landing passes insertText an explicit point, so insertText skips the pending marks, and the command frame gives the key the marks of the visible text before gone. That bug stays open until a change to how the stored landing applies pending marks fixes it. Its owner is natamox.
• Where the caret lands after a rule and which marks carry to the next key, except as later keys in a sequence show them.
• Redo, undo past the last keystroke and the undo-on-delete of EDIT-PROFILE-AUTOFMT-TEXT-004.
• Content longer than one character, text after the caret, marks other than bold around the caret, and substitutions or smart quotes inside a word.
• Sequences of more than three keys at the gate, and keys outside the 15-character alphabet, so (tm), 1/2 and © are typed only as declared shorthands. A mark rule gets one content per colliding rule and side, so a rule whose several sources complete with the same delimiter is typed with only one of them.
• A known finding whose result changes. An identity names the keys and the context, not the result, so a known failure that gets worse stays green.
• Which of two rules on the same keys should win. The check reports the declaration that never applies; the spec decides.

/pstack:maintain-formal-verification-skill brings this verification back in line after changes that did not recheck it.