def pk_bits
import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOFimport Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/aml_pkglength.bend as K
54# the bits from the top down, so that they are matched in binder order
55def pk_bits(+b31: Bool, +b30: Bool, +b29: Bool, +b28: Bool, +b27: Bool, +b26: Bool, +b25: Bool, +b24: Bool, +b23: Bool, +b22: Bool, +b21: Bool, +b20: Bool, +b19: Bool, +b18: Bool, +b17: Bool, +b16: Bool, +b15: Bool, +b14: Bool, +b13: Bool, +b12: Bool, +b11: Bool, +b10: Bool, +b9: Bool, +b8: Bool, +b7: Bool, +b6: Bool, +b5: Bool, +b4: Bool, +b3: Bool, +b2: Bool, +b1: Bool, +b0: Bool, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})), r))) == Done{K.AmlPkgLen{U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
56 match b31:
57 case True{}:
58 pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{True{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
59 case False{}:
60 match b30:
61 case True{}:
62 pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
63 case False{}:
64 match b29:
65 case True{}:
66 pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
67 case False{}:
68 match b28:
69 case True{}:
70 pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
71 case False{}:
72 match b27:
73 case True{}:
74 {==}
75 case False{}:
76 match b26:
77 case True{}:
78 {==}
79 case False{}:
80 match b25:
81 case True{}:
82 {==}
83 case False{}:
84 match b24:
85 case True{}:
86 {==}
87 case False{}:
88 match b23:
89 case True{}:
90 {==}
91 case False{}:
92 match b22:
93 case True{}:
94 {==}
95 case False{}:
96 match b21:
97 case True{}:
98 {==}
99 case False{}:
100 match b20:
101 case True{}:
102 {==}
103 case False{}:
104 match b19:
105 case True{}:
106 {==}
107 case False{}:
108 match b18:
109 case True{}:
110 {==}
111 case False{}:
112 match b17:
113 case True{}:
114 {==}
115 case False{}:
116 match b16:
117 case True{}:
118 {==}
119 case False{}:
120 match b15:
121 case True{}:
122 {==}
123 case False{}:
124 match b14:
125 case True{}:
126 {==}
127 case False{}:
128 match b13:
129 case True{}:
130 {==}
131 case False{}:
132 match b12:
133 case True{}:
134 {==}
135 case False{}:
136 match b11:
137 case True{}:
138 {==}
139 case False{}:
140 match b10:
141 case True{}:
142 {==}
143 case False{}:
144 match b9:
145 case True{}:
146 {==}
147 case False{}:
148 match b8:
149 case True{}:
150 {==}
151 case False{}:
152 match b7:
153 case True{}:
154 {==}
155 case False{}:
156 match b6:
157 case True{}:
158 {==}
159 case False{}:
160 {==}