def absorb_ok

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

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/poly.bend as P
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/gf.bend as GF
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as B

62# (Y xor X) * H for one 16-byte block.
63def absorb_ok(+h: I.Block, +y: I.Block, +x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +x12: U32, +x13: U32, +x14: U32, +x15: U32) -> {D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) == G.mul(Word.xor(128n, D.R(y), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), D.R(h)) : Word(128n)}:
64  match y:
65    case I.B{y0, y1, y2, y3}:
66      %Equal.sym(Word(128n), G.mul(Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), D.R(h)), GF.sa(128n, G.low(), P.coefficients(128n, Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))), Word.zero(128n), D.R(h)), GF.mul_sa(128n, G.low(), Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), D.R(h))) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
67      %Equal.sym(List<&2, Bool>, P.coefficients(128n, Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))), G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), B.block_xor_ok(y0, y1, y2, y3, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == GF.sa(128n, G.low(), _, Word.zero(128n), D.R(h)) : Word(128n)}
68      %Equal.cong(List<&2, Bool>, Word(128n), l => D.F(I.Acc{I.zero(), h}, l), List.append(&2, Bool, G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), Nil{}), G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), append_nil(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])))) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
69      %Equal.sym(Word(128n), D.F(I.Acc{I.zero(), h}, List.append(&2, Bool, G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), Nil{})), D.F(D.steps(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), I.Acc{I.zero(), h}), Nil{}), steps_ok(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), I.Acc{I.zero(), h}, Nil{})) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
70      %Equal.sym(Word(128n), D.F(D.steps(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), I.Acc{I.zero(), h}), Nil{}), D.R(I.acc_z(D.steps(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), I.Acc{I.zero(), h}))), f_nil(D.steps(G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), I.Acc{I.zero(), h}))) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
71      %mul_bytes_steps(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}) : {D.R(I.acc_z(I.mul_bytes(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]), I.Acc{I.zero(), h}))) == D.R(I.acc_z(_)) : Word(128n)}
72      {==}