src/hub_sha/core.bend checks

raw source on the hub · import mylsm-lsm-store@0.4.0.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 10 · raw

Data

Represent ShaWindow data used by the SHA-256 compression implementation.

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 16 · raw

0x571fd57004366c423dfd4b51196743b5/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 21 · raw

@+word:U32 -> @+bit_shift:Nat -> U32

Handle rotr in the SHA-256 compression implementation.

def big0 source · line 25 · raw

@+word:U32 -> U32

Compute the big sigma function for 0 for the SHA-256 compression implementation.

def big1 source · line 31 · raw

@+word:U32 -> U32

Compute the big sigma function for 1 for the SHA-256 compression implementation.

def small0 source · line 37 · raw

@+word:U32 -> U32

Compute the small sigma function for 0 for the SHA-256 compression implementation.

def small1 source · line 43 · raw

@+word:U32 -> U32

Compute the small sigma function for 1 for the SHA-256 compression implementation.

def choose source · line 49 · raw

@+word_x:U32 -> @word_y:U32 -> @word_z:U32 -> U32

Handle choose in the SHA-256 compression implementation.

def majority source · line 53 · raw

@+word_x:U32 -> @+word_y:U32 -> @+word_z:U32 -> U32

Handle majority in the SHA-256 compression implementation.

def step source · line 57 · raw

@state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> @round_constant:U32 -> @schedule_word:U32 -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Handle step in the SHA-256 compression implementation.

def feedforward source · line 64 · raw

@prior_state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> @round_state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Feed forward for the SHA-256 compression implementation.

def get source · line 71 · raw

@xs:List<&2, U32> -> @index:Nat -> U32

Handle get in the SHA-256 compression implementation.

def next_word_slow source · line 81 · raw

@+history:List<&2, U32> -> U32

Reverse history: at round t, index j contains W[t-1-j].

def next_word source · line 88 · 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 96 · raw

@rounds_left:Nat -> @+history:List<&2, U32> -> List<&2, U32>

Handle expand in the SHA-256 compression implementation.

def schedule source · line 105 · raw

@extra:Nat -> @+block:List<&2, U32> -> List<&2, U32>

Handle schedule in the SHA-256 compression implementation.

def rounds source · line 110 · raw

@ks:List<&2, U32> -> @ws:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Handle rounds in the SHA-256 compression implementation.

def compress source · line 120 · raw

@ws:List<&2, U32> -> @ks:List<&2, U32> -> @+state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Compression consumes an already expanded 64-word schedule.

def expanded_rounds source · line 126 · raw

@rounds_left:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 137 · raw

@ws:List<&2, U32> -> @+extra:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Consume the original block words, then continue directly with its expansion.

def window_rounds source · line 154 · raw

@rounds_left:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 166 · raw

@ws:List<&2, U32> -> @+extra:Nat -> @win:ShaWindow -> @ks:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Handle window schedule rounds in the SHA-256 compression implementation.

def fused_compress_slow source · line 182 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Handle fused compress slow in the SHA-256 compression implementation.

def fused_compress source · line 186 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Handle fused compress in the SHA-256 compression implementation.

def window_compress16 source · line 197 · raw

@+word_a:U32 -> @+word_b:U32 -> @+word_c:U32 -> @+word_d:U32 -> @+word_e:U32 -> @+word_f:U32 -> @+word_g:U32 -> @+word_h:U32 -> @+word_i:U32 -> @+word_j:U32 -> @+round_constant:U32 -> @+word_l:U32 -> @+word_m:U32 -> @+count:U32 -> @+word_o:U32 -> @+word_p:U32 -> @+extra:Nat -> @+ks:List<&2, U32> -> @+state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 243 · raw

@+word:U32 -> List<&2, U32>

Handle be32 in the SHA-256 compression implementation.

def length_octets source · line 248 · raw

@count:Nat -> @+byte_length:Nat -> @acc:List<&2, U32> -> List<&2, U32>

Return the length of gth octets in the SHA-256 compression implementation.

def bit_length source · line 256 · raw

@+byte_length:Nat -> List<&2, U32>

Handle bit length in the SHA-256 compression implementation.

def pack source · line 261 · raw

@word_a:U32 -> @word_b:U32 -> @word_c:U32 -> @word_d:U32 -> U32

Handle pack in the SHA-256 compression implementation.

def digest source · line 267 · raw

@state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> List<&2, U32>

Handle digest in the SHA-256 compression implementation.

def block_bytes source · line 273 · raw

@bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 286 · raw

List<&2, U32>

FIPS 180-4 round constants, the table the specialized rounds below inline.

def kr64 source · line 308 · raw

@state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 312 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 63.

def kr62 source · line 321 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 62.

def kr61 source · line 330 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 61.

def kr60 source · line 339 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 60.

def kr59 source · line 348 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 59.

def kr58 source · line 357 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 58.

def kr57 source · line 366 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 57.

def kr56 source · line 375 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 56.

def kr55 source · line 384 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 55.

def kr54 source · line 393 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 54.

def kr53 source · line 402 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 53.

def kr52 source · line 411 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 52.

def kr51 source · line 420 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 51.

def kr50 source · line 429 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 50.

def kr49 source · line 438 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 49.

def kr48 source · line 447 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 48.

def kr47 source · line 456 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 47.

def kr46 source · line 465 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 46.

def kr45 source · line 474 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 45.

def kr44 source · line 483 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 44.

def kr43 source · line 492 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 43.

def kr42 source · line 501 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 42.

def kr41 source · line 510 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 41.

def kr40 source · line 519 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 40.

def kr39 source · line 528 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 39.

def kr38 source · line 537 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 38.

def kr37 source · line 546 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 37.

def kr36 source · line 555 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 36.

def kr35 source · line 564 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 35.

def kr34 source · line 573 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 34.

def kr33 source · line 582 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 33.

def kr32 source · line 591 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 32.

def kr31 source · line 600 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 31.

def kr30 source · line 609 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 30.

def kr29 source · line 618 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 29.

def kr28 source · line 627 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 28.

def kr27 source · line 636 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 27.

def kr26 source · line 645 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 26.

def kr25 source · line 654 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 25.

def kr24 source · line 663 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 24.

def kr23 source · line 672 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 23.

def kr22 source · line 681 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 22.

def kr21 source · line 690 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 21.

def kr20 source · line 699 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 20.

def kr19 source · line 708 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 19.

def kr18 source · line 717 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 18.

def kr17 source · line 726 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 17.

def kr16 source · line 735 · raw

@rounds_left:Nat -> @win:ShaWindow -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Return the SHA-256 round constant for schedule index 16.

def fips_compress16 source · line 744 · raw

@+word_a:U32 -> @+word_b:U32 -> @+word_c:U32 -> @+word_d:U32 -> @+word_e:U32 -> @+word_f:U32 -> @+word_g:U32 -> @+word_h:U32 -> @+word_i:U32 -> @+word_j:U32 -> @+round_constant:U32 -> @+word_l:U32 -> @+word_m:U32 -> @+count:U32 -> @+word_o:U32 -> @+word_p:U32 -> @+rounds_left:Nat -> @+state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

window_compress16 specialized to the FIPS table: no constant list is walked.

def suffix source · line 784 · raw

@+byte_length: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 792 · raw

@+byte_length: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 804 · raw

@+byte_length:Nat -> U32

Return the length of lo in the SHA-256 compression implementation.

def fin0 source · line 815 · raw

@+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 820 · raw

@+t0:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 1 to the compression state.

def fin2 source · line 825 · raw

@+t0:U32 -> @+t1:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 2 to the compression state.

def fin3 source · line 830 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 3 to the compression state.

def fin4 source · line 835 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 4 to the compression state.

def fin5 source · line 848 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 5 to the compression state.

def fin6 source · line 862 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 6 to the compression state.

def fin7 source · line 877 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 7 to the compression state.

def fin8 source · line 893 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 8 to the compression state.

def fin9 source · line 910 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 9 to the compression state.

def fin10 source · line 928 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 10 to the compression state.

def fin11 source · line 947 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 11 to the compression state.

def fin12 source · line 967 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 12 to the compression state.

def fin13 source · line 988 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 13 to the compression state.

def fin14 source · line 1010 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 14 to the compression state.

def fin15 source · line 1033 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 15 to the compression state.

def fin16 source · line 1057 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 16 to the compression state.

def fin17 source · line 1082 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 17 to the compression state.

def fin18 source · line 1108 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 18 to the compression state.

def fin19 source · line 1135 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 19 to the compression state.

def fin20 source · line 1163 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 20 to the compression state.

def fin21 source · line 1192 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 21 to the compression state.

def fin22 source · line 1222 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 22 to the compression state.

def fin23 source · line 1253 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 23 to the compression state.

def fin24 source · line 1285 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 24 to the compression state.

def fin25 source · line 1318 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 25 to the compression state.

def fin26 source · line 1352 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 26 to the compression state.

def fin27 source · line 1387 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 27 to the compression state.

def fin28 source · line 1423 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 28 to the compression state.

def fin29 source · line 1460 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 29 to the compression state.

def fin30 source · line 1498 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 30 to the compression state.

def fin31 source · line 1537 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 31 to the compression state.

def fin32 source · line 1577 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 32 to the compression state.

def fin33 source · line 1618 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 33 to the compression state.

def fin34 source · line 1660 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 34 to the compression state.

def fin35 source · line 1703 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 35 to the compression state.

def fin36 source · line 1747 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 36 to the compression state.

def fin37 source · line 1792 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 37 to the compression state.

def fin38 source · line 1838 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 38 to the compression state.

def fin39 source · line 1885 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 39 to the compression state.

def fin40 source · line 1933 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 40 to the compression state.

def fin41 source · line 1982 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 41 to the compression state.

def fin42 source · line 2032 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 42 to the compression state.

def fin43 source · line 2083 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 43 to the compression state.

def fin44 source · line 2135 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 44 to the compression state.

def fin45 source · line 2188 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 45 to the compression state.

def fin46 source · line 2242 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 46 to the compression state.

def fin47 source · line 2297 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 47 to the compression state.

def fin48 source · line 2353 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 48 to the compression state.

def fin49 source · line 2410 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 49 to the compression state.

def fin50 source · line 2468 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 50 to the compression state.

def fin51 source · line 2527 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 51 to the compression state.

def fin52 source · line 2587 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 52 to the compression state.

def fin53 source · line 2648 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 53 to the compression state.

def fin54 source · line 2710 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 54 to the compression state.

def fin55 source · line 2773 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 55 to the compression state.

def fin56 source · line 2837 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 56 to the compression state.

def fin57 source · line 2903 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 57 to the compression state.

def fin58 source · line 2970 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 58 to the compression state.

def fin59 source · line 3038 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 59 to the compression state.

def fin60 source · line 3107 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 60 to the compression state.

def fin61 source · line 3177 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 61 to the compression state.

def fin62 source · line 3248 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 62 to the compression state.

def fin63 source · line 3320 · 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 -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Apply SHA-256 round 63 to the compression state.

def fips_blocks source · line 3393 · raw

@bytes:List<&2, U32> -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Tail-recursive block loop over an already padded byte list.

def zeros_onto source · line 3401 · raw

@word_z:Nat -> @acc:List<&2, U32> -> List<&2, U32>

Append zero padding to onto for the SHA-256 compression implementation.

def padding source · line 3409 · raw

@+byte_length:Nat -> List<&2, U32>

The padding suffix built only with tail-recursive loops.

def byte_count source · line 3413 · raw

@bytes:List<&2, U32> -> @acc:Nat -> Nat

Handle byte lengths for count for the SHA-256 compression implementation.

def finish_n source · line 3426 · raw

@+tail:List<&2, U32> -> @+byte_length:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 3560 · raw

@+tail:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

count is the number of bytes already hashed, always a multiple of 64.

def stream source · line 3566 · raw

@+bytes:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/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 3579 · raw

@arg_s:String -> List<&2, U32>

ASCII convenience only; binary inputs use sha256 directly.

def hex_digit_if source · line 3587 · raw

@digit:U32 -> @small:Bool -> Char

Decode hexadecimal digit if for the SHA-256 compression implementation.

def hex_digit source · line 3595 · raw

@+digit:U32 -> Char

Decode hexadecimal digit for the SHA-256 compression implementation.

def hex_word_go source · line 3599 · raw

@digit_count:Nat -> @+word:U32 -> @acc:String -> String

Decode hexadecimal word go for the SHA-256 compression implementation.

def hex_word source · line 3607 · raw

@word:U32 -> String

Decode hexadecimal word for the SHA-256 compression implementation.

def hex source · line 3611 · raw

@ws:List<&2, U32> -> String

Handle hex in the SHA-256 compression implementation.

def sha256 source · line 3619 · raw

@bytes:List<&2, U32> -> List<&2, U32>

Handle sha256 in the SHA-256 compression implementation.