~/bend-docscommunity

spec/crypto/sha512.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as Sha512

2 imports
import Base
import ../../src/crypto/sha512/types.bend as T

Definitions

def add source · line 19 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

FIPS 180-4 section 3.2: x + y mod 2^64. The low halves add modulo 2^32; the high halves add the carry out of the low half, which is 1 exactly when the low sum wrapped below either addend.

def xor source · line 25 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def and source · line 30 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def not source · line 35 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def rotr_small source · line 42 · raw

@+hi:U32 -> @+lo:U32 -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

ROTR^n on the halves for 0 < n < 32: each half keeps its bits shifted right and takes the other half's low n bits at the top.

def rotr_split source · line 47 · raw

@+hi:U32 -> @+lo:U32 -> @+n:Nat -> @small:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

32 <= n < 64: rotating by 32 swaps the halves, then rotate by n - 32.

def rotr source · line 55 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

FIPS 180-4 section 3.2: ROTR^n(x) = (x >> n) OR (x << 64 - n), 0 < n < 64.

def shr source · line 61 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

FIPS 180-4 section 3.2: SHR^n(x) = x >> n, here for 0 < n < 32.

def sum0 source · line 68 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def sum1 source · line 71 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def sigma0 source · line 74 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def sigma1 source · line 77 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def ch source · line 80 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @z:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def maj source · line 83 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+z:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def initial source · line 89 · raw

0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

Section 5.3.5: the initial hash value H(0).

def constants source · line 96 · raw

List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

Section 4.2.3: K0 .. K79.

def octets source · line 141 · raw

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

A base-256 representation, most significant digit first, of fixed width.

def length_field source · line 152 · raw

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

The 128-bit block of the message length in bits, 8n: its low octet is 8 * (n mod 32) and the fifteen above it are n div 32 in base 256 (8n = 256 * (n div 32) + 8 * (n mod 32)), so no Nat above n is formed.

def zero_count_if source · line 158 · raw

@r:Nat -> @fits:Bool -> Nat

The k zero bytes with n + 1 + k = 112 (mod 128): a remainder of 0..111 leaves room for the length in this block, one of 112..127 needs another block.

def zero_count source · line 165 · raw

@+r:Nat -> Nat

def padding_suffix source · line 168 · raw

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

def pad source · line 172 · raw

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

def decode source · line 177 · raw

@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32

def words source · line 183 · raw

@bytes:List<&2, U32> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

Big-endian 64-bit words, eight bytes each (a trailing partial word is dropped; padded messages have none).

def nth source · line 193 · raw

@history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @index:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

In reverse history, index j is W[t-1-j]; the zero default makes nth total.

def previous source · line 202 · raw

@history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @lag:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

def recurrence source · line 206 · raw

@+history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane

W[t] = sigma1(W[t-2]) + W[t-7] + sigma0(W[t-15]) + W[t-16]

def extension source · line 210 · raw

@rounds:Nat -> @+history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

def schedule source · line 219 · raw

@extra:Nat -> @+block:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

SHA-512 instantiates extra = 64, extending the 16 block words to 80.

def schedules source · line 222 · raw

@ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+extra:Nat -> List<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>>

def prepare source · line 229 · raw

@bytes:List<&2, U32> -> @extra:Nat -> List<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>>

def step source · line 234 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> @k:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def rounds source · line 240 · raw

@ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @_:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def feedforward source · line 250 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def compress source · line 255 · raw

@ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def blocks source · line 258 · raw

@prepared:List<&2, List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>> -> @+ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> @_:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State

def digest source · line 266 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

def hash source · line 270 · raw

@bytes:List<&2, U32> -> @extra:Nat -> @ks:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

def sha512 source · line 274 · raw

@bytes:List<&2, U32> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane>

SHA-512(M): the eight words H(N).

def word_octets source · line 280 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> List<&2, U32>

Each word most significant octet first.

def digest_octets source · line 288 · raw

@ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane> -> List<&2, U32>

def sha512_bytes source · line 296 · raw

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

The 64-byte SHA-512 digest.