def aes_hex_word_and_equiv

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

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

25def aes_hex_word_and_equiv(n: Nat, mask: Word(n), value: Word(n)) ->
26    {AES.hex_word_and(n, mask, value) == Word.and(n, value, mask) : Word(n)}:
27    match n mask value:
28        case 0n WNil{} WNil{}: {==}
29        case 1n+p WCon{False{}, mask_tail} WCon{value_bit, value_tail}:
30            recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
31            Equal.trans(Word(1n+p),
32              WCon{False{}, AES.hex_word_and(p, mask_tail, value_tail)},
33              WCon{False{}, Word.and(p, value_tail, mask_tail)},
34              WCon{Bool.and(value_bit, False{}), Word.and(p, value_tail, mask_tail)},
35              Equal.cong(Word(p), Word(1n+p), tail => WCon{False{}, tail},
36                AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
37              Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
38                False{}, Bool.and(value_bit, False{}), Equal.sym(Bool,
39                  Bool.and(value_bit, False{}), False{}, aes_bool_and_false(value_bit))))
40        case 1n+p WCon{True{}, mask_tail} WCon{value_bit, value_tail}:
41            recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
42            Equal.trans(Word(1n+p),
43              WCon{value_bit, AES.hex_word_and(p, mask_tail, value_tail)},
44              WCon{value_bit, Word.and(p, value_tail, mask_tail)},
45              WCon{Bool.and(value_bit, True{}), Word.and(p, value_tail, mask_tail)},
46              Equal.cong(Word(p), Word(1n+p), tail => WCon{value_bit, tail},
47                AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
48              Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
49                value_bit, Bool.and(value_bit, True{}), Equal.sym(Bool,
50                  Bool.and(value_bit, True{}), value_bit, aes_bool_and_true(value_bit))))