def pk.u8.c1
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
1037# the values 32 to 63
1038def pk.u8.c1(r: Nat) -> {Nat.is_le(32n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(32n+r))) == 32n+r : Nat}:
1039 match r:
1040 case 0n:
1041 h => {==}
1042 case 1n+r1:
1043 match r1:
1044 case 0n:
1045 h => {==}
1046 case 1n+r2:
1047 match r2:
1048 case 0n:
1049 h => {==}
1050 case 1n+r3:
1051 match r3:
1052 case 0n:
1053 h => {==}
1054 case 1n+r4:
1055 match r4:
1056 case 0n:
1057 h => {==}
1058 case 1n+r5:
1059 match r5:
1060 case 0n:
1061 h => {==}
1062 case 1n+r6:
1063 match r6:
1064 case 0n:
1065 h => {==}
1066 case 1n+r7:
1067 match r7:
1068 case 0n:
1069 h => {==}
1070 case 1n+r8:
1071 match r8:
1072 case 0n:
1073 h => {==}
1074 case 1n+r9:
1075 match r9:
1076 case 0n:
1077 h => {==}
1078 case 1n+r10:
1079 match r10:
1080 case 0n:
1081 h => {==}
1082 case 1n+r11:
1083 match r11:
1084 case 0n:
1085 h => {==}
1086 case 1n+r12:
1087 match r12:
1088 case 0n:
1089 h => {==}
1090 case 1n+r13:
1091 match r13:
1092 case 0n:
1093 h => {==}
1094 case 1n+r14:
1095 match r14:
1096 case 0n:
1097 h => {==}
1098 case 1n+r15:
1099 match r15:
1100 case 0n:
1101 h => {==}
1102 case 1n+r16:
1103 match r16:
1104 case 0n:
1105 h => {==}
1106 case 1n+r17:
1107 match r17:
1108 case 0n:
1109 h => {==}
1110 case 1n+r18:
1111 match r18:
1112 case 0n:
1113 h => {==}
1114 case 1n+r19:
1115 match r19:
1116 case 0n:
1117 h => {==}
1118 case 1n+r20:
1119 match r20:
1120 case 0n:
1121 h => {==}
1122 case 1n+r21:
1123 match r21:
1124 case 0n:
1125 h => {==}
1126 case 1n+r22:
1127 match r22:
1128 case 0n:
1129 h => {==}
1130 case 1n+r23:
1131 match r23:
1132 case 0n:
1133 h => {==}
1134 case 1n+r24:
1135 match r24:
1136 case 0n:
1137 h => {==}
1138 case 1n+r25:
1139 match r25:
1140 case 0n:
1141 h => {==}
1142 case 1n+r26:
1143 match r26:
1144 case 0n:
1145 h => {==}
1146 case 1n+r27:
1147 match r27:
1148 case 0n:
1149 h => {==}
1150 case 1n+r28:
1151 match r28:
1152 case 0n:
1153 h => {==}
1154 case 1n+r29:
1155 match r29:
1156 case 0n:
1157 h => {==}
1158 case 1n+r30:
1159 match r30:
1160 case 0n:
1161 h => {==}
1162 case 1n+r31:
1163 match r31:
1164 case 0n:
1165 h => {==}
1166 case 1n+r32:
1167 pk.u8.c2(r32)