AESEnvelopeProof.aes_hex_word_and_equiv: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 25-50 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=25&end_line=50

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

def aes_hex_word_and_equiv(n: Nat, mask: Word(n), value: Word(n)) ->
    {AES.hex_word_and(n, mask, value) == Word.and(n, value, mask) : Word(n)}:
    match n mask value:
        case 0n WNil{} WNil{}: {==}
        case 1n+p WCon{False{}, mask_tail} WCon{value_bit, value_tail}:
            recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
            Equal.trans(Word(1n+p),
              WCon{False{}, AES.hex_word_and(p, mask_tail, value_tail)},
              WCon{False{}, Word.and(p, value_tail, mask_tail)},
              WCon{Bool.and(value_bit, False{}), Word.and(p, value_tail, mask_tail)},
              Equal.cong(Word(p), Word(1n+p), tail => WCon{False{}, tail},
                AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
              Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
                False{}, Bool.and(value_bit, False{}), Equal.sym(Bool,
                  Bool.and(value_bit, False{}), False{}, aes_bool_and_false(value_bit))))
        case 1n+p WCon{True{}, mask_tail} WCon{value_bit, value_tail}:
            recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
            Equal.trans(Word(1n+p),
              WCon{value_bit, AES.hex_word_and(p, mask_tail, value_tail)},
              WCon{value_bit, Word.and(p, value_tail, mask_tail)},
              WCon{Bool.and(value_bit, True{}), Word.and(p, value_tail, mask_tail)},
              Equal.cong(Word(p), Word(1n+p), tail => WCon{value_bit, tail},
                AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
              Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
                value_bit, Bool.and(value_bit, True{}), Equal.sym(Bool,
                  Bool.and(value_bit, True{}), value_bit, aes_bool_and_true(value_bit))))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_word_and
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_bool_and_false
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_bool_and_true