src/hub_sha/core.bend checks
raw source on the hub · import mylsm-lsm-store@0.3.1.0/src/hub_sha/core.bend as Core
Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
(src/crypto/sha/core.bend), byte-identical except Window renamed to
ShaWindow: Bend 2.0.28 Base added a GUI Window type that collides with
this module's schedule-window type. Verify against NIST vectors, not the
upstream PROOF.bend (which covers the original names).
2 imports
import Base import ./state.bend as S
Types
type ShaWindow source · line 9 · 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 15 · raw
0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 19 · raw
@+x:U32 -> @+n:Nat -> U32
def big0 source · line 22 · raw
@+x:U32 -> U32
def big1 source · line 27 · raw
@+x:U32 -> U32
def small0 source · line 32 · raw
@+x:U32 -> U32
def small1 source · line 37 · raw
@+x:U32 -> U32
def choose source · line 42 · raw
@+x:U32 -> @y:U32 -> @z:U32 -> U32
def majority source · line 45 · raw
@+x:U32 -> @+y:U32 -> @+z:U32 -> U32
def step source · line 48 · raw
@s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> @k:U32 -> @w:U32 -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def feedforward source · line 54 · raw
@x:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> @y:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def get source · line 60 · raw
@xs:List<&2, U32> -> @n:Nat -> U32
def next_word_slow source · line 70 · raw
@+history:List<&2, U32> -> U32
Reverse history: at round t, index j contains W[t-1-j].
def next_word source · line 77 · 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 84 · raw
@n:Nat -> @+history:List<&2, U32> -> List<&2, U32>
def schedule source · line 92 · raw
@extra:Nat -> @+block:List<&2, U32> -> List<&2, U32>
def rounds source · line 96 · raw
@ks:List<&2, U32> -> @ws:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def compress source · line 106 · raw
@ws:List<&2, U32> -> @ks:List<&2, U32> -> @+s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
Compression consumes an already expanded 64-word schedule.
def expanded_rounds source · line 112 · raw
@n:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 123 · raw
@ws:List<&2, U32> -> @+extra:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
Consume the original block words, then continue directly with its expansion.
def window_rounds source · line 134 · raw
@n:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 145 · raw
@ws:List<&2, U32> -> @+extra:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fused_compress_slow source · line 154 · raw
@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fused_compress source · line 157 · raw
@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def window_compress16 source · line 168 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 197 · raw
@+x:U32 -> List<&2, U32>
def length_octets source · line 201 · raw
@count:Nat -> @+n:Nat -> @acc:List<&2, U32> -> List<&2, U32>
def bit_length source · line 208 · raw
@+n:Nat -> List<&2, U32>
def pack source · line 212 · raw
@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32
def digest source · line 217 · raw
@s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> List<&2, U32>
def block_bytes source · line 223 · raw
@bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 236 · raw
List<&2, U32>
FIPS 180-4 round constants, the table the specialized rounds below inline.
def kr64 source · line 258 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 261 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr62 source · line 269 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr61 source · line 277 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr60 source · line 285 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr59 source · line 293 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr58 source · line 301 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr57 source · line 309 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr56 source · line 317 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr55 source · line 325 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr54 source · line 333 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr53 source · line 341 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr52 source · line 349 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr51 source · line 357 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr50 source · line 365 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr49 source · line 373 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr48 source · line 381 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr47 source · line 389 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr46 source · line 397 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr45 source · line 405 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr44 source · line 413 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr43 source · line 421 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr42 source · line 429 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr41 source · line 437 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr40 source · line 445 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr39 source · line 453 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr38 source · line 461 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr37 source · line 469 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr36 source · line 477 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr35 source · line 485 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr34 source · line 493 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr33 source · line 501 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr32 source · line 509 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr31 source · line 517 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr30 source · line 525 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr29 source · line 533 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr28 source · line 541 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr27 source · line 549 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr26 source · line 557 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr25 source · line 565 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr24 source · line 573 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr23 source · line 581 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr22 source · line 589 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr21 source · line 597 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr20 source · line 605 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr19 source · line 613 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr18 source · line 621 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr17 source · line 629 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def kr16 source · line 637 · raw
@q:Nat -> @win:ShaWindow -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fips_compress16 source · line 646 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
window_compress16 specialized to the FIPS table: no constant list is walked.
def suffix source · line 670 · 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 678 · 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 689 · raw
@+n:Nat -> U32
def fin0 source · line 700 · raw
@+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 704 · raw
@+t0:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin2 source · line 708 · raw
@+t0:U32 -> @+t1:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin3 source · line 712 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin4 source · line 716 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin5 source · line 720 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin6 source · line 724 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin7 source · line 728 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin8 source · line 732 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin9 source · line 736 · raw
@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin10 source · line 740 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin11 source · line 744 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin12 source · line 748 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin13 source · line 752 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin14 source · line 756 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin15 source · line 760 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin16 source · line 764 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin17 source · line 768 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin18 source · line 772 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin19 source · line 776 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin20 source · line 780 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin21 source · line 784 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin22 source · line 788 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin23 source · line 792 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin24 source · line 796 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin25 source · line 800 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin26 source · line 804 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin27 source · line 808 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin28 source · line 812 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin29 source · line 816 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin30 source · line 820 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin31 source · line 824 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin32 source · line 828 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin33 source · line 832 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin34 source · line 836 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin35 source · line 840 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin36 source · line 844 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin37 source · line 848 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin38 source · line 852 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin39 source · line 856 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin40 source · line 860 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin41 source · line 864 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin42 source · line 868 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin43 source · line 872 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin44 source · line 876 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin45 source · line 880 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin46 source · line 884 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin47 source · line 888 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin48 source · line 892 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin49 source · line 896 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin50 source · line 900 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin51 source · line 904 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin52 source · line 908 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin53 source · line 912 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin54 source · line 916 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin55 source · line 920 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin56 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin57 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin58 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin59 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin60 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin61 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin62 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 -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fin63 source · line 959 · 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:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
def fips_blocks source · line 965 · raw
@bytes:List<&2, U32> -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
Tail-recursive block loop over an already padded byte list.
def zeros_onto source · line 972 · raw
@z:Nat -> @acc:List<&2, U32> -> List<&2, U32>
def padding source · line 980 · raw
@+n:Nat -> List<&2, U32>
The padding suffix built only with tail-recursive loops.
def byte_count source · line 983 · raw
@bytes:List<&2, U32> -> @acc:Nat -> Nat
def finish_n source · line 996 · raw
@+tail:List<&2, U32> -> @+n:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 1130 · raw
@+tail:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State
count is the number of bytes already hashed, always a multiple of 64.
def stream source · line 1136 · raw
@+bytes:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0x0ae7ac793853e753f5f74c16e06ee078/src/hub_sha/state.State -> 0x0ae7ac793853e753f5f74c16e06ee078/src/hub_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 1149 · raw
@s:String -> List<&2, U32>
ASCII convenience only; binary inputs use sha256 directly.
def hex_digit_if source · line 1156 · raw
@x:U32 -> @small:Bool -> Char
def hex_digit source · line 1163 · raw
@+x:U32 -> Char
def hex_word_go source · line 1166 · raw
@n:Nat -> @+x:U32 -> @acc:String -> String
def hex_word source · line 1173 · raw
@x:U32 -> String
def hex source · line 1176 · raw
@ws:List<&2, U32> -> String
def sha256 source · line 1183 · raw
@bytes:List<&2, U32> -> List<&2, U32>