PROOF.bend

bend-osdev-caps@0.1.0.0 · 1,120 lines · 86 definitions

1import Base
2import bend-osdev-caps@0.1.0.0/caps.bend as C
3import bend-osdev-caps@0.1.0.0/exec.bend as E
4import bend-osdev-caps@0.1.0.0/adjust.bend as A
5import bend-osdev-caps@0.1.0.0/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
21def bits.disc(b: Bool) -> Type:
22  match b:
23    case False{}:
24      Unit
25    case True{}:
26      Empty
27
28def bits.disc2(b: Bool) -> Type:
29  match b:
30    case False{}:
31      Empty
32    case True{}:
33      Unit
34
35def bits.ft(+e: {False{} == True{} : Bool}) -> bits.disc(True{}):
36  %e : bits.disc(_)
37  Unit{}
38
39def bits.tf(+e: {True{} == False{} : Bool}) -> bits.disc2(False{}):
40  %e : bits.disc2(_)
41  Unit{}
42
43def bits.absurd(-x: Bool, +e: {False{} == True{} : Bool}) -> {x == True{} : Bool}:
44  Empty.absurd({x == True{} : Bool}, bits.ft(e))
45
46def 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
49def 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
54def 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
61def 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
68def 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
81def 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
86def 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
91def 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
96def 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
101def 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
112def 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
121def 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
130def 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
144def 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
149def 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
154def 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
158def 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
166def 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
177def 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
188def 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
203def 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
218def 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
289def 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
360def 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
431def 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
470def 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
493def 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
516def 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
539def 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
562def 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
587def 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
604def 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
632def 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
637def 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
642def 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
647def 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
652def 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
657def 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
662def 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
667def 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
672def 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
677def 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
682def 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
687def 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
692def 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
697def 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
702def 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)
710def 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
720def 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
731def 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
738def 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
745def 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
750def 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
755def 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
762def 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
769def 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
776def 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
783def 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
794def 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
805def 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
813def 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
818def 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
827def 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
834def 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
841def 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
848def 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
853def 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
862def 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
869def 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
876def 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
883def 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
888def 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
897def 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
904def 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
911def 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
919def 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
928def 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
937def 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
948def 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
955def 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
966def 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
975def 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
978def Laws.execve_effective_within_permitted(k, c, f, ign):
979  ex.eff(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
980
981def Laws.execve_ambient_within_permitted(k, c, f, ign):
982  ex.ap(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
983
984def Laws.execve_bounding_unchanged(k, c, f, ign):
985  ex.bnd(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
986
987def Laws.execve_inheritable_unchanged(k, c, f, ign):
988  ex.inh(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
989
990def Laws.execve_permitted_bounded(k, c, f, ign):
991  ex.bound(E.CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
992
993def 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
996def 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
999def 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
1002def 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
1009def 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
1016def 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
1027def 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
1038def 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
1041def 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
1044def 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
1047def 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
1050def 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
1053def 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
1056def 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
1059def Laws.ambient_lower_valid(k, c, x, h):
1060  al.valid(C.CapsKernel.valid(k, x), c, x)(h)
1061
1062def Laws.ambient_lower_rest_unchanged(k, c, x):
1063  al.rest(C.CapsKernel.valid(k, x), c, x)
1064
1065def 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
1070def Laws.name_first():
1071  {==}
1072
1073def Laws.name_last():
1074  {==}
1075
1076def Laws.name_beyond():
1077  {==}
1078
1079def Laws.of_name_sys_admin():
1080  {==}
1081
1082def Laws.show_full():
1083  {==}
1084
1085def Laws.show_two():
1086  {==}
1087
1088def Laws.vector_dumb_binary():
1089  {==}
1090
1091def Laws.vector_suid_root_with_caps():
1092  {==}
1093
1094def Laws.vector_suid_root_plain():
1095  {==}
1096
1097def Laws.vector_suid_ignored():
1098  {==}
1099
1100def Laws.vector_capset_grows():
1101  {==}
1102
1103def Laws.vector_ambient_not_inheritable():
1104  {==}
1105
1106def Laws.vector_drop_invalid():
1107  {==}
1108
1109def Laws.witness_valid():
1110  {==}
1111
1112def Laws.witness_ambient_inheritable():
1113  {==}
1114
1115def Laws.witness_ambient_inheritable_state():
1116  {==}
1117
1118def Laws.witness_nonzero_uid():
1119  {==}
1120# END GENERATED: laws