Authored recording order

Handle $ARGUMENTS. check, or no argument, runs the gate bound. deep runs --blocks=2 and compares its failures with Findings. lower runs --lower after a fix removes a known finding. case <identity> runs --case=<identity> to print one case's full detail. update brings the verification in line with changed code, as Coverage record says.

The property. Bob runs one command on a document that holds another author's pending change. In Suggesting and in Editing, accepting every change gives what a plain editor gives when it runs the same command on the accepted document. In Suggesting, rejecting every change gives what rejecting them gave before the command, and after a key, so does rejecting only Bob's. In Suggesting, each element's proposed children are the ones accepting everything keeps. After a key, a letter typed next lands where the plain editor puts it. In both intents the review ledger equals the kernel's projection after loading, after the command and after its undo, undo gives back the document before, review marks included, redo gives back the result, and an undo after another peer appends a paragraph gives the document before with that paragraph.

The harm. A reviewer who accepts a suggestion gets a document the author never typed, and one who rejects it keeps part of it. Seven recording fixes landed between 2026-10-24 and 2026-11-02, each found one case at a time by a lucky seed or a beta tester, and three seeds of the sampled laws in packages/plitejs/test/authored-tree-recording-laws.spec.ts still name open bugs.

What it checks

packages/plitejs/scripts/authored-recording-order.ts runs the real recorder, resolver and history on every case up to a bound. It checks the TypeScript code itself, not a model of it, because no verifier runs on this code.

1. Worlds. quotes is the recording laws' schema: paragraphs and quotes of paragraphs, with links, a pending align line format on paragraphs and quotes, and no prefix. titled puts a required title before the same body through schema.content.prefix, the shape behind 09a9769bcc.
2. Documents. packages/plitejs/scripts/authored-documents.ts, the builder the decision-order check uses, builds every document of up to --blocks top-level blocks, --marks pending marks and --changes changes. It places marks at every place recording writes one: a join, a joined claim, a split, a follow, a block's or leaf's insertion or deletion, a wrap or unwrap, an align format with and without its stored value, and the cut link that Enter inside a link writes. The script turns change s0 into alice and s1 into bob, so --marks=2 gives Bob pending changes of his own. In titled, the first block becomes the title, and the title never carries a whole-block insertion or deletion, because a required block cannot be pending as a whole. In both worlds, no document holds a pending join on a quote or on a block right after one, because no recording writes one there: Suggesting records a join into a quote as a copy of the line moved inside it and a struck original, and Editing merges the lines at once.
3. Commands. Every step at every caret beside a letter: type Z, Enter, Backspace and Delete, and a selection delete in both directions between every two carets. Every command the recording laws use: paste of two lines at every caret, deleteRange and typeOver from every letter to itself or a later one, transferText, moveNode and transferNode for every pair of letters, wrap, unwrap and removeLink at every letter, and replaceChildren at every shift. Each runs as Bob in Suggesting and in Editing.
4. Laws. The script calls the laws in packages/plitejs/test/support/recording-laws.ts, the same code the sampled spec calls, and adds the history laws. A case records its first failure per rule:
   • recording-accept: accepting everything differs from what a plain editor gives when it runs the same step or command on the accepted document. After a step, the law also compares the two after a letter typed next.
   • recording-reject: rejecting everything differs from doing so before the command. After a step, the law also compares rejecting only Bob's changes.
   • recording-applies: accepting or rejecting everything does not apply.
   • recording-proposed: after a Suggesting command, an element's proposed children differ from the ones accepting everything keeps.
   • recording-schema: the step or command throws a schema validation error under review where a plain editor on the accepted document runs it.
   • recording-plain: a step or a text command throws a schema validation error in a plain editor on the accepted document. The rule leaves out moveNode, transferNode, nest, wrap, unwrap and replaceChildren, because each names a node or slot the schema may refuse on purpose. A step runs where the accept law places it on the accepted document, so a step whose letter accepting removes still runs. Every other law reads a plain-editor schema error as a refusal and skips the case, which is how typing over a whole document that starts with a quote stayed hidden until this rule.
   • recording-ledger: the review ledger differs from the kernel's projection after the load, the command or its undo.
   • recording-undo: undo, redo, the command again after undo, or undo after another peer appends a paragraph does not give what it should. The remote paragraph goes at the end of the document, because beside a moved letter the law would have to pick a side. An undo that puts a block back at the end could land on either side of that paragraph, so the law checks that the paragraph is still there and that the other blocks are the document before.
   • recording-shape: an empty element, two joins on a line, a typed letter with a deletion, a doubled letter or another author's lost letter.
   • recording-throws: any other error.
5. A refusal the editor gives on purpose, such as "decide the pending join first", counts in the summary's refused and is not a failure, because the editor declined what it cannot record. A refusal after the laws started comparing is a failure.
6. It compares the findings with packages/plitejs/scripts/authored-recording-order-baseline.json through tooling/scripts/finding-baseline.mjs. Every finding is filed under packages/plitejs/src/authored. An identity names the world, the document as the builder's story prints it, the intent and the command, never the result.

Run it

Run every command from the repository root.

• pnpm check:authored-recording checks the gate bound: one block, one pending mark, line formats, both worlds. With one mark, every pending change is alice's. It compares 9,062 cases on 71 documents in 28 to 33 s while other sessions load the machine, with load averages from 16 to 77, and in 89 to 110 s at load averages from 71 to 89. It prints one JSON summary line, then each finding the baseline does not list. pnpm check authored-recording runs the same step through the check runner, and pnpm check --affected runs it for a change under packages/plitejs/src/, to the script, its document builder or baseline, to a file under packages/plitejs/test/support/, to config/plite-source-aliases.ts or to tooling/scripts/finding-baseline.mjs.
• --blocks, --marks and --changes raise one part of the bound. --world=quotes --blocks=2 builds 293 documents and compares 92,250 cases in 200 to 330 s on a quiet machine, and in 684 s while other sessions load it. --marks=2 gives Bob his own pending changes. A bound other than the gate's, --world, --case or --replay skips the baseline and exits 1 on any failure.
• --world=quotes or --world=titled runs one world.
• --replay='<counterexample>' runs every command on the document a sampled recording law's counterexample leaves. Pass the [initial, history, command] array fast-check prints. It runs in the quotes world and skips the baseline.
• --case='<identity or part of one>' prints the full stack of each failure whose identity contains it. Add --world to make it quick, such as --world=titled --case='title("a") paragraph{join alice:1}("b") :: propose Enter at b|1'.
• --jobs=<n> sets the number of worker processes, the machine's cores up to 16 by default.
• Exit 0 is a pass and exit 1 a finding or a document that does not load. Exit 2 is a bad flag or a crashed worker. At the gate the run also fails when it compares other than 9,062 cases, the GATE_CASES constant, so a change that stops commands from applying cannot shrink the gate while the baseline still matches. Update the constant only with the reason the count moved.
• After a fix removes a known finding, the gate fails until you run pnpm check:authored-recording --lower. The baseline never grows. --init seeds only a rule the baseline lacks, and --lower and --init write nothing when the case count misses GATE_CASES.

Read a failure

A finding prints its rule, identity and the first line of its detail:

recording-reject titled title{align alice:1}("a") paragraph("b") :: propose Enter at a|0
  rejecting everything differs: {"before":[...],"intent":"propose","step":{...}}

recording-schema titled title("a") paragraph("b"{insert alice:1}) :: propose select a|0..b|1 Backspace
  Editor primary root cannot contain "title".

Both are known findings. In the first, Bob's suggested Enter at the start of the title records a new title and turns the old one into a paragraph, and rejecting everything leaves both. In the second, Bob's suggested delete across the title and Alice's pending insertion builds a document the schema refuses. Run --case on the identity for the full diff and stack.

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

• Real bug. A user can reach the document and run the command, the plain editor runs it, and a law still fails. Fix the recorder, resolver or history, then run --lower.
• Modeling error. The document is one no recording reaches, or the law's oracle is ambiguous for that command, such as an undo that has to choose which side of a moved letter another peer's text stays on. Fix the builder or the script with the reason, as the title rule and the remote paragraph above do.
• Intended change. A change to what a command does changes the plain editor too, so the laws follow it. Never weaken a law or add a baseline entry to get green.

Findings

The gate finds 261: 43 recording-accept, 33 recording-applies, 5 recording-plain, 72 recording-reject and 108 recording-schema. All but 8 sit beside the required title, which no sampled law's schema holds. Each class is one cause:

• A selection delete, deleteRange or typeOver across the title and the body. With any pending change in the document, the step throws Editor primary root cannot contain "title" in Suggesting, and in Editing when the title holds a pending deletion. 108 recording-schema entries.
• Paste of two lines in a titled document. Rejecting everything does not apply, or gives another document, and accepting everything differs from the plain editor. Pasting into the title records a new title and a type change on the old one. 33 recording-applies, 36 recording-reject and 8 recording-accept entries.
• Suggested Enter in a titled document. Rejecting everything gives another document. At the title's start the old title becomes a paragraph under a new empty title, and the reject leaves both. The split records no history of the type and properties it drops from the new line, and the resolver treats the emptied title as gone, so the line that holds the title's text stands in for it instead of rejoining it. 35 recording-reject entries, and 8 recording-accept entries beside a body another author struck whole.
• A plain Backspace or range delete that leaves the title alone. In a plain editor, Backspace at the start of a quote right after an empty title joins the quote's line into the title, and a delete or typeOver from the title's first letter, inside a link, to the end of the body joins the body into it. Either leaves the root without the body block the schema requires, so the step throws Editor primary root requires at least 2 children. 5 recording-plain entries.
• Editing Enter right before another author's struck letter. The next letter Bob types lands on the other line than a plain editor puts it. 4 quotes and 12 titled recording-accept entries.
• A wrap inside a quote with a pending unwrap. Accepting everything loses Bob's wrap: quote{unwrap alice:1}(paragraph("a")) with a suggested wrap of a accepts to paragraph("a"), where the plain editor gives quote(paragraph("a")). 3 quotes and 1 titled recording-accept entries, and in titled 1 more beside a pending join.
• Moves and transfers beside the title. moveNode and transferNode of a quoted line with a pending align or unwrap to after the title, and transferText across a split link, accept to another document than the plain editor's. 6 recording-accept entries.
• Suggested Enter at the start of a line that holds another author's joined claim. Rejecting everything does not give back the document before. A prototype that fixes the titled Enter class clears this entry too, so it has the same cause. 1 recording-reject entry.

--world=quotes --blocks=2 fails 643 cases: 260 recording-accept, 356 recording-undo, 11 recording-ledger, 10 recording-reject and 6 recording-plain. The deep run reads no baseline. Two of its classes are the gate's quotes classes: Editing Enter before a struck letter in 28 cases, and a suggested Enter beside a joined claim in all 10 reject cases. It adds these classes:

• Undo after another peer appends a paragraph. In Editing, a delete that merges two blocks, such as Delete at the end of quote(paragraph("a")) before paragraph{align alice:1}("b"), leaves quote(paragraph("ab")) after its undo once another peer appends a paragraph. All 356 recording-undo cases, 18 of them an Editing typeOver of a quote and the block after it.
• Moves, deleteRange and typeOver beside a pending join inside a quote. paragraph("a") quote(paragraph("b") paragraph{join alice:1}("c")) with moveNode a before c accepts to another document than the plain editor's. 101 recording-accept cases.
• Commands beside a pending unwrap of a two-line quote. Wraps, moves, deleteRange, typeOver and replaceChildren on paragraph("a") quote{unwrap alice:1}(paragraph("b") paragraph("c")) accept to another document. 77 recording-accept cases.
• Editing moves of a quoted line with a pending align. quote(paragraph[align center]{align alice:1}("a")) paragraph("b") with moveNode a after b. 32 recording-accept cases.
• deleteRange and typeOver beside a line another author struck whole. 20 recording-accept cases, such as deleteRange a..b on paragraph("a") quote(paragraph("b") paragraph{delete alice:1}("c"{delete alice:1})). In 4 of them a typeOver covers the whole document once the struck line is gone.
• A plain delete from the start of a quote's later line to the start of a block two lines below. On quote(paragraph("a") paragraph("b")) paragraph("c") paragraph("d"), which accepting a pending unwrap leaves, select b|0..d|0 with Backspace or Delete throws Editor element "quote" at [0] cannot contain "text", because the delete puts an empty copy of the quote before it. A delete from b|0 to the empty line that accepting another author's struck c leaves throws the same error. 6 recording-plain cases. The table subject's Open work owns this with the other hanging deletes from a container's block.
• The review ledger after an Editing delete or move and its undo. Beside a pending split the accepted preview differs from the kernel's in 9 cases, and beside a pending join the proposed preview does in 2.
• Moves beside a pending split. 2 recording-accept cases.

What a pass proves

The gate catches a history that loses its mappings or keeps a redo it should clear, and a review ledger that merges two authors' cards. Bugs planted at fc9906287b showed where that holds:

• Mutant rec-undo-h2, where addMapping in packages/plitejs/src/history/history-state.ts drops the mapping that a history-skip commit queues, gives 4,521 recording-undo findings. Undo after another peer appends a paragraph no longer applies, because the undo entry still counts the document without that paragraph. Undo and redo alone never see this bug, which is why the remote law exists.
• Mutant rec-undo-h5, where a new undo entry no longer clears the redo stack, gives 4,521 recording-undo findings. The command again after its undo leaves a redo.
• Mutant rec-r8, where the ledger merges a card with the previous one by book alone and not by author, gives 777 recording-ledger findings.
• The three open seeds of the sampled laws, -956128617, -627200196 and 719949670, fail the same law here. --replay with each counterexample gives 3, 16 and 7 recording-proposed findings, and the counterexample's own command is among them. Seed 198320648 passes in the spec and here, because an earlier fix removed its bug.

The gate does not catch three resolver bugs, and neither does --world=quotes --blocks=2, whose findings under each mutant equal the clean run's one for one:

• rec-r2, where rejecting a cut joins its halves without the content between them, in packages/plitejs/src/authored/tree/cuts.ts.
• rec-r6, where a rejected cut whose left half no longer holds keeps its dependencies, in the same file.
• rec-r12, where resolveAuthoredChildren ignores a stored accept verdict.

Each needs a document no generated document holds: plain content between the halves of a cut, which only an earlier edit writes, or a stored verdict. The decision-order check and the sampled laws at their default runs miss them too.

Coverage record

Synced at test(plitejs): check every recording command's accept and reject on every small document. 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 "check every recording command's accept and reject", then run git log --oneline <that commit>..HEAD -- with the table's files and packages/plitejs/scripts/authored-recording-order.ts. For each commit it lists, read the diff and confirm three things. A new command or mark kind that recording writes is in actsOf or the builder. A new refusal the editor gives on purpose is still an EditorRefusalError. The laws still compare with a plain editor, not with the resolver's own output. Move the sync commit in this file forward, naming its subject, only after that check and a run of pnpm check:authored-recording.

What it does not cover

• Documents of more than one top-level block at the gate, and prior edits. The sampled laws start at two blocks with two-letter lines and up to three earlier edits, so they still own that space.
• Plain content between the halves of a cut and stored verdicts, so the three resolver mutants in What a pass proves pass.
• --replay reads only a recording law's counterexample, [initial, history, command]. The ledger law's counterexample has another shape, and the flag refuses it.
• A bug the resolver repeats before and after the command. The reject law compares the resolver with itself across the command, so a resolver that rejects some stored shape wrongly passes when the shape was already there.
• A node command that a plain editor's schema refuses wrongly. recording-plain leaves out commands that name a node or slot, and every other law skips a case whose plain editor throws a schema error.
• A key typed over a selection. typeOver calls tx.text.insert, while a keystroke dispatches the text.insert command, which replaces whole blocks first. Over the whole text of a quote with a pending unwrap, that command refuses in both intents where tx.text.insert records, and the check would count the refusal as no failure.
• Decisions one at a time, stored verdicts and their order, which the authored-decision-order check owns.
• Named roots, nested roots, tables, lists and marks other than links, which neither world holds.
• The browser, beforeinput, IME, the clipboard and Yjs.

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