Skip to content

v4.27.0-rc1 #147

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
pandaman64 merged 4 commits into from
Dec 16, 2025
Merged

v4.27.0-rc1 #147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
29ffe2f
Update regex to v4.27.0-rc1
pandaman64 Dec 16, 2025
228528c
Update correctness to v4.27.0-rc1
pandaman64 Dec 16, 2025
8fb231d
Migrate remaining ValidPos
pandaman64 Dec 16, 2025
2475cf3
Upgrade docbuild to v4.27.0-rc1
pandaman64 Dec 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions correctness/RegexCorrectness/Backtracker/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,14 @@ import Mathlib.Tactic.DepRewrite
set_option autoImplicit false

open Regex.Data (BitMatrix BVPos)
open String (ValidPos)
open String (Pos)

namespace Regex.Backtracker

namespace captureNextAux.pushNext

variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed}
{startPos : ValidPos s} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : BVPos startPos}
{startPos : Pos s} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : BVPos startPos}

theorem done (hn : nfa[state] = .done) : pushNext σ nfa wf startPos stack update state pos = stack := by
rw! [pushNext, hn]
Expand Down Expand Up @@ -75,7 +75,7 @@ theorem sparse_neg {cs : Data.Classes} {state' : Nat} (hn : nfa[state] = .sparse
| .inl h => simp [h]
| .inr ⟨ne, hc⟩ => simp [ne, hc]

theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
{motive : List (StackEntry σ nfa startPos) → σ.Update → Fin nfa.nodes.size → BVPos startPos → Prop}
(done : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : BVPos startPos),
nfa[state] = .done → motive stack update state pos)
Expand Down Expand Up @@ -147,7 +147,7 @@ theorem fun_cases' (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos

end captureNextAux.pushNext

theorem captureNextAux.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
theorem captureNextAux.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
(motive : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → List (StackEntry σ nfa startPos) → Prop)
(base : ∀ (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), motive visited [])
(visited : ∀ (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : BVPos startPos) (stack' : List (StackEntry σ nfa startPos)),
Expand Down Expand Up @@ -175,7 +175,7 @@ Simplification lemmas for `captureNextAux`.
-/
section

variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}
variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)}

theorem captureNextAux_base :
captureNextAux σ nfa wf startPos visited [] = (.none, visited) := by
Expand Down Expand Up @@ -206,7 +206,7 @@ theorem captureNextAux_next {update state pos stack'} (mem : ¬visited.get state

end

theorem captureNext.go.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : ValidPos s)
theorem captureNext.go.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : Pos s)
(motive : (pos : BVPos startPos) → BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → Prop)
(found : ∀ (pos : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)),
captureNextAux σ nfa wf startPos visited [⟨σ.empty, ⟨nfa.start, wf.start_lt⟩, pos⟩] = (.some update, visited') →
Expand All @@ -231,7 +231,7 @@ Simplification lemmas for `captureNext.go`.
section

variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed}
{startPos : ValidPos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : BVPos startPos}
{startPos : Pos s} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : BVPos startPos}

theorem captureNext.go_found {update visited'} (h : captureNextAux σ nfa wf startPos visited [⟨σ.empty, ⟨nfa.start, wf.start_lt⟩, pos⟩] = (.some update, visited')) :
captureNext.go σ nfa wf startPos pos visited = .some update := by
Expand Down
12 changes: 6 additions & 6 deletions correctness/RegexCorrectness/Backtracker/Compile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import RegexCorrectness.NFA.Semantics

set_option autoImplicit false

open String (ValidPos)
open String (Pos)
open Regex.NFA (EquivUpdate)
open Regex.Data (CaptureGroups BitMatrix BVPos)

Expand All @@ -14,7 +14,7 @@ namespace captureNext

theorem path_done_of_some {s nfa wf pos update} (hres : captureNext (HistoryStrategy s) nfa wf pos = .some update) :
∃ state pos' pos'', nfa[state] = .done ∧ pos ≤ pos' ∧ Path nfa wf pos' pos'' state update := by
let bvpos : BVPos pos := ⟨pos, ValidPos.le_refl _⟩
let bvpos : BVPos pos := ⟨pos, Pos.le_refl _⟩
dsimp [captureNext] at hres
have ⟨state, bvpos', bvpos'', hn, le, path⟩ := go.path_done_of_some hres
exact ⟨state, bvpos'.current, bvpos''.current, hn, le, path⟩
Expand All @@ -32,25 +32,25 @@ theorem capture_of_some_compile {s e pos update} (hres : captureNext (HistoryStr
exact ⟨pos', pos'', groups, le, c, eqv⟩

theorem ne_done_of_path_of_none {s nfa wf pos} (hres : captureNext (HistoryStrategy s) nfa wf pos = .none) :
∀ (pos' pos'' : ValidPos s) (state : Fin nfa.nodes.size) (update : List (Nat × ValidPos s)),
∀ (pos' pos'' : Pos s) (state : Fin nfa.nodes.size) (update : List (Nat × Pos s)),
pos ≤ pos' →
Path nfa wf pos' pos'' state update →
nfa[state] ≠ .done := by
dsimp [captureNext] at hres

let bvpos : BVPos pos := ⟨pos, ValidPos.le_refl _⟩
let bvpos : BVPos pos := ⟨pos, Pos.le_refl _⟩
let visited := BitMatrix.zero nfa.nodes.size (pos.remainingBytes + 1)

have h := go.ne_done_of_path_of_none hres (BVPos.le_refl _) go.Inv.zero captureNextAux.NotDoneInv.zero

intro pos' pos'' state update le path hn
let bvpos' : BVPos pos := ⟨pos', le⟩
let bvpos'' : BVPos pos := ⟨pos'', ValidPos.le_trans le path.le⟩
let bvpos'' : BVPos pos := ⟨pos'', Pos.le_trans le path.le⟩

exact h bvpos' bvpos'' state update bvpos'.le path hn

theorem not_captures_of_none_compile {s e pos} (hres : captureNext (HistoryStrategy s) (NFA.compile e) NFA.compile_wf pos = .none)
(pos' pos'' : ValidPos s) (groups : CaptureGroups s) (le : pos ≤ pos') :
(pos' pos'' : Pos s) (groups : CaptureGroups s) (le : pos ≤ pos') :
¬e.Captures pos' pos'' groups := by
intro c
have ⟨update, _, path⟩ := NFA.path_of_captures_compile rfl c
Expand Down
10 changes: 5 additions & 5 deletions correctness/RegexCorrectness/Backtracker/Correctness.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ open Regex (NFA)
open Regex.Data (Expr CaptureGroups)
open Regex.Strategy (EquivMaterializedUpdate materializeRegexGroups materializeUpdates)
open RegexCorrectness.Spec (SearchProblem)
open String (ValidPos)
open String (Pos)

namespace Regex.Backtracker

theorem captureNext_soundness {s e bufferSize pos matchedB}
(disj : e.Disjoint)
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .some matchedB) :
∃ (pos' pos'' : ValidPos s) (groups : CaptureGroups s),
∃ (pos' pos'' : Pos s) (groups : CaptureGroups s),
pos ≤ pos' ∧
e.Captures pos' pos'' groups ∧
EquivMaterializedUpdate (materializeRegexGroups groups) matchedB := by
Expand All @@ -31,7 +31,7 @@ theorem captureNext_soundness {s e bufferSize pos matchedB}

theorem captureNext_completeness' {s e bufferSize pos}
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .none)
(pos' pos'' : ValidPos s) (groups : CaptureGroups s) (le : pos ≤ pos') (c : e.Captures pos' pos'' groups) :
(pos' pos'' : Pos s) (groups : CaptureGroups s) (le : pos ≤ pos') (c : e.Captures pos' pos'' groups) :
False := by
match hresH : captureNext (HistoryStrategy s) (NFA.compile e) NFA.compile_wf pos with
| .some matchedH =>
Expand All @@ -41,13 +41,13 @@ theorem captureNext_completeness' {s e bufferSize pos}

theorem captureNext_completeness {s e bufferSize pos}
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) NFA.compile_wf pos = .none) :
¬∃ (pos' pos'' : ValidPos s) (groups : CaptureGroups s),
¬∃ (pos' pos'' : Pos s) (groups : CaptureGroups s),
pos ≤ pos' ∧
e.Captures pos' pos'' groups := by
grind [captureNext_completeness']

-- NOTE: we don't make this an instance because there are multiple decision procedures
def decideSearchProblem {s : String} (e : Expr) (pos : ValidPos s) (disj : e.Disjoint) : Decidable (SearchProblem e pos) :=
def decideSearchProblem {s : String} (e : Expr) (pos : Pos s) (disj : e.Disjoint) : Decidable (SearchProblem e pos) :=
match hresB : captureNext (BufferStrategy s 0) (NFA.compile e) NFA.compile_wf pos with
| .some _ => .isTrue <|
have ⟨pos', pos'', groups, le, c, _⟩ := captureNext_soundness disj hresB
Expand Down
16 changes: 8 additions & 8 deletions correctness/RegexCorrectness/Backtracker/Path.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,27 +3,27 @@ import RegexCorrectness.NFA.Semantics.Path

set_option autoImplicit false

open String (ValidPos)
open String (Pos)
open Regex.Data (BVPos)

namespace Regex.Backtracker

inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : ValidPos s) : ValidPos s → Fin nfa.nodes.size → List (Nat × ValidPos s) → Prop where
inductive Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : Pos s) : Pos s → Fin nfa.nodes.size → List (Nat × Pos s) → Prop where
| init : Path nfa wf pos pos ⟨nfa.start, wf.start_lt⟩ []
| more {i j : Fin nfa.nodes.size} {pos' pos'' update₁ update₂ update₃} (prev : Path nfa wf pos pos' i update₁) (step : nfa.Step 0 i pos' j pos'' update₂)
(equpdate : update₃ = update₁ ++ List.ofOption update₂) :
Path nfa wf pos pos'' j update₃

namespace Path

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : ValidPos s} {i j : Fin nfa.nodes.size}
{update update₁ update₂ update₃ : List (Nat × ValidPos s)}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : Pos s} {i j : Fin nfa.nodes.size}
{update update₁ update₂ update₃ : List (Nat × Pos s)}

theorem le (path : Path nfa wf pos pos' i update) :
pos ≤ pos' := by
induction path with
| init => exact ValidPos.le_refl _
| more _ step _ ih => exact ValidPos.le_trans ih step.le
| init => exact Pos.le_refl _
| more _ step _ ih => exact Pos.le_trans ih step.le

theorem eq_or_nfaPath (path : Path nfa wf pos pos' i update) :
(pos' = pos ∧ i.val = nfa.start ∧ update = []) ∨
Expand Down Expand Up @@ -56,9 +56,9 @@ theorem of_nfaPath {i : Nat} (path : nfa.Path 0 nfa.start pos i pos' update) :
have path₁ : Path nfa wf pos pos ⟨nfa.start, wf.start_lt⟩ [] := .init
exact path₁.concat_nfaPath wf.start_lt path (by simp)

def bvpos' {startPos : ValidPos s} {bvpos : BVPos startPos} {pos' i update}
def bvpos' {startPos : Pos s} {bvpos : BVPos startPos} {pos' i update}
(path : Path nfa wf bvpos.current pos' i update) : BVPos startPos :=
⟨pos', ValidPos.le_trans bvpos.le path.le⟩
⟨pos', Pos.le_trans bvpos.le path.le⟩

end Path

Expand Down
8 changes: 4 additions & 4 deletions correctness/RegexCorrectness/Backtracker/Refinement.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@ set_option autoImplicit false
open Regex (NFA)
open Regex.Data (BitMatrix BVPos)
open Regex.Strategy (materializeUpdates)
open String (ValidPos ValidPosPlusOne)
open String (Pos PosPlusOne)
namespace Regex.Backtracker

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bufferSize : Nat}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bufferSize : Nat}

def StackEntry.materialize (entryH : StackEntry (HistoryStrategy s) nfa startPos) : StackEntry (BufferStrategy s bufferSize) nfa startPos :=
⟨materializeUpdates bufferSize entryH.update, entryH.state, entryH.pos⟩
Expand All @@ -24,10 +24,10 @@ theorem materializeStack.nil : materializeStack [] = ([] : List (StackEntry (Buf
theorem materializeStack.cons {entryH stackH} :
materializeStack (entryH :: stackH) = (StackEntry.materialize entryH :: materializeStack stackH : List (StackEntry (BufferStrategy s bufferSize) nfa startPos)) := rfl

def materializeResultAux (resultH : Option (List (Nat × ValidPos s)) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) :=
def materializeResultAux (resultH : Option (List (Nat × Pos s)) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option (Buffer s bufferSize) × BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) :=
⟨resultH.1.map (materializeUpdates bufferSize), resultH.2⟩

def materializeResult (resultH : Option (List (Nat × ValidPos s))) : Option (Buffer s bufferSize) :=
def materializeResult (resultH : Option (List (Nat × Pos s))) : Option (Buffer s bufferSize) :=
resultH.map (materializeUpdates bufferSize)

theorem captureNextAux.pushNext.refines {s nfa wf startPos bufferSize stackH stackB updateH updateB state pos}
Expand Down
28 changes: 14 additions & 14 deletions correctness/RegexCorrectness/Backtracker/Traversal/Invariants.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import RegexCorrectness.Backtracker.Path
set_option autoImplicit false

open Regex.Data (BitMatrix BVPos)
open String (ValidPos)
open String (Pos)
open Regex.NFA (Step)

namespace Regex.Backtracker.captureNextAux
Expand Down Expand Up @@ -46,7 +46,7 @@ end

section

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
{visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)} {update' visited'}

def StackInv (wf : nfa.WellFormed) (bvpos : BVPos startPos) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
Expand Down Expand Up @@ -156,11 +156,11 @@ end

section

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s}
{bvpos₀ : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}

def ClosureInv (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry (HistoryStrategy s) nfa startPos)) : Prop :=
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
bvpos₀ ≤ bvpos →
visited.get state bvpos.index →
nfa.Step 0 state bvpos.current state' bvpos'.current update →
Expand All @@ -171,7 +171,7 @@ namespace ClosureInv
-- Preservation of the non-visited cases
theorem preserves' {entry stack'} (inv : ClosureInv bvpos₀ visited (entry :: stack))
(nextEntries : List (StackEntry (HistoryStrategy s) nfa startPos)) (hstack : stack' = nextEntries ++ stack)
(hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
(hnext : ∀ (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
nfa.Step 0 entry.state entry.pos.current state' bvpos'.current update →
∃ entry' ∈ nextEntries, entry'.state = state' ∧ entry'.pos = bvpos') :
ClosureInv bvpos₀ (visited.set entry.state entry.pos.index) stack' := by
Expand Down Expand Up @@ -256,7 +256,7 @@ theorem preserves {stack update state bvpos} (wf : nfa.WellFormed) (inv : Closur
| char_neg stack' update state bvpos c state' hn h =>
rw [pushNext.char_neg hn h]
apply inv.preserves' [] (by simp)
have {ne : bvpos.current ≠ s.endValidPos} : bvpos.current.get ne ≠ c := by
have {ne : bvpos.current ≠ s.endPos} : bvpos.current.get ne ≠ c := by
match h with
| .inl eq => simp [eq] at ne
| .inr ⟨ne', hc⟩ => simpa [BVPos.get] using hc
Expand All @@ -272,7 +272,7 @@ theorem preserves {stack update state bvpos} (wf : nfa.WellFormed) (inv : Closur
| sparse_neg stack' update state bvpos cs state' hn h =>
rw [pushNext.sparse_neg hn h]
apply inv.preserves' [] (by simp)
have {ne : bvpos.current ≠ s.endValidPos} : bvpos.current.get ne ∉ cs := by
have {ne : bvpos.current ≠ s.endPos} : bvpos.current.get ne ∉ cs := by
match h with
| .inl eq => simp [eq] at ne
| .inr ⟨ne', hc⟩ => simpa [BVPos.get] using hc
Expand Down Expand Up @@ -311,14 +311,14 @@ theorem step_closure {bvpos₀ bvpos : BVPos startPos} {result} (hres : captureN
exact ih hres (cinv.preserves wf hn) stinv.preserves

def StepClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × ValidPos s)),
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : Option (Nat × Pos s)),
bvpos₀ ≤ bvpos →
visited.get state bvpos.index →
nfa.Step 0 state bvpos.current state' bvpos'.current update →
visited.get state' bvpos'.index

def PathClosure (bvpos₀ : BVPos startPos) (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : List (Nat × ValidPos s)),
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos) (state' : Fin nfa.nodes.size) (bvpos' : BVPos startPos) (update : List (Nat × Pos s)),
bvpos₀ ≤ bvpos →
visited.get state bvpos.index →
nfa.Path 0 state bvpos.current state' bvpos'.current update →
Expand All @@ -331,12 +331,12 @@ theorem zero : PathClosure bvpos₀ (BitMatrix.zero nfa.nodes.size (startPos.rem
simp at hmem

theorem of_step_closure {bvpos₀ : BVPos startPos} (wf : nfa.WellFormed) (h : StepClosure bvpos₀ visited) : PathClosure bvpos₀ visited := by
let motive (i : Nat) (pos : ValidPos s) : Prop :=
let motive (i : Nat) (pos : Pos s) : Prop :=
∃ (isLt : i < nfa.nodes.size) (bvpos : BVPos startPos), bvpos₀ ≤ bvpos ∧ pos = bvpos.current ∧ visited.get ⟨i, isLt⟩ bvpos.index
have cls i pos j pos' update (base : motive i pos) (step : nfa.Step 0 i pos j pos' update) : motive j pos' := by
have ⟨_, bvpos, le, hbvpos, hmem⟩ := base

let bvpos' : BVPos startPos := ⟨pos', ValidPos.le_trans (hbvpos ▸ bvpos.le) step.le⟩
let bvpos' : BVPos startPos := ⟨pos', Pos.le_trans (hbvpos ▸ bvpos.le) step.le⟩

have le₀' : bvpos₀ ≤ bvpos' := BVPos.le_trans le (BVPos.le_iff.mpr (hbvpos ▸ step.le))
have visited' := h ⟨i, step.lt⟩ bvpos ⟨j, step.lt_right wf⟩ bvpos' update le hmem (by simp [←hbvpos, bvpos', step])
Expand Down Expand Up @@ -369,7 +369,7 @@ end

section

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bvpos₀ bvpos : BVPos startPos}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos}
{visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}

def VisitedInv (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) (visited visited' : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
Expand All @@ -386,7 +386,7 @@ theorem rfl (wf : nfa.WellFormed) (bvpos₀ bvpos : BVPos startPos) : VisitedInv

theorem preserves {bvpos' : BVPos startPos} {state : Fin nfa.nodes.size}
(inv : VisitedInv wf bvpos₀ bvpos visited visited')
(update : List (Nat × ValidPos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
(update : List (Nat × Pos s)) (path : Path nfa wf bvpos.current bvpos'.current state update) :
VisitedInv wf bvpos₀ bvpos visited (visited'.set state bvpos'.index) := by
intro state' bvpos'' le' hmem
simp [visited'.get_set] at hmem
Expand Down Expand Up @@ -423,7 +423,7 @@ end

section

variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}
variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : Pos s} {bvpos₀ bvpos : BVPos startPos} {visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {stack : List (StackEntry (HistoryStrategy s) nfa startPos)}

def NotDoneInv (visited : BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Prop :=
∀ (state : Fin nfa.nodes.size) (bvpos : BVPos startPos),
Expand Down
Loading