Status: Proof sketch documented; no checked contextual Rocq module exists yet
Rocq target module: rocq/liblevenshtein/ContextualCompletion/DraftBuffer.v
Date: 2025-01-21
Authors: Formal Verification Team
This theorem establishes that draft buffer operations (insert, delete) maintain UTF-8 validity and consistency invariants. It ensures that incremental character-level updates preserve well-formed Unicode strings, which is critical for:
User Impact: Without UTF-8 consistency, the system could:
Performance Impact: Character-level operations enable:
\mathcal{O}(1)$ insert/delete vs $\mathcal{O}(n)$ string rebuild)let mut buffer = DraftBuffer::new();
// User types: r, e, s, u, l, t
buffer.insert('r'); // ← 1 byte ASCII
buffer.insert('e');
buffer.insert('s');
buffer.insert('u');
buffer.insert('l');
buffer.insert('t');
assert_eq!(buffer.as_str(), "result"); // ✓ Valid UTF-8
// User types emoji: 🔥 (4-byte character)
buffer.insert('🔥'); // ← 4 bytes UTF-8: F0 9F 94 A5
assert_eq!(buffer.as_str(), "result🔥"); // ✓ Still valid UTF-8
// User hits backspace
assert_eq!(buffer.delete(), Some('🔥')); // ← Removes entire 4-byte char
assert_eq!(buffer.as_str(), "result"); // ✓ Valid UTF-8 preserved
// WRONG implementation would do:
// delete_byte() → removes 1 byte → "result\xF0\x9F\x94" ✗ INVALID UTF-8!
Correctness Properties:
\text{insert}(c);\ \text{delete}() \equiv \text{identity}$len() counts characters, not bytes(* Unicode scalar value - valid UTF-8 character *)
Inductive Char : Type :=
| AsciiChar (c : ascii) (* 1-byte: 0x00-0x7F *)
| TwoByteChar (b1 b2 : byte) (* 2-byte: 0x80-0x7FF *)
| ThreeByteChar (b1 b2 b3 : byte) (* 3-byte: 0x800-0xFFFF *)
| FourByteChar (b1 b2 b3 b4 : byte). (* 4-byte: 0x10000-0x10FFFF *)
(* Draft buffer - sequence of valid UTF-8 characters *)
Definition DraftBuffer := list Char.
(* UTF-8 validity predicate *)
Definition valid_utf8_char (c : Char) : Prop :=
match c with
| AsciiChar a => True (* All ASCII is valid *)
| TwoByteChar b1 b2 =>
(* b1: 110xxxxx, b2: 10xxxxxx *)
(b1 >= 0xC2 /\ b1 <= 0xDF) /\
(b2 >= 0x80 /\ b2 <= 0xBF)
| ThreeByteChar b1 b2 b3 =>
(* b1: 1110xxxx, b2/b3: 10xxxxxx *)
(b1 >= 0xE0 /\ b1 <= 0xEF) /\
(b2 >= 0x80 /\ b2 <= 0xBF) /\
(b3 >= 0x80 /\ b3 <= 0xBF)
| FourByteChar b1 b2 b3 b4 =>
(* b1: 11110xxx, b2/b3/b4: 10xxxxxx *)
(b1 >= 0xF0 /\ b1 <= 0xF4) /\
(b2 >= 0x80 /\ b2 <= 0xBF) /\
(b3 >= 0x80 /\ b3 <= 0xBF) /\
(b4 >= 0x80 /\ b4 <= 0xBF)
end.
(* Buffer validity - all characters are valid UTF-8 *)
Definition valid_buffer (buf : DraftBuffer) : Prop :=
forall c, In c buf -> valid_utf8_char c.
(* Insert character at end *)
Definition insert (buf : DraftBuffer) (c : Char) : DraftBuffer :=
buf ++ [c].
(* Delete last character *)
Definition delete (buf : DraftBuffer) : option (Char * DraftBuffer) :=
match rev buf with
| [] => None (* Empty buffer *)
| c :: rest => Some (c, rev rest) (* Return deleted char + new buffer *)
end.
(* Buffer length (in characters, not bytes) *)
Definition length (buf : DraftBuffer) : nat :=
List.length buf.
(* Convert to UTF-8 bytes *)
Fixpoint to_bytes (buf : DraftBuffer) : list byte :=
match buf with
| [] => []
| c :: rest =>
(char_to_bytes c) ++ (to_bytes rest)
end.
Draft Buffer Consistency: For any valid draft buffer B, the operations insert(c) and delete() preserve UTF-8 validity and maintain consistency invariants.
Specifically:
delete(insert(B, c)) = (c, B)length(B) counts characters, not bytesTheorem draft_buffer_consistency :
forall (buf : DraftBuffer) (c : Char),
valid_buffer buf ->
valid_utf8_char c ->
(* Property 1: Insert preserves validity *)
valid_buffer (insert buf c) /\
(* Property 2: Delete preserves validity *)
(forall buf', delete buf = Some (_, buf') -> valid_buffer buf') /\
(* Property 3: Insert-delete idempotence *)
delete (insert buf c) = Some (c, buf) /\
(* Property 4: Length consistency *)
length (insert buf c) = S (length buf) /\
(forall c' buf', delete buf = Some (c', buf') ->
length buf' = pred (length buf)).
English: If buffer is valid and character is valid UTF-8, then:
Direct proof using UTF-8 invariant preservation. Since Rust's char type is a Unicode scalar value (always valid UTF-8), the proof reduces to showing:
Property 1 (Insert Preserves Validity):
(* Given: valid_buffer buf, valid_utf8_char c *)
(* Goal: valid_buffer (buf ++ [c]) *)
Proof.
unfold valid_buffer.
intros c' Hin.
apply in_app_or in Hin.
destruct Hin as [Hin_buf | Hin_c].
- (* c' from original buffer *)
apply H. auto. (* H: valid_buffer buf *)
- (* c' is the new character *)
simpl in Hin_c.
destruct Hin_c as [Heq | []]; subst.
apply H0. (* H0: valid_utf8_char c *)
Qed.
Property 2 (Delete Preserves Validity):
(* Given: valid_buffer buf, delete buf = Some (c, buf') *)
(* Goal: valid_buffer buf' *)
Proof.
unfold delete.
destruct (rev buf) as [| last rest] eqn:Hrev.
- (* Empty buffer *)
discriminate. (* delete returns None, contradiction *)
- (* Non-empty: buf = rev (last :: rest) *)
injection H as Heq_c Heq_buf'.
subst buf'.
unfold valid_buffer.
intros c' Hin'.
(* c' is in rev rest = original buffer minus last *)
assert (In c' buf) as Hin_orig.
{ apply in_rev. rewrite Hrev. simpl. right. apply in_rev. auto. }
apply H. auto. (* H: valid_buffer buf *)
Qed.
Property 3 (Insert-Delete Idempotence):
(* Goal: delete (buf ++ [c]) = Some (c, buf) *)
Proof.
unfold delete.
rewrite rev_app_distr.
simpl.
reflexivity. (* rev (buf ++ [c]) = [c] ++ rev buf *)
Qed.
Property 4 (Length Consistency):
(* Goal 4a: length (buf ++ [c]) = S (length buf) *)
Proof.
unfold length.
rewrite app_length.
simpl. omega.
Qed.
(* Goal 4b: delete buf = Some (c, buf') → length buf' = pred (length buf) *)
Proof.
unfold delete.
destruct (rev buf) as [| last rest] eqn:Hrev; [discriminate |].
injection 1 as _ Heq_buf'. subst buf'.
unfold length.
rewrite rev_length.
rewrite <- Hrev.
rewrite rev_length.
simpl. omega.
Qed.
All operations terminate trivially:
insert: Appends to list ($\mathcal{O}(1)$ in VecDeque)delete: Pattern match on last element ($\mathcal{O}(1)$)length: List length ($\mathcal{O}(1)$ in implementation, uses cached size)Lemma 1: UTF-8 Char Validity is Decidable
Lemma valid_utf8_char_dec :
forall c : Char, {valid_utf8_char c} + {~ valid_utf8_char c}.
Proof: Case analysis on Char constructors, check byte ranges.
Lemma 2: Empty Buffer is Valid
Lemma empty_buffer_valid :
valid_buffer [].
Proof: Vacuously true - no elements to be invalid.
Lemma 3: Append Preserves Validity
Lemma append_preserves_validity :
forall buf1 buf2,
valid_buffer buf1 ->
valid_buffer buf2 ->
valid_buffer (buf1 ++ buf2).
Proof: Element in append is in one of the two buffers (both valid).
Lemma 4: Reverse Preserves Validity
Lemma rev_preserves_validity :
forall buf,
valid_buffer buf ->
valid_buffer (rev buf).
Proof: In c (rev buf) <-> In c buf (from stdlib), validity preserved.
Lemma 5: Rust Char is Always Valid UTF-8
Axiom rust_char_valid :
forall (c : Char), valid_utf8_char c.
Justification: Rust's char type is a Unicode scalar value, defined to be valid UTF-8. This is enforced by the Rust compiler and standard library.
Primary Implementation:
src/contextual/draft_buffer.rsDraftBufferinsert(), delete(), len(), as_str(), as_bytes()#[derive(Debug, Clone)]
pub struct DraftBuffer {
/// Character storage (VecDeque for efficient push/pop on both ends)
chars: VecDeque<char>, // ← Rust's char = Unicode scalar value (always valid UTF-8)
}
impl DraftBuffer {
/// Insert a character at the end of the buffer.
pub fn insert(&mut self, ch: char) {
self.chars.push_back(ch); // ← O(1) append
}
/// Delete the last character from the buffer (backspace).
pub fn delete(&mut self) -> Option<char> {
self.chars.pop_back() // ← O(1) remove, returns deleted char
}
/// Get the buffer length in characters.
pub fn len(&self) -> usize {
self.chars.len() // ← O(1), counts chars not bytes
}
/// Get the buffer content as a string slice.
pub fn as_str(&self) -> String {
self.chars.iter().collect() // ← O(n) conversion to String
}
/// Get the buffer content as a byte vector (UTF-8).
pub fn as_bytes(&self) -> Vec<u8> {
self.as_str().into_bytes() // ← Guaranteed valid UTF-8
}
}
Correspondence to Formal Specification:
| Formal Construct | Rust Implementation | Correctness Notes |
|---|---|---|
Char type | char (Unicode scalar) | Rust guarantees valid UTF-8 ✓ |
DraftBuffer | VecDeque<char> | Sequence of valid chars ✓ |
insert buf c | self.chars.push_back(c) | Appends to end ✓ |
delete buf | self.chars.pop_back() | Removes from end, returns char ✓ |
length buf | self.chars.len() | Counts characters ✓ |
valid_buffer | Implicit (Rust type system) | VecDeque<char> is always valid ✓ |
to_bytes | self.as_str().into_bytes() | Valid UTF-8 guaranteed ✓ |
Rust Type System Enforcement:
UTF-8 Validity: The Rust compiler enforces that char is a Unicode scalar value:
let c: char = '🔥'; // ✓ Valid 4-byte char
// let c: char = 0xD800 as char; // ✗ Compile error! Surrogate not allowed
No Byte-Level Access: Cannot split characters:
let mut buffer = DraftBuffer::from_string("🔥");
buffer.delete(); // Removes entire 4-byte char atomically ✓
// No way to delete individual bytes! ✓
String Conversion Safety:
let s: String = buffer.as_str(); // Always valid UTF-8
assert!(std::str::from_utf8(s.as_bytes()).is_ok()); // ✓ Never panics
Time Complexity:
insert(c): $\mathcal{O}(1)$ amortized (VecDeque growth)delete(): $\mathcal{O}(1)$ exactlen(): $\mathcal{O}(1)$ exact (cached)as_str(): $\mathcal{O}(n)$ allocationas_bytes(): $\mathcal{O}(n)$ allocationSpace Complexity:
Benchmarks (from implementation comments):
Location: src/contextual/draft_buffer.rs:284-350 (#[cfg(test)])
Test 1: Insert Preserves Validity
#[test]
fn test_insert() {
let mut buffer = DraftBuffer::new();
buffer.insert('a');
buffer.insert('b');
buffer.insert('c');
assert_eq!(buffer.as_str(), "abc"); // ✓ Valid UTF-8
assert_eq!(buffer.len(), 3); // ✓ Character count
}
Test 2: Multi-Byte Character Handling
#[test]
fn test_unicode() {
let mut buffer = DraftBuffer::new();
buffer.insert('你'); // 3-byte Chinese character
buffer.insert('好');
assert_eq!(buffer.as_str(), "你好");
assert_eq!(buffer.len(), 2); // ✓ 2 characters, not 6 bytes
}
Test 3: Delete Preserves Validity
#[test]
fn test_delete() {
let mut buffer = DraftBuffer::from_string("test");
assert_eq!(buffer.delete(), Some('t'));
assert_eq!(buffer.as_str(), "tes"); // ✓ Valid UTF-8
assert_eq!(buffer.len(), 3);
}
Test 4: Insert-Delete Idempotence
#[test]
fn test_insert_delete_idempotence() {
let mut buffer = DraftBuffer::from_string("hello");
let original = buffer.as_str();
buffer.insert('!');
assert_eq!(buffer.delete(), Some('!'));
assert_eq!(buffer.as_str(), original); // ✓ Recovered original
}
Test 5: Emoji Handling (4-byte chars)
#[test]
fn test_emoji() {
let mut buffer = DraftBuffer::new();
buffer.insert('🔥'); // 4-byte emoji
buffer.insert('💯');
assert_eq!(buffer.as_str(), "🔥💯");
assert_eq!(buffer.len(), 2); // ✓ 2 chars, not 8 bytes
assert_eq!(buffer.delete(), Some('💯'));
assert_eq!(buffer.as_str(), "🔥"); // ✓ Atomic delete
}
rholang-language-server Integration:
Location: /home/dylon/Workspace/f1r3fly.io/rholang-language-server/tests/test_completion.rs
Test: Incremental Completion Updates
#[test]
fn test_incremental_typing() {
let client = setup_lsp_client();
// User types: r, e, s
client.did_change("r");
let completions = client.completion();
assert!(completions.contains("result")); // ✓ Prefix "r" matches
client.did_change("e"); // Now "re"
let completions = client.completion();
assert!(completions.contains("result")); // ✓ Prefix "re" matches
client.did_change("s"); // Now "res"
let completions = client.completion();
assert!(completions.contains("result")); // ✓ Prefix "res" matches
// Each update must maintain UTF-8 validity (tested implicitly)
// If UTF-8 was corrupted, completion query would panic ✗
}
Test: Unicode Symbol Completion
#[test]
fn test_unicode_symbols() {
let code = r#"
new 变量1 in {
new 变量2 in {
变 // ← Cursor: typing Chinese prefix
}
}
"#;
let completions = query_completion(code, "变");
assert_eq!(completions, vec!["变量2", "变量1"]); // ✓ UTF-8 preserved
}
Property 1: UTF-8 Round-Trip
proptest! {
#[test]
fn utf8_roundtrip(chars in prop::collection::vec(any::<char>(), 0..100)) {
let mut buffer = DraftBuffer::new();
for c in &chars {
buffer.insert(*c);
}
let string = buffer.as_str();
assert!(std::str::from_utf8(string.as_bytes()).is_ok()); // ✓ Valid UTF-8
let recovered = DraftBuffer::from_string(&string);
assert_eq!(recovered.as_str(), string); // ✓ Round-trip works
}
}
Property 2: Insert-Delete Idempotence
proptest! {
#[test]
fn insert_delete_inverse(
initial in prop::collection::vec(any::<char>(), 0..100),
c in any::<char>()
) {
let mut buffer = DraftBuffer::new();
for ch in initial {
buffer.insert(ch);
}
let before = buffer.as_str();
buffer.insert(c);
buffer.delete();
assert_eq!(buffer.as_str(), before); // ✓ Identity preserved
}
}
Property 3: Length Consistency
proptest! {
#[test]
fn length_counts_chars_not_bytes(chars in prop::collection::vec(any::<char>(), 0..100)) {
let mut buffer = DraftBuffer::new();
for c in &chars {
buffer.insert(*c);
}
assert_eq!(buffer.len(), chars.len()); // ✓ Character count
let bytes = buffer.as_bytes();
// Length in bytes may be different (multi-byte chars)
assert!(bytes.len() >= chars.len()); // ✓ Bytes ≥ chars
}
}
Target module contents:
Update rocq/liblevenshtein/ContextualCompletion/Core.v
Char, DraftBuffer, valid_utf8_char typeschar axiomCreate rocq/liblevenshtein/ContextualCompletion/DraftBuffer.v
insert, delete, length functionsExtract to verified implementation
VecDeque<char> maintains invariantsPriority: Medium (Rust type system already enforces UTF-8)
Candidate coverage:
Current: $\mathcal{O}(1)$ insert/delete, $\mathcal{O}(n)$ string conversion
Potential Optimization: Lazy string conversion
as_str() result, invalidate on mutationDecision: Keep eager string conversion unless profiling shows that caching justifies the extra memory.
Current: Operates on Unicode scalar values (code points)
Optional extension: Grapheme cluster awareness
"é" can be 1 code point (U+00E9) or 2 (U+0065 + U+0301)Use case: Proper handling of complex emoji (skin tone modifiers, etc.)
Depends on: None (foundational, relies only on Rust type system)
Required by:
See also:
char documentation: https://doc.rust-lang.org/std/primitive.char.htmlCreated:
char guarantees)Status: Proof-sketch documentation complete; no checked contextual Rocq module exists yet.
Key Insight: Most correctness comes "for free" from Rust's char type. Formal proof mainly needs to capture this guarantee as an axiom.
Implementation:
src/contextual/draft_buffer.rs:112-159 - Insert/delete operationssrc/contextual/draft_buffer.rs:284-350 - Unit testsRust Documentation:
Unicode Specification:
Formal Verification:
char guarantees)Last Updated: 2025-01-21 Review trigger: Reconcile this page when a checked contextual Rocq module is added.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |