1	import Base
2	import ../../../src/crypto/keccak/keccak.bend as K
3	import ../../../src/crypto/keccak/types.bend as T
4	
5	law rejected:
6	  for a: Array<U32>
7	  for n: Nat
8	  {K.checked(24n,False{},a,n) == None{} : Maybe<&1,Array<U32>>}
9	
10	def rejected(a,n):
11	  {==}
12	
13	law digest_size:
14	  for s: T.State
15	  {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(s))) == 8 : U32}
16	
17	def 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	
21	def 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	
25	law digest_word0:
26	  for +s: T.State
27	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),0)) == word0(s) : U32}
28	
29	def 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	
33	def 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	
37	law digest_word1:
38	  for +s: T.State
39	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),1)) == word1(s) : U32}
40	
41	def 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	
45	def 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	
49	law digest_word2:
50	  for +s: T.State
51	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),2)) == word2(s) : U32}
52	
53	def 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	
57	def 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	
61	law digest_word3:
62	  for +s: T.State
63	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),3)) == word3(s) : U32}
64	
65	def 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	
69	def 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	
73	law digest_word4:
74	  for +s: T.State
75	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),4)) == word4(s) : U32}
76	
77	def 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	
81	def 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	
85	law digest_word5:
86	  for +s: T.State
87	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),5)) == word5(s) : U32}
88	
89	def 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	
93	def 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	
97	law digest_word6:
98	  for +s: T.State
99	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),6)) == word6(s) : U32}
100	
101	def 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	
105	def 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	
109	law digest_word7:
110	  for +s: T.State
111	  {Pair.snd(Array<U32>,U32,Array.get(U32,K.digest(s),7)) == word7(s) : U32}
112	
113	def 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	
117	law 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	
124	def 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	
128	law suffix0:
129	  for w: U32
130	  {K.partial(w,0n) == 1 : U32}
131	
132	def suffix0(w): {==}
133	
134	law suffix1:
135	  for +w: U32
136	  {K.partial(w,1n) == U32.or(U32.and(w,255),256) : U32}
137	
138	def suffix1(w): {==}
139	
140	law suffix2:
141	  for +w: U32
142	  {K.partial(w,2n) == U32.or(U32.and(w,65535),65536) : U32}
143	
144	def suffix2(w): {==}
145	
146	law suffix3:
147	  for +w: U32
148	  {K.partial(w,3n) == U32.or(U32.and(w,16777215),16777216) : U32}
149	
150	def suffix3(w): {==}
151	
152	law whole_word:
153	  for +w: U32
154	  for n: Nat
155	  {K.partial(w,4n+n) == w : U32}
156	
157	def whole_word(w,n): {==}
158	
159	law empty_suffix:
160	  for w: U32
161	  {K.pad_word(w,0n,0n) == 1 : U32}
162	
163	def empty_suffix(w): {==}
164	
165	law empty_last_word:
166	  for w: U32
167	  {U32.or(K.pad_word(w,132n,0n),2147483648) == 2147483648 : U32}
168	
169	def empty_last_word(w): {==}
170	
171	law 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	
175	def combined_padding(w): {==}