1	import Base
2	import ./types.bend as T
3	import ./core.bend as Core
4	
5	# SHA-512 (FIPS 180-4). Bytes are U32 values, each < 256; the digest is the
6	# 64 bytes of H0..H7, most significant first. Proved equal to the executable
7	# specification spec/crypto/sha512.bend for every input:
8	# proofs/crypto/sha512/laws.bend.
9	def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
10	  Core.sha512(bytes)
11	
12	def ascii(s: String) -> List<&2, U32>:
13	  match s:
14	    case SNil{}:
15	      Nil{}
16	    case SCon{Chr{c}, t}:
17	      c <> ascii(t)
18	
19	def hex_digit_if(x: U32, small: Bool) -> Char:
20	  match small:
21	    case True{}:
22	      Chr{(48 + x : U32)}
23	    case False{}:
24	      Chr{(87 + x : U32)}
25	
26	def hex_digit(+x: U32) -> Char:
27	  hex_digit_if(x, U32.is_lt(x, 10))
28	
29	# Lowercase hex of a byte list.
30	def hex(bytes: List<&2, U32>) -> String:
31	  match bytes:
32	    case Nil{}:
33	      ""
34	    case +b <> t:
35	      SCon{hex_digit(U32.and(U32.shrn(b, 4n), 15)), SCon{hex_digit(U32.and(b, 15)), hex(t)}}