def ghash_all_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash.bend:128

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D

128# GHASH_H(A || 0^v || C || 0^u || [len(A)]_64 || [len(C)]_64).
129def ghash_all_ok(+h: I.Block, +aad: List<&2, U32>, +c: List<&2, U32>) -> {G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), Word.zero(128n)) == D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))) : Word(128n)}:
130  Equal.trans(Word(128n),
131    G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), D.R(I.zero())),
132    G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
133    D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
134    ghash_ok(h, aad, List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), I.zero()),
135    Equal.trans(Word(128n),
136      G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
137      G.ghash(D.R(h), List.append(&2, U32, G.len64(aad), G.len64(c)), D.R(I.ghash(h, c, I.ghash(h, aad, I.zero())))),
138      D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
139      ghash_ok(h, c, List.append(&2, U32, G.len64(aad), G.len64(c)), I.ghash(h, aad, I.zero())),
140      ghash_ok(h, I.lengths(aad, c), Nil{}, I.ghash(h, c, I.ghash(h, aad, I.zero())))))