~/jendhub

def nfa.step

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:2934

import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-apparmor@0.1.0.0/text.bend as X
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

2934# one byte: the positions after it accept t exactly when, before it, the
2935# positions (with the carried ones) accept h then t
2936def nfa.step(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +cin: Bool, +ain: Bool, +h: U32, +t: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.next(seq, bs, cin, ain, h), t) == Bool.or(Bool.and(ain, G.AaGSeq.matches(seq, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(seq, Con{h, t})), G.AaGNfa.sem(seq, bs, Con{h, t}))) : Bool}:
2937  match seq:
2938    case Nil{}:
2939      nfa.taut_nil(ain, X.AaText.is_nil(t), cin, G.AaGNfa.hd(bs))
2940    case Con{tok, r}:
2941      match tok:
2942        case G.AaGChar{c}:
2943          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGChar{c}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGChar{c}, r}, bs, Con{h, t}))) : Bool}
2944          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, U32.is_eq(h, c), G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
2945        case G.AaGAny{}:
2946          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGAny{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGAny{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGAny{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGAny{}, r}, bs, Con{h, t}))) : Bool}
2947          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGAny{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
2948        case G.AaGClass{n, rs}:
2949          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGClass{n, rs}, r}, bs, Con{h, t}))) : Bool}
2950          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, G.AaGClass.has(n, rs, h), G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
2951        case G.AaGStar{}:
2952          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), ain), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGStar{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGStar{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGStar{}, r}, bs, Con{h, t}))) : Bool}
2953          nfa.taut_star(G.AaGNfa.hd(bs), cin, ain, U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
2954        case G.AaGStar2{}:
2955          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), ain), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGStar2{}, r}, bs, Con{h, t}))) : Bool}
2956          nfa.taut_star2(G.AaGNfa.hd(bs), cin, ain, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))

Uses (20)

Used by (1)