1	# share/sha: the sha256 a package hash is built from. The digest itself comes from
2	# noah-emp/bend-sha256, which proves its output equal to an executable FIPS
3	# 180-4 specification; this file is only the string-in, hex-out shape ez uses.
4	# The dependency hashes packed big-endian words and returns eight of them, or
5	# nothing when the declared length does not fit the array.
6	import Base
7	import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as S
8	
9	# four big-endian bytes in one word, each kept to eight bits
10	def pack(first: U32, second: U32, third: U32, fourth: U32) -> U32:
11	  (U32.shln((first .&. 255 : U32), 24n)
12	    .|. U32.shln((second .&. 255 : U32), 16n)
13	    .|. U32.shln((third .&. 255 : U32), 8n) .|. (fourth .&. 255) : U32)
14	
15	# one character as the byte it contributes
16	def byte(ch: Char) -> U32:
17	  Char.to_u32(ch)
18	
19	# how many words hold this many bytes
20	def words.of(len: Nat) -> Nat:
21	  Nat.div(Nat.add(len, 3n), 4n)
22	
23	# one more bit of depth when the capacity does not yet hold the words. The
24	# rest is a thunk, so the stop does not build the next depth.
25	def depth.step(more: Bool, acc: Nat, rest: Unit -> Nat) -> Nat:
26	  match more:
27	    case False{}:
28	      acc
29	    case True{}:
30	      rest(Unit{})
31	
32	# the depth of an array whose capacity, 2^depth, is at least `words`
33	def depth.go(bits: Nat, +words: Nat, +cap: Nat, +acc: Nat) -> Nat:
34	  match bits:
35	    case 0n:
36	      acc
37	    case 1n+p:
38	      depth.step(Nat.is_lt(cap, words), acc,
39	        _u => depth.go(p, words, Nat.mul(cap, 2n), Nat.add(acc, 1n)))
40	
41	# the depth of the array that holds this many words, at most 32
42	def depth(words: Nat) -> Nat:
43	  depth.go(32n, words, 1n, 0n)
44	
45	# the string packed into the array, four bytes to a word. A short tail packs
46	# zeros in the unused bytes; the byte length says they are padding. The walk
47	# calls itself on the tail, which is the string shrinking.
48	def fill(text: String, +index: U32, arr: Array<U32>) -> Array<U32>:
49	  match text:
50	    case SNil{}:
51	      arr
52	    case SCon{w, SNil{}}:
53	      Array.set(U32, arr, index, pack(byte(w), 0, 0, 0))
54	    case SCon{w, SCon{x, SNil{}}}:
55	      Array.set(U32, arr, index, pack(byte(w), byte(x), 0, 0))
56	    case SCon{w, SCon{x, SCon{y, SNil{}}}}:
57	      Array.set(U32, arr, index, pack(byte(w), byte(x), byte(y), 0))
58	    case SCon{w, SCon{x, SCon{y, SCon{z, t}}}}:
59	      fill(t, U32.inc(index), Array.set(U32, arr, index, pack(byte(w), byte(x), byte(y), byte(z))))
60	
61	# the string packed into big-endian words, four bytes each
62	def bytes(+text: String) -> Array<U32>:
63	  +n = String.length(text)
64	  fill(text, 0, Array.new(U32, depth(words.of(n)), 0))
65	
66	# a length that does not fit is not a digest. A digest is sixty-four hex
67	# characters, so this empty answer cannot be mistaken for one.
68	def show(answer: Maybe<&1, Array<U32>>) -> String:
69	  match answer:
70	    case None{}:
71	      ""
72	    case Some{digest}:
73	      S.hex(digest)
74	
75	# the hex sha256 digest of a string whose characters are bytes: each one is
76	# reduced to its low eight bits. NAR serials are held this way.
77	def raw(+text: String) -> String:
78	  match text:
79	    case SNil{}:
80	      show(S.sha256(bytes(text), 0n))
81	    case SCon{_c, _t}:
82	      show(S.sha256(bytes(text), String.length(text)))
83	
84	# one byte as a character: a UTF-8 string is held in a Bend string one byte to
85	# a character, the shape `raw` hashes
86	def utf8.byte(+code: U32) -> Char:
87	  Chr{(code .&. 255 : U32)}
88	
89	def utf8.one(+code: U32) -> String:
90	  SCon{utf8.byte(code), SNil{}}
91	
92	def utf8.two(+code: U32) -> String:
93	  SCon{utf8.byte((192 .|. U32.shrn(code, 6n) : U32)),
94	    SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}}
95	
96	def utf8.three(+code: U32) -> String:
97	  SCon{utf8.byte((224 .|. U32.shrn(code, 12n) : U32)),
98	    SCon{utf8.byte((128 .|. (U32.shrn(code, 6n) .&. 63 : U32) : U32)),
99	      SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}}}
100	
101	def utf8.four(+code: U32) -> String:
102	  SCon{utf8.byte((240 .|. U32.shrn(code, 18n) : U32)),
103	    SCon{utf8.byte((128 .|. (U32.shrn(code, 12n) .&. 63 : U32) : U32)),
104	      SCon{utf8.byte((128 .|. (U32.shrn(code, 6n) .&. 63 : U32) : U32)),
105	        SCon{utf8.byte((128 .|. (code .&. 63 : U32) : U32)), SNil{}}}}}
106	
107	def utf8.put.three(three: Bool, +code: U32) -> String:
108	  match three:
109	    case True{}:
110	      utf8.three(code)
111	    case False{}:
112	      utf8.four(code)
113	
114	def utf8.put.two(two: Bool, +code: U32) -> String:
115	  match two:
116	    case True{}:
117	      utf8.two(code)
118	    case False{}:
119	      utf8.put.three(U32.is_lt(code, 65536), code)
120	
121	def utf8.put.ascii(ascii: Bool, +code: U32) -> String:
122	  match ascii:
123	    case True{}:
124	      utf8.one(code)
125	    case False{}:
126	      utf8.put.two(U32.is_lt(code, 2048), code)
127	
128	def utf8.put(+code: U32) -> String:
129	  utf8.put.ascii(U32.is_lt(code, 128), code)
130	
131	# the string's characters encoded as UTF-8, each byte a character
132	def utf8(+text: String) -> String:
133	  match text:
134	    case SNil{}:
135	      ""
136	    case SCon{c, t}:
137	      utf8.put(Char.to_u32(c)) ++ utf8(t)
138	
139	# the hex sha256 digest of a text's UTF-8 bytes, which is what `sha256sum`
140	# says of the file the text was read from, and what `bend --publish` and the
141	# hub hash a package file and its manifest by. The match is what a symbolic
142	# string sticks on, so a proof that only unfolds `hash_of` does not enter
143	# the digest.
144	def hex(+text: String) -> String:
145	  match text:
146	    case SNil{}:
147	      raw(text)
148	    case SCon{_c, _t}:
149	      raw(utf8(text))