1	import Base
2	import ../../../src/crypto/sha/state.bend as S256
3	import ../../../src/crypto/sha/core.bend as C256
4	import ../../../src/crypto/sha/sha256.bend as SHA256
5	import ../../../src/crypto/sha512/core.bend as C512
6	import ../../../src/crypto/sha3/core.bend as C3
7	import ../../../src/crypto/hash.bend as Hash
8	import ../sha/conformance.bend as SC
9	import ../sha/laws.bend as SL
10	import ../sha/correctness.bend as SCorr
11	import ../sha512/conformance.bend as S512
12	import ../sha3/conformance.bend as S3
13	import ./lists.bend as L
14	import ./incremental.bend as I
15	import ./laws.bend as Laws
16	
17	# Gate for src/crypto/hash.bend: `bend proofs/crypto/hash/proof.bend` prints
18	# ALL PROOFS CHECK when every clause of laws.bend holds.
19	
20	def Laws.Sha256.value(bytes):
21	  SL.sha256_bytes_correct(bytes)
22	
23	def Laws.Sha512.value(bytes):
24	  S512.sha512_correct(bytes)
25	
26	def Laws.Sha3_256.value(bytes):
27	  S3.keccak_correct(bytes, 24n)
28	
29	def Laws.Sha256.length(bytes):
30	  SL.sha256_bytes_length(bytes)
31	
32	def Laws.Sha512.length(bytes):
33	  S512.digest_length(C512.blocks(C512.lanes(List.append(&2, U32, bytes,
34	    C512.suffix(List.length(&2, U32, bytes)))), 64n, C512.round_constants(), C512.initial()))
35	
36	def Laws.Sha3_256.length(bytes):
37	  S3.digest_length(C3.absorb(C3.lanes(List.append(&2, U32, bytes,
38	    C3.suffix(List.length(&2, U32, bytes)))), 24n, C3.zero()))
39	
40	# The one-shot SHA-256 is its block loop over the padded message (the SHA-256
41	# package's stream_correct, with nothing hashed before).
42	law oneshot256:
43	  for +m: List<&2, U32>
44	  {Hash.sha256(m) == SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
45	    C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))) : List<&2, U32>}
46	
47	def oneshot256(m):
48	  %L.add_zero(List.length(&2, U32, m)) :
49	    {Hash.sha256(m) == SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
50	      C256.suffix(_)), 48n, C256.round_constants(), C256.initial()))) : List<&2, U32>}
51	  Equal.cong(S256.State, List<&2, U32>, t => SHA256.digest_bytes(C256.digest(t)),
52	    C256.stream(m, 0n, 48n, C256.initial()),
53	    C256.block_bytes(List.append(&2, U32, m, C256.suffix(Nat.add(List.length(&2, U32, m), 0n))),
54	      48n, C256.round_constants(), C256.initial()),
55	    SC.stream_correct(m, 0n, 48n, C256.initial()))
56	
57	def Laws.Incremental.sha256(chunks):
58	  +m = List.concat(&2, U32, chunks)
59	  Equal.trans(List<&2, U32>,
60	    Hash.digest(Hash.update_all(Hash.new_sha256(), chunks)),
61	    SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
62	      C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))),
63	    Hash.sha256(m),
64	    I.incremental256(chunks),
65	    Equal.sym(List<&2, U32>, Hash.sha256(m), SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, m,
66	      C256.suffix(List.length(&2, U32, m))), 48n, C256.round_constants(), C256.initial()))), oneshot256(m)))
67	
68	def Laws.Incremental.sha512(chunks):
69	  I.incremental512(chunks)
70	
71	def Laws.Incremental.sha3_256(chunks):
72	  I.incremental3(chunks)
73	
74	def Laws.Split.sha256(a, b):
75	  %L.append_nil(b) :
76	    {Hash.digest(Hash.update(Hash.update(Hash.new_sha256(), a), b)) == Hash.sha256(List.append(&2, U32, a, _)) : List<&2, U32>}
77	  Laws.Incremental.sha256([a, b])
78	
79	def Laws.Split.sha512(a, b):
80	  %L.append_nil(b) :
81	    {Hash.digest(Hash.update(Hash.update(Hash.new_sha512(), a), b)) == Hash.sha512(List.append(&2, U32, a, _)) : List<&2, U32>}
82	  Laws.Incremental.sha512([a, b])
83	
84	def Laws.Split.sha3_256(a, b):
85	  %L.append_nil(b) :
86	    {Hash.digest(Hash.update(Hash.update(Hash.new_sha3_256(), a), b)) == Hash.sha3_256(List.append(&2, U32, a, _)) : List<&2, U32>}
87	  Laws.Incremental.sha3_256([a, b])