Ghash.step_ok: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend as Ghash
Lines 17-21 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend&start_line=17&end_line=21

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

# One bit of Algorithm 1: Z += c*V, V = V*x.
def step_ok(+c: Bool, +z: I.Block, +v: I.Block, +rest: List<&2, Bool>) -> {D.F(I.Acc{z, v}, c <> rest) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}:
  %B.zstep_ok(c, z, v) : {GF.sa(128n, G.low(), rest, _, P.times_x(128n, G.low(), D.R(v))) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
  %B.mulx_ok(v) : {GF.sa(128n, G.low(), rest, D.R(I.add_masked(D.bit(c), z, v)), _) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
  {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend&name=sa
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=mulx_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=zstep_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=F
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&name=times_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=Acc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=add_masked
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=step