src/crypto/sha/packed/core.bend checks
raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/core.bend as Core
2 imports
import Base import ../state.bend as S
Types
type ShaWindow source · line 4 · raw
Data
W@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> @e:U32 -> @f:U32 -> @g:U32 -> @h:U32 -> @i:U32 -> @j:U32 -> @k:U32 -> @l:U32 -> @m:U32 -> @n:U32 -> @o:U32 -> @p:U32 -> ShaWindow
Definitions
def initial source · line 10 · raw
0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
SHA-256 for byte sequences. Each input U32 contributes its low 8 bits. SHA-256 arithmetic is native U32, hence addition wraps modulo 2^32.
def big0 source · line 14 · raw
@+x:U32 -> U32
def big1 source · line 19 · raw
@+x:U32 -> U32
def small0 source · line 24 · raw
@+x:U32 -> U32
def small1 source · line 29 · raw
@+x:U32 -> U32
def choose source · line 34 · raw
@+x:U32 -> @y:U32 -> @z:U32 -> U32
def majority source · line 37 · raw
@+x:U32 -> @+y:U32 -> @+z:U32 -> U32
def step source · line 40 · raw
@s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> @k:U32 -> @w:U32 -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def feedforward source · line 46 · raw
@x:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> @y:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def pack source · line 52 · raw
@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32
def kr64 source · line 57 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr63 source · line 60 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr62 source · line 68 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr61 source · line 76 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr60 source · line 84 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr59 source · line 92 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr58 source · line 100 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr57 source · line 108 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr56 source · line 116 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr55 source · line 124 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr54 source · line 132 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr53 source · line 140 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr52 source · line 148 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr51 source · line 156 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr50 source · line 164 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr49 source · line 172 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr48 source · line 180 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr47 source · line 188 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr46 source · line 196 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr45 source · line 204 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr44 source · line 212 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr43 source · line 220 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr42 source · line 228 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr41 source · line 236 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr40 source · line 244 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr39 source · line 252 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr38 source · line 260 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr37 source · line 268 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr36 source · line 276 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr35 source · line 284 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr34 source · line 292 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr33 source · line 300 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr32 source · line 308 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr31 source · line 316 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr30 source · line 324 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr29 source · line 332 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr28 source · line 340 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr27 source · line 348 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr26 source · line 356 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr25 source · line 364 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr24 source · line 372 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr23 source · line 380 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr22 source · line 388 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr21 source · line 396 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr20 source · line 404 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr19 source · line 412 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr18 source · line 420 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr17 source · line 428 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def kr16 source · line 436 · raw
@q:Nat -> @win:ShaWindow -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
def fips_compress16 source · line 445 · raw
@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+q:Nat -> @+s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State
window_compress16 specialized to the FIPS table: no constant list is walked.
def len_hi source · line 469 · raw
@+n:Nat -> U32
FIPS padding suffix for a message of n bytes, computed with modular arithmetic. The proofs state the streaming hash in terms of it.
def len_lo source · line 480 · raw
@+n:Nat -> U32