spec/crypto/sha3.bend checks

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

3 imports

import Base
import ../../src/crypto/keccak/types.bend as T
import ./keccak/permutation.bend as K

Definitions

def padding_bytes source · line 25 · raw

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

M || 01 || pad10*1(r, |M| + 2) at the byte level, for q = 1..136 bytes to the end of the block: the suffix bits 0, 1 and the first pad bit 1 are the byte 0x06; the last pad bit is the top bit, 0x80, of the block's last byte; with one byte left both fall in it: 0x86.

def padding source · line 34 · raw

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

def pad source · line 37 · raw

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

def le32 source · line 42 · raw

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

def lanes source · line 47 · raw

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

Little-endian 64-bit lanes, eight bytes each.

def initial source · line 57 · raw

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

S = 0^1600.

def to_lanes source · line 64 · raw

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

def of_lanes source · line 69 · raw

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

def xor_lanes source · line 77 · raw

@xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane> -> @ys:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane>

Lane-wise XOR of a block into the leading lanes of the state.

def absorb source · line 85 · raw

@ls:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane> -> @+rounds:Nat -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State

Section 4, step 6: S = f(S XOR (P_i || 0^c)) for each r-bit block P_i.

def lane_bytes source · line 94 · raw

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

Section 4, steps 7-10: d = 256 <= r, so Z is the first 32 bytes of S.

def state_bytes source · line 100 · raw

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

def squeeze source · line 107 · raw

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

def keccak source · line 110 · raw

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

def sha3_256 source · line 114 · raw

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

SHA3-256(M): 32 bytes.