def pk.u8
import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
1169# the values 0 to 31
1170def pk.u8(r: Nat) -> {Nat.is_le(r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(r))) == r : Nat}:
1171 match r:
1172 case 0n:
1173 h => {==}
1174 case 1n+r1:
1175 match r1:
1176 case 0n:
1177 h => {==}
1178 case 1n+r2:
1179 match r2:
1180 case 0n:
1181 h => {==}
1182 case 1n+r3:
1183 match r3:
1184 case 0n:
1185 h => {==}
1186 case 1n+r4:
1187 match r4:
1188 case 0n:
1189 h => {==}
1190 case 1n+r5:
1191 match r5:
1192 case 0n:
1193 h => {==}
1194 case 1n+r6:
1195 match r6:
1196 case 0n:
1197 h => {==}
1198 case 1n+r7:
1199 match r7:
1200 case 0n:
1201 h => {==}
1202 case 1n+r8:
1203 match r8:
1204 case 0n:
1205 h => {==}
1206 case 1n+r9:
1207 match r9:
1208 case 0n:
1209 h => {==}
1210 case 1n+r10:
1211 match r10:
1212 case 0n:
1213 h => {==}
1214 case 1n+r11:
1215 match r11:
1216 case 0n:
1217 h => {==}
1218 case 1n+r12:
1219 match r12:
1220 case 0n:
1221 h => {==}
1222 case 1n+r13:
1223 match r13:
1224 case 0n:
1225 h => {==}
1226 case 1n+r14:
1227 match r14:
1228 case 0n:
1229 h => {==}
1230 case 1n+r15:
1231 match r15:
1232 case 0n:
1233 h => {==}
1234 case 1n+r16:
1235 match r16:
1236 case 0n:
1237 h => {==}
1238 case 1n+r17:
1239 match r17:
1240 case 0n:
1241 h => {==}
1242 case 1n+r18:
1243 match r18:
1244 case 0n:
1245 h => {==}
1246 case 1n+r19:
1247 match r19:
1248 case 0n:
1249 h => {==}
1250 case 1n+r20:
1251 match r20:
1252 case 0n:
1253 h => {==}
1254 case 1n+r21:
1255 match r21:
1256 case 0n:
1257 h => {==}
1258 case 1n+r22:
1259 match r22:
1260 case 0n:
1261 h => {==}
1262 case 1n+r23:
1263 match r23:
1264 case 0n:
1265 h => {==}
1266 case 1n+r24:
1267 match r24:
1268 case 0n:
1269 h => {==}
1270 case 1n+r25:
1271 match r25:
1272 case 0n:
1273 h => {==}
1274 case 1n+r26:
1275 match r26:
1276 case 0n:
1277 h => {==}
1278 case 1n+r27:
1279 match r27:
1280 case 0n:
1281 h => {==}
1282 case 1n+r28:
1283 match r28:
1284 case 0n:
1285 h => {==}
1286 case 1n+r29:
1287 match r29:
1288 case 0n:
1289 h => {==}
1290 case 1n+r30:
1291 match r30:
1292 case 0n:
1293 h => {==}
1294 case 1n+r31:
1295 match r31:
1296 case 0n:
1297 h => {==}
1298 case 1n+r32:
1299 pk.u8.c1(r32)