Crate strop_core 

strop-core: the buffer. A rope, byte-offset positions, edit ops. No UI, no modes, no grammar — the thing everything else edits.

Modules

cohortguard

The recovery-cohort kernel, verified (0057 VF18): the checkpoint completeness decision, the save-retirement staleness rule and the cohort watermark step for draft recovery (0056 AR04 §5). These are the decisions editor/recovery/{mod,store}.rs make on the real checkpoint path — extracted pure and called from those sites, never a copied algorithm. cargo verus verify checks them; the normal build compiles the verus! block as plain Rust (ghost code erases), the same arrangement as editmap.rs (0045).

commands

Frontend command metadata shared by the TUI, native GUI and automation. Dispatch ownership stays in the engine; this data carries only stable identities, user-facing rows and whether the row is dispatchable today.

diagnostics

Mutation diagnostics at the mechanics boundary, including open undo groups.

editmap

The anchor-mapping kernel, verified (0045): map_position carries the proof of its contract in-tree; cargo verus verify checks it, and the normal build compiles the verus! block as plain Rust (ghost code erases). This is the production function editor/transact.rs calls — not a copy.

frontend_input

Physical/logical input facts before an editor or terminal chooses semantics. No toolkit types, grammar normalization, native work or implicit key expansion.

history

Undo history (Helix helix-core/history.rs lineage, ported): revisions form a tree — every committed transaction is a node holding both its undo and redo edit sets; u walks to the parent, Ctrl-r descends to the last-visited child. Editing after an undo forks a new branch; the tree keeps the old one (0001 pillar 4: Neovim users expect branches).

id

Stable identities and typed coordinates (0014 wave 2).

languages

The canonical language metadata catalog (0051 §3): ONE in-repo table mapping file extensions to language names and back. The LSP registry and the query compiler both consume this — there is no second table.

layout

The layout layer (0017, R6 in 0031): one line’s byte↔display-cell maps and grapheme boundaries. Every visible-line consumer — renderer, cursor placement, selection overlays, diagnostics, mouse hit-testing — reads this instead of deriving positions by char index.

mutguard

The mutation-authority kernel, verified (0057 VF18): who may apply a text mutation, who may save, and when a confirmed save retires dirty state. The decisions are the guards buffer/mutation.rs and buffer/io.rs run on the real path — extracted pure and called from those guards, never a copied algorithm. cargo verus verify checks them; the normal build compiles the verus! block as plain Rust (ghost code erases), the same arrangement as editmap.rs (0045).

path_serde

Versioned native path representation. No lossy round-trip can select a file.

process

Worker-only child ownership. Cancellation revokes a private Unix process group or a helper’s lease; only its owner may revoke the capability and reap the PID.

projectguard

The projection-admission kernel, verified (0057 VF18): whether a journal edit to a collection’s projected view lands inside one excerpt’s writable body. Generated chrome (headers, gap rows, card borders) owns no edit — write-back refuses it — and this decision is the guard editor/collections/editing.rs runs per sequential change on the real path, extracted pure and called from that loop, never a copied algorithm. cargo verus verify checks it; the normal build compiles the verus! block as plain Rust (ghost code erases), the same arrangement as editmap.rs (0045).

searchguard

The search publication-boundary kernel, verified (0063 §6.6): the decisions SearchLifecycle.tla names as its invariants, carried as proof obligations on the production functions the guard sites call — not a copy. cargo verus verify checks them; the normal build compiles the verus! block as plain Rust (ghost code erases), the same arrangement as editmap.rs (0045).

selection

One selection model for everything (0014 wave 2): normal mode is a collapsed selection, visual mode is a stretched one, multicursor is several. Cursor / anchor / extra-cursors used to be three fields that could disagree; the set owns them with the invariants in one place.

theme

The one strop-owned color seed (0065 D3). Every surface — TUI render constants and the terminal’s default palette — derives from these values; nothing restates a hex triple locally. Config-file overrides are 0005’s follow-on; until then this module is the single source.

viewguard

The prepared-view freshness kernel, verified (0057 VF18): the staleness re-key rule for the published PreparedView (0056 AR03). A prepared pane window is keyed by document identity + revision and the owning view generation; when the live document revision moves past the prepared one, the window is stale and must not drive coordinate conversions or viewport decisions. The decision is the one editor/prepare.rs::PreparedPane::is_stale makes on the real paint path — extracted pure and called from it, never a copied algorithm. cargo verus verify checks it; the normal build compiles the verus! block as plain Rust (ghost code erases), the same arrangement as editmap.rs (0045).

worker

Structs

Buffer

A text buffer. Positions are UTF-8 byte offsets, everywhere (0001 §5.1).

BufferSeed

A pure, serializable image of a buffer at the startup seed boundary. The buffer’s diagnostic trace identity is deliberately absent: it names a process-local incarnation, not document semantics.

Change

HistoryMove

InputEdit

Pre-edit and post-edit geometry recorded at the instant text changes.

PreparedReplacements

Validated, sorted replacements bound to one exact buffer incarnation/revision. The editor may restore prompt selection state before acquiring its write lease.

Range

A half-open byte range [start, end) plus its vim shape. Fields are ByteOffset — the storage coordinate is typed end to end (0014).

Replacement

SavePlan

The frozen save plan (0058 WK09): admission evidence decomposed so the engine can route the write through the worker’s Store intent. Carries the same fields SaveRequest::execute consumes in-process.

SaveReceipt

SaveRequest

SystemEdit

UserEdit

Enums

ChangeOrigin

EditError

MotionShape

How vim thinks about a range (0014): charwise ops carry the motion’s inclusivity (dfx vs dtx differ by it); linewise is line-shaped. Blockwise lands with visual block — the enum is the extension point.

ReadonlyReason

Why a buffer refuses edits (0056 AR14): the typed owner :explain renders, recorded at the site that actually imposed the policy — never a generic hint. None alongside readonly is reserved for tests that poke the mutation guard directly.