proofs/crypto/blake/blake2b/api.bend source

proofs/crypto/blake/blake2b/api.bend on the hub · documented module

import Baseimport ../../../../src/crypto/blake/blake2b/types.bend as Timport ../../../../src/crypto/blake/blake2b/blake2b.bend as Ilaw digest_size:  for h: T.Chain  {Pair.snd(Array<U32>,U32,Array.size(U32,I.digest(h))) == 16 : U32}def digest_size(h):  match h:    case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}: {==}law capacity_gate:  for a: Array<U32>  for +n: Nat  for +capacity: U32  for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}  {I.sized(n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}def capacity_gate(a,n,capacity,invalid):  Equal.cong(Bool,Maybe<&1,Array<U32>>,b => I.checked(b,a,n),    Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))),False{},invalid)