Module 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.

Verified contract (Verus 0.2026.09.06, rustc 1.98.0, z3 4.16.0):

• anchors before the edit never move;
• anchors at/past the old end shift by the delta (right affinity);
• anchors inside the replaced range collapse to the edit start;
• the mapping is monotone and stays inside the new buffer length.

Functions

check_batch

Sort by start and validate: out is the batch production applies. (Sort, then sweep consecutive pairs, like prepare_replacements.) clippy::result_unit_err / needless_range_loop: the unit error is the verified contract (the ensures clauses carry the reason), and the indexed sweep is what the invariants prove over.

map_position

One anchor through one edit. Callers guarantee no overflow: positions are byte offsets bounded by the buffer length, and new_end is the post-edit end of the replaced range (start + replacement length).