Liking cljdoc? Tell your friends :D

Formal Verification of Levenshtein Automata

Project Status: 🚧 Phase 1 & 9 Complete - Foundation + Contextual Completion Proof Assistant: Rocq (formerly Coq) Started: 2025-11-17 Team: Formal Verification Team

Overview
Motivation
Project Structure
Current Status
Proven Theorems
Getting Started
Development Workflow
Roadmap
References

Overview

This directory contains formal proofs of correctness for the Levenshtein automata implementation in liblevenshtein-rust. We use the Rocq proof assistant to mechanically verify that the algorithms correctly implement the theory described in docs/research/weighted-levenshtein-automata/README.md.

Goals

Prove correctness of core automaton operations from first principles
Establish rigorous foundation for current implementation
Guide implementation fixes through formal specification
Enable safe extensions to generalized automata (phonetic operations, etc.)
Build confidence in critical algorithms used by downstream applications

Approach

We follow a specification-first methodology:

Theory → Formalization → Proof → Specification → Implementation Fix

Start with theoretical foundations (Wagner-Fischer DP, edit graphs)
Formalize in Rocq with detailed documentation
Prove key properties mechanically
Extract formal specification
Compare with Rust implementation and fix discrepancies

Motivation

The Problem

Three tests related to generalized automata are currently failing:

test_phonetic_split_multiple
test_phonetic_split_with_standard_ops
test_new_i_splitting_invalid

Traditional debugging has been expensive and inconclusive. These failures likely stem from subtle interactions between:

Fractional-weight phonetic operations
Multi-step operation state machines
Position invariant checking
Subsumption-based state minimization

The Solution

Formal verification provides:

Mathematical certainty: Prove algorithms correct, not just test them
Systematic coverage: Proofs cover all cases, not just tested inputs
Root cause identification: Proof failures reveal exact assumptions violated
Documentation as code: Proofs serve as executable specifications
Regression prevention: Once proven, correctness is permanent

Why Rocq?

Industry-proven: Used to verify CompCert C compiler, seL4 microkernel
Expressive: Dependent types allow precise specifications
Practical: Can extract verified code to OCaml/Haskell/Scheme
Well-supported: Large standard library, active community
Prior art: Similar approach used in /var/tmp/debug/f1r3node/

Project Structure

rocq/liblevenshtein/           # Rocq proof files
├── Core.v                     # Foundational definitions ✓
├── Invariants.v               # Position invariant proofs ✓
├── Operations.v               # Standard operations ✓
├── Transitions.v              # State transitions ✓
├── PhoneticOperations.v       # Phonetic split operations ✓
├── SubwordOperations.v        # Subword operation model ✓
└── _CoqProject                # Build configuration

docs/formal-verification/      # Human-readable documentation
├── README.md                  # This file
├── STATUS.md                  # Current proof status
├── VALIDATION_MATRIX.md       # Rust/proof validation matrix
├── FINDINGS.md                # Formal audit findings
├── 03_standard_operations.md  # Standard operation proof notes
├── 04_phonetic_operations.md  # Phonetic operation proof notes
└── proofs/                    # Detailed proof documentation
    ├── 01_subsumption_properties.md  # Phase 1 ✓
    ├── 02_position_invariants.md     # Phase 2 ✓
    └── 06_contextual_completion/      # Phase 9 ✓
        ├── README.md                  # Category overview
        ├── 01_context_visibility.md   # Context tree visibility
        ├── 02_draft_consistency.md    # UTF-8 draft buffer operations
        ├── 03_checkpoint_stack.md     # Undo/redo correctness
        ├── 04_query_fusion.md         # Completion result correctness
        ├── 05_distance_correctness.md # Levenshtein distance algorithm
        ├── 06_hierarchical_visibility.md # Scope isolation
        └── 07_finalization.md         # Atomicity of draft→dictionary

Current Status

Phase 1: Foundation & Quick Wins ✅ COMPLETE

Completed: 2025-11-17

Deliverables

✅ Project structure created (rocq/liblevenshtein/)
✅ Core.v - Foundational definitions (585 lines)
- Position types (6 variants)
- Invariant predicates (I, M, transposing, splitting)
- Subsumption relation
- Helper lemmas
✅ Three foundational theorems proven:
- Irreflexivity: $~ (p \sqsubseteq p)$
- Transitivity: $p_{1} \sqsubseteq p_{2} \to p_{2} \sqsubseteq p_{3} \to p_{1} \sqsubseteq p_{3}$
- Variant restriction: $\text{variant}(p_{1}) \ne \text{variant}(p_{2}) \to ~ (p_{1} \sqsubseteq p_{2})$
✅ Comprehensive documentation (01_subsumption_properties.md, 600+ lines)

Verification

$ cd rocq/liblevenshtein
$ coqc -R . LevensteinAutomata Core.v
# Success! Generated Core.vo (53,419 bytes)

All proofs compile and verify successfully under Rocq 9.x.

Proven Theorems

Subsumption Properties (Core.v)

Theorem	Statement	Significance	Status
Irreflexivity	$`\forall p, \lnot (p \sqsubseteq p)`$	No position subsumes itself	✅ Proven
Transitivity	$`p_{1}\sqsubseteq p_{2} \land p_{2}\sqsubseteq p_{3} \to p_{1}\sqsubseteq p_{3}`$	Subsumption chains compose	✅ Proven
Variant Restriction	$`\text{variant}(p_{1})\ne \text{variant}(p_{2}) \to \lnot (p_{1}\sqsubseteq p_{2})`$	Different types don't subsume	✅ Proven
Anti-Symmetry	$`p_{1}\sqsubseteq p_{2} \land p_{2}\sqsubseteq p_{1} \to \text{False}`$	No cycles in subsumption	✅ Proven (derived)

Key Insights

Subsumption is a strict partial order - This justifies using it for state minimization
Anti-chain preservation is well-founded - State minimization algorithms terminate
Variant boundaries are enforced - Position types cannot be confused

Getting Started

Prerequisites

Install Rocq (Coq):

# Arch Linux
sudo pacman -S coq

# Ubuntu/Debian
sudo apt-get install coq

# Via opam (OCaml package manager)
opam install coq

# Verify installation
coqc --version  # Should show 8.17+ or 9.x (Rocq)

Recommended tools:

ProofGeneral (Emacs mode) or VSCoq (VS Code extension)
CoqIDE (graphical interface)

Building the Proofs

cd /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/rocq/liblevenshtein

# Compile all proofs
coqc -R . LevensteinAutomata Core.v

# Or use make (when Makefile generated)
coq_makefile -f _CoqProject -o Makefile
make

Reading the Proofs

Start with the documentation:

Read docs/formal-verification/README.md (this file)
Study docs/formal-verification/proofs/01_subsumption_properties.md
Open rocq/liblevenshtein/Core.v in ProofGeneral/VSCoq
Step through proofs interactively

Tip: Proofs have extensive inline comments explaining each step.

Interactive Development

Using ProofGeneral (Emacs):

emacs rocq/liblevenshtein/Core.v
# Use C-c C-n to step forward through proof
# Use C-c C-u to step backward
# Use C-c C-RET to process to cursor

Using VSCoq (VS Code):

code rocq/liblevenshtein/Core.v
# Use Alt+Down to step forward
# Use Alt+Up to step backward
# Hover over terms to see types

Development Workflow

Adding New Proofs

Document first: Create markdown file in docs/formal-verification/proofs/
- State theorem informally
- Explain proof intuition
- Sketch proof structure
Formalize: Add definitions and theorem statements to appropriate .v file
- Include detailed comments
- Cross-reference theory documents
Prove: Develop proof incrementally
- Use tactics like lia, auto, destruct, induction
- Add intermediate lemmas as needed
- Document non-obvious steps

Verify: Compile and check

coqc -R . LevensteinAutomata YourFile.v

Document: Update markdown with final proof
- Annotate Coq code
- Explain key insights
- Note implementation impact

Proof Style Guidelines

Comments:

Every theorem must have a comment block explaining:
- Informal statement
- Intuition (why it's true)
- Proof strategy
- Connection to theory document
- Implementation correspondence

Structure:

Use sections to organize related definitions/theorems
Break complex proofs into lemmas
Name lemmas descriptively (e.g., subsumes_requires_error_gap)

Tactics:

Prefer lia for arithmetic (auto-solves linear inequalities)
Use destruct for case analysis
Use induction for recursive structures
Document when manual reasoning is needed

Example:

(**
  THEOREM: Subsumption is Irreflexive

  INTUITION: No position can subsume itself because subsumption
             requires errors(p₂) > errors(p₁), but for p⊑p we'd
             need errors(p) > errors(p), which is impossible.

  PROOF STRATEGY: Direct from definition + lia solver

  REFERENCE: Part II, Section 3.1 of weighted-levenshtein-automata doc
*)
Theorem subsumes_irreflexive : forall p, ~ (p ⊑ p).
Proof.
  intros p [_ [Hcontr _]].  (* Extract errors(p) > errors(p) *)
  lia.                       (* Contradiction *)
Qed.

Testing Against Implementation

After proving properties, add property-based tests to Rust:

#[cfg(test)]
mod formal_verification_tests {
    use super::*;
    use proptest::prelude::*;

    // Property: Irreflexivity (from Core.v)
    proptest! {
        #[test]
        fn subsumption_irreflexive(
            offset in any::<i32>(),
            errors in 0u8..10,
            variant in any::<PositionVariant>()
        ) {
            let pos = create_position(variant, offset, errors);
            assert!(!subsumes(&pos, &pos, errors));
        }
    }

    // Property: Transitivity (from Core.v)
    proptest! {
        #[test]
        fn subsumption_transitive(/* ... */) {
            // If p1 ⊑ p2 and p2 ⊑ p3, then p1 ⊑ p3
            // ...
        }
    }
}

Roadmap

Phase 2: Position Invariants (Est. 2 days)

Goal: Prove position constructors maintain invariants

Deliverables:

Invariants.v: Formalize invariant checking
Prove new_i correctness
Prove new_m correctness
Prove accessor functions safe
Documentation: 02_position_invariants.md

Key theorems:

new_i_valid: Valid inputs → valid I-type position
new_m_valid: Valid inputs → valid M-type position
invariant_decidable: Invariant checking is computable

Phase 3: Standard Operations (Est. 3 days)

Goal: Prove standard edit operations correct

Deliverables:

Operations.v: Operation type definitions
Transitions.v: Successor computation
Prove match, substitute, insert, delete correct
Prove invariant preservation
Documentation: 03_standard_operations.md

Key theorems:

successor_match_valid: Match produces valid successors
successor_substitute_valid: Substitute preserves invariants
operation_cost_correct: Cost accounting is accurate

Phase 4: Multi-Step Operations (Est. 2 days)

Goal: Extend to transposition and merge

Deliverables:

Extend Transitions.v with transposition
Prove entry/completion protocol
Prove merge operation
Documentation: 04_multi_step_operations.md

Defer: Split operations (phonetic) to Phase 8+

Key theorems:

transposition_entry_sound: Entry → completion exists
transposition_complete_valid: Completion produces valid position
merge_correct: Direct 2→1 merge is sound

Phase 5: Anti-Chain Preservation (Est. 2 days)

Goal: Prove state minimization algorithm correct

Deliverables:

State.v: State representation and anti-chain
Formalize add_position algorithm
Prove anti-chain preservation
Documentation: 05_state_management.md

Key theorems:

add_position_preserves_anti_chain: Main correctness theorem
anti_chain_decidable: Anti-chain checking is computable
state_size_bound: $\mathcal{O}(n^{2})$ state size

Phase 6: Specification Extraction (Est. 1 day)

Goal: Extract formal spec from proofs

Deliverables:

SPECIFICATION.md: Formal specification document
Preconditions/postconditions for all operations
Invariant contracts
Complexity bounds

Phase 7: Implementation Fixes (Est. 2 days)

Goal: Fix Rust code to match proven spec

Deliverables:

DISCREPANCIES.md: Documented differences
FIX_REPORT.md: Changes made with justification
Updated Rust implementation
Regression tests
IMPLEMENTATION_GUIDE.md: Maintenance guide

Expected outcome: Standard operation tests pass

Phase 8+: Future Work (Deferred)

Phonetic operations (fractional weights):

Formalize rational arithmetic (Q type)
Prove split operation correctness
Handle weight truncation
Fix failing phonetic tests

Full automaton acceptance:

Prove accepts(word, query, n) ⟺ $\text{distance}(\text{word}, \text{query}) \le n$
Completeness and soundness theorems

Extraction to verified implementation:

Extract Coq to OCaml/Haskell
Generate verified Rust via transpilation
CompCert-style certified compilation

Phase 9: Contextual Completion Correctness ✅ COMPLETE

Completed: 2025-01-21

Goal: Establish formal foundation for contextual completion engine used by rholang-language-server

Deliverables:

✅ Category structure created (proofs/06_contextual_completion/)
✅ Category README (280 lines) - Overview, reading paths, dependencies
✅ Theorem 1: Context Tree Visibility (550 lines)
- Proves visible_contexts() returns all ancestors in order
- Soundness, completeness, correct ordering
✅ Theorem 2: Draft Buffer Consistency (650 lines)
- Proves UTF-8 validity preserved during insert/delete
- Leverages Rust's char type guarantees
✅ Theorem 3: Checkpoint Stack Correctness (600 lines)
- Proves undo/redo exactness and idempotence
- Length-only checkpoint design (8 bytes vs full buffer)
✅ Theorem 4: Query Fusion Completeness (concise)
- Proves complete() returns union of draft + finalized
- Soundness, completeness, deduplication, draft priority
✅ Theorem 5: Levenshtein Distance Correctness (full)
- Proves naive $\mathcal{O}(n\cdot m)$ implementation matches Wagner-Fischer
- Triangle inequality, symmetry, identity proofs
✅ Theorem 6: Hierarchical Visibility Soundness (full)
- Proves children see parents, parents don't see children
- No lateral visibility (siblings isolated)
✅ Theorem 7: Finalization Atomicity (full)
- Proves draft→dictionary is all-or-nothing
- No partial states observable by concurrent queries

Key Insights:

Hybrid approach: Documentation first (Phase 9.1), Coq formalization deferred (Phase 9.2)
Digestible chunks: 550-650 lines per theorem (3-6 pages)
Implementation traceability: Every theorem mapped to exact Rust source lines
Downstream impact: Enables formal verification of rholang-language-server scope detection

Verification Status:

Documentation: ✅ Complete (7 theorems + category README)
Coq formalization: ⏳ Planned (Phase 9.2)
Property-based tests: ⏳ Planned (Phase 9.3)

Files Created:

proofs/06_contextual_completion/README.md
proofs/06_contextual_completion/01_context_visibility.md
proofs/06_contextual_completion/02_draft_consistency.md
proofs/06_contextual_completion/03_checkpoint_stack.md
proofs/06_contextual_completion/04_query_fusion.md
proofs/06_contextual_completion/05_distance_correctness.md
proofs/06_contextual_completion/06_hierarchical_visibility.md
proofs/06_contextual_completion/07_finalization.md

References

Theory Documents

Primary reference:

docs/research/weighted-levenshtein-automata/README.md (765 lines)
- Part I: Derivation from Wagner-Fischer DP
- Part II: General operation framework
- Part III: Weighted extensions (discretization)

Supporting documents:

docs/generalized/phase2d_completion_report.md - Implementation status
docs/generalized/phase3b_requirements.md - Phonetic operations (400+ lines)
docs/algorithms/README.md - Algorithm layer documentation (504 lines)

Implementation

Core files:

src/transducer/generalized/position.rs (757 lines) - Position types
src/transducer/generalized/state.rs (1600+ lines) - State management
src/transducer/generalized/automaton.rs (1700+ lines) - Main automaton
src/transducer/generalized/subsumption.rs (334 lines) - Subsumption checks

Test files:

src/transducer/generalized/automaton.rs:1200-1700 - Unit tests
tests/integration_tests.rs - Integration tests
tests/proptest_*.rs - Property-based tests

External Resources

Rocq/Coq:

Rocq Documentation - Official docs
Software Foundations - Tutorial series
CPDT - Certified Programming with Dependent Types
Math Comp Book - Mathematical Components

Similar Projects:

/var/tmp/debug/f1r3node/docs/formal-verification/coq/ - Rholang proofs (13 files)
CompCert - Verified C compiler
seL4 - Verified microkernel

Papers:

Mitankin, "Levenshtein Automata" (thesis) - Position types, subsumption
Wagner & Fischer, "String-to-string correction problem" (1974) - DP algorithm
Schulz & Mihov, "Fast string correction with Levenshtein automata" (2002)

Contributing

Adding New Proofs

Discuss approach in team meeting
Create tracking issue
Follow development workflow above
Submit for review before merging

Code Review Checklist

[ ] Proof compiles without warnings
[ ] Comprehensive inline comments
[ ] Markdown documentation created/updated
[ ] Cross-references to theory docs
[ ] Cross-references to Rust implementation
[ ] Examples provided where helpful
[ ] Proof strategy explained
[ ] Key lemmas identified and documented

Style Consistency

Follow the style established in Core.v:

ASCII art diagrams where helpful
Inline comments for proof steps
Section headers with descriptions
Notation defined before use
Helper lemmas proven separately

Troubleshooting

Compilation Errors

Scope issues (Z vs nat):

(* Wrong: *)
errors p <= max_distance p  (* Interpreted as Z.le with Z_scope open *)

(* Right: *)
(errors p <= max_distance p)%nat  (* Explicitly use nat scope *)

Type mismatches:

(* Wrong: *)
assert (errors p2 > errors p1) by lia.  (* nat in scope that expects Z *)

(* Right: *)
assert (Hgap: (errors p2 > errors p1)%nat). { lia. }

Triangle inequality:

(* Wrong: *)
apply Z.abs_triangle.  (* Goal doesn't match lemma form *)

(* Right: *)
replace (x - y) with ((x - z) + (z - y)) by lia.
apply Z.abs_triangle.