Regex.Compiler.Lemmas

Lemmas #

Proof that Compiler.Code.compile gives an array with the Compiler.nextOfLt and NFA.Capture.valid property

c_compile_spec: main result

source

def Compiler.Lemmas.tacticInst_mvar :

Lean.ParserDescr

instantiate mvar, mspec with a precondition like fun s => s = states ∧ P gives a uninstantiated mvar

Equations

Compiler.Lemmas.tacticInst_mvar = Lean.ParserDescr.node `Compiler.Lemmas.tacticInst_mvar 1024 (Lean.ParserDescr.nonReservedSymbol "inst_mvar" false)

Instances For

source

def Compiler.Lemmas.tacticInst_mvars :

Lean.ParserDescr

instantiate mvars, mspec with a precondition like fun s => s = states ∧ P gives a uninstantiated mvar

Equations

Compiler.Lemmas.tacticInst_mvars = Lean.ParserDescr.node `Compiler.Lemmas.tacticInst_mvars 1024 (Lean.ParserDescr.nonReservedSymbol "inst_mvars" false)

Instances For

source

theorem Compiler.Lemmas.lift_StackT_to_EStateM_spec {σ α : Type} {n : σ} {ε : Type} (v : StateT σ Id α) {P : σ → Prop} (Q : σ → α → σ → Prop) (hspec : ⦃fun (s : σ) => ⌜s = n ∧ P n⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q n a s⌝, ())⦄) :

⦃fun (s : σ) => ⌜s = n ∧ P n⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q n a s⌝, fun (x : ε) => ⌜True ⌝, ())⦄

source

def Compiler.Lemmas.coe_spec_StackT_to_EStateM {σ α ε : Type} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} (hspec : ⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, ())⦄) :

⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x : σ) => ⌜True ⌝, ())⦄

Equations

⋯ = hspec

Instances For

source

instance Compiler.Lemmas.instCoeTripleStateTIdPureEStateMLiftM_regex {σ α ε : Type} {v : StateT σ Id α} {P : σ → Prop} {Q : α → σ → Prop} :

Coe (⦃fun (s : σ) => ⌜P s⌝⦄ v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, ())⦄) (⦃fun (s : σ) => ⌜P s⌝⦄ liftM v ⦃(fun (a : α) (s : σ) => ⌜Q a s⌝, fun (x : ε) (x : σ) => ⌜True ⌝, ())⦄)

Equations

Compiler.Lemmas.instCoeTripleStateTIdPureEStateMLiftM_regex = { coe := ⋯ }

source

def Compiler.Lemmas.tRefLt (t : ThompsonRef) (r : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.tRefLt t r = (t.start < r.size ∧ t.end < r.size)

Instances For

source

def Compiler.Lemmas.statesNextOfLeLt (prevs s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.statesNextOfLeLt prevs s = (prevs.size ≤ s.size ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.stateIdNextOfLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.stateIdNextOfLt prevs sid s = (prevs.size < s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.stateIdNextOfLeLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.stateIdNextOfLeLt prevs sid s = (prevs.size ≤ s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.stateIdNextOfEqLt (prevs : Array NFA.Unchecked.State) (sid : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.stateIdNextOfEqLt prevs sid s = (prevs.size = s.size ∧ sid < s.size ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.tRefNextOfLt (prevs : Array NFA.Unchecked.State) (t : ThompsonRef) (s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.tRefNextOfLt prevs t s = (prevs.size < s.size ∧ Compiler.Lemmas.tRefLt t s ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.tRefNextOfLeLt (prevs : Array NFA.Unchecked.State) (t : ThompsonRef) (s : Array NFA.Unchecked.State) :

Prop

Equations

Compiler.Lemmas.tRefNextOfLeLt prevs t s = (prevs.size ≤ s.size ∧ Compiler.Lemmas.tRefLt t s ∧ Compiler.nextOfLt s)

Instances For

source

def Compiler.Lemmas.cValid (caps : Array NFA.Capture) :

Prop

Equations

Compiler.Lemmas.cValid caps = NFA.Capture.valid caps

Instances For

source

def Compiler.Lemmas.cMemAndValid (prev caps : Array NFA.Capture) :

Prop

Equations

Compiler.Lemmas.cMemAndValid prev caps = ((∀ (a : NFA.Capture), a ∈ prev → a ∈ caps) ∧ NFA.Capture.valid caps)

Instances For

source

def Compiler.Lemmas.cValidFunc (captures : Array NFA.Capture) :

Array NFA.Capture → Prop

Equations

Compiler.Lemmas.cValidFunc captures curr = (curr = captures ∧ Compiler.Lemmas.cValid captures)

Instances For

source

def Compiler.Lemmas.cMemAndValidFunc (captures : Array NFA.Capture) :

Array NFA.Capture → Prop

Equations

Compiler.Lemmas.cMemAndValidFunc captures curr = (curr = captures ∧ Compiler.Lemmas.cMemAndValid captures curr)

Instances For

source

@[simp]

theorem Compiler.Lemmas.cMemAndValid_of_cValid (captures s : Array NFA.Capture) :

s = captures ∧ cValid captures → cMemAndValid captures s

source

@[simp]

theorem Compiler.Lemmas.cMemAndValidFunc_of_cValidFunc (captures s : Array NFA.Capture) :

cValidFunc captures s → cMemAndValidFunc captures s

source

theorem Compiler.Lemmas.lift_CompilerM_bind_pure {ε σ α : Type} [MonadLiftT (EStateM ε σ) Code.CompilerM] (x : EStateM ε σ α) :

liftM x >>= EStateM.pure = liftM x

source

theorem Compiler.Lemmas.pure_of_imp_spec {α σ ε : Type} {x : α} {P1 P2 : α → σ → Prop} (h : ∀ (a : α) (s : σ), P1 a s → P2 a s) :

⦃fun (s : σ) => ⌜P1 x s⌝⦄ EStateM.pure x ⦃(fun (r : α) (s : σ) => ⌜P2 r s⌝, fun (x : ε) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.patch_spec («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} {states : Array NFA.Unchecked.State} :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ «from» < states.size ∧ to < states.size⌝⦄ Code.patch «from» to ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => ⌜stateIdNextOfEqLt states to r⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.patch_lift_spec («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states ∧ «from» < states.size ∧ to < states.size) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.patch «from» to) ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfEqLt states to s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.push_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push sid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.push_lift_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ liftM (Code.push sid) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.push_run_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) (h1 : nextOfLt states) (h2 : sid.nextOf ≤ states.size) :

⦃⌜True ⌝⦄ StateT.run (Code.push sid) states ⦃(fun (r : NFA.Unchecked.StateID × Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r.fst r.snd⌝, ())⦄

source

theorem Compiler.Lemmas.push_run_lift_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ liftM (Code.push sid states) ⦃(fun (r : NFA.Unchecked.StateID × Array NFA.Unchecked.State) (x : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r.fst r.snd⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.push'_spec (sid : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ sid.nextOf ≤ states.size⌝⦄ Code.push' sid ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_match_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_match pattern_id ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_match_lift_spec (pattern_id : NFA.PatternID) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.add_match pattern_id) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_union_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_union_lift_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_union_lift'_spec (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.add_union ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_union_reverse_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_union_reverse_lift_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_backrefence_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_backrefence case_insensitive b ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_backrefence_lift_spec (case_insensitive : Bool) (b : Nat) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM (Code.add_backrefence case_insensitive b) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_range_spec (start «end» : UInt32) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_range start «end» ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_empty_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_empty_lift_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_empty_lift'_spec (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.add_empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_fail_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_fail_lift_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_fail ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.eat_next_of_le {mode : NFA.Unchecked.EatMode} (states : Array NFA.Unchecked.State) (h : mode.nextOf < states.size) :

(NFA.Unchecked.State.Eat mode 0).nextOf ≤ states.size

source

theorem Compiler.Lemmas.add_eat_spec (mode : NFA.Unchecked.EatMode) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ mode.nextOf < states.size⌝⦄ Code.add_eat mode ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_change_state_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_change_state_lift_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ liftM Code.add_change_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.add_remove_state_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_remove_state ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_next_char_spec (offset : Nat) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.add_next_char offset ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.add_next_char_lift_spec (offset : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.add_next_char offset) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_empty_spec (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.c_empty_lift_spec (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM Code.c_empty ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[simp]

theorem Compiler.Lemmas.transition_lt_of_lt (states : Array NFA.Unchecked.State) (trans : Array NFA.Unchecked.Transition) (h : ∀ (i : Nat) (x : i < trans.size), trans[i].next ≤ states.size) :

(NFA.Unchecked.State.SparseTransitions trans).nextOf ≤ states.size

source

theorem Compiler.Lemmas.add_sparse_spec (trans : Array NFA.Unchecked.Transition) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states ∧ ∀ (i : Nat) (x : i < trans.size), trans[i].next ≤ states.size⌝⦄ Code.add_sparse trans ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.c_unicode_class_spec (cls : Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_unicode_class cls ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.c_unicode_class_lift_spec (cls : Syntax.ClassUnicode) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_unicode_class cls) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_literal_spec (c : Char) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_literal c ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.c_literal_lift_spec (c : Char) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_literal c) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_look_spec (look : Syntax.Look) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_look look ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, ())⦄

source

theorem Compiler.Lemmas.c_look_lift_spec (look : Syntax.Look) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_look look) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_possessive_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states⌝⦄ Code.c_possessive tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_possessive_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.tref_le_of_lt_spec {captures : Array NFA.Capture} (states : Array NFA.Unchecked.State) (tref : ThompsonRef) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states tref s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝⦄ EStateM.pure tref ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_possessive_le_lift_spec (tref : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tref.start < states.size ∧ tref.end < states.size ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_possessive tref) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_cap'_start_spec (group slot : Nat) (isValid : NFA.Capture.IsValid NFA.Capture.Role.Start group slot) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_cap' NFA.Capture.Role.Start group slot isValid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst ∧ { role := NFA.Capture.Role.Start, group := group, slot := slot, isValid := isValid } ∈ s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_cap'_end_spec (group slot : Nat) (isValid : NFA.Capture.IsValid NFA.Capture.Role.End group slot) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) (h : ∃ (c : NFA.Capture ), c ∈ captures ∧ c.role = NFA.Capture.Role.Start ∧ c.group = group) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_cap' NFA.Capture.Role.End group slot isValid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_back_ref_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_back_ref case_insensitive n ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_back_ref_lift_spec (case_insensitive : Bool) (n : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_back_ref case_insensitive n) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_PositiveLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_PositiveLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_PositiveLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_NegativeLookahead compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_NegativeLookahead_lift_spec (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_NegativeLookahead compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_PositiveLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_PositiveLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_PositiveLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_lookaround_NegativeLookbehind next_char compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_lookaround_NegativeLookbehind_lift_spec (next_char : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ next_char < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_lookaround_NegativeLookbehind next_char compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_some_1_false_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_some_1_false union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_some_1_false_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_some_1_false union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_some_1_true_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_some_1_true union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_some_1_true_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_some_1_true union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_none_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_repetition_0_none union compiled ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_repetition_0_none_lift_spec (union : NFA.Unchecked.StateID) (compiled : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_repetition_0_none union compiled) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.greedy_union_spec (greedy : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ if greedy = true then liftM Code.add_union else liftM Code.add_union_reverse ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_0_pre_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_at_least_0_pre compiled greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_0_pre_lift_spec (compiled : ThompsonRef) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_0_pre compiled greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_set_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) {groups : Array Nat} :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ s.snd.snd = groups⌝⦄ Code.c_at_least_set possible_empty_capture_group greedy ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜states = s.fst ∧ groups.size ≤ s.snd.snd.size⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_0_post_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ plus < states.size ∧ compiled.start < states.size ∧ nextOfLt states⌝⦄ Code.c_at_least_0_post compiled plus greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_0_post_lift_spec (compiled : ThompsonRef) (plus : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ plus < states.size ∧ compiled.start < states.size ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_0_post compiled plus greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_0_spec (compiled : ThompsonRef) (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ tRefLt compiled states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_at_least_0 compiled possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_1_pre_spec (greedy : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_at_least_1_pre greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_1_pre_lift_spec (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_1_pre greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_1_post_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states⌝⦄ Code.c_at_least_1_post compiled union possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_1_post_lift_spec (compiled : ThompsonRef) (union : NFA.Unchecked.StateID) (possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ union < states.size ∧ tRefLt compiled states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_1_post compiled union possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_1_spec (possible_empty_capture_group : Option Nat) (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_at_least_1 possible_empty_capture_group greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_2_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ nextOfLt states⌝⦄ Code.c_at_least_2 «prefix» last greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_at_least_2_lift_spec («prefix» last : ThompsonRef) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt «prefix» states ∧ tRefLt last states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_at_least_2 «prefix» last greedy possessive) ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLeLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_bounded.fold.patch.pre_spec (compiled : ThompsonRef) (prev_end : NFA.Unchecked.StateID) (greedy : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.pre compiled prev_end greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_bounded.fold.patch.possessive_spec (compiled : ThompsonRef) (empty : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.possessive compiled empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_bounded.fold.patch.post_spec (compiled : ThompsonRef) (union empty : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ compiled.end < states.size ∧ union < states.size ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch.post compiled union empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_bounded.fold.patch_spec (compiled : ThompsonRef) (prev_end empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ empty < states.size ∧ nextOfLt states⌝⦄ Code.c_bounded.fold.patch compiled prev_end empty greedy possessive ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_bounded.fold.patch_lift_spec (compiled : ThompsonRef) (prev_end empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt compiled states ∧ prev_end < states.size ∧ empty < states.size ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_bounded.fold.patch compiled prev_end empty greedy possessive) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_alt_iter_step_spec (first second : ThompsonRef) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ tRefLt first states ∧ tRefLt second states ∧ nextOfLt states⌝⦄ Code.c_alt_iter_step first second ⦃(fun (r : NFA.Unchecked.StateID × NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜tRefNextOfLt states { start := r.fst, «end» := r.snd } s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_alt_iter_step_lift_spec (first second : ThompsonRef) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ tRefLt first states ∧ tRefLt second states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_alt_iter_step first second) ⦃(fun (r : NFA.Unchecked.StateID × NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states { start := r.fst, «end» := r.snd } s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_rep_pre_spec (greedy : Bool) (states : Array NFA.Unchecked.State) :

⦃fun (s : Array NFA.Unchecked.State) => ⌜s = states ∧ nextOfLt states⌝⦄ Code.c_rep_pre greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_rep_pre_lift_spec (greedy : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ liftM (Code.c_rep_pre greedy) ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLt states r s.fst ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_concat_fold_spec (tail : Array Syntax.Hir) (sid : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ sid < states.size ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_concat.fold tail sid ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_concat_spec (hirs : Array Syntax.Hir) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜(s.fst = states ∧ nextOfLt states) ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_concat hirs ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_alt_iter_fold_spec (hirs : Array Syntax.Hir) (union «end» : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ union < states.size ∧ «end» < states.size ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_alt_iter.fold hirs union «end» ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜statesNextOfLeLt states s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_alt_iter_spec (hirs : Array Syntax.Hir) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_alt_iter hirs ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_exactly_fold_spec (hir : Syntax.Hir) (n : Nat) («end» : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ «end» < states.size ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_exactly.fold hir n «end» ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_exactly_spec (hir : Syntax.Hir) (n : Nat) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_exactly hir n ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_at_least_spec (hir : Syntax.Hir) (n : Nat) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_at_least hir n greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_bounded_fold_spec (hir : Syntax.Hir) (n : Nat) («prefix» : ThompsonRef) (empty : NFA.Unchecked.StateID) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ tRefLt «prefix» states ∧ empty < states.size ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_bounded.fold hir n «prefix» empty greedy possessive ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜stateIdNextOfLeLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_bounded_spec (hir : Syntax.Hir) (min max : Nat) (greedy possessive : Bool) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_bounded hir min max greedy possessive ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_lookaround_spec (look : Syntax.Lookaround) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_lookaround look ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_repetition_spec (rep : Syntax.Repetition) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_repetition rep ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_cap_spec (hir : Syntax.Capture) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c_cap hir ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_spec (hir : Syntax.Hir) (states : Array NFA.Unchecked.State) (captures : Array NFA.Capture) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst = states ∧ nextOfLt states ∧ s.snd.fst = captures ∧ cValid captures⌝⦄ Code.c hir ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_init_spec (anchored : Bool) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst.size = 0 ∧ s.snd.fst.size = 0⌝⦄ Code.init anchored ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefLt r s.fst ∧ nextOfLt s.fst ∧ cValid s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.c_compile_spec (anchored : Bool) (hir : Syntax.Hir) :

⦃fun (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜s.fst.size = 0 ∧ s.snd.fst.size = 0⌝⦄ Code.compile anchored hir ⦃(fun (x : Unit) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜nextOfLt s.fst ∧ cValid s.snd.fst⌝, fun (x : String) => ⌜True ⌝, ())⦄

source

theorem Compiler.Lemmas.compile_nextOf_lt {states : Array NFA.Unchecked.State} {captures : Array NFA.Capture} {groups : Array Nat} {anchored : Bool} {expr : Syntax.Hir} (h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups)) :

nextOfLt states

source

theorem Compiler.Lemmas.compile_captures_valid {states : Array NFA.Unchecked.State} {captures : Array NFA.Capture} {groups : Array Nat} {anchored : Bool} {expr : Syntax.Hir} (h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups)) :

NFA.Capture.valid captures