def fixed_hex_equal

qasim-bend-kit@0.1.0.2 · proof/AES_IdentityProof.bend:89

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

89def fixed_hex_equal(+n: Nat, +first: List<&2, U32>, +second: List<&2, U32>,
90    first_size: {List.length(&2, U32, first) == n : Nat},
91    second_size: {List.length(&2, U32, second) == n : Nat},
92    same: {AES.hex_bytes(AES.fixed_bytes(n, first)) == AES.hex_bytes(AES.fixed_bytes(n, second)) : String}) ->
93    {AES.hex_bytes(first) == AES.hex_bytes(second) : String}:
94    first_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
95        AES.fixed_bytes(n, first), first, Encoding.aes_fixed_bytes_identity(n, first, first_size))
96    second_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
97        AES.fixed_bytes(n, second), second, Encoding.aes_fixed_bytes_identity(n, second, second_size))
98    Equal.trans(String, AES.hex_bytes(first), AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(second),
99        Equal.sym(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(first), first_path),
100        Equal.trans(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(AES.fixed_bytes(n, second)),
101            AES.hex_bytes(second), same, second_path))