src/share/sha.bend checks

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/share/sha.bend as Sha

share/sha: the sha256 a package hash is built from. The digest itself comes from noah-emp/bend-sha256, which proves its output equal to an executable FIPS 180-4 specification; this file is only the string-in, hex-out shape ez uses. The dependency hashes packed big-endian words and returns eight of them, or nothing when the declared length does not fit the array.

2 imports

import Base
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as S

Definitions

def pack source · line 10 · raw

@first:U32 -> @second:U32 -> @third:U32 -> @fourth:U32 -> U32

four big-endian bytes in one word, each kept to eight bits

def byte source · line 16 · raw

@ch:Char -> U32

one character as the byte it contributes

def words.of source · line 20 · raw

@len:Nat -> Nat

how many words hold this many bytes

def depth.step source · line 25 · raw

@more:Bool -> @acc:Nat -> @rest:(@_:Unit -> Nat) -> Nat

one more bit of depth when the capacity does not yet hold the words. The rest is a thunk, so the stop does not build the next depth.

def depth.go source · line 33 · raw

@bits:Nat -> @+words:Nat -> @+cap:Nat -> @+acc:Nat -> Nat

the depth of an array whose capacity, 2^depth, is at least words

def depth source · line 42 · raw

@words:Nat -> Nat

the depth of the array that holds this many words, at most 32

def fill source · line 48 · raw

@text:String -> @+index:U32 -> @arr:Array<U32> -> Array<U32>

the string packed into the array, four bytes to a word. A short tail packs zeros in the unused bytes; the byte length says they are padding. The walk calls itself on the tail, which is the string shrinking.

def bytes source · line 62 · raw

@+text:String -> Array<U32>

the string packed into big-endian words, four bytes each

def show source · line 68 · raw

@answer:Maybe<&1, Array<U32>> -> String

a length that does not fit is not a digest. A digest is sixty-four hex characters, so this empty answer cannot be mistaken for one.

def raw source · line 77 · raw

@+text:String -> String

the hex sha256 digest of a string whose characters are bytes: each one is reduced to its low eight bits. NAR serials are held this way.

def utf8.byte source · line 86 · raw

@+code:U32 -> Char

one byte as a character: a UTF-8 string is held in a Bend string one byte to a character, the shape raw hashes

def utf8.one source · line 89 · raw

@+code:U32 -> String

def utf8.two source · line 92 · raw

@+code:U32 -> String

def utf8.three source · line 96 · raw

@+code:U32 -> String

def utf8.four source · line 101 · raw

@+code:U32 -> String

def utf8.put.three source · line 107 · raw

@three:Bool -> @+code:U32 -> String

def utf8.put.two source · line 114 · raw

@two:Bool -> @+code:U32 -> String

def utf8.put.ascii source · line 121 · raw

@ascii:Bool -> @+code:U32 -> String

def utf8.put source · line 128 · raw

@+code:U32 -> String

def utf8 source · line 132 · raw

@+text:String -> String

the string's characters encoded as UTF-8, each byte a character

def hex source · line 144 · raw

@+text:String -> String

the hex sha256 digest of a text's UTF-8 bytes, which is what sha256sum says of the file the text was read from, and what bend --publish and the hub hash a package file and its manifest by. The match is what a symbolic string sticks on, so a proof that only unfolds hash_of does not enter the digest.