~/bend-docscommunity

src/crypto/hash.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/hash.bend as Hash

Generated by tools/generators/hash_gen.py; do not edit by hand.

9 imports
import Base
import ./sha/state.bend as S256
import ./sha/core.bend as C256
import ./sha/sha256.bend as SHA256
import ./sha512/types.bend as T512
import ./sha512/core.bend as C512
import ./keccak/types.bend as TK
import ./keccak/permutation.bend as P
import ./sha3/core.bend as C3

Types

type Sha256State source · line 29 · raw

Data

A chaining state and the buffered bytes of the unfinished block.

type Sha512State source · line 32 · raw

Data

type Sha3State source · line 35 · raw

Data

type Hasher source · line 38 · raw

Data

type Read256 source · line 61 · raw

Data

One block read 4 bytes at a time into its 16 words, or Short when fewer than 64 bytes are left.

type Read512 source · line 208 · raw

Data

One block read 8 bytes at a time into its 16 words, or Short when fewer than 128 bytes are left.

type Read3 source · line 355 · raw

Data

One block read 8 bytes at a time into its 17 words, or Short when fewer than 136 bytes are left.

Definitions

def sha256 source · line 46 · raw

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

SHA-256 (FIPS 180-4), 32 bytes.

def sha512 source · line 50 · raw

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

SHA-512 (FIPS 180-4), 64 bytes.

def sha3_256 source · line 54 · raw

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

SHA3-256 (FIPS 202), 32 bytes.

def read256_16 source · line 65 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @w14:U32 -> @w15:U32 -> Read256

def read256_15 source · line 68 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> @w14:U32 -> Read256

def read256_14 source · line 75 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> @w13:U32 -> Read256

def read256_13 source · line 82 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @w12:U32 -> Read256

def read256_12 source · line 89 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> Read256

def read256_11 source · line 96 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> Read256

def read256_10 source · line 103 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> Read256

def read256_9 source · line 110 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> Read256

def read256_8 source · line 117 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> Read256

def read256_7 source · line 124 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> Read256

def read256_6 source · line 131 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> Read256

def read256_5 source · line 138 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> Read256

def read256_4 source · line 145 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> Read256

def read256_3 source · line 152 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> @w2:U32 -> Read256

def read256_2 source · line 159 · raw

@bytes:List<&2, U32> -> @w0:U32 -> @w1:U32 -> Read256

def read256_1 source · line 166 · raw

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

def read256_0 source · line 173 · raw

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

def absorb256 source · line 184 · raw

@fuel:Nat -> @r:Read256 -> @orig:List<&2, U32> -> @+q:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> Sha256State

Compress every whole block (fuel bounds the count: any fuel >= the number of blocks reads them all; fewer leaves the rest buffered, still correct). The chaining state and the unread bytes; orig is the list the read r started at. q is the algorithm's round parameter (48n), kept a variable for the proofs.

def step256 source · line 193 · raw

@st:Sha256State -> @xs:List<&2, U32> -> @+q:Nat -> Sha256State

def finish256 source · line 199 · raw

@st:Sha256State -> @+len:Nat -> @+q:Nat -> List<&2, U32>

def read512_16 source · line 212 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w14:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w15:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_15 source · line 215 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w14:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_14 source · line 222 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_13 source · line 229 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_12 source · line 236 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_11 source · line 243 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_10 source · line 250 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_9 source · line 257 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_8 source · line 264 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_7 source · line 271 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_6 source · line 278 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_5 source · line 285 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_4 source · line 292 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_3 source · line 299 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_2 source · line 306 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_1 source · line 313 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.Lane -> Read512

def read512_0 source · line 320 · raw

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

def absorb512 source · line 331 · raw

@fuel:Nat -> @r:Read512 -> @orig:List<&2, U32> -> @+q:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha512/types.State -> Sha512State

Compress every whole block (fuel bounds the count: any fuel >= the number of blocks reads them all; fewer leaves the rest buffered, still correct). The chaining state and the unread bytes; orig is the list the read r started at. q is the algorithm's round parameter (64n), kept a variable for the proofs.

def step512 source · line 340 · raw

@st:Sha512State -> @xs:List<&2, U32> -> @+q:Nat -> Sha512State

def finish512 source · line 346 · raw

@st:Sha512State -> @+len:Nat -> @+q:Nat -> List<&2, U32>

def read3_17 source · line 359 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w14:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w15:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w16:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_16 source · line 362 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w14:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w15:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_15 source · line 369 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w14:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_14 source · line 376 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w13:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_13 source · line 383 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w12:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_12 source · line 390 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w11:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_11 source · line 397 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w10:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_10 source · line 404 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w9:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_9 source · line 411 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w8:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_8 source · line 418 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w7:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_7 source · line 425 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w6:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_6 source · line 432 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w5:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_5 source · line 439 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w4:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_4 source · line 446 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w3:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_3 source · line 453 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w2:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_2 source · line 460 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> @w1:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_1 source · line 467 · raw

@bytes:List<&2, U32> -> @w0:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.Lane -> Read3

def read3_0 source · line 474 · raw

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

def absorb3 source · line 485 · raw

@fuel:Nat -> @r:Read3 -> @orig:List<&2, U32> -> @+q:Nat -> @s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/keccak/types.State -> Sha3State

Compress every whole block (fuel bounds the count: any fuel >= the number of blocks reads them all; fewer leaves the rest buffered, still correct). The chaining state and the unread bytes; orig is the list the read r started at. q is the algorithm's round parameter (24n), kept a variable for the proofs.

def step3 source · line 494 · raw

@st:Sha3State -> @xs:List<&2, U32> -> @+q:Nat -> Sha3State

def finish3 source · line 500 · raw

@st:Sha3State -> @+len:Nat -> @+q:Nat -> List<&2, U32>

def new_sha256 source · line 507 · raw

Hasher

def new_sha512 source · line 510 · raw

Hasher

def new_sha3_256 source · line 513 · raw

Hasher

def update source · line 516 · raw

@h:Hasher -> @+bytes:List<&2, U32> -> Hasher

def fold source · line 525 · raw

@chunks:List<&2, List<&2, U32>> -> @h:Hasher -> Hasher

def update_all source · line 532 · raw

@h:Hasher -> @chunks:List<&2, List<&2, U32>> -> Hasher

def digest source · line 535 · raw

@h:Hasher -> List<&2, U32>