def byte_mask_identity

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:118

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

118def byte_mask_identity(+value: U32,
119    below_256: {U32.is_lt(value, 256) == True{} : Bool}) ->
120    {Core.gcm_hex_mask(value, 255) == value : U32}:
121    match value:
122        case U32{bits}:
123            nat_below = Equal.trans(Bool,
124                Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
125                U32.is_lt(U32{bits}, 256),
126                True{},
127                Equal.sym(Bool,
128                    U32.is_lt(U32{bits}, 256),
129                    Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
130                    HubU32.is_lt_nat(U32{bits}, 256)),
131                below_256)
132            scaled_below = Equal.trans(Bool,
133                Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
134                Nat.is_lt(U32.to_nat(U32{bits}), 256n),
135                True{},
136                Equal.cong(Nat, Bool,
137                    bound => Nat.is_lt(U32.to_nat(U32{bits}), bound),
138                    U32.to_nat(256), 256n, {==}),
139                nat_below)
140            masked = HubU32.mask_word(U32{bits}, 255, 8n,
141                {==}, scaled_below)
142            Equal.trans(U32,
143                Core.gcm_hex_mask(U32{bits}, 255),
144                U32.and(255, U32{bits}),
145                U32{bits}, {==},
146                Equal.trans(U32,
147                    U32.and(255, U32{bits}),
148                    U32.and(U32{bits}, 255),
149                    U32{bits},
150                    Equal.cong(Word(32n), U32, w => U32{w},
151                        Word.and(32n, word_bits(255), bits),
152                        Word.and(32n, bits, word_bits(255)),
153                        word_and_comm(32n, word_bits(255), bits)),
154                    masked))