~/jendhub

insn.bend

bend-osdev-bpf@0.1.0.0 · 482 lines · 44 definitions

1# bend-osdev-bpf: classic BPF instructions, raw and decoded.
2#
3# A classic BPF program is a list of struct sock_filter {code: u16, jt: u8,
4# jf: u8, k: u32} (the BSD bpf(4) manual page; McCanne and Jacobson, "The BSD
5# Packet Filter", USENIX 1993). BpfRaw is that struct, field for field. BpfOp
6# is the same instruction decoded into what it does, one constructor per
7# instruction and addressing mode, so code that builds or inspects a program
8# never handles opcode bits.
9#
10# The opcode is class | size | mode for loads, class | op | source for ALU
11# and jumps, class | rval for returns:
12#   class  LD 0, LDX 1, ST 2, STX 3, ALU 4, JMP 5, RET 6, MISC 7
13#   size   W 0x00, H 0x08, B 0x10
14#   mode   IMM 0x00, ABS 0x20, IND 0x40, MEM 0x60, LEN 0x80, MSH 0xa0
15#   ALU    ADD 0x00, SUB 0x10, MUL 0x20, DIV 0x30, OR 0x40, AND 0x50,
16#          LSH 0x60, RSH 0x70, NEG 0x80, MOD 0x90, XOR 0xa0
17#   JMP    JA 0x00, JEQ 0x10, JGT 0x20, JGE 0x30, JSET 0x40
18#   source K 0x00, X 0x08;  rval K 0x00, A 0x10;  MISC TAX 0x00, TXA 0x80
19import Base
20import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21
22# Instructions
23
24type BpfSize is Data:
25  BpfW{}
26  BpfH{}
27  BpfB{}
28
29type BpfAluOp is Data:
30  BpfAdd{}
31  BpfSub{}
32  BpfMul{}
33  BpfDiv{}
34  BpfOr{}
35  BpfAnd{}
36  BpfLsh{}
37  BpfRsh{}
38  BpfMod{}
39  BpfXor{}
40
41type BpfCond is Data:
42  BpfJeq{}
43  BpfJgt{}
44  BpfJge{}
45  BpfJset{}
46
47# the second operand of an ALU or jump instruction: the constant k, or X
48type BpfSrc is Data:
49  BpfK{k: U32}
50  BpfX{}
51
52# what a return instruction answers: the constant k, or A
53type BpfRval is Data:
54  BpfRetK{k: U32}
55  BpfRetA{}
56
57# A decoded instruction. Jump offsets count the instructions skipped: a jump
58# at index i by n goes to index i + 1 + n, so jumps only move forward.
59type BpfOp is Data:
60  BpfLdAbs{size: BpfSize, k: U32}
61  BpfLdInd{size: BpfSize, k: U32}
62  BpfLdImm{k: U32}
63  BpfLdLen{}
64  BpfLdMem{k: U32}
65  BpfLdxImm{k: U32}
66  BpfLdxMem{k: U32}
67  BpfLdxLen{}
68  BpfLdxMsh{k: U32}
69  BpfSt{k: U32}
70  BpfStx{k: U32}
71  BpfAlu{op: BpfAluOp, src: BpfSrc}
72  BpfNeg{}
73  BpfJa{k: U32}
74  BpfJmp{cond: BpfCond, src: BpfSrc, jt: U32, jf: U32}
75  BpfRet{rval: BpfRval}
76  BpfTax{}
77  BpfTxa{}
78
79# struct sock_filter; code is 16 bits and jt, jf are 8 bits when stored
80type BpfRaw is Data:
81  BpfRaw{code: U32, jt: U32, jf: U32, k: U32}
82
83# the byte order of a stored program, and of a filter's loads
84type BpfOrder is Data:
85  BpfBig{}
86  BpfLittle{}
87
88# Every failure: decoding (BadCode, Truncated, StoredTooLong), validation
89# (Empty to SeccompInsn), installing seccomp filters (PathTooLong), and
90# running a program that was not validated (FellOff, BadScratch).
91type BpfError is Data:
92  BpfErrBadCode{pc: Nat, code: U32}
93  BpfErrTruncated{len: Nat}
94  BpfErrStoredTooLong{max: Nat}
95  BpfErrEmpty{}
96  BpfErrTooLong{len: Nat}
97  BpfErrJump{pc: Nat}
98  BpfErrJumpField{pc: Nat}
99  BpfErrNoReturn{pc: Nat}
100  BpfErrScratch{pc: Nat}
101  BpfErrDivZero{pc: Nat}
102  BpfErrMemInit{pc: Nat}
103  BpfErrSeccompLoad{pc: Nat}
104  BpfErrSeccompInsn{pc: Nat}
105  BpfErrPathTooLong{total: Nat}
106  BpfErrFellOff{}
107  BpfErrBadScratch{k: U32}
108
109# BPF_MEMWORDS: the scratch memory is M[0] to M[15]
110def bpf_memwords() -> U32:
111  16
112
113# The C macros BPF_STMT(code, k) and BPF_JUMP(code, k, jt, jf)
114
115def bpf_stmt(code: U32, k: U32) -> BpfRaw:
116  BpfRaw{code, 0, 0, k}
117
118def bpf_jump(code: U32, k: U32, jt: U32, jf: U32) -> BpfRaw:
119  BpfRaw{code, jt, jf, k}
120
121def BpfRaw.code(r: BpfRaw) -> U32:
122  match r:
123    case BpfRaw{code, jt, jf, k}:
124      code
125
126# Encoding
127
128def BpfSize.bits(s: BpfSize) -> U32:
129  match s:
130    case BpfW{}:
131      0
132    case BpfH{}:
133      8
134    case BpfB{}:
135      16
136
137def BpfAluOp.bits(o: BpfAluOp) -> U32:
138  match o:
139    case BpfAdd{}:
140      0
141    case BpfSub{}:
142      16
143    case BpfMul{}:
144      32
145    case BpfDiv{}:
146      48
147    case BpfOr{}:
148      64
149    case BpfAnd{}:
150      80
151    case BpfLsh{}:
152      96
153    case BpfRsh{}:
154      112
155    case BpfMod{}:
156      144
157    case BpfXor{}:
158      160
159
160def BpfCond.bits(c: BpfCond) -> U32:
161  match c:
162    case BpfJeq{}:
163      16
164    case BpfJgt{}:
165      32
166    case BpfJge{}:
167      48
168    case BpfJset{}:
169      64
170
171def BpfSrc.bits(s: BpfSrc) -> U32:
172  match s:
173    case BpfK{k}:
174      0
175    case BpfX{}:
176      8
177
178def BpfSrc.k(s: BpfSrc) -> U32:
179  match s:
180    case BpfK{k}:
181      k
182    case BpfX{}:
183      0
184
185def BpfRval.encode(r: BpfRval) -> BpfRaw:
186  match r:
187    case BpfRetK{k}:
188      BpfRaw{6, 0, 0, k}
189    case BpfRetA{}:
190      BpfRaw{22, 0, 0, 0}
191
192# the sock_filter of an instruction; unused fields are 0
193def BpfOp.encode(op: BpfOp) -> BpfRaw:
194  match op:
195    case BpfLdAbs{size, k}:
196      BpfRaw{U32.or(32, BpfSize.bits(size)), 0, 0, k}
197    case BpfLdInd{size, k}:
198      BpfRaw{U32.or(64, BpfSize.bits(size)), 0, 0, k}
199    case BpfLdImm{k}:
200      BpfRaw{0, 0, 0, k}
201    case BpfLdLen{}:
202      BpfRaw{128, 0, 0, 0}
203    case BpfLdMem{k}:
204      BpfRaw{96, 0, 0, k}
205    case BpfLdxImm{k}:
206      BpfRaw{1, 0, 0, k}
207    case BpfLdxMem{k}:
208      BpfRaw{97, 0, 0, k}
209    case BpfLdxLen{}:
210      BpfRaw{129, 0, 0, 0}
211    case BpfLdxMsh{k}:
212      BpfRaw{177, 0, 0, k}
213    case BpfSt{k}:
214      BpfRaw{2, 0, 0, k}
215    case BpfStx{k}:
216      BpfRaw{3, 0, 0, k}
217    case BpfAlu{o, +src}:
218      BpfRaw{U32.or(4, U32.or(BpfAluOp.bits(o), BpfSrc.bits(src))), 0, 0, BpfSrc.k(src)}
219    case BpfNeg{}:
220      BpfRaw{132, 0, 0, 0}
221    case BpfJa{k}:
222      BpfRaw{5, 0, 0, k}
223    case BpfJmp{c, +src, jt, jf}:
224      BpfRaw{U32.or(5, U32.or(BpfCond.bits(c), BpfSrc.bits(src))), jt, jf, BpfSrc.k(src)}
225    case BpfRet{r}:
226      BpfRval.encode(r)
227    case BpfTax{}:
228      BpfRaw{7, 0, 0, 0}
229    case BpfTxa{}:
230      BpfRaw{135, 0, 0, 0}
231
232# Decoding: every opcode classic BPF defines, and nothing else
233
234def BpfRaw.decode.pick(hit: Bool, op: BpfOp, rest: Maybe<&2, BpfOp>) -> Maybe<&2, BpfOp>:
235  match hit:
236    case True{}:
237      Some{op}
238    case False{}:
239      rest
240
241# the instruction a sock_filter holds, or None for an opcode classic BPF does
242# not define; fields the instruction does not use are ignored
243def BpfRaw.decode(r: BpfRaw) -> Maybe<&2, BpfOp>:
244  match r:
245    case BpfRaw{+code, +jt, +jf, +k}:
246      BpfRaw.decode.pick(U32.is_eq(code, 32), BpfLdAbs{BpfW{}, k},
247      BpfRaw.decode.pick(U32.is_eq(code, 40), BpfLdAbs{BpfH{}, k},
248      BpfRaw.decode.pick(U32.is_eq(code, 48), BpfLdAbs{BpfB{}, k},
249      BpfRaw.decode.pick(U32.is_eq(code, 64), BpfLdInd{BpfW{}, k},
250      BpfRaw.decode.pick(U32.is_eq(code, 72), BpfLdInd{BpfH{}, k},
251      BpfRaw.decode.pick(U32.is_eq(code, 80), BpfLdInd{BpfB{}, k},
252      BpfRaw.decode.pick(U32.is_eq(code, 0), BpfLdImm{k},
253      BpfRaw.decode.pick(U32.is_eq(code, 128), BpfLdLen{},
254      BpfRaw.decode.pick(U32.is_eq(code, 96), BpfLdMem{k},
255      BpfRaw.decode.pick(U32.is_eq(code, 1), BpfLdxImm{k},
256      BpfRaw.decode.pick(U32.is_eq(code, 97), BpfLdxMem{k},
257      BpfRaw.decode.pick(U32.is_eq(code, 129), BpfLdxLen{},
258      BpfRaw.decode.pick(U32.is_eq(code, 177), BpfLdxMsh{k},
259      BpfRaw.decode.pick(U32.is_eq(code, 2), BpfSt{k},
260      BpfRaw.decode.pick(U32.is_eq(code, 3), BpfStx{k},
261      BpfRaw.decode.pick(U32.is_eq(code, 4), BpfAlu{BpfAdd{}, BpfK{k}},
262      BpfRaw.decode.pick(U32.is_eq(code, 12), BpfAlu{BpfAdd{}, BpfX{}},
263      BpfRaw.decode.pick(U32.is_eq(code, 20), BpfAlu{BpfSub{}, BpfK{k}},
264      BpfRaw.decode.pick(U32.is_eq(code, 28), BpfAlu{BpfSub{}, BpfX{}},
265      BpfRaw.decode.pick(U32.is_eq(code, 36), BpfAlu{BpfMul{}, BpfK{k}},
266      BpfRaw.decode.pick(U32.is_eq(code, 44), BpfAlu{BpfMul{}, BpfX{}},
267      BpfRaw.decode.pick(U32.is_eq(code, 52), BpfAlu{BpfDiv{}, BpfK{k}},
268      BpfRaw.decode.pick(U32.is_eq(code, 60), BpfAlu{BpfDiv{}, BpfX{}},
269      BpfRaw.decode.pick(U32.is_eq(code, 68), BpfAlu{BpfOr{}, BpfK{k}},
270      BpfRaw.decode.pick(U32.is_eq(code, 76), BpfAlu{BpfOr{}, BpfX{}},
271      BpfRaw.decode.pick(U32.is_eq(code, 84), BpfAlu{BpfAnd{}, BpfK{k}},
272      BpfRaw.decode.pick(U32.is_eq(code, 92), BpfAlu{BpfAnd{}, BpfX{}},
273      BpfRaw.decode.pick(U32.is_eq(code, 100), BpfAlu{BpfLsh{}, BpfK{k}},
274      BpfRaw.decode.pick(U32.is_eq(code, 108), BpfAlu{BpfLsh{}, BpfX{}},
275      BpfRaw.decode.pick(U32.is_eq(code, 116), BpfAlu{BpfRsh{}, BpfK{k}},
276      BpfRaw.decode.pick(U32.is_eq(code, 124), BpfAlu{BpfRsh{}, BpfX{}},
277      BpfRaw.decode.pick(U32.is_eq(code, 148), BpfAlu{BpfMod{}, BpfK{k}},
278      BpfRaw.decode.pick(U32.is_eq(code, 156), BpfAlu{BpfMod{}, BpfX{}},
279      BpfRaw.decode.pick(U32.is_eq(code, 164), BpfAlu{BpfXor{}, BpfK{k}},
280      BpfRaw.decode.pick(U32.is_eq(code, 172), BpfAlu{BpfXor{}, BpfX{}},
281      BpfRaw.decode.pick(U32.is_eq(code, 132), BpfNeg{},
282      BpfRaw.decode.pick(U32.is_eq(code, 5), BpfJa{k},
283      BpfRaw.decode.pick(U32.is_eq(code, 21), BpfJmp{BpfJeq{}, BpfK{k}, jt, jf},
284      BpfRaw.decode.pick(U32.is_eq(code, 29), BpfJmp{BpfJeq{}, BpfX{}, jt, jf},
285      BpfRaw.decode.pick(U32.is_eq(code, 37), BpfJmp{BpfJgt{}, BpfK{k}, jt, jf},
286      BpfRaw.decode.pick(U32.is_eq(code, 45), BpfJmp{BpfJgt{}, BpfX{}, jt, jf},
287      BpfRaw.decode.pick(U32.is_eq(code, 53), BpfJmp{BpfJge{}, BpfK{k}, jt, jf},
288      BpfRaw.decode.pick(U32.is_eq(code, 61), BpfJmp{BpfJge{}, BpfX{}, jt, jf},
289      BpfRaw.decode.pick(U32.is_eq(code, 69), BpfJmp{BpfJset{}, BpfK{k}, jt, jf},
290      BpfRaw.decode.pick(U32.is_eq(code, 77), BpfJmp{BpfJset{}, BpfX{}, jt, jf},
291      BpfRaw.decode.pick(U32.is_eq(code, 6), BpfRet{BpfRetK{k}},
292      BpfRaw.decode.pick(U32.is_eq(code, 22), BpfRet{BpfRetA{}},
293      BpfRaw.decode.pick(U32.is_eq(code, 7), BpfTax{},
294      BpfRaw.decode.pick(U32.is_eq(code, 135), BpfTxa{},
295      None{})))))))))))))))))))))))))))))))))))))))))))))))))
296# Programs. Each program-wide loop is a tail call over an accumulator,
297# reversed at the end, so a program of any length runs on both lanes. The
298# structural forms (*.ref) are the references the proofs reason about;
299# PROOF.bend proves each equal to its tail form for every input (F_encode,
300# F_decode).
301
302def bpf_encode.ref(ops: List<&2, BpfOp>) -> List<&2, BpfRaw>:
303  match ops:
304    case Nil{}:
305      Nil{}
306    case Con{op, t}:
307      Con{BpfOp.encode(op), bpf_encode.ref(t)}
308
309# the encoded instructions, last first, onto acc
310def bpf_encode.go(ops: List<&2, BpfOp>, acc: List<&2, BpfRaw>) -> List<&2, BpfRaw>:
311  match ops:
312    case Nil{}:
313      acc
314    case Con{op, t}:
315      bpf_encode.go(t, Con{BpfOp.encode(op), acc})
316
317def bpf_encode(ops: List<&2, BpfOp>) -> List<&2, BpfRaw>:
318  List.reverse(&2, BpfRaw, bpf_encode.go(ops, Nil{}))
319
320def bpf_decode.cons(m: Maybe<&2, BpfOp>, e: BpfError, rest: Result<&2, &2, BpfError, List<&2, BpfOp>>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
321  match m:
322    case None{}:
323      Fail{e}
324    case Some{op}:
325      match rest:
326        case Fail{f}:
327          Fail{f}
328        case Done{ops}:
329          Done{Con{op, ops}}
330
331def bpf_decode.ref.go(rs: List<&2, BpfRaw>, +pc: Nat) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
332  match rs:
333    case Nil{}:
334      Done{Nil{}}
335    case Con{+r, t}:
336      bpf_decode.cons(BpfRaw.decode(r), BpfErrBadCode{pc, BpfRaw.code(r)}, bpf_decode.ref.go(t, 1n+pc))
337
338def bpf_decode.ref(rs: List<&2, BpfRaw>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
339  bpf_decode.ref.go(rs, 0n)
340
341# one decoded instruction pushed onto the instructions so far (last first)
342def bpf_decode.push(m: Maybe<&2, BpfOp>, e: BpfError, acc: List<&2, BpfOp>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
343  match m:
344    case None{}:
345      Fail{e}
346    case Some{op}:
347      Done{Con{op, acc}}
348
349# a: the instructions before pc, last first, or the first failure; the loop
350# stops at the instruction after a failure
351def bpf_decode.go(rs: List<&2, BpfRaw>, +pc: Nat, a: Result<&2, &2, BpfError, List<&2, BpfOp>>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
352  match rs:
353    case Nil{}:
354      match a:
355        case Fail{e}:
356          Fail{e}
357        case Done{acc}:
358          Done{List.reverse(&2, BpfOp, acc)}
359    case Con{+r, t}:
360      match a:
361        case Fail{e}:
362          Fail{e}
363        case Done{acc}:
364          bpf_decode.go(t, 1n+pc, bpf_decode.push(BpfRaw.decode(r), BpfErrBadCode{pc, BpfRaw.code(r)}, acc))
365
366# every instruction decoded, or the first one that is not classic BPF
367def bpf_decode(rs: List<&2, BpfRaw>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
368  bpf_decode.go(rs, 0n, Done{Nil{}})
369
370# Stored programs: 8 bytes per instruction, in the given byte order
371
372def BpfRaw.to_octets(order: BpfOrder, r: BpfRaw) -> B.Octets:
373  match order:
374    case BpfLittle{}:
375      match r:
376        case BpfRaw{code, jt, jf, k}:
377          B.Octets.concat([B.Octets.le16(code), B.Octets.of_list([jt, jf]), B.Octets.le32(k)])
378    case BpfBig{}:
379      match r:
380        case BpfRaw{code, jt, jf, k}:
381          B.Octets.concat([B.Octets.be16(code), B.Octets.of_list([jt, jf]), B.Octets.be32(k)])
382
383# each instruction's 8 bytes, last first, onto acc
384def bpf_to_octets.go(rs: List<&2, BpfRaw>, +order: BpfOrder, acc: List<&2, B.Octets>) -> List<&2, B.Octets>:
385  match rs:
386    case Nil{}:
387      acc
388    case Con{r, t}:
389      bpf_to_octets.go(t, order, Con{BpfRaw.to_octets(order, r), acc})
390
391def bpf_to_octets(+order: BpfOrder, rs: List<&2, BpfRaw>) -> B.Octets:
392  B.Octets.concat(List.reverse(&2, B.Octets, bpf_to_octets.go(rs, order, Nil{})))
393
394def bpf_field(m: Maybe<&2, U32>) -> U32:
395  Maybe.default(&2, U32, m, 0)
396
397def BpfRaw.of_octets(order: BpfOrder, +o: B.Octets) -> BpfRaw:
398  match order:
399    case BpfLittle{}:
400      BpfRaw{bpf_field(B.Octets.le16_at(o, 0n)), bpf_field(B.Octets.at(o, 2n)), bpf_field(B.Octets.at(o, 3n)), bpf_field(B.Octets.le32_at(o, 4n))}
401    case BpfBig{}:
402      BpfRaw{bpf_field(B.Octets.be16_at(o, 0n)), bpf_field(B.Octets.at(o, 2n)), bpf_field(B.Octets.at(o, 3n)), bpf_field(B.Octets.be32_at(o, 4n))}
403
404# the next n instructions, onto acc (last first), then all of them in order
405def bpf_of_octets.go(n: Nat, +order: BpfOrder, +o: B.Octets, acc: List<&2, BpfRaw>) -> List<&2, BpfRaw>:
406  match n:
407    case 0n:
408      List.reverse(&2, BpfRaw, acc)
409    case 1n+p:
410      bpf_of_octets.go(p, order, B.Octets.drop(8n, o), Con{BpfRaw.of_octets(order, B.Octets.take(8n, o)), acc})
411
412def bpf_of_octets.rem(r: Nat, q: Nat, +order: BpfOrder, +o: B.Octets, +len: Nat) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>:
413  match r:
414    case 0n:
415      Done{bpf_of_octets.go(q, order, o, Nil{})}
416    case 1n+p:
417      Fail{BpfErrTruncated{len}}
418
419def bpf_of_octets.fin(+order: BpfOrder, +o: B.Octets, +len: Nat, qr: Nat & Nat) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>:
420  (q, r) = qr
421  bpf_of_octets.rem(r, q, order, o, len)
422
423# over: the input's byte at offset max, if it has one
424def bpf_of_octets.fits(over: Maybe<&2, U32>, max: Nat, +order: BpfOrder, +o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>:
425  match over:
426    case Some{b}:
427      Fail{BpfErrStoredTooLong{max}}
428    case None{}:
429      +len = B.Octets.len(o)
430      bpf_of_octets.fin(order, o, len, Nat.divmod(len, 8n))
431
432# 8 * BPF_MAXINSNS: the bytes of the longest program validation accepts by
433# default (LAWS.bend: octets_max_default ties it to bpf_maxinsns)
434def bpf_octets_max() -> Nat:
435  32768n
436
437# a stored program's instructions: at most max bytes, a multiple of 8. The
438# limit is checked first, by looking for the byte at offset max, so a longer
439# input costs max steps whatever its length
440def bpf_of_octets_with(+max: Nat, +order: BpfOrder, +o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>:
441  bpf_of_octets.fits(B.Octets.at(o, max), max, order, o)
442
443# the same, with the default limit, bpf_octets_max()
444def bpf_of_octets(+order: BpfOrder, o: B.Octets) -> Result<&2, &2, BpfError, List<&2, BpfRaw>>:
445  bpf_of_octets_with(bpf_octets_max(), order, o)
446
447# Text
448
449def BpfError.show(e: BpfError) -> String:
450  match e:
451    case BpfErrBadCode{pc, code}:
452      "bad opcode " ++ U32.show(code) ++ " at " ++ Nat.show(pc)
453    case BpfErrTruncated{len}:
454      "truncated program of " ++ Nat.show(len) ++ " bytes"
455    case BpfErrStoredTooLong{max}:
456      "stored program over " ++ Nat.show(max) ++ " bytes"
457    case BpfErrEmpty{}:
458      "empty program"
459    case BpfErrTooLong{len}:
460      "program too long: " ++ Nat.show(len)
461    case BpfErrJump{pc}:
462      "jump out of range at " ++ Nat.show(pc)
463    case BpfErrJumpField{pc}:
464      "jump offset over 255 at " ++ Nat.show(pc)
465    case BpfErrNoReturn{pc}:
466      "no return after " ++ Nat.show(pc)
467    case BpfErrScratch{pc}:
468      "scratch index out of range at " ++ Nat.show(pc)
469    case BpfErrDivZero{pc}:
470      "division by constant zero at " ++ Nat.show(pc)
471    case BpfErrMemInit{pc}:
472      "scratch read before write at " ++ Nat.show(pc)
473    case BpfErrSeccompLoad{pc}:
474      "load not allowed in seccomp at " ++ Nat.show(pc)
475    case BpfErrSeccompInsn{pc}:
476      "instruction not allowed in seccomp at " ++ Nat.show(pc)
477    case BpfErrPathTooLong{total}:
478      "seccomp filters too long: " ++ Nat.show(total)
479    case BpfErrFellOff{}:
480      "ran past the end"
481    case BpfErrBadScratch{k}:
482      "scratch index " ++ U32.show(k)