def aes_hex_mask_idempotent

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

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

76def aes_hex_mask_idempotent(+value: U32, mask: U32) ->
77    {AES.hex_mask(AES.hex_mask(value, mask), mask) ==
78     AES.hex_mask(value, mask) : U32}:
79    match value mask:
80        case U32{value_word} U32{mask_word}:
81            Equal.cong(Word(32n), U32,
82                word => U32{word},
83                AES.hex_word_and(32n, mask_word,
84                    AES.hex_word_and(32n, mask_word, value_word)),
85                AES.hex_word_and(32n, mask_word, value_word),
86                aes_hex_word_and_idempotent(32n, mask_word, value_word))