src/share/sha.bend

ezx@1.11.0.0 · 149 lines · 21 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))