def aes_hex_pair_roundtrip

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:214

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

214def aes_hex_pair_roundtrip(+byte: U32) ->
215    {AES.hex_pair(
216        AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
217        AES.hex_digit(AES.hex_mask(byte, 255))) ==
218     Some{AES.hex_mask(byte, 255)} : Maybe<&2, U32>}:
219    +normalized = AES.hex_mask(byte, 255)
220    +high = U32.shrn(normalized, 4n)
221    +low = normalized
222    high_decoded = AES.hex_nibble(Char.to_u32(AES.hex_digit(high)))
223    low_decoded = AES.hex_nibble(Char.to_u32(AES.hex_digit(low)))
224    high_inverse = aes_hex_digit_inverse(high)
225    low_inverse = aes_hex_digit_inverse(low)
226    low_changed = Equal.cong(Maybe<&2, U32>, Maybe<&2, U32>,
227        nibble => AES.hex_pair.combine(high_decoded, nibble),
228        low_decoded, Some{AES.hex_mask(low, 15)}, low_inverse)
229    high_changed = Equal.cong(Maybe<&2, U32>, Maybe<&2, U32>,
230        nibble => AES.hex_pair.combine(nibble, Some{AES.hex_mask(low, 15)}),
231        high_decoded, Some{AES.hex_mask(high, 15)}, high_inverse)
232    pair_changed = Equal.trans(Maybe<&2, U32>,
233        AES.hex_pair.combine(high_decoded, low_decoded),
234        AES.hex_pair.combine(high_decoded, Some{AES.hex_mask(low, 15)}),
235        AES.hex_pair.combine(Some{AES.hex_mask(high, 15)}, Some{AES.hex_mask(low, 15)}),
236        low_changed, high_changed)
237    join_equal = aes_hex_join_masked_shift_mask(normalized)
238    normalized_equal = aes_hex_mask_idempotent(byte, 255)
239    joined_to_byte = Equal.trans(U32,
240        AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15)),
241        AES.hex_mask(normalized, 255), normalized,
242        join_equal, normalized_equal)
243    joined_some = Equal.cong(U32, Maybe<&2, U32>, value => Some{value},
244        AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15)),
245        normalized, joined_to_byte)
246    Equal.trans(Maybe<&2, U32>, AES.hex_pair(
247        AES.hex_digit(U32.shrn(normalized, 4n)), AES.hex_digit(normalized)),
248        AES.hex_pair.combine(high_decoded, low_decoded), Some{normalized},
249        {==},
250        Equal.trans(Maybe<&2, U32>,
251            AES.hex_pair.combine(high_decoded, low_decoded),
252            AES.hex_pair.combine(Some{AES.hex_mask(high, 15)},
253                Some{AES.hex_mask(low, 15)}),
254            Some{normalized}, pair_changed,
255            Equal.trans(Maybe<&2, U32>,
256                AES.hex_pair.combine(Some{AES.hex_mask(high, 15)},
257                    Some{AES.hex_mask(low, 15)}),
258                Some{AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15))},
259                Some{normalized}, {==}, joined_some)))