def aes_decode_hex_bytes
qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:261
import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
261def aes_decode_hex_bytes(+bytes: List<&2, U32>) ->
262 {AES.decode_hex(AES.hex_bytes(bytes)) == Some{aes_hex_mask_bytes(bytes)} : Maybe<&2, List<&2, U32>>}:
263 match bytes:
264 case Nil{}: {==}
265 case byte <> tail:
266 +normalized = AES.hex_mask(byte, 255)
267 +rest_pairs = AES.hex_pairs(String.to_list(AES.hex_bytes(tail)))
268 +rest_decoded = AES.collect_hex(rest_pairs)
269 tail_proof = aes_decode_hex_bytes(tail)
270 pair_proof = aes_hex_pair_roundtrip(byte)
271 pair_changed = Equal.cong(Maybe<&2, U32>,
272 Maybe<&2, List<&2, U32>>,
273 pair => AES.collect_hex.cons(pair, rest_decoded),
274 AES.hex_pair(
275 AES.hex_digit(U32.shrn(normalized, 4n)),
276 AES.hex_digit(normalized)),
277 Some{normalized}, pair_proof)
278 tail_changed = Equal.cong(Maybe<&2, List<&2, U32>>,
279 Maybe<&2, List<&2, U32>>,
280 result => AES.collect_hex.cons(Some{normalized}, result),
281 rest_decoded, Some{aes_hex_mask_bytes(tail)}, tail_proof)
282 Equal.trans(Maybe<&2, List<&2, U32>>,
283 AES.collect_hex.cons(
284 AES.hex_pair(
285 AES.hex_digit(U32.shrn(normalized, 4n)),
286 AES.hex_digit(normalized)), rest_decoded),
287 AES.collect_hex.cons(Some{normalized}, rest_decoded),
288 Some{normalized <> aes_hex_mask_bytes(tail)},
289 pair_changed,
290 Equal.trans(Maybe<&2, List<&2, U32>>,
291 AES.collect_hex.cons(Some{normalized}, rest_decoded),
292 Some{normalized <> aes_hex_mask_bytes(tail)},
293 Some{normalized <> aes_hex_mask_bytes(tail)},
294 tail_changed, {==}))