~/bend-docscommunity

src/crypto/keccak/keccak.bend checks

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/keccak.bend as Keccak

4 imports
import Base
import ./types.bend as T
import ./lane.bend as L
import ./permutation.bend as P

Definitions

def mix source · line 6 · raw

@s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @w31:U32 -> @w32:U32 -> @w33:U32 -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def read33 source · line 11 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @w31:U32 -> @w32:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read32 source · line 15 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @w31:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read31 source · line 19 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read30 source · line 23 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read29 source · line 27 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read28 source · line 31 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read27 source · line 35 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read26 source · line 39 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read25 source · line 43 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read24 source · line 47 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read23 source · line 51 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read22 source · line 55 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read21 source · line 59 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read20 source · line 63 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read19 source · line 67 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read18 source · line 71 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read17 source · line 75 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read16 source · line 79 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read15 source · line 83 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read14 source · line 87 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read13 source · line 91 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read12 source · line 95 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read11 source · line 99 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read10 source · line 103 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read9 source · line 107 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read8 source · line 111 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read7 source · line 115 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read6 source · line 119 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read5 source · line 123 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read4 source · line 127 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read3 source · line 131 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read2 source · line 135 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read1 source · line 139 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def read0 source · line 143 · raw

@+round_count:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def absorb source · line 147 · raw

@+round_count:Nat -> @a:Array<U32> -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State)

def partial source · line 151 · raw

@w:U32 -> @delta:Nat -> U32

Little-endian Keccak pad10*1, domain suffix 0x01.

def pad_choose source · line 159 · raw

@c:Cmp -> @w:U32 -> @delta:Nat -> U32

def pad_word source · line 165 · raw

@w:U32 -> @+pos:Nat -> @+remain:Nat -> U32

def pad33 source · line 168 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @w31:U32 -> @w32:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad32 source · line 172 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @w31:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad31 source · line 176 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @w30:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad30 source · line 180 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @w29:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad29 source · line 184 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @w28:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad28 source · line 188 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @w27:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad27 source · line 192 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @w26:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad26 source · line 196 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @w25:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad25 source · line 200 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @w24:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad24 source · line 204 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @w23:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad23 source · line 208 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @w22:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad22 source · line 212 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @w21:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad21 source · line 216 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @w20:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad20 source · line 220 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @w19:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad19 source · line 224 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @w18:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad18 source · line 228 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @w17:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad17 source · line 232 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @w16:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad16 source · line 236 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad15 source · line 240 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad14 source · line 244 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad13 source · line 248 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @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 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad12 source · line 252 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @w11:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad11 source · line 256 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @w10:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad10 source · line 260 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @w9:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad9 source · line 264 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @w8:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad8 source · line 268 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @w7:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad7 source · line 272 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @w6:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad6 source · line 276 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @w5:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad5 source · line 280 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @w4:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad4 source · line 284 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @w3:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad3 source · line 288 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @w2:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad2 source · line 292 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @w1:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad1 source · line 296 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @w0:U32 -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def pad0 source · line 300 · raw

@+round_count:Nat -> @+remain:Nat -> @+index:U32 -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> @pair:Pair(Array<U32>, U32) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def finish source · line 304 · raw

@+round_count:Nat -> @a:Array<U32> -> @+index:U32 -> @remain:Nat -> @s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def blocks source · line 307 · raw

@+round_count:Nat -> @n:Nat -> @+index:U32 -> @remain:Nat -> @pair:Pair(Array<U32>, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State) -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def unchecked source · line 312 · raw

@+round_count:Nat -> @a:Array<U32> -> @+length:Nat -> 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State

def digest source · line 315 · raw

@s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.State -> Array<U32>

def checked source · line 329 · raw

@+round_count:Nat -> @valid:Bool -> @a:Array<U32> -> @length:Nat -> Maybe<&1, Array<U32>>

def sized source · line 334 · raw

@+round_count:Nat -> @+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&1, Array<U32>>

def keccak256_rounds source · line 338 · raw

@+round_count:Nat -> @a:Array<U32> -> @length:Nat -> Maybe<&1, Array<U32>>

def keccak256 source · line 342 · raw

@a:Array<U32> -> @length:Nat -> Maybe<&1, Array<U32>>