Compress.model: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend as Compress
Lines 103-104 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend&start_line=103&end_line=104

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

def model(+r: Nat, +h: T.State,+m0: U32,+m1: U32,+m2: U32,+m3: U32,+m4: U32,+m5: U32,+m6: U32,+m7: U32,+m8: U32,+m9: U32,+m10: U32,+m11: U32,+m12: U32,+m13: U32,+m14: U32,+m15: U32,t0: U32,t1: U32,last: Bool) -> T.State:
  C.finish(h,rounds(r,0n,C.init(h,t0,t1,last),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/compress.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/compress.bend&name=init
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend&name=State