1	# Generated by tools/generators/sha3_gen.py; do not edit by hand.
2	import Base
3	import ../../../src/crypto/keccak/types.bend as T
4	import ../../../src/crypto/keccak/permutation.bend as P
5	import ../../../src/crypto/sha3/core.bend as C
6	import ../../../spec/crypto/sha3.bend as F
7	import ../../../spec/crypto/keccak/permutation.bend as K
8	import ../keccak/permutation.bend as KP
9	
10	# src/crypto/sha3/core.bend refines spec/crypto/sha3.bend: the block XOR is
11	# equal after opening every lane, the permutation is the Keccak package's
12	# proved one (KP.rounds_correct, for every round count), and the absorbing,
13	# the parsing, the padding and the squeeze follow by induction or unfolding.
14	# The round count stays a variable until the end (24 is never unfolded).
15	
16	law inject_correct:
17	  for +s: T.State
18	  for +l0: T.Lane
19	  for +l1: T.Lane
20	  for +l2: T.Lane
21	  for +l3: T.Lane
22	  for +l4: T.Lane
23	  for +l5: T.Lane
24	  for +l6: T.Lane
25	  for +l7: T.Lane
26	  for +l8: T.Lane
27	  for +l9: T.Lane
28	  for +l10: T.Lane
29	  for +l11: T.Lane
30	  for +l12: T.Lane
31	  for +l13: T.Lane
32	  for +l14: T.Lane
33	  for +l15: T.Lane
34	  for +l16: T.Lane
35	  {C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) == F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16])) : T.State}
36	
37	def inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16):
38	  match s l0 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 l11 l12 l13 l14 l15 l16:
39	    case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}} T.W{u0, v0} T.W{u1, v1} T.W{u2, v2} T.W{u3, v3} T.W{u4, v4} T.W{u5, v5} T.W{u6, v6} T.W{u7, v7} T.W{u8, v8} T.W{u9, v9} T.W{u10, v10} T.W{u11, v11} T.W{u12, v12} T.W{u13, v13} T.W{u14, v14} T.W{u15, v15} T.W{u16, v16}:
40	      {==}
41	
42	law absorb_correct:
43	  for +ls: List<&2, T.Lane>
44	  for +rounds: Nat
45	  for +s: T.State
46	  {C.absorb(ls, rounds, s) == F.absorb(ls, rounds, s) : T.State}
47	
48	def absorb_correct(ls, rounds, s):
49	  match ls:
50	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest:
51	      +x = F.of_lanes(F.xor_lanes(F.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16]))
52	      %inject_correct(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) :
53	        {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, K.rounds(rounds, 0n, _)) : T.State}
54	      %KP.rounds_correct(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)) :
55	        {C.absorb(l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest, rounds, s) == F.absorb(rest, rounds, _) : T.State}
56	      absorb_correct(rest, rounds, P.rounds(rounds, 0n, C.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)))
57	    case Nil{}:
58	      {==}
59	    case l0 <> Nil{}:
60	      {==}
61	    case l0 <> l1 <> Nil{}:
62	      {==}
63	    case l0 <> l1 <> l2 <> Nil{}:
64	      {==}
65	    case l0 <> l1 <> l2 <> l3 <> Nil{}:
66	      {==}
67	    case l0 <> l1 <> l2 <> l3 <> l4 <> Nil{}:
68	      {==}
69	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> Nil{}:
70	      {==}
71	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> Nil{}:
72	      {==}
73	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> Nil{}:
74	      {==}
75	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> Nil{}:
76	      {==}
77	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> Nil{}:
78	      {==}
79	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> Nil{}:
80	      {==}
81	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> Nil{}:
82	      {==}
83	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> Nil{}:
84	      {==}
85	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> Nil{}:
86	      {==}
87	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> Nil{}:
88	      {==}
89	    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> Nil{}:
90	      {==}
91	
92	law lanes_correct:
93	  for +bytes: List<&2, U32>
94	  {C.lanes(bytes) == F.lanes(bytes) : List<&2, T.Lane>}
95	
96	def lanes_correct(bytes):
97	  match bytes:
98	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
99	      %lanes_correct(rest) :
100	        {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.le32(b0, b1, b2, b3), F.le32(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>}
101	      {==}
102	    case Nil{}:
103	      {==}
104	    case b0 <> Nil{}:
105	      {==}
106	    case b0 <> b1 <> Nil{}:
107	      {==}
108	    case b0 <> b1 <> b2 <> Nil{}:
109	      {==}
110	    case b0 <> b1 <> b2 <> b3 <> Nil{}:
111	      {==}
112	    case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}:
113	      {==}
114	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}:
115	      {==}
116	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}:
117	      {==}
118	
119	law tail_correct:
120	  for +q: Nat
121	  {C.tail(q) == F.padding_bytes(q) : List<&2, U32>}
122	
123	def tail_correct(q):
124	  match q:
125	    case 0n:
126	      {==}
127	    case 1n:
128	      {==}
129	    case 2n+k:
130	      {==}
131	
132	law suffix_correct:
133	  for +n: Nat
134	  {C.suffix(n) == F.padding(n) : List<&2, U32>}
135	
136	def suffix_correct(n):
137	  tail_correct(Nat.sub(136n, Nat.mod(n, 136n)))
138	
139	law digest_correct:
140	  for +s: T.State
141	  {C.digest_bytes(s) == F.squeeze(s) : List<&2, U32>}
142	
143	def digest_correct(s):
144	  match s:
145	    case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}:
146	      {==}
147	
148	law digest_length:
149	  for +s: T.State
150	  {List.length(&2, U32, C.digest_bytes(s)) == 32n : Nat}
151	
152	def digest_length(s):
153	  match s:
154	    case T.S{T.W{p0, q0}, T.W{p1, q1}, T.W{p2, q2}, T.W{p3, q3}, T.W{p4, q4}, T.W{p5, q5}, T.W{p6, q6}, T.W{p7, q7}, T.W{p8, q8}, T.W{p9, q9}, T.W{p10, q10}, T.W{p11, q11}, T.W{p12, q12}, T.W{p13, q13}, T.W{p14, q14}, T.W{p15, q15}, T.W{p16, q16}, T.W{p17, q17}, T.W{p18, q18}, T.W{p19, q19}, T.W{p20, q20}, T.W{p21, q21}, T.W{p22, q22}, T.W{p23, q23}, T.W{p24, q24}}:
155	      {==}
156	
157	law keccak_correct:
158	  for +bytes: List<&2, U32>
159	  for +rounds: Nat
160	  {C.keccak(bytes, rounds) == F.keccak(bytes, rounds) : List<&2, U32>}
161	
162	def keccak_correct(bytes, rounds):
163	  +n = List.length(&2, U32, bytes)
164	  %suffix_correct(n) :
165	    {C.keccak(bytes, rounds) == F.squeeze(F.absorb(F.lanes(List.append(&2, U32, bytes, _)), rounds, F.initial())) : List<&2, U32>}
166	  +padded = List.append(&2, U32, bytes, C.suffix(n))
167	  %lanes_correct(padded) :
168	    {C.keccak(bytes, rounds) == F.squeeze(F.absorb(_, rounds, F.initial())) : List<&2, U32>}
169	  %absorb_correct(C.lanes(padded), rounds, C.zero()) :
170	    {C.keccak(bytes, rounds) == F.squeeze(_) : List<&2, U32>}
171	  digest_correct(C.absorb(C.lanes(padded), rounds, C.zero()))