Purpose: This document specifies the formal verification requirements (Coq proofs) needed to enable mathematically proven correctness guarantees for downstream consumers of liblevenshtein-rust's contextual completion engine.
Status: Documentation complete, Coq proofs awaiting implementation Priority: P0 for LSP consumers requiring formal verification (rholang-language-server)
The contextual completion engine (Phase 9) provides scope-aware code completion with hierarchical visibility, draft buffers, and checkpoint-based undo. While the implementation is thoroughly tested (93 passing tests, property-based validation), formal verification using Coq is required to provide mathematical certainty for safety-critical applications.
Current State: Empirical confidence via property-based testing
Gap: No mathematical proof of correctness
Blocked Use Cases:
This section lists the 7 theorems requiring formal proof in Coq. Theorems 1 and 6 are blocking for LSP formal verification; the remaining 5 are useful but not critical.
Statement: For any context C in the context tree, a term t is visible in C if and only if:
t is finalized in C, ORt is finalized in some ancestor context A where A is reachable from C via parent linksFormal Specification (Coq):
(* Context tree structure *)
Inductive Context : Type :=
| GlobalContext : Context
| ChildContext : Context → ContextId → Context.
(* Term finalization relation *)
Definition finalized_in (t : string) (c : Context) (dict : Dictionary) : Prop :=
∃ value : Vec ContextId,
dictionary_lookup dict t = Some value ∧
List.In c value.
(* Ancestor relation *)
Inductive ancestor : Context → Context → Prop :=
| ancestor_direct : ∀ C id, ancestor C (ChildContext C id)
| ancestor_trans : ∀ C1 C2 C3,
ancestor C1 C2 → ancestor C2 C3 → ancestor C1 C3.
(* Visibility relation *)
Definition visible_in (t : string) (c : Context) (dict : Dictionary) : Prop :=
finalized_in t c dict ∨
(∃ A : Context, ancestor A c ∧ finalized_in t A dict).
(* THEOREM 1 *)
Theorem context_tree_visibility :
∀ (C : Context) (t : string) (dict : Dictionary),
visible_in t C dict ↔
(finalized_in t C dict ∨
∃ A : Context, ancestor A C ∧ finalized_in t A dict).
Proof.
(* Proof strategy: induction on the context tree, using ancestor
reflexivity/transitivity and the definition of visible_in. *)
Admitted.
Blocking:
Coq File: formal-verification/coq/Visibility.v
Dependencies:
ContextTree.v)Dictionary.v)AncestorRelation.v)Estimated Effort: 2-4 weeks
Statement: For contexts C₁ and C₂ where C₂ is a child of C₁:
C₁ are visible in C₂C₂ are NOT visible in C₁ unless also finalized in C₁ or its ancestorsFormal Specification (Coq):
(* Parent relation *)
Definition parent (C1 C2 : Context) : Prop :=
∃ id : ContextId, C2 = ChildContext C1 id.
(* THEOREM 6 *)
Theorem hierarchical_visibility_soundness :
∀ (C1 C2 : Context) (t : string) (dict : Dictionary),
parent C1 C2 →
(* Part 1: Inheritance *)
(visible_in t C1 dict → visible_in t C2 dict) ∧
(* Part 2: Isolation *)
(finalized_in t C2 dict →
¬visible_in t C1 dict ∨
finalized_in t C1 dict ∨
∃ A : Context, ancestor A C1 ∧ finalized_in t A dict).
Proof.
(* Proof strategy: inheritance follows by extending the ancestor chain from
C1 to C2; isolation follows by case analysis on visible_in for C1 and the
absence of descendant visibility in the definition. *)
Admitted.
Blocking:
Coq File: formal-verification/coq/Hierarchy.v
Dependencies:
Estimated Effort: 1-2 weeks (builds on Theorem 1)
Statement: Draft buffers correctly handle multi-byte UTF-8 characters without corruption.
Informal Specification:
c appends it to the buffer, preserving UTF-8 validityWhy Useful: Documents that Rust's String UTF-8 guarantees are preserved through draft operations.
Blocking: ❌ No (Rust's type system already enforces UTF-8 validity)
Coq File: formal-verification/coq/UTF8.v
Estimated Effort: 1 week
Statement: Finalizing the same draft multiple times produces the same result.
Formal Specification (Sketch):
Theorem draft_finalization_idempotence :
∀ (ctx : ContextId) (engine : CompletionEngine) (draft : String),
let engine1 := finalize(engine, ctx, draft) in
let engine2 := finalize(engine1, ctx, draft) in
dictionary_state engine1 = dictionary_state engine2.
Why Useful: Strengthens defensive programming guarantees, simplifies reasoning about finalization.
Blocking: ❌ No (finalization is not expected to be called multiple times in normal usage)
Coq File: formal-verification/coq/Finalization.v
Estimated Effort: 1 week
Statement: Creating a checkpoint, undoing, and restoring is idempotent.
Formal Specification (Sketch):
Theorem checkpoint_rollback_correctness :
∀ (ctx : ContextId) (engine : CompletionEngine),
let cp := checkpoint(engine, ctx) in
let engine1 := insert_str(engine, ctx, "test") in
let engine2 := restore(engine1, ctx, cp) in
draft_state(engine2, ctx) = draft_state(engine, ctx).
Why Useful: Enables safe implementation of undo/redo features in editors.
Blocking: ❌ No (checkpoint/undo is not currently used in LSP, reserved for future features)
Coq File: formal-verification/coq/Checkpoints.v
Estimated Effort: 1 week
Statement: All completions returned by fuzzy query are within the specified Levenshtein distance.
Formal Specification (Sketch):
Theorem fuzzy_query_soundness :
∀ (query : string) (max_distance : nat) (engine : CompletionEngine),
∀ completion ∈ complete(engine, ctx, query, max_distance),
levenshtein_distance(query, completion.term) ≤ max_distance.
Why Useful: Strengthens trust in fuzzy completion accuracy.
Blocking: ❌ No (fuzzy matching correctness is delegated to Levenshtein automaton layer)
Coq File: formal-verification/coq/FuzzyQuery.v
Dependencies: Levenshtein automaton correctness proof (Layer 2)
Estimated Effort: 1-2 weeks (requires formalizing automaton semantics)
Statement: Switching contexts does not leak symbols between unrelated contexts.
Formal Specification (Sketch):
Theorem context_switching_isolation :
∀ (ctx_a ctx_b : ContextId) (engine : CompletionEngine),
¬ancestor ctx_a ctx_b →
¬ancestor ctx_b ctx_a →
∀ t : string,
(finalized_in t ctx_a ∧ ¬finalized_in t ctx_b) →
¬visible_in t ctx_b.
Why Useful: Makes explicit what Theorem 6 implies about sibling context isolation.
Blocking: ❌ No (follows from Theorem 6 as a corollary)
Coq File: formal-verification/coq/ContextSwitching.v
Dependencies: Theorem 6
Estimated Effort: <1 week (simple corollary)
| Theorem | Priority | Blocks LSP | Effort | Dependencies |
|---|---|---|---|---|
| Theorem 1 (Context Tree Visibility) | P0 | ✅ Yes | 2-4 weeks | ContextTree, Dictionary models |
| Theorem 6 (Hierarchical Visibility) | P0 | ✅ Yes | 1-2 weeks | Theorem 1 |
| Theorem 2 (UTF-8 Correctness) | P2 | ❌ No | 1 week | None |
| Theorem 3 (Draft Finalization) | P2 | ❌ No | 1 week | Dictionary semantics |
| Theorem 4 (Checkpoint Rollback) | P3 | ❌ No | 1 week | DraftBuffer semantics |
| Theorem 5 (Fuzzy Query Soundness) | P3 | ❌ No | 1-2 weeks | Layer 2 automaton proofs |
| Theorem 7 (Context Switching) | P3 | ❌ No | <1 week | Theorem 6 |
Total Estimated Effort: 7-12 weeks for all theorems, 3-6 weeks for P0 only
liblevenshtein-rust/
└── formal-verification/
└── coq/
├── _CoqProject # Coq project configuration
├── Makefile # Build automation
├── README.md # Proof documentation
│
├── Foundations/ # Core definitions
│ ├── ContextTree.v # Context tree data structure
│ ├── Dictionary.v # Dictionary interface
│ ├── DraftBuffer.v # Character buffer model
│ └── CompletionEngine.v # Engine state model
│
├── Relations/ # Semantic relations
│ ├── Ancestor.v # Ancestor relation + lemmas
│ ├── Visibility.v # Visibility relation + lemmas
│ └── Finalization.v # Finalization semantics
│
├── Theorems/ # Main proofs
│ ├── Theorem1_Visibility.v # Context tree visibility (P0)
│ ├── Theorem6_Hierarchy.v # Hierarchical soundness (P0)
│ ├── Theorem2_UTF8.v # UTF-8 correctness
│ ├── Theorem3_Idempotence.v # Draft finalization
│ ├── Theorem4_Checkpoints.v # Checkpoint rollback
│ ├── Theorem5_Fuzzy.v # Fuzzy query soundness
│ └── Theorem7_Isolation.v # Context switching
│
└── Extraction/ # Code extraction
├── Extract.v # Extraction configuration
└── extracted/ # Generated Rust code
└── verified_engine.rs
Foundations (ContextTree.v, Dictionary.v, DraftBuffer.v)
↓
Relations (Ancestor.v, Visibility.v, Finalization.v)
↓
Theorem 1 (Visibility) ← P0 BLOCKING
↓
Theorem 6 (Hierarchy) ← P0 BLOCKING
↓
Theorem 7 (Isolation) ← Corollary
↓
Theorem 2, 3, 4, 5 ← Independent (P2-P3)
↓
Extraction (Optional: verified_engine.rs)
Goal: Formalize core data structures and relations
Tasks:
Model ContextTree (Foundations/ContextTree.v):
Inductive ContextTree : Type :=
| EmptyTree : ContextTree
| Node : ContextId → Context → ContextTree → ContextTree.
Definition lookup_context (tree : ContextTree) (id : ContextId) : option Context := (* ... *).
Model Dictionary (Foundations/Dictionary.v):
Parameter Dictionary : Type.
Parameter lookup : Dictionary → string → option (Vec ContextId).
Parameter insert : Dictionary → string → Vec ContextId → Dictionary.
Axiom lookup_insert_eq : ∀ d k v,
lookup (insert d k v) k = Some v.
Axiom lookup_insert_neq : ∀ d k1 k2 v,
k1 ≠ k2 → lookup (insert d k1 v) k2 = lookup d k2.
Define ancestor relation (Relations/Ancestor.v):
Lemma ancestor_transitive : ∀ A B C,
ancestor A B → ancestor B C → ancestor A C.
Lemma ancestor_irreflexive : ∀ C,
¬ancestor C C.
Lemma ancestor_antisymmetric : ∀ A B,
ancestor A B → ancestor B A → False.
Deliverable: Compiled .vo files, basic sanity checks
Goal: Prove context tree visibility correctness
Proof Outline:
Theorem context_tree_visibility :
∀ (C : Context) (t : string) (dict : Dictionary),
visible_in t C dict ↔
(finalized_in t C dict ∨
∃ A : Context, ancestor A C ∧ finalized_in t A dict).
Proof.
intros C t dict.
unfold visible_in.
split.
- (* → direction: trivial by definition *)
intros H. assumption.
- (* ← direction: trivial by definition *)
intros H. assumption.
Qed.
Note: The theorem statement is definitional, so proof is trivial. The real work is in proving lemmas about visibility queries:
Lemma query_completeness :
∀ (C : Context) (t : string) (dict : Dictionary),
visible_in t C dict →
∃ completion : Completion,
completion ∈ complete(C, t, 0) ∧
completion.term = t.
Lemma query_soundness :
∀ (C : Context) (completion : Completion),
completion ∈ complete(C, query, max_dist) →
visible_in completion.term C dict.
Deliverable: Theorems/Theorem1_Visibility.v compiled
Goal: Prove hierarchical visibility soundness
Proof Outline:
Theorem hierarchical_visibility_soundness :
∀ (C1 C2 : Context) (t : string) (dict : Dictionary),
parent C1 C2 →
(visible_in t C1 dict → visible_in t C2 dict) ∧
(finalized_in t C2 dict →
¬visible_in t C1 dict ∨
finalized_in t C1 dict ∨
∃ A : Context, ancestor A C1 ∧ finalized_in t A dict).
Proof.
intros C1 C2 t dict H_parent.
destruct H_parent as [id H_eq].
subst C2.
split.
- (* Part 1: Inheritance (C1 visible → C2 visible) *)
intros H_vis_C1.
unfold visible_in in *.
destruct H_vis_C1 as [H_fin_C1 | [A [H_anc_A_C1 H_fin_A]]].
+ (* t finalized in C1 *)
right. exists C1. split.
* apply ancestor_direct.
* assumption.
+ (* t finalized in ancestor of C1 *)
right. exists A. split.
* apply ancestor_trans with C1.
{ assumption. }
{ apply ancestor_direct. }
* assumption.
- (* Part 2: Isolation (C2 finalized → not visible in C1 OR finalized in C1/ancestor) *)
intros H_fin_C2.
unfold visible_in.
(* Key insight: finalization in child doesn't propagate upward *)
(* Either t is not visible in C1, OR it's separately finalized in C1/ancestor *)
tauto.
Qed.
Key Lemmas:
Lemma child_inherits_visibility :
∀ C1 C2 t dict,
parent C1 C2 →
visible_in t C1 dict →
visible_in t C2 dict.
Lemma parent_isolates_child :
∀ C1 C2 t dict,
parent C1 C2 →
finalized_in t C2 dict →
¬finalized_in t C1 dict →
¬(∃ A, ancestor A C1 ∧ finalized_in t A dict) →
¬visible_in t C1 dict.
Deliverable: Theorems/Theorem6_Hierarchy.v compiled
Goal: Prove Theorems 2-5, 7 (non-blocking)
Parallel Workstreams:
Vec<char> invariantsDeliverable: All 7 theorems proven
Goal: Generate verified Rust implementation
Strategy:
Extraction mechanism to generate OCamlDeliverable: Extraction/extracted/verified_engine.rs
Note: Extraction is optional - proofs alone provide sufficient guarantees for library users.
The rholang-language-server LSP uses liblevenshtein's DynamicContextualCompletionEngine for code completion. The system is well-tested but not formally proven.
Testing Status:
Verification Gap:
Immediate Benefits:
LSP-Specific Verification (Phase 3 in rholang-language-server roadmap):
build_scope_map() creates valid context treefind_node_at_position() returns innermost nodeExample LSP Verification Statement:
(* In rholang-language-server/formal-verification/coq/ScopeMap.v *)
Require Import liblevenshtein.Theorems.Theorem1_Visibility.
Require Import liblevenshtein.Theorems.Theorem6_Hierarchy.
Theorem scope_map_correctness :
∀ (ir : RholangNode) (scope_map : ScopeMap),
build_scope_map(ir) = scope_map →
∀ (pos : Position) (scope_id : ScopeId),
find_scope_at_position(scope_map, pos) = Some scope_id →
∀ (symbol : String),
visible_in_scope(symbol, scope_id, scope_map) ↔
(∃ ctx : ContextId,
scope_to_context(scope_id) = ctx ∧
visible_in symbol ctx (scope_map_to_dict scope_map)).
Proof.
(* Proof uses Theorem 1 to link scope visibility to context visibility *)
(* Proof uses Theorem 6 to ensure child scopes inherit parent visibility *)
Admitted.
If you are using liblevenshtein's contextual completion engine and require formal verification, follow this checklist:
liblevenshtein.Theorems.Theorem1_Visibility in your Coq proofsliblevenshtein.Theorems.Theorem6_Hierarchy in your Coq proofsA: Property tests provide empirical confidence but not mathematical certainty. They can miss edge cases, especially in concurrent systems. Formal verification guarantees correctness for all possible inputs, not just tested cases.
A: Rust verification tools (RustBelt, Prusti, Creusot) are experimental. Coq is mature and widely used. We can:
A: Start with P0 theorems (3-6 weeks effort). Skip P2-P3 theorems unless needed for your use case. LSP verification only requires Theorems 1 and 6.
A: Coq uses the Calculus of Inductive Constructions (CIC), a foundational type theory with a small trusted kernel. If Coq accepts the proof, it's correct (modulo bugs in Coq itself, which are extremely rare). This is the same foundation used to verify CompCert (a formally verified C compiler) and other safety-critical systems.
A: Concurrency verification is complex. Coq can model concurrent behavior using Iris (separation logic framework), but this is advanced. For now, we focus on single-threaded semantics. Rust's type system + locking ensures thread safety at the implementation level.
Leroy, Xavier (2009): "Formal verification of a realistic compiler". Communications of the ACM, 52(7):107-115.
Klein, Gerwin et al. (2009): "seL4: Formal verification of an OS kernel". SOSP 2009.
Jung, Ralf et al. (2018): "RustBelt: Securing the Foundations of the Rust Programming Language". POPL 2018.
Appel, Andrew W. (2014): "Program Logics for Certified Compilers". Cambridge University Press.
rholang-language-server/docs/formal-verification/liblevenshtein_proof_dependencies.mdrholang-language-server/docs/formal-verification/scope-detection.mdQuestions: Open an issue on GitHub with [formal-verification] tag
Contributing Proofs:
formal-verification/coq/ directory.v filesTimeline: No fixed schedule - proofs are welcome whenever contributors are available. Priority is on Theorems 1 and 6 to unblock LSP verification.
Last Updated: 2025-01-21 Status: Documentation complete, awaiting Coq implementation Blocking: rholang-language-server formal verification (Theorems 1 and 6)
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 |