1	import Base
2	import ../../../src/crypto/sha/state.bend as State
3	import ../../../src/crypto/sha/sha256.bend as SHA
4	import ../../../spec/crypto/sha.bend as FIPS
5	import ./conformance.bend as Conformance
6	import ./laws.bend as Laws
7	
8	# This gate contains NO concrete-message test vectors.
9	def Laws.constants_correct():
10	  {==}
11	
12	def Laws.sha256_correct(bytes):
13	  Conformance.sha256_correct(bytes)
14	
15	law digest_octets_length:
16	  for s: State.State
17	  {List.length(&2, U32, FIPS.digest_octets(FIPS.digest(s))) == 32n : Nat}
18	
19	def digest_octets_length(s):
20	  match s:
21	    case State.H{a, b, c, d, e, f, g, h}:
22	      {==}
23	
24	def Laws.digest_bytes_correct(ws):
25	  match ws:
26	    case Nil{}:
27	      {==}
28	    case w <> tail:
29	      %Laws.digest_bytes_correct(tail) :
30	        {SHA.digest_bytes(w <> tail) == List.append(&2, U32, FIPS.word_octets(w), _) : List<&2, U32>}
31	      {==}
32	
33	def Laws.sha256_bytes_correct(bytes):
34	  %Laws.sha256_correct(bytes) :
35	    {SHA.sha256_bytes(bytes) == FIPS.digest_octets(_) : List<&2, U32>}
36	  Laws.digest_bytes_correct(SHA.sha256(bytes))
37	
38	def Laws.sha256_bytes_length(bytes):
39	  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(bytes), FIPS.sha256_bytes(bytes), Laws.sha256_bytes_correct(bytes)) :
40	    {List.length(&2, U32, _) == 32n : Nat}
41	  digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))