1	import Base
2	import ../../../../src/crypto/blake/blake2b/types.bend as T
3	import ../../../../src/crypto/blake/blake2b/blake2b.bend as I
4	
5	law digest_size:
6	  for h: T.Chain
7	  {Pair.snd(Array<U32>,U32,Array.size(U32,I.digest(h))) == 16 : U32}
8	
9	def digest_size(h):
10	  match h:
11	    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}}: {==}
12	
13	law capacity_gate:
14	  for a: Array<U32>
15	  for +n: Nat
16	  for +capacity: U32
17	  for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
18	  {I.sized(n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
19	
20	def capacity_gate(a,n,capacity,invalid):
21	  Equal.cong(Bool,Maybe<&1,Array<U32>>,b => I.checked(b,a,n),
22	    Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))),False{},invalid)