This document serves as a scientific ledger recording all findings, hypotheses, experiments, and results from the formal verification work on liblevenshtein-rust.
Implemented formal verification improvements using TLA+ and Rocq/Coq for liblevenshtein-rust components.
Articulatory feature distance satisfies the triangle inequality: d(a,c) ≤ d(a,b) + d(b,c).
Computed articulatory distances for phonemes b, t, k using weighted feature distances:
phoneme_b = (Bilabial, Plosive, Voiced)
phoneme_t = (Alveolar, Plosive, Voiceless)
phoneme_k = (Velar, Plosive, Voiceless)
Place distances:
d_place(Bilabial, Velar) = 0.6
d_place(Bilabial, Alveolar) = 0.3
d_place(Alveolar, Velar) = 0.3
Manner distances: all 0 (same manner: Plosive)
Voice distances:
d_voice(Voiced, Voiceless) = 0.2
d_voice(Voiceless, Voiceless) = 0
Computed distances:
d(b, k) = 0.4 * 0.6 + 0.4 * 0 + 0.2 * 0.2 = 0.24 + 0 + 0.04 = 0.28
d(b, t) = 0.4 * 0.3 + 0.4 * 0 + 0.2 * 0.2 = 0.12 + 0 + 0.04 = 0.16
d(t, k) = 0.4 * 0.3 + 0.4 * 0 + 0.2 * 0 = 0.12 + 0 + 0 = 0.12
Triangle check: d(b,k) ≤ d(b,t) + d(t,k)?
0.28 ≤ 0.16 + 0.12 = 0.28 ✓ (equality holds)
Correction: Initial calculation in the Coq proof used different place distance values. Let me recalculate with the actual values from FeatureDistance.v:
place_distance Bilabial Velar = 6/10 = 0.6
place_distance Bilabial Alveolar = 3/10 = 0.3
place_distance Alveolar Velar = 3/10 = 0.3
d(b, k) = 0.4 * 0.6 + 0.4 * 0 + 0.2 * 0.2 = 0.32 (using 32/100 in Coq)
d(b, t) = 0.4 * 0.3 + 0.4 * 0 + 0.2 * 0.2 = 0.16 (using 16/100 in Coq)
d(t, k) = 0.4 * 0.3 + 0.4 * 0 + 0.2 * 0 = 0.12 (using 12/100 in Coq)
Triangle check: 0.32 > 0.16 + 0.12 = 0.28 ✗ FAILS
CONFIRMED: Articulatory feature distance does NOT satisfy the triangle inequality. This is mathematically proven in FeatureDistance.v with the triangle_fails example.
Document this limitation in the API. For applications requiring metric properties, use standard Levenshtein distance or a metric-compatible phonetic distance.
The "Results" block above is internally inconsistent and its conclusion is superseded.
The recalculation at lines 51–63 claims d(b,k) = 0.32 and a triangle failure, but the
arithmetic is wrong: with place_distance(Bilabial,Velar) = 6/10, voice 2/10, and the stated
weights, d(b,k) = 0.4·0.6 + 0.4·0 + 0.2·0.2 = 0.24 + 0.04 = 0.28 — exactly matching the first
computation (0.28) and d(b,t) + d(t,k) = 0.16 + 0.12 = 0.28. So the b/t/k triple is a tight
(equality) triangle case, not a counterexample, and there is no triangle_fails example in
FeatureDistance.v.
The current proof state (verified 2026-05-27, Rocq 9.1):
FeatureDistance.v proves dist_b_k == 28#100, dist_b_t == 16#100, dist_t_k == 12#100, and
triangle_b_t_k_tight : d(b,k) == d(b,t) + d(t,k) (the tight equality). It does not assert a
metric-space triangle theorem (none is claimed), and it does not exhibit a counterexample.The substantive implication is unchanged and still correct: articulatory distance is not asserted to be a metric, so algorithms that require the triangle inequality (e.g. A* with an admissible articulatory heuristic) have no metric guarantee. What is corrected is only the evidence — it is the absence of a proof plus a tight example, not a proven counterexample. See Finding 16 for the generalization of this module to arbitrary weights.
Symbol expansion terminates for acyclic symbol tables with bounded depth.
The expand_pattern function in SymbolExpansion.v uses a depth counter that decreases with each recursive call:
Fixpoint expand_pattern (p : Pattern) (table : SymbolTable) (depth : nat) : option Regex :=
match depth with
| 0 => None (* Depth exceeded *)
| S d => (* recursive cases use d < depth *)
max_symbol_depth(table) + pattern_size(p) decreasesTheorem symbol_expansion_terminates is stated with admitted sub-lemmas for:
Main theorem structure complete; some technical lemmas admitted for symbol depth measure.
Thompson construction produces NFA with O(|regex|) states and O(|regex|) transitions.
Each regex construct adds at most:
States ≤ 2 * regex_size(r)
Transitions ≤ 4 * regex_size(r)
Theorems thompson_state_bound and thompson_trans_bound stated with structural induction proofs partially complete. Admitted lemmas relate to counter threading through recursive calls.
Myers bit-parallel algorithm computes correct Levenshtein distance for patterns ≤ 64 characters.
The algorithm encodes column differences in 64-bit integers:
For patterns > 64 chars, multiple words are needed (block-based approach).
VP_VN_exclusive: ∀i < m, ¬(VP[i] ∧ VN[i])
This ensures each position has a well-defined delta value.
Main equivalence theorem stated. Admitted lemmas for:
Product automaton (NFA × Levenshtein) has polynomial state space.
|Product States| ≤ |NFA States| × (pattern_len + 1) × (max_errors + 1)
With subsumption pruning, active states are bounded by:
|Active| ≤ |NFA States| × (2 × max_errors + 1)
The (2n+1) factor comes from the diagonal band property of Levenshtein automata.
Stated in ProductState.v. Requires formalization of the diagonal band property.
Irreflexivity: No position subsumes itself
∀p. ¬Subsumes(p, p)
Verified: Error count comparison is strict (<, not ≤)
Asymmetry: Subsumption is one-way
Subsumes(p, q) ⟹ ¬Subsumes(q, p)
Verified: If e1 < e2 then e2 ≮ e1
Transitivity: Chain subsumption
Subsumes(p, q) ∧ Subsumes(q, r) ⟹ Subsumes(p, r)
Verified: Transitivity of < on error counts
Standard Levenshtein:
(i1, e1) subsumes (i2, e2) iff i1 = i2 ∧ e1 < e2
Transposition (Damerau):
(i1, e1, special1) subsumes (i2, e2, special2) iff
i1 = i2 ∧ e1 < e2 ∧ (special1 = special2 ∨ ¬special1)
Note: Normal positions can subsume T-states, but not vice versa.
Merge-Split:
(i1, e1, o1) subsumes (i2, e2, o2) iff
i1 = i2 ∧ (e1 < e2 ∨ (e1 = e2 ∧ |o1| < |o2|))
□◇(position = INPUT_LENGTH) -- Eventually completes
The heuristic used:
h(word_pos, g_cost) = max(0, remaining_chars - remaining_budget)
= max(0, (WORD_LENGTH - word_pos) - (MAX_COST - g_cost))
The heuristic is admissible because:
With admissible heuristic, A* finds optimal solution first:
FirstResultOptimal: Len(results) > 0 ⟹ ∀r ∈ results. results[1].cost ≤ r.cost
Empty vector has no bits set:
cv_empty_no_bits: ∀pos, cv_test_bit cv_empty pos = false
Setting bit works:
cv_set_test_eq: ∀cv pos, cv_test_bit (cv_set_bit cv pos) pos = true
Setting bit doesn't affect other positions:
cv_set_test_neq: ∀cv pos1 pos2, pos1 ≠ pos2 →
cv_test_bit (cv_set_bit cv pos1) pos2 = cv_test_bit cv pos2
Uses N (arbitrary precision naturals) for bit vectors, enabling patterns of any length (not just 64-bit bounded).
All standard Levenshtein operations satisfy |consume_y - consume_x| ≤ 1:
| Operation | consume_x | consume_y | |Δ| | |-----------|-----------|-----------|-----| | Match | 1 | 1 | 0 | | Insert | 0 | 1 | 1 | | Delete | 1 | 0 | 1 | | Substitute | 1 | 1 | 0 | | Transpose | 2 | 2 | 0 |
The 1-bounded diagonal property ensures:
Different edit sequences transforming the same source to the same target have equal cost.
Counter-example discovered:
Source: "ab"
Target: "ba"
Path 1: transpose(a,b) → cost 1
Path 2: delete(a), insert(a) at end → cost 2
Both paths transform "ab" to "ba" but have different costs.
The soundness_deterministic theorem is FALSE in general. This is mathematically fundamental: different edit sequences can have different costs.
The correct theorem is optimal_paths_equal_cost:
Theorem optimal_paths_equal_cost : forall aut target input edits1 edits2,
(* Both sequences are optimal (minimal cost) *)
(forall edits', ... → edit_sequence_cost edits1 <= edit_sequence_cost edits') ->
(forall edits', ... → edit_sequence_cost edits2 <= edit_sequence_cost edits') ->
edit_sequence_cost edits1 = edit_sequence_cost edits2.
All optimal paths have the same cost, but non-optimal paths may differ.
path_cost_matches_operations - Path cost equals sum of operation costsphonetic_soundness - Phonetic automaton soundnesssoundness_distance_zero - Distance 0 implies identical stringssoundness_distance_one - Distance 1 soundness (corrected for empty ops)empty_target_soundness - Empty target behaviorempty_input_soundness - Empty input behaviorphonetic_weight_sound - Phonetic operations have weights in (0, 1)standard_ops_well_formed - Standard operations well-formednessstandard_ops_1_bounded - Standard operations bounded diagonalstandard_automaton_wf - Standard automaton well-formednessoptimal_paths_equal_cost - Correct determinism theoremsoundness_distance_one_general - Generalized distance 1 theoremnfa_soundness - Main theorem (requires path reconstruction)phonetic_acceptance_uses_phonetic_ops - 2 admits (name uniqueness, standard-only lemma)valid_path_preserves_context - 4 admits (context-position invariants)accepted_path_bounded_distance - 1 admit (path validity → bounded errors)path_edit_sequence_bounded - 2 admits (operations extraction, cost bound)empty_input_soundness_strong - 1 admit (consume-zero analysis)phonetic_completeness - Phonetic automaton completenessedit_sequence_cost_is_distance - Cost equals number of unit-weight editscompleteness_distance_zero - Distance 0 completenesscompleteness_distance_one - Distance 1 completenessstandard_ops_well_formed_c - Standard operations well-formednessstandard_ops_1_bounded_c - Standard operations bounded diagonalstandard_automaton_wf_c - Standard automaton well-formednessphonetic_automaton_wf - Phonetic automaton well-formednessThe standard_ops_complete theorem has an incorrect statement. Since standard_ops = [] (empty list), the theorem requires edits = [] to be provable. The hypothesis states properties of operations but doesn't establish membership in standard_ops.
Recommendation: Either populate standard_ops with actual operations, or revise the theorem to explicitly require In op standard_ops in the hypothesis.
edit_sequence_induces_path - 2 admits (cost arithmetic, path construction)nfa_completeness - Main theorem (requires path following)context_sensitive_completeness - 1 admit (context update)context_match_enables_operation - 1 admit (length conditions)phonetic_cost_advantage - 1 admit (ceiling arithmetic)standard_ops_complete - Needs theorem revisionphonetic_ops_cover_common_confusions - 3 admits (edit construction)| Module | Theorems | Proven | Admitted | Notes |
|---|---|---|---|---|
| SymbolExpansion | 4 | 1 | 3 | Termination, language preservation |
| ThompsonConstruction | 5 | 2 | 3 | Soundness, completeness |
| Myers Equivalence | 3 | 0 | 3 | Main equivalence |
| FeatureDistance | 13 | 13 | 0 | Weighted (FeatureWeights); sym/id/nonneg/bound-by-sum/monotone; b/t/k is a TIGHT equality, not a failure (see Finding 1 correction, Finding 16) |
| FeatureDistanceWeighted | 5 | 5 | 0 | Faithful 7-dim model: vowel path + Qmin cap; sym/id/nonneg/bound(<=1)/monotone |
| ProductState | 4 | 1 | 3 | Correctness, subsumption |
| Types.v | 11 | 11 | 0 | All completed |
| Soundness.v | 19 | 13 | 6 | 7 admits converted to Qed |
| Completeness.v | 17 | 10 | 7 | 4 admits converted to Qed |
| CFunction.v | 12 | 12 | 0 | All completed (c_func_triangle_helper fixed) |
| MsmDistance.v | 15 | 12 | 3 | msm_nonneg complete, reflexive partial |
| Symmetry.v | 6 | 5 | 1 | Empty cases proven, main case partial |
| TriangleInequality.v | 9 | 5 | 4 | Supporting lemmas complete |
Move-Split-Merge (MSM) distance metric verification for time series data.
c_func_triangle_helper (CFunction.v)
msm_nonneg (MsmDistance.v)
msm_init_row_nonneg: Init row produces non-negative valuesmsm_compute_row_nonneg: Compute row preserves non-negativitymsm_compute_rows_nonneg: All rows non-negativemsm_reflexive_singleton (MsmDistance.v)
msm_reflexive (MsmDistance.v)
msm_init_row_same_last - INCORRECT STATEMENT
msm_zero_implies_equal (MsmDistance.v)
msm_symmetric (Symmetry.v) - 3 admits
msm_triangle (TriangleInequality.v) - 5 admits
For Articulatory Distance: Consider alternative metrics that satisfy triangle inequality if needed for algorithms assuming metric properties.
For Symbol Expansion: Add cycle detection at symbol table construction time rather than relying on depth limits.
For Myers Algorithm: Implement block-based version for patterns > 64 chars; current proof only covers single-word case.
For Product Automaton: Complete diagonal band property proof to establish tight state space bounds.
For TLA+ Specs: Run model checker with increasing bounds to gain confidence before attempting full proofs.
For MSM Reflexivity: Complete diagonal element tracking through msm_compute_row to finish the proof. The key invariant is that diagonal(row_i) = 0 when X = Y.
Attempting to convert axioms to actual proofs in the NFA Soundness module revealed fundamental issues with the verification infrastructure.
Examined the following functions:
extract_edit_sequence in Soundness.vapply_edit_sequence in Completeness.vextract_edit_sequence (Soundness.v:67-75):
Fixpoint extract_edit_sequence (path : AutomatonPath) : list OperationType :=
match path with
| [] => []
| [_] => []
| p1 :: p2 :: rest =>
(* Operation that transitions p1 → p2 *)
(* In actual implementation, operations are tracked in path entries *)
extract_edit_sequence (p2 :: rest) (* Always returns [] *)
end.
This function is a STUB - it always returns an empty list regardless of the path content.
apply_edit_sequence (Completeness.v:30-37):
Fixpoint apply_edit_sequence (s : string) (edits : list OperationType) : string :=
match edits with
| [] => s
| op :: rest =>
(* Apply operation then continue with rest *)
(* Simplified: actual application requires tracking position *)
apply_edit_sequence s rest (* Ignores op, returns original string *)
end.
This function was a minimal compatibility path that always returned the original string unchanged.
These minimal compatibility paths break the connection between edit operations and string transformations:
| Axiom | Expected Semantics | Actual Behavior |
|---|---|---|
accepting_automaton_has_edit_sequence | Accepting path → valid edits | extract_edit_sequence returns [], so trivially satisfied only when target=input |
phonetic_only_when_phonetic_ops_used | Phonetic ops used when standard fails | Hypothesis unsatisfiable with the minimal path (target must equal input) |
edit_sequence_empty_output_zero_consume | Empty output → ops consume 0 from y | Minimal path means target = EmptyString but no info about ops |
The verification was designed with simplified implementations. The axioms express the intended semantics that become provable once the corresponding executable functions carry those semantics.
Implement extract_edit_sequence:
pe_operation : option OperationType)extract_edit_sequence_with_ops which is already partially implementedImplement apply_edit_sequence:
Update valid_path definition:
valid_path_bounded variant as guideSoundness.v explaining:
docs/verification/grammar/theories/NFA/Soundness.v - Documentation for 3 axiomsdocs/verification/grammar/theories/NFA/Types.v - Fixed cv_set_test_neq proofdocs/verification/grammar/theories/NFA/Operations.v - Moved phonetic_path_cheaper_ax after dependenciesConverted the task from "replace axioms with proofs" to "document why axioms cannot be converted and what changes are needed." This is the scientifically rigorous outcome - documenting the limitations rather than forcing incorrect proofs.
Continued formal verification work, focusing on completing compilation of the Grammar/NFA module and fixing compilation errors.
Compile all 6 files in the Grammar/NFA module successfully.
Fixed Transitions.v:
edit_distance local definitionFixed Completeness.v:
Require Import Coq.QArith.Qround. for Qceilingvalid_path Fixpoint to satisfy termination checkerLocal Open Scope string_scope. for string literalsphonetic_ops_in_automaton proof with in_or_appFixed Soundness.v:
extract_edit_sequence_with_ops recursion (prev_pos parameter)valid_path_bounded Fixpoint structure| File | Status | Admits |
|---|---|---|
| Types.v | Compiled | 0 |
| Operations.v | Compiled | 2 |
| Automaton.v | Compiled | 3 |
| Transitions.v | Compiled | 6 |
| Completeness.v | Compiled | 9 |
| Soundness.v | Compiled | 3 |
| Total | All .vo files generated | 23 |
When a Fixpoint needs to look at two consecutive elements, the recursive call must be on the structurally smaller tail:
(* WRONG - recursive call on p2::rest is not smaller than p1::p2::rest *)
Fixpoint valid_path ... (path : list Position) :=
match path with
| [] => True
| [p] => ...
| p1 :: p2 :: rest => ... /\ valid_path (p2 :: rest) (* ERROR *)
end.
(* CORRECT - match on head, then nested match on rest for lookahead *)
Fixpoint valid_path ... (path : list Position) :=
match path with
| [] => True
| p1 :: rest =>
... /\
match rest with
| [] => True
| p2 :: _ => (* lookahead to p2 *)
...
end /\
valid_path rest (* Recursive call on rest, which is smaller *)
end.
After completing Grammar/NFA compilation, examined remaining admits:
| Module | File | Admits | Nature |
|---|---|---|---|
| Core/Automaton | Completeness.v | 2 | Known FALSE lemma (fold_state_insert_incl) |
| Core/Automaton | Soundness.v | 3 | Deep proof dependencies |
| Core/Automaton | MainTheorem.v | 2 | Depends on admitted completeness lemmas |
| Core/Composition | DamerauComposition.v | 2 | Triangle inequality bounds |
| Grammar/Composition | Correctness.v | 3 | See current grammar verification README |
| Grammar/NFA | Multiple | 23 | Various |
| Total | 37 |
The fold_state_insert_incl lemma at line 4853 is documented as FALSE:
(* The claim incl pos_list1 pos_list2 implies
incl (positions (fold ... pos_list1 ...)) (positions (fold ... pos_list2 ...))
is FALSE because antichain filtering can remove positions from pos_list1
that would have been subsumed by new positions in pos_list2. *)
This requires restructuring the proofs that depend on it.
Triangle inequality bounds fail in specific cases:
The remaining admits require significant mathematical work and/or architectural changes to the proofs. They are not simple fixes.
docs/verification/grammar/theories/NFA/Transitions.v - Fixed compilation errorsdocs/verification/grammar/theories/NFA/Completeness.v - Fixed Fixpoint termination and importsdocs/verification/grammar/theories/NFA/Soundness.v - Fixed multiple proof issuesContext: HEAD commit 7304a33 added (G4) a weighted articulatory distance — a
FeatureDistanceWeights struct of per-dimension f64 base costs whose Default/standard
reproduces the built-in IPA constants — and (G9) a value-yielding transducer query
Transducer::query_values. This session brought both to a formally-verified standard.
FeatureWeights parameter preserves
symmetry and identity for all weights, and (for non-negative weights) non-negativity and
boundedness-by-weight-sum; and the distance is per-dimension monotone (non-decreasing in each
weight). The historical <= 1 bound is recoverable for the standard weights (which sum to one)..min(1.0) cap) satisfies the same properties, with boundedness <= 1 holding for all
non-negative weights because the cap enforces it.query_values reads each match's value during traversal so that the yielded value equals the
dictionary's stored value (no second lookup), skips valueless finals, and is sound / complete /
deduplicating like the underlying query.light profile):
docs/verification/articulatory/theories/FeatureDistance.v: introduced
Record FeatureWeights, standard_weights, weights_nonneg, and articulatory_distance_w;
re-proved articulatory_w_symmetric, articulatory_w_identity, articulatory_w_nonneg,
articulatory_w_bounded_by_sum, articulatory_w_monotone (+ per-dimension corollaries), and
recovered articulatory_bounded (0 <= d <= 1) for standard_weights via
standard_weights_sum_to_one. The historical articulatory_symmetric/_identity names are kept
as standard-weight corollaries; the b/t/k examples and triangle_b_t_k_tight are unchanged.docs/verification/articulatory/theories/FeatureDistanceWeighted.v: a faithful 7-dimension
model with the vowel path and the explicit cap via Qmin, mirroring Rust FeatureDistanceWeights
field-for-field; proved fsd7_symmetric, fsd7_identity, fsd7_nonneg, fsd7_bounded (for all
weights, from the cap), and fsd7_monotone (non-strict, through the cap), with non-vacuity examples.docs/verification/tla/ValueYieldingQuery.tla (+ .cfg) modeling the
query_values BFS over a concrete dictionary with valued/valueless and in-range/out-of-range finals
and a shared-term dedup case; checked ValueCorrectness, Soundness, NoValuelessYielded,
DedupInv, CompletenessInv, and EventuallyTerminates.tests/proptest_articulatory_weighted.rs (symmetry/identity/
non-negativity/boundedness/default-parity/per-dimension monotonicity over arbitrary weights;
weighted edit-distance default-parity + symmetry) and tests/proptest_value_yielding_query.rs
(value-parity, set-parity vs query_with_distance, soundness, completeness, dedup, mixed-skip).0 Admitted / 0 Axiom, verified by grep and the coq-file light build). FeatureDistance.v: 13 theorems/
corollaries; FeatureDistanceWeighted.v: 5 main theorems + supporting lemmas + 3 examples.Model checking completed. No error has been found. (31 distinct states, depth 8); the model
emits no constant-level-formula warnings (invariants reference variables → non-vacuous). Evidence
committed to docs/verification/tla/states/tlc-results-2026-05-27.txt.--features phonetic-rules for G4; default + --features pathmap-backend
for G9). The existing suite stays green (the unweighted functions delegate to the weighted leaf with
Default weights, preserving behavior).CONFIRMED. The additive weight parameterization preserves the metric-shaped properties
(symmetry, identity) for all weights and is non-negative, bounded, and per-dimension monotone for
non-negative weights; the capped 7-dimension model is bounded by 1 for all non-negative weights. The
monotonicity is non-strict (the cap saturates increases) — which is exactly why the Rust proptest
monotonicity property is stated with >=, and the per-dimension unit tests use cap-safe character
pairs for strict monotonicity. For G9, the value-yielding query's new surface (value read during
traversal, valueless-skip) is verified by the TLA+ ValueCorrectness/NoValuelessYielded invariants
and the value-parity property test against the real dictionary.
FeatureWeights{w_place,w_manner,w_voice} / FeatureWeights7{...} ↔ Rust
FeatureDistanceWeights; standard_weights* ↔ FeatureDistanceWeights::standard().articulatory_w_monotone* / fsd7_monotone ↔ Rust weighted_*_monotonic unit tests and
weighted_per_dimension_monotonicity proptest.ValueCorrectness ↔ Rust prop_value_yielding_value_parity; NoValuelessYielded ↔
test_value_yielding_skips_valueless_final / prop_value_yielding_mixed_skip.The W3 T2 consumer suite reported that docs/verification/tla/LlevBatchLease.tla's Reduce
action was guarded by cursor = "idle", while the liblevenshtein C ABI accepts llev_query_reduce
on an already-ended cursor (returns Ok, fires zero callbacks, out_count = 0). The model was
therefore strictly narrower than the implementation: reduce-on-ended was an un-modeled transition
(neither Reduce, which needed idle, nor ReduceRejected, which needs leased).
Widening Reduce's guard from cursor = "idle" to cursor \in {"idle", "ended"} faithfully
models reduce-on-ended as an Ok no-op, provided that entering "ended" always drains
batchesLeft to 0 — then from "ended" the existential consumed \in 0..batchesLeft is forced to
0, so the step mints no generation, consumes no batch, and keeps the cursor "ended". All existing
invariants and the four temporal properties should continue to hold, and ReduceNeverLeaks should
then cover the ended path automatically.
"ended" are
NextBatchEnds (guarded by batchesLeft = 0) and Reduce (sets cursor' = "ended" only when
batchesLeft' = 0). Encoded it as a new checked invariant
EndedHasNoBatches == cursor = "ended" => batchesLeft = 0.Reduce's guard, added EndedHasNoBatches to LlevBatchLease.cfg, and re-ran TLC under
the repository cap (systemd-run --user --scope -p MemoryMax=8G, MaxGeneration = 3,
MaxBatches = 4).Model checking completed. No error has been found. — 31 distinct states. TypeOK,
EndedHasNoBatches, GenerationsNeverZero, BusyImpliesLeased, and RejectedFreeKeepsOwnership
all hold as invariants; AdvanceOnlyUnleased, LeaseTagStable, ReduceNeverLeaks, and
FreedIsTerminal all hold as temporal properties. Because Reduce now fires from {idle, ended}
and always yields cursor' \in {idle, ended}, the unchanged property
ReduceNeverLeaks == [][Reduce => cursor' # "leased"]_vars now certifies the ended path too, with no
change to any property statement.
CONFIRMED and FIXED. The gap was in the model, not the implementation — the ABI was already correct; the spec was under-specified. The batch-lease spec now models reduce-on-ended exactly as the ABI implements it, and the widening is justified by a machine-checked invariant rather than by inspection alone. No production code changed.
Reduce (widened) <-> Rust llev_query_reduce accepting an ended cursor (Ok, zero
callbacks): tests/ffi_batch_lease_correspondence.rs::free_on_idle_and_on_ended_cursors_succeeds
and the reducer laws in tests/ffi_reducer_laws.rs.EndedHasNoBatches <-> the ABI guarantee that an exhausted cursor holds no leasable batch.docs/verification/ABI_INVARIANTS.tsv) point at the now
complete model.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 |