1	# Properties, for every input:
2	#   * a validated program always answers, whatever the validator's options:
3	#     bpf_run gives Done, whatever the input (it never runs past its end or
4	#     misuses scratch memory), and
5	#     instructions after it are never reached; the same for seccomp filters;
6	#   * RET k answers k;
7	#   * jumps move forward over exactly the instructions they skip;
8	#   * decoding an encoded instruction or program gives it back;
9	#   * a stored program longer than the limit is refused, whatever its bytes;
10	#   * stacked seccomp filters answer the most restrictive action, the newer
11	#     filter's on a tie, and the grouping does not matter.
12	#
13	# Vectors: the bpf(4) and seccomp(2) examples, one case of each rule, and a
14	# witness for each hypothesis.
15	import Base
16	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17	import bend-osdev-word64@0.1.0.0/word64.bend as W
18	import ./insn.bend as I
19	import ./validate.bend as V
20	import ./bpf.bend as R
21	import ./seccomp.bend as S
22	
23	law validated_returns:
24	  for +opts: V.BpfValidateOptions
25	  for +prog: List<&2, I.BpfOp>
26	  for +inp: R.BpfInput
27	  for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
28	  {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run(inp, prog)) == True{} : Bool}
29	
30	law validated_ignores_tail:
31	  for +opts: V.BpfValidateOptions
32	  for +prog: List<&2, I.BpfOp>
33	  for +rest: List<&2, I.BpfOp>
34	  for +inp: R.BpfInput
35	  for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
36	  {R.bpf_run(inp, List.append(&2, I.BpfOp, prog, rest)) == R.bpf_run(inp, prog) : Result<&2, &2, I.BpfError, U32>}
37	
38	law ret_k:
39	  for k: U32
40	  for +inp: R.BpfInput
41	  {R.bpf_run(inp, [I.BpfRet{I.BpfRetK{k}}]) == Done{k} : Result<&2, &2, I.BpfError, U32>}
42	
43	law ja_skips:
44	  for k: U32
45	  for +skipped: List<&2, I.BpfOp>
46	  for +rest: List<&2, I.BpfOp>
47	  for +inp: R.BpfInput
48	  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(k) : Nat}
49	  {R.bpf_run(inp, Con{I.BpfJa{k}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
50	
51	law jeq_taken_skips:
52	  for jt: U32
53	  for jf: U32
54	  for +skipped: List<&2, I.BpfOp>
55	  for +rest: List<&2, I.BpfOp>
56	  for +inp: R.BpfInput
57	  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jt) : Nat}
58	  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{0}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
59	
60	law jeq_not_taken_skips:
61	  for jt: U32
62	  for jf: U32
63	  for +skipped: List<&2, I.BpfOp>
64	  for +rest: List<&2, I.BpfOp>
65	  for +inp: R.BpfInput
66	  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jf) : Nat}
67	  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
68	
69	law insn_round_trip:
70	  for op: I.BpfOp
71	  {I.BpfRaw.decode(I.BpfOp.encode(op)) == Some{op} : Maybe<&2, I.BpfOp>}
72	
73	law program_round_trip:
74	  for +prog: List<&2, I.BpfOp>
75	  {I.bpf_decode(I.bpf_encode(prog)) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
76	
77	# a stored program with a byte at offset max (so more than max bytes) is
78	# refused, whatever its bytes
79	law octets_over_limit:
80	  for +max: Nat
81	  for +order: I.BpfOrder
82	  for +o: B.Octets
83	  for b: U32
84	  for e: {B.Octets.at(o, max) == Some{b} : Maybe<&2, U32>}
85	  {I.bpf_of_octets_with(max, order, o) == Fail{I.BpfErrStoredTooLong{max}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
86	
87	law most_restrictive:
88	  for a: S.SeccompAction
89	  for b: S.SeccompAction
90	  {S.SeccompAction.rank(S.seccomp_combine(a, b)) == Nat.min(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) : Nat}
91	
92	law combine_newer:
93	  for +a: S.SeccompAction
94	  for +b: S.SeccompAction
95	  for e: {Nat.is_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) == True{} : Bool}
96	  {S.seccomp_combine(a, b) == a : S.SeccompAction}
97	
98	law combine_older:
99	  for +a: S.SeccompAction
100	  for +b: S.SeccompAction
101	  for e: {Nat.is_lt(S.SeccompAction.rank(b), S.SeccompAction.rank(a)) == True{} : Bool}
102	  {S.seccomp_combine(a, b) == b : S.SeccompAction}
103	
104	law combine_assoc:
105	  for a: S.SeccompAction
106	  for b: S.SeccompAction
107	  for c: S.SeccompAction
108	  {S.seccomp_combine(a, S.seccomp_combine(b, c)) == S.seccomp_combine(S.seccomp_combine(a, b), c) : S.SeccompAction}
109	
110	law action_round_trip:
111	  for a: S.SeccompAction
112	  {S.SeccompAction.of_u32(S.SeccompAction.to_u32(a)) == S.SeccompAction.clip(a) : S.SeccompAction}
113	
114	law seccomp_validated_acts:
115	  for +opts: V.BpfValidateOptions
116	  for +order: I.BpfOrder
117	  for +prog: List<&2, I.BpfOp>
118	  for +d: S.SeccompData
119	  for +ok: {S.seccomp_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
120	  {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run(order, prog, d)) == True{} : Bool}
121	
122	# Vectors: the documentation's examples, and one case of each rule
123	
124	# bpf(4), EXAMPLES: accept only Reverse ARP requests, as the manual writes it
125	# with BPF_STMT and BPF_JUMP (0x8035, ETHERTYPE_REVARP; 3, REVARP_REQUEST)
126	def rarp() -> List<&2, I.BpfRaw>:
127	  [I.bpf_stmt(40, 12), I.bpf_jump(21, 32821, 0, 3), I.bpf_stmt(40, 20), I.bpf_jump(21, 3, 0, 1), I.bpf_stmt(6, 42), I.bpf_stmt(6, 0)]
128	
129	def rarp_ops() -> List<&2, I.BpfOp>:
130	  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{32821}, 0, 3}, I.BpfLdAbs{I.BpfH{}, 20}, I.BpfJmp{I.BpfJeq{}, I.BpfK{3}, 0, 1}, I.BpfRet{I.BpfRetK{42}}, I.BpfRet{I.BpfRetK{0}}]
131	
132	# bpf(4): accept IP packets between 128.3.112.15 and 128.3.112.35
133	def hosts() -> List<&2, I.BpfOp>:
134	  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2048}, 0, 8}, I.BpfLdAbs{I.BpfW{}, 26}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708943}, 0, 2}, I.BpfLdAbs{I.BpfW{}, 30}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708963}, 3, 4}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708963}, 0, 3}, I.BpfLdAbs{I.BpfW{}, 30}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708943}, 0, 1}, I.BpfRet{I.BpfRetK{4294967295}}, I.BpfRet{I.BpfRetK{0}}]
135	
136	# bpf(4): accept TCP finger packets (port 79), skipping IP fragments, with
137	# the IP header length from BPF_LDX | BPF_MSH
138	def finger() -> List<&2, I.BpfOp>:
139	  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2048}, 0, 10}, I.BpfLdAbs{I.BpfB{}, 23}, I.BpfJmp{I.BpfJeq{}, I.BpfK{6}, 0, 8}, I.BpfLdAbs{I.BpfH{}, 20}, I.BpfJmp{I.BpfJset{}, I.BpfK{8191}, 6, 0}, I.BpfLdxMsh{14}, I.BpfLdInd{I.BpfH{}, 14}, I.BpfJmp{I.BpfJeq{}, I.BpfK{79}, 2, 0}, I.BpfLdInd{I.BpfH{}, 16}, I.BpfJmp{I.BpfJeq{}, I.BpfK{79}, 0, 1}, I.BpfRet{I.BpfRetK{4294967295}}, I.BpfRet{I.BpfRetK{0}}]
140	
141	# Ethernet frames: a RARP request, an ARP request, and IPv4 TCP packets
142	def pkt_rarp() -> B.Octets:
143	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 128, 53, 0, 1, 8, 0, 6, 4, 0, 3, 2, 0, 0, 0, 0, 1, 10, 0, 0, 1, 0, 0, 0, 0, 0, 0, 10, 0, 0, 2])
144	
145	def pkt_arp() -> B.Octets:
146	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 6, 0, 1, 8, 0, 6, 4, 0, 1, 2, 0, 0, 0, 0, 1, 10, 0, 0, 1, 0, 0, 0, 0, 0, 0, 10, 0, 0, 2])
147	
148	# from 128.3.112.15 to 128.3.112.35, and from 128.3.112.15 to 10.0.0.1
149	def pkt_ab() -> B.Octets:
150	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 128, 3, 112, 15, 128, 3, 112, 35, 3, 232, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
151	
152	def pkt_ac() -> B.Octets:
153	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 128, 3, 112, 15, 10, 0, 0, 1, 3, 232, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
154	
155	# to TCP port 79; to port 80; a fragment to port 79; and to port 79 after a
156	# 24-byte IP header
157	def pkt_finger() -> B.Octets:
158	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 79, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
159	
160	def pkt_web() -> B.Octets:
161	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
162	
163	def pkt_frag() -> B.Octets:
164	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 32, 1, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 79, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
165	
166	def pkt_finger_opts() -> B.Octets:
167	  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 70, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 1, 2, 3, 4, 0, 79, 3, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
168	
169	law rarp_prepares:
170	  {V.bpf_prepare(V.bpf_maxinsns(), rarp()) == Done{rarp_ops()} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
171	
172	law rarp_accepts:
173	  {R.bpf_run(R.bpf_packet(pkt_rarp()), rarp_ops()) == Done{42} : Result<&2, &2, I.BpfError, U32>}
174	
175	law rarp_rejects_arp:
176	  {R.bpf_run(R.bpf_packet(pkt_arp()), rarp_ops()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
177	
178	law hosts_accepts:
179	  {R.bpf_run(R.bpf_packet(pkt_ab()), hosts()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
180	
181	law hosts_rejects:
182	  {R.bpf_run(R.bpf_packet(pkt_ac()), hosts()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
183	
184	law finger_accepts:
185	  {R.bpf_run(R.bpf_packet(pkt_finger()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
186	
187	law finger_accepts_options:
188	  {R.bpf_run(R.bpf_packet(pkt_finger_opts()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
189	
190	law finger_rejects_port:
191	  {R.bpf_run(R.bpf_packet(pkt_web()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
192	
193	law finger_rejects_fragment:
194	  {R.bpf_run(R.bpf_packet(pkt_frag()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
195	
196	# a load past the end of the input answers 0
197	law short_packet:
198	  {R.bpf_run(R.bpf_packet(B.Octets.of_list([8, 0, 69])), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
199	
200	# so does a division by X = 0
201	law divide_by_zero_x:
202	  {R.bpf_run(R.bpf_packet(pkt_arp()), [I.BpfLdImm{7}, I.BpfAlu{I.BpfDiv{}, I.BpfX{}}, I.BpfRet{I.BpfRetK{1}}]) == Done{0} : Result<&2, &2, I.BpfError, U32>}
203	
204	law length_load:
205	  {R.bpf_run(R.bpf_packet(pkt_rarp()), [I.BpfLdLen{}, I.BpfRet{I.BpfRetA{}}]) == Done{42} : Result<&2, &2, I.BpfError, U32>}
206	
207	# M[15] = 5; X = 3; A = M[15] * X = 15; M[0] = X; X = M[15]; A = -(A - X)
208	law scratch_and_alu:
209	  {R.bpf_run(R.bpf_packet(pkt_rarp()), [I.BpfLdImm{5}, I.BpfSt{15}, I.BpfLdxImm{3}, I.BpfLdMem{15}, I.BpfAlu{I.BpfMul{}, I.BpfX{}}, I.BpfStx{0}, I.BpfLdxMem{15}, I.BpfAlu{I.BpfSub{}, I.BpfX{}}, I.BpfNeg{}, I.BpfRet{I.BpfRetA{}}]) == Done{4294967286} : Result<&2, &2, I.BpfError, U32>}
210	
211	law validate_accepts:
212	  {V.bpf_validate(V.bpf_maxinsns(), finger()) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
213	
214	law validate_empty:
215	  {V.bpf_validate(V.bpf_maxinsns(), []) == Fail{I.BpfErrEmpty{}} : Result<&2, &2, I.BpfError, Unit>}
216	
217	law validate_too_long:
218	  {V.bpf_validate(12n, finger()) == Fail{I.BpfErrTooLong{13n}} : Result<&2, &2, I.BpfError, Unit>}
219	
220	law validate_jump_out:
221	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfJa{1}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrJump{0n}} : Result<&2, &2, I.BpfError, Unit>}
222	
223	law validate_no_return:
224	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfRet{I.BpfRetA{}}, I.BpfLdImm{1}]) == Fail{I.BpfErrNoReturn{1n}} : Result<&2, &2, I.BpfError, Unit>}
225	
226	law validate_scratch:
227	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfSt{16}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrScratch{0n}} : Result<&2, &2, I.BpfError, Unit>}
228	
229	law validate_div_zero:
230	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfAlu{I.BpfMod{}, I.BpfK{0}}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrDivZero{0n}} : Result<&2, &2, I.BpfError, Unit>}
231	
232	law decode_bad_opcode:
233	  {I.bpf_decode([I.bpf_stmt(6, 0), I.bpf_stmt(14, 0)]) == Fail{I.BpfErrBadCode{1n, 14}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
234	
235	law program_bytes:
236	  {B.Octets.hex(I.bpf_to_octets(I.BpfLittle{}, rarp())) == "280000000c000000150000033580000028000000140000001500000103000000060000002a0000000600000000000000" : String}
237	
238	law program_bytes_back:
239	  {I.bpf_of_octets(I.BpfBig{}, I.bpf_to_octets(I.BpfBig{}, rarp())) == Done{rarp()} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
240	
241	# the default limit on stored programs: 8 bytes for each of BPF_MAXINSNS
242	# instructions (compared as U32, which holds both)
243	law octets_max_default:
244	  {U32.from_nat(I.bpf_octets_max()) == U32.mul(8, U32.from_nat(V.bpf_maxinsns())) : U32}
245	
246	law octets_limit_refuses:
247	  {I.bpf_of_octets_with(16n, I.BpfBig{}, B.Octets.zeros(17n)) == Fail{I.BpfErrStoredTooLong{16n}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
248	
249	law octets_limit_accepts:
250	  {I.bpf_of_octets_with(16n, I.BpfLittle{}, I.bpf_to_octets(I.BpfLittle{}, [I.bpf_stmt(6, 1), I.bpf_stmt(22, 0)])) == Done{[I.bpf_stmt(6, 1), I.bpf_stmt(22, 0)]} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
251	
252	# seccomp(2), EXAMPLES, install_filter(syscall_nr, t_arch, f_errno) with
253	# t_arch = AUDIT_ARCH_X86_64, so upper_nr_limit = X32_SYSCALL_BIT - 1: the
254	# call syscall_nr fails with f_errno, other calls are allowed, and another
255	# architecture or an x32 call (nr above the limit) kills the process
256	def seccomp_example(nr: U32, e: U32) -> List<&2, I.BpfOp>:
257	  [I.BpfLdAbs{I.BpfW{}, 4}, I.BpfJmp{I.BpfJeq{}, I.BpfK{S.seccomp_arch_x86_64()}, 0, 5}, I.BpfLdAbs{I.BpfW{}, 0}, I.BpfJmp{I.BpfJgt{}, I.BpfK{U32.sub(S.seccomp_x32_syscall_bit(), 1)}, 3, 0}, I.BpfJmp{I.BpfJeq{}, I.BpfK{nr}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{e})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompKillProcess{})}}]
258	
259	def sc_call(nr: U32, arch: U32) -> S.SeccompData:
260	  S.SeccompData{nr, arch, W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero()}
261	
262	# ERRNO(e) for system call nr, ALLOW for the others
263	def deny(nr: U32, e: U32) -> List<&2, I.BpfOp>:
264	  [I.BpfLdAbs{I.BpfW{}, 0}, I.BpfJmp{I.BpfJeq{}, I.BpfK{nr}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{e})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}]
265	
266	law seccomp_example_valid:
267	  {S.seccomp_validate(V.bpf_maxinsns(), seccomp_example(59, 99)) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
268	
269	law seccomp_example_errno:
270	  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(59, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{99}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
271	
272	law seccomp_example_allow:
273	  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
274	
275	law seccomp_example_other_arch:
276	  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(59, S.seccomp_arch_i386())) == Done{S.SeccompKillProcess{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
277	
278	law seccomp_example_x32:
279	  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(1073741883, S.seccomp_arch_x86_64())) == Done{S.SeccompKillProcess{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
280	
281	law seccomp_rejects_byte_load:
282	  {S.seccomp_validate(V.bpf_maxinsns(), finger()) == Fail{I.BpfErrSeccompLoad{0n}} : Result<&2, &2, I.BpfError, Unit>}
283	
284	law seccomp_rejects_unaligned:
285	  {S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdAbs{I.BpfW{}, 6}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrSeccompLoad{0n}} : Result<&2, &2, I.BpfError, Unit>}
286	
287	# two filters with the same action: the newer one wins, with its data
288	law stack_newest_on_tie:
289	  {S.seccomp_eval([deny(39, 1), deny(39, 2)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{1}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
290	
291	law stack_most_restrictive:
292	  {S.seccomp_eval([deny(39, 1), [I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompTrap{5})}}], deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompTrap{5}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
293	
294	law stack_empty_allows:
295	  {S.seccomp_eval([], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
296	
297	law unknown_action_kills:
298	  {S.SeccompAction.of_u32(65536) == S.SeccompKillProcess{} : S.SeccompAction}
299	
300	law install_path_limit:
301	  {S.seccomp_install(S.SeccompLimits{4096n, 19n}, [deny(39, 1), deny(39, 2)], I.bpf_encode(deny(110, 3))) == Fail{I.BpfErrPathTooLong{20n}} : Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>}
302	
303	law install_pushes:
304	  {S.seccomp_install(S.seccomp_limits(), [deny(39, 1)], I.bpf_encode(deny(110, 3))) == Done{[deny(110, 3), deny(39, 1)]} : Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>}
305	
306	law seccomp_rejects_mod:
307	  {S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdImm{7}, I.BpfAlu{I.BpfMod{}, I.BpfK{3}}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrSeccompInsn{1n}} : Result<&2, &2, I.BpfError, Unit>}
308	
309	# the page's runs: ./a.out 1 0xC000003E 99 makes write (1) fail, and
310	# ./a.out 295 0xC000003E 99 leaves the calls whoami makes alone
311	law seccomp_example_write:
312	  {S.seccomp_run(S.seccomp_order(), seccomp_example(1, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{99}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
313	
314	law seccomp_example_preadv:
315	  {S.seccomp_run(S.seccomp_order(), seccomp_example(295, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
316	
317	# scratch memory read before it is written: refused by default, on every
318	# path (here the jump past the store), and allowed by the permissive options
319	law validate_mem_init:
320	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{0n}} : Result<&2, &2, I.BpfError, Unit>}
321	
322	law validate_mem_init_path:
323	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}, I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, 1, 0}, I.BpfSt{2}, I.BpfLdMem{2}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{3n}} : Result<&2, &2, I.BpfError, Unit>}
324	
325	law validate_mem_init_written:
326	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}, I.BpfSt{2}, I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, 1, 0}, I.BpfSt{3}, I.BpfLdMem{2}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
327	
328	# code after a jump is reached only by jumps to it; code after a return
329	# counts as reached from the return, as Linux counts it
330	law validate_mem_after_jump:
331	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{0}, I.BpfSt{0}, I.BpfJa{1}, I.BpfLdMem{1}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
332	
333	law validate_mem_after_return:
334	  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{0}, I.BpfRet{I.BpfRetA{}}, I.BpfLdMem{1}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{2n}} : Result<&2, &2, I.BpfError, Unit>}
335	
336	law validate_permissive:
337	  {V.bpf_validate_with(V.BpfValidateOptions.permissive(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
338	
339	# Witnesses: each hypothesis of a law above holds for some input (the
340	# validation hypotheses: validate_accepts, validate_permissive and
341	# seccomp_example_valid; octets_over_limit: witness_octets_over)
342	
343	law witness_skip_length:
344	  {List.length(&2, I.BpfOp, [I.BpfTax{}, I.BpfTxa{}, I.BpfNeg{}]) == U32.to_nat(3) : Nat}
345	
346	law witness_octets_over:
347	  {B.Octets.at(B.Octets.zeros(9n), 8n) == Some{0} : Maybe<&2, U32>}
348	
349	law witness_rank_le:
350	  {Nat.is_le(S.SeccompAction.rank(S.SeccompErrno{1}), S.SeccompAction.rank(S.SeccompErrno{2})) == True{} : Bool}
351	
352	law witness_rank_lt:
353	  {Nat.is_lt(S.SeccompAction.rank(S.SeccompKillProcess{}), S.SeccompAction.rank(S.SeccompAllow{})) == True{} : Bool}