1	import Base
2	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
3	import bend-osdev-word64@0.1.0.0/word64.bend as W
4	import ./insn.bend as I
5	import ./validate.bend as V
6	import ./bpf.bend as R
7	import ./seccomp.bend as S
8	import ./LAWS.bend as Laws
9	
10	# Contradictions
11	
12	def absurd.bool(b: Bool) -> Type:
13	  match b:
14	    case True{}:
15	      Unit
16	    case False{}:
17	      Empty
18	
19	def absurd.ft(e: {False{} == True{} : Bool}) -> Empty:
20	  %Equal.sym(Bool, False{}, True{}, e) : absurd.bool(_)
21	  Unit{}
22	
23	def 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	
30	def absurd.fd(-e: I.BpfError, h: {Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> Empty:
31	  %h : absurd.res(_)
32	  Unit{}
33	
34	def 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	# What validation's success says
42	
43	def 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	
50	def 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	
59	def 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	
66	def 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	# The interpreter's steps: a step is fine if it answers, or goes on to an
70	# instruction that exists
71	
72	def 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	
81	def 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	
88	def 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	
95	def 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	
98	def 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	# the two range checks inside bpf_check.jmp
106	def 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	
109	def 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	# every instruction that passed its checks steps to an instruction that exists
114	def 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	# A run from a fine step, over instructions that passed their checks,
164	# answers Done: induction on the instructions
165	def 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	# The validator runs tail calls: bpf_count for the length and bpf_check.go
189	# for the instructions' checks. They equal the structural forms the proofs
190	# above use, for every program (F_count, F_check).
191	
192	def 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	
199	def 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	
206	def 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	
214	def 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	# the tail form, from any verdict so far, with n the length
220	def 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	
237	def 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	# each pass of bpf_validate_with runs only once the one before it holds
242	def 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	
251	def 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	
258	def 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	# what bpf_validate's success gives a run: the checks of every instruction,
268	# and at least one instruction
269	def 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	
275	def 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	
282	def 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	# Appending instructions after a validated program changes nothing: the run
286	# never reaches them
287	
288	def 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	
295	def 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	
318	def 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	
321	def Laws.ret_k(k, inp):
322	  {==}
323	
324	# Jumps move forward over exactly the instructions they skip: induction on
325	# the skipped instructions
326	
327	def 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	
334	def 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	
338	def 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	
342	def 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	# Decoding what encoding wrote gives the instructions back
347	
348	def 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	
487	def 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	# bpf_encode and bpf_decode are tail calls over an accumulator, reversed at
497	# the end; they equal the structural forms above for every input (F_encode,
498	# F_decode)
499	
500	def 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	
507	def 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	# reversing twice gives the list back
515	def 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	
518	def 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	
525	def 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	# what the tail form ends with, given the instructions decoded so far (acc,
532	# last first) and what the structural form answers for the rest
533	def 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	
540	def 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	
547	def 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	
558	def 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	
574	def 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	
581	def 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	
586	def 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	# Seccomp actions, by cases
593	
594	def 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	
598	def 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	
745	def 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	
1916	def 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	      {==}
1940	def 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	
1949	def 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	
1953	def 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	
1957	def 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	
1964	def 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	
1973	def 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	# Vectors, by computation
1977	
1978	def Laws.rarp_prepares():
1979	  {==}
1980	
1981	def Laws.rarp_accepts():
1982	  {==}
1983	
1984	def Laws.rarp_rejects_arp():
1985	  {==}
1986	
1987	def Laws.hosts_accepts():
1988	  {==}
1989	
1990	def Laws.hosts_rejects():
1991	  {==}
1992	
1993	def Laws.finger_accepts():
1994	  {==}
1995	
1996	def Laws.finger_accepts_options():
1997	  {==}
1998	
1999	def Laws.finger_rejects_port():
2000	  {==}
Lines 1-2000 of 2132. More: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&start_line=2001