1	import Base
2	import ../../../src/crypto/sha512/types.bend as T
3	import ../../../src/crypto/sha512/sha512.bend as SHA
4	import ../../../spec/crypto/sha512.bend as FIPS
5	import ../../../spec/lib/common.bend as C
6	import ./words.bend as Words
7	
8	# SHA-512: the public API against the complete, independent FIPS 180-4
9	# specification spec/crypto/sha512.bend. No test vector, table or premise.
10	
11	# The digest of every byte list is the specification's.
12	law sha512_correct:
13	  for +bytes: List<&2, U32>
14	  {SHA.sha512(bytes) == FIPS.sha512_bytes(bytes) : List<&2, U32>}
15	
16	# Every digest is 64 bytes.
17	law sha512_length:
18	  for +bytes: List<&2, U32>
19	  {List.length(&2, U32, SHA.sha512(bytes)) == 64n : Nat}
20	
21	# The specification's word addition is addition modulo 2^64 (FIPS 180-4
22	# section 3.2), with W{hi, lo} read as lo + 2^32 hi.
23	law spec_add_mod:
24	  for +a: T.Lane
25	  for +b: T.Lane
26	  {Words.value(FIPS.add(a, b)) == C.low(64n, Nat.add(Words.value(a), Words.value(b))) : Nat}