src/crypto/sha/core.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/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
0xd9a2fae439ac7ff9e21e0853948f94fe/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 rotr source · line 14 · raw
@+x:U32 -> @+n:Nat -> U32
def big0 source · line 17 · raw
@+x:U32 -> U32
def big1 source · line 22 · raw
@+x:U32 -> U32
def small0 source · line 27 · raw
@+x:U32 -> U32
def small1 source · line 32 · raw
@+x:U32 -> U32
def choose source · line 37 · raw
@+x:U32 -> @y:U32 -> @z:U32 -> U32
def majority source · line 40 · raw
@+x:U32 -> @+y:U32 -> @+z:U32 -> U32
def step source · line 43 · raw
@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @k:U32 -> @w:U32 -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def feedforward source · line 49 · raw
@x:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @y:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def get source · line 55 · raw
@xs:List<&2, U32> -> @n:Nat -> U32
def next_word_slow source · line 65 · raw
@+history:List<&2, U32> -> U32
Reverse history: at round t, index j contains W[t-1-j].
def next_word source · line 72 · raw
@+history:List<&2, U32> -> U32
Schedule histories always contain at least 16 words. Destructuring that prefix avoids four independent linked-list walks for every expanded word; the fallback preserves the total behavior used by the universal refinement theorem.
def expand source · line 79 · raw
@n:Nat -> @+history:List<&2, U32> -> List<&2, U32>
def schedule source · line 87 · raw
@extra:Nat -> @+block:List<&2, U32> -> List<&2, U32>
def rounds source · line 91 · raw
@ks:List<&2, U32> -> @ws:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def compress source · line 101 · raw
@ws:List<&2, U32> -> @ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Compression consumes an already expanded 64-word schedule.
def expanded_rounds source · line 107 · raw
@n:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Generate each derived schedule word immediately before its round. The reverse history is still retained for the recurrence, but the chronological 48-word extension is never materialized.
def schedule_rounds source · line 118 · raw
@ws:List<&2, U32> -> @+extra:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Consume the original block words, then continue directly with its expansion.
def window_rounds source · line 129 · raw
@n:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
A fixed rolling window drops schedule words as soon as they are older than 16 rounds. This avoids growing and reference-counting the reverse history list.
def window_schedule_rounds source · line 140 · raw
@ws:List<&2, U32> -> @+extra:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fused_compress_slow source · line 149 · raw
@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fused_compress source · line 152 · raw
@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def window_compress16 source · line 163 · 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 -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Fast path for the 16-word blocks produced by block_bytes. It executes the seed rounds directly and constructs only the fixed rolling window.
def be32 source · line 192 · raw
@+x:U32 -> List<&2, U32>
def length_octets source · line 196 · raw
@count:Nat -> @+n:Nat -> @acc:List<&2, U32> -> List<&2, U32>
def bit_length source · line 203 · raw
@+n:Nat -> List<&2, U32>
def pack source · line 207 · raw
@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32
def digest source · line 212 · raw
@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> List<&2, U32>
def block_bytes source · line 218 · raw
@bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Generic block decoder over a padded byte list and any constant table. The fast path below is proved equal to it with the FIPS table.
def round_constants source · line 231 · raw
List<&2, U32>
FIPS 180-4 round constants, the table the specialized rounds below inline.
def kr64 source · line 253 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
SHA-256 round t (16 <= t < 64) with its constant as a literal. Like window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round derives its schedule word from the rolling window before continuing with round t+1. Defined last-to-first because names must precede use.
def kr63 source · line 256 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr62 source · line 264 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr61 source · line 272 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr60 source · line 280 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr59 source · line 288 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr58 source · line 296 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr57 source · line 304 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr56 source · line 312 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr55 source · line 320 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr54 source · line 328 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr53 source · line 336 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr52 source · line 344 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr51 source · line 352 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr50 source · line 360 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr49 source · line 368 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr48 source · line 376 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr47 source · line 384 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr46 source · line 392 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr45 source · line 400 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr44 source · line 408 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr43 source · line 416 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr42 source · line 424 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr41 source · line 432 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr40 source · line 440 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr39 source · line 448 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr38 source · line 456 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr37 source · line 464 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr36 source · line 472 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr35 source · line 480 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr34 source · line 488 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr33 source · line 496 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr32 source · line 504 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr31 source · line 512 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr30 source · line 520 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr29 source · line 528 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr28 source · line 536 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr27 source · line 544 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr26 source · line 552 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr25 source · line 560 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr24 source · line 568 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr23 source · line 576 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr22 source · line 584 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr21 source · line 592 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr20 source · line 600 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr19 source · line 608 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr18 source · line 616 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr17 source · line 624 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def kr16 source · line 632 · raw
@q:Nat -> @win:ShaWindow -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fips_compress16 source · line 641 · 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:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
window_compress16 specialized to the FIPS table: no constant list is walked.
def suffix source · line 665 · raw
@+n:Nat -> List<&2, 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_hi source · line 673 · raw
@+n:Nat -> U32
Big-endian words of the 64-bit message bit length 8n, computed from n with exactly the digit expressions bit_length produces, but without building and matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low] where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
def len_lo source · line 684 · raw
@+n:Nat -> U32
def fin0 source · line 695 · raw
@+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Final block(s) for an n-byte message ending in r = 0..63 tail bytes. Each tail length has its own padded layout: the tail bytes, the 0x80 marker, the zero fill and the big-endian bit length are packed straight into schedule words, so no padded list is built.
def fin1 source · line 699 · raw
@+t0:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin2 source · line 703 · raw
@+t0:U32 -> @+t1:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin3 source · line 707 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin4 source · line 711 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin5 source · line 715 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin6 source · line 719 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin7 source · line 723 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin8 source · line 727 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin9 source · line 731 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin10 source · line 735 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin11 source · line 739 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin12 source · line 743 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin13 source · line 747 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin14 source · line 751 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin15 source · line 755 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin16 source · line 759 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin17 source · line 763 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin18 source · line 767 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin19 source · line 771 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin20 source · line 775 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin21 source · line 779 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin22 source · line 783 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin23 source · line 787 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin24 source · line 791 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin25 source · line 795 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin26 source · line 799 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin27 source · line 803 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin28 source · line 807 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin29 source · line 811 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin30 source · line 815 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin31 source · line 819 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin32 source · line 823 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin33 source · line 827 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin34 source · line 831 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin35 source · line 835 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin36 source · line 839 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin37 source · line 843 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin38 source · line 847 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin39 source · line 851 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin40 source · line 855 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin41 source · line 859 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin42 source · line 863 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin43 source · line 867 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin44 source · line 871 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin45 source · line 875 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin46 source · line 879 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin47 source · line 883 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin48 source · line 887 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin49 source · line 891 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin50 source · line 895 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin51 source · line 899 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin52 source · line 903 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin53 source · line 907 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin54 source · line 911 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin55 source · line 915 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin56 source · line 919 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin57 source · line 924 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin58 source · line 929 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin59 source · line 934 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin60 source · line 939 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin61 source · line 944 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin62 source · line 949 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+t61:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fin63 source · line 954 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+t61:U32 -> @+t62:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
def fips_blocks source · line 960 · raw
@bytes:List<&2, U32> -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Tail-recursive block loop over an already padded byte list.
def zeros_onto source · line 967 · raw
@z:Nat -> @acc:List<&2, U32> -> List<&2, U32>
def padding source · line 975 · raw
@+n:Nat -> List<&2, U32>
The padding suffix built only with tail-recursive loops.
def byte_count source · line 978 · raw
@bytes:List<&2, U32> -> @acc:Nat -> Nat
def finish_n source · line 991 · raw
@+tail:List<&2, U32> -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Final block(s) of an n-byte message whose tail has fewer than 64 bytes. stream never passes 64 or more bytes; that case pads with tail-recursive loops. The match is exhaustive: a default case would make Bend rebuild the consumed cells at every depth. Length words are computed directly from n; note that sharing any List<U32> would make Bend reference-count every list match, including the input loop in stream.
def finish source · line 1125 · raw
@+tail:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
count is the number of bytes already hashed, always a multiple of 64.
def stream source · line 1131 · raw
@+bytes:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State
Compress complete 64-byte blocks straight from the input list, so the message is never copied, counted or reversed. count is the number of bytes already hashed and extra the number of derived schedule words (48).
def ascii source · line 1144 · raw
@s:String -> List<&2, U32>
ASCII convenience only; binary inputs use sha256 directly.
def hex_digit_if source · line 1151 · raw
@x:U32 -> @small:Bool -> Char
def hex_digit source · line 1158 · raw
@+x:U32 -> Char
def hex_word_go source · line 1161 · raw
@n:Nat -> @+x:U32 -> @acc:String -> String
def hex_word source · line 1168 · raw
@x:U32 -> String
def hex source · line 1171 · raw
@ws:List<&2, U32> -> String
def sha256 source · line 1178 · raw
@bytes:List<&2, U32> -> List<&2, U32>