1	import Base
2	import ../../../../src/crypto/sha/packed/sha256.bend as Runtime
3	import ../../../../src/crypto/sha/packed/buffer.bend as Buffer
4	import ./legacy_model.bend as SHA
5	import ../../../../spec/crypto/sha.bend as FIPS
6	import ../../../../spec/crypto/sha/packed.bend as PackedSpec
7	
8	# These claims mention the actual public API and the complete independent spec.
9	# There are no arbitrary preprocessing functions, tables, or correctness premises.
10	law constants_correct:
11	  {SHA.constants() == FIPS.constants() : List<&2, U32>}
12	
13	law sha256_correct:
14	  for +bytes: List<&2, U32>
15	  {SHA.sha256(bytes) == FIPS.sha256(bytes) : List<&2, U32>}
16	
17	law digest_bytes_correct:
18	  for +ws: List<&2, U32>
19	  {SHA.digest_bytes(ws) == FIPS.digest_octets(ws) : List<&2, U32>}
20	
21	law sha256_bytes_correct:
22	  for +bytes: List<&2, U32>
23	  {SHA.sha256_bytes(bytes) == FIPS.sha256_bytes(bytes) : List<&2, U32>}
24	
25	law sha256_bytes_length:
26	  for +bytes: List<&2, U32>
27	  {List.length(&2, U32, SHA.sha256_bytes(bytes)) == 32n : Nat}
28	
29	# A separate packed-format contract; the original list-to-FIPS theorem is unchanged.
30	law sha256_packed_correct:
31	  for words: Array<U32>
32	  for +byte_length: Nat
33	  {SHA.sha256_packed(words,byte_length) == PackedSpec.sha256(words,byte_length) : Maybe<&2,List<&2,U32>>}
34	
35	# Actual production array API; historical list laws above concern only its model.
36	law sha256_array_correct:
37	  for words: Array<U32>
38	  for +byte_length: Nat
39	  {Runtime.sha256(words,byte_length) == Buffer.result(PackedSpec.hash(words,byte_length)) : Maybe<&1,Array<U32>>}