AESMaskedXorProof.byte_mask_identity: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as AESMaskedXorProof
Lines 118-154 of qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&start_line=118&end_line=154

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as HubU32

def byte_mask_identity(+value: U32,
    below_256: {U32.is_lt(value, 256) == True{} : Bool}) ->
    {Core.gcm_hex_mask(value, 255) == value : U32}:
    match value:
        case U32{bits}:
            nat_below = Equal.trans(Bool,
                Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
                U32.is_lt(U32{bits}, 256),
                True{},
                Equal.sym(Bool,
                    U32.is_lt(U32{bits}, 256),
                    Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
                    HubU32.is_lt_nat(U32{bits}, 256)),
                below_256)
            scaled_below = Equal.trans(Bool,
                Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
                Nat.is_lt(U32.to_nat(U32{bits}), 256n),
                True{},
                Equal.cong(Nat, Bool,
                    bound => Nat.is_lt(U32.to_nat(U32{bits}), bound),
                    U32.to_nat(256), 256n, {==}),
                nat_below)
            masked = HubU32.mask_word(U32{bits}, 255, 8n,
                {==}, scaled_below)
            Equal.trans(U32,
                Core.gcm_hex_mask(U32{bits}, 255),
                U32.and(255, U32{bits}),
                U32{bits}, {==},
                Equal.trans(U32,
                    U32.and(255, U32{bits}),
                    U32.and(U32{bits}, 255),
                    U32{bits},
                    Equal.cong(Word(32n), U32, w => U32{w},
                        Word.and(32n, word_bits(255), bits),
                        Word.and(32n, bits, word_bits(255)),
                        word_and_comm(32n, word_bits(255), bits)),
                    masked))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=is_lt_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=mask_word
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=word_and_comm
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=word_bits