1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
//! Conformance harness (0024): a reference model (plain String) and the
//! real editor driven by the SAME generated operation streams through
//! the production headless path. Every step asserts text equality plus
//! the protocol invariants the TLA+ spec proves at the model level:
//! panes reference live docs (NoStalePane), the revision never goes
//! back (RevisionTracksPublications — the epoch counts publications,
//! undo included), anchors stay inside the text on char boundaries.
//! The transaction/ticket boundary itself has its own oracle module:
//! transaction_conformance.rs (R12).
//!
//! Deterministic: a seeded xorshift, no wall clock, no I/O.
use super::*;
use strop_core::Buffer;
/// Seeded PRNG (xorshift64) — the stream is reproducible by seed.
struct Rng(u64);
impl Rng {
fn next(&mut self) -> u64 {
let mut x = self.0;
x ^= x << 13;
x ^= x >> 7;
x ^= x << 17;
self.0 = x;
x
}
fn below(&mut self, n: usize) -> usize {
(self.next() % n.max(1) as u64) as usize
}
}
/// The reference model: text as a String, cursor as a byte offset, one
/// undo stack of full-text snapshots (the model's history is exact).
struct Model {
text: String,
cursor: usize,
undo: Vec<String>,
/// Text as of the last session boundary (vim's undo target).
boundary: String,
}
impl Model {
fn clamp(&mut self) {
if self.cursor > self.text.len() {
self.cursor = self.text.len();
}
while self.cursor > 0 && !self.text.is_char_boundary(self.cursor) {
self.cursor -= 1;
}
}
fn insert(&mut self, s: &str) {
self.clamp();
self.text.insert_str(self.cursor, s);
self.cursor += s.len();
}
fn backspace(&mut self) {
self.clamp();
if self.cursor > 0 {
let prev = self.text[..self.cursor].chars().last().unwrap().len_utf8();
self.text.replace_range(self.cursor - prev..self.cursor, "");
self.cursor -= prev;
}
}
/// vim's undo unit is the insert SESSION: at a boundary, the undo
/// target is the text AS OF the previous boundary.
fn mark(&mut self) {
self.undo.push(self.boundary.clone());
self.boundary = self.text.clone();
}
fn undo(&mut self) {
if let Some(t) = self.undo.pop() {
self.text = t;
self.cursor = self.cursor.min(self.text.len());
self.clamp();
// the restored state IS the new session's start point
self.boundary = self.text.clone();
}
}
fn left(&mut self) {
self.clamp();
if self.cursor > 0 {
self.cursor -= self.text[..self.cursor].chars().last().unwrap().len_utf8();
}
}
fn right(&mut self) {
self.clamp();
if self.cursor < self.text.len() {
self.cursor += self.text[self.cursor..].chars().next().unwrap().len_utf8();
}
}
}
/// One generated operation stream, applied to both. Invariants checked
/// every step on the real editor.
fn run_stream(seed: u64, ops: usize) {
let mut rng = Rng(seed);
let mut model = Model {
text: String::new(),
cursor: 0,
undo: Vec::new(),
boundary: String::new(),
};
let mut e = Editor::new(Buffer::from_text(""));
e.feed(Key::Esc); // dismiss the welcome card (first key is a card key)
e.feed_text("i");
// the epoch counts publications (typing, undo moves included): it
// never goes back within a document's life (RevisionTracksPublications)
let mut last_revision = e.buf().revision().get();
for step in 0..ops {
let choice = rng.below(100);
if choice < 40 {
let c = (b'a' + (rng.below(26)) as u8) as char;
model.insert(&c.to_string());
e.feed(Key::Char(c));
} else if choice < 55 {
model.backspace();
e.feed(Key::Backspace);
} else if choice < 65 {
model.left();
e.feed(Key::Left);
} else if choice < 75 {
model.right();
e.feed(Key::Right);
} else if choice < 82 {
// session boundary: Esc closes the unit in both
e.feed(Key::Esc);
model.mark();
// then undo one unit
e.feed_text("u");
model.undo();
e.feed_text("i");
} else {
let c = (b'a' + (rng.below(26)) as u8) as char;
model.insert(&c.to_string());
e.feed(Key::Char(c));
}
let _ = step;
// text equality — through the public accessor, never the field
let got = e.buf().text().to_string();
assert_eq!(
got, model.text,
"seed {seed} step {step}: editor and model diverged"
);
// invariants: cursor in bounds on a char boundary
let h = e.head();
assert!(h <= e.buf().len_bytes(), "cursor past the text");
assert!(e.buf().is_boundary(h), "cursor mid-char");
// the revision is the publication count: monotonic, never back
let revision = e.buf().revision().get();
assert!(
revision >= last_revision,
"seed {seed} step {step}: revision went back ({last_revision} -> {revision})"
);
last_revision = revision;
// every pane references a live document (NoStalePane)
for p in &e.panes {
assert!(e.docs.get(p.doc).is_some(), "pane holds a stale doc id");
}
}
}
#[test]
fn conformance_generated_streams_match_the_model() {
for seed in [1, 7, 42, 1337, 99991] {
run_stream(seed, 200);
}
}