~/bend-docscommunity

proofs/crypto/sha/packed/core_model.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/packed/core_model.bend as Core_model

Proof-only historical implementation model; not a production dependency.

3 imports
import Base
import ../../../../src/crypto/sha/packed/core.bend as Runtime
import ../../../../src/crypto/sha/state.bend as S

Definitions

def rotr source · line 6 · raw

@+x:U32 -> @+n:Nat -> U32

def get source · line 9 · raw

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

def next_word_slow source · line 19 · raw

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

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

def next_word source · line 26 · 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 33 · raw

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

def schedule source · line 41 · raw

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

def rounds source · line 45 · raw

@ks:List<&2, U32> -> @ws:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def compress source · line 55 · raw

@ws:List<&2, U32> -> @ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Compression consumes an already expanded 64-word schedule.

def expanded_rounds source · line 61 · raw

@n:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Generate each derived schedule word immediately before its round. The reverse history is still retained for the recurrence, but the chronological 48-word extension is never materialized.

def schedule_rounds source · line 72 · raw

@ws:List<&2, U32> -> @+extra:Nat -> @+history:List<&2, U32> -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

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

def window_rounds source · line 83 · raw

@n:Nat -> @win:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/core.ShaWindow -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

A fixed rolling window drops schedule words as soon as they are older than 16 rounds. This avoids growing and reference-counting the reverse history list.

def window_schedule_rounds source · line 94 · raw

@ws:List<&2, U32> -> @+extra:Nat -> @win:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/packed/core.ShaWindow -> @ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fused_compress_slow source · line 103 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fused_compress source · line 106 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def window_compress16 source · line 117 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Fast path for the 16-word blocks produced by block_bytes. It executes the seed rounds directly and constructs only the fixed rolling window.

def be32 source · line 146 · raw

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

def length_octets source · line 150 · raw

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

def bit_length source · line 157 · raw

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

def digest source · line 161 · raw

@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> List<&2, U32>

def block_bytes source · line 167 · raw

@bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Generic block decoder over a padded byte list and any constant table. The fast path below is proved equal to it with the FIPS table.

def round_constants source · line 180 · raw

List<&2, U32>

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

def suffix source · line 202 · raw

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

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 fin0 source · line 210 · raw

@+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

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 fin1 source · line 214 · raw

@+t0:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin2 source · line 218 · raw

@+t0:U32 -> @+t1:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin3 source · line 222 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin4 source · line 226 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin5 source · line 230 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin6 source · line 234 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin7 source · line 238 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin8 source · line 242 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin9 source · line 246 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin10 source · line 250 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin11 source · line 254 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin12 source · line 258 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin13 source · line 262 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin14 source · line 266 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin15 source · line 270 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin16 source · line 274 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin17 source · line 278 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin18 source · line 282 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin19 source · line 286 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin20 source · line 290 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin21 source · line 294 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin22 source · line 298 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin23 source · line 302 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin24 source · line 306 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin25 source · line 310 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin26 source · line 314 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin27 source · line 318 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin28 source · line 322 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin29 source · line 326 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin30 source · line 330 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin31 source · line 334 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin32 source · line 338 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin33 source · line 342 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin34 source · line 346 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin35 source · line 350 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin36 source · line 354 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin37 source · line 358 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin38 source · line 362 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin39 source · line 366 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin40 source · line 370 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin41 source · line 374 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin42 source · line 378 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin43 source · line 382 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin44 source · line 386 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin45 source · line 390 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin46 source · line 394 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin47 source · line 398 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin48 source · line 402 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin49 source · line 406 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin50 source · line 410 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin51 source · line 414 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin52 source · line 418 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin53 source · line 422 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin54 source · line 426 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin55 source · line 430 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin56 source · line 434 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin57 source · line 439 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin58 source · line 444 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin59 source · line 449 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin60 source · line 454 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin61 source · line 459 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin62 source · line 464 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+t61:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fin63 source · line 469 · raw

@+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @+t16:U32 -> @+t17:U32 -> @+t18:U32 -> @+t19:U32 -> @+t20:U32 -> @+t21:U32 -> @+t22:U32 -> @+t23:U32 -> @+t24:U32 -> @+t25:U32 -> @+t26:U32 -> @+t27:U32 -> @+t28:U32 -> @+t29:U32 -> @+t30:U32 -> @+t31:U32 -> @+t32:U32 -> @+t33:U32 -> @+t34:U32 -> @+t35:U32 -> @+t36:U32 -> @+t37:U32 -> @+t38:U32 -> @+t39:U32 -> @+t40:U32 -> @+t41:U32 -> @+t42:U32 -> @+t43:U32 -> @+t44:U32 -> @+t45:U32 -> @+t46:U32 -> @+t47:U32 -> @+t48:U32 -> @+t49:U32 -> @+t50:U32 -> @+t51:U32 -> @+t52:U32 -> @+t53:U32 -> @+t54:U32 -> @+t55:U32 -> @+t56:U32 -> @+t57:U32 -> @+t58:U32 -> @+t59:U32 -> @+t60:U32 -> @+t61:U32 -> @+t62:U32 -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

def fips_blocks source · line 475 · raw

@bytes:List<&2, U32> -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

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

def zeros_onto source · line 482 · raw

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

def padding source · line 490 · raw

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

The padding suffix built only with tail-recursive loops.

def byte_count source · line 493 · raw

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

def finish_n source · line 506 · raw

@+tail:List<&2, U32> -> @+n:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Final block(s) of an n-byte message whose tail has fewer than 64 bytes. stream never passes 64 or more bytes; that case pads with tail-recursive loops. The match is exhaustive: a default case would make Bend rebuild the consumed cells at every depth. Length words are computed directly from n; note that sharing any List<U32> would make Bend reference-count every list match, including the input loop in stream.

def finish source · line 640 · raw

@+tail:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

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

def stream source · line 646 · raw

@+bytes:List<&2, U32> -> @count:Nat -> @+extra:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State

Compress complete 64-byte blocks straight from the input list, so the message is never copied, counted or reversed. count is the number of bytes already hashed and extra the number of derived schedule words (48).

def ascii source · line 659 · raw

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

ASCII convenience only; binary inputs use sha256 directly.

def hex_digit_if source · line 666 · raw

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

def hex_digit source · line 673 · raw

@+x:U32 -> Char

def hex_word_go source · line 676 · raw

@n:Nat -> @+x:U32 -> @acc:String -> String

def hex_word source · line 683 · raw

@x:U32 -> String

def hex source · line 686 · raw

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

def sha256 source · line 693 · raw

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