Gcm.inc_ok: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend as Gcm
Lines 55-60 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend&start_line=55&end_line=60

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
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_bits.bend as B

def inc_ok(+q0: T.Quad, +q1: T.Quad, +q2: T.Quad, +c: U32) -> {G.inc32(cb(q0, q1, q2, c)) == cb(q0, q1, q2, U32.inc(c)) : List<&2, U32>}:
  match q0 q1 q2:
    case T.W{a0, a1, a2, a3} T.W{a4, a5, a6, a7} T.W{a8, a9, a10, a11}:
      %Equal.sym(U32, G.int32(U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)), c, B.int32_ctr(c)) : {List.append(&2, U32, [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11], G.str32(U32.inc(_))) == cb(T.W{a0, a1, a2, a3}, T.W{a4, a5, a6, a7}, T.W{a8, a9, a10, a11}, U32.inc(c)) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.str32(U32.inc(c)), [U32.and(255, U32.shrn(U32.inc(c), 24n)), U32.and(255, U32.shrn(U32.inc(c), 16n)), U32.and(255, U32.shrn(U32.inc(c), 8n)), U32.and(255, U32.inc(c))], B.str32_ctr(U32.inc(c))) : {List.append(&2, U32, [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11], _) == cb(T.W{a0, a1, a2, a3}, T.W{a4, a5, a6, a7}, T.W{a8, a9, a10, a11}, U32.inc(c)) : List<&2, U32>}
      {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend&name=cb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=int32_ctr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&name=str32_ctr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=inc32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=int32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=str32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend&name=Quad