1	import Base
2	import ./caps.bend as C
3	import ./exec.bend as E
4	import ./adjust.bend as A
5	import ./LAWS.bend as Laws
6	
7	# Every set operation works bit by bit, so each fact about sets is proved by
8	# induction on the width n of a word (the bits.* lemmas): at each bit, every
9	# combination of the bits involved either satisfies the fact (and the rest is
10	# the induction hypothesis) or contradicts a hypothesis. A set is a native
11	# U32 (capabilities 0 to 31) and a Word(9n) (32 to 40): each set.* lemma
12	# opens its sets into the U32's Word(32n) and the Word(9n), and applies the
13	# bits.* lemma at widths 32 and 9 (set.bridge shows that the native subset
14	# test on the low word, a & ~b == 0, is the bitwise one). The laws then
15	# follow by unfolding the operations and choosing which set lemma each case
16	# needs. Hypotheses are taken as arguments after the match ("convoy" style),
17	# so that matching on a value refines them too.
18	
19	# Contradictions
20	
21	def bits.disc(b: Bool) -> Type:
22	  match b:
23	    case False{}:
24	      Unit
25	    case True{}:
26	      Empty
27	
28	def bits.disc2(b: Bool) -> Type:
29	  match b:
30	    case False{}:
31	      Empty
32	    case True{}:
33	      Unit
34	
35	def bits.ft(+e: {False{} == True{} : Bool}) -> bits.disc(True{}):
36	  %e : bits.disc(_)
37	  Unit{}
38	
39	def bits.tf(+e: {True{} == False{} : Bool}) -> bits.disc2(False{}):
40	  %e : bits.disc2(_)
41	  Unit{}
42	
43	def bits.absurd(-x: Bool, +e: {False{} == True{} : Bool}) -> {x == True{} : Bool}:
44	  Empty.absurd({x == True{} : Bool}, bits.ft(e))
45	
46	def bits.absurd_eq(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}:
47	  Empty.absurd({x == y : T}, bits.ft(e))
48	
49	def bits.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}:
50	  Empty.absurd({x == y : T}, bits.tf(e))
51	
52	# Conjunctions
53	
54	def bool.and_l(+x: Bool, +y: Bool) -> {Bool.and(x, y) == True{} : Bool} -> {x == True{} : Bool}:
55	  match x:
56	    case True{}:
57	      h => {==}
58	    case False{}:
59	      h => bits.absurd(False{}, h)
60	
61	def bool.and_r(+x: Bool, +y: Bool) -> {Bool.and(x, y) == True{} : Bool} -> {y == True{} : Bool}:
62	  match x:
63	    case True{}:
64	      h => h
65	    case False{}:
66	      h => bits.absurd(y, h)
67	
68	def bool.and3(+x: Bool, +y: Bool, +z: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {z == True{} : Bool} -> {Bool.and(x, Bool.and(y, z)) == True{} : Bool}:
69	  match x y z:
70	    case True{} True{} True{}:
71	      hx => hy => hz => {==}
72	    case False{} y z:
73	      hx => hy => hz => bits.absurd(Bool.and(False{}, Bool.and(y, z)), hx)
74	    case True{} False{} z:
75	      hx => hy => hz => bits.absurd(Bool.and(True{}, Bool.and(False{}, z)), hy)
76	    case True{} True{} False{}:
77	      hx => hy => hz => bits.absurd(False{}, hz)
78	
79	# A state is valid exactly when its three subset tests pass
80	
81	def valid.intro(+s: C.CapState) -> {C.CapSet.subset(C.CapState.effective(s), C.CapState.permitted(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.permitted(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapState.valid(s) == True{} : Bool}:
82	  match s:
83	    case C.CapState{+p, +i, +e, +b, +a}:
84	      h1 => h2 => h3 => bool.and3(C.CapSet.subset(e, p), C.CapSet.subset(a, p), C.CapSet.subset(a, i))(h1)(h2)(h3)
85	
86	def valid.ep(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.effective(s), C.CapState.permitted(s)) == True{} : Bool}:
87	  match s:
88	    case C.CapState{+p, +i, +e, +b, +a}:
89	      h => bool.and_l(C.CapSet.subset(e, p), Bool.and(C.CapSet.subset(a, p), C.CapSet.subset(a, i)))(h)
90	
91	def valid.ap(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.permitted(s)) == True{} : Bool}:
92	  match s:
93	    case C.CapState{+p, +i, +e, +b, +a}:
94	      h => bool.and_l(C.CapSet.subset(a, p), C.CapSet.subset(a, i))(bool.and_r(C.CapSet.subset(e, p), Bool.and(C.CapSet.subset(a, p), C.CapSet.subset(a, i)))(h))
95	
96	def valid.ai(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool}:
97	  match s:
98	    case C.CapState{+p, +i, +e, +b, +a}:
99	      h => bool.and_r(C.CapSet.subset(a, p), C.CapSet.subset(a, i))(bool.and_r(C.CapSet.subset(e, p), Bool.and(C.CapSet.subset(a, p), C.CapSet.subset(a, i)))(h))
100	
101	def bool.and2(+x: Bool, +y: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {Bool.and(x, y) == True{} : Bool}:
102	  match x:
103	    case True{}:
104	      hx => hy => hy
105	    case False{}:
106	      hx => hy => bits.absurd(Bool.and(False{}, y), hx)
107	
108	# A set and its two parts. A set is a native U32 (capabilities 0 to 31) and
109	# a Word(9n) (32 to 40); opening the U32 gives its Word(32n). The subset test
110	# on the low word is native (a & ~b == 0), and is the bitwise test there:
111	
112	def set.fin_ff(+t: Cmp) -> {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == Cmp.is_eq(t) : Bool}:
113	  match t:
114	    case LT{}:
115	      {==}
116	    case EQ{}:
117	      {==}
118	    case GT{}:
119	      {==}
120	
121	def set.fin_tf(+t: Cmp) -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, t)) == False{} : Bool}:
122	  match t:
123	    case LT{}:
124	      {==}
125	    case EQ{}:
126	      {==}
127	    case GT{}:
128	      {==}
129	
130	def set.bridge(+n: Nat, +x: Word(n), +y: Word(n)) -> {Cmp.is_eq(Word.cmp(n, Word.and(n, x, Word.not(n, y)), Word.zero(n))) == C.CapBits.subset(n, x, y) : Bool}:
131	  match n:
132	    case 0n:
133	      {==}
134	    case 1n+p:
135	      match x y:
136	        case WCon{True{}, +xt} WCon{True{}, +yt}:
137	          Equal.trans(Bool, Cmp.is_eq(Word.cmp.fin(False{}, False{}, Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p)))), Cmp.is_eq(Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p))), C.CapBits.subset(p, xt, yt), set.fin_ff(Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p))), set.bridge(p, xt, yt))
138	        case WCon{True{}, +xt} WCon{False{}, +yt}:
139	          set.fin_tf(Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p)))
140	        case WCon{False{}, +xt} WCon{+yb, +yt}:
141	          Equal.trans(Bool, Cmp.is_eq(Word.cmp.fin(False{}, False{}, Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p)))), Cmp.is_eq(Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p))), C.CapBits.subset(p, xt, yt), set.fin_ff(Word.cmp(p, Word.and(p, xt, Word.not(p, yt)), Word.zero(p))), set.bridge(p, xt, yt))
142	
143	# a set within another, from its parts within theirs, and back
144	def set.sub_intro(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapBits.subset(32n, al, bl) == True{} : Bool} -> {C.CapBits.subset(9n, ah, bh) == True{} : Bool} -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool}:
145	  hl => hh =>
146	    %Equal.sym(Bool, Cmp.is_eq(Word.cmp(32n, Word.and(32n, al, Word.not(32n, bl)), Word.zero(32n))), C.CapBits.subset(32n, al, bl), set.bridge(32n, al, bl)) : {Bool.and(_, C.CapBits.subset(9n, ah, bh)) == True{} : Bool}
147	    bool.and2(C.CapBits.subset(32n, al, bl), C.CapBits.subset(9n, ah, bh))(hl)(hh)
148	
149	def set.sub_lo(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool} -> {C.CapBits.subset(32n, al, bl) == True{} : Bool}:
150	  h =>
151	    %set.bridge(32n, al, bl) : {_ == True{} : Bool}
152	    bool.and_l(Cmp.is_eq(Word.cmp(32n, Word.and(32n, al, Word.not(32n, bl)), Word.zero(32n))), C.CapBits.subset(9n, ah, bh))(h)
153	
154	def set.sub_hi(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool} -> {C.CapBits.subset(9n, ah, bh) == True{} : Bool}:
155	  h => bool.and_r(Cmp.is_eq(Word.cmp(32n, Word.and(32n, al, Word.not(32n, bl)), Word.zero(32n))), C.CapBits.subset(9n, ah, bh))(h)
156	
157	# two sets are equal when their parts are
158	def set.eq_intro(+l1: Word(32n), +l2: Word(32n), +h1: Word(9n), +h2: Word(9n), +e1: {l1 == l2 : Word(32n)}, +e2: {h1 == h2 : Word(9n)}) -> {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l2}, h2} : C.CapSet()}:
159	  %e1 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{_}, h2} : C.CapSet()}
160	  %e2 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l1}, _} : C.CapSet()}
161	  {==}
162	
163	# BEGIN GENERATED by gen/proof.py: lemmas
164	# Per-bit lemmas (generated: every combination of the bits at each position)
165	
166	def bits.sub_refl(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, x, x) == True{} : Bool}:
167	  match n:
168	    case 0n:
169	      {==}
170	    case 1n+n1:
171	      match x:
172	        case WCon{True{}, +xt}:
173	          bits.sub_refl(n1, xt)
174	        case WCon{False{}, +xt}:
175	          bits.sub_refl(n1, xt)
176	
177	def bits.sub_zero(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, Word.zero(n), x) == True{} : Bool}:
178	  match n:
179	    case 0n:
180	      {==}
181	    case 1n+n1:
182	      match x:
183	        case WCon{True{}, +xt}:
184	          bits.sub_zero(n1, xt)
185	        case WCon{False{}, +xt}:
186	          bits.sub_zero(n1, xt)
187	
188	def bits.sub_or_r(+n: Nat, +x: Word(n), +c: Word(n)) -> {C.CapBits.subset(n, c, Word.or(n, x, c)) == True{} : Bool}:
189	  match n:
190	    case 0n:
191	      {==}
192	    case 1n+n1:
193	      match x c:
194	        case WCon{True{}, +xt} WCon{True{}, +ct}:
195	          bits.sub_or_r(n1, xt, ct)
196	        case WCon{True{}, +xt} WCon{False{}, +ct}:
197	          bits.sub_or_r(n1, xt, ct)
198	        case WCon{False{}, +xt} WCon{True{}, +ct}:
199	          bits.sub_or_r(n1, xt, ct)
200	        case WCon{False{}, +xt} WCon{False{}, +ct}:
201	          bits.sub_or_r(n1, xt, ct)
202	
203	def bits.sub_minus(+n: Nat, +x: Word(n), +y: Word(n)) -> {C.CapBits.subset(n, Word.and(n, x, Word.not(n, y)), x) == True{} : Bool}:
204	  match n:
205	    case 0n:
206	      {==}
207	    case 1n+n1:
208	      match x y:
209	        case WCon{True{}, +xt} WCon{True{}, +yt}:
210	          bits.sub_minus(n1, xt, yt)
211	        case WCon{True{}, +xt} WCon{False{}, +yt}:
212	          bits.sub_minus(n1, xt, yt)
213	        case WCon{False{}, +xt} WCon{True{}, +yt}:
214	          bits.sub_minus(n1, xt, yt)
215	        case WCon{False{}, +xt} WCon{False{}, +yt}:
216	          bits.sub_minus(n1, xt, yt)
217	
218	def bits.bound_a(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}:
219	  match n:
220	    case 0n:
221	      {==}
222	    case 1n+n1:
223	      match i fi fp b a:
224	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
225	          bits.bound_a(n1, it, fit, fpt, bt, at)
226	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
227	          bits.bound_a(n1, it, fit, fpt, bt, at)
228	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
229	          bits.bound_a(n1, it, fit, fpt, bt, at)
230	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
231	          bits.bound_a(n1, it, fit, fpt, bt, at)
232	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
233	          bits.bound_a(n1, it, fit, fpt, bt, at)
234	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
235	          bits.bound_a(n1, it, fit, fpt, bt, at)
236	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
237	          bits.bound_a(n1, it, fit, fpt, bt, at)
238	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
239	          bits.bound_a(n1, it, fit, fpt, bt, at)
240	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
241	          bits.bound_a(n1, it, fit, fpt, bt, at)
242	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
243	          bits.bound_a(n1, it, fit, fpt, bt, at)
244	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
245	          bits.bound_a(n1, it, fit, fpt, bt, at)
246	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
247	          bits.bound_a(n1, it, fit, fpt, bt, at)
248	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
249	          bits.bound_a(n1, it, fit, fpt, bt, at)
250	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
251	          bits.bound_a(n1, it, fit, fpt, bt, at)
252	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
253	          bits.bound_a(n1, it, fit, fpt, bt, at)
254	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
255	          bits.bound_a(n1, it, fit, fpt, bt, at)
256	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
257	          bits.bound_a(n1, it, fit, fpt, bt, at)
258	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
259	          bits.bound_a(n1, it, fit, fpt, bt, at)
260	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
261	          bits.bound_a(n1, it, fit, fpt, bt, at)
262	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
263	          bits.bound_a(n1, it, fit, fpt, bt, at)
264	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
265	          bits.bound_a(n1, it, fit, fpt, bt, at)
266	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
267	          bits.bound_a(n1, it, fit, fpt, bt, at)
268	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
269	          bits.bound_a(n1, it, fit, fpt, bt, at)
270	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
271	          bits.bound_a(n1, it, fit, fpt, bt, at)
272	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
273	          bits.bound_a(n1, it, fit, fpt, bt, at)
274	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
275	          bits.bound_a(n1, it, fit, fpt, bt, at)
276	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
277	          bits.bound_a(n1, it, fit, fpt, bt, at)
278	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
279	          bits.bound_a(n1, it, fit, fpt, bt, at)
280	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
281	          bits.bound_a(n1, it, fit, fpt, bt, at)
282	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
283	          bits.bound_a(n1, it, fit, fpt, bt, at)
284	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
285	          bits.bound_a(n1, it, fit, fpt, bt, at)
286	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
287	          bits.bound_a(n1, it, fit, fpt, bt, at)
288	
289	def bits.bound_z(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), Word.zero(n)), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}:
290	  match n:
291	    case 0n:
292	      {==}
293	    case 1n+n1:
294	      match i fi fp b a:
295	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
296	          bits.bound_z(n1, it, fit, fpt, bt, at)
297	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
298	          bits.bound_z(n1, it, fit, fpt, bt, at)
299	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
300	          bits.bound_z(n1, it, fit, fpt, bt, at)
301	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
302	          bits.bound_z(n1, it, fit, fpt, bt, at)
303	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
304	          bits.bound_z(n1, it, fit, fpt, bt, at)
305	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
306	          bits.bound_z(n1, it, fit, fpt, bt, at)
307	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
308	          bits.bound_z(n1, it, fit, fpt, bt, at)
309	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
310	          bits.bound_z(n1, it, fit, fpt, bt, at)
311	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
312	          bits.bound_z(n1, it, fit, fpt, bt, at)
313	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
314	          bits.bound_z(n1, it, fit, fpt, bt, at)
315	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
316	          bits.bound_z(n1, it, fit, fpt, bt, at)
317	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
318	          bits.bound_z(n1, it, fit, fpt, bt, at)
319	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
320	          bits.bound_z(n1, it, fit, fpt, bt, at)
321	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
322	          bits.bound_z(n1, it, fit, fpt, bt, at)
323	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
324	          bits.bound_z(n1, it, fit, fpt, bt, at)
325	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
326	          bits.bound_z(n1, it, fit, fpt, bt, at)
327	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
328	          bits.bound_z(n1, it, fit, fpt, bt, at)
329	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
330	          bits.bound_z(n1, it, fit, fpt, bt, at)
331	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
332	          bits.bound_z(n1, it, fit, fpt, bt, at)
333	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
334	          bits.bound_z(n1, it, fit, fpt, bt, at)
335	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
336	          bits.bound_z(n1, it, fit, fpt, bt, at)
337	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
338	          bits.bound_z(n1, it, fit, fpt, bt, at)
339	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
340	          bits.bound_z(n1, it, fit, fpt, bt, at)
341	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
342	          bits.bound_z(n1, it, fit, fpt, bt, at)
343	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
344	          bits.bound_z(n1, it, fit, fpt, bt, at)
345	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
346	          bits.bound_z(n1, it, fit, fpt, bt, at)
347	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
348	          bits.bound_z(n1, it, fit, fpt, bt, at)
349	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
350	          bits.bound_z(n1, it, fit, fpt, bt, at)
351	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
352	          bits.bound_z(n1, it, fit, fpt, bt, at)
353	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
354	          bits.bound_z(n1, it, fit, fpt, bt, at)
355	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
356	          bits.bound_z(n1, it, fit, fpt, bt, at)
357	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
358	          bits.bound_z(n1, it, fit, fpt, bt, at)
359	
360	def bits.bound_va(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, a, i) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, i)) == True{} : Bool}:
361	  match n:
362	    case 0n:
363	      h0 => {==}
364	    case 1n+n1:
365	      match i fi fp b a:
366	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
367	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
368	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
369	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
370	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
371	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
372	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
373	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
374	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
375	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
376	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
377	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
378	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
379	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
380	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
381	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
382	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
383	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
384	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
385	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
386	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
387	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
388	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
389	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
390	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
391	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
392	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
393	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
394	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
395	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
396	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
397	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
398	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
399	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
400	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
401	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
402	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
403	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
404	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
405	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
406	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
407	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
408	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
409	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
410	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
411	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
412	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
413	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
414	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
415	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
416	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
417	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
418	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
419	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
420	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
421	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
422	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
423	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
424	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
425	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
426	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
427	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
428	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
429	          h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
430	
431	def bits.bound_vz(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), Word.zero(n)), Word.or(n, b, i)) == True{} : Bool}:
432	  match n:
433	    case 0n:
434	      {==}
435	    case 1n+n1:
436	      match i fi fp b:
437	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
438	          bits.bound_vz(n1, it, fit, fpt, bt)
439	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
440	          bits.bound_vz(n1, it, fit, fpt, bt)
441	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
442	          bits.bound_vz(n1, it, fit, fpt, bt)
443	        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
444	          bits.bound_vz(n1, it, fit, fpt, bt)
445	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
446	          bits.bound_vz(n1, it, fit, fpt, bt)
447	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
448	          bits.bound_vz(n1, it, fit, fpt, bt)
449	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
450	          bits.bound_vz(n1, it, fit, fpt, bt)
451	        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
452	          bits.bound_vz(n1, it, fit, fpt, bt)
453	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
454	          bits.bound_vz(n1, it, fit, fpt, bt)
455	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
456	          bits.bound_vz(n1, it, fit, fpt, bt)
457	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
458	          bits.bound_vz(n1, it, fit, fpt, bt)
459	        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
460	          bits.bound_vz(n1, it, fit, fpt, bt)
461	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
462	          bits.bound_vz(n1, it, fit, fpt, bt)
463	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
464	          bits.bound_vz(n1, it, fit, fpt, bt)
465	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
466	          bits.bound_vz(n1, it, fit, fpt, bt)
467	        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
468	          bits.bound_vz(n1, it, fit, fpt, bt)
469	
470	def bits.amb_p(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), p) == True{} : Bool}:
471	  match n:
472	    case 0n:
473	      {==}
474	    case 1n+n1:
475	      match a p i:
476	        case WCon{True{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
477	          bits.amb_p(n1, at, pt, it)
478	        case WCon{True{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
479	          bits.amb_p(n1, at, pt, it)
480	        case WCon{True{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
481	          bits.amb_p(n1, at, pt, it)
482	        case WCon{True{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
483	          bits.amb_p(n1, at, pt, it)
484	        case WCon{False{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
485	          bits.amb_p(n1, at, pt, it)
486	        case WCon{False{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
487	          bits.amb_p(n1, at, pt, it)
488	        case WCon{False{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
489	          bits.amb_p(n1, at, pt, it)
490	        case WCon{False{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
491	          bits.amb_p(n1, at, pt, it)
492	
493	def bits.amb_i(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), i) == True{} : Bool}:
494	  match n:
495	    case 0n:
496	      {==}
497	    case 1n+n1:
498	      match a p i:
499	        case WCon{True{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
500	          bits.amb_i(n1, at, pt, it)
501	        case WCon{True{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
502	          bits.amb_i(n1, at, pt, it)
503	        case WCon{True{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
504	          bits.amb_i(n1, at, pt, it)
505	        case WCon{True{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
506	          bits.amb_i(n1, at, pt, it)
507	        case WCon{False{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
508	          bits.amb_i(n1, at, pt, it)
509	        case WCon{False{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
510	          bits.amb_i(n1, at, pt, it)
511	        case WCon{False{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
512	          bits.amb_i(n1, at, pt, it)
513	        case WCon{False{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
514	          bits.amb_i(n1, at, pt, it)
515	
516	def bits.lub(+n: Nat, +a: Word(n), +s: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, s, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, a, s), p) == True{} : Bool}:
517	  match n:
518	    case 0n:
519	      h0 => h1 => {==}
520	    case 1n+n1:
521	      match a s p:
522	        case WCon{True{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
523	          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
524	        case WCon{True{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
525	          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h0)
526	        case WCon{True{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
527	          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
528	        case WCon{True{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
529	          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{False{}, st}), WCon{False{}, pt}), h0)
530	        case WCon{False{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
531	          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
532	        case WCon{False{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
533	          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{False{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h1)
534	        case WCon{False{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
535	          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
536	        case WCon{False{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
537	          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
538	
539	def bits.minus_within(+n: Nat, +a: Word(n), +y: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.and(n, a, Word.not(n, y)), p) == True{} : Bool}:
540	  match n:
541	    case 0n:
542	      h0 => {==}
543	    case 1n+n1:
544	      match a y p:
545	        case WCon{True{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
546	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
547	        case WCon{True{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
548	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.and(1n+n1, WCon{True{}, at}, Word.not(1n+n1, WCon{True{}, yt})), WCon{False{}, pt}), h0)
549	        case WCon{True{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
550	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
551	        case WCon{True{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
552	          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.and(1n+n1, WCon{True{}, at}, Word.not(1n+n1, WCon{False{}, yt})), WCon{False{}, pt}), h0)
553	        case WCon{False{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
554	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
555	        case WCon{False{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
556	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
557	        case WCon{False{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
558	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
559	        case WCon{False{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
560	          h0 => bits.minus_within(n1, at, yt, pt)(h0)
561	
562	def bits.root_a(+n: Nat, +i: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, a, i) == True{} : Bool} -> {Word.or(n, Word.or(n, Word.and(n, i, C.CapBits.all(n)), Word.and(n, C.CapBits.all(n), b)), a) == Word.or(n, i, b) : Word(n)}:
563	  match n:
564	    case 0n:
565	      match i b a:
566	        case WNil{} WNil{} WNil{}:
567	          h0 => {==}
568	    case 1n+n1:
569	      match i b a:
570	        case WCon{True{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
571	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
572	        case WCon{True{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
573	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
574	        case WCon{True{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
575	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
576	        case WCon{True{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
577	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
578	        case WCon{False{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
579	          h0 => bits.absurd_eq(Word(1n+n1), Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, C.CapBits.all(1n+n1)), Word.and(1n+n1, C.CapBits.all(1n+n1), WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, it}, WCon{True{}, bt}), h0)
580	        case WCon{False{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
581	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
582	        case WCon{False{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
583	          h0 => bits.absurd_eq(Word(1n+n1), Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, C.CapBits.all(1n+n1)), Word.and(1n+n1, C.CapBits.all(1n+n1), WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, it}, WCon{False{}, bt}), h0)
584	        case WCon{False{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
585	          h0 => Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), at), Word.or(n1, it, bt), bits.root_a(n1, it, bt, at)(h0))
586	
587	def bits.root_z(+n: Nat, +i: Word(n), +b: Word(n)) -> {Word.or(n, Word.or(n, Word.and(n, i, C.CapBits.all(n)), Word.and(n, C.CapBits.all(n), b)), Word.zero(n)) == Word.or(n, i, b) : Word(n)}:
588	  match n:
589	    case 0n:
590	      match i b:
591	        case WNil{} WNil{}:
592	          {==}
593	    case 1n+n1:
594	      match i b:
595	        case WCon{True{}, +it} WCon{True{}, +bt}:
596	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), Word.zero(n1)), Word.or(n1, it, bt), bits.root_z(n1, it, bt))
597	        case WCon{True{}, +it} WCon{False{}, +bt}:
598	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), Word.zero(n1)), Word.or(n1, it, bt), bits.root_z(n1, it, bt))
599	        case WCon{False{}, +it} WCon{True{}, +bt}:
600	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), Word.zero(n1)), Word.or(n1, it, bt), bits.root_z(n1, it, bt))
601	        case WCon{False{}, +it} WCon{False{}, +bt}:
602	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, C.CapBits.all(n1)), Word.and(n1, C.CapBits.all(n1), bt)), Word.zero(n1)), Word.or(n1, it, bt), bits.root_z(n1, it, bt))
603	
604	def bits.nonroot(+n: Nat, +i: Word(n), +b: Word(n), +a: Word(n)) -> {Word.or(n, Word.or(n, Word.and(n, i, Word.zero(n)), Word.and(n, Word.zero(n), b)), a) == a : Word(n)}:
605	  match n:
606	    case 0n:
607	      match i b a:
608	        case WNil{} WNil{} WNil{}:
609	          {==}
610	    case 1n+n1:
611	      match i b a:
612	        case WCon{True{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
613	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
614	        case WCon{True{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
615	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
616	        case WCon{True{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
617	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
618	        case WCon{True{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
619	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
620	        case WCon{False{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
621	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
622	        case WCon{False{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
623	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
624	        case WCon{False{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
625	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
626	        case WCon{False{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
627	          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
628	
629	# The same facts on capability sets: each splits its sets into their two
630	# parts and applies the per-bit lemma at widths 32 and 9.
631	
632	def set.sub_refl(+x: C.CapSet()) -> {C.CapSet.subset(x, x) == True{} : Bool}:
633	  match x:
634	    case C.CapSetW{U32{+xl}, +xh}:
635	      set.sub_intro(xl, xl, xh, xh)(bits.sub_refl(32n, xl))(bits.sub_refl(9n, xh))
636	
637	def set.sub_zero(+x: C.CapSet()) -> {C.CapSet.subset(C.CapSet.empty(), x) == True{} : Bool}:
638	  match x:
639	    case C.CapSetW{U32{+xl}, +xh}:
640	      set.sub_intro(Word.zero(32n), xl, Word.zero(9n), xh)(bits.sub_zero(32n, xl))(bits.sub_zero(9n, xh))
641	
642	def set.sub_or_r(+x: C.CapSet(), +c: C.CapSet()) -> {C.CapSet.subset(c, C.CapSet.union(x, c)) == True{} : Bool}:
643	  match x c:
644	    case C.CapSetW{U32{+xl}, +xh} C.CapSetW{U32{+cl}, +ch}:
645	      set.sub_intro(cl, Word.or(32n, xl, cl), ch, Word.or(9n, xh, ch))(bits.sub_or_r(32n, xl, cl))(bits.sub_or_r(9n, xh, ch))
646	
647	def set.sub_minus(+x: C.CapSet(), +y: C.CapSet()) -> {C.CapSet.subset(C.CapSet.minus(x, y), x) == True{} : Bool}:
648	  match x y:
649	    case C.CapSetW{U32{+xl}, +xh} C.CapSetW{U32{+yl}, +yh}:
650	      set.sub_intro(Word.and(32n, xl, Word.not(32n, yl)), xl, Word.and(9n, xh, Word.not(9n, yh)), xh)(bits.sub_minus(32n, xl, yl))(bits.sub_minus(9n, xh, yh))
651	
652	def set.bound_a(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a), C.CapSet.union(b, C.CapSet.union(i, a))) == True{} : Bool}:
653	  match i fi fp b a:
654	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+fil}, +fih} C.CapSetW{U32{+fpl}, +fph} C.CapSetW{U32{+bl}, +bh} C.CapSetW{U32{+al}, +ah}:
655	      set.sub_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, fil), Word.and(32n, fpl, bl)), al), Word.or(32n, bl, Word.or(32n, il, al)), Word.or(9n, Word.or(9n, Word.and(9n, ih, fih), Word.and(9n, fph, bh)), ah), Word.or(9n, bh, Word.or(9n, ih, ah)))(bits.bound_a(32n, il, fil, fpl, bl, al))(bits.bound_a(9n, ih, fih, fph, bh, ah))
656	
657	def set.bound_z(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()), C.CapSet.union(b, C.CapSet.union(i, a))) == True{} : Bool}:
658	  match i fi fp b a:
659	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+fil}, +fih} C.CapSetW{U32{+fpl}, +fph} C.CapSetW{U32{+bl}, +bh} C.CapSetW{U32{+al}, +ah}:
660	      set.sub_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, fil), Word.and(32n, fpl, bl)), Word.zero(32n)), Word.or(32n, bl, Word.or(32n, il, al)), Word.or(9n, Word.or(9n, Word.and(9n, ih, fih), Word.and(9n, fph, bh)), Word.zero(9n)), Word.or(9n, bh, Word.or(9n, ih, ah)))(bits.bound_z(32n, il, fil, fpl, bl, al))(bits.bound_z(9n, ih, fih, fph, bh, ah))
661	
662	def set.bound_va(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(a, i) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a), C.CapSet.union(b, i)) == True{} : Bool}:
663	  match i fi fp b a:
664	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+fil}, +fih} C.CapSetW{U32{+fpl}, +fph} C.CapSetW{U32{+bl}, +bh} C.CapSetW{U32{+al}, +ah}:
665	      +h0 => set.sub_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, fil), Word.and(32n, fpl, bl)), al), Word.or(32n, bl, il), Word.or(9n, Word.or(9n, Word.and(9n, ih, fih), Word.and(9n, fph, bh)), ah), Word.or(9n, bh, ih))(bits.bound_va(32n, il, fil, fpl, bl, al)(set.sub_lo(al, il, ah, ih)(h0)))(bits.bound_va(9n, ih, fih, fph, bh, ah)(set.sub_hi(al, il, ah, ih)(h0)))
666	
667	def set.bound_vz(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()), C.CapSet.union(b, i)) == True{} : Bool}:
668	  match i fi fp b:
669	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+fil}, +fih} C.CapSetW{U32{+fpl}, +fph} C.CapSetW{U32{+bl}, +bh}:
670	      set.sub_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, fil), Word.and(32n, fpl, bl)), Word.zero(32n)), Word.or(32n, bl, il), Word.or(9n, Word.or(9n, Word.and(9n, ih, fih), Word.and(9n, fph, bh)), Word.zero(9n)), Word.or(9n, bh, ih))(bits.bound_vz(32n, il, fil, fpl, bl))(bits.bound_vz(9n, ih, fih, fph, bh))
671	
672	def set.amb_p(+a: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(a, p), i), p) == True{} : Bool}:
673	  match a p i:
674	    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+pl}, +ph} C.CapSetW{U32{+il}, +ih}:
675	      set.sub_intro(Word.and(32n, Word.and(32n, al, pl), il), pl, Word.and(9n, Word.and(9n, ah, ph), ih), ph)(bits.amb_p(32n, al, pl, il))(bits.amb_p(9n, ah, ph, ih))
676	
677	def set.amb_i(+a: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(a, p), i), i) == True{} : Bool}:
678	  match a p i:
679	    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+pl}, +ph} C.CapSetW{U32{+il}, +ih}:
680	      set.sub_intro(Word.and(32n, Word.and(32n, al, pl), il), il, Word.and(9n, Word.and(9n, ah, ph), ih), ih)(bits.amb_i(32n, al, pl, il))(bits.amb_i(9n, ah, ph, ih))
681	
682	def set.lub(+a: C.CapSet(), +s: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(s, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(a, s), p) == True{} : Bool}:
683	  match a s p:
684	    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+sl}, +sh} C.CapSetW{U32{+pl}, +ph}:
685	      +h0 => +h1 => set.sub_intro(Word.or(32n, al, sl), pl, Word.or(9n, ah, sh), ph)(bits.lub(32n, al, sl, pl)(set.sub_lo(al, pl, ah, ph)(h0))(set.sub_lo(sl, pl, sh, ph)(h1)))(bits.lub(9n, ah, sh, ph)(set.sub_hi(al, pl, ah, ph)(h0))(set.sub_hi(sl, pl, sh, ph)(h1)))
686	
687	def set.minus_within(+a: C.CapSet(), +y: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.minus(a, y), p) == True{} : Bool}:
688	  match a y p:
689	    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+yl}, +yh} C.CapSetW{U32{+pl}, +ph}:
690	      +h0 => set.sub_intro(Word.and(32n, al, Word.not(32n, yl)), pl, Word.and(9n, ah, Word.not(9n, yh)), ph)(bits.minus_within(32n, al, yl, pl)(set.sub_lo(al, pl, ah, ph)(h0)))(bits.minus_within(9n, ah, yh, ph)(set.sub_hi(al, pl, ah, ph)(h0)))
691	
692	def set.root_a(+i: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(a, i) == True{} : Bool} -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.full()), C.CapSet.inter(C.CapSet.full(), b)), a) == C.CapSet.union(i, b) : C.CapSet()}:
693	  match i b a:
694	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+bl}, +bh} C.CapSetW{U32{+al}, +ah}:
695	      +h0 => set.eq_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, C.CapBits.all(32n)), Word.and(32n, C.CapBits.all(32n), bl)), al), Word.or(32n, il, bl), Word.or(9n, Word.or(9n, Word.and(9n, ih, C.CapBits.all(9n)), Word.and(9n, C.CapBits.all(9n), bh)), ah), Word.or(9n, ih, bh), bits.root_a(32n, il, bl, al)(set.sub_lo(al, il, ah, ih)(h0)), bits.root_a(9n, ih, bh, ah)(set.sub_hi(al, il, ah, ih)(h0)))
696	
697	def set.root_z(+i: C.CapSet(), +b: C.CapSet()) -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.full()), C.CapSet.inter(C.CapSet.full(), b)), C.CapSet.empty()) == C.CapSet.union(i, b) : C.CapSet()}:
698	  match i b:
699	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+bl}, +bh}:
700	      set.eq_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, C.CapBits.all(32n)), Word.and(32n, C.CapBits.all(32n), bl)), Word.zero(32n)), Word.or(32n, il, bl), Word.or(9n, Word.or(9n, Word.and(9n, ih, C.CapBits.all(9n)), Word.and(9n, C.CapBits.all(9n), bh)), Word.zero(9n)), Word.or(9n, ih, bh), bits.root_z(32n, il, bl), bits.root_z(9n, ih, bh))
701	
702	def set.nonroot(+i: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.empty()), C.CapSet.inter(C.CapSet.empty(), b)), a) == a : C.CapSet()}:
703	  match i b a:
704	    case C.CapSetW{U32{+il}, +ih} C.CapSetW{U32{+bl}, +bh} C.CapSetW{U32{+al}, +ah}:
705	      set.eq_intro(Word.or(32n, Word.or(32n, Word.and(32n, il, Word.zero(32n)), Word.and(32n, Word.zero(32n), bl)), al), al, Word.or(9n, Word.or(9n, Word.and(9n, ih, Word.zero(9n)), Word.and(9n, Word.zero(9n), bh)), ah), ah, bits.nonroot(32n, il, bl, al), bits.nonroot(9n, ih, bh, ah))
706	
707	# END GENERATED: lemmas
708	
709	# a set that has capability k contains the set {k} (has is that subset test)
710	def caps.has_of(+v: Bool, +s: C.CapSet(), +x: U32) -> {C.CapSet.has.go(v, s, x) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.of.go(v, x), s) == True{} : Bool}:
711	  match v:
712	    case False{}:
713	      h => bits.absurd(C.CapSet.subset(C.CapSet.of.go(False{}, x), s), h)
714	    case True{}:
715	      h => h
716	
717	# BEGIN GENERATED by gen/proof.py: laws
718	# execve: the transformation, for every flags record and state
719	
720	def ex.eff(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.effective(E.CapExec.sets(fl, s)), C.CapState.permitted(E.CapExec.sets(fl, s))) == True{} : Bool}:
721	  match fl s:
722	    case E.CapExecFlags{True{}, True{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
723	      set.sub_refl(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()))
724	    case E.CapExecFlags{True{}, False{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
725	      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty())
726	    case E.CapExecFlags{False{}, True{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
727	      set.sub_refl(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a))
728	    case E.CapExecFlags{False{}, False{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
729	      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a)
730	
731	def ex.ap(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(E.CapExec.sets(fl, s)), C.CapState.permitted(E.CapExec.sets(fl, s))) == True{} : Bool}:
732	  match fl s:
733	    case E.CapExecFlags{True{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
734	      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty())
735	    case E.CapExecFlags{False{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
736	      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a)
737	
738	def ex.ai(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(E.CapExec.sets(fl, s)), C.CapState.inheritable(E.CapExec.sets(fl, s))) == True{} : Bool}:
739	  match fl s:
740	    case E.CapExecFlags{True{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
741	      h => set.sub_zero(i)
742	    case E.CapExecFlags{False{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
743	      h => h
744	
745	def ex.bnd(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapState.bounding(E.CapExec.sets(fl, s)) == C.CapState.bounding(s) : C.CapSet()}:
746	  match fl s:
747	    case E.CapExecFlags{priv, feff, fp, fi} C.CapState{+p, +i, +e, +b, +a}:
748	      {==}
749	
750	def ex.inh(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapState.inheritable(E.CapExec.sets(fl, s)) == C.CapState.inheritable(s) : C.CapSet()}:
751	  match fl s:
752	    case E.CapExecFlags{priv, feff, fp, fi} C.CapState{+p, +i, +e, +b, +a}:
753	      {==}
754	
755	def ex.bound(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.permitted(E.CapExec.sets(fl, s)), C.CapSet.union(C.CapState.bounding(s), C.CapSet.union(C.CapState.inheritable(s), C.CapState.ambient(s)))) == True{} : Bool}:
756	  match fl s:
757	    case E.CapExecFlags{True{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
758	      set.bound_z(i, fi, fp, b, a)
759	    case E.CapExecFlags{False{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
760	      set.bound_a(i, fi, fp, b, a)
761	
762	def ex.bound_v(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(E.CapExec.sets(fl, s)), C.CapSet.union(C.CapState.bounding(s), C.CapState.inheritable(s))) == True{} : Bool}:
763	  match fl s:
764	    case E.CapExecFlags{True{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
765	      h => set.bound_vz(i, fi, fp, b)
766	    case E.CapExecFlags{False{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
767	      h => set.bound_va(i, fi, fp, b, a)(h)
768	
769	def ex.root_p(+priv: Bool, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapState.permitted(E.CapExec.sets(E.CapExecFlags{priv, True{}, C.CapSet.full(), C.CapSet.full()}, s)) == C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s)) : C.CapSet()}:
770	  match priv s:
771	    case True{} C.CapState{+p, +i, +e, +b, +a}:
772	      h => set.root_z(i, b)
773	    case False{} C.CapState{+p, +i, +e, +b, +a}:
774	      h => set.root_a(i, b, a)(h)
775	
776	def ex.root_e(+priv: Bool, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapState.effective(E.CapExec.sets(E.CapExecFlags{priv, True{}, C.CapSet.full(), C.CapSet.full()}, s)) == C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s)) : C.CapSet()}:
777	  match priv s:
778	    case True{} C.CapState{+p, +i, +e, +b, +a}:
779	      h => set.root_z(i, b)
780	    case False{} C.CapState{+p, +i, +e, +b, +a}:
781	      h => set.root_a(i, b, a)(h)
782	
783	def ex.nonroot_p(+nr: Bool, +r0: Bool, +e0: Bool, +s: C.CapState) -> {r0 == False{} : Bool} -> {e0 == False{} : Bool} -> {C.CapState.permitted(E.CapExec.sets(E.CapExec.flags.go(nr, r0, e0, False{}, None{}), s)) == C.CapState.ambient(s) : C.CapSet()}:
784	  match nr r0 e0 s:
785	    case True{} r0 e0 C.CapState{+p, +i, +e, +b, +a}:
786	      hr => he => set.nonroot(i, b, a)
787	    case False{} True{} e0 C.CapState{+p, +i, +e, +b, +a}:
788	      hr => he => bits.absurd_tf(C.CapSet(), C.CapState.permitted(E.CapExec.sets(E.CapExec.flags.go(False{}, True{}, e0, False{}, None{}), C.CapState{p, i, e, b, a})), a, hr)
789	    case False{} False{} True{} C.CapState{+p, +i, +e, +b, +a}:
790	      hr => he => bits.absurd_tf(C.CapSet(), C.CapState.permitted(E.CapExec.sets(E.CapExec.flags.go(False{}, False{}, True{}, False{}, None{}), C.CapState{p, i, e, b, a})), a, he)
791	    case False{} False{} False{} C.CapState{+p, +i, +e, +b, +a}:
792	      hr => he => set.nonroot(i, b, a)
793	
794	def ex.nonroot_e(+nr: Bool, +r0: Bool, +e0: Bool, +s: C.CapState) -> {r0 == False{} : Bool} -> {e0 == False{} : Bool} -> {C.CapState.effective(E.CapExec.sets(E.CapExec.flags.go(nr, r0, e0, False{}, None{}), s)) == C.CapState.ambient(s) : C.CapSet()}:
795	  match nr r0 e0 s:
796	    case True{} r0 e0 C.CapState{+p, +i, +e, +b, +a}:
797	      hr => he => {==}
798	    case False{} True{} e0 C.CapState{+p, +i, +e, +b, +a}:
799	      hr => he => bits.absurd_tf(C.CapSet(), C.CapState.effective(E.CapExec.sets(E.CapExec.flags.go(False{}, True{}, e0, False{}, None{}), C.CapState{p, i, e, b, a})), a, hr)
800	    case False{} False{} True{} C.CapState{+p, +i, +e, +b, +a}:
801	      hr => he => bits.absurd_tf(C.CapSet(), C.CapState.effective(E.CapExec.sets(E.CapExec.flags.go(False{}, False{}, True{}, False{}, None{}), C.CapState{p, i, e, b, a})), a, he)
802	    case False{} False{} False{} C.CapState{+p, +i, +e, +b, +a}:
803	      hr => he => {==}
804	
805	def ex.result(+ok: Bool, +c: C.CapCred, +eu: U32, +s: C.CapState) -> {C.Caps.sets_or(E.CapExec.fin(ok, c, eu, s), s) == s : C.CapState}:
806	  match ok c:
807	    case False{} c:
808	      {==}
809	    case True{} C.CapCred{r, e, sv, nr, na, st}:
810	      {==}
811	
812	# capset: each rule in turn
813	def cs.p.done(+c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.done(c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}:
814	  match c:
815	    case C.CapCred{r, eu, sv, nr, na, C.CapState{+op, +oi, +oe, +ob, +oa}}:
816	      h => h
817	
818	def cs.p.r4(+sp: Bool, +iok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r4(sp, iok, c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}:
819	  match sp iok:
820	    case True{} iok:
821	      h => cs.p.done(c, e, p, i)(h)
822	    case False{} True{}:
823	      h => cs.p.done(c, e, p, i)(h)
824	    case False{} False{}:
825	      h => set.sub_refl(C.CapState.permitted(C.CapCred.sets(c)))
826	
827	def cs.p.r3(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r3(ok, c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}:
828	  match ok:
829	    case False{}:
830	      h => set.sub_refl(C.CapState.permitted(C.CapCred.sets(c)))
831	    case True{}:
832	      h => cs.p.r4(C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.permitted(C.CapCred.sets(c)))), c, e, p, i)(h)
833	
834	def cs.p.r2(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r2(ok, c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}:
835	  match ok:
836	    case False{}:
837	      h => set.sub_refl(C.CapState.permitted(C.CapCred.sets(c)))
838	    case True{}:
839	      h => cs.p.r3(C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.bounding(C.CapCred.sets(c)))), c, e, p, i)(h)
840	
841	def cs.p.r1(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))) == ok : Bool} -> {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r1(ok, c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}:
842	  match ok:
843	    case False{}:
844	      h => set.sub_refl(C.CapState.permitted(C.CapCred.sets(c)))
845	    case True{}:
846	      h => cs.p.r2(C.CapSet.subset(e, p), c, e, p, i)(h)
847	
848	def cs.b.done(+c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.done(c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}:
849	  match c:
850	    case C.CapCred{r, eu, sv, nr, na, C.CapState{+op, +oi, +oe, +ob, +oa}}:
851	      {==}
852	
853	def cs.b.r4(+sp: Bool, +iok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r4(sp, iok, c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}:
854	  match sp iok:
855	    case True{} iok:
856	      cs.b.done(c, e, p, i)
857	    case False{} True{}:
858	      cs.b.done(c, e, p, i)
859	    case False{} False{}:
860	      {==}
861	
862	def cs.b.r3(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r3(ok, c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}:
863	  match ok:
864	    case False{}:
865	      {==}
866	    case True{}:
867	      cs.b.r4(C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.permitted(C.CapCred.sets(c)))), c, e, p, i)
868	
869	def cs.b.r2(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r2(ok, c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}:
870	  match ok:
871	    case False{}:
872	      {==}
873	    case True{}:
874	      cs.b.r3(C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.bounding(C.CapCred.sets(c)))), c, e, p, i)
875	
876	def cs.b.r1(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r1(ok, c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}:
877	  match ok:
878	    case False{}:
879	      {==}
880	    case True{}:
881	      cs.b.r2(C.CapSet.subset(e, p), c, e, p, i)
882	
883	def cs.v.done(+c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(e, p) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.done(c, e, p, i), c))) == True{} : Bool}:
884	  match c:
885	    case C.CapCred{r, eu, sv, nr, na, C.CapState{+op, +oi, +oe, +ob, +oa}}:
886	      h => bool.and3(C.CapSet.subset(e, p), C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(oa, p), i), p), C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(oa, p), i), i))(h)(set.amb_p(oa, p, i))(set.amb_i(oa, p, i))
887	
888	def cs.v.r4(+sp: Bool, +iok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(e, p) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r4(sp, iok, c, e, p, i), c))) == True{} : Bool}:
889	  match sp iok:
890	    case True{} iok:
891	      h => hv => cs.v.done(c, e, p, i)(h)
892	    case False{} True{}:
893	      h => hv => cs.v.done(c, e, p, i)(h)
894	    case False{} False{}:
895	      h => hv => hv
896	
897	def cs.v.r3(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(e, p) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r3(ok, c, e, p, i), c))) == True{} : Bool}:
898	  match ok:
899	    case False{}:
900	      h => hv => hv
901	    case True{}:
902	      h => hv => cs.v.r4(C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.permitted(C.CapCred.sets(c)))), c, e, p, i)(h)(hv)
903	
904	def cs.v.r2(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(e, p) == ok : Bool} -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r2(ok, c, e, p, i), c))) == True{} : Bool}:
905	  match ok:
906	    case False{}:
907	      h => hv => hv
908	    case True{}:
909	      h => hv => cs.v.r3(C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.bounding(C.CapCred.sets(c)))), c, e, p, i)(h)(hv)
910	
911	def cs.v.r1(+ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.capset.r1(ok, c, e, p, i), c))) == True{} : Bool}:
912	  match ok:
913	    case False{}:
914	      hv => hv
915	    case True{}:
916	      hv => cs.v.r2(C.CapSet.subset(e, p), c, e, p, i)({==})(hv)
917	
918	# prctl
919	def bd.sub(+v: Bool, +sp: Bool, +c: C.CapCred, +x: U32) -> {C.CapSet.subset(C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.bset_drop.go(v, sp, c, x), c))), C.CapState.bounding(C.CapCred.sets(c))) == True{} : Bool}:
920	  match v sp c:
921	    case False{} sp c:
922	      set.sub_refl(C.CapState.bounding(C.CapCred.sets(c)))
923	    case True{} False{} c:
924	      set.sub_refl(C.CapState.bounding(C.CapCred.sets(c)))
925	    case True{} True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
926	      set.sub_minus(b, C.CapSet.of(x))
927	
928	def bd.rest(+v: Bool, +sp: Bool, +c: C.CapCred, +x: U32) -> {C.CapState.with_bounding(C.CapCred.sets(C.Caps.or(A.CapAdjust.bset_drop.go(v, sp, c, x), c)), C.CapSet.empty()) == C.CapState.with_bounding(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}:
929	  match v sp c:
930	    case False{} sp c:
931	      {==}
932	    case True{} False{} c:
933	      {==}
934	    case True{} True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
935	      {==}
936	
937	def ar.valid(+v: Bool, +lk: Bool, +al: Bool, +c: C.CapCred, +x: U32) -> {A.CapAdjust.ambient.allowed(c, x) == al : Bool} -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.ambient_raise.go(v, lk, al, c, x), c))) == True{} : Bool}:
938	  match v lk al c:
939	    case False{} lk al c:
940	      h => hv => hv
941	    case True{} True{} al c:
942	      h => hv => hv
943	    case True{} False{} False{} c:
944	      h => hv => hv
945	    case True{} False{} True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
946	      +h => +hv => bool.and3(C.CapSet.subset(e, p), C.CapSet.subset(C.CapSet.union(a, C.CapSet.of(x)), p), C.CapSet.subset(C.CapSet.union(a, C.CapSet.of(x)), i))(valid.ep(C.CapState{p, i, e, b, a})(hv))(set.lub(a, C.CapSet.of(x), p)(valid.ap(C.CapState{p, i, e, b, a})(hv))(caps.has_of(C.Cap.valid(x), p, x)(bool.and_l(C.CapSet.has(p, x), C.CapSet.has(i, x))(h))))(set.lub(a, C.CapSet.of(x), i)(valid.ai(C.CapState{p, i, e, b, a})(hv))(caps.has_of(C.Cap.valid(x), i, x)(bool.and_r(C.CapSet.has(p, x), C.CapSet.has(i, x))(h))))
947	
948	def al.valid(+v: Bool, +c: C.CapCred, +x: U32) -> {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} -> {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.CapAdjust.ambient_lower.go(v, c, x), c))) == True{} : Bool}:
949	  match v c:
950	    case False{} c:
951	      hv => hv
952	    case True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
953	      +hv => bool.and3(C.CapSet.subset(e, p), C.CapSet.subset(C.CapSet.minus(a, C.CapSet.of(x)), p), C.CapSet.subset(C.CapSet.minus(a, C.CapSet.of(x)), i))(valid.ep(C.CapState{p, i, e, b, a})(hv))(set.minus_within(a, C.CapSet.of(x), p)(valid.ap(C.CapState{p, i, e, b, a})(hv)))(set.minus_within(a, C.CapSet.of(x), i)(valid.ai(C.CapState{p, i, e, b, a})(hv)))
954	
955	def ar.rest(+v: Bool, +lk: Bool, +al: Bool, +c: C.CapCred, +x: U32) -> {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.CapAdjust.ambient_raise.go(v, lk, al, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}:
956	  match v lk al c:
957	    case False{} lk al c:
958	      {==}
959	    case True{} True{} al c:
960	      {==}
961	    case True{} False{} False{} c:
962	      {==}
963	    case True{} False{} True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
964	      {==}
965	
966	def al.rest(+v: Bool, +c: C.CapCred, +x: U32) -> {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.CapAdjust.ambient_lower.go(v, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}:
967	  match v c:
968	    case False{} c:
969	      {==}
970	    case True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
971	      {==}
972	
973	# The laws
974	
975	def Laws.execve_result(k, c, f, ign):
976	  ex.result(E.CapExec.dumb_ok(E.CapExec.file_caps(k, f, ign), C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign))), c, E.CapExec.new_euid(c, f, ign), E.Caps.execve.sets(k, c, f, ign))
977	
978	def Laws.execve_effective_within_permitted(k, c, f, ign):
979	  ex.eff(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
980	
981	def Laws.execve_ambient_within_permitted(k, c, f, ign):
982	  ex.ap(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
983	
984	def Laws.execve_bounding_unchanged(k, c, f, ign):
985	  ex.bnd(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
986	
987	def Laws.execve_inheritable_unchanged(k, c, f, ign):
988	  ex.inh(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
989	
990	def Laws.execve_permitted_bounded(k, c, f, ign):
991	  ex.bound(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
992	
993	def Laws.execve_ambient_within_inheritable(k, c, f, ign, h):
994	  ex.ai(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))(h)
995	
996	def Laws.execve_permitted_bounded_valid(k, c, f, ign, h):
997	  ex.bound_v(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))(h)
998	
999	def Laws.execve_valid(k, c, f, ign, h):
1000	  valid.intro(E.Caps.execve.sets(k, c, f, ign))(ex.eff(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c)))(ex.ap(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c)))(ex.ai(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))(valid.ai(C.CapCred.sets(c))(h)))
1001	
1002	def Laws.execve_root_permitted(k, s, sv, na, u, sg, fc, ign, h):
1003	  match ign:
1004	    case True{}:
1005	      ex.root_p(E.CapExec.privileged(True{}, False{}, sg, E.CapExec.file_caps(k, C.CapFile{u, False{}, sg, fc}, True{})), s)(h)
1006	    case False{}:
1007	      ex.root_p(E.CapExec.privileged(False{}, False{}, sg, E.CapExec.file_caps(k, C.CapFile{u, False{}, sg, fc}, False{})), s)(h)
1008	
1009	def Laws.execve_root_effective(k, s, sv, na, u, sg, fc, ign, h):
1010	  match ign:
1011	    case True{}:
1012	      ex.root_e(E.CapExec.privileged(True{}, False{}, sg, E.CapExec.file_caps(k, C.CapFile{u, False{}, sg, fc}, True{})), s)(h)
1013	    case False{}:
1014	      ex.root_e(E.CapExec.privileged(False{}, False{}, sg, E.CapExec.file_caps(k, C.CapFile{u, False{}, sg, fc}, False{})), s)(h)
1015	
1016	def Laws.execve_nonroot_permitted(k, r, e, hr, he, s, sv, nr, na, u, ign):
1017	  match k ign:
1018	    case C.CapsKernel{l, True{}} True{}:
1019	      ex.nonroot_p(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1020	    case C.CapsKernel{l, True{}} False{}:
1021	      ex.nonroot_p(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1022	    case C.CapsKernel{l, False{}} True{}:
1023	      ex.nonroot_p(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1024	    case C.CapsKernel{l, False{}} False{}:
1025	      ex.nonroot_p(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1026	
1027	def Laws.execve_nonroot_effective(k, r, e, hr, he, s, sv, nr, na, u, ign):
1028	  match k ign:
1029	    case C.CapsKernel{l, True{}} True{}:
1030	      ex.nonroot_e(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1031	    case C.CapsKernel{l, True{}} False{}:
1032	      ex.nonroot_e(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1033	    case C.CapsKernel{l, False{}} True{}:
1034	      ex.nonroot_e(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1035	    case C.CapsKernel{l, False{}} False{}:
1036	      ex.nonroot_e(nr, U32.is_eq(r, 0), U32.is_eq(e, 0), s)(hr)(he)
1037	
1038	def Laws.capset_permitted_never_grows(c, e, p, i):
1039	  cs.p.r1(C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))), c, e, p, i)({==})
1040	
1041	def Laws.capset_bounding_unchanged(c, e, p, i):
1042	  cs.b.r1(C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))), c, e, p, i)
1043	
1044	def Laws.capset_valid(c, e, p, i, h):
1045	  cs.v.r1(C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))), c, e, p, i)(h)
1046	
1047	def Laws.bset_drop_never_grows(k, c, x):
1048	  bd.sub(C.CapsKernel.valid(k, x), C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), c, x)
1049	
1050	def Laws.bset_drop_rest_unchanged(k, c, x):
1051	  bd.rest(C.CapsKernel.valid(k, x), C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), c, x)
1052	
1053	def Laws.ambient_raise_valid(k, c, x, h):
1054	  ar.valid(C.CapsKernel.valid(k, x), C.CapCred.no_ambient_raise(c), A.CapAdjust.ambient.allowed(c, x), c, x)({==})(h)
1055	
1056	def Laws.ambient_raise_rest_unchanged(k, c, x):
1057	  ar.rest(C.CapsKernel.valid(k, x), C.CapCred.no_ambient_raise(c), A.CapAdjust.ambient.allowed(c, x), c, x)
1058	
1059	def Laws.ambient_lower_valid(k, c, x, h):
1060	  al.valid(C.CapsKernel.valid(k, x), c, x)(h)
1061	
1062	def Laws.ambient_lower_rest_unchanged(k, c, x):
1063	  al.rest(C.CapsKernel.valid(k, x), c, x)
1064	
1065	def Laws.ambient_clear_all_empty(c):
1066	  match c:
1067	    case C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
1068	      {==}
1069	
1070	def Laws.name_first():
1071	  {==}
1072	
1073	def Laws.name_last():
1074	  {==}
1075	
1076	def Laws.name_beyond():
1077	  {==}
1078	
1079	def Laws.of_name_sys_admin():
1080	  {==}
1081	
1082	def Laws.show_full():
1083	  {==}
1084	
1085	def Laws.show_two():
1086	  {==}
1087	
1088	def Laws.vector_dumb_binary():
1089	  {==}
1090	
1091	def Laws.vector_suid_root_with_caps():
1092	  {==}
1093	
1094	def Laws.vector_suid_root_plain():
1095	  {==}
1096	
1097	def Laws.vector_suid_ignored():
1098	  {==}
1099	
1100	def Laws.vector_capset_grows():
1101	  {==}
1102	
1103	def Laws.vector_ambient_not_inheritable():
1104	  {==}
1105	
1106	def Laws.vector_drop_invalid():
1107	  {==}
1108	
1109	def Laws.witness_valid():
1110	  {==}
1111	
1112	def Laws.witness_ambient_inheritable():
1113	  {==}
1114	
1115	def Laws.witness_ambient_inheritable_state():
1116	  {==}
1117	
1118	def Laws.witness_nonzero_uid():
1119	  {==}
1120	# END GENERATED: laws