proofs/crypto/keccak/laws.bend
bend-collections-laws-crypto@1.0.0.0 · 40 lines · 6 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as S
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/keccak.bend as K
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as Sponge
7
8
9law permutation_rounds:
10 for +n: Nat
11 for +i: Nat
12 for +s: T.State
13 {P.rounds(n,i,s) == S.rounds(n,i,s) : T.State}
14
15law digest_size:
16 for s: T.State
17 {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(s))) == 8 : U32}
18
19law capacity_rejection:
20 for a: Array<U32>
21 for +n: Nat
22 for +capacity: U32
23 for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
24 {K.sized(24n,n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
25
26law packed_sponge_correct:
27 for +r: Nat
28 for a: Array<U32>
29 for +length: Nat
30 {K.keccak256_rounds(r,a,length) == Sponge.keccak256_rounds(r,a,length) : Maybe<&1,Array<U32>>}
31
32law ethereum_round_count:
33 for a: Array<U32>
34 for +length: Nat
35 {K.keccak256(a,length) == K.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}
36
37law ethereum_keccak256:
38 for a: Array<U32>
39 for +length: Nat
40 {K.keccak256(a,length) == Sponge.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}