~/bend-docscommunity

packed_spec.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.bend as Packed_spec

3 imports
import Base
import ./fips.bend as F
import ./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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State

def gather source · line 69 · raw

@+extra:Nat -> @n:Nat -> @+index:U32 -> @+padding:Bool -> @+remain:Nat -> @+total:Nat -> @s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> @acc:List<&2, U32> -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State)

def final_extra source · line 77 · raw

@+extra:Nat -> @more:Bool -> @+total:Nat -> @pair:Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State) -> Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State)

def blocks source · line 83 · raw

@+extra:Nat -> @n:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State) -> Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State)

def take_state source · line 90 · raw

@pair:Pair(Array<U32>, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State) -> 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State

def hash_unchecked source · line 93 · raw

@a:Array<U32> -> @+length:Nat -> 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State

def checked source · line 96 · raw

@valid:Bool -> @a:Array<U32> -> @length:Nat -> Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State>

def sized source · line 101 · raw

@+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State>

def hash source · line 105 · raw

@a:Array<U32> -> @length:Nat -> Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State>

def digest_result source · line 108 · raw

@r:Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State> -> Maybe<&2, List<&2, U32>>

def sha256 source · line 113 · raw

@a:Array<U32> -> @length:Nat -> Maybe<&2, List<&2, U32>>