src/crypto/sha/packed/packed.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/packed.bend as Packed
3 imports
import Base import ./core.bend as Core import ../state.bend as S
Definitions
def at source · line 6 · raw
@a:Array<U32> -> @i:U32 -> Pair(Array<U32>, U32)
Packed big-endian words: four bytes per U32. Array<U32> is flat u32 storage in native C.
def partial source · line 9 · raw
@+w:U32 -> @delta:Nat -> U32
def pad_choose source · line 17 · raw
@c:Cmp -> @w:U32 -> @delta:Nat -> U32
def pad_word source · line 23 · raw
@w:U32 -> @+pos:Nat -> @+remain:Nat -> U32
def length_word source · line 26 · raw
@short:Bool -> @w:U32 -> @length:U32 -> U32
def read16 source · line 31 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @w14:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read15 source · line 35 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read14 source · line 39 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read13 source · line 43 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read12 source · line 47 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read11 source · line 51 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read10 source · line 55 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read9 source · line 59 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read8 source · line 63 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read7 source · line 67 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read6 source · line 71 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read5 source · line 75 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read4 source · line 79 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read3 source · line 83 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @w1:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read2 source · line 87 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @w0:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def read1 source · line 91 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad16 source · line 95 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @w14:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad15 source · line 99 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad14 source · line 103 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad13 source · line 107 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad12 source · line 111 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad11 source · line 115 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad10 source · line 119 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad9 source · line 123 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad8 source · line 127 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad7 source · line 131 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad6 source · line 135 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad5 source · line 139 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad4 source · line 143 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad3 source · line 147 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @w1:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad2 source · line 151 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @w0:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def pad1 source · line 155 · raw
@+extra:Nat -> @+index:U32 -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def final_extra source · line 159 · raw
@+extra:Nat -> @more:Bool -> @+total:Nat -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def blocks source · line 165 · raw
@+extra:Nat -> @n:Nat -> @+index:U32 -> @+remain:Nat -> @+total:Nat -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State)
def take_state source · line 172 · raw
@pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State) -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def hash_unchecked source · line 176 · raw
@a:Array<U32> -> @+length:Nat -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Internal entry; callers must establish length <= 4*array capacity.
def checked source · line 179 · raw
@valid:Bool -> @a:Array<U32> -> @length:Nat -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>
def sized source · line 184 · raw
@+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>
def hash source · line 189 · raw
@a:Array<U32> -> @length:Nat -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State>
Public bounded API; consumes the input array, without constructing a byte list.