proofs/crypto/blake/blake2b/api.bend

bend-collections-laws-crypto@1.0.0.0 · 22 lines · 2 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as I
4
5law digest_size:
6  for h: T.Chain
7  {Pair.snd(Array<U32>,U32,Array.size(U32,I.digest(h))) == 16 : U32}
8
9def 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
13law 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
20def 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)