sha256.bend checks

raw source on the hub · import 0xfbc4773809086afacef84e7fba6d620c/sha256.bend as Sha256

SHA-256 (FIPS 180-4), for Digest authentication with SHA-256 (RFC 7616). Bytes are U32s below 256; a block is 16 big-endian words.

1 import

import Base

Types

Data

The eight words of the state.

Sha

@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> @e:U32 -> @f:U32 -> @g:U32 -> @h:U32 -> Sha

@+x:U32 -> @+n:Nat -> U32

x rotated right by n bits (0 < n < 32).

List<&2, U32>

The round constants: the first 32 bits of the fractional parts of the cube roots of the first 64 primes.

@+x:U32 -> U32

@+x:U32 -> U32

@m:Maybe<&2, U32> -> U32

@xs:List<&2, U32> -> @i:Nat -> U32

@n:Nat -> @+win:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

The message schedule: n more words after a window of the last 16 (the oldest first), each made of four of them; onto acc, the last first.

@+ws:List<&2, U32> -> List<&2, U32>

The 64 words of a block's schedule, from its 16.

@ks:List<&2, U32> -> @ws:List<&2, U32> -> @st:Sha -> Sha

The 64 steps over one block: a constant and a schedule word each.

@x:Sha -> @y:Sha -> Sha

@n:Nat -> @bs:List<&2, U32> -> List<&2, U32>

The first n big-endian words of a byte list.

@fuel:Nat -> @+bs:List<&2, U32> -> @+st:Sha -> Sha

Every 64-byte block folded into the state; fuel: the block count.

@n:Nat -> List<&2, U32>

@+x:U32 -> List<&2, U32>

A word's four bytes, big-endian.

@+bs:List<&2, U32> -> List<&2, U32>

The message padded: a 1 bit, zeros up to 56 mod 64, the bit length in 64 bits (messages here are far below 512 MB, so its high word is 0).

@st:Sha -> List<&2, U32>

@+p:List<&2, U32> -> List<&2, U32>

@bs:List<&2, U32> -> List<&2, U32>

The 32 bytes of the SHA-256 of bs.