src/share/sha.bend
ezx@1.4.0.0 · 149 lines · 0 definitions
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.
6import Base
7import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as S
8
9# four big-endian bytes in one word, each kept to eight bits
10def 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
16def byte(ch: Char) -> U32:
17 Char.to_u32(ch)
18
19# how many words hold this many bytes
20def 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.
25def 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`
33def 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
42def 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.
48def 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
62def 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.
68def 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.
77def 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
86def utf8.byte(+code: U32) -> Char:
87 Chr{(code .&. 255 : U32)}
88
89def utf8.one(+code: U32) -> String:
90 SCon{utf8.byte(code), SNil{}}
91
92def 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
96def 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
101def 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
107def 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
114def 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
121def 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
128def 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
132def 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.
144def hex(+text: String) -> String:
145 match text:
146 case SNil{}:
147 raw(text)
148 case SCon{_c, _t}:
149 raw(utf8(text))