PROOF.bend
bend-osdev-apparmor@0.1.0.0 · 3,947 lines · 121 definitions
1import Base
2import bend-osdev-apparmor@0.1.0.0/text.bend as X
3import bend-osdev-apparmor@0.1.0.0/glob.bend as G
4import bend-osdev-apparmor@0.1.0.0/perm.bend as P
5import bend-osdev-apparmor@0.1.0.0/options.bend as O
6import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
7import bend-osdev-apparmor@0.1.0.0/eval.bend as V
8import bend-osdev-apparmor@0.1.0.0/transitions.bend as TR
9import bend-osdev-apparmor@0.1.0.0/rule_file.bend as F
10import bend-osdev-apparmor@0.1.0.0/rule_capability.bend as RC
11import bend-osdev-apparmor@0.1.0.0/rule_network.bend as RN
12import bend-osdev-apparmor@0.1.0.0/rule_signal.bend as RS
13import bend-osdev-apparmor@0.1.0.0/rule_ptrace.bend as RP
14import bend-osdev-apparmor@0.1.0.0/rule_mount.bend as RM
15import bend-osdev-apparmor@0.1.0.0/rule_dbus.bend as RD
16import bend-osdev-apparmor@0.1.0.0/rule_change_profile.bend as RX
17import bend-osdev-apparmor@0.1.0.0/LAWS.bend as Laws
18
19
20
21def b.or_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}:
22 match a:
23 case True{}:
24 {==}
25 case False{}:
26 {==}
27
28def b.or_false_r(+a: Bool) -> {Bool.or(a, False{}) == a : Bool}:
29 match a:
30 case True{}:
31 {==}
32 case False{}:
33 {==}
34
35def b.and_false_r(+a: Bool) -> {Bool.and(a, False{}) == False{} : Bool}:
36 match a:
37 case True{}:
38 {==}
39 case False{}:
40 {==}
41
42def b.and_true_r(+a: Bool) -> {Bool.and(a, True{}) == a : Bool}:
43 match a:
44 case True{}:
45 {==}
46 case False{}:
47 {==}
48
49
50def b.factor(+p: Bool, +n: Bool, +f: Bool, +q: Bool) -> {Bool.or(Bool.and(Bool.and(p, n), f), Bool.and(p, q)) == Bool.and(p, Bool.or(Bool.and(n, f), q)) : Bool}:
51 match p:
52 case True{}:
53 {==}
54 case False{}:
55 {==}
56
57
58
59def b.disc(+b: Bool) -> Type:
60 match b:
61 case False{}:
62 Unit
63 case True{}:
64 Empty
65
66def b.ft(+e: {False{} == True{} : Bool}) -> b.disc(True{}):
67 %e : b.disc(_)
68 Unit{}
69
70def b.absurd(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}:
71 Empty.absurd({x == y : T}, b.ft(e))
72
73def b.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}:
74 Empty.absurd({x == y : T}, b.ft(Equal.sym(Bool, True{}, False{}, e)))
75
76
77def fe(+r: List<&2, G.AaGTok>, d: List<&2, List<&2, U32>>) -> Bool:
78 match d:
79 case Nil{}:
80 False{}
81 case Con{p, ps}:
82 Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps))
83
84def fe_any(+r: List<&2, G.AaGTok>, ds: List<&2, List<&2, List<&2, U32>>>) -> Bool:
85 match ds:
86 case Nil{}:
87 False{}
88 case Con{d, t}:
89 Bool.or(fe(r, d), fe_any(r, t))
90
91def fa_app(+seq: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(seq, G.AaGCuts.append(xs, ys)) == Bool.or(G.AaGSeq.fits_any(seq, xs), G.AaGSeq.fits_any(seq, ys)) : Bool}:
92 match xs:
93 case Nil{}:
94 {==}
95 case Con{d, t}:
96 %Equal.sym(Bool, G.AaGSeq.fits_any(seq, G.AaGCuts.append(t, ys)), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)), fa_app(seq, t, ys)) : {Bool.or(G.AaGSeq.fits(seq, d), _) == Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)) : Bool}
97 Equal.sym(Bool, Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)), Bool.or(G.AaGSeq.fits(seq, d), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys))), b.or_assoc(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)))
98
99def fe_app(+r: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.append(xs, ys)) == Bool.or(fe_any(r, xs), fe_any(r, ys)) : Bool}:
100 match xs:
101 case Nil{}:
102 {==}
103 case Con{d, t}:
104 %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(t, ys)), Bool.or(fe_any(r, t), fe_any(r, ys)), fe_app(r, t, ys)) : {Bool.or(fe(r, d), _) == Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)) : Bool}
105 Equal.sym(Bool, Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)), Bool.or(fe(r, d), Bool.or(fe_any(r, t), fe_any(r, ys))), b.or_assoc(fe(r, d), fe_any(r, t), fe_any(r, ys)))
106
107
108def ef_char(+c: U32, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
109 match ds:
110 case Nil{}:
111 {==}
112 case Con{d, t}:
113 ef_char(c, r, t)
114
115def ef_any(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
116 match ds:
117 case Nil{}:
118 {==}
119 case Con{d, t}:
120 ef_any(r, t)
121
122def ef_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
123 match ds:
124 case Nil{}:
125 {==}
126 case Con{d, t}:
127 ef_class(n, rs, r, t)
128
129
130def ef_star(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
131 match ds:
132 case Nil{}:
133 {==}
134 case Con{d, t}:
135 %ef_star(r, t) : {Bool.or(G.AaGSeq.fits(r, d), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
136 {==}
137
138def ef_star2(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
139 match ds:
140 case Nil{}:
141 {==}
142 case Con{d, t}:
143 %ef_star2(r, t) : {Bool.or(G.AaGSeq.fits(r, d), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
144 {==}
145
146
147
148def gr_char(+c: U32, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_eq(h, c), fe_any(r, ds)) : Bool}:
149 match ds:
150 case Nil{}:
151 Equal.sym(Bool, Bool.and(U32.is_eq(h, c), False{}), False{}, b.and_false_r(U32.is_eq(h, c)))
152 case Con{d, t}:
153 match d:
154 case Nil{}:
155 gr_char(c, r, h, t)
156 case Con{p, ps}:
157 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_eq(h, c), fe_any(r, t)), gr_char(c, r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_eq(h, c), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_eq(h, c), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
158 b.factor(U32.is_eq(h, c), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
159
160def gr_any(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), fe_any(r, ds)) : Bool}:
161 match ds:
162 case Nil{}:
163 Equal.sym(Bool, Bool.and(U32.is_ne(h, 47), False{}), False{}, b.and_false_r(U32.is_ne(h, 47)))
164 case Con{d, t}:
165 match d:
166 case Nil{}:
167 gr_any(r, h, t)
168 case Con{p, ps}:
169 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_ne(h, 47), fe_any(r, t)), gr_any(r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_ne(h, 47), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_ne(h, 47), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
170 b.factor(U32.is_ne(h, 47), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
171
172def gr_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, ds)) : Bool}:
173 match ds:
174 case Nil{}:
175 Equal.sym(Bool, Bool.and(G.AaGClass.has(n, rs, h), False{}), False{}, b.and_false_r(G.AaGClass.has(n, rs, h)))
176 case Con{d, t}:
177 match d:
178 case Nil{}:
179 gr_class(n, rs, r, h, t)
180 case Con{p, ps}:
181 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, t)), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, t)), gr_class(n, rs, r, h, t)) : {Bool.or(Bool.and(Bool.and(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(G.AaGClass.has(n, rs, h), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
182 b.factor(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
183
184
185def gr_star(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, ds)) : Bool}:
186 match ds:
187 case Nil{}:
188 Equal.sym(Bool, Bool.and(U32.is_ne(h, 47), False{}), False{}, b.and_false_r(U32.is_ne(h, 47)))
189 case Con{d, t}:
190 match d:
191 case Nil{}:
192 gr_star(r, h, t)
193 case Con{p, ps}:
194 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t)), gr_star(r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_ne(h, 47), G.AaGPiece.no_slash(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_ne(h, 47), Bool.or(Bool.and(G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps)), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))) : Bool}
195 b.factor(U32.is_ne(h, 47), G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))
196
197
198def gr_star2(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, ds)) == G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, ds) : Bool}:
199 match ds:
200 case Nil{}:
201 {==}
202 case Con{d, t}:
203 match d:
204 case Nil{}:
205 gr_star2(r, h, t)
206 case Con{p, ps}:
207 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, t)), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t), gr_star2(r, h, t)) : {Bool.or(G.AaGSeq.fits(r, ps), _) == Bool.or(G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t)) : Bool}
208 {==}
209
210
211def fe_ef(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
212 match ds:
213 case Nil{}:
214 {==}
215 case Con{d, t}:
216 %fe_ef(r, t) : {Bool.or(G.AaGSeq.fits(r, d), fe_any(r, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
217 {==}
218
219def fe_gr(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.grow(h, ds)) == False{} : Bool}:
220 match ds:
221 case Nil{}:
222 {==}
223 case Con{d, t}:
224 match d:
225 case Nil{}:
226 fe_gr(r, h, t)
227 case Con{p, ps}:
228 fe_gr(r, h, t)
229
230def fe_cuts(+r: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), s)) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), s)) : Bool}:
231 match s:
232 case Nil{}:
233 fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))
234 case Con{h, t}:
235 %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fe_app(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {_ == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
236 %Equal.sym(Bool, fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(_, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
237 %Equal.sym(Bool, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), False{}, fe_gr(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
238 b.or_false_r(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})))
239
240
241
242def glob.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}:
243 match seq:
244 case Nil{}:
245 match s:
246 case Nil{}:
247 {==}
248 case Con{h, t}:
249 {==}
250 case Con{tok, r}:
251 match tok:
252 case G.AaGChar{c}:
253 match s:
254 case Nil{}:
255 Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
256 case Con{h, t}:
257 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == _ : Bool}
258 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
259 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_eq(h, c), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_char(c, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
260 %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
261 %glob.thm(r, t) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
262 {==}
263 case G.AaGAny{}:
264 match s:
265 case Nil{}:
266 Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
267 case Con{h, t}:
268 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == _ : Bool}
269 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
270 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_any(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
271 %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
272 %glob.thm(r, t) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
273 {==}
274 case G.AaGClass{n, rs}:
275 match s:
276 case Nil{}:
277 Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
278 case Con{h, t}:
279 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == _ : Bool}
280 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
281 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_class(n, rs, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
282 %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
283 %glob.thm(r, t) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
284 {==}
285 case G.AaGStar{}:
286 match s:
287 case Nil{}:
288 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
289 glob.thm(r, Nil{})
290 case Con{h, t}:
291 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == _ : Bool}
292 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
293 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_star(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
294 %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
295 %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), _)) : Bool}
296 {==}
297 case G.AaGStar2{}:
298 match s:
299 case Nil{}:
300 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
301 glob.thm(r, Nil{})
302 case Con{h, t}:
303 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == _ : Bool}
304 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
305 %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), gr_star2(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
306 %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : Bool}
307 %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), _) : Bool}
308 {==}
309
310
311
312
313
314def nfa.taut_nil(+a: Bool, +n: Bool, +c: Bool, +b: Bool) -> {Bool.and(a, n) == Bool.or(Bool.and(a, n), Bool.or(Bool.and(c, False{}), Bool.and(b, False{}))) : Bool}:
315 match a:
316 case True{}:
317 match n:
318 case True{}:
319 match c:
320 case True{}:
321 match b:
322 case True{}:
323 {==}
324 case False{}:
325 {==}
326 case False{}:
327 match b:
328 case True{}:
329 {==}
330 case False{}:
331 {==}
332 case False{}:
333 match c:
334 case True{}:
335 match b:
336 case True{}:
337 {==}
338 case False{}:
339 {==}
340 case False{}:
341 match b:
342 case True{}:
343 {==}
344 case False{}:
345 {==}
346 case False{}:
347 match n:
348 case True{}:
349 match c:
350 case True{}:
351 match b:
352 case True{}:
353 {==}
354 case False{}:
355 {==}
356 case False{}:
357 match b:
358 case True{}:
359 {==}
360 case False{}:
361 {==}
362 case False{}:
363 match c:
364 case True{}:
365 match b:
366 case True{}:
367 {==}
368 case False{}:
369 {==}
370 case False{}:
371 match b:
372 case True{}:
373 {==}
374 case False{}:
375 {==}
376
377def nfa.taut_adv(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), False{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), e), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.and(e, q)), Bool.or(Bool.and(hb, Bool.and(e, q)), z))) : Bool}:
378 match hb:
379 case True{}:
380 match cin:
381 case True{}:
382 match ain:
383 case True{}:
384 match e:
385 case True{}:
386 match p:
387 case True{}:
388 match q:
389 case True{}:
390 match r:
391 case True{}:
392 match z:
393 case True{}:
394 {==}
395 case False{}:
396 {==}
397 case False{}:
398 match z:
399 case True{}:
400 {==}
401 case False{}:
402 {==}
403 case False{}:
404 match r:
405 case True{}:
406 match z:
407 case True{}:
408 {==}
409 case False{}:
410 {==}
411 case False{}:
412 match z:
413 case True{}:
414 {==}
415 case False{}:
416 {==}
417 case False{}:
418 match q:
419 case True{}:
420 match r:
421 case True{}:
422 match z:
423 case True{}:
424 {==}
425 case False{}:
426 {==}
427 case False{}:
428 match z:
429 case True{}:
430 {==}
431 case False{}:
432 {==}
433 case False{}:
434 match r:
435 case True{}:
436 match z:
437 case True{}:
438 {==}
439 case False{}:
440 {==}
441 case False{}:
442 match z:
443 case True{}:
444 {==}
445 case False{}:
446 {==}
447 case False{}:
448 match p:
449 case True{}:
450 match q:
451 case True{}:
452 match r:
453 case True{}:
454 match z:
455 case True{}:
456 {==}
457 case False{}:
458 {==}
459 case False{}:
460 match z:
461 case True{}:
462 {==}
463 case False{}:
464 {==}
465 case False{}:
466 match r:
467 case True{}:
468 match z:
469 case True{}:
470 {==}
471 case False{}:
472 {==}
473 case False{}:
474 match z:
475 case True{}:
476 {==}
477 case False{}:
478 {==}
479 case False{}:
480 match q:
481 case True{}:
482 match r:
483 case True{}:
484 match z:
485 case True{}:
486 {==}
487 case False{}:
488 {==}
489 case False{}:
490 match z:
491 case True{}:
492 {==}
493 case False{}:
494 {==}
495 case False{}:
496 match r:
497 case True{}:
498 match z:
499 case True{}:
500 {==}
501 case False{}:
502 {==}
503 case False{}:
504 match z:
505 case True{}:
506 {==}
507 case False{}:
508 {==}
509 case False{}:
510 match e:
511 case True{}:
512 match p:
513 case True{}:
514 match q:
515 case True{}:
516 match r:
517 case True{}:
518 match z:
519 case True{}:
520 {==}
521 case False{}:
522 {==}
523 case False{}:
524 match z:
525 case True{}:
526 {==}
527 case False{}:
528 {==}
529 case False{}:
530 match r:
531 case True{}:
532 match z:
533 case True{}:
534 {==}
535 case False{}:
536 {==}
537 case False{}:
538 match z:
539 case True{}:
540 {==}
541 case False{}:
542 {==}
543 case False{}:
544 match q:
545 case True{}:
546 match r:
547 case True{}:
548 match z:
549 case True{}:
550 {==}
551 case False{}:
552 {==}
553 case False{}:
554 match z:
555 case True{}:
556 {==}
557 case False{}:
558 {==}
559 case False{}:
560 match r:
561 case True{}:
562 match z:
563 case True{}:
564 {==}
565 case False{}:
566 {==}
567 case False{}:
568 match z:
569 case True{}:
570 {==}
571 case False{}:
572 {==}
573 case False{}:
574 match p:
575 case True{}:
576 match q:
577 case True{}:
578 match r:
579 case True{}:
580 match z:
581 case True{}:
582 {==}
583 case False{}:
584 {==}
585 case False{}:
586 match z:
587 case True{}:
588 {==}
589 case False{}:
590 {==}
591 case False{}:
592 match r:
593 case True{}:
594 match z:
595 case True{}:
596 {==}
597 case False{}:
598 {==}
599 case False{}:
600 match z:
601 case True{}:
602 {==}
603 case False{}:
604 {==}
605 case False{}:
606 match q:
607 case True{}:
608 match r:
609 case True{}:
610 match z:
611 case True{}:
612 {==}
613 case False{}:
614 {==}
615 case False{}:
616 match z:
617 case True{}:
618 {==}
619 case False{}:
620 {==}
621 case False{}:
622 match r:
623 case True{}:
624 match z:
625 case True{}:
626 {==}
627 case False{}:
628 {==}
629 case False{}:
630 match z:
631 case True{}:
632 {==}
633 case False{}:
634 {==}
635 case False{}:
636 match ain:
637 case True{}:
638 match e:
639 case True{}:
640 match p:
641 case True{}:
642 match q:
643 case True{}:
644 match r:
645 case True{}:
646 match z:
647 case True{}:
648 {==}
649 case False{}:
650 {==}
651 case False{}:
652 match z:
653 case True{}:
654 {==}
655 case False{}:
656 {==}
657 case False{}:
658 match r:
659 case True{}:
660 match z:
661 case True{}:
662 {==}
663 case False{}:
664 {==}
665 case False{}:
666 match z:
667 case True{}:
668 {==}
669 case False{}:
670 {==}
671 case False{}:
672 match q:
673 case True{}:
674 match r:
675 case True{}:
676 match z:
677 case True{}:
678 {==}
679 case False{}:
680 {==}
681 case False{}:
682 match z:
683 case True{}:
684 {==}
685 case False{}:
686 {==}
687 case False{}:
688 match r:
689 case True{}:
690 match z:
691 case True{}:
692 {==}
693 case False{}:
694 {==}
695 case False{}:
696 match z:
697 case True{}:
698 {==}
699 case False{}:
700 {==}
701 case False{}:
702 match p:
703 case True{}:
704 match q:
705 case True{}:
706 match r:
707 case True{}:
708 match z:
709 case True{}:
710 {==}
711 case False{}:
712 {==}
713 case False{}:
714 match z:
715 case True{}:
716 {==}
717 case False{}:
718 {==}
719 case False{}:
720 match r:
721 case True{}:
722 match z:
723 case True{}:
724 {==}
725 case False{}:
726 {==}
727 case False{}:
728 match z:
729 case True{}:
730 {==}
731 case False{}:
732 {==}
733 case False{}:
734 match q:
735 case True{}:
736 match r:
737 case True{}:
738 match z:
739 case True{}:
740 {==}
741 case False{}:
742 {==}
743 case False{}:
744 match z:
745 case True{}:
746 {==}
747 case False{}:
748 {==}
749 case False{}:
750 match r:
751 case True{}:
752 match z:
753 case True{}:
754 {==}
755 case False{}:
756 {==}
757 case False{}:
758 match z:
759 case True{}:
760 {==}
761 case False{}:
762 {==}
763 case False{}:
764 match e:
765 case True{}:
766 match p:
767 case True{}:
768 match q:
769 case True{}:
770 match r:
771 case True{}:
772 match z:
773 case True{}:
774 {==}
775 case False{}:
776 {==}
777 case False{}:
778 match z:
779 case True{}:
780 {==}
781 case False{}:
782 {==}
783 case False{}:
784 match r:
785 case True{}:
786 match z:
787 case True{}:
788 {==}
789 case False{}:
790 {==}
791 case False{}:
792 match z:
793 case True{}:
794 {==}
795 case False{}:
796 {==}
797 case False{}:
798 match q:
799 case True{}:
800 match r:
801 case True{}:
802 match z:
803 case True{}:
804 {==}
805 case False{}:
806 {==}
807 case False{}:
808 match z:
809 case True{}:
810 {==}
811 case False{}:
812 {==}
813 case False{}:
814 match r:
815 case True{}:
816 match z:
817 case True{}:
818 {==}
819 case False{}:
820 {==}
821 case False{}:
822 match z:
823 case True{}:
824 {==}
825 case False{}:
826 {==}
827 case False{}:
828 match p:
829 case True{}:
830 match q:
831 case True{}:
832 match r:
833 case True{}:
834 match z:
835 case True{}:
836 {==}
837 case False{}:
838 {==}
839 case False{}:
840 match z:
841 case True{}:
842 {==}
843 case False{}:
844 {==}
845 case False{}:
846 match r:
847 case True{}:
848 match z:
849 case True{}:
850 {==}
851 case False{}:
852 {==}
853 case False{}:
854 match z:
855 case True{}:
856 {==}
857 case False{}:
858 {==}
859 case False{}:
860 match q:
861 case True{}:
862 match r:
863 case True{}:
864 match z:
865 case True{}:
866 {==}
867 case False{}:
868 {==}
869 case False{}:
870 match z:
871 case True{}:
872 {==}
873 case False{}:
874 {==}
875 case False{}:
876 match r:
877 case True{}:
878 match z:
879 case True{}:
880 {==}
881 case False{}:
882 {==}
883 case False{}:
884 match z:
885 case True{}:
886 {==}
887 case False{}:
888 {==}
889 case False{}:
890 match cin:
891 case True{}:
892 match ain:
893 case True{}:
894 match e:
895 case True{}:
896 match p:
897 case True{}:
898 match q:
899 case True{}:
900 match r:
901 case True{}:
902 match z:
903 case True{}:
904 {==}
905 case False{}:
906 {==}
907 case False{}:
908 match z:
909 case True{}:
910 {==}
911 case False{}:
912 {==}
913 case False{}:
914 match r:
915 case True{}:
916 match z:
917 case True{}:
918 {==}
919 case False{}:
920 {==}
921 case False{}:
922 match z:
923 case True{}:
924 {==}
925 case False{}:
926 {==}
927 case False{}:
928 match q:
929 case True{}:
930 match r:
931 case True{}:
932 match z:
933 case True{}:
934 {==}
935 case False{}:
936 {==}
937 case False{}:
938 match z:
939 case True{}:
940 {==}
941 case False{}:
942 {==}
943 case False{}:
944 match r:
945 case True{}:
946 match z:
947 case True{}:
948 {==}
949 case False{}:
950 {==}
951 case False{}:
952 match z:
953 case True{}:
954 {==}
955 case False{}:
956 {==}
957 case False{}:
958 match p:
959 case True{}:
960 match q:
961 case True{}:
962 match r:
963 case True{}:
964 match z:
965 case True{}:
966 {==}
967 case False{}:
968 {==}
969 case False{}:
970 match z:
971 case True{}:
972 {==}
973 case False{}:
974 {==}
975 case False{}:
976 match r:
977 case True{}:
978 match z:
979 case True{}:
980 {==}
981 case False{}:
982 {==}
983 case False{}:
984 match z:
985 case True{}:
986 {==}
987 case False{}:
988 {==}
989 case False{}:
990 match q:
991 case True{}:
992 match r:
993 case True{}:
994 match z:
995 case True{}:
996 {==}
997 case False{}:
998 {==}
999 case False{}:
1000 match z:
1001 case True{}:
1002 {==}
1003 case False{}:
1004 {==}
1005 case False{}:
1006 match r:
1007 case True{}:
1008 match z:
1009 case True{}:
1010 {==}
1011 case False{}:
1012 {==}
1013 case False{}:
1014 match z:
1015 case True{}:
1016 {==}
1017 case False{}:
1018 {==}
1019 case False{}:
1020 match e:
1021 case True{}:
1022 match p:
1023 case True{}:
1024 match q:
1025 case True{}:
1026 match r:
1027 case True{}:
1028 match z:
1029 case True{}:
1030 {==}
1031 case False{}:
1032 {==}
1033 case False{}:
1034 match z:
1035 case True{}:
1036 {==}
1037 case False{}:
1038 {==}
1039 case False{}:
1040 match r:
1041 case True{}:
1042 match z:
1043 case True{}:
1044 {==}
1045 case False{}:
1046 {==}
1047 case False{}:
1048 match z:
1049 case True{}:
1050 {==}
1051 case False{}:
1052 {==}
1053 case False{}:
1054 match q:
1055 case True{}:
1056 match r:
1057 case True{}:
1058 match z:
1059 case True{}:
1060 {==}
1061 case False{}:
1062 {==}
1063 case False{}:
1064 match z:
1065 case True{}:
1066 {==}
1067 case False{}:
1068 {==}
1069 case False{}:
1070 match r:
1071 case True{}:
1072 match z:
1073 case True{}:
1074 {==}
1075 case False{}:
1076 {==}
1077 case False{}:
1078 match z:
1079 case True{}:
1080 {==}
1081 case False{}:
1082 {==}
1083 case False{}:
1084 match p:
1085 case True{}:
1086 match q:
1087 case True{}:
1088 match r:
1089 case True{}:
1090 match z:
1091 case True{}:
1092 {==}
1093 case False{}:
1094 {==}
1095 case False{}:
1096 match z:
1097 case True{}:
1098 {==}
1099 case False{}:
1100 {==}
1101 case False{}:
1102 match r:
1103 case True{}:
1104 match z:
1105 case True{}:
1106 {==}
1107 case False{}:
1108 {==}
1109 case False{}:
1110 match z:
1111 case True{}:
1112 {==}
1113 case False{}:
1114 {==}
1115 case False{}:
1116 match q:
1117 case True{}:
1118 match r:
1119 case True{}:
1120 match z:
1121 case True{}:
1122 {==}
1123 case False{}:
1124 {==}
1125 case False{}:
1126 match z:
1127 case True{}:
1128 {==}
1129 case False{}:
1130 {==}
1131 case False{}:
1132 match r:
1133 case True{}:
1134 match z:
1135 case True{}:
1136 {==}
1137 case False{}:
1138 {==}
1139 case False{}:
1140 match z:
1141 case True{}:
1142 {==}
1143 case False{}:
1144 {==}
1145 case False{}:
1146 match ain:
1147 case True{}:
1148 match e:
1149 case True{}:
1150 match p:
1151 case True{}:
1152 match q:
1153 case True{}:
1154 match r:
1155 case True{}:
1156 match z:
1157 case True{}:
1158 {==}
1159 case False{}:
1160 {==}
1161 case False{}:
1162 match z:
1163 case True{}:
1164 {==}
1165 case False{}:
1166 {==}
1167 case False{}:
1168 match r:
1169 case True{}:
1170 match z:
1171 case True{}:
1172 {==}
1173 case False{}:
1174 {==}
1175 case False{}:
1176 match z:
1177 case True{}:
1178 {==}
1179 case False{}:
1180 {==}
1181 case False{}:
1182 match q:
1183 case True{}:
1184 match r:
1185 case True{}:
1186 match z:
1187 case True{}:
1188 {==}
1189 case False{}:
1190 {==}
1191 case False{}:
1192 match z:
1193 case True{}:
1194 {==}
1195 case False{}:
1196 {==}
1197 case False{}:
1198 match r:
1199 case True{}:
1200 match z:
1201 case True{}:
1202 {==}
1203 case False{}:
1204 {==}
1205 case False{}:
1206 match z:
1207 case True{}:
1208 {==}
1209 case False{}:
1210 {==}
1211 case False{}:
1212 match p:
1213 case True{}:
1214 match q:
1215 case True{}:
1216 match r:
1217 case True{}:
1218 match z:
1219 case True{}:
1220 {==}
1221 case False{}:
1222 {==}
1223 case False{}:
1224 match z:
1225 case True{}:
1226 {==}
1227 case False{}:
1228 {==}
1229 case False{}:
1230 match r:
1231 case True{}:
1232 match z:
1233 case True{}:
1234 {==}
1235 case False{}:
1236 {==}
1237 case False{}:
1238 match z:
1239 case True{}:
1240 {==}
1241 case False{}:
1242 {==}
1243 case False{}:
1244 match q:
1245 case True{}:
1246 match r:
1247 case True{}:
1248 match z:
1249 case True{}:
1250 {==}
1251 case False{}:
1252 {==}
1253 case False{}:
1254 match z:
1255 case True{}:
1256 {==}
1257 case False{}:
1258 {==}
1259 case False{}:
1260 match r:
1261 case True{}:
1262 match z:
1263 case True{}:
1264 {==}
1265 case False{}:
1266 {==}
1267 case False{}:
1268 match z:
1269 case True{}:
1270 {==}
1271 case False{}:
1272 {==}
1273 case False{}:
1274 match e:
1275 case True{}:
1276 match p:
1277 case True{}:
1278 match q:
1279 case True{}:
1280 match r:
1281 case True{}:
1282 match z:
1283 case True{}:
1284 {==}
1285 case False{}:
1286 {==}
1287 case False{}:
1288 match z:
1289 case True{}:
1290 {==}
1291 case False{}:
1292 {==}
1293 case False{}:
1294 match r:
1295 case True{}:
1296 match z:
1297 case True{}:
1298 {==}
1299 case False{}:
1300 {==}
1301 case False{}:
1302 match z:
1303 case True{}:
1304 {==}
1305 case False{}:
1306 {==}
1307 case False{}:
1308 match q:
1309 case True{}:
1310 match r:
1311 case True{}:
1312 match z:
1313 case True{}:
1314 {==}
1315 case False{}:
1316 {==}
1317 case False{}:
1318 match z:
1319 case True{}:
1320 {==}
1321 case False{}:
1322 {==}
1323 case False{}:
1324 match r:
1325 case True{}:
1326 match z:
1327 case True{}:
1328 {==}
1329 case False{}:
1330 {==}
1331 case False{}:
1332 match z:
1333 case True{}:
1334 {==}
1335 case False{}:
1336 {==}
1337 case False{}:
1338 match p:
1339 case True{}:
1340 match q:
1341 case True{}:
1342 match r:
1343 case True{}:
1344 match z:
1345 case True{}:
1346 {==}
1347 case False{}:
1348 {==}
1349 case False{}:
1350 match z:
1351 case True{}:
1352 {==}
1353 case False{}:
1354 {==}
1355 case False{}:
1356 match r:
1357 case True{}:
1358 match z:
1359 case True{}:
1360 {==}
1361 case False{}:
1362 {==}
1363 case False{}:
1364 match z:
1365 case True{}:
1366 {==}
1367 case False{}:
1368 {==}
1369 case False{}:
1370 match q:
1371 case True{}:
1372 match r:
1373 case True{}:
1374 match z:
1375 case True{}:
1376 {==}
1377 case False{}:
1378 {==}
1379 case False{}:
1380 match z:
1381 case True{}:
1382 {==}
1383 case False{}:
1384 {==}
1385 case False{}:
1386 match r:
1387 case True{}:
1388 match z:
1389 case True{}:
1390 {==}
1391 case False{}:
1392 {==}
1393 case False{}:
1394 match z:
1395 case True{}:
1396 {==}
1397 case False{}:
1398 {==}
1399
1400def nfa.taut_star(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), e), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, Bool.and(e, p))), Bool.or(Bool.and(hb, Bool.or(r, Bool.and(e, p))), z))) : Bool}:
1401 match hb:
1402 case True{}:
1403 match cin:
1404 case True{}:
1405 match ain:
1406 case True{}:
1407 match e:
1408 case True{}:
1409 match p:
1410 case True{}:
1411 match q:
1412 case True{}:
1413 match r:
1414 case True{}:
1415 match z:
1416 case True{}:
1417 {==}
1418 case False{}:
1419 {==}
1420 case False{}:
1421 match z:
1422 case True{}:
1423 {==}
1424 case False{}:
1425 {==}
1426 case False{}:
1427 match r:
1428 case True{}:
1429 match z:
1430 case True{}:
1431 {==}
1432 case False{}:
1433 {==}
1434 case False{}:
1435 match z:
1436 case True{}:
1437 {==}
1438 case False{}:
1439 {==}
1440 case False{}:
1441 match q:
1442 case True{}:
1443 match r:
1444 case True{}:
1445 match z:
1446 case True{}:
1447 {==}
1448 case False{}:
1449 {==}
1450 case False{}:
1451 match z:
1452 case True{}:
1453 {==}
1454 case False{}:
1455 {==}
1456 case False{}:
1457 match r:
1458 case True{}:
1459 match z:
1460 case True{}:
1461 {==}
1462 case False{}:
1463 {==}
1464 case False{}:
1465 match z:
1466 case True{}:
1467 {==}
1468 case False{}:
1469 {==}
1470 case False{}:
1471 match p:
1472 case True{}:
1473 match q:
1474 case True{}:
1475 match r:
1476 case True{}:
1477 match z:
1478 case True{}:
1479 {==}
1480 case False{}:
1481 {==}
1482 case False{}:
1483 match z:
1484 case True{}:
1485 {==}
1486 case False{}:
1487 {==}
1488 case False{}:
1489 match r:
1490 case True{}:
1491 match z:
1492 case True{}:
1493 {==}
1494 case False{}:
1495 {==}
1496 case False{}:
1497 match z:
1498 case True{}:
1499 {==}
1500 case False{}:
1501 {==}
1502 case False{}:
1503 match q:
1504 case True{}:
1505 match r:
1506 case True{}:
1507 match z:
1508 case True{}:
1509 {==}
1510 case False{}:
1511 {==}
1512 case False{}:
1513 match z:
1514 case True{}:
1515 {==}
1516 case False{}:
1517 {==}
1518 case False{}:
1519 match r:
1520 case True{}:
1521 match z:
1522 case True{}:
1523 {==}
1524 case False{}:
1525 {==}
1526 case False{}:
1527 match z:
1528 case True{}:
1529 {==}
1530 case False{}:
1531 {==}
1532 case False{}:
1533 match e:
1534 case True{}:
1535 match p:
1536 case True{}:
1537 match q:
1538 case True{}:
1539 match r:
1540 case True{}:
1541 match z:
1542 case True{}:
1543 {==}
1544 case False{}:
1545 {==}
1546 case False{}:
1547 match z:
1548 case True{}:
1549 {==}
1550 case False{}:
1551 {==}
1552 case False{}:
1553 match r:
1554 case True{}:
1555 match z:
1556 case True{}:
1557 {==}
1558 case False{}:
1559 {==}
1560 case False{}:
1561 match z:
1562 case True{}:
1563 {==}
1564 case False{}:
1565 {==}
1566 case False{}:
1567 match q:
1568 case True{}:
1569 match r:
1570 case True{}:
1571 match z:
1572 case True{}:
1573 {==}
1574 case False{}:
1575 {==}
1576 case False{}:
1577 match z:
1578 case True{}:
1579 {==}
1580 case False{}:
1581 {==}
1582 case False{}:
1583 match r:
1584 case True{}:
1585 match z:
1586 case True{}:
1587 {==}
1588 case False{}:
1589 {==}
1590 case False{}:
1591 match z:
1592 case True{}:
1593 {==}
1594 case False{}:
1595 {==}
1596 case False{}:
1597 match p:
1598 case True{}:
1599 match q:
1600 case True{}:
1601 match r:
1602 case True{}:
1603 match z:
1604 case True{}:
1605 {==}
1606 case False{}:
1607 {==}
1608 case False{}:
1609 match z:
1610 case True{}:
1611 {==}
1612 case False{}:
1613 {==}
1614 case False{}:
1615 match r:
1616 case True{}:
1617 match z:
1618 case True{}:
1619 {==}
1620 case False{}:
1621 {==}
1622 case False{}:
1623 match z:
1624 case True{}:
1625 {==}
1626 case False{}:
1627 {==}
1628 case False{}:
1629 match q:
1630 case True{}:
1631 match r:
1632 case True{}:
1633 match z:
1634 case True{}:
1635 {==}
1636 case False{}:
1637 {==}
1638 case False{}:
1639 match z:
1640 case True{}:
1641 {==}
1642 case False{}:
1643 {==}
1644 case False{}:
1645 match r:
1646 case True{}:
1647 match z:
1648 case True{}:
1649 {==}
1650 case False{}:
1651 {==}
1652 case False{}:
1653 match z:
1654 case True{}:
1655 {==}
1656 case False{}:
1657 {==}
1658 case False{}:
1659 match ain:
1660 case True{}:
1661 match e:
1662 case True{}:
1663 match p:
1664 case True{}:
1665 match q:
1666 case True{}:
1667 match r:
1668 case True{}:
1669 match z:
1670 case True{}:
1671 {==}
1672 case False{}:
1673 {==}
1674 case False{}:
1675 match z:
1676 case True{}:
1677 {==}
1678 case False{}:
1679 {==}
1680 case False{}:
1681 match r:
1682 case True{}:
1683 match z:
1684 case True{}:
1685 {==}
1686 case False{}:
1687 {==}
1688 case False{}:
1689 match z:
1690 case True{}:
1691 {==}
1692 case False{}:
1693 {==}
1694 case False{}:
1695 match q:
1696 case True{}:
1697 match r:
1698 case True{}:
1699 match z:
1700 case True{}:
1701 {==}
1702 case False{}:
1703 {==}
1704 case False{}:
1705 match z:
1706 case True{}:
1707 {==}
1708 case False{}:
1709 {==}
1710 case False{}:
1711 match r:
1712 case True{}:
1713 match z:
1714 case True{}:
1715 {==}
1716 case False{}:
1717 {==}
1718 case False{}:
1719 match z:
1720 case True{}:
1721 {==}
1722 case False{}:
1723 {==}
1724 case False{}:
1725 match p:
1726 case True{}:
1727 match q:
1728 case True{}:
1729 match r:
1730 case True{}:
1731 match z:
1732 case True{}:
1733 {==}
1734 case False{}:
1735 {==}
1736 case False{}:
1737 match z:
1738 case True{}:
1739 {==}
1740 case False{}:
1741 {==}
1742 case False{}:
1743 match r:
1744 case True{}:
1745 match z:
1746 case True{}:
1747 {==}
1748 case False{}:
1749 {==}
1750 case False{}:
1751 match z:
1752 case True{}:
1753 {==}
1754 case False{}:
1755 {==}
1756 case False{}:
1757 match q:
1758 case True{}:
1759 match r:
1760 case True{}:
1761 match z:
1762 case True{}:
1763 {==}
1764 case False{}:
1765 {==}
1766 case False{}:
1767 match z:
1768 case True{}:
1769 {==}
1770 case False{}:
1771 {==}
1772 case False{}:
1773 match r:
1774 case True{}:
1775 match z:
1776 case True{}:
1777 {==}
1778 case False{}:
1779 {==}
1780 case False{}:
1781 match z:
1782 case True{}:
1783 {==}
1784 case False{}:
1785 {==}
1786 case False{}:
1787 match e:
1788 case True{}:
1789 match p:
1790 case True{}:
1791 match q:
1792 case True{}:
1793 match r:
1794 case True{}:
1795 match z:
1796 case True{}:
1797 {==}
1798 case False{}:
1799 {==}
1800 case False{}:
1801 match z:
1802 case True{}:
1803 {==}
1804 case False{}:
1805 {==}
1806 case False{}:
1807 match r:
1808 case True{}:
1809 match z:
1810 case True{}:
1811 {==}
1812 case False{}:
1813 {==}
1814 case False{}:
1815 match z:
1816 case True{}:
1817 {==}
1818 case False{}:
1819 {==}
1820 case False{}:
1821 match q:
1822 case True{}:
1823 match r:
1824 case True{}:
1825 match z:
1826 case True{}:
1827 {==}
1828 case False{}:
1829 {==}
1830 case False{}:
1831 match z:
1832 case True{}:
1833 {==}
1834 case False{}:
1835 {==}
1836 case False{}:
1837 match r:
1838 case True{}:
1839 match z:
1840 case True{}:
1841 {==}
1842 case False{}:
1843 {==}
1844 case False{}:
1845 match z:
1846 case True{}:
1847 {==}
1848 case False{}:
1849 {==}
1850 case False{}:
1851 match p:
1852 case True{}:
1853 match q:
1854 case True{}:
1855 match r:
1856 case True{}:
1857 match z:
1858 case True{}:
1859 {==}
1860 case False{}:
1861 {==}
1862 case False{}:
1863 match z:
1864 case True{}:
1865 {==}
1866 case False{}:
1867 {==}
1868 case False{}:
1869 match r:
1870 case True{}:
1871 match z:
1872 case True{}:
1873 {==}
1874 case False{}:
1875 {==}
1876 case False{}:
1877 match z:
1878 case True{}:
1879 {==}
1880 case False{}:
1881 {==}
1882 case False{}:
1883 match q:
1884 case True{}:
1885 match r:
1886 case True{}:
1887 match z:
1888 case True{}:
1889 {==}
1890 case False{}:
1891 {==}
1892 case False{}:
1893 match z:
1894 case True{}:
1895 {==}
1896 case False{}:
1897 {==}
1898 case False{}:
1899 match r:
1900 case True{}:
1901 match z:
1902 case True{}:
1903 {==}
1904 case False{}:
1905 {==}
1906 case False{}:
1907 match z:
1908 case True{}:
1909 {==}
1910 case False{}:
1911 {==}
1912 case False{}:
1913 match cin:
1914 case True{}:
1915 match ain:
1916 case True{}:
1917 match e:
1918 case True{}:
1919 match p:
1920 case True{}:
1921 match q:
1922 case True{}:
1923 match r:
1924 case True{}:
1925 match z:
1926 case True{}:
1927 {==}
1928 case False{}:
1929 {==}
1930 case False{}:
1931 match z:
1932 case True{}:
1933 {==}
1934 case False{}:
1935 {==}
1936 case False{}:
1937 match r:
1938 case True{}:
1939 match z:
1940 case True{}:
1941 {==}
1942 case False{}:
1943 {==}
1944 case False{}:
1945 match z:
1946 case True{}:
1947 {==}
1948 case False{}:
1949 {==}
1950 case False{}:
1951 match q:
1952 case True{}:
1953 match r:
1954 case True{}:
1955 match z:
1956 case True{}:
1957 {==}
1958 case False{}:
1959 {==}
1960 case False{}:
1961 match z:
1962 case True{}:
1963 {==}
1964 case False{}:
1965 {==}
1966 case False{}:
1967 match r:
1968 case True{}:
1969 match z:
1970 case True{}:
1971 {==}
1972 case False{}:
1973 {==}
1974 case False{}:
1975 match z:
1976 case True{}:
1977 {==}
1978 case False{}:
1979 {==}
1980 case False{}:
1981 match p:
1982 case True{}:
1983 match q:
1984 case True{}:
1985 match r:
1986 case True{}:
1987 match z:
1988 case True{}:
1989 {==}
1990 case False{}:
1991 {==}
1992 case False{}:
1993 match z:
1994 case True{}:
1995 {==}
1996 case False{}:
1997 {==}
1998 case False{}:
1999 match r:
2000 case True{}:
2001 match z:
2002 case True{}:
2003 {==}
2004 case False{}:
2005 {==}
2006 case False{}:
2007 match z:
2008 case True{}:
2009 {==}
2010 case False{}:
2011 {==}
2012 case False{}:
2013 match q:
2014 case True{}:
2015 match r:
2016 case True{}:
2017 match z:
2018 case True{}:
2019 {==}
2020 case False{}:
2021 {==}
2022 case False{}:
2023 match z:
2024 case True{}:
2025 {==}
2026 case False{}:
2027 {==}
2028 case False{}:
2029 match r:
2030 case True{}:
2031 match z:
2032 case True{}:
2033 {==}
2034 case False{}:
2035 {==}
2036 case False{}:
2037 match z:
2038 case True{}:
2039 {==}
2040 case False{}:
2041 {==}
2042 case False{}:
2043 match e:
2044 case True{}:
2045 match p:
2046 case True{}:
2047 match q:
2048 case True{}:
2049 match r:
2050 case True{}:
2051 match z:
2052 case True{}:
2053 {==}
2054 case False{}:
2055 {==}
2056 case False{}:
2057 match z:
2058 case True{}:
2059 {==}
2060 case False{}:
2061 {==}
2062 case False{}:
2063 match r:
2064 case True{}:
2065 match z:
2066 case True{}:
2067 {==}
2068 case False{}:
2069 {==}
2070 case False{}:
2071 match z:
2072 case True{}:
2073 {==}
2074 case False{}:
2075 {==}
2076 case False{}:
2077 match q:
2078 case True{}:
2079 match r:
2080 case True{}:
2081 match z:
2082 case True{}:
2083 {==}
2084 case False{}:
2085 {==}
2086 case False{}:
2087 match z:
2088 case True{}:
2089 {==}
2090 case False{}:
2091 {==}
2092 case False{}:
2093 match r:
2094 case True{}:
2095 match z:
2096 case True{}:
2097 {==}
2098 case False{}:
2099 {==}
2100 case False{}:
2101 match z:
2102 case True{}:
2103 {==}
2104 case False{}:
2105 {==}
2106 case False{}:
2107 match p:
2108 case True{}:
2109 match q:
2110 case True{}:
2111 match r:
2112 case True{}:
2113 match z:
2114 case True{}:
2115 {==}
2116 case False{}:
2117 {==}
2118 case False{}:
2119 match z:
2120 case True{}:
2121 {==}
2122 case False{}:
2123 {==}
2124 case False{}:
2125 match r:
2126 case True{}:
2127 match z:
2128 case True{}:
2129 {==}
2130 case False{}:
2131 {==}
2132 case False{}:
2133 match z:
2134 case True{}:
2135 {==}
2136 case False{}:
2137 {==}
2138 case False{}:
2139 match q:
2140 case True{}:
2141 match r:
2142 case True{}:
2143 match z:
2144 case True{}:
2145 {==}
2146 case False{}:
2147 {==}
2148 case False{}:
2149 match z:
2150 case True{}:
2151 {==}
2152 case False{}:
2153 {==}
2154 case False{}:
2155 match r:
2156 case True{}:
2157 match z:
2158 case True{}:
2159 {==}
2160 case False{}:
2161 {==}
2162 case False{}:
2163 match z:
2164 case True{}:
2165 {==}
2166 case False{}:
2167 {==}
2168 case False{}:
2169 match ain:
2170 case True{}:
2171 match e:
2172 case True{}:
2173 match p:
2174 case True{}:
2175 match q:
2176 case True{}:
2177 match r:
2178 case True{}:
2179 match z:
2180 case True{}:
2181 {==}
2182 case False{}:
2183 {==}
2184 case False{}:
2185 match z:
2186 case True{}:
2187 {==}
2188 case False{}:
2189 {==}
2190 case False{}:
2191 match r:
2192 case True{}:
2193 match z:
2194 case True{}:
2195 {==}
2196 case False{}:
2197 {==}
2198 case False{}:
2199 match z:
2200 case True{}:
2201 {==}
2202 case False{}:
2203 {==}
2204 case False{}:
2205 match q:
2206 case True{}:
2207 match r:
2208 case True{}:
2209 match z:
2210 case True{}:
2211 {==}
2212 case False{}:
2213 {==}
2214 case False{}:
2215 match z:
2216 case True{}:
2217 {==}
2218 case False{}:
2219 {==}
2220 case False{}:
2221 match r:
2222 case True{}:
2223 match z:
2224 case True{}:
2225 {==}
2226 case False{}:
2227 {==}
2228 case False{}:
2229 match z:
2230 case True{}:
2231 {==}
2232 case False{}:
2233 {==}
2234 case False{}:
2235 match p:
2236 case True{}:
2237 match q:
2238 case True{}:
2239 match r:
2240 case True{}:
2241 match z:
2242 case True{}:
2243 {==}
2244 case False{}:
2245 {==}
2246 case False{}:
2247 match z:
2248 case True{}:
2249 {==}
2250 case False{}:
2251 {==}
2252 case False{}:
2253 match r:
2254 case True{}:
2255 match z:
2256 case True{}:
2257 {==}
2258 case False{}:
2259 {==}
2260 case False{}:
2261 match z:
2262 case True{}:
2263 {==}
2264 case False{}:
2265 {==}
2266 case False{}:
2267 match q:
2268 case True{}:
2269 match r:
2270 case True{}:
2271 match z:
2272 case True{}:
2273 {==}
2274 case False{}:
2275 {==}
2276 case False{}:
2277 match z:
2278 case True{}:
2279 {==}
2280 case False{}:
2281 {==}
2282 case False{}:
2283 match r:
2284 case True{}:
2285 match z:
2286 case True{}:
2287 {==}
2288 case False{}:
2289 {==}
2290 case False{}:
2291 match z:
2292 case True{}:
2293 {==}
2294 case False{}:
2295 {==}
2296 case False{}:
2297 match e:
2298 case True{}:
2299 match p:
2300 case True{}:
2301 match q:
2302 case True{}:
2303 match r:
2304 case True{}:
2305 match z:
2306 case True{}:
2307 {==}
2308 case False{}:
2309 {==}
2310 case False{}:
2311 match z:
2312 case True{}:
2313 {==}
2314 case False{}:
2315 {==}
2316 case False{}:
2317 match r:
2318 case True{}:
2319 match z:
2320 case True{}:
2321 {==}
2322 case False{}:
2323 {==}
2324 case False{}:
2325 match z:
2326 case True{}:
2327 {==}
2328 case False{}:
2329 {==}
2330 case False{}:
2331 match q:
2332 case True{}:
2333 match r:
2334 case True{}:
2335 match z:
2336 case True{}:
2337 {==}
2338 case False{}:
2339 {==}
2340 case False{}:
2341 match z:
2342 case True{}:
2343 {==}
2344 case False{}:
2345 {==}
2346 case False{}:
2347 match r:
2348 case True{}:
2349 match z:
2350 case True{}:
2351 {==}
2352 case False{}:
2353 {==}
2354 case False{}:
2355 match z:
2356 case True{}:
2357 {==}
2358 case False{}:
2359 {==}
2360 case False{}:
2361 match p:
2362 case True{}:
2363 match q:
2364 case True{}:
2365 match r:
2366 case True{}:
2367 match z:
2368 case True{}:
2369 {==}
2370 case False{}:
2371 {==}
2372 case False{}:
2373 match z:
2374 case True{}:
2375 {==}
2376 case False{}:
2377 {==}
2378 case False{}:
2379 match r:
2380 case True{}:
2381 match z:
2382 case True{}:
2383 {==}
2384 case False{}:
2385 {==}
2386 case False{}:
2387 match z:
2388 case True{}:
2389 {==}
2390 case False{}:
2391 {==}
2392 case False{}:
2393 match q:
2394 case True{}:
2395 match r:
2396 case True{}:
2397 match z:
2398 case True{}:
2399 {==}
2400 case False{}:
2401 {==}
2402 case False{}:
2403 match z:
2404 case True{}:
2405 {==}
2406 case False{}:
2407 {==}
2408 case False{}:
2409 match r:
2410 case True{}:
2411 match z:
2412 case True{}:
2413 {==}
2414 case False{}:
2415 {==}
2416 case False{}:
2417 match z:
2418 case True{}:
2419 {==}
2420 case False{}:
2421 {==}
2422
2423def nfa.taut_star2(+hb: Bool, +cin: Bool, +ain: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), True{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, p)), Bool.or(Bool.and(hb, Bool.or(r, p)), z))) : Bool}:
2424 match hb:
2425 case True{}:
2426 match cin:
2427 case True{}:
2428 match ain:
2429 case True{}:
2430 match p:
2431 case True{}:
2432 match q:
2433 case True{}:
2434 match r:
2435 case True{}:
2436 match z:
2437 case True{}:
2438 {==}
2439 case False{}:
2440 {==}
2441 case False{}:
2442 match z:
2443 case True{}:
2444 {==}
2445 case False{}:
2446 {==}
2447 case False{}:
2448 match r:
2449 case True{}:
2450 match z:
2451 case True{}:
2452 {==}
2453 case False{}:
2454 {==}
2455 case False{}:
2456 match z:
2457 case True{}:
2458 {==}
2459 case False{}:
2460 {==}
2461 case False{}:
2462 match q:
2463 case True{}:
2464 match r:
2465 case True{}:
2466 match z:
2467 case True{}:
2468 {==}
2469 case False{}:
2470 {==}
2471 case False{}:
2472 match z:
2473 case True{}:
2474 {==}
2475 case False{}:
2476 {==}
2477 case False{}:
2478 match r:
2479 case True{}:
2480 match z:
2481 case True{}:
2482 {==}
2483 case False{}:
2484 {==}
2485 case False{}:
2486 match z:
2487 case True{}:
2488 {==}
2489 case False{}:
2490 {==}
2491 case False{}:
2492 match p:
2493 case True{}:
2494 match q:
2495 case True{}:
2496 match r:
2497 case True{}:
2498 match z:
2499 case True{}:
2500 {==}
2501 case False{}:
2502 {==}
2503 case False{}:
2504 match z:
2505 case True{}:
2506 {==}
2507 case False{}:
2508 {==}
2509 case False{}:
2510 match r:
2511 case True{}:
2512 match z:
2513 case True{}:
2514 {==}
2515 case False{}:
2516 {==}
2517 case False{}:
2518 match z:
2519 case True{}:
2520 {==}
2521 case False{}:
2522 {==}
2523 case False{}:
2524 match q:
2525 case True{}:
2526 match r:
2527 case True{}:
2528 match z:
2529 case True{}:
2530 {==}
2531 case False{}:
2532 {==}
2533 case False{}:
2534 match z:
2535 case True{}:
2536 {==}
2537 case False{}:
2538 {==}
2539 case False{}:
2540 match r:
2541 case True{}:
2542 match z:
2543 case True{}:
2544 {==}
2545 case False{}:
2546 {==}
2547 case False{}:
2548 match z:
2549 case True{}:
2550 {==}
2551 case False{}:
2552 {==}
2553 case False{}:
2554 match ain:
2555 case True{}:
2556 match p:
2557 case True{}:
2558 match q:
2559 case True{}:
2560 match r:
2561 case True{}:
2562 match z:
2563 case True{}:
2564 {==}
2565 case False{}:
2566 {==}
2567 case False{}:
2568 match z:
2569 case True{}:
2570 {==}
2571 case False{}:
2572 {==}
2573 case False{}:
2574 match r:
2575 case True{}:
2576 match z:
2577 case True{}:
2578 {==}
2579 case False{}:
2580 {==}
2581 case False{}:
2582 match z:
2583 case True{}:
2584 {==}
2585 case False{}:
2586 {==}
2587 case False{}:
2588 match q:
2589 case True{}:
2590 match r:
2591 case True{}:
2592 match z:
2593 case True{}:
2594 {==}
2595 case False{}:
2596 {==}
2597 case False{}:
2598 match z:
2599 case True{}:
2600 {==}
2601 case False{}:
2602 {==}
2603 case False{}:
2604 match r:
2605 case True{}:
2606 match z:
2607 case True{}:
2608 {==}
2609 case False{}:
2610 {==}
2611 case False{}:
2612 match z:
2613 case True{}:
2614 {==}
2615 case False{}:
2616 {==}
2617 case False{}:
2618 match p:
2619 case True{}:
2620 match q:
2621 case True{}:
2622 match r:
2623 case True{}:
2624 match z:
2625 case True{}:
2626 {==}
2627 case False{}:
2628 {==}
2629 case False{}:
2630 match z:
2631 case True{}:
2632 {==}
2633 case False{}:
2634 {==}
2635 case False{}:
2636 match r:
2637 case True{}:
2638 match z:
2639 case True{}:
2640 {==}
2641 case False{}:
2642 {==}
2643 case False{}:
2644 match z:
2645 case True{}:
2646 {==}
2647 case False{}:
2648 {==}
2649 case False{}:
2650 match q:
2651 case True{}:
2652 match r:
2653 case True{}:
2654 match z:
2655 case True{}:
2656 {==}
2657 case False{}:
2658 {==}
2659 case False{}:
2660 match z:
2661 case True{}:
2662 {==}
2663 case False{}:
2664 {==}
2665 case False{}:
2666 match r:
2667 case True{}:
2668 match z:
2669 case True{}:
2670 {==}
2671 case False{}:
2672 {==}
2673 case False{}:
2674 match z:
2675 case True{}:
2676 {==}
2677 case False{}:
2678 {==}
2679 case False{}:
2680 match cin:
2681 case True{}:
2682 match ain:
2683 case True{}:
2684 match p:
2685 case True{}:
2686 match q:
2687 case True{}:
2688 match r:
2689 case True{}:
2690 match z:
2691 case True{}:
2692 {==}
2693 case False{}:
2694 {==}
2695 case False{}:
2696 match z:
2697 case True{}:
2698 {==}
2699 case False{}:
2700 {==}
2701 case False{}:
2702 match r:
2703 case True{}:
2704 match z:
2705 case True{}:
2706 {==}
2707 case False{}:
2708 {==}
2709 case False{}:
2710 match z:
2711 case True{}:
2712 {==}
2713 case False{}:
2714 {==}
2715 case False{}:
2716 match q:
2717 case True{}:
2718 match r:
2719 case True{}:
2720 match z:
2721 case True{}:
2722 {==}
2723 case False{}:
2724 {==}
2725 case False{}:
2726 match z:
2727 case True{}:
2728 {==}
2729 case False{}:
2730 {==}
2731 case False{}:
2732 match r:
2733 case True{}:
2734 match z:
2735 case True{}:
2736 {==}
2737 case False{}:
2738 {==}
2739 case False{}:
2740 match z:
2741 case True{}:
2742 {==}
2743 case False{}:
2744 {==}
2745 case False{}:
2746 match p:
2747 case True{}:
2748 match q:
2749 case True{}:
2750 match r:
2751 case True{}:
2752 match z:
2753 case True{}:
2754 {==}
2755 case False{}:
2756 {==}
2757 case False{}:
2758 match z:
2759 case True{}:
2760 {==}
2761 case False{}:
2762 {==}
2763 case False{}:
2764 match r:
2765 case True{}:
2766 match z:
2767 case True{}:
2768 {==}
2769 case False{}:
2770 {==}
2771 case False{}:
2772 match z:
2773 case True{}:
2774 {==}
2775 case False{}:
2776 {==}
2777 case False{}:
2778 match q:
2779 case True{}:
2780 match r:
2781 case True{}:
2782 match z:
2783 case True{}:
2784 {==}
2785 case False{}:
2786 {==}
2787 case False{}:
2788 match z:
2789 case True{}:
2790 {==}
2791 case False{}:
2792 {==}
2793 case False{}:
2794 match r:
2795 case True{}:
2796 match z:
2797 case True{}:
2798 {==}
2799 case False{}:
2800 {==}
2801 case False{}:
2802 match z:
2803 case True{}:
2804 {==}
2805 case False{}:
2806 {==}
2807 case False{}:
2808 match ain:
2809 case True{}:
2810 match p:
2811 case True{}:
2812 match q:
2813 case True{}:
2814 match r:
2815 case True{}:
2816 match z:
2817 case True{}:
2818 {==}
2819 case False{}:
2820 {==}
2821 case False{}:
2822 match z:
2823 case True{}:
2824 {==}
2825 case False{}:
2826 {==}
2827 case False{}:
2828 match r:
2829 case True{}:
2830 match z:
2831 case True{}:
2832 {==}
2833 case False{}:
2834 {==}
2835 case False{}:
2836 match z:
2837 case True{}:
2838 {==}
2839 case False{}:
2840 {==}
2841 case False{}:
2842 match q:
2843 case True{}:
2844 match r:
2845 case True{}:
2846 match z:
2847 case True{}:
2848 {==}
2849 case False{}:
2850 {==}
2851 case False{}:
2852 match z:
2853 case True{}:
2854 {==}
2855 case False{}:
2856 {==}
2857 case False{}:
2858 match r:
2859 case True{}:
2860 match z:
2861 case True{}:
2862 {==}
2863 case False{}:
2864 {==}
2865 case False{}:
2866 match z:
2867 case True{}:
2868 {==}
2869 case False{}:
2870 {==}
2871 case False{}:
2872 match p:
2873 case True{}:
2874 match q:
2875 case True{}:
2876 match r:
2877 case True{}:
2878 match z:
2879 case True{}:
2880 {==}
2881 case False{}:
2882 {==}
2883 case False{}:
2884 match z:
2885 case True{}:
2886 {==}
2887 case False{}:
2888 {==}
2889 case False{}:
2890 match r:
2891 case True{}:
2892 match z:
2893 case True{}:
2894 {==}
2895 case False{}:
2896 {==}
2897 case False{}:
2898 match z:
2899 case True{}:
2900 {==}
2901 case False{}:
2902 {==}
2903 case False{}:
2904 match q:
2905 case True{}:
2906 match r:
2907 case True{}:
2908 match z:
2909 case True{}:
2910 {==}
2911 case False{}:
2912 {==}
2913 case False{}:
2914 match z:
2915 case True{}:
2916 {==}
2917 case False{}:
2918 {==}
2919 case False{}:
2920 match r:
2921 case True{}:
2922 match z:
2923 case True{}:
2924 {==}
2925 case False{}:
2926 {==}
2927 case False{}:
2928 match z:
2929 case True{}:
2930 {==}
2931 case False{}:
2932 {==}
2933
2934
2935
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}))
2957
2958
2959def nfa.dead(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +s: List<&2, U32>, +e: {G.AaGNfa.alive(bs) == False{} : Bool}) -> {G.AaGNfa.sem(seq, bs, s) == False{} : Bool}:
2960 match seq:
2961 case Nil{}:
2962 match bs:
2963 case Nil{}:
2964 {==}
2965 case Con{b, rest}:
2966 match b:
2967 case True{}:
2968 b.absurd_tf(Bool, G.AaGNfa.sem(Nil{}, Con{True{}, rest}, s), False{}, e)
2969 case False{}:
2970 {==}
2971 case Con{tok, r}:
2972 match bs:
2973 case Nil{}:
2974 nfa.dead(r, Nil{}, s, {==})
2975 case Con{b, rest}:
2976 match b:
2977 case True{}:
2978 b.absurd_tf(Bool, G.AaGNfa.sem(Con{tok, r}, Con{True{}, rest}, s), False{}, e)
2979 case False{}:
2980 nfa.dead(r, rest, s, e)
2981
2982
2983def nfa.run(+s: List<&2, U32>, +a: Bool, +seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +e: {G.AaGNfa.alive(bs) == a : Bool}) -> {G.AaGNfa.run(s, a, seq, bs) == G.AaGNfa.sem(seq, bs, s) : Bool}:
2984 match s:
2985 case Nil{}:
2986 {==}
2987 case Con{h, t}:
2988 match a:
2989 case False{}:
2990 Equal.sym(Bool, G.AaGNfa.sem(seq, bs, Con{h, t}), False{}, nfa.dead(seq, bs, Con{h, t}, e))
2991 case True{}:
2992 Equal.trans(Bool, G.AaGNfa.run(t, G.AaGNfa.alive(G.AaGNfa.next(seq, bs, False{}, False{}, h)), seq, G.AaGNfa.next(seq, bs, False{}, False{}, h)), G.AaGNfa.sem(seq, G.AaGNfa.next(seq, bs, False{}, False{}, h), t), G.AaGNfa.sem(seq, bs, Con{h, t}), nfa.run(t, G.AaGNfa.alive(G.AaGNfa.next(seq, bs, False{}, False{}, h)), seq, G.AaGNfa.next(seq, bs, False{}, False{}, h), {==}), nfa.step(seq, bs, False{}, False{}, h, t))
2993
2994def nfa.falses_dead(+seq: List<&2, G.AaGTok>) -> {G.AaGNfa.alive(G.AaGNfa.falses(seq)) == False{} : Bool}:
2995 match seq:
2996 case Nil{}:
2997 {==}
2998 case Con{tok, r}:
2999 nfa.falses_dead(r)
3000
3001
3002def nfa.start(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.start(seq), s) == G.AaGSeq.matches(seq, s) : Bool}:
3003 match seq:
3004 case Nil{}:
3005 {==}
3006 case Con{tok, r}:
3007 %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.falses(r), s), False{}, nfa.dead(r, G.AaGNfa.falses(r), s, nfa.falses_dead(r))) : {Bool.or(G.AaGSeq.matches(Con{tok, r}, s), _) == G.AaGSeq.matches(Con{tok, r}, s) : Bool}
3008 b.or_false_r(G.AaGSeq.matches(Con{tok, r}, s))
3009
3010def nfa.start_alive(+seq: List<&2, G.AaGTok>) -> {G.AaGNfa.alive(G.AaGNfa.start(seq)) == True{} : Bool}:
3011 match seq:
3012 case Nil{}:
3013 {==}
3014 case Con{tok, r}:
3015 {==}
3016
3017def nfa.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.run(seq, s) == G.AaGSeq.matches(seq, s) : Bool}:
3018 Equal.trans(Bool, G.AaGNfa.run(s, True{}, seq, G.AaGNfa.start(seq)), G.AaGNfa.sem(seq, G.AaGNfa.start(seq), s), G.AaGSeq.matches(seq, s), nfa.run(s, True{}, seq, G.AaGNfa.start(seq), nfa.start_alive(seq)), nfa.start(seq, s))
3019
3020def glob.alts(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches.go(alts, s) == G.AaGlob.model.go(alts, s) : Bool}:
3021 match alts:
3022 case Nil{}:
3023 {==}
3024 case Con{a, t}:
3025 %glob.thm(a, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
3026 %nfa.thm(a, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
3027 %glob.alts(t, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(G.AaGSeq.run(a, s), _) : Bool}
3028 {==}
3029
3030def glob.alts_ref(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches_ref.go(alts, s) == G.AaGlob.model.go(alts, s) : Bool}:
3031 match alts:
3032 case Nil{}:
3033 {==}
3034 case Con{a, t}:
3035 %glob.thm(a, s) : {Bool.or(G.AaGSeq.matches(a, s), G.AaGlob.matches_ref.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
3036 %glob.alts_ref(t, s) : {Bool.or(G.AaGSeq.matches(a, s), G.AaGlob.matches_ref.go(t, s)) == Bool.or(G.AaGSeq.matches(a, s), _) : Bool}
3037 {==}
3038
3039def Laws.glob_seq_model(seq, s):
3040 glob.thm(seq, s)
3041
3042def Laws.glob_run(seq, s):
3043 nfa.thm(seq, s)
3044
3045def Laws.glob_model(g, s):
3046 match g:
3047 case G.AaGlob{alts, lit}:
3048 glob.alts(alts, s)
3049
3050def Laws.glob_ref_model(g, s):
3051 match g:
3052 case G.AaGlob{alts, lit}:
3053 glob.alts_ref(alts, s)
3054
3055
3056
3057
3058
3059
3060def bits.minus_meets(+a: List<&2, Bool>, +d: List<&2, Bool>) -> {P.AaBits.meets(P.AaBits.minus(a, d), d) == False{} : Bool}:
3061 match a:
3062 case Nil{}:
3063 {==}
3064 case Con{x, xs}:
3065 match x:
3066 case False{}:
3067 match d:
3068 case Nil{}:
3069 {==}
3070 case Con{y, ys}:
3071 bits.minus_meets(xs, ys)
3072 case True{}:
3073 match d:
3074 case Nil{}:
3075 {==}
3076 case Con{y, ys}:
3077 match y:
3078 case True{}:
3079 bits.minus_meets(xs, ys)
3080 case False{}:
3081 bits.minus_meets(xs, ys)
3082
3083
3084def bits.nany_meets(+r: List<&2, Bool>, +d: List<&2, Bool>) -> {Bool.and(Bool.not(P.AaBits.any(r)), P.AaBits.meets(r, d)) == False{} : Bool}:
3085 match r:
3086 case Nil{}:
3087 {==}
3088 case Con{z, zs}:
3089 match z:
3090 case True{}:
3091 {==}
3092 case False{}:
3093 match d:
3094 case Nil{}:
3095 b.and_false_r(Bool.not(P.AaBits.any(zs)))
3096 case Con{y, ys}:
3097 bits.nany_meets(zs, ys)
3098
3099
3100def bits.covers_meets(+a: List<&2, Bool>, +d: List<&2, Bool>, +r: List<&2, Bool>) -> {Bool.and(P.AaBits.covers(P.AaBits.minus(a, d), r), P.AaBits.meets(r, d)) == False{} : Bool}:
3101 match a:
3102 case Nil{}:
3103 match d:
3104 case Nil{}:
3105 match r:
3106 case Nil{}:
3107 {==}
3108 case Con{z, zs}:
3109 b.and_false_r(P.AaBits.covers(Nil{}, Con{z, zs}))
3110 case Con{y, ys}:
3111 match r:
3112 case Nil{}:
3113 {==}
3114 case Con{z, zs}:
3115 match z:
3116 case True{}:
3117 {==}
3118 case False{}:
3119 bits.nany_meets(zs, ys)
3120 case Con{x, xs}:
3121 match x:
3122 case True{}:
3123 match d:
3124 case Nil{}:
3125 match r:
3126 case Nil{}:
3127 {==}
3128 case Con{z, zs}:
3129 b.and_false_r(P.AaBits.covers(Con{True{}, xs}, Con{z, zs}))
3130 case Con{y, ys}:
3131 match y:
3132 case True{}:
3133 match r:
3134 case Nil{}:
3135 {==}
3136 case Con{z, zs}:
3137 match z:
3138 case True{}:
3139 {==}
3140 case False{}:
3141 bits.covers_meets(xs, ys, zs)
3142 case False{}:
3143 match r:
3144 case Nil{}:
3145 {==}
3146 case Con{z, zs}:
3147 match z:
3148 case True{}:
3149 bits.covers_meets(xs, ys, zs)
3150 case False{}:
3151 bits.covers_meets(xs, ys, zs)
3152 case False{}:
3153 match d:
3154 case Nil{}:
3155 match r:
3156 case Nil{}:
3157 {==}
3158 case Con{z, zs}:
3159 b.and_false_r(P.AaBits.covers(Con{False{}, xs}, Con{z, zs}))
3160 case Con{y, ys}:
3161 match y:
3162 case True{}:
3163 match r:
3164 case Nil{}:
3165 {==}
3166 case Con{z, zs}:
3167 match z:
3168 case True{}:
3169 {==}
3170 case False{}:
3171 bits.covers_meets(xs, ys, zs)
3172 case False{}:
3173 match r:
3174 case Nil{}:
3175 {==}
3176 case Con{z, zs}:
3177 match z:
3178 case True{}:
3179 {==}
3180 case False{}:
3181 bits.covers_meets(xs, ys, zs)
3182
3183def bits.or_assoc(+a: List<&2, Bool>, +b: List<&2, Bool>, +c: List<&2, Bool>) -> {P.AaBits.or(P.AaBits.or(a, b), c) == P.AaBits.or(a, P.AaBits.or(b, c)) : List<&2, Bool>}:
3184 match a:
3185 case Nil{}:
3186 {==}
3187 case Con{x, xs}:
3188 match b:
3189 case Nil{}:
3190 {==}
3191 case Con{y, ys}:
3192 match c:
3193 case Nil{}:
3194 {==}
3195 case Con{z, zs}:
3196 %b.or_assoc(x, y, z) : {Con{Bool.or(Bool.or(x, y), z), P.AaBits.or(P.AaBits.or(xs, ys), zs)} == Con{_, P.AaBits.or(xs, P.AaBits.or(ys, zs))} : List<&2, Bool>}
3197 %bits.or_assoc(xs, ys, zs) : {Con{Bool.or(Bool.or(x, y), z), P.AaBits.or(P.AaBits.or(xs, ys), zs)} == Con{Bool.or(Bool.or(x, y), z), _} : List<&2, Bool>}
3198 {==}
3199
3200def b.or_idem(+a: Bool) -> {Bool.or(a, a) == a : Bool}:
3201 match a:
3202 case True{}:
3203 {==}
3204 case False{}:
3205 {==}
3206
3207def bits.or_idem(+a: List<&2, Bool>) -> {P.AaBits.or(a, a) == a : List<&2, Bool>}:
3208 match a:
3209 case Nil{}:
3210 {==}
3211 case Con{x, xs}:
3212 %b.or_idem(x) : {Con{Bool.or(x, x), P.AaBits.or(xs, xs)} == Con{_, xs} : List<&2, Bool>}
3213 %bits.or_idem(xs) : {Con{Bool.or(x, x), P.AaBits.or(xs, xs)} == Con{Bool.or(x, x), _} : List<&2, Bool>}
3214 {==}
3215
3216def bits.or_nil_r(+a: List<&2, Bool>) -> {P.AaBits.or(a, Nil{}) == a : List<&2, Bool>}:
3217 match a:
3218 case Nil{}:
3219 {==}
3220 case Con{x, xs}:
3221 {==}
3222
3223
3224
3225def pm.covers_meets(+a: P.AaPerms, +d: P.AaPerms, +r: P.AaPerms) -> {Bool.and(P.AaPerms.covers(P.AaPerms.minus(a, d), r), P.AaPerms.meets(r, d)) == False{} : Bool}:
3226 match a:
3227 case P.AaPerms{x}:
3228 match d:
3229 case P.AaPerms{y}:
3230 match r:
3231 case P.AaPerms{z}:
3232 bits.covers_meets(x, y, z)
3233
3234def pm.minus_meets(+a: P.AaPerms, +d: P.AaPerms) -> {P.AaPerms.meets(P.AaPerms.minus(a, d), d) == False{} : Bool}:
3235 match a:
3236 case P.AaPerms{x}:
3237 match d:
3238 case P.AaPerms{y}:
3239 bits.minus_meets(x, y)
3240
3241def pm.assoc(+a: P.AaPerms, +b: P.AaPerms, +c: P.AaPerms) -> {P.AaPerms.union(P.AaPerms.union(a, b), c) == P.AaPerms.union(a, P.AaPerms.union(b, c)) : P.AaPerms}:
3242 match a:
3243 case P.AaPerms{x}:
3244 match b:
3245 case P.AaPerms{y}:
3246 match c:
3247 case P.AaPerms{z}:
3248 Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(P.AaBits.or(x, y), z), P.AaBits.or(x, P.AaBits.or(y, z)), bits.or_assoc(x, y, z))
3249
3250def pm.idem(+a: P.AaPerms) -> {P.AaPerms.union(a, a) == a : P.AaPerms}:
3251 match a:
3252 case P.AaPerms{x}:
3253 Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(x, x), x, bits.or_idem(x))
3254
3255def pm.none_r(+a: P.AaPerms) -> {P.AaPerms.union(a, P.AaPerms.none()) == a : P.AaPerms}:
3256 match a:
3257 case P.AaPerms{x}:
3258 Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(x, Nil{}), x, bits.or_nil_r(x))
3259
3260
3261
3262def dec.ok(+b: Bool) -> {V.AaDecision.allowed(V.AaEval.choose(b, V.AaAudit{}, V.AaAllow{})) == True{} : Bool}:
3263 match b:
3264 case True{}:
3265 {==}
3266 case False{}:
3267 {==}
3268
3269
3270def dw.mode(+hit: Bool, +cov: Bool, +m: PR.AaMode, +opts: O.AaOptions, +ok: V.AaDecision, +no: V.AaDecision, +h: {hit == True{} : Bool}, +e: {Bool.and(cov, hit) == False{} : Bool}, +h1: {V.AaEval.deny_applies(opts, m) == True{} : Bool}, +hno: {V.AaDecision.allowed(no) == False{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, hit, O.AaOptions.complain_deny(opts), ok, no)) == False{} : Bool}:
3271 match hit:
3272 case False{}:
3273 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, False{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, h)
3274 case True{}:
3275 match cov:
3276 case True{}:
3277 b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, True{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, e)
3278 case False{}:
3279 match m:
3280 case PR.AaModeEnforce{}:
3281 hno
3282 case PR.AaModePrompt{}:
3283 hno
3284 case PR.AaModeKill{}:
3285 {==}
3286 case PR.AaModeDefaultAllow{}:
3287 hno
3288 case PR.AaModeUnconfined{}:
3289 b.absurd(Bool, True{}, False{}, h1)
3290 case PR.AaModeComplain{}:
3291 match opts:
3292 case O.AaOptions{c, d, v}:
3293 match c:
3294 case True{}:
3295 hno
3296 case False{}:
3297 b.absurd(Bool, True{}, False{}, h1)
3298
3299def dw.acc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +acc: V.AaAcc, +h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(flags)) == True{} : Bool}, +h2: {P.AaPerms.meets(req, V.AaAcc.deny(acc)) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.acc(opts, flags, req, acc)) == False{} : Bool}:
3300 match flags:
3301 case PR.AaFlags{m, fa}:
3302 match acc:
3303 case V.AaAcc{al, de, au, qu}:
3304 dw.mode(P.AaPerms.meets(req, de), P.AaPerms.covers(P.AaPerms.minus(al, de), req), m, opts, V.AaEval.choose(Bool.or(fa, P.AaPerms.meets(req, au)), V.AaAudit{}, V.AaAllow{}), V.AaDeny{Bool.or(fa, Bool.not(P.AaPerms.covers(P.AaPerms.minus(qu, au), P.AaPerms.minus(req, P.AaPerms.minus(al, de)))))}, h2, pm.covers_meets(al, de, req), h1, {==})
3305
3306
3307def ud.mode(+cov: Bool, +m: PR.AaMode, +hit: Bool, +cd: Bool, +ok: V.AaDecision, +no: V.AaDecision, +hc: {cov == False{} : Bool}, +h1: {PR.AaMode.enforcing(m) == True{} : Bool}, +hno: {V.AaDecision.allowed(no) == False{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, hit, cd, ok, no)) == False{} : Bool}:
3308 match cov:
3309 case True{}:
3310 b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, hit, cd, ok, no)), False{}, hc)
3311 case False{}:
3312 match m:
3313 case PR.AaModeEnforce{}:
3314 hno
3315 case PR.AaModePrompt{}:
3316 hno
3317 case PR.AaModeKill{}:
3318 {==}
3319 case PR.AaModeDefaultAllow{}:
3320 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), False{}, h1)
3321 case PR.AaModeUnconfined{}:
3322 b.absurd(Bool, True{}, False{}, h1)
3323 case PR.AaModeComplain{}:
3324 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(Bool.and(cd, hit), no, V.AaComplain{})), False{}, h1)
3325
3326
3327def cd.mode(+m: PR.AaMode, +cov: Bool, +hit: Bool, +opts: O.AaOptions, +ok: V.AaDecision, +no: V.AaDecision, +h: {PR.AaMode.is_complain(m) == True{} : Bool}, +e: {Bool.and(cov, hit) == False{} : Bool}, +hok: {V.AaDecision.allowed(ok) == True{} : Bool}, +hno: {V.AaDecision.allowed(no) == False{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, hit, O.AaOptions.complain_deny(opts), ok, no)) == Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)) : Bool}:
3328 match m:
3329 case PR.AaModeComplain{}:
3330 match cov:
3331 case True{}:
3332 match hit:
3333 case True{}:
3334 b.absurd_tf(Bool, V.AaDecision.allowed(ok), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), True{})), e)
3335 case False{}:
3336 match opts:
3337 case O.AaOptions{c, d, v}:
3338 match c:
3339 case True{}:
3340 hok
3341 case False{}:
3342 hok
3343 case False{}:
3344 match hit:
3345 case True{}:
3346 match opts:
3347 case O.AaOptions{c, d, v}:
3348 match c:
3349 case True{}:
3350 hno
3351 case False{}:
3352 {==}
3353 case False{}:
3354 match opts:
3355 case O.AaOptions{c, d, v}:
3356 match c:
3357 case True{}:
3358 {==}
3359 case False{}:
3360 {==}
3361 case PR.AaModeEnforce{}:
3362 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3363 case PR.AaModePrompt{}:
3364 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3365 case PR.AaModeKill{}:
3366 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, V.AaKill{})), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3367 case PR.AaModeDefaultAllow{}:
3368 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3369 case PR.AaModeUnconfined{}:
3370 b.absurd(Bool, True{}, Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3371
3372def cd.acc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +acc: V.AaAcc, +h: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.acc(opts, flags, req, acc)) == Bool.not(Bool.and(O.AaOptions.complain_deny(opts), P.AaPerms.meets(req, V.AaAcc.deny(acc)))) : Bool}:
3373 match flags:
3374 case PR.AaFlags{m, fa}:
3375 match acc:
3376 case V.AaAcc{al, de, au, qu}:
3377 cd.mode(m, P.AaPerms.covers(P.AaPerms.minus(al, de), req), P.AaPerms.meets(req, de), opts, V.AaEval.choose(Bool.or(fa, P.AaPerms.meets(req, au)), V.AaAudit{}, V.AaAllow{}), V.AaDeny{Bool.or(fa, Bool.not(P.AaPerms.covers(P.AaPerms.minus(qu, au), P.AaPerms.minus(req, P.AaPerms.minus(al, de)))))}, h, pm.covers_meets(al, de, req), dec.ok(Bool.or(fa, P.AaPerms.meets(req, au))), {==})
3378
3379def gnd.acc(+acc: V.AaAcc) -> {P.AaPerms.meets(V.AaAcc.granted(acc), V.AaAcc.deny(acc)) == False{} : Bool}:
3380 match acc:
3381 case V.AaAcc{al, de, au, qu}:
3382 pm.minus_meets(al, de)
3383
3384def Laws.granted_never_denied(gs):
3385 gnd.acc(V.AaAcc.of(gs))
3386
3387def Laws.deny_wins(opts, gs, flags, req, h1, h2):
3388 dw.acc(opts, flags, req, V.AaAcc.of(gs), h1, h2)
3389
3390def ud.law(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +h1: {PR.AaMode.enforcing(PR.AaFlags.mode(flags)) == True{} : Bool}, +h2: {P.AaPerms.any(req) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, Nil{})) == False{} : Bool}:
3391 match flags:
3392 case PR.AaFlags{m, fa}:
3393 match req:
3394 case P.AaPerms{rb}:
3395 match rb:
3396 case Nil{}:
3397 b.absurd(Bool, V.AaDecision.allowed(V.AaEval.decide(opts, PR.AaFlags{m, fa}, P.AaPerms{Nil{}}, Nil{})), False{}, h2)
3398 case Con{y, ys}:
3399 ud.mode(P.AaPerms.covers(P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none()), P.AaPerms{Con{y, ys}}), m, P.AaPerms.meets(P.AaPerms{Con{y, ys}}, P.AaPerms.none()), O.AaOptions.complain_deny(opts), V.AaEval.choose(Bool.or(fa, P.AaPerms.meets(P.AaPerms{Con{y, ys}}, P.AaPerms.none())), V.AaAudit{}, V.AaAllow{}), V.AaDeny{Bool.or(fa, Bool.not(P.AaPerms.covers(P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none()), P.AaPerms.minus(P.AaPerms{Con{y, ys}}, P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none())))))}, Equal.cong(Bool, Bool, x => Bool.not(x), Bool.or(y, P.AaBits.any(ys)), True{}, h2), h1, {==})
3400
3401def Laws.unmatched_denied(opts, flags, req, h1, h2):
3402 ud.law(opts, flags, req, h1, h2)
3403
3404def Laws.complain_decided_by_deny(opts, flags, req, gs, h):
3405 cd.acc(opts, flags, req, V.AaAcc.of(gs), h)
3406
3407def cnd.law(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +gs: List<&2, P.AaGrant>, +h1: {O.AaOptions.complain_deny(opts) == False{} : Bool}, +h2: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == True{} : Bool}:
3408 Equal.trans(Bool, V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), P.AaPerms.meets(req, V.AaEval.denied(gs)))), True{}, Laws.complain_decided_by_deny(opts, flags, req, gs, h2), Equal.cong(Bool, Bool, x => Bool.not(Bool.and(x, P.AaPerms.meets(req, V.AaEval.denied(gs)))), O.AaOptions.complain_deny(opts), False{}, h1))
3409
3410def Laws.complain_never_denies(opts, flags, req, gs, h1, h2):
3411 cnd.law(opts, flags, req, gs, h1, h2)
3412
3413def fdw.law(+opts: O.AaOptions, +p: PR.AaProfile, +q: F.AaFileQuery, +h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool}, +h2: {P.AaPerms.meets(F.AaFileQuery.req(q), V.AaEval.denied(F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(p)), q))) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool}:
3414 match q:
3415 case F.AaFileQuery{path, owner, req}:
3416 Laws.deny_wins(opts, F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(p)), F.AaFileQuery{path, owner, req}), PR.AaProfile.flags(p), req, h1, h2)
3417
3418def Laws.file_deny_wins(opts, p, q, h1, h2):
3419 fdw.law(opts, p, q, h1, h2)
3420
3421def fud.law(+opts: O.AaOptions, +p: PR.AaProfile, +q: F.AaFileQuery, +h1: {PR.AaMode.enforcing(PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool}, +h2: {F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(p)), q) == Nil{} : List<&2, F.AaFileRule>}, +h3: {P.AaPerms.any(F.AaFileQuery.req(q)) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool}:
3422 match q:
3423 case F.AaFileQuery{path, owner, req}:
3424 %Equal.sym(List<&2, F.AaFileRule>, F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(p)), F.AaFileQuery{path, owner, req}), Nil{}, h2) : {V.AaDecision.allowed(V.AaEval.decide(opts, PR.AaProfile.flags(p), req, F.AaFileRule.grants.of(_))) == False{} : Bool}
3425 Laws.unmatched_denied(opts, PR.AaProfile.flags(p), req, h1, h3)
3426
3427def Laws.file_unmatched_denied(opts, p, q, h1, h2, h3):
3428 fud.law(opts, p, q, h1, h2, h3)
3429
3430
3431
3432def acc.join_empty_l(+a: V.AaAcc) -> {V.AaAcc.join(V.AaAcc.empty(), a) == a : V.AaAcc}:
3433 match a:
3434 case V.AaAcc{al, de, au, qu}:
3435 match al:
3436 case P.AaPerms{x1}:
3437 match de:
3438 case P.AaPerms{x2}:
3439 match au:
3440 case P.AaPerms{x3}:
3441 match qu:
3442 case P.AaPerms{x4}:
3443 {==}
3444
3445def acc.join_empty_r(+a: V.AaAcc) -> {V.AaAcc.join(a, V.AaAcc.empty()) == a : V.AaAcc}:
3446 match a:
3447 case V.AaAcc{al, de, au, qu}:
3448 %pm.none_r(al) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{_, de, au, qu} : V.AaAcc}
3449 %pm.none_r(de) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), _, au, qu} : V.AaAcc}
3450 %pm.none_r(au) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), _, qu} : V.AaAcc}
3451 %pm.none_r(qu) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), _} : V.AaAcc}
3452 {==}
3453
3454def acc.join_assoc(+a: V.AaAcc, +b: V.AaAcc, +c: V.AaAcc) -> {V.AaAcc.join(V.AaAcc.join(a, b), c) == V.AaAcc.join(a, V.AaAcc.join(b, c)) : V.AaAcc}:
3455 match a:
3456 case V.AaAcc{al1, de1, au1, qu1}:
3457 match b:
3458 case V.AaAcc{al2, de2, au2, qu2}:
3459 match c:
3460 case V.AaAcc{al3, de3, au3, qu3}:
3461 %pm.assoc(al1, al2, al3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{_, P.AaPerms.union(de1, P.AaPerms.union(de2, de3)), P.AaPerms.union(au1, P.AaPerms.union(au2, au3)), P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
3462 %pm.assoc(de1, de2, de3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), _, P.AaPerms.union(au1, P.AaPerms.union(au2, au3)), P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
3463 %pm.assoc(au1, au2, au3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), _, P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
3464 %pm.assoc(qu1, qu2, qu3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), _} : V.AaAcc}
3465 {==}
3466
3467def acc.join_idem(+a: V.AaAcc) -> {V.AaAcc.join(a, a) == a : V.AaAcc}:
3468 match a:
3469 case V.AaAcc{al, de, au, qu}:
3470 %pm.idem(al) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{_, de, au, qu} : V.AaAcc}
3471 %pm.idem(de) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), _, au, qu} : V.AaAcc}
3472 %pm.idem(au) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), _, qu} : V.AaAcc}
3473 %pm.idem(qu) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), _} : V.AaAcc}
3474 {==}
3475
3476def from_join(+ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(ys, acc) == V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())) : V.AaAcc}:
3477 match ys:
3478 case Nil{}:
3479 Equal.sym(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.empty()), acc, acc.join_empty_r(acc))
3480 case Con{g, t}:
3481 Equal.trans(V.AaAcc, V.AaAcc.from(t, V.AaAcc.join(acc, V.AaAcc.single(g))), V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), from_join(t, V.AaAcc.join(acc, V.AaAcc.single(g))), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), acc.join_assoc(acc, V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty())), Equal.sym(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), Equal.trans(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, x), V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g))), V.AaAcc.join(V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), from_join(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, V.AaAcc.join(x, V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.single(g), acc.join_empty_l(V.AaAcc.single(g)))))))
3482
3483def from_idem(+ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(ys, V.AaAcc.from(ys, acc)) == V.AaAcc.from(ys, acc) : V.AaAcc}:
3484 Equal.trans(V.AaAcc, V.AaAcc.from(ys, V.AaAcc.from(ys, acc)), V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), from_join(ys, V.AaAcc.from(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(x, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.from(ys, acc), acc.join_assoc(acc, V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, x), V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty()), acc.join_idem(V.AaAcc.from(ys, V.AaAcc.empty()))), Equal.sym(V.AaAcc, V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc))))))
3485
3486def from_app(+xs: List<&2, P.AaGrant>, +ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(P.AaGrant.append(xs, ys), acc) == V.AaAcc.from(ys, V.AaAcc.from(xs, acc)) : V.AaAcc}:
3487 match xs:
3488 case Nil{}:
3489 {==}
3490 case Con{g, t}:
3491 from_app(t, ys, V.AaAcc.add(acc, g))
3492
3493def inc.acc(+g0: List<&2, P.AaGrant>, +g1: List<&2, P.AaGrant>) -> {V.AaAcc.of(P.AaGrant.append(P.AaGrant.append(g0, g1), g1)) == V.AaAcc.of(P.AaGrant.append(g0, g1)) : V.AaAcc}:
3494 Equal.trans(V.AaAcc, V.AaAcc.from(P.AaGrant.append(P.AaGrant.append(g0, g1), g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_app(P.AaGrant.append(g0, g1), g1, V.AaAcc.empty()), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.from(g1, x), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_idem(g1, V.AaAcc.from(g0, V.AaAcc.empty())), Equal.sym(V.AaAcc, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())))))
3495
3496def inc.decide(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +g0: List<&2, P.AaGrant>, +g1: List<&2, P.AaGrant>) -> {V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(g0, g1), g1)) == V.AaEval.decide(opts, flags, req, P.AaGrant.append(g0, g1)) : V.AaDecision}:
3497 Equal.cong(V.AaAcc, V.AaDecision, a => V.AaEval.decide.acc(opts, flags, req, a), V.AaAcc.of(P.AaGrant.append(P.AaGrant.append(g0, g1), g1)), V.AaAcc.of(P.AaGrant.append(g0, g1)), inc.acc(g0, g1))
3498
3499
3500
3501def file.mgo(+hit: Bool, +r: F.AaFileRule, +a: List<&2, F.AaFileRule>, +b: List<&2, F.AaFileRule>) -> {F.AaFileRule.matching.go(hit, r, F.AaFileRule.append(a, b)) == F.AaFileRule.append(F.AaFileRule.matching.go(hit, r, a), b) : List<&2, F.AaFileRule>}:
3502 match hit:
3503 case True{}:
3504 {==}
3505 case False{}:
3506 {==}
3507
3508def file.match_app(+xs: List<&2, F.AaFileRule>, +ys: List<&2, F.AaFileRule>, +q: F.AaFileQuery) -> {F.AaFileRule.matching(F.AaFileRule.append(xs, ys), q) == F.AaFileRule.append(F.AaFileRule.matching(xs, q), F.AaFileRule.matching(ys, q)) : List<&2, F.AaFileRule>}:
3509 match xs:
3510 case Nil{}:
3511 {==}
3512 case Con{r, t}:
3513 Equal.trans(List<&2, F.AaFileRule>, F.AaFileRule.matching.go(F.AaFileRule.matches(r, q), r, F.AaFileRule.matching(F.AaFileRule.append(t, ys), q)), F.AaFileRule.matching.go(F.AaFileRule.matches(r, q), r, F.AaFileRule.append(F.AaFileRule.matching(t, q), F.AaFileRule.matching(ys, q))), F.AaFileRule.append(F.AaFileRule.matching.go(F.AaFileRule.matches(r, q), r, F.AaFileRule.matching(t, q)), F.AaFileRule.matching(ys, q)), Equal.cong(List<&2, F.AaFileRule>, List<&2, F.AaFileRule>, x => F.AaFileRule.matching.go(F.AaFileRule.matches(r, q), r, x), F.AaFileRule.matching(F.AaFileRule.append(t, ys), q), F.AaFileRule.append(F.AaFileRule.matching(t, q), F.AaFileRule.matching(ys, q)), file.match_app(t, ys, q)), file.mgo(F.AaFileRule.matches(r, q), r, F.AaFileRule.matching(t, q), F.AaFileRule.matching(ys, q)))
3514
3515def file.gof_app(+xs: List<&2, F.AaFileRule>, +ys: List<&2, F.AaFileRule>) -> {F.AaFileRule.grants.of(F.AaFileRule.append(xs, ys)) == P.AaGrant.append(F.AaFileRule.grants.of(xs), F.AaFileRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3516 match xs:
3517 case Nil{}:
3518 {==}
3519 case Con{r, t}:
3520 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{F.AaFileRule.grant(r), x}, F.AaFileRule.grants.of(F.AaFileRule.append(t, ys)), P.AaGrant.append(F.AaFileRule.grants.of(t), F.AaFileRule.grants.of(ys)), file.gof_app(t, ys))
3521
3522def file.gapp(+xs: List<&2, F.AaFileRule>, +ys: List<&2, F.AaFileRule>, +q: F.AaFileQuery) -> {F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q) == P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3523 Equal.trans(List<&2, P.AaGrant>, F.AaFileRule.grants.of(F.AaFileRule.matching(F.AaFileRule.append(xs, ys), q)), F.AaFileRule.grants.of(F.AaFileRule.append(F.AaFileRule.matching(xs, q), F.AaFileRule.matching(ys, q))), P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), Equal.cong(List<&2, F.AaFileRule>, List<&2, P.AaGrant>, x => F.AaFileRule.grants.of(x), F.AaFileRule.matching(F.AaFileRule.append(xs, ys), q), F.AaFileRule.append(F.AaFileRule.matching(xs, q), F.AaFileRule.matching(ys, q)), file.match_app(xs, ys, q)), file.gof_app(F.AaFileRule.matching(xs, q), F.AaFileRule.matching(ys, q)))
3524
3525def file.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, F.AaFileRule>, +ys: List<&2, F.AaFileRule>, +q: F.AaFileQuery) -> {V.AaEval.decide(opts, flags, req, F.AaFileRule.grants(F.AaFileRule.append(F.AaFileRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q)) : V.AaDecision}:
3526 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, F.AaFileRule.grants(F.AaFileRule.append(F.AaFileRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), F.AaFileRule.grants(F.AaFileRule.append(F.AaFileRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, F.AaFileRule.grants(F.AaFileRule.append(F.AaFileRule.append(xs, ys), ys), q), P.AaGrant.append(F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q), F.AaFileRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(ys, q)), file.gapp(F.AaFileRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q), P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), file.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q)), inc.decide(opts, flags, req, F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, F.AaFileRule.grants(F.AaFileRule.append(xs, ys), q), P.AaGrant.append(F.AaFileRule.grants(xs, q), F.AaFileRule.grants(ys, q)), file.gapp(xs, ys, q)))))
3527
3528def file.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: F.AaFileQuery) -> {V.AaEval.file(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.file(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3529 match p:
3530 case PR.AaProfile{n, a, f, r0, c, h}:
3531 match r0:
3532 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3533 match r:
3534 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3535 match q:
3536 case F.AaFileQuery{path, owner, req}:
3537 file.inc(opts, f, req, f0, f1, F.AaFileQuery{path, owner, req})
3538
3539def Laws.include_idempotent_file(opts, p, r, q):
3540 file.law(opts, p, r, q)
3541
3542
3543
3544def cap.mgo(+hit: Bool, +r: RC.AaCapRule, +a: List<&2, RC.AaCapRule>, +b: List<&2, RC.AaCapRule>) -> {RC.AaCapRule.matching.go(hit, r, RC.AaCapRule.append(a, b)) == RC.AaCapRule.append(RC.AaCapRule.matching.go(hit, r, a), b) : List<&2, RC.AaCapRule>}:
3545 match hit:
3546 case True{}:
3547 {==}
3548 case False{}:
3549 {==}
3550
3551def cap.match_app(+xs: List<&2, RC.AaCapRule>, +ys: List<&2, RC.AaCapRule>, +q: RC.AaCapQuery) -> {RC.AaCapRule.matching(RC.AaCapRule.append(xs, ys), q) == RC.AaCapRule.append(RC.AaCapRule.matching(xs, q), RC.AaCapRule.matching(ys, q)) : List<&2, RC.AaCapRule>}:
3552 match xs:
3553 case Nil{}:
3554 {==}
3555 case Con{r, t}:
3556 Equal.trans(List<&2, RC.AaCapRule>, RC.AaCapRule.matching.go(RC.AaCapRule.matches(r, q), r, RC.AaCapRule.matching(RC.AaCapRule.append(t, ys), q)), RC.AaCapRule.matching.go(RC.AaCapRule.matches(r, q), r, RC.AaCapRule.append(RC.AaCapRule.matching(t, q), RC.AaCapRule.matching(ys, q))), RC.AaCapRule.append(RC.AaCapRule.matching.go(RC.AaCapRule.matches(r, q), r, RC.AaCapRule.matching(t, q)), RC.AaCapRule.matching(ys, q)), Equal.cong(List<&2, RC.AaCapRule>, List<&2, RC.AaCapRule>, x => RC.AaCapRule.matching.go(RC.AaCapRule.matches(r, q), r, x), RC.AaCapRule.matching(RC.AaCapRule.append(t, ys), q), RC.AaCapRule.append(RC.AaCapRule.matching(t, q), RC.AaCapRule.matching(ys, q)), cap.match_app(t, ys, q)), cap.mgo(RC.AaCapRule.matches(r, q), r, RC.AaCapRule.matching(t, q), RC.AaCapRule.matching(ys, q)))
3557
3558def cap.gof_app(+xs: List<&2, RC.AaCapRule>, +ys: List<&2, RC.AaCapRule>) -> {RC.AaCapRule.grants.of(RC.AaCapRule.append(xs, ys)) == P.AaGrant.append(RC.AaCapRule.grants.of(xs), RC.AaCapRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3559 match xs:
3560 case Nil{}:
3561 {==}
3562 case Con{r, t}:
3563 match r:
3564 case RC.AaCapRule{qu, ks}:
3565 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), x}, RC.AaCapRule.grants.of(RC.AaCapRule.append(t, ys)), P.AaGrant.append(RC.AaCapRule.grants.of(t), RC.AaCapRule.grants.of(ys)), cap.gof_app(t, ys))
3566
3567def cap.gapp(+xs: List<&2, RC.AaCapRule>, +ys: List<&2, RC.AaCapRule>, +q: RC.AaCapQuery) -> {RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q) == P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3568 Equal.trans(List<&2, P.AaGrant>, RC.AaCapRule.grants.of(RC.AaCapRule.matching(RC.AaCapRule.append(xs, ys), q)), RC.AaCapRule.grants.of(RC.AaCapRule.append(RC.AaCapRule.matching(xs, q), RC.AaCapRule.matching(ys, q))), P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), Equal.cong(List<&2, RC.AaCapRule>, List<&2, P.AaGrant>, x => RC.AaCapRule.grants.of(x), RC.AaCapRule.matching(RC.AaCapRule.append(xs, ys), q), RC.AaCapRule.append(RC.AaCapRule.matching(xs, q), RC.AaCapRule.matching(ys, q)), cap.match_app(xs, ys, q)), cap.gof_app(RC.AaCapRule.matching(xs, q), RC.AaCapRule.matching(ys, q)))
3569
3570def cap.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RC.AaCapRule>, +ys: List<&2, RC.AaCapRule>, +q: RC.AaCapQuery) -> {V.AaEval.decide(opts, flags, req, RC.AaCapRule.grants(RC.AaCapRule.append(RC.AaCapRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q)) : V.AaDecision}:
3571 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RC.AaCapRule.grants(RC.AaCapRule.append(RC.AaCapRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RC.AaCapRule.grants(RC.AaCapRule.append(RC.AaCapRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RC.AaCapRule.grants(RC.AaCapRule.append(RC.AaCapRule.append(xs, ys), ys), q), P.AaGrant.append(RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q), RC.AaCapRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(ys, q)), cap.gapp(RC.AaCapRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q), P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), cap.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q)), inc.decide(opts, flags, req, RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RC.AaCapRule.grants(RC.AaCapRule.append(xs, ys), q), P.AaGrant.append(RC.AaCapRule.grants(xs, q), RC.AaCapRule.grants(ys, q)), cap.gapp(xs, ys, q)))))
3572
3573def cap.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RC.AaCapQuery) -> {V.AaEval.capability(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.capability(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3574 match p:
3575 case PR.AaProfile{n, a, f, r0, c, h}:
3576 match r0:
3577 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3578 match r:
3579 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3580 cap.inc(opts, f, RC.AaCapQuery.req(), c0, c1, q)
3581
3582def Laws.include_idempotent_capability(opts, p, r, q):
3583 cap.law(opts, p, r, q)
3584
3585
3586
3587def net.mgo(+hit: Bool, +r: RN.AaNetRule, +a: List<&2, RN.AaNetRule>, +b: List<&2, RN.AaNetRule>) -> {RN.AaNetRule.matching.go(hit, r, RN.AaNetRule.append(a, b)) == RN.AaNetRule.append(RN.AaNetRule.matching.go(hit, r, a), b) : List<&2, RN.AaNetRule>}:
3588 match hit:
3589 case True{}:
3590 {==}
3591 case False{}:
3592 {==}
3593
3594def net.match_app(+xs: List<&2, RN.AaNetRule>, +ys: List<&2, RN.AaNetRule>, +q: RN.AaNetQuery) -> {RN.AaNetRule.matching(RN.AaNetRule.append(xs, ys), q) == RN.AaNetRule.append(RN.AaNetRule.matching(xs, q), RN.AaNetRule.matching(ys, q)) : List<&2, RN.AaNetRule>}:
3595 match xs:
3596 case Nil{}:
3597 {==}
3598 case Con{r, t}:
3599 Equal.trans(List<&2, RN.AaNetRule>, RN.AaNetRule.matching.go(RN.AaNetRule.matches(r, q), r, RN.AaNetRule.matching(RN.AaNetRule.append(t, ys), q)), RN.AaNetRule.matching.go(RN.AaNetRule.matches(r, q), r, RN.AaNetRule.append(RN.AaNetRule.matching(t, q), RN.AaNetRule.matching(ys, q))), RN.AaNetRule.append(RN.AaNetRule.matching.go(RN.AaNetRule.matches(r, q), r, RN.AaNetRule.matching(t, q)), RN.AaNetRule.matching(ys, q)), Equal.cong(List<&2, RN.AaNetRule>, List<&2, RN.AaNetRule>, x => RN.AaNetRule.matching.go(RN.AaNetRule.matches(r, q), r, x), RN.AaNetRule.matching(RN.AaNetRule.append(t, ys), q), RN.AaNetRule.append(RN.AaNetRule.matching(t, q), RN.AaNetRule.matching(ys, q)), net.match_app(t, ys, q)), net.mgo(RN.AaNetRule.matches(r, q), r, RN.AaNetRule.matching(t, q), RN.AaNetRule.matching(ys, q)))
3600
3601def net.gof_app(+xs: List<&2, RN.AaNetRule>, +ys: List<&2, RN.AaNetRule>) -> {RN.AaNetRule.grants.of(RN.AaNetRule.append(xs, ys)) == P.AaGrant.append(RN.AaNetRule.grants.of(xs), RN.AaNetRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3602 match xs:
3603 case Nil{}:
3604 {==}
3605 case Con{r, t}:
3606 match r:
3607 case RN.AaNetRule{qu, d, ty, pr}:
3608 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), x}, RN.AaNetRule.grants.of(RN.AaNetRule.append(t, ys)), P.AaGrant.append(RN.AaNetRule.grants.of(t), RN.AaNetRule.grants.of(ys)), net.gof_app(t, ys))
3609
3610def net.gapp(+xs: List<&2, RN.AaNetRule>, +ys: List<&2, RN.AaNetRule>, +q: RN.AaNetQuery) -> {RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q) == P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3611 Equal.trans(List<&2, P.AaGrant>, RN.AaNetRule.grants.of(RN.AaNetRule.matching(RN.AaNetRule.append(xs, ys), q)), RN.AaNetRule.grants.of(RN.AaNetRule.append(RN.AaNetRule.matching(xs, q), RN.AaNetRule.matching(ys, q))), P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), Equal.cong(List<&2, RN.AaNetRule>, List<&2, P.AaGrant>, x => RN.AaNetRule.grants.of(x), RN.AaNetRule.matching(RN.AaNetRule.append(xs, ys), q), RN.AaNetRule.append(RN.AaNetRule.matching(xs, q), RN.AaNetRule.matching(ys, q)), net.match_app(xs, ys, q)), net.gof_app(RN.AaNetRule.matching(xs, q), RN.AaNetRule.matching(ys, q)))
3612
3613def net.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RN.AaNetRule>, +ys: List<&2, RN.AaNetRule>, +q: RN.AaNetQuery) -> {V.AaEval.decide(opts, flags, req, RN.AaNetRule.grants(RN.AaNetRule.append(RN.AaNetRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q)) : V.AaDecision}:
3614 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RN.AaNetRule.grants(RN.AaNetRule.append(RN.AaNetRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RN.AaNetRule.grants(RN.AaNetRule.append(RN.AaNetRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RN.AaNetRule.grants(RN.AaNetRule.append(RN.AaNetRule.append(xs, ys), ys), q), P.AaGrant.append(RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q), RN.AaNetRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(ys, q)), net.gapp(RN.AaNetRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q), P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), net.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q)), inc.decide(opts, flags, req, RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RN.AaNetRule.grants(RN.AaNetRule.append(xs, ys), q), P.AaGrant.append(RN.AaNetRule.grants(xs, q), RN.AaNetRule.grants(ys, q)), net.gapp(xs, ys, q)))))
3615
3616def net.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RN.AaNetQuery) -> {V.AaEval.network(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.network(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3617 match p:
3618 case PR.AaProfile{n, a, f, r0, c, h}:
3619 match r0:
3620 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3621 match r:
3622 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3623 net.inc(opts, f, RN.AaNetQuery.req(), n0, n1, q)
3624
3625def Laws.include_idempotent_network(opts, p, r, q):
3626 net.law(opts, p, r, q)
3627
3628
3629
3630def sig.mgo(+hit: Bool, +r: RS.AaSignalRule, +a: List<&2, RS.AaSignalRule>, +b: List<&2, RS.AaSignalRule>) -> {RS.AaSignalRule.matching.go(hit, r, RS.AaSignalRule.append(a, b)) == RS.AaSignalRule.append(RS.AaSignalRule.matching.go(hit, r, a), b) : List<&2, RS.AaSignalRule>}:
3631 match hit:
3632 case True{}:
3633 {==}
3634 case False{}:
3635 {==}
3636
3637def sig.match_app(+xs: List<&2, RS.AaSignalRule>, +ys: List<&2, RS.AaSignalRule>, +q: RS.AaSignalQuery) -> {RS.AaSignalRule.matching(RS.AaSignalRule.append(xs, ys), q) == RS.AaSignalRule.append(RS.AaSignalRule.matching(xs, q), RS.AaSignalRule.matching(ys, q)) : List<&2, RS.AaSignalRule>}:
3638 match xs:
3639 case Nil{}:
3640 {==}
3641 case Con{r, t}:
3642 Equal.trans(List<&2, RS.AaSignalRule>, RS.AaSignalRule.matching.go(RS.AaSignalRule.matches(r, q), r, RS.AaSignalRule.matching(RS.AaSignalRule.append(t, ys), q)), RS.AaSignalRule.matching.go(RS.AaSignalRule.matches(r, q), r, RS.AaSignalRule.append(RS.AaSignalRule.matching(t, q), RS.AaSignalRule.matching(ys, q))), RS.AaSignalRule.append(RS.AaSignalRule.matching.go(RS.AaSignalRule.matches(r, q), r, RS.AaSignalRule.matching(t, q)), RS.AaSignalRule.matching(ys, q)), Equal.cong(List<&2, RS.AaSignalRule>, List<&2, RS.AaSignalRule>, x => RS.AaSignalRule.matching.go(RS.AaSignalRule.matches(r, q), r, x), RS.AaSignalRule.matching(RS.AaSignalRule.append(t, ys), q), RS.AaSignalRule.append(RS.AaSignalRule.matching(t, q), RS.AaSignalRule.matching(ys, q)), sig.match_app(t, ys, q)), sig.mgo(RS.AaSignalRule.matches(r, q), r, RS.AaSignalRule.matching(t, q), RS.AaSignalRule.matching(ys, q)))
3643
3644def sig.gof_app(+xs: List<&2, RS.AaSignalRule>, +ys: List<&2, RS.AaSignalRule>) -> {RS.AaSignalRule.grants.of(RS.AaSignalRule.append(xs, ys)) == P.AaGrant.append(RS.AaSignalRule.grants.of(xs), RS.AaSignalRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3645 match xs:
3646 case Nil{}:
3647 {==}
3648 case Con{r, t}:
3649 match r:
3650 case RS.AaSignalRule{qu, p, s, pe}:
3651 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, p), x}, RS.AaSignalRule.grants.of(RS.AaSignalRule.append(t, ys)), P.AaGrant.append(RS.AaSignalRule.grants.of(t), RS.AaSignalRule.grants.of(ys)), sig.gof_app(t, ys))
3652
3653def sig.gapp(+xs: List<&2, RS.AaSignalRule>, +ys: List<&2, RS.AaSignalRule>, +q: RS.AaSignalQuery) -> {RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q) == P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3654 Equal.trans(List<&2, P.AaGrant>, RS.AaSignalRule.grants.of(RS.AaSignalRule.matching(RS.AaSignalRule.append(xs, ys), q)), RS.AaSignalRule.grants.of(RS.AaSignalRule.append(RS.AaSignalRule.matching(xs, q), RS.AaSignalRule.matching(ys, q))), P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), Equal.cong(List<&2, RS.AaSignalRule>, List<&2, P.AaGrant>, x => RS.AaSignalRule.grants.of(x), RS.AaSignalRule.matching(RS.AaSignalRule.append(xs, ys), q), RS.AaSignalRule.append(RS.AaSignalRule.matching(xs, q), RS.AaSignalRule.matching(ys, q)), sig.match_app(xs, ys, q)), sig.gof_app(RS.AaSignalRule.matching(xs, q), RS.AaSignalRule.matching(ys, q)))
3655
3656def sig.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RS.AaSignalRule>, +ys: List<&2, RS.AaSignalRule>, +q: RS.AaSignalQuery) -> {V.AaEval.decide(opts, flags, req, RS.AaSignalRule.grants(RS.AaSignalRule.append(RS.AaSignalRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q)) : V.AaDecision}:
3657 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RS.AaSignalRule.grants(RS.AaSignalRule.append(RS.AaSignalRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RS.AaSignalRule.grants(RS.AaSignalRule.append(RS.AaSignalRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RS.AaSignalRule.grants(RS.AaSignalRule.append(RS.AaSignalRule.append(xs, ys), ys), q), P.AaGrant.append(RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q), RS.AaSignalRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(ys, q)), sig.gapp(RS.AaSignalRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q), P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), sig.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q)), inc.decide(opts, flags, req, RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RS.AaSignalRule.grants(RS.AaSignalRule.append(xs, ys), q), P.AaGrant.append(RS.AaSignalRule.grants(xs, q), RS.AaSignalRule.grants(ys, q)), sig.gapp(xs, ys, q)))))
3658
3659def sig.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RS.AaSignalQuery) -> {V.AaEval.signal(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.signal(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3660 match p:
3661 case PR.AaProfile{n, a, f, r0, c, h}:
3662 match r0:
3663 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3664 match r:
3665 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3666 sig.inc(opts, f, RS.AaSignalQuery.req(q), s0, s1, q)
3667
3668def Laws.include_idempotent_signal(opts, p, r, q):
3669 sig.law(opts, p, r, q)
3670
3671
3672
3673def ptr.mgo(+hit: Bool, +r: RP.AaPtraceRule, +a: List<&2, RP.AaPtraceRule>, +b: List<&2, RP.AaPtraceRule>) -> {RP.AaPtraceRule.matching.go(hit, r, RP.AaPtraceRule.append(a, b)) == RP.AaPtraceRule.append(RP.AaPtraceRule.matching.go(hit, r, a), b) : List<&2, RP.AaPtraceRule>}:
3674 match hit:
3675 case True{}:
3676 {==}
3677 case False{}:
3678 {==}
3679
3680def ptr.match_app(+xs: List<&2, RP.AaPtraceRule>, +ys: List<&2, RP.AaPtraceRule>, +q: RP.AaPtraceQuery) -> {RP.AaPtraceRule.matching(RP.AaPtraceRule.append(xs, ys), q) == RP.AaPtraceRule.append(RP.AaPtraceRule.matching(xs, q), RP.AaPtraceRule.matching(ys, q)) : List<&2, RP.AaPtraceRule>}:
3681 match xs:
3682 case Nil{}:
3683 {==}
3684 case Con{r, t}:
3685 Equal.trans(List<&2, RP.AaPtraceRule>, RP.AaPtraceRule.matching.go(RP.AaPtraceRule.matches(r, q), r, RP.AaPtraceRule.matching(RP.AaPtraceRule.append(t, ys), q)), RP.AaPtraceRule.matching.go(RP.AaPtraceRule.matches(r, q), r, RP.AaPtraceRule.append(RP.AaPtraceRule.matching(t, q), RP.AaPtraceRule.matching(ys, q))), RP.AaPtraceRule.append(RP.AaPtraceRule.matching.go(RP.AaPtraceRule.matches(r, q), r, RP.AaPtraceRule.matching(t, q)), RP.AaPtraceRule.matching(ys, q)), Equal.cong(List<&2, RP.AaPtraceRule>, List<&2, RP.AaPtraceRule>, x => RP.AaPtraceRule.matching.go(RP.AaPtraceRule.matches(r, q), r, x), RP.AaPtraceRule.matching(RP.AaPtraceRule.append(t, ys), q), RP.AaPtraceRule.append(RP.AaPtraceRule.matching(t, q), RP.AaPtraceRule.matching(ys, q)), ptr.match_app(t, ys, q)), ptr.mgo(RP.AaPtraceRule.matches(r, q), r, RP.AaPtraceRule.matching(t, q), RP.AaPtraceRule.matching(ys, q)))
3686
3687def ptr.gof_app(+xs: List<&2, RP.AaPtraceRule>, +ys: List<&2, RP.AaPtraceRule>) -> {RP.AaPtraceRule.grants.of(RP.AaPtraceRule.append(xs, ys)) == P.AaGrant.append(RP.AaPtraceRule.grants.of(xs), RP.AaPtraceRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3688 match xs:
3689 case Nil{}:
3690 {==}
3691 case Con{r, t}:
3692 match r:
3693 case RP.AaPtraceRule{qu, p, pe}:
3694 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, p), x}, RP.AaPtraceRule.grants.of(RP.AaPtraceRule.append(t, ys)), P.AaGrant.append(RP.AaPtraceRule.grants.of(t), RP.AaPtraceRule.grants.of(ys)), ptr.gof_app(t, ys))
3695
3696def ptr.gapp(+xs: List<&2, RP.AaPtraceRule>, +ys: List<&2, RP.AaPtraceRule>, +q: RP.AaPtraceQuery) -> {RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q) == P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3697 Equal.trans(List<&2, P.AaGrant>, RP.AaPtraceRule.grants.of(RP.AaPtraceRule.matching(RP.AaPtraceRule.append(xs, ys), q)), RP.AaPtraceRule.grants.of(RP.AaPtraceRule.append(RP.AaPtraceRule.matching(xs, q), RP.AaPtraceRule.matching(ys, q))), P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), Equal.cong(List<&2, RP.AaPtraceRule>, List<&2, P.AaGrant>, x => RP.AaPtraceRule.grants.of(x), RP.AaPtraceRule.matching(RP.AaPtraceRule.append(xs, ys), q), RP.AaPtraceRule.append(RP.AaPtraceRule.matching(xs, q), RP.AaPtraceRule.matching(ys, q)), ptr.match_app(xs, ys, q)), ptr.gof_app(RP.AaPtraceRule.matching(xs, q), RP.AaPtraceRule.matching(ys, q)))
3698
3699def ptr.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RP.AaPtraceRule>, +ys: List<&2, RP.AaPtraceRule>, +q: RP.AaPtraceQuery) -> {V.AaEval.decide(opts, flags, req, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(RP.AaPtraceRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q)) : V.AaDecision}:
3700 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(RP.AaPtraceRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RP.AaPtraceRule.grants(RP.AaPtraceRule.append(RP.AaPtraceRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(RP.AaPtraceRule.append(xs, ys), ys), q), P.AaGrant.append(RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q), RP.AaPtraceRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(ys, q)), ptr.gapp(RP.AaPtraceRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q), P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), ptr.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q)), inc.decide(opts, flags, req, RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RP.AaPtraceRule.grants(RP.AaPtraceRule.append(xs, ys), q), P.AaGrant.append(RP.AaPtraceRule.grants(xs, q), RP.AaPtraceRule.grants(ys, q)), ptr.gapp(xs, ys, q)))))
3701
3702def ptr.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RP.AaPtraceQuery) -> {V.AaEval.ptrace(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.ptrace(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3703 match p:
3704 case PR.AaProfile{n, a, f, r0, c, h}:
3705 match r0:
3706 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3707 match r:
3708 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3709 ptr.inc(opts, f, RP.AaPtraceQuery.req(q), p0, p1, q)
3710
3711def Laws.include_idempotent_ptrace(opts, p, r, q):
3712 ptr.law(opts, p, r, q)
3713
3714
3715
3716def mnt.mgo(+hit: Bool, +r: RM.AaMountRule, +a: List<&2, RM.AaMountRule>, +b: List<&2, RM.AaMountRule>) -> {RM.AaMountRule.matching.go(hit, r, RM.AaMountRule.append(a, b)) == RM.AaMountRule.append(RM.AaMountRule.matching.go(hit, r, a), b) : List<&2, RM.AaMountRule>}:
3717 match hit:
3718 case True{}:
3719 {==}
3720 case False{}:
3721 {==}
3722
3723def mnt.match_app(+xs: List<&2, RM.AaMountRule>, +ys: List<&2, RM.AaMountRule>, +q: RM.AaMountQuery) -> {RM.AaMountRule.matching(RM.AaMountRule.append(xs, ys), q) == RM.AaMountRule.append(RM.AaMountRule.matching(xs, q), RM.AaMountRule.matching(ys, q)) : List<&2, RM.AaMountRule>}:
3724 match xs:
3725 case Nil{}:
3726 {==}
3727 case Con{r, t}:
3728 Equal.trans(List<&2, RM.AaMountRule>, RM.AaMountRule.matching.go(RM.AaMountRule.matches(r, q), r, RM.AaMountRule.matching(RM.AaMountRule.append(t, ys), q)), RM.AaMountRule.matching.go(RM.AaMountRule.matches(r, q), r, RM.AaMountRule.append(RM.AaMountRule.matching(t, q), RM.AaMountRule.matching(ys, q))), RM.AaMountRule.append(RM.AaMountRule.matching.go(RM.AaMountRule.matches(r, q), r, RM.AaMountRule.matching(t, q)), RM.AaMountRule.matching(ys, q)), Equal.cong(List<&2, RM.AaMountRule>, List<&2, RM.AaMountRule>, x => RM.AaMountRule.matching.go(RM.AaMountRule.matches(r, q), r, x), RM.AaMountRule.matching(RM.AaMountRule.append(t, ys), q), RM.AaMountRule.append(RM.AaMountRule.matching(t, q), RM.AaMountRule.matching(ys, q)), mnt.match_app(t, ys, q)), mnt.mgo(RM.AaMountRule.matches(r, q), r, RM.AaMountRule.matching(t, q), RM.AaMountRule.matching(ys, q)))
3729
3730def mnt.gof_app(+xs: List<&2, RM.AaMountRule>, +ys: List<&2, RM.AaMountRule>) -> {RM.AaMountRule.grants.of(RM.AaMountRule.append(xs, ys)) == P.AaGrant.append(RM.AaMountRule.grants.of(xs), RM.AaMountRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3731 match xs:
3732 case Nil{}:
3733 {==}
3734 case Con{r, t}:
3735 match r:
3736 case RM.AaMountRule{qu, op, fs, os, so, tg}:
3737 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), x}, RM.AaMountRule.grants.of(RM.AaMountRule.append(t, ys)), P.AaGrant.append(RM.AaMountRule.grants.of(t), RM.AaMountRule.grants.of(ys)), mnt.gof_app(t, ys))
3738
3739def mnt.gapp(+xs: List<&2, RM.AaMountRule>, +ys: List<&2, RM.AaMountRule>, +q: RM.AaMountQuery) -> {RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q) == P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3740 Equal.trans(List<&2, P.AaGrant>, RM.AaMountRule.grants.of(RM.AaMountRule.matching(RM.AaMountRule.append(xs, ys), q)), RM.AaMountRule.grants.of(RM.AaMountRule.append(RM.AaMountRule.matching(xs, q), RM.AaMountRule.matching(ys, q))), P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), Equal.cong(List<&2, RM.AaMountRule>, List<&2, P.AaGrant>, x => RM.AaMountRule.grants.of(x), RM.AaMountRule.matching(RM.AaMountRule.append(xs, ys), q), RM.AaMountRule.append(RM.AaMountRule.matching(xs, q), RM.AaMountRule.matching(ys, q)), mnt.match_app(xs, ys, q)), mnt.gof_app(RM.AaMountRule.matching(xs, q), RM.AaMountRule.matching(ys, q)))
3741
3742def mnt.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RM.AaMountRule>, +ys: List<&2, RM.AaMountRule>, +q: RM.AaMountQuery) -> {V.AaEval.decide(opts, flags, req, RM.AaMountRule.grants(RM.AaMountRule.append(RM.AaMountRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q)) : V.AaDecision}:
3743 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RM.AaMountRule.grants(RM.AaMountRule.append(RM.AaMountRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RM.AaMountRule.grants(RM.AaMountRule.append(RM.AaMountRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RM.AaMountRule.grants(RM.AaMountRule.append(RM.AaMountRule.append(xs, ys), ys), q), P.AaGrant.append(RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q), RM.AaMountRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(ys, q)), mnt.gapp(RM.AaMountRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q), P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), mnt.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q)), inc.decide(opts, flags, req, RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RM.AaMountRule.grants(RM.AaMountRule.append(xs, ys), q), P.AaGrant.append(RM.AaMountRule.grants(xs, q), RM.AaMountRule.grants(ys, q)), mnt.gapp(xs, ys, q)))))
3744
3745def mnt.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RM.AaMountQuery) -> {V.AaEval.mount(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.mount(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3746 match p:
3747 case PR.AaProfile{n, a, f, r0, c, h}:
3748 match r0:
3749 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3750 match r:
3751 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3752 mnt.inc(opts, f, RM.AaMountQuery.req(), m0, m1, q)
3753
3754def Laws.include_idempotent_mount(opts, p, r, q):
3755 mnt.law(opts, p, r, q)
3756
3757
3758
3759def dbs.mgo(+hit: Bool, +r: RD.AaDbusRule, +a: List<&2, RD.AaDbusRule>, +b: List<&2, RD.AaDbusRule>) -> {RD.AaDbusRule.matching.go(hit, r, RD.AaDbusRule.append(a, b)) == RD.AaDbusRule.append(RD.AaDbusRule.matching.go(hit, r, a), b) : List<&2, RD.AaDbusRule>}:
3760 match hit:
3761 case True{}:
3762 {==}
3763 case False{}:
3764 {==}
3765
3766def dbs.match_app(+xs: List<&2, RD.AaDbusRule>, +ys: List<&2, RD.AaDbusRule>, +q: RD.AaDbusQuery) -> {RD.AaDbusRule.matching(RD.AaDbusRule.append(xs, ys), q) == RD.AaDbusRule.append(RD.AaDbusRule.matching(xs, q), RD.AaDbusRule.matching(ys, q)) : List<&2, RD.AaDbusRule>}:
3767 match xs:
3768 case Nil{}:
3769 {==}
3770 case Con{r, t}:
3771 Equal.trans(List<&2, RD.AaDbusRule>, RD.AaDbusRule.matching.go(RD.AaDbusRule.matches(r, q), r, RD.AaDbusRule.matching(RD.AaDbusRule.append(t, ys), q)), RD.AaDbusRule.matching.go(RD.AaDbusRule.matches(r, q), r, RD.AaDbusRule.append(RD.AaDbusRule.matching(t, q), RD.AaDbusRule.matching(ys, q))), RD.AaDbusRule.append(RD.AaDbusRule.matching.go(RD.AaDbusRule.matches(r, q), r, RD.AaDbusRule.matching(t, q)), RD.AaDbusRule.matching(ys, q)), Equal.cong(List<&2, RD.AaDbusRule>, List<&2, RD.AaDbusRule>, x => RD.AaDbusRule.matching.go(RD.AaDbusRule.matches(r, q), r, x), RD.AaDbusRule.matching(RD.AaDbusRule.append(t, ys), q), RD.AaDbusRule.append(RD.AaDbusRule.matching(t, q), RD.AaDbusRule.matching(ys, q)), dbs.match_app(t, ys, q)), dbs.mgo(RD.AaDbusRule.matches(r, q), r, RD.AaDbusRule.matching(t, q), RD.AaDbusRule.matching(ys, q)))
3772
3773def dbs.gof_app(+xs: List<&2, RD.AaDbusRule>, +ys: List<&2, RD.AaDbusRule>) -> {RD.AaDbusRule.grants.of(RD.AaDbusRule.append(xs, ys)) == P.AaGrant.append(RD.AaDbusRule.grants.of(xs), RD.AaDbusRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3774 match xs:
3775 case Nil{}:
3776 {==}
3777 case Con{r, t}:
3778 match r:
3779 case RD.AaDbusRule{qu, p, bus, path, iface, member, name, pn, pl}:
3780 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, p), x}, RD.AaDbusRule.grants.of(RD.AaDbusRule.append(t, ys)), P.AaGrant.append(RD.AaDbusRule.grants.of(t), RD.AaDbusRule.grants.of(ys)), dbs.gof_app(t, ys))
3781
3782def dbs.gapp(+xs: List<&2, RD.AaDbusRule>, +ys: List<&2, RD.AaDbusRule>, +q: RD.AaDbusQuery) -> {RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q) == P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3783 Equal.trans(List<&2, P.AaGrant>, RD.AaDbusRule.grants.of(RD.AaDbusRule.matching(RD.AaDbusRule.append(xs, ys), q)), RD.AaDbusRule.grants.of(RD.AaDbusRule.append(RD.AaDbusRule.matching(xs, q), RD.AaDbusRule.matching(ys, q))), P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), Equal.cong(List<&2, RD.AaDbusRule>, List<&2, P.AaGrant>, x => RD.AaDbusRule.grants.of(x), RD.AaDbusRule.matching(RD.AaDbusRule.append(xs, ys), q), RD.AaDbusRule.append(RD.AaDbusRule.matching(xs, q), RD.AaDbusRule.matching(ys, q)), dbs.match_app(xs, ys, q)), dbs.gof_app(RD.AaDbusRule.matching(xs, q), RD.AaDbusRule.matching(ys, q)))
3784
3785def dbs.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RD.AaDbusRule>, +ys: List<&2, RD.AaDbusRule>, +q: RD.AaDbusQuery) -> {V.AaEval.decide(opts, flags, req, RD.AaDbusRule.grants(RD.AaDbusRule.append(RD.AaDbusRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q)) : V.AaDecision}:
3786 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RD.AaDbusRule.grants(RD.AaDbusRule.append(RD.AaDbusRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RD.AaDbusRule.grants(RD.AaDbusRule.append(RD.AaDbusRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RD.AaDbusRule.grants(RD.AaDbusRule.append(RD.AaDbusRule.append(xs, ys), ys), q), P.AaGrant.append(RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q), RD.AaDbusRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(ys, q)), dbs.gapp(RD.AaDbusRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q), P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), dbs.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q)), inc.decide(opts, flags, req, RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RD.AaDbusRule.grants(RD.AaDbusRule.append(xs, ys), q), P.AaGrant.append(RD.AaDbusRule.grants(xs, q), RD.AaDbusRule.grants(ys, q)), dbs.gapp(xs, ys, q)))))
3787
3788def dbs.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RD.AaDbusQuery) -> {V.AaEval.dbus(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.dbus(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3789 match p:
3790 case PR.AaProfile{n, a, f, r0, c, h}:
3791 match r0:
3792 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3793 match r:
3794 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3795 dbs.inc(opts, f, RD.AaDbusQuery.req(q), d0, d1, q)
3796
3797def Laws.include_idempotent_dbus(opts, p, r, q):
3798 dbs.law(opts, p, r, q)
3799
3800
3801
3802def chg.mgo(+hit: Bool, +r: RX.AaChangeRule, +a: List<&2, RX.AaChangeRule>, +b: List<&2, RX.AaChangeRule>) -> {RX.AaChangeRule.matching.go(hit, r, RX.AaChangeRule.append(a, b)) == RX.AaChangeRule.append(RX.AaChangeRule.matching.go(hit, r, a), b) : List<&2, RX.AaChangeRule>}:
3803 match hit:
3804 case True{}:
3805 {==}
3806 case False{}:
3807 {==}
3808
3809def chg.match_app(+xs: List<&2, RX.AaChangeRule>, +ys: List<&2, RX.AaChangeRule>, +q: RX.AaChangeQuery) -> {RX.AaChangeRule.matching(RX.AaChangeRule.append(xs, ys), q) == RX.AaChangeRule.append(RX.AaChangeRule.matching(xs, q), RX.AaChangeRule.matching(ys, q)) : List<&2, RX.AaChangeRule>}:
3810 match xs:
3811 case Nil{}:
3812 {==}
3813 case Con{r, t}:
3814 Equal.trans(List<&2, RX.AaChangeRule>, RX.AaChangeRule.matching.go(RX.AaChangeRule.matches(r, q), r, RX.AaChangeRule.matching(RX.AaChangeRule.append(t, ys), q)), RX.AaChangeRule.matching.go(RX.AaChangeRule.matches(r, q), r, RX.AaChangeRule.append(RX.AaChangeRule.matching(t, q), RX.AaChangeRule.matching(ys, q))), RX.AaChangeRule.append(RX.AaChangeRule.matching.go(RX.AaChangeRule.matches(r, q), r, RX.AaChangeRule.matching(t, q)), RX.AaChangeRule.matching(ys, q)), Equal.cong(List<&2, RX.AaChangeRule>, List<&2, RX.AaChangeRule>, x => RX.AaChangeRule.matching.go(RX.AaChangeRule.matches(r, q), r, x), RX.AaChangeRule.matching(RX.AaChangeRule.append(t, ys), q), RX.AaChangeRule.append(RX.AaChangeRule.matching(t, q), RX.AaChangeRule.matching(ys, q)), chg.match_app(t, ys, q)), chg.mgo(RX.AaChangeRule.matches(r, q), r, RX.AaChangeRule.matching(t, q), RX.AaChangeRule.matching(ys, q)))
3815
3816def chg.gof_app(+xs: List<&2, RX.AaChangeRule>, +ys: List<&2, RX.AaChangeRule>) -> {RX.AaChangeRule.grants.of(RX.AaChangeRule.append(xs, ys)) == P.AaGrant.append(RX.AaChangeRule.grants.of(xs), RX.AaChangeRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3817 match xs:
3818 case Nil{}:
3819 {==}
3820 case Con{r, t}:
3821 match r:
3822 case RX.AaChangeRule{qu, e, s, tg}:
3823 Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), x}, RX.AaChangeRule.grants.of(RX.AaChangeRule.append(t, ys)), P.AaGrant.append(RX.AaChangeRule.grants.of(t), RX.AaChangeRule.grants.of(ys)), chg.gof_app(t, ys))
3824
3825def chg.gapp(+xs: List<&2, RX.AaChangeRule>, +ys: List<&2, RX.AaChangeRule>, +q: RX.AaChangeQuery) -> {RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q) == P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)) : List<&2, P.AaGrant>}:
3826 Equal.trans(List<&2, P.AaGrant>, RX.AaChangeRule.grants.of(RX.AaChangeRule.matching(RX.AaChangeRule.append(xs, ys), q)), RX.AaChangeRule.grants.of(RX.AaChangeRule.append(RX.AaChangeRule.matching(xs, q), RX.AaChangeRule.matching(ys, q))), P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), Equal.cong(List<&2, RX.AaChangeRule>, List<&2, P.AaGrant>, x => RX.AaChangeRule.grants.of(x), RX.AaChangeRule.matching(RX.AaChangeRule.append(xs, ys), q), RX.AaChangeRule.append(RX.AaChangeRule.matching(xs, q), RX.AaChangeRule.matching(ys, q)), chg.match_app(xs, ys, q)), chg.gof_app(RX.AaChangeRule.matching(xs, q), RX.AaChangeRule.matching(ys, q)))
3827
3828def chg.inc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +xs: List<&2, RX.AaChangeRule>, +ys: List<&2, RX.AaChangeRule>, +q: RX.AaChangeQuery) -> {V.AaEval.decide(opts, flags, req, RX.AaChangeRule.grants(RX.AaChangeRule.append(RX.AaChangeRule.append(xs, ys), ys), q)) == V.AaEval.decide(opts, flags, req, RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q)) : V.AaDecision}:
3829 Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, RX.AaChangeRule.grants(RX.AaChangeRule.append(RX.AaChangeRule.append(xs, ys), ys), q)), V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), RX.AaChangeRule.grants(RX.AaChangeRule.append(RX.AaChangeRule.append(xs, ys), ys), q), P.AaGrant.append(P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(ys, q)), Equal.trans(List<&2, P.AaGrant>, RX.AaChangeRule.grants(RX.AaChangeRule.append(RX.AaChangeRule.append(xs, ys), ys), q), P.AaGrant.append(RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q), RX.AaChangeRule.grants(ys, q)), P.AaGrant.append(P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(ys, q)), chg.gapp(RX.AaChangeRule.append(xs, ys), ys, q), Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => P.AaGrant.append(x, RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q), P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), chg.gapp(xs, ys, q)))), Equal.trans(V.AaDecision, V.AaEval.decide(opts, flags, req, P.AaGrant.append(P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q))), V.AaEval.decide(opts, flags, req, RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q)), inc.decide(opts, flags, req, RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), Equal.cong(List<&2, P.AaGrant>, V.AaDecision, x => V.AaEval.decide(opts, flags, req, x), P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q), Equal.sym(List<&2, P.AaGrant>, RX.AaChangeRule.grants(RX.AaChangeRule.append(xs, ys), q), P.AaGrant.append(RX.AaChangeRule.grants(xs, q), RX.AaChangeRule.grants(ys, q)), chg.gapp(xs, ys, q)))))
3830
3831def chg.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RX.AaChangeQuery) -> {V.AaEval.change_profile(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.change_profile(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3832 match p:
3833 case PR.AaProfile{n, a, f, r0, c, h}:
3834 match r0:
3835 case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3836 match r:
3837 case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3838 chg.inc(opts, f, RX.AaChangeQuery.req(), x0, x1, q)
3839
3840def Laws.include_idempotent_change_profile(opts, p, r, q):
3841 chg.law(opts, p, r, q)
3842
3843
3844
3845def ex.law(+opts: O.AaOptions, +pol: PR.AaPolicy, +name: List<&2, U32>, +owner: Bool, +path: List<&2, U32>, +p: PR.AaProfile, +h1: {PR.AaPolicy.lookup(pol, name) == Some{p} : Maybe<&2, PR.AaProfile>}, +h2: {TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))) == False{} : Bool}, +h3: {V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})) == False{} : Bool}) -> {TR.AaExecResult.ok(TR.AaTrans.exec(opts, pol, name, owner, path)) == False{} : Bool}:
3846 %Equal.sym(Maybe<&2, PR.AaProfile>, PR.AaPolicy.lookup(pol, name), Some{p}, h1) : {TR.AaExecResult.ok(TR.AaTrans.exec.of(_, opts, pol, name, owner, path)) == False{} : Bool}
3847 %Equal.sym(Bool, TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))), False{}, h2) : {TR.AaExecResult.ok(TR.AaTrans.exec.mode(_, opts, pol, p, name, owner, path)) == False{} : Bool}
3848 %Equal.sym(Bool, V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})), False{}, h3) : {TR.AaExecResult.ok(TR.AaTrans.exec.granted(_, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)}, pol, p, name, path, V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)}))) == False{} : Bool}
3849 {==}
3850
3851def Laws.exec_needs_x(opts, pol, name, owner, path, p, h1, h2, h3):
3852 ex.law(opts, pol, name, owner, path, p, h1, h2, h3)
3853
3854
3855
3856def Laws.deny_wins_sat():
3857 {==}
3858
3859def Laws.deny_wins_example():
3860 {==}
3861
3862def Laws.allow_example():
3863 {==}
3864
3865def Laws.audit_example():
3866 {==}
3867
3868def Laws.unmatched_sat():
3869 {==}
3870
3871def Laws.file_unmatched_sat():
3872 {==}
3873
3874def Laws.unmatched_example():
3875 {==}
3876
3877def Laws.complain_sat():
3878 {==}
3879
3880def Laws.complain_example_unmatched():
3881 {==}
3882
3883def Laws.complain_example_deny_rule():
3884 {==}
3885
3886def Laws.complain_example_no_deny():
3887 {==}
3888
3889def Laws.kill_example():
3890 {==}
3891
3892def Laws.exec_needs_x_sat():
3893 {==}
3894
3895def Laws.exec_needs_x_sat2():
3896 {==}
3897
3898def Laws.glob_star_not_empty_segment():
3899 {==}
3900
3901def Laws.glob_star_file():
3902 {==}
3903
3904def Laws.glob_star_no_slash():
3905 {==}
3906
3907def Laws.glob_star2_not_dir_itself():
3908 {==}
3909
3910def Laws.glob_star2_deep():
3911 {==}
3912
3913def Laws.glob_star_inside_segment():
3914 {==}
3915
3916def Laws.glob_star_in_braces():
3917 {==}
3918
3919def Laws.glob_negated_class_slash():
3920 {==}
3921
3922def Laws.glob_slashes_collapse():
3923 {==}
3924
3925def Laws.glob_class_range():
3926 {==}
3927
3928def Laws.glob_nested_braces():
3929 {==}
3930
3931def Laws.glob_question():
3932 {==}
3933
3934def Laws.glob_one_alternative_rejected():
3935 {==}
3936
3937def Laws.glob_trailing_dash_rejected():
3938 {==}
3939
3940def Laws.glob_empty_class_rejected():
3941 {==}
3942
3943def Laws.policy_file_vectors():
3944 {==}
3945
3946def Laws.policy_exec_vectors():
3947 {==}