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