spec/crypto/sha/packed.bend checks
raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.bend as Packed
3 imports
import Base import ../sha.bend as F import ../../../src/crypto/sha/state.bend as S
Definitions
def len_hi source · line 8 · raw
@+n:Nat -> U32
Packed-format reference: logical input byte j is the big-endian byte j%4 of array word floor(j/4). Only the declared prefix is part of the message. Block collection uses a generic list reader, not the optimized 16-read chain.
def len_lo source · line 19 · raw
@+n:Nat -> U32
def partial source · line 26 · raw
@+w:U32 -> @delta:Nat -> U32
def pad_choose source · line 34 · raw
@c:Cmp -> @w:U32 -> @delta:Nat -> U32
def pad_word source · line 40 · raw
@w:U32 -> @+pos:Nat -> @+remain:Nat -> U32
def length_word source · line 43 · raw
@short:Bool -> @w:U32 -> @length:U32 -> U32
def padded_word source · line 49 · raw
@+position:Nat -> @w:U32 -> @+remain:Nat -> @total:Nat -> U32
def padded_words source · line 55 · raw
@ws:List<&2, U32> -> @+position:Nat -> @+remain:Nat -> @+total:Nat -> List<&2, U32>
def prepare source · line 61 · raw
@padding:Bool -> @ws:List<&2, U32> -> @remain:Nat -> @total:Nat -> List<&2, U32>
def compress source · line 66 · raw
@ws:List<&2, U32> -> @extra:Nat -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def gather source · line 69 · raw
@+extra:Nat -> @n:Nat -> @+index:U32 -> @+padding:Bool -> @+remain:Nat -> @+total:Nat -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> @acc:List<&2, U32> -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State)
def final_extra source · line 77 · raw
@+extra:Nat -> @more:Bool -> @+total:Nat -> @pair:Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State)
def blocks source · line 83 · raw
@+extra:Nat -> @n:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State)
def take_state source · line 90 · raw
@pair:Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def hash_unchecked source · line 93 · raw
@a:Array<U32> -> @+length:Nat -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def checked source · line 96 · raw
@valid:Bool -> @a:Array<U32> -> @length:Nat -> Maybe<&2, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State>
def sized source · line 101 · raw
@+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&2, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State>
def hash source · line 105 · raw
@a:Array<U32> -> @length:Nat -> Maybe<&2, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State>
def digest_result source · line 108 · raw
@r:Maybe<&2, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State> -> Maybe<&2, List<&2, U32>>
def sha256 source · line 113 · raw
@a:Array<U32> -> @length:Nat -> Maybe<&2, List<&2, U32>>