PROOF.bend
bend-osdev-bpf@0.1.0.0 · 2,132 lines · 47 definitions
1import Base
2import bend-osdev-bytes@0.1.0.0/bytes.bend as B
3import bend-osdev-word64@0.1.0.0/word64.bend as W
4import bend-osdev-bpf@0.1.0.0/insn.bend as I
5import bend-osdev-bpf@0.1.0.0/validate.bend as V
6import bend-osdev-bpf@0.1.0.0/bpf.bend as R
7import bend-osdev-bpf@0.1.0.0/seccomp.bend as S
8import bend-osdev-bpf@0.1.0.0/LAWS.bend as Laws
9
10
11
12def absurd.bool(b: Bool) -> Type:
13 match b:
14 case True{}:
15 Unit
16 case False{}:
17 Empty
18
19def absurd.ft(e: {False{} == True{} : Bool}) -> Empty:
20 %Equal.sym(Bool, False{}, True{}, e) : absurd.bool(_)
21 Unit{}
22
23def absurd.res(r: Result<&2, &2, I.BpfError, Unit>) -> Type:
24 match r:
25 case Fail{e}:
26 Unit
27 case Done{u}:
28 Empty
29
30def absurd.fd(-e: I.BpfError, h: {Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> Empty:
31 %h : absurd.res(_)
32 Unit{}
33
34def nat.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
35 match x:
36 case 0n:
37 {==}
38 case 1n+p:
39 {==}
40
41
42
43def need_ok(b: Bool, -e: I.BpfError, h: {V.bpf_chk(b, e) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {b == True{} : Bool}:
44 match b:
45 case True{}:
46 {==}
47 case False{}:
48 Empty.absurd({False{} == True{} : Bool}, absurd.fd(e, h))
49
50def both_l(r: Result<&2, &2, I.BpfError, Unit>, -s: Result<&2, &2, I.BpfError, Unit>, h: {V.bpf_both(r, s) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {r == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
51 match r:
52 case Fail{e}:
53 Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
54 case Done{u}:
55 match u:
56 case Unit{}:
57 {==}
58
59def both_r(r: Result<&2, &2, I.BpfError, Unit>, -s: Result<&2, &2, I.BpfError, Unit>, h: {V.bpf_both(r, s) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {s == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
60 match r:
61 case Fail{e}:
62 Empty.absurd({s == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
63 case Done{u}:
64 h
65
66def nxt(-pc: Nat, r: Nat, h: {V.bpf_check.next(pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(0n, r) == True{} : Bool}:
67 need_ok(Nat.is_lt(0n, r), I.BpfErrNoReturn{pc}, h)
68
69
70
71
72def step_ok(cur: R.BpfStep, r: Nat) -> Bool:
73 match cur:
74 case R.BpfNext{+skip, +st}:
75 Nat.is_lt(skip, r)
76 case R.BpfStop{v}:
77 True{}
78 case R.BpfFault{e}:
79 False{}
80
81def step_of_ok(m: Maybe<&2, R.BpfState>, -r: Nat, e: {Nat.is_lt(0n, r) == True{} : Bool}) -> {step_ok(R.bpf_step.of(m), r) == True{} : Bool}:
82 match m:
83 case None{}:
84 {==}
85 case Some{st}:
86 e
87
88def scratch_ok(ok: Bool, -k: U32, -st: R.BpfState, -r: Nat, e1: {ok == True{} : Bool}, e2: {Nat.is_lt(0n, r) == True{} : Bool}) -> {step_ok(R.bpf_scratch(ok, k, st), r) == True{} : Bool}:
89 match ok:
90 case True{}:
91 e2
92 case False{}:
93 Empty.absurd({step_ok(R.bpf_scratch(False{}, k, st), r) == True{} : Bool}, absurd.ft(e1))
94
95def mem_ok(+k: U32, -st: R.BpfState, +pc: Nat, +r: Nat, +h: {V.bpf_check.mem(k, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {step_ok(R.bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, st), r) == True{} : Bool}:
96 scratch_ok(U32.is_lt(k, I.bpf_memwords()), k, st, r, need_ok(U32.is_lt(k, I.bpf_memwords()), I.BpfErrScratch{pc}, both_l(V.bpf_chk(U32.is_lt(k, I.bpf_memwords()), I.BpfErrScratch{pc}), V.bpf_check.next(pc, r), h)), nxt(pc, r, both_r(V.bpf_chk(U32.is_lt(k, I.bpf_memwords()), I.BpfErrScratch{pc}), V.bpf_check.next(pc, r), h)))
97
98def jsel_ok(hit: Bool, -jt: U32, -jf: U32, -r: Nat, e1: {Nat.is_lt(U32.to_nat(jt), r) == True{} : Bool}, e2: {Nat.is_lt(U32.to_nat(jf), r) == True{} : Bool}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}:
99 match hit:
100 case True{}:
101 e1
102 case False{}:
103 e2
104
105
106def jmp_ranges(+jt: U32, +jf: U32, +pc: Nat, +r: Nat, +h: {V.bpf_check.jmp(jt, jf, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_both(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc})) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
107 both_r(V.bpf_chk(U32.is_lt(jf, 256), I.BpfErrJumpField{pc}), V.bpf_both(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc})), both_r(V.bpf_chk(U32.is_lt(jt, 256), I.BpfErrJumpField{pc}), V.bpf_both(V.bpf_chk(U32.is_lt(jf, 256), I.BpfErrJumpField{pc}), V.bpf_both(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}))), h))
108
109def jmp_ok(+jt: U32, +jf: U32, +pc: Nat, +r: Nat, hit: Bool, h: {V.bpf_check.jmp(jt, jf, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}:
110 +g = jmp_ranges(jt, jf, pc, r, h)
111 jsel_ok(hit, jt, jf, r, need_ok(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}, both_l(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}), g)), need_ok(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}, both_r(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}), g)))
112
113
114def exec_ok(op: I.BpfOp, st: R.BpfState, +inp: R.BpfInput, +pc: Nat, +r: Nat, h: {V.bpf_check.op(op, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {step_ok(R.bpf_exec(op, st, inp), r) == True{} : Bool}:
115 match op:
116 case I.BpfLdAbs{+size, +k}:
117 step_of_ok(R.bpf_set_a.m(R.bpf_load(inp, size, k), st), r, nxt(pc, r, h))
118 case I.BpfLdInd{+size, +k}:
119 match st:
120 case R.BpfState{+a, +x, +mem}:
121 step_of_ok(R.bpf_set_a.m(R.bpf_load.ind(inp, size, x, k), R.BpfState{a, x, mem}), r, nxt(pc, r, h))
122 case I.BpfLdImm{+k}:
123 nxt(pc, r, h)
124 case I.BpfLdLen{}:
125 nxt(pc, r, h)
126 case I.BpfLdMem{+k}:
127 mem_ok(k, R.bpf_mem.lda(st, k), pc, r, h)
128 case I.BpfLdxImm{+k}:
129 nxt(pc, r, h)
130 case I.BpfLdxMem{+k}:
131 mem_ok(k, R.bpf_mem.ldx(st, k), pc, r, h)
132 case I.BpfLdxLen{}:
133 nxt(pc, r, h)
134 case I.BpfLdxMsh{+k}:
135 step_of_ok(R.bpf_set_x.m(R.bpf_load.msh(inp, k), st), r, nxt(pc, r, h))
136 case I.BpfSt{+k}:
137 mem_ok(k, R.bpf_mem.st(st, k), pc, r, h)
138 case I.BpfStx{+k}:
139 mem_ok(k, R.bpf_mem.stx(st, k), pc, r, h)
140 case I.BpfAlu{+o, +src}:
141 match st:
142 case R.BpfState{+a, +x, +mem}:
143 step_of_ok(R.bpf_set_a.m(R.bpf_alu(o, a, R.bpf_src(src, x)), R.BpfState{a, x, mem}), r, nxt(pc, r, both_r(V.bpf_check.div(o, src, pc), V.bpf_check.next(pc, r), h)))
144 case I.BpfNeg{}:
145 nxt(pc, r, h)
146 case I.BpfJa{+k}:
147 need_ok(Nat.is_lt(U32.to_nat(k), r), I.BpfErrJump{pc}, h)
148 case I.BpfJmp{+c, +src, +jt, +jf}:
149 match st:
150 case R.BpfState{+a, +x, +mem}:
151 jmp_ok(jt, jf, pc, r, R.bpf_test(c, a, R.bpf_src(src, x)), h)
152 case I.BpfRet{+v}:
153 match v:
154 case I.BpfRetK{+k}:
155 {==}
156 case I.BpfRetA{}:
157 {==}
158 case I.BpfTax{}:
159 nxt(pc, r, h)
160 case I.BpfTxa{}:
161 nxt(pc, r, h)
162
163
164
165def go_ok(xs: List<&2, I.BpfOp>, cur: R.BpfStep, +inp: R.BpfInput, +pc: Nat, +v: {V.bpf_check.all(xs, pc) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, p: {step_ok(cur, List.length(&2, I.BpfOp, xs)) == True{} : Bool}) -> {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(xs, cur, inp)) == True{} : Bool}:
166 match xs:
167 case Nil{}:
168 match cur:
169 case R.BpfNext{+skip, +st}:
170 Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Nil{}, R.BpfNext{skip, st}, inp)) == True{} : Bool}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(skip, 0n), True{}, Equal.sym(Bool, Nat.is_lt(skip, 0n), False{}, nat.lt_zero(skip)), p)))
171 case R.BpfStop{w}:
172 {==}
173 case R.BpfFault{e}:
174 Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Nil{}, R.BpfFault{e}, inp)) == True{} : Bool}, absurd.ft(p))
175 case Con{+op, +t}:
176 match cur:
177 case R.BpfNext{+skip, +st}:
178 match skip:
179 case 0n:
180 go_ok(t, R.bpf_exec(op, st, inp), inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), exec_ok(op, st, inp, pc, List.length(&2, I.BpfOp, t), both_l(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v)))
181 case 1n+s:
182 go_ok(t, R.BpfNext{s, st}, inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), p)
183 case R.BpfStop{w}:
184 {==}
185 case R.BpfFault{e}:
186 Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Con{op, t}, R.BpfFault{e}, inp)) == True{} : Bool}, absurd.ft(p))
187
188
189
190
191
192def add_succ(+a: Nat, +n: Nat) -> {Nat.add(a, 1n+n) == 1n+Nat.add(a, n) : Nat}:
193 match a:
194 case 0n:
195 {==}
196 case 1n+p:
197 Equal.cong(Nat, Nat, k => 1n+k, Nat.add(p, 1n+n), 1n+Nat.add(p, n), add_succ(p, n))
198
199def add_zero(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
200 match a:
201 case 0n:
202 {==}
203 case 1n+p:
204 Equal.cong(Nat, Nat, k => 1n+k, Nat.add(p, 0n), p, add_zero(p))
205
206def g_count(+xs: List<&2, I.BpfOp>, +n: Nat) -> {V.bpf_count.go(xs, n) == Nat.add(List.length(&2, I.BpfOp, xs), n) : Nat}:
207 match xs:
208 case Nil{}:
209 {==}
210 case Con{h, t}:
211 Equal.trans(Nat, V.bpf_count.go(t, 1n+n), Nat.add(List.length(&2, I.BpfOp, t), 1n+n), 1n+Nat.add(List.length(&2, I.BpfOp, t), n),
212 g_count(t, 1n+n), add_succ(List.length(&2, I.BpfOp, t), n))
213
214def F_count(+xs: List<&2, I.BpfOp>) -> {List.length(&2, I.BpfOp, xs) == V.bpf_count(xs) : Nat}:
215 Equal.sym(Nat, V.bpf_count(xs), List.length(&2, I.BpfOp, xs),
216 Equal.trans(Nat, V.bpf_count.go(xs, 0n), Nat.add(List.length(&2, I.BpfOp, xs), 0n), List.length(&2, I.BpfOp, xs),
217 g_count(xs, 0n), add_zero(List.length(&2, I.BpfOp, xs))))
218
219
220def g_check(xs: List<&2, I.BpfOp>, +pc: Nat, ok: Result<&2, &2, I.BpfError, Unit>) -> {V.bpf_check.go(xs, pc, ok, List.length(&2, I.BpfOp, xs)) == V.bpf_both(ok, V.bpf_check.all(xs, pc)) : Result<&2, &2, I.BpfError, Unit>}:
221 match xs:
222 case Nil{}:
223 match ok:
224 case Fail{e}:
225 {==}
226 case Done{u}:
227 match u:
228 case Unit{}:
229 {==}
230 case Con{op, +t}:
231 match ok:
232 case Fail{e}:
233 {==}
234 case Done{u}:
235 g_check(t, 1n+pc, V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)))
236
237def F_check(+xs: List<&2, I.BpfOp>) -> {V.bpf_check.all(xs, 0n) == V.bpf_check.go(xs, 0n, Done{Unit{}}, V.bpf_count(xs)) : Result<&2, &2, I.BpfError, Unit>}:
238 %F_count(xs) : {V.bpf_check.all(xs, 0n) == V.bpf_check.go(xs, 0n, Done{Unit{}}, _) : Result<&2, &2, I.BpfError, Unit>}
239 Equal.sym(Result<&2, &2, I.BpfError, Unit>, V.bpf_check.go(xs, 0n, Done{Unit{}}, List.length(&2, I.BpfOp, xs)), V.bpf_check.all(xs, 0n), g_check(xs, 0n, Done{Unit{}}))
240
241
242def ops_l(v: Result<&2, &2, I.BpfError, Unit>, -n: Nat, -need: Bool, -prog: List<&2, I.BpfOp>, h: {V.bpf_validate.ops(v, n, need, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {v == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
243 match v:
244 case Fail{e}:
245 Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
246 case Done{u}:
247 match u:
248 case Unit{}:
249 {==}
250
251def ops_r(v: Result<&2, &2, I.BpfError, Unit>, -n: Nat, -need: Bool, -prog: List<&2, I.BpfOp>, h: {V.bpf_validate.ops(v, n, need, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_validate.mem(V.bpf_check.go(prog, 0n, Done{Unit{}}, n), need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
252 match v:
253 case Fail{e}:
254 Empty.absurd({V.bpf_validate.mem(V.bpf_check.go(prog, 0n, Done{Unit{}}, n), need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
255 case Done{u}:
256 h
257
258def mem_l(v: Result<&2, &2, I.BpfError, Unit>, -need: Bool, -n: Nat, -prog: List<&2, I.BpfOp>, h: {V.bpf_validate.mem(v, need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {v == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
259 match v:
260 case Fail{e}:
261 Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
262 case Done{u}:
263 match u:
264 case Unit{}:
265 {==}
266
267
268
269def valid_all(opts: V.BpfValidateOptions, +prog: List<&2, I.BpfOp>, ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_check.all(prog, 0n) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
270 match opts:
271 case V.BpfValidateOptions{+max, +need}:
272 Equal.trans(Result<&2, &2, I.BpfError, Unit>, V.bpf_check.all(prog, 0n), V.bpf_check.go(prog, 0n, Done{Unit{}}, V.bpf_count(prog)), Done{Unit{}}, F_check(prog),
273 mem_l(V.bpf_check.go(prog, 0n, Done{Unit{}}, V.bpf_count(prog)), need, V.bpf_count(prog), prog, ops_r(V.bpf_check.len(V.bpf_count(prog), max), V.bpf_count(prog), need, prog, ok)))
274
275def valid_nonempty(opts: V.BpfValidateOptions, +prog: List<&2, I.BpfOp>, ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(0n, List.length(&2, I.BpfOp, prog)) == True{} : Bool}:
276 match opts:
277 case V.BpfValidateOptions{+max, +need}:
278 +n = V.bpf_count(prog)
279 %Equal.sym(Nat, List.length(&2, I.BpfOp, prog), V.bpf_count(prog), F_count(prog)) : {Nat.is_lt(0n, _) == True{} : Bool}
280 need_ok(Nat.is_lt(0n, n), I.BpfErrEmpty{}, both_l(V.bpf_chk(Nat.is_lt(0n, n), I.BpfErrEmpty{}), V.bpf_chk(Nat.is_le(n, max), I.BpfErrTooLong{n}), ops_l(V.bpf_check.len(n, max), n, need, prog, ok)))
281
282def Laws.validated_returns(opts, prog, inp, ok):
283 go_ok(prog, R.BpfNext{0n, R.bpf_init()}, inp, 0n, valid_all(opts, prog, ok), valid_nonempty(opts, prog, ok))
284
285
286
287
288def go_stop(q: List<&2, I.BpfOp>, -w: U32, +inp: R.BpfInput) -> {R.bpf_run.go(q, R.BpfStop{w}, inp) == Done{w} : Result<&2, &2, I.BpfError, U32>}:
289 match q:
290 case Nil{}:
291 {==}
292 case Con{op, t}:
293 {==}
294
295def go_app(xs: List<&2, I.BpfOp>, +q: List<&2, I.BpfOp>, cur: R.BpfStep, +inp: R.BpfInput, +pc: Nat, +v: {V.bpf_check.all(xs, pc) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, p: {step_ok(cur, List.length(&2, I.BpfOp, xs)) == True{} : Bool}) -> {R.bpf_run.go(List.append(&2, I.BpfOp, xs, q), cur, inp) == R.bpf_run.go(xs, cur, inp) : Result<&2, &2, I.BpfError, U32>}:
296 match xs:
297 case Nil{}:
298 match cur:
299 case R.BpfNext{+skip, +st}:
300 Empty.absurd({R.bpf_run.go(q, R.BpfNext{skip, st}, inp) == R.bpf_run.go(Nil{}, R.BpfNext{skip, st}, inp) : Result<&2, &2, I.BpfError, U32>}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(skip, 0n), True{}, Equal.sym(Bool, Nat.is_lt(skip, 0n), False{}, nat.lt_zero(skip)), p)))
301 case R.BpfStop{w}:
302 go_stop(q, w, inp)
303 case R.BpfFault{e}:
304 Empty.absurd({R.bpf_run.go(q, R.BpfFault{e}, inp) == R.bpf_run.go(Nil{}, R.BpfFault{e}, inp) : Result<&2, &2, I.BpfError, U32>}, absurd.ft(p))
305 case Con{+op, +t}:
306 match cur:
307 case R.BpfNext{+skip, +st}:
308 match skip:
309 case 0n:
310 go_app(t, q, R.bpf_exec(op, st, inp), inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), exec_ok(op, st, inp, pc, List.length(&2, I.BpfOp, t), both_l(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v)))
311 case 1n+s:
312 go_app(t, q, R.BpfNext{s, st}, inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), p)
313 case R.BpfStop{w}:
314 {==}
315 case R.BpfFault{e}:
316 Empty.absurd({R.bpf_run.go(Con{op, List.append(&2, I.BpfOp, t, q)}, R.BpfFault{e}, inp) == R.bpf_run.go(Con{op, t}, R.BpfFault{e}, inp) : Result<&2, &2, I.BpfError, U32>}, absurd.ft(p))
317
318def Laws.validated_ignores_tail(opts, prog, rest, inp, ok):
319 go_app(prog, rest, R.BpfNext{0n, R.bpf_init()}, inp, 0n, valid_all(opts, prog, ok), valid_nonempty(opts, prog, ok))
320
321def Laws.ret_k(k, inp):
322 {==}
323
324
325
326
327def skip_app(skipped: List<&2, I.BpfOp>, +rest: List<&2, I.BpfOp>, +st: R.BpfState, +inp: R.BpfInput) -> {R.bpf_run.go(List.append(&2, I.BpfOp, skipped, rest), R.BpfNext{List.length(&2, I.BpfOp, skipped), st}, inp) == R.bpf_run.go(rest, R.BpfNext{0n, st}, inp) : Result<&2, &2, I.BpfError, U32>}:
328 match skipped:
329 case Nil{}:
330 {==}
331 case Con{h, t}:
332 skip_app(t, rest, st, inp)
333
334def Laws.ja_skips(k, skipped, rest, inp, e):
335 %e : {R.bpf_run.go(List.append(&2, I.BpfOp, skipped, rest), R.BpfNext{_, R.bpf_init()}, inp) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
336 skip_app(skipped, rest, R.bpf_init(), inp)
337
338def Laws.jeq_taken_skips(jt, jf, skipped, rest, inp, e):
339 %e : {R.bpf_run.go(List.append(&2, I.BpfOp, skipped, rest), R.BpfNext{_, R.bpf_init()}, inp) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
340 skip_app(skipped, rest, R.bpf_init(), inp)
341
342def Laws.jeq_not_taken_skips(jt, jf, skipped, rest, inp, e):
343 %e : {R.bpf_run.go(List.append(&2, I.BpfOp, skipped, rest), R.BpfNext{_, R.bpf_init()}, inp) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
344 skip_app(skipped, rest, R.bpf_init(), inp)
345
346
347
348def Laws.insn_round_trip(op):
349 match op:
350 case I.BpfLdAbs{size, k}:
351 match size:
352 case I.BpfW{}:
353 {==}
354 case I.BpfH{}:
355 {==}
356 case I.BpfB{}:
357 {==}
358 case I.BpfLdInd{size, k}:
359 match size:
360 case I.BpfW{}:
361 {==}
362 case I.BpfH{}:
363 {==}
364 case I.BpfB{}:
365 {==}
366 case I.BpfLdImm{k}:
367 {==}
368 case I.BpfLdLen{}:
369 {==}
370 case I.BpfLdMem{k}:
371 {==}
372 case I.BpfLdxImm{k}:
373 {==}
374 case I.BpfLdxMem{k}:
375 {==}
376 case I.BpfLdxLen{}:
377 {==}
378 case I.BpfLdxMsh{k}:
379 {==}
380 case I.BpfSt{k}:
381 {==}
382 case I.BpfStx{k}:
383 {==}
384 case I.BpfNeg{}:
385 {==}
386 case I.BpfJa{k}:
387 {==}
388 case I.BpfTax{}:
389 {==}
390 case I.BpfTxa{}:
391 {==}
392 case I.BpfAlu{a, src}:
393 match a:
394 case I.BpfAdd{}:
395 match src:
396 case I.BpfK{k}:
397 {==}
398 case I.BpfX{}:
399 {==}
400 case I.BpfSub{}:
401 match src:
402 case I.BpfK{k}:
403 {==}
404 case I.BpfX{}:
405 {==}
406 case I.BpfMul{}:
407 match src:
408 case I.BpfK{k}:
409 {==}
410 case I.BpfX{}:
411 {==}
412 case I.BpfDiv{}:
413 match src:
414 case I.BpfK{k}:
415 {==}
416 case I.BpfX{}:
417 {==}
418 case I.BpfOr{}:
419 match src:
420 case I.BpfK{k}:
421 {==}
422 case I.BpfX{}:
423 {==}
424 case I.BpfAnd{}:
425 match src:
426 case I.BpfK{k}:
427 {==}
428 case I.BpfX{}:
429 {==}
430 case I.BpfLsh{}:
431 match src:
432 case I.BpfK{k}:
433 {==}
434 case I.BpfX{}:
435 {==}
436 case I.BpfRsh{}:
437 match src:
438 case I.BpfK{k}:
439 {==}
440 case I.BpfX{}:
441 {==}
442 case I.BpfMod{}:
443 match src:
444 case I.BpfK{k}:
445 {==}
446 case I.BpfX{}:
447 {==}
448 case I.BpfXor{}:
449 match src:
450 case I.BpfK{k}:
451 {==}
452 case I.BpfX{}:
453 {==}
454 case I.BpfJmp{c, src, jt, jf}:
455 match c:
456 case I.BpfJeq{}:
457 match src:
458 case I.BpfK{k}:
459 {==}
460 case I.BpfX{}:
461 {==}
462 case I.BpfJgt{}:
463 match src:
464 case I.BpfK{k}:
465 {==}
466 case I.BpfX{}:
467 {==}
468 case I.BpfJge{}:
469 match src:
470 case I.BpfK{k}:
471 {==}
472 case I.BpfX{}:
473 {==}
474 case I.BpfJset{}:
475 match src:
476 case I.BpfK{k}:
477 {==}
478 case I.BpfX{}:
479 {==}
480 case I.BpfRet{v}:
481 match v:
482 case I.BpfRetK{k}:
483 {==}
484 case I.BpfRetA{}:
485 {==}
486
487def decode_go(prog: List<&2, I.BpfOp>, +pc: Nat) -> {I.bpf_decode.ref.go(I.bpf_encode.ref(prog), pc) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
488 match prog:
489 case Nil{}:
490 {==}
491 case Con{+op, +t}:
492 %Equal.sym(Maybe<&2, I.BpfOp>, I.BpfRaw.decode(I.BpfOp.encode(op)), Some{op}, Laws.insn_round_trip(op)) : {I.bpf_decode.cons(_, I.BpfErrBadCode{pc, I.BpfRaw.code(I.BpfOp.encode(op))}, I.bpf_decode.ref.go(I.bpf_encode.ref(t), 1n+pc)) == Done{Con{op, t}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
493 %Equal.sym(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode.ref.go(I.bpf_encode.ref(t), 1n+pc), Done{t}, decode_go(t, 1n+pc)) : {I.bpf_decode.cons(Some{op}, I.BpfErrBadCode{pc, I.BpfRaw.code(I.BpfOp.encode(op))}, _) == Done{Con{op, t}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
494 {==}
495
496
497
498
499
500def rev_rr(-A: Data, xs: List<&2, A>, acc: List<&2, A>, b: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), b) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, b)) : List<&2, A>}:
501 match xs:
502 case Nil{}:
503 {==}
504 case Con{h, t}:
505 rev_rr(A, t, Con{h, acc}, b)
506
507def app_nil(-A: Data, +xs: List<&2, A>) -> {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}:
508 match xs:
509 case Nil{}:
510 {==}
511 case Con{h, t}:
512 Equal.cong(List<&2, A>, List<&2, A>, l => Con{h, l}, List.append(&2, A, t, Nil{}), t, app_nil(A, t))
513
514
515def rev_twice(-A: Data, +xs: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}) == xs : List<&2, A>}:
516 Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}), List.append(&2, A, xs, Nil{}), xs, rev_rr(A, xs, Nil{}, Nil{}), app_nil(A, xs))
517
518def g_encode(ops: List<&2, I.BpfOp>, acc: List<&2, I.BpfRaw>) -> {I.bpf_encode.go(ops, acc) == List.reverse.go(&2, I.BpfRaw, I.bpf_encode.ref(ops), acc) : List<&2, I.BpfRaw>}:
519 match ops:
520 case Nil{}:
521 {==}
522 case Con{op, t}:
523 g_encode(t, Con{I.BpfOp.encode(op), acc})
524
525def F_encode(+ops: List<&2, I.BpfOp>) -> {I.bpf_encode.ref(ops) == I.bpf_encode(ops) : List<&2, I.BpfRaw>}:
526 Equal.sym(List<&2, I.BpfRaw>, I.bpf_encode(ops), I.bpf_encode.ref(ops),
527 Equal.trans(List<&2, I.BpfRaw>, I.bpf_encode(ops), List.reverse.go(&2, I.BpfRaw, List.reverse.go(&2, I.BpfRaw, I.bpf_encode.ref(ops), Nil{}), Nil{}), I.bpf_encode.ref(ops),
528 Equal.cong(List<&2, I.BpfRaw>, List<&2, I.BpfRaw>, l => List.reverse.go(&2, I.BpfRaw, l, Nil{}), I.bpf_encode.go(ops, Nil{}), List.reverse.go(&2, I.BpfRaw, I.bpf_encode.ref(ops), Nil{}), g_encode(ops, Nil{})),
529 rev_twice(I.BpfRaw, I.bpf_encode.ref(ops))))
530
531
532
533def dec.after(acc: List<&2, I.BpfOp>, r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
534 match r:
535 case Fail{f}:
536 Fail{f}
537 case Done{ops}:
538 Done{List.reverse.go(&2, I.BpfOp, acc, ops)}
539
540def dec.after2(a: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
541 match a:
542 case Fail{e}:
543 Fail{e}
544 case Done{acc}:
545 dec.after(acc, r)
546
547def dec_step(m: Maybe<&2, I.BpfOp>, -e: I.BpfError, -acc: List<&2, I.BpfOp>, r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {dec.after2(I.bpf_decode.push(m, e, acc), r) == dec.after(acc, I.bpf_decode.cons(m, e, r)) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
548 match m:
549 case None{}:
550 {==}
551 case Some{op}:
552 match r:
553 case Fail{f}:
554 {==}
555 case Done{ops}:
556 {==}
557
558def g_decode(rs: List<&2, I.BpfRaw>, +pc: Nat, a: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {I.bpf_decode.go(rs, pc, a) == dec.after2(a, I.bpf_decode.ref.go(rs, pc)) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
559 match rs:
560 case Nil{}:
561 match a:
562 case Fail{e}:
563 {==}
564 case Done{acc}:
565 {==}
566 case Con{+r, +t}:
567 match a:
568 case Fail{e}:
569 {==}
570 case Done{+acc}:
571 Equal.trans(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode.go(t, 1n+pc, I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc)), dec.after2(I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc), I.bpf_decode.ref.go(t, 1n+pc)), dec.after(acc, I.bpf_decode.cons(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, I.bpf_decode.ref.go(t, 1n+pc))),
572 g_decode(t, 1n+pc, I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc)), dec_step(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc, I.bpf_decode.ref.go(t, 1n+pc)))
573
574def dec_nil(r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {dec.after(Nil{}, r) == r : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
575 match r:
576 case Fail{f}:
577 {==}
578 case Done{ops}:
579 {==}
580
581def F_decode(+rs: List<&2, I.BpfRaw>) -> {I.bpf_decode.ref(rs) == I.bpf_decode(rs) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
582 Equal.sym(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode(rs), I.bpf_decode.ref(rs),
583 Equal.trans(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode(rs), dec.after(Nil{}, I.bpf_decode.ref.go(rs, 0n)), I.bpf_decode.ref.go(rs, 0n),
584 g_decode(rs, 0n, Done{Nil{}}), dec_nil(I.bpf_decode.ref.go(rs, 0n))))
585
586def Laws.program_round_trip(prog):
587 %F_encode(prog) : {I.bpf_decode(_) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
588 %F_decode(I.bpf_encode.ref(prog)) : {_ == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
589 decode_go(prog, 0n)
590
591
592
593
594def Laws.octets_over_limit(max, order, o, b, e):
595 %Equal.sym(Maybe<&2, U32>, B.Octets.at(o, max), Some{b}, e) : {I.bpf_of_octets.fits(_, max, order, o) == Fail{I.BpfErrStoredTooLong{max}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
596 {==}
597
598def Laws.most_restrictive(a, b):
599 match a:
600 case S.SeccompKillProcess{}:
601 match b:
602 case S.SeccompKillProcess{}:
603 {==}
604 case S.SeccompKillThread{}:
605 {==}
606 case S.SeccompTrap{db}:
607 {==}
608 case S.SeccompErrno{db}:
609 {==}
610 case S.SeccompUserNotif{}:
611 {==}
612 case S.SeccompTrace{db}:
613 {==}
614 case S.SeccompLog{}:
615 {==}
616 case S.SeccompAllow{}:
617 {==}
618 case S.SeccompKillThread{}:
619 match b:
620 case S.SeccompKillProcess{}:
621 {==}
622 case S.SeccompKillThread{}:
623 {==}
624 case S.SeccompTrap{db}:
625 {==}
626 case S.SeccompErrno{db}:
627 {==}
628 case S.SeccompUserNotif{}:
629 {==}
630 case S.SeccompTrace{db}:
631 {==}
632 case S.SeccompLog{}:
633 {==}
634 case S.SeccompAllow{}:
635 {==}
636 case S.SeccompTrap{da}:
637 match b:
638 case S.SeccompKillProcess{}:
639 {==}
640 case S.SeccompKillThread{}:
641 {==}
642 case S.SeccompTrap{db}:
643 {==}
644 case S.SeccompErrno{db}:
645 {==}
646 case S.SeccompUserNotif{}:
647 {==}
648 case S.SeccompTrace{db}:
649 {==}
650 case S.SeccompLog{}:
651 {==}
652 case S.SeccompAllow{}:
653 {==}
654 case S.SeccompErrno{da}:
655 match b:
656 case S.SeccompKillProcess{}:
657 {==}
658 case S.SeccompKillThread{}:
659 {==}
660 case S.SeccompTrap{db}:
661 {==}
662 case S.SeccompErrno{db}:
663 {==}
664 case S.SeccompUserNotif{}:
665 {==}
666 case S.SeccompTrace{db}:
667 {==}
668 case S.SeccompLog{}:
669 {==}
670 case S.SeccompAllow{}:
671 {==}
672 case S.SeccompUserNotif{}:
673 match b:
674 case S.SeccompKillProcess{}:
675 {==}
676 case S.SeccompKillThread{}:
677 {==}
678 case S.SeccompTrap{db}:
679 {==}
680 case S.SeccompErrno{db}:
681 {==}
682 case S.SeccompUserNotif{}:
683 {==}
684 case S.SeccompTrace{db}:
685 {==}
686 case S.SeccompLog{}:
687 {==}
688 case S.SeccompAllow{}:
689 {==}
690 case S.SeccompTrace{da}:
691 match b:
692 case S.SeccompKillProcess{}:
693 {==}
694 case S.SeccompKillThread{}:
695 {==}
696 case S.SeccompTrap{db}:
697 {==}
698 case S.SeccompErrno{db}:
699 {==}
700 case S.SeccompUserNotif{}:
701 {==}
702 case S.SeccompTrace{db}:
703 {==}
704 case S.SeccompLog{}:
705 {==}
706 case S.SeccompAllow{}:
707 {==}
708 case S.SeccompLog{}:
709 match b:
710 case S.SeccompKillProcess{}:
711 {==}
712 case S.SeccompKillThread{}:
713 {==}
714 case S.SeccompTrap{db}:
715 {==}
716 case S.SeccompErrno{db}:
717 {==}
718 case S.SeccompUserNotif{}:
719 {==}
720 case S.SeccompTrace{db}:
721 {==}
722 case S.SeccompLog{}:
723 {==}
724 case S.SeccompAllow{}:
725 {==}
726 case S.SeccompAllow{}:
727 match b:
728 case S.SeccompKillProcess{}:
729 {==}
730 case S.SeccompKillThread{}:
731 {==}
732 case S.SeccompTrap{db}:
733 {==}
734 case S.SeccompErrno{db}:
735 {==}
736 case S.SeccompUserNotif{}:
737 {==}
738 case S.SeccompTrace{db}:
739 {==}
740 case S.SeccompLog{}:
741 {==}
742 case S.SeccompAllow{}:
743 {==}
744
745def Laws.combine_assoc(a, b, c):
746 match a:
747 case S.SeccompKillProcess{}:
748 match b:
749 case S.SeccompKillProcess{}:
750 match c:
751 case S.SeccompKillProcess{}:
752 {==}
753 case S.SeccompKillThread{}:
754 {==}
755 case S.SeccompTrap{dc}:
756 {==}
757 case S.SeccompErrno{dc}:
758 {==}
759 case S.SeccompUserNotif{}:
760 {==}
761 case S.SeccompTrace{dc}:
762 {==}
763 case S.SeccompLog{}:
764 {==}
765 case S.SeccompAllow{}:
766 {==}
767 case S.SeccompKillThread{}:
768 match c:
769 case S.SeccompKillProcess{}:
770 {==}
771 case S.SeccompKillThread{}:
772 {==}
773 case S.SeccompTrap{dc}:
774 {==}
775 case S.SeccompErrno{dc}:
776 {==}
777 case S.SeccompUserNotif{}:
778 {==}
779 case S.SeccompTrace{dc}:
780 {==}
781 case S.SeccompLog{}:
782 {==}
783 case S.SeccompAllow{}:
784 {==}
785 case S.SeccompTrap{db}:
786 match c:
787 case S.SeccompKillProcess{}:
788 {==}
789 case S.SeccompKillThread{}:
790 {==}
791 case S.SeccompTrap{dc}:
792 {==}
793 case S.SeccompErrno{dc}:
794 {==}
795 case S.SeccompUserNotif{}:
796 {==}
797 case S.SeccompTrace{dc}:
798 {==}
799 case S.SeccompLog{}:
800 {==}
801 case S.SeccompAllow{}:
802 {==}
803 case S.SeccompErrno{db}:
804 match c:
805 case S.SeccompKillProcess{}:
806 {==}
807 case S.SeccompKillThread{}:
808 {==}
809 case S.SeccompTrap{dc}:
810 {==}
811 case S.SeccompErrno{dc}:
812 {==}
813 case S.SeccompUserNotif{}:
814 {==}
815 case S.SeccompTrace{dc}:
816 {==}
817 case S.SeccompLog{}:
818 {==}
819 case S.SeccompAllow{}:
820 {==}
821 case S.SeccompUserNotif{}:
822 match c:
823 case S.SeccompKillProcess{}:
824 {==}
825 case S.SeccompKillThread{}:
826 {==}
827 case S.SeccompTrap{dc}:
828 {==}
829 case S.SeccompErrno{dc}:
830 {==}
831 case S.SeccompUserNotif{}:
832 {==}
833 case S.SeccompTrace{dc}:
834 {==}
835 case S.SeccompLog{}:
836 {==}
837 case S.SeccompAllow{}:
838 {==}
839 case S.SeccompTrace{db}:
840 match c:
841 case S.SeccompKillProcess{}:
842 {==}
843 case S.SeccompKillThread{}:
844 {==}
845 case S.SeccompTrap{dc}:
846 {==}
847 case S.SeccompErrno{dc}:
848 {==}
849 case S.SeccompUserNotif{}:
850 {==}
851 case S.SeccompTrace{dc}:
852 {==}
853 case S.SeccompLog{}:
854 {==}
855 case S.SeccompAllow{}:
856 {==}
857 case S.SeccompLog{}:
858 match c:
859 case S.SeccompKillProcess{}:
860 {==}
861 case S.SeccompKillThread{}:
862 {==}
863 case S.SeccompTrap{dc}:
864 {==}
865 case S.SeccompErrno{dc}:
866 {==}
867 case S.SeccompUserNotif{}:
868 {==}
869 case S.SeccompTrace{dc}:
870 {==}
871 case S.SeccompLog{}:
872 {==}
873 case S.SeccompAllow{}:
874 {==}
875 case S.SeccompAllow{}:
876 match c:
877 case S.SeccompKillProcess{}:
878 {==}
879 case S.SeccompKillThread{}:
880 {==}
881 case S.SeccompTrap{dc}:
882 {==}
883 case S.SeccompErrno{dc}:
884 {==}
885 case S.SeccompUserNotif{}:
886 {==}
887 case S.SeccompTrace{dc}:
888 {==}
889 case S.SeccompLog{}:
890 {==}
891 case S.SeccompAllow{}:
892 {==}
893 case S.SeccompKillThread{}:
894 match b:
895 case S.SeccompKillProcess{}:
896 match c:
897 case S.SeccompKillProcess{}:
898 {==}
899 case S.SeccompKillThread{}:
900 {==}
901 case S.SeccompTrap{dc}:
902 {==}
903 case S.SeccompErrno{dc}:
904 {==}
905 case S.SeccompUserNotif{}:
906 {==}
907 case S.SeccompTrace{dc}:
908 {==}
909 case S.SeccompLog{}:
910 {==}
911 case S.SeccompAllow{}:
912 {==}
913 case S.SeccompKillThread{}:
914 match c:
915 case S.SeccompKillProcess{}:
916 {==}
917 case S.SeccompKillThread{}:
918 {==}
919 case S.SeccompTrap{dc}:
920 {==}
921 case S.SeccompErrno{dc}:
922 {==}
923 case S.SeccompUserNotif{}:
924 {==}
925 case S.SeccompTrace{dc}:
926 {==}
927 case S.SeccompLog{}:
928 {==}
929 case S.SeccompAllow{}:
930 {==}
931 case S.SeccompTrap{db}:
932 match c:
933 case S.SeccompKillProcess{}:
934 {==}
935 case S.SeccompKillThread{}:
936 {==}
937 case S.SeccompTrap{dc}:
938 {==}
939 case S.SeccompErrno{dc}:
940 {==}
941 case S.SeccompUserNotif{}:
942 {==}
943 case S.SeccompTrace{dc}:
944 {==}
945 case S.SeccompLog{}:
946 {==}
947 case S.SeccompAllow{}:
948 {==}
949 case S.SeccompErrno{db}:
950 match c:
951 case S.SeccompKillProcess{}:
952 {==}
953 case S.SeccompKillThread{}:
954 {==}
955 case S.SeccompTrap{dc}:
956 {==}
957 case S.SeccompErrno{dc}:
958 {==}
959 case S.SeccompUserNotif{}:
960 {==}
961 case S.SeccompTrace{dc}:
962 {==}
963 case S.SeccompLog{}:
964 {==}
965 case S.SeccompAllow{}:
966 {==}
967 case S.SeccompUserNotif{}:
968 match c:
969 case S.SeccompKillProcess{}:
970 {==}
971 case S.SeccompKillThread{}:
972 {==}
973 case S.SeccompTrap{dc}:
974 {==}
975 case S.SeccompErrno{dc}:
976 {==}
977 case S.SeccompUserNotif{}:
978 {==}
979 case S.SeccompTrace{dc}:
980 {==}
981 case S.SeccompLog{}:
982 {==}
983 case S.SeccompAllow{}:
984 {==}
985 case S.SeccompTrace{db}:
986 match c:
987 case S.SeccompKillProcess{}:
988 {==}
989 case S.SeccompKillThread{}:
990 {==}
991 case S.SeccompTrap{dc}:
992 {==}
993 case S.SeccompErrno{dc}:
994 {==}
995 case S.SeccompUserNotif{}:
996 {==}
997 case S.SeccompTrace{dc}:
998 {==}
999 case S.SeccompLog{}:
1000 {==}
1001 case S.SeccompAllow{}:
1002 {==}
1003 case S.SeccompLog{}:
1004 match c:
1005 case S.SeccompKillProcess{}:
1006 {==}
1007 case S.SeccompKillThread{}:
1008 {==}
1009 case S.SeccompTrap{dc}:
1010 {==}
1011 case S.SeccompErrno{dc}:
1012 {==}
1013 case S.SeccompUserNotif{}:
1014 {==}
1015 case S.SeccompTrace{dc}:
1016 {==}
1017 case S.SeccompLog{}:
1018 {==}
1019 case S.SeccompAllow{}:
1020 {==}
1021 case S.SeccompAllow{}:
1022 match c:
1023 case S.SeccompKillProcess{}:
1024 {==}
1025 case S.SeccompKillThread{}:
1026 {==}
1027 case S.SeccompTrap{dc}:
1028 {==}
1029 case S.SeccompErrno{dc}:
1030 {==}
1031 case S.SeccompUserNotif{}:
1032 {==}
1033 case S.SeccompTrace{dc}:
1034 {==}
1035 case S.SeccompLog{}:
1036 {==}
1037 case S.SeccompAllow{}:
1038 {==}
1039 case S.SeccompTrap{da}:
1040 match b:
1041 case S.SeccompKillProcess{}:
1042 match c:
1043 case S.SeccompKillProcess{}:
1044 {==}
1045 case S.SeccompKillThread{}:
1046 {==}
1047 case S.SeccompTrap{dc}:
1048 {==}
1049 case S.SeccompErrno{dc}:
1050 {==}
1051 case S.SeccompUserNotif{}:
1052 {==}
1053 case S.SeccompTrace{dc}:
1054 {==}
1055 case S.SeccompLog{}:
1056 {==}
1057 case S.SeccompAllow{}:
1058 {==}
1059 case S.SeccompKillThread{}:
1060 match c:
1061 case S.SeccompKillProcess{}:
1062 {==}
1063 case S.SeccompKillThread{}:
1064 {==}
1065 case S.SeccompTrap{dc}:
1066 {==}
1067 case S.SeccompErrno{dc}:
1068 {==}
1069 case S.SeccompUserNotif{}:
1070 {==}
1071 case S.SeccompTrace{dc}:
1072 {==}
1073 case S.SeccompLog{}:
1074 {==}
1075 case S.SeccompAllow{}:
1076 {==}
1077 case S.SeccompTrap{db}:
1078 match c:
1079 case S.SeccompKillProcess{}:
1080 {==}
1081 case S.SeccompKillThread{}:
1082 {==}
1083 case S.SeccompTrap{dc}:
1084 {==}
1085 case S.SeccompErrno{dc}:
1086 {==}
1087 case S.SeccompUserNotif{}:
1088 {==}
1089 case S.SeccompTrace{dc}:
1090 {==}
1091 case S.SeccompLog{}:
1092 {==}
1093 case S.SeccompAllow{}:
1094 {==}
1095 case S.SeccompErrno{db}:
1096 match c:
1097 case S.SeccompKillProcess{}:
1098 {==}
1099 case S.SeccompKillThread{}:
1100 {==}
1101 case S.SeccompTrap{dc}:
1102 {==}
1103 case S.SeccompErrno{dc}:
1104 {==}
1105 case S.SeccompUserNotif{}:
1106 {==}
1107 case S.SeccompTrace{dc}:
1108 {==}
1109 case S.SeccompLog{}:
1110 {==}
1111 case S.SeccompAllow{}:
1112 {==}
1113 case S.SeccompUserNotif{}:
1114 match c:
1115 case S.SeccompKillProcess{}:
1116 {==}
1117 case S.SeccompKillThread{}:
1118 {==}
1119 case S.SeccompTrap{dc}:
1120 {==}
1121 case S.SeccompErrno{dc}:
1122 {==}
1123 case S.SeccompUserNotif{}:
1124 {==}
1125 case S.SeccompTrace{dc}:
1126 {==}
1127 case S.SeccompLog{}:
1128 {==}
1129 case S.SeccompAllow{}:
1130 {==}
1131 case S.SeccompTrace{db}:
1132 match c:
1133 case S.SeccompKillProcess{}:
1134 {==}
1135 case S.SeccompKillThread{}:
1136 {==}
1137 case S.SeccompTrap{dc}:
1138 {==}
1139 case S.SeccompErrno{dc}:
1140 {==}
1141 case S.SeccompUserNotif{}:
1142 {==}
1143 case S.SeccompTrace{dc}:
1144 {==}
1145 case S.SeccompLog{}:
1146 {==}
1147 case S.SeccompAllow{}:
1148 {==}
1149 case S.SeccompLog{}:
1150 match c:
1151 case S.SeccompKillProcess{}:
1152 {==}
1153 case S.SeccompKillThread{}:
1154 {==}
1155 case S.SeccompTrap{dc}:
1156 {==}
1157 case S.SeccompErrno{dc}:
1158 {==}
1159 case S.SeccompUserNotif{}:
1160 {==}
1161 case S.SeccompTrace{dc}:
1162 {==}
1163 case S.SeccompLog{}:
1164 {==}
1165 case S.SeccompAllow{}:
1166 {==}
1167 case S.SeccompAllow{}:
1168 match c:
1169 case S.SeccompKillProcess{}:
1170 {==}
1171 case S.SeccompKillThread{}:
1172 {==}
1173 case S.SeccompTrap{dc}:
1174 {==}
1175 case S.SeccompErrno{dc}:
1176 {==}
1177 case S.SeccompUserNotif{}:
1178 {==}
1179 case S.SeccompTrace{dc}:
1180 {==}
1181 case S.SeccompLog{}:
1182 {==}
1183 case S.SeccompAllow{}:
1184 {==}
1185 case S.SeccompErrno{da}:
1186 match b:
1187 case S.SeccompKillProcess{}:
1188 match c:
1189 case S.SeccompKillProcess{}:
1190 {==}
1191 case S.SeccompKillThread{}:
1192 {==}
1193 case S.SeccompTrap{dc}:
1194 {==}
1195 case S.SeccompErrno{dc}:
1196 {==}
1197 case S.SeccompUserNotif{}:
1198 {==}
1199 case S.SeccompTrace{dc}:
1200 {==}
1201 case S.SeccompLog{}:
1202 {==}
1203 case S.SeccompAllow{}:
1204 {==}
1205 case S.SeccompKillThread{}:
1206 match c:
1207 case S.SeccompKillProcess{}:
1208 {==}
1209 case S.SeccompKillThread{}:
1210 {==}
1211 case S.SeccompTrap{dc}:
1212 {==}
1213 case S.SeccompErrno{dc}:
1214 {==}
1215 case S.SeccompUserNotif{}:
1216 {==}
1217 case S.SeccompTrace{dc}:
1218 {==}
1219 case S.SeccompLog{}:
1220 {==}
1221 case S.SeccompAllow{}:
1222 {==}
1223 case S.SeccompTrap{db}:
1224 match c:
1225 case S.SeccompKillProcess{}:
1226 {==}
1227 case S.SeccompKillThread{}:
1228 {==}
1229 case S.SeccompTrap{dc}:
1230 {==}
1231 case S.SeccompErrno{dc}:
1232 {==}
1233 case S.SeccompUserNotif{}:
1234 {==}
1235 case S.SeccompTrace{dc}:
1236 {==}
1237 case S.SeccompLog{}:
1238 {==}
1239 case S.SeccompAllow{}:
1240 {==}
1241 case S.SeccompErrno{db}:
1242 match c:
1243 case S.SeccompKillProcess{}:
1244 {==}
1245 case S.SeccompKillThread{}:
1246 {==}
1247 case S.SeccompTrap{dc}:
1248 {==}
1249 case S.SeccompErrno{dc}:
1250 {==}
1251 case S.SeccompUserNotif{}:
1252 {==}
1253 case S.SeccompTrace{dc}:
1254 {==}
1255 case S.SeccompLog{}:
1256 {==}
1257 case S.SeccompAllow{}:
1258 {==}
1259 case S.SeccompUserNotif{}:
1260 match c:
1261 case S.SeccompKillProcess{}:
1262 {==}
1263 case S.SeccompKillThread{}:
1264 {==}
1265 case S.SeccompTrap{dc}:
1266 {==}
1267 case S.SeccompErrno{dc}:
1268 {==}
1269 case S.SeccompUserNotif{}:
1270 {==}
1271 case S.SeccompTrace{dc}:
1272 {==}
1273 case S.SeccompLog{}:
1274 {==}
1275 case S.SeccompAllow{}:
1276 {==}
1277 case S.SeccompTrace{db}:
1278 match c:
1279 case S.SeccompKillProcess{}:
1280 {==}
1281 case S.SeccompKillThread{}:
1282 {==}
1283 case S.SeccompTrap{dc}:
1284 {==}
1285 case S.SeccompErrno{dc}:
1286 {==}
1287 case S.SeccompUserNotif{}:
1288 {==}
1289 case S.SeccompTrace{dc}:
1290 {==}
1291 case S.SeccompLog{}:
1292 {==}
1293 case S.SeccompAllow{}:
1294 {==}
1295 case S.SeccompLog{}:
1296 match c:
1297 case S.SeccompKillProcess{}:
1298 {==}
1299 case S.SeccompKillThread{}:
1300 {==}
1301 case S.SeccompTrap{dc}:
1302 {==}
1303 case S.SeccompErrno{dc}:
1304 {==}
1305 case S.SeccompUserNotif{}:
1306 {==}
1307 case S.SeccompTrace{dc}:
1308 {==}
1309 case S.SeccompLog{}:
1310 {==}
1311 case S.SeccompAllow{}:
1312 {==}
1313 case S.SeccompAllow{}:
1314 match c:
1315 case S.SeccompKillProcess{}:
1316 {==}
1317 case S.SeccompKillThread{}:
1318 {==}
1319 case S.SeccompTrap{dc}:
1320 {==}
1321 case S.SeccompErrno{dc}:
1322 {==}
1323 case S.SeccompUserNotif{}:
1324 {==}
1325 case S.SeccompTrace{dc}:
1326 {==}
1327 case S.SeccompLog{}:
1328 {==}
1329 case S.SeccompAllow{}:
1330 {==}
1331 case S.SeccompUserNotif{}:
1332 match b:
1333 case S.SeccompKillProcess{}:
1334 match c:
1335 case S.SeccompKillProcess{}:
1336 {==}
1337 case S.SeccompKillThread{}:
1338 {==}
1339 case S.SeccompTrap{dc}:
1340 {==}
1341 case S.SeccompErrno{dc}:
1342 {==}
1343 case S.SeccompUserNotif{}:
1344 {==}
1345 case S.SeccompTrace{dc}:
1346 {==}
1347 case S.SeccompLog{}:
1348 {==}
1349 case S.SeccompAllow{}:
1350 {==}
1351 case S.SeccompKillThread{}:
1352 match c:
1353 case S.SeccompKillProcess{}:
1354 {==}
1355 case S.SeccompKillThread{}:
1356 {==}
1357 case S.SeccompTrap{dc}:
1358 {==}
1359 case S.SeccompErrno{dc}:
1360 {==}
1361 case S.SeccompUserNotif{}:
1362 {==}
1363 case S.SeccompTrace{dc}:
1364 {==}
1365 case S.SeccompLog{}:
1366 {==}
1367 case S.SeccompAllow{}:
1368 {==}
1369 case S.SeccompTrap{db}:
1370 match c:
1371 case S.SeccompKillProcess{}:
1372 {==}
1373 case S.SeccompKillThread{}:
1374 {==}
1375 case S.SeccompTrap{dc}:
1376 {==}
1377 case S.SeccompErrno{dc}:
1378 {==}
1379 case S.SeccompUserNotif{}:
1380 {==}
1381 case S.SeccompTrace{dc}:
1382 {==}
1383 case S.SeccompLog{}:
1384 {==}
1385 case S.SeccompAllow{}:
1386 {==}
1387 case S.SeccompErrno{db}:
1388 match c:
1389 case S.SeccompKillProcess{}:
1390 {==}
1391 case S.SeccompKillThread{}:
1392 {==}
1393 case S.SeccompTrap{dc}:
1394 {==}
1395 case S.SeccompErrno{dc}:
1396 {==}
1397 case S.SeccompUserNotif{}:
1398 {==}
1399 case S.SeccompTrace{dc}:
1400 {==}
1401 case S.SeccompLog{}:
1402 {==}
1403 case S.SeccompAllow{}:
1404 {==}
1405 case S.SeccompUserNotif{}:
1406 match c:
1407 case S.SeccompKillProcess{}:
1408 {==}
1409 case S.SeccompKillThread{}:
1410 {==}
1411 case S.SeccompTrap{dc}:
1412 {==}
1413 case S.SeccompErrno{dc}:
1414 {==}
1415 case S.SeccompUserNotif{}:
1416 {==}
1417 case S.SeccompTrace{dc}:
1418 {==}
1419 case S.SeccompLog{}:
1420 {==}
1421 case S.SeccompAllow{}:
1422 {==}
1423 case S.SeccompTrace{db}:
1424 match c:
1425 case S.SeccompKillProcess{}:
1426 {==}
1427 case S.SeccompKillThread{}:
1428 {==}
1429 case S.SeccompTrap{dc}:
1430 {==}
1431 case S.SeccompErrno{dc}:
1432 {==}
1433 case S.SeccompUserNotif{}:
1434 {==}
1435 case S.SeccompTrace{dc}:
1436 {==}
1437 case S.SeccompLog{}:
1438 {==}
1439 case S.SeccompAllow{}:
1440 {==}
1441 case S.SeccompLog{}:
1442 match c:
1443 case S.SeccompKillProcess{}:
1444 {==}
1445 case S.SeccompKillThread{}:
1446 {==}
1447 case S.SeccompTrap{dc}:
1448 {==}
1449 case S.SeccompErrno{dc}:
1450 {==}
1451 case S.SeccompUserNotif{}:
1452 {==}
1453 case S.SeccompTrace{dc}:
1454 {==}
1455 case S.SeccompLog{}:
1456 {==}
1457 case S.SeccompAllow{}:
1458 {==}
1459 case S.SeccompAllow{}:
1460 match c:
1461 case S.SeccompKillProcess{}:
1462 {==}
1463 case S.SeccompKillThread{}:
1464 {==}
1465 case S.SeccompTrap{dc}:
1466 {==}
1467 case S.SeccompErrno{dc}:
1468 {==}
1469 case S.SeccompUserNotif{}:
1470 {==}
1471 case S.SeccompTrace{dc}:
1472 {==}
1473 case S.SeccompLog{}:
1474 {==}
1475 case S.SeccompAllow{}:
1476 {==}
1477 case S.SeccompTrace{da}:
1478 match b:
1479 case S.SeccompKillProcess{}:
1480 match c:
1481 case S.SeccompKillProcess{}:
1482 {==}
1483 case S.SeccompKillThread{}:
1484 {==}
1485 case S.SeccompTrap{dc}:
1486 {==}
1487 case S.SeccompErrno{dc}:
1488 {==}
1489 case S.SeccompUserNotif{}:
1490 {==}
1491 case S.SeccompTrace{dc}:
1492 {==}
1493 case S.SeccompLog{}:
1494 {==}
1495 case S.SeccompAllow{}:
1496 {==}
1497 case S.SeccompKillThread{}:
1498 match c:
1499 case S.SeccompKillProcess{}:
1500 {==}
1501 case S.SeccompKillThread{}:
1502 {==}
1503 case S.SeccompTrap{dc}:
1504 {==}
1505 case S.SeccompErrno{dc}:
1506 {==}
1507 case S.SeccompUserNotif{}:
1508 {==}
1509 case S.SeccompTrace{dc}:
1510 {==}
1511 case S.SeccompLog{}:
1512 {==}
1513 case S.SeccompAllow{}:
1514 {==}
1515 case S.SeccompTrap{db}:
1516 match c:
1517 case S.SeccompKillProcess{}:
1518 {==}
1519 case S.SeccompKillThread{}:
1520 {==}
1521 case S.SeccompTrap{dc}:
1522 {==}
1523 case S.SeccompErrno{dc}:
1524 {==}
1525 case S.SeccompUserNotif{}:
1526 {==}
1527 case S.SeccompTrace{dc}:
1528 {==}
1529 case S.SeccompLog{}:
1530 {==}
1531 case S.SeccompAllow{}:
1532 {==}
1533 case S.SeccompErrno{db}:
1534 match c:
1535 case S.SeccompKillProcess{}:
1536 {==}
1537 case S.SeccompKillThread{}:
1538 {==}
1539 case S.SeccompTrap{dc}:
1540 {==}
1541 case S.SeccompErrno{dc}:
1542 {==}
1543 case S.SeccompUserNotif{}:
1544 {==}
1545 case S.SeccompTrace{dc}:
1546 {==}
1547 case S.SeccompLog{}:
1548 {==}
1549 case S.SeccompAllow{}:
1550 {==}
1551 case S.SeccompUserNotif{}:
1552 match c:
1553 case S.SeccompKillProcess{}:
1554 {==}
1555 case S.SeccompKillThread{}:
1556 {==}
1557 case S.SeccompTrap{dc}:
1558 {==}
1559 case S.SeccompErrno{dc}:
1560 {==}
1561 case S.SeccompUserNotif{}:
1562 {==}
1563 case S.SeccompTrace{dc}:
1564 {==}
1565 case S.SeccompLog{}:
1566 {==}
1567 case S.SeccompAllow{}:
1568 {==}
1569 case S.SeccompTrace{db}:
1570 match c:
1571 case S.SeccompKillProcess{}:
1572 {==}
1573 case S.SeccompKillThread{}:
1574 {==}
1575 case S.SeccompTrap{dc}:
1576 {==}
1577 case S.SeccompErrno{dc}:
1578 {==}
1579 case S.SeccompUserNotif{}:
1580 {==}
1581 case S.SeccompTrace{dc}:
1582 {==}
1583 case S.SeccompLog{}:
1584 {==}
1585 case S.SeccompAllow{}:
1586 {==}
1587 case S.SeccompLog{}:
1588 match c:
1589 case S.SeccompKillProcess{}:
1590 {==}
1591 case S.SeccompKillThread{}:
1592 {==}
1593 case S.SeccompTrap{dc}:
1594 {==}
1595 case S.SeccompErrno{dc}:
1596 {==}
1597 case S.SeccompUserNotif{}:
1598 {==}
1599 case S.SeccompTrace{dc}:
1600 {==}
1601 case S.SeccompLog{}:
1602 {==}
1603 case S.SeccompAllow{}:
1604 {==}
1605 case S.SeccompAllow{}:
1606 match c:
1607 case S.SeccompKillProcess{}:
1608 {==}
1609 case S.SeccompKillThread{}:
1610 {==}
1611 case S.SeccompTrap{dc}:
1612 {==}
1613 case S.SeccompErrno{dc}:
1614 {==}
1615 case S.SeccompUserNotif{}:
1616 {==}
1617 case S.SeccompTrace{dc}:
1618 {==}
1619 case S.SeccompLog{}:
1620 {==}
1621 case S.SeccompAllow{}:
1622 {==}
1623 case S.SeccompLog{}:
1624 match b:
1625 case S.SeccompKillProcess{}:
1626 match c:
1627 case S.SeccompKillProcess{}:
1628 {==}
1629 case S.SeccompKillThread{}:
1630 {==}
1631 case S.SeccompTrap{dc}:
1632 {==}
1633 case S.SeccompErrno{dc}:
1634 {==}
1635 case S.SeccompUserNotif{}:
1636 {==}
1637 case S.SeccompTrace{dc}:
1638 {==}
1639 case S.SeccompLog{}:
1640 {==}
1641 case S.SeccompAllow{}:
1642 {==}
1643 case S.SeccompKillThread{}:
1644 match c:
1645 case S.SeccompKillProcess{}:
1646 {==}
1647 case S.SeccompKillThread{}:
1648 {==}
1649 case S.SeccompTrap{dc}:
1650 {==}
1651 case S.SeccompErrno{dc}:
1652 {==}
1653 case S.SeccompUserNotif{}:
1654 {==}
1655 case S.SeccompTrace{dc}:
1656 {==}
1657 case S.SeccompLog{}:
1658 {==}
1659 case S.SeccompAllow{}:
1660 {==}
1661 case S.SeccompTrap{db}:
1662 match c:
1663 case S.SeccompKillProcess{}:
1664 {==}
1665 case S.SeccompKillThread{}:
1666 {==}
1667 case S.SeccompTrap{dc}:
1668 {==}
1669 case S.SeccompErrno{dc}:
1670 {==}
1671 case S.SeccompUserNotif{}:
1672 {==}
1673 case S.SeccompTrace{dc}:
1674 {==}
1675 case S.SeccompLog{}:
1676 {==}
1677 case S.SeccompAllow{}:
1678 {==}
1679 case S.SeccompErrno{db}:
1680 match c:
1681 case S.SeccompKillProcess{}:
1682 {==}
1683 case S.SeccompKillThread{}:
1684 {==}
1685 case S.SeccompTrap{dc}:
1686 {==}
1687 case S.SeccompErrno{dc}:
1688 {==}
1689 case S.SeccompUserNotif{}:
1690 {==}
1691 case S.SeccompTrace{dc}:
1692 {==}
1693 case S.SeccompLog{}:
1694 {==}
1695 case S.SeccompAllow{}:
1696 {==}
1697 case S.SeccompUserNotif{}:
1698 match c:
1699 case S.SeccompKillProcess{}:
1700 {==}
1701 case S.SeccompKillThread{}:
1702 {==}
1703 case S.SeccompTrap{dc}:
1704 {==}
1705 case S.SeccompErrno{dc}:
1706 {==}
1707 case S.SeccompUserNotif{}:
1708 {==}
1709 case S.SeccompTrace{dc}:
1710 {==}
1711 case S.SeccompLog{}:
1712 {==}
1713 case S.SeccompAllow{}:
1714 {==}
1715 case S.SeccompTrace{db}:
1716 match c:
1717 case S.SeccompKillProcess{}:
1718 {==}
1719 case S.SeccompKillThread{}:
1720 {==}
1721 case S.SeccompTrap{dc}:
1722 {==}
1723 case S.SeccompErrno{dc}:
1724 {==}
1725 case S.SeccompUserNotif{}:
1726 {==}
1727 case S.SeccompTrace{dc}:
1728 {==}
1729 case S.SeccompLog{}:
1730 {==}
1731 case S.SeccompAllow{}:
1732 {==}
1733 case S.SeccompLog{}:
1734 match c:
1735 case S.SeccompKillProcess{}:
1736 {==}
1737 case S.SeccompKillThread{}:
1738 {==}
1739 case S.SeccompTrap{dc}:
1740 {==}
1741 case S.SeccompErrno{dc}:
1742 {==}
1743 case S.SeccompUserNotif{}:
1744 {==}
1745 case S.SeccompTrace{dc}:
1746 {==}
1747 case S.SeccompLog{}:
1748 {==}
1749 case S.SeccompAllow{}:
1750 {==}
1751 case S.SeccompAllow{}:
1752 match c:
1753 case S.SeccompKillProcess{}:
1754 {==}
1755 case S.SeccompKillThread{}:
1756 {==}
1757 case S.SeccompTrap{dc}:
1758 {==}
1759 case S.SeccompErrno{dc}:
1760 {==}
1761 case S.SeccompUserNotif{}:
1762 {==}
1763 case S.SeccompTrace{dc}:
1764 {==}
1765 case S.SeccompLog{}:
1766 {==}
1767 case S.SeccompAllow{}:
1768 {==}
1769 case S.SeccompAllow{}:
1770 match b:
1771 case S.SeccompKillProcess{}:
1772 match c:
1773 case S.SeccompKillProcess{}:
1774 {==}
1775 case S.SeccompKillThread{}:
1776 {==}
1777 case S.SeccompTrap{dc}:
1778 {==}
1779 case S.SeccompErrno{dc}:
1780 {==}
1781 case S.SeccompUserNotif{}:
1782 {==}
1783 case S.SeccompTrace{dc}:
1784 {==}
1785 case S.SeccompLog{}:
1786 {==}
1787 case S.SeccompAllow{}:
1788 {==}
1789 case S.SeccompKillThread{}:
1790 match c:
1791 case S.SeccompKillProcess{}:
1792 {==}
1793 case S.SeccompKillThread{}:
1794 {==}
1795 case S.SeccompTrap{dc}:
1796 {==}
1797 case S.SeccompErrno{dc}:
1798 {==}
1799 case S.SeccompUserNotif{}:
1800 {==}
1801 case S.SeccompTrace{dc}:
1802 {==}
1803 case S.SeccompLog{}:
1804 {==}
1805 case S.SeccompAllow{}:
1806 {==}
1807 case S.SeccompTrap{db}:
1808 match c:
1809 case S.SeccompKillProcess{}:
1810 {==}
1811 case S.SeccompKillThread{}:
1812 {==}
1813 case S.SeccompTrap{dc}:
1814 {==}
1815 case S.SeccompErrno{dc}:
1816 {==}
1817 case S.SeccompUserNotif{}:
1818 {==}
1819 case S.SeccompTrace{dc}:
1820 {==}
1821 case S.SeccompLog{}:
1822 {==}
1823 case S.SeccompAllow{}:
1824 {==}
1825 case S.SeccompErrno{db}:
1826 match c:
1827 case S.SeccompKillProcess{}:
1828 {==}
1829 case S.SeccompKillThread{}:
1830 {==}
1831 case S.SeccompTrap{dc}:
1832 {==}
1833 case S.SeccompErrno{dc}:
1834 {==}
1835 case S.SeccompUserNotif{}:
1836 {==}
1837 case S.SeccompTrace{dc}:
1838 {==}
1839 case S.SeccompLog{}:
1840 {==}
1841 case S.SeccompAllow{}:
1842 {==}
1843 case S.SeccompUserNotif{}:
1844 match c:
1845 case S.SeccompKillProcess{}:
1846 {==}
1847 case S.SeccompKillThread{}:
1848 {==}
1849 case S.SeccompTrap{dc}:
1850 {==}
1851 case S.SeccompErrno{dc}:
1852 {==}
1853 case S.SeccompUserNotif{}:
1854 {==}
1855 case S.SeccompTrace{dc}:
1856 {==}
1857 case S.SeccompLog{}:
1858 {==}
1859 case S.SeccompAllow{}:
1860 {==}
1861 case S.SeccompTrace{db}:
1862 match c:
1863 case S.SeccompKillProcess{}:
1864 {==}
1865 case S.SeccompKillThread{}:
1866 {==}
1867 case S.SeccompTrap{dc}:
1868 {==}
1869 case S.SeccompErrno{dc}:
1870 {==}
1871 case S.SeccompUserNotif{}:
1872 {==}
1873 case S.SeccompTrace{dc}:
1874 {==}
1875 case S.SeccompLog{}:
1876 {==}
1877 case S.SeccompAllow{}:
1878 {==}
1879 case S.SeccompLog{}:
1880 match c:
1881 case S.SeccompKillProcess{}:
1882 {==}
1883 case S.SeccompKillThread{}:
1884 {==}
1885 case S.SeccompTrap{dc}:
1886 {==}
1887 case S.SeccompErrno{dc}:
1888 {==}
1889 case S.SeccompUserNotif{}:
1890 {==}
1891 case S.SeccompTrace{dc}:
1892 {==}
1893 case S.SeccompLog{}:
1894 {==}
1895 case S.SeccompAllow{}:
1896 {==}
1897 case S.SeccompAllow{}:
1898 match c:
1899 case S.SeccompKillProcess{}:
1900 {==}
1901 case S.SeccompKillThread{}:
1902 {==}
1903 case S.SeccompTrap{dc}:
1904 {==}
1905 case S.SeccompErrno{dc}:
1906 {==}
1907 case S.SeccompUserNotif{}:
1908 {==}
1909 case S.SeccompTrace{dc}:
1910 {==}
1911 case S.SeccompLog{}:
1912 {==}
1913 case S.SeccompAllow{}:
1914 {==}
1915
1916def Laws.action_round_trip(a):
1917 match a:
1918 case S.SeccompKillProcess{}:
1919 {==}
1920 case S.SeccompKillThread{}:
1921 {==}
1922 case S.SeccompTrap{d}:
1923 match d:
1924 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
1925 {==}
1926 case S.SeccompErrno{d}:
1927 match d:
1928 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
1929 {==}
1930 case S.SeccompUserNotif{}:
1931 {==}
1932 case S.SeccompTrace{d}:
1933 match d:
1934 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
1935 {==}
1936 case S.SeccompLog{}:
1937 {==}
1938 case S.SeccompAllow{}:
1939 {==}
1940def nat.lt_not_le(x: Nat, y: Nat, e: {Nat.is_lt(y, x) == True{} : Bool}) -> {Nat.is_le(x, y) == False{} : Bool}:
1941 match x y:
1942 case 0n _:
1943 Empty.absurd({Nat.is_le(0n, y) == False{} : Bool}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(y, 0n), True{}, Equal.sym(Bool, Nat.is_lt(y, 0n), False{}, nat.lt_zero(y)), e)))
1944 case 1n+xp 0n:
1945 {==}
1946 case 1n+xp 1n+yp:
1947 nat.lt_not_le(xp, yp, e)
1948
1949def Laws.combine_newer(a, b, e):
1950 %Equal.sym(Bool, Nat.is_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b)), True{}, e) : {S.seccomp_combine.pick(_, a, b) == a : S.SeccompAction}
1951 {==}
1952
1953def Laws.combine_older(a, b, e):
1954 %Equal.sym(Bool, Nat.is_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b)), False{}, nat.lt_not_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b), e)) : {S.seccomp_combine.pick(_, a, b) == b : S.SeccompAction}
1955 {==}
1956
1957def fin_done(r: Result<&2, &2, I.BpfError, U32>, e: {Result.is_done(&2, &2, I.BpfError, U32, r) == True{} : Bool}) -> {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run.fin(r)) == True{} : Bool}:
1958 match r:
1959 case Fail{f}:
1960 Empty.absurd({Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run.fin(Fail{f})) == True{} : Bool}, absurd.ft(e))
1961 case Done{v}:
1962 {==}
1963
1964def sc_l(v: Result<&2, &2, I.BpfError, Unit>, -prog: List<&2, I.BpfOp>, h: {S.seccomp_validate.go(v, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {v == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
1965 match v:
1966 case Fail{e}:
1967 Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
1968 case Done{u}:
1969 match u:
1970 case Unit{}:
1971 {==}
1972
1973def Laws.seccomp_validated_acts(opts, order, prog, d, ok):
1974 fin_done(R.bpf_run(S.SeccompData.input(order, d), prog), Laws.validated_returns(opts, prog, S.SeccompData.input(order, d), sc_l(V.bpf_validate_with(opts, prog), prog, ok)))
1975
1976
1977
1978def Laws.rarp_prepares():
1979 {==}
1980
1981def Laws.rarp_accepts():
1982 {==}
1983
1984def Laws.rarp_rejects_arp():
1985 {==}
1986
1987def Laws.hosts_accepts():
1988 {==}
1989
1990def Laws.hosts_rejects():
1991 {==}
1992
1993def Laws.finger_accepts():
1994 {==}
1995
1996def Laws.finger_accepts_options():
1997 {==}
1998
1999def Laws.finger_rejects_port():
2000 {==}
2001
2002def Laws.finger_rejects_fragment():
2003 {==}
2004
2005def Laws.short_packet():
2006 {==}
2007
2008def Laws.divide_by_zero_x():
2009 {==}
2010
2011def Laws.length_load():
2012 {==}
2013
2014def Laws.scratch_and_alu():
2015 {==}
2016
2017def Laws.validate_accepts():
2018 {==}
2019
2020def Laws.validate_empty():
2021 {==}
2022
2023def Laws.validate_too_long():
2024 {==}
2025
2026def Laws.validate_jump_out():
2027 {==}
2028
2029def Laws.validate_no_return():
2030 {==}
2031
2032def Laws.validate_scratch():
2033 {==}
2034
2035def Laws.validate_div_zero():
2036 {==}
2037
2038def Laws.decode_bad_opcode():
2039 {==}
2040
2041def Laws.program_bytes():
2042 {==}
2043
2044def Laws.program_bytes_back():
2045 {==}
2046
2047def Laws.seccomp_example_valid():
2048 {==}
2049
2050def Laws.seccomp_example_errno():
2051 {==}
2052
2053def Laws.seccomp_example_allow():
2054 {==}
2055
2056def Laws.seccomp_example_other_arch():
2057 {==}
2058
2059def Laws.seccomp_example_x32():
2060 {==}
2061
2062def Laws.seccomp_rejects_byte_load():
2063 {==}
2064
2065def Laws.seccomp_rejects_unaligned():
2066 {==}
2067
2068def Laws.stack_newest_on_tie():
2069 {==}
2070
2071def Laws.stack_most_restrictive():
2072 {==}
2073
2074def Laws.stack_empty_allows():
2075 {==}
2076
2077def Laws.unknown_action_kills():
2078 {==}
2079
2080def Laws.install_path_limit():
2081 {==}
2082
2083def Laws.install_pushes():
2084 {==}
2085
2086def Laws.seccomp_rejects_mod():
2087 {==}
2088
2089def Laws.seccomp_example_write():
2090 {==}
2091
2092def Laws.seccomp_example_preadv():
2093 {==}
2094
2095def Laws.validate_mem_init():
2096 {==}
2097
2098def Laws.validate_mem_init_path():
2099 {==}
2100
2101def Laws.validate_mem_init_written():
2102 {==}
2103
2104def Laws.validate_permissive():
2105 {==}
2106
2107def Laws.witness_skip_length():
2108 {==}
2109
2110def Laws.witness_rank_le():
2111 {==}
2112
2113def Laws.witness_rank_lt():
2114 {==}
2115
2116def Laws.validate_mem_after_jump():
2117 {==}
2118
2119def Laws.validate_mem_after_return():
2120 {==}
2121
2122def Laws.octets_max_default():
2123 {==}
2124
2125def Laws.octets_limit_refuses():
2126 {==}
2127
2128def Laws.octets_limit_accepts():
2129 {==}
2130
2131def Laws.witness_octets_over():
2132 {==}