Date: 2025-11-19 (Updated: apply_rule_at_preserves_prefix completed)
Status: Prefix preservation proven, position-independence infrastructure built, proof structure documented
File: position_skipping_proof.v
Completion: 37/38 theorems proven with Qed (97.4%)
This document summarizes the formal verification work on the position skipping optimization for phonetic rewrite rules. The optimization attempts to improve performance by avoiding redundant position searches, but we prove it requires careful conditions to maintain correctness.
Standard Algorithm:
for each iteration:
for each rule:
search from position 0 to find first match
if found: apply rule and restart iteration
if no rule matched: terminate
Optimized Algorithm (Position Skipping):
let last_pos = 0
for each iteration:
for each rule:
search from position last_pos to find first match
if found: apply rule, set last_pos = match_position, restart iteration
if no rule matched: terminate
Hypothesis: Starting search from last_pos instead of 0 should be safe since we just modified at that position.
find_first_match_from_lower_bound (PROVEN ✓)Lemma find_first_match_from_lower_bound :
forall r s start_pos n pos,
find_first_match_from r s start_pos n = Some pos ->
(start_pos <= pos)%nat.
Significance: Establishes that the optimized search only finds matches at or after start_pos, confirming its fundamental behavior.
find_first_match_from_empty (PROVEN ✓)Lemma find_first_match_from_empty :
forall r s start_pos,
(start_pos > length s)%nat ->
find_first_match_from r s start_pos 0 = None.
Significance: Boundary condition - search with zero range returns None.
apply_rules_seq_opt_terminates (PROVEN ✓)Theorem apply_rules_seq_opt_terminates :
forall rules s fuel last_pos,
exists result,
apply_rules_seq_opt rules s fuel last_pos = Some result.
Significance: Termination guarantee. The optimized algorithm always terminates (proven by structural induction on fuel).
final_position_can_change (PROVEN ✓)Lemma final_position_can_change :
exists s s' pos,
(length s' < length s)%nat /\
context_matches Final s pos = false /\
context_matches Final s' pos = true.
Significance: Identifies the safety issue. Demonstrates that Context::Final matching can change after string transformations, which is the root cause of potential unsafety.
find_first_match_from_equivalent_when_no_early_matches (ADMITTED)Lemma find_first_match_from_equivalent_when_no_early_matches :
forall r s start_pos,
no_early_matches r s start_pos ->
(forall pos, find_first_match_from r s start_pos (length s - start_pos + 1) = Some pos ->
find_first_match r s (length s) = Some pos).
Status: Proof strategy outlined, requires detailed induction.
position_skip_safe_for_local_contexts (ADMITTED)Theorem position_skip_safe_for_local_contexts :
forall rules s fuel,
(forall r, In r rules -> position_dependent_context (context r) = false) ->
apply_rules_seq rules s fuel = apply_rules_seq_opt rules s fuel 0.
Status: Main safety theorem. Proof strategy:
Final), matches don't appear at earlier positions after transformationDefinition position_dependent_context (ctx : Context) : bool :=
match ctx with
| Final => true (* Depends on string length *)
| Initial => false (* Position 0 is invariant *)
| BeforeVowel _ => false (* Local structure only *)
| AfterConsonant _ => false
| BeforeConsonant _ => false
| AfterVowel _ => false
| Anywhere => false
end.
Definition no_early_matches (r : RewriteRule) (s : PhoneticString) (start_pos : nat) : Prop :=
forall pos, (pos < start_pos)%nat -> can_apply_at r s pos = false.
Position skipping is SAFE if:
Context::Final (proven conditionally)Position skipping is UNSAFE if:
Context::Final and the string can shortenp, an earlier position q < p can become finalfn has_final_context_rule(rules: &[RewriteRule]) -> bool {
rules.iter().any(|r| matches!(r.context, Context::Final))
}
if has_final_context_rule(rules) {
// Use standard algorithm (always search from position 0)
} else {
// Use optimized algorithm (position skipping)
}
fn apply_rules_seq_hybrid(rules: &[RewriteRule], s: &[Phone], fuel: usize) -> Option<Vec<Phone>> {
let has_final = has_final_context_rule(rules);
let mut last_pos = 0;
for iteration in 0..fuel {
for rule in rules {
let start_pos = if has_final || matches!(rule.context, Context::Final) {
0 // Always search from beginning for Final-context rules
} else {
last_pos // Use optimization for other contexts
};
if let Some(pos) = find_first_match_from(rule, s, start_pos) {
s = apply_rule_at(rule, s, pos)?;
last_pos = pos;
break; // Restart iteration
}
}
}
Some(s)
}
// Don't implement position skipping at all
// Use standard algorithm for v0.8.0
// Re-evaluate for v0.9.0 if profiling shows bottleneck
Date Updated: 2025-11-19 (Final Session - Search Equivalence Completed) Status: ✅ COMPILATION SUCCESSFUL - 36/38 theorems/lemmas proven with Qed (94.7% complete)
| Component | Status | Lines of Proof |
|---|---|---|
| Algorithm definition | ✓ Complete | 45 |
| Arithmetic & bounds lemmas | ✓ 6 Proven | ~50 |
| Helper lemmas (find_first_match) | ✓ 9 Proven | ~180 |
| Phase 1-3 helper lemmas | ✓ 7 Proven | ~35 |
| Termination theorem | ✓ Proven | 28 |
| Safety characterization (Final context) | ✓ Proven | 20 |
| Conditional safety theorem | ✓ Proven | 15 |
| find_first_match_finds_first_true | ✓ Proven | ~67 |
| Bidirectional search equivalence | ✓ Proven | ~90 |
| Position-independence infrastructure | ✓ 5 Proven, 1 Admitted | ~60 |
| Main theorem (position_skip_safe_for_local_contexts) | ⚠️ Admitted (proof structure documented) | ~80 |
| Total | 36 theorems proven, 2 admitted | ~750 lines |
Legend:
Qed (no admits)apply_rules_seq_opt_terminates): Optimized algorithm always terminates ✓ Provenfind_first_match_equiv_from_zero): Fuel-based and position-based search are equivalent ✓ Proven (NEW)find_first_match_equiv_from_zero_reverse, find_first_match_from_zero_bidirectional): Both directions of search equivalence ✓ Proven (NEW)position_skipping_conditionally_safe): Position skipping is safe when no rules have position-dependent contexts ✓ Provenfinal_position_can_change): Context::Final creates position-dependent matching ✓ Proven by counterexampleapply_rule_at_preserves_prefix): Rule application preserves phones before match position ✓ Proven (list manipulation with nth_error)initial_context_preserved, anywhere_context_preserved): Simple contexts preserved at earlier positions ✓ Proven (NEW)position_skip_safe_for_local_contexts): ⚠️ Admitted with detailed proof structure (requires complex case analysis on all context types)RECOMMENDATION: Do NOT implement position skipping optimization
Rationale:
Context::FinalFuture Work (v0.9.0+):
Context::Final edge casesposition_skipping_proof.v (253 lines) - Complete Coq formalizationcoqc -Q . PhoneticRewrites position_skipping_proof.vdocs/optimization/phonetic/00-investigation-log.mddocs/optimization/phonetic/07-algorithmic-optimization-analysis.mddocs/verification/phonetic/rewrite_rules.vdocs/verification/phonetic/zompist_rules.vDate Completed: 2025-11-19 (Final session - search equivalence completed) Verified By: Coq proof assistant (v9.x+) Compilation: ✅ SUCCESSFUL (position_skipping_proof.vo generated) Status: ✅ NEAR COMPLETION (36/38 theorems proven with Qed - 94.7% complete, 2 admitted with documented proof gaps)
Arithmetic & Bounds Lemmas:
sub_add_inverse - Subtraction addition inverse for bounded natsub_S_decompose - Successor subtraction decompositionsub_lt_mono - Subtraction monotonicity with successorpos_in_search_range - Position in search range boundssearch_range_bound - Search range upper boundsearch_range_strict_bound - Strict search range boundSearch Algorithm Lemmas:
7. ✓ find_first_match_from_lower_bound - Search returns positions >= start
8. ✓ find_first_match_from_empty - Empty search returns None
9. ✓ find_first_match_some_implies_can_apply - Found position is valid
10. ✓ find_first_match_is_first - No earlier positions match
11. ✓ find_first_match_from_upper_bound - Search returns positions in bounds
12. ✓ find_first_match_from_is_first - Search finds first valid position
13. ✓ find_first_match_from_implies_can_apply - Found position has can_apply_at true
Main Theorems:
14. ✓ apply_rules_seq_opt_terminates - Termination guarantee
15. ✓ final_position_can_change - Counterexample for Final context unsafety
16. ✓ position_skipping_conditionally_safe - Safety under position-independence
find_first_match_search_range - Contains admit for empty string edge case (non-empty pattern axiom needed)find_first_match_finds_first_true - Proof strategy outlined (truncating subtraction complexity)find_first_match_equiv_from_zero - Bidirectional equivalence (requires complex mutual induction)find_first_match_from_equivalent_when_no_early_matches - Main Theorem 1 (contains 2 admits for non-empty pattern edge cases)apply_rule_at_pos_valid - Helper axiom (non-empty pattern requirement)position_skip_safe_for_local_contexts - Main Theorem 2 (requires position-independence preservation lemmas)Truncating Subtraction: ✅ SOLVED - Added 6 arithmetic lemmas to handle truncating nat subtraction correctly
Search Algorithm Properties: ✅ SOLVED - Proved 9 lemmas characterizing find_first_match behavior
Search Algorithm Correctness: ✅ MOSTLY SOLVED - Proved 7 out of 9 helper lemmas with full Qed (2 admitted for edge cases)
Non-Empty Pattern Axiom: Several edge cases (empty string matching, positions beyond string length) require an axiom that patterns are non-empty, which is reasonable for phonetic rewrite rules but not formally stated in the model.
Truncating Subtraction in Complex Proofs: While basic arithmetic lemmas handle most cases, complex inductive proofs involving length s - S fuel' still encounter edge cases that are difficult to prove.
Position-Independence Preservation: Main Theorem 2 requires proving that transformations don't create new matches at earlier positions - extensive case analysis on each context type (Initial, BeforeVowel, AfterConsonant, etc.).
Bidirectional Search Equivalence: Complex mutual induction on search range and fuel parameters.
✓ File compiles successfully: coqc -Q . PhoneticRewrites position_skipping_proof.v
✓ Output generated: position_skipping_proof.vo (43 KB)
✓ Zero compilation errors
✓ ~490 lines of formal Coq proofs
✓ 16/22 theorems proven with Qed (73% complete)
✓ 6 theorems admitted with documented edge cases
Starting Point: 4/6 theorems proven (original state) Final Result: 16/22 theorems proven with Qed (73% complete)
Improvements Made:
Time Investment: ~7 hours of focused proof work Lines of Proof: ~490 lines of formal Coq code Compilation: ✅ SUCCESSFUL - Zero errors, generates position_skipping_proof.vo (43 KB)
What Was Proven:
What Remains:
Production Impact:
Starting Point: 23/25 theorems proven (92%) Final Result: 36/38 theorems proven (94.7%) Improvement: +13 theorems proven, +150 lines of proof
Objective: Prove bidirectional equivalence between fuel-based and position-based search
Theorems Proven:
find_first_match_equiv_general - Generalized equivalence with arbitrary fuel and start_pos (~75 lines)find_first_match_equiv_from_zero - Main forward direction equivalence (~25 lines)find_first_match_equiv_from_zero_reverse - Reverse direction (~15 lines)find_first_match_from_zero_bidirectional - Bidirectional wrapper (~10 lines)Key Technique: Created generalized helper lemma with arbitrary parameters, then derived main theorem as special case. This avoided complex arithmetic reasoning about truncating nat subtraction.
Proof Strategy: Induction on fuel with careful handling of:
lia tactic for truncating subtractionObjective: Build lemmas to support main safety theorem
Theorems Proven:
context_preserved_at_earlier_positions - Definition of context preservationinitial_context_preserved - Initial context only depends on pos = 0 (~15 lines)anywhere_context_preserved - Anywhere context always matches (~10 lines)Theorems Admitted:
apply_rule_at_preserves_prefix~~ - ✓ COMPLETED (37 lines with assert-based strategy)
rewrite <- H_s'.) and separate assertions for each directioninjection was reversed; needed nth_error_app1 and nth_error_firstnRemoved:
position_independent_context_preserved - Too complex, requires case analysis on all 6 context typesObjective: Complete position_skip_safe_for_local_contexts proof
Progress:
find_first_match_from_zero_bidirectional lemmaRemaining Admits in Main Theorem:
wf_rule r assumption - should be theorem preconditionProof Gap Analysis:
The core challenge is proving that for position-independent contexts, applying a rule at position pos doesn't create new matches at earlier positions p < pos. This requires:
apply_rule_at preserves prefix (admitted as straightforward)Estimate: 4-6 hours of focused proof work to complete, primarily mechanical case analysis
Updates to 00-proof-summary.md:
Before: ~600 lines, 23 Qed, 2 Admitted After: ~750 lines, 36 Qed, 2 Admitted Compilation: ✅ Zero errors, generates position_skipping_proof.vo successfully
Estimated Time: 6-8 hours
Required Proofs:
apply_rule_at_preserves_prefix~~ - ✓ COMPLETEDposition_skip_safe_for_local_contexts (~5-7 hours) - Case analysis on all context types (REMAINING)Approach:
nth_error_app1, nth_error_firstn for prefix preservation~~ ✓ COMPLETEDConfidence: HIGH - No fundamental blockers, just mechanical case analysis
Session Progress: Successfully completed apply_rule_at_preserves_prefix proof, advancing from 36/38 (94.7%) to 37/38 (97.4%) completion.
Key Achievement: The prefix preservation lemma is now formally proven, establishing that rule application at position pos leaves all phones before pos unchanged. This required careful handling of Coq's list manipulation tactics, particularly:
rewrite <- H_s'.) due to equality direction from injectionnth_error_app1 and nth_error_firstn from Coq's List libraryArchival Gap: One theorem was still admitted in this summary
(position_skip_safe_for_local_contexts), requiring extensive case analysis on
all context types. The optimization stayed outside the v0.8.0 acceptance scope;
reviving it requires fresh profiling and a proof-session plan.
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 |