1	import Base
2	import ../../../src/crypto/hash.bend as Hash
3	import ../../../spec/crypto/sha.bend as FIPS180
4	import ../../../spec/crypto/sha512.bend as FIPS180_512
5	import ../../../spec/crypto/sha3.bend as FIPS202
6	
7	# The clauses of src/crypto/hash.bend. Proved in proof.bend for every input.
8	
9	# Each one-shot function is its standard's executable specification.
10	law Sha256.value:
11	  for +bytes: List<&2, U32>
12	  {Hash.sha256(bytes) == FIPS180.sha256_bytes(bytes) : List<&2, U32>}
13	
14	law Sha512.value:
15	  for +bytes: List<&2, U32>
16	  {Hash.sha512(bytes) == FIPS180_512.sha512_bytes(bytes) : List<&2, U32>}
17	
18	law Sha3_256.value:
19	  for +bytes: List<&2, U32>
20	  {Hash.sha3_256(bytes) == FIPS202.sha3_256(bytes) : List<&2, U32>}
21	
22	# Digest sizes: 32, 64 and 32 bytes.
23	law Sha256.length:
24	  for +bytes: List<&2, U32>
25	  {List.length(&2, U32, Hash.sha256(bytes)) == 32n : Nat}
26	
27	law Sha512.length:
28	  for +bytes: List<&2, U32>
29	  {List.length(&2, U32, Hash.sha512(bytes)) == 64n : Nat}
30	
31	law Sha3_256.length:
32	  for +bytes: List<&2, U32>
33	  {List.length(&2, U32, Hash.sha3_256(bytes)) == 32n : Nat}
34	
35	# Incremental hashing equals one-shot hashing for every split of the input:
36	# the chunks, in order, digest to the hash of their concatenation.
37	law Incremental.sha256:
38	  for +chunks: List<&2, List<&2, U32>>
39	  {Hash.digest(Hash.update_all(Hash.new_sha256(), chunks)) == Hash.sha256(List.concat(&2, U32, chunks)) : List<&2, U32>}
40	
41	law Incremental.sha512:
42	  for +chunks: List<&2, List<&2, U32>>
43	  {Hash.digest(Hash.update_all(Hash.new_sha512(), chunks)) == Hash.sha512(List.concat(&2, U32, chunks)) : List<&2, U32>}
44	
45	law Incremental.sha3_256:
46	  for +chunks: List<&2, List<&2, U32>>
47	  {Hash.digest(Hash.update_all(Hash.new_sha3_256(), chunks)) == Hash.sha3_256(List.concat(&2, U32, chunks)) : List<&2, U32>}
48	
49	# The two-chunk case, spelled with update.
50	law Split.sha256:
51	  for +a: List<&2, U32>
52	  for +b: List<&2, U32>
53	  {Hash.digest(Hash.update(Hash.update(Hash.new_sha256(), a), b)) == Hash.sha256(List.append(&2, U32, a, b)) : List<&2, U32>}
54	
55	law Split.sha512:
56	  for +a: List<&2, U32>
57	  for +b: List<&2, U32>
58	  {Hash.digest(Hash.update(Hash.update(Hash.new_sha512(), a), b)) == Hash.sha512(List.append(&2, U32, a, b)) : List<&2, U32>}
59	
60	law Split.sha3_256:
61	  for +a: List<&2, U32>
62	  for +b: List<&2, U32>
63	  {Hash.digest(Hash.update(Hash.update(Hash.new_sha3_256(), a), b)) == Hash.sha3_256(List.append(&2, U32, a, b)) : List<&2, U32>}