fips.bend checks
raw source on the hub · import 0xda83506fb9f059ead7afcfa2f498df5f/fips.bend as Fips
2 imports
import Base import ./state.bend as Types
Definitions
def initial source · line 9 · raw
0xda83506fb9f059ead7afcfa2f498df5f/state.State
def rotate source · line 14 · raw
@+x:U32 -> @+n:Nat -> U32
FIPS 4.1.2: ROR_n(x) = SHR_n(x) OR SHL_(32-n)(x).
def sigma0 source · line 17 · raw
@+x:U32 -> U32
def sigma1 source · line 20 · raw
@+x:U32 -> U32
def sum0 source · line 23 · raw
@+x:U32 -> U32
def sum1 source · line 26 · raw
@+x:U32 -> U32
def ch source · line 29 · raw
@+x:U32 -> @y:U32 -> @z:U32 -> U32
def maj source · line 32 · raw
@+x:U32 -> @+y:U32 -> @+z:U32 -> U32
def octets source · line 36 · raw
@width:Nat -> @+n:Nat -> List<&2, U32>
A base-256 representation, most significant digit first, of fixed width.
def length_field source · line 45 · raw
@+n:Nat -> List<&2, U32>
8*n = 256*(n/32) + 8*(n mod 32); avoids overflowing runtime Nat.
def zero_count_if source · line 51 · raw
@r:Nat -> @fits:Bool -> Nat
FIPS padding: a remainder of 0..55 leaves room in this block; a remainder of 56..63 needs another block. No modular shortcut is used.
def zero_count source · line 58 · raw
@+r:Nat -> Nat
def padding_suffix source · line 61 · raw
@+n:Nat -> List<&2, U32>
def pad source · line 65 · raw
@+bytes:List<&2, U32> -> List<&2, U32>
def decode source · line 68 · raw
@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32
def words source · line 72 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def nth source · line 81 · raw
@history:List<&2, U32> -> @index:Nat -> U32
In reverse history, index j denotes W[t-1-j]. Only valid indices are reached for the actual 16-word input blocks; default zero makes nth total.
def previous source · line 91 · raw
@history:List<&2, U32> -> @lag:Nat -> U32
The FIPS recurrence names prior words by lags 2, 7, 15 and 16.
def recurrence source · line 94 · raw
@+history:List<&2, U32> -> U32
def extension source · line 98 · raw
@rounds:Nat -> @+history:List<&2, U32> -> List<&2, U32>
def schedule source · line 107 · raw
@extra:Nat -> @+block:List<&2, U32> -> List<&2, U32>
Standard SHA-256 instantiates extra=48, extending the initial 16 to 64.
def schedules source · line 110 · raw
@ws:List<&2, U32> -> @+extra:Nat -> List<&2, List<&2, U32>>
def prepare source · line 117 · raw
@bytes:List<&2, U32> -> @extra:Nat -> List<&2, List<&2, U32>>
def step source · line 120 · raw
@s:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> @k:U32 -> @w:U32 -> 0xda83506fb9f059ead7afcfa2f498df5f/state.State
def rounds source · line 126 · raw
@ks:List<&2, U32> -> @ws:List<&2, U32> -> @_:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> 0xda83506fb9f059ead7afcfa2f498df5f/state.State
def feedforward source · line 136 · raw
@x:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> @y:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> 0xda83506fb9f059ead7afcfa2f498df5f/state.State
def compress source · line 142 · raw
@ws:List<&2, U32> -> @ks:List<&2, U32> -> @+s:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> 0xda83506fb9f059ead7afcfa2f498df5f/state.State
def blocks source · line 145 · raw
@prepared:List<&2, List<&2, U32>> -> @+ks:List<&2, U32> -> @_:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> 0xda83506fb9f059ead7afcfa2f498df5f/state.State
def digest source · line 153 · raw
@s:0xda83506fb9f059ead7afcfa2f498df5f/state.State -> List<&2, U32>
def hash source · line 157 · raw
@bytes:List<&2, U32> -> @extra:Nat -> @ks:List<&2, U32> -> List<&2, U32>
def constants source · line 161 · raw
List<&2, U32>
FIPS 180-4 section 4.2.2, transcribed separately from the implementation.
def sha256 source · line 179 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def word_octets source · line 183 · raw
@+w:U32 -> List<&2, U32>
FIPS digest serialization: most significant octet of each word first.
def digest_octets source · line 188 · raw
@ws:List<&2, U32> -> List<&2, U32>
def sha256_bytes source · line 195 · raw
@bytes:List<&2, U32> -> List<&2, U32>