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
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
@[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⌝, ())⦄
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⌝, ())⦄
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
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