def top_xor

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:155

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P

155def top_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {P.top(n, Word.xor(n, a, b)) == Bool.xor(P.top(n, a), P.top(n, b)) : Bool}:
156  match n a b:
157    case 0n WNil{} WNil{}:
158      {==}
159    case 1n WCon{x, s} WCon{y, t}:
160      {==}
161    case 2n+p WCon{x, s} WCon{y, t}:
162      top_xor(1n+p, s, t)