Regex.Compiler.Lemmas.Compile

Lemmas #

Proof that Compiler.Code.compile gives an array with the Compiler.NextOfLt and Capture.Valid property and has no exceptions

c_compile_spec: main result

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 ∧ patchAssignable states prev_end⌝⦄ Code.c_bounded.fold.patch.pre compiled prev_end greedy ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states compiled.end⌝⦄ Code.c_bounded.fold.patch.possessive compiled empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states union ∧ patchAssignable states compiled.end⌝⦄ Code.c_bounded.fold.patch.post compiled union empty ⦃(fun (r : NFA.Unchecked.StateID) (s : Array NFA.Unchecked.State) => ⌜stateIdNextOfLeLt states r s ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states prev_end ∧ patchAssignable states compiled.end⌝⦄ 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 ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states prev_end ∧ patchAssignable states compiled.end) ∧ 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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states first.end ∧ patchAssignable states second.end⌝⦄ 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 ∧ assignableIf states s ∧ patchAssignable s r.fst ∧ patchAssignable s r.snd⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states first.end ∧ patchAssignable states second.end) ∧ 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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.fst ∧ patchAssignable s.fst r.snd) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s ∧ patchAssignable s r⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r) ∧ s.snd.fst = captures ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

source

@[simp]

theorem Compiler.Lemmas.cMemAndValid_iff (prev caps : Array NFA.Capture) :

cMemAndValid prev caps ↔ (∀ (a : NFA.Capture), a ∈ prev → a ∈ caps) ∧ NFA.Capture.Valid caps

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 ∧ patchAssignable states union ∧ 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 ∧ assignableIf states s.fst ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states sid) ∧ 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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

source

@[irreducible]

theorem Compiler.Lemmas.c_alt_iter_spec (alt : Syntax.Alternation) (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 alt ⦃(fun (r : ThompsonRef) (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat) => ⌜tRefNextOfLt states r s.fst ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states «end» ∧ 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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable states «prefix».end ∧ 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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ assignableIf states s.fst ∧ patchAssignable s.fst r.end ∧ cMemAndValid captures s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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 ∧ patchAssignable s.fst r.end ∧ cValid s.snd.fst⌝, fun (x : String) => ⌜False ⌝, PUnit.unit )⦄

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) => ⌜False ⌝, PUnit.unit )⦄

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

source

theorem Compiler.Lemmas.compile_eq_ok {anchored : Bool} {expr : Syntax.Hir} :

∃ (s : Array NFA.Unchecked.State × Array NFA.Capture × Array Nat), Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () s