Blake2b.advance: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as Blake2b
Lines 196-205 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend&start_line=196&end_line=205

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T

# t := t + x on the 128-bit counter, carrying from limb to limb.
def advance(c: T.Counter, +x: U32) -> T.Counter:
  match c:
    case T.C{c0,c1,c2,c3}:
      +s0 = U32.add(c0,x)
      +k0 = Bool.to_u32(U32.is_lt(s0,x))
      +s1 = U32.add(c1,k0)
      +k1 = Bool.to_u32(U32.is_lt(s1,k0))
      +s2 = U32.add(c2,k1)
      T.C{s0,s1,s2,U32.add(c3,Bool.to_u32(U32.is_lt(s2,k1)))}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.to_u32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Counter