proofs/crypto/keccak/api.bend
bend-collections-laws-crypto@1.0.0.0 · 175 lines · 27 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/keccak.bend as K
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
4
5law rejected:
6 for a: Array<U32>
7 for n: Nat
8 {K.checked(24n,False{},a,n) == None{} : Maybe<&1,Array<U32>>}
9
10def rejected(a,n):
11 {==}
12
13law digest_size:
14 for s: T.State
15 {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(s))) == 8 : U32}
16
17def digest_size(s):
18 match s:
19 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
20
21def word0(s: T.State) -> U32:
22 match s:
23 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: a0
24
25law digest_word0:
26 for +s: T.State
27 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),0)) == word0(s) : U32}
28
29def digest_word0(s):
30 match s:
31 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
32
33def word1(s: T.State) -> U32:
34 match s:
35 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: b0
36
37law digest_word1:
38 for +s: T.State
39 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),1)) == word1(s) : U32}
40
41def digest_word1(s):
42 match s:
43 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
44
45def word2(s: T.State) -> U32:
46 match s:
47 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: a1
48
49law digest_word2:
50 for +s: T.State
51 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),2)) == word2(s) : U32}
52
53def digest_word2(s):
54 match s:
55 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
56
57def word3(s: T.State) -> U32:
58 match s:
59 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: b1
60
61law digest_word3:
62 for +s: T.State
63 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),3)) == word3(s) : U32}
64
65def digest_word3(s):
66 match s:
67 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
68
69def word4(s: T.State) -> U32:
70 match s:
71 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: a2
72
73law digest_word4:
74 for +s: T.State
75 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),4)) == word4(s) : U32}
76
77def digest_word4(s):
78 match s:
79 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
80
81def word5(s: T.State) -> U32:
82 match s:
83 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: b2
84
85law digest_word5:
86 for +s: T.State
87 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),5)) == word5(s) : U32}
88
89def digest_word5(s):
90 match s:
91 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
92
93def word6(s: T.State) -> U32:
94 match s:
95 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: a3
96
97law digest_word6:
98 for +s: T.State
99 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),6)) == word6(s) : U32}
100
101def digest_word6(s):
102 match s:
103 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
104
105def word7(s: T.State) -> U32:
106 match s:
107 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: b3
108
109law digest_word7:
110 for +s: T.State
111 {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),7)) == word7(s) : U32}
112
113def digest_word7(s):
114 match s:
115 case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}: {==}
116
117law capacity_gate:
118 for a: Array<U32>
119 for +n: Nat
120 for +capacity: U32
121 for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
122 {K.sized(24n,n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
123
124def capacity_gate(a,n,capacity,invalid):
125 Equal.cong(Bool,Maybe<&1,Array<U32>>,b => K.checked(24n,b,a,n),
126 Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))),False{},invalid)
127
128law suffix0:
129 for w: U32
130 {K.partial(w,0n) == 1 : U32}
131
132def suffix0(w): {==}
133
134law suffix1:
135 for +w: U32
136 {K.partial(w,1n) == U32.or(U32.and(w,255),256) : U32}
137
138def suffix1(w): {==}
139
140law suffix2:
141 for +w: U32
142 {K.partial(w,2n) == U32.or(U32.and(w,65535),65536) : U32}
143
144def suffix2(w): {==}
145
146law suffix3:
147 for +w: U32
148 {K.partial(w,3n) == U32.or(U32.and(w,16777215),16777216) : U32}
149
150def suffix3(w): {==}
151
152law whole_word:
153 for +w: U32
154 for n: Nat
155 {K.partial(w,4n+n) == w : U32}
156
157def whole_word(w,n): {==}
158
159law empty_suffix:
160 for w: U32
161 {K.pad_word(w,0n,0n) == 1 : U32}
162
163def empty_suffix(w): {==}
164
165law empty_last_word:
166 for w: U32
167 {U32.or(K.pad_word(w,132n,0n),2147483648) == 2147483648 : U32}
168
169def empty_last_word(w): {==}
170
171law combined_padding:
172 for +w: U32
173 {U32.or(K.pad_word(w,132n,135n),2147483648) == U32.or(U32.or(U32.and(w,16777215),16777216),2147483648) : U32}
174
175def combined_padding(w): {==}