def word_and_comm

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

import Base

95def word_and_comm(+n: Nat, +x: Word(n), +y: Word(n)) ->
96    {Word.and(n, x, y) == Word.and(n, y, x) : Word(n)}:
97    match n x y:
98        case 0n WNil{} WNil{}: {==}
99        case 1n+p WCon{xb, xt} WCon{yb, yt}:
100            head = bool_and_comm(xb, yb)
101            tail = word_and_comm(p, xt, yt)
102            Equal.trans(Word(1n+p),
103                Word.and(1n+p, WCon{xb, xt}, WCon{yb, yt}),
104                WCon{Bool.and(xb, yb), Word.and(p, xt, yt)},
105                Word.and(1n+p, WCon{yb, yt}, WCon{xb, xt}),
106                {==},
107                Equal.trans(Word(1n+p),
108                    WCon{Bool.and(xb, yb), Word.and(p, xt, yt)},
109                    WCon{Bool.and(yb, xb), Word.and(p, xt, yt)},
110                    WCon{Bool.and(yb, xb), Word.and(p, yt, xt)},
111                    Equal.cong(Bool, Word(1n+p),
112                        bit => WCon{bit, Word.and(p, xt, yt)},
113                        Bool.and(xb, yb), Bool.and(yb, xb), head),
114                    Equal.cong(Word(p), Word(1n+p),
115                        bits => WCon{Bool.and(yb, xb), bits},
116                        Word.and(p, xt, yt), Word.and(p, yt, xt), tail)))