def aes_hex_byte_prefix_idempotent

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

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

150def aes_hex_byte_prefix_idempotent(+byte: U32, +tail: String) ->
151    {SCon{AES.hex_digit(U32.shrn(AES.hex_mask(AES.hex_mask(byte, 255), 255), 4n)),
152       SCon{AES.hex_digit(AES.hex_mask(AES.hex_mask(byte, 255), 255)), tail}} ==
153     SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
154       SCon{AES.hex_digit(AES.hex_mask(byte, 255)), tail}} : String}:
155    +normalized = AES.hex_mask(byte, 255)
156    +twice = AES.hex_mask(normalized, 255)
157    +mask_equal = aes_hex_mask_idempotent(byte, 255)
158    low_equal = Equal.cong(U32, Char, value => AES.hex_digit(value),
159        twice, normalized,
160        mask_equal)
161    high_equal = Equal.cong(U32, Char,
162        value => AES.hex_digit(U32.shrn(value, 4n)), twice, normalized,
163        mask_equal)
164    inner_equal = Equal.cong(Char, String,
165        value => SCon{value, tail}, AES.hex_digit(twice),
166        AES.hex_digit(normalized), low_equal)
167    inner_path = Equal.cong(String, String,
168        rest => SCon{AES.hex_digit(U32.shrn(twice, 4n)), rest},
169        SCon{AES.hex_digit(twice), tail},
170        SCon{AES.hex_digit(normalized), tail}, inner_equal)
171    high_path = Equal.cong(Char, String,
172        value => SCon{value, SCon{AES.hex_digit(normalized), tail}},
173        AES.hex_digit(U32.shrn(twice, 4n)),
174        AES.hex_digit(U32.shrn(normalized, 4n)), high_equal)
175    Equal.trans(String,
176        SCon{AES.hex_digit(U32.shrn(twice, 4n)),
177            SCon{AES.hex_digit(twice), tail}},
178        SCon{AES.hex_digit(U32.shrn(twice, 4n)),
179            SCon{AES.hex_digit(normalized), tail}},
180        SCon{AES.hex_digit(U32.shrn(normalized, 4n)),
181            SCon{AES.hex_digit(normalized), tail}},
182        inner_path, high_path)