src/crypto/chacha/chacha20.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/chacha/chacha20.bend as Chacha20

2 imports

import Base
import ./core.bend as C

Types

type Key source · line 18 · raw

Data

K

@k0:U32 -> @k1:U32 -> @k2:U32 -> @k3:U32 -> @k4:U32 -> @k5:U32 -> @k6:U32 -> @k7:U32 -> Key

type Nonce source · line 21 · raw

Data

N
```
@n0:U32 -> @n1:U32 -> @n2:U32 -> Nonce
```

Definitions

def word source · line 26 · raw

@b0:U32 -> @b1:U32 -> @b2:U32 -> @b3:U32 -> U32

def words source · line 30 · raw

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

def at source · line 35 · raw

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

def key_words source · line 41 · raw

@+ws:List<&2, U32> -> Key

def nonce_words source · line 44 · raw

@+ws:List<&2, U32> -> Nonce

def key source · line 47 · raw

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

def nonce source · line 50 · raw

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

def state source · line 55 · raw

@k:Key -> @counter:U32 -> @n:Nonce -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/chacha/core.State

def keystream source · line 61 · raw

@+r:Nat -> @k:Key -> @counter:U32 -> @n:Nonce -> List<&2, U32>

The 64 keystream bytes of block counter, with r double rounds.

def xor_front source · line 67 · raw

@ks:List<&2, U32> -> @xs:List<&2, U32> -> List<&2, U32>

XOR the keystream onto the front of xs, as far as both go.

def skip source · line 72 · raw

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

def stream source · line 80 · raw

@fuel:Nat -> @+xs:List<&2, U32> -> @+r:Nat -> @+k:Key -> @+counter:U32 -> @+n:Nonce -> List<&2, U32>

Blocks of 64 bytes, block j under counter + j; fuel bounds the number of blocks (the length of xs is enough).

def encrypt_rounds source · line 88 · raw

@+r:Nat -> @key_bytes:List<&2, U32> -> @counter:U32 -> @nonce_bytes:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>

def block_body source · line 91 · raw

@+r:Nat -> @key_bytes:List<&2, U32> -> @counter:U32 -> @nonce_bytes:List<&2, U32> -> List<&2, U32>

def block_rounds source · line 97 · raw

@+r:Nat -> @key_bytes:List<&2, U32> -> @counter:U32 -> @nonce_bytes:List<&2, U32> -> List<&2, U32>

The block function entered through a match on the key's first cell: both arms are block_body; with a symbolic key the proof checker leaves the call unevaluated instead of unrolling the rounds when it compares types.

def hstate source · line 104 · raw

@k:Key -> @+ws:List<&2, U32> -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/chacha/core.State

def hchacha_body source · line 109 · raw

@+r:Nat -> @key_bytes:List<&2, U32> -> @nonce_bytes:List<&2, U32> -> List<&2, U32>

def hchacha_rounds source · line 112 · raw

@+r:Nat -> @key_bytes:List<&2, U32> -> @nonce_bytes:List<&2, U32> -> List<&2, U32>

def hchacha20_unchecked source · line 117 · raw

@key_bytes:List<&2, U32> -> @nonce_bytes:List<&2, U32> -> List<&2, U32>

def take source · line 120 · raw

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

def xencrypt_unchecked source · line 128 · raw

@key_bytes:List<&2, U32> -> @counter:U32 -> @+nonce_bytes:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>

XChaCha20: ChaCha20 under the HChaCha20 subkey of nonce[0..16], with the nonce 0x00000000 || nonce[16..24].

def has_length source · line 134 · raw

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

def valid source · line 137 · raw

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

def when source · line 140 · raw

@ok:Bool -> @x:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def chacha20_block source · line 147 · raw

@+key_bytes:List<&2, U32> -> @counter:U32 -> @+nonce_bytes:List<&2, U32> -> Maybe<&2, List<&2, U32>>

chacha20_block(key, counter, nonce): 64 bytes, or None unless the key has 32 bytes and the nonce 12.

def chacha20 source · line 152 · raw

@+key_bytes:List<&2, U32> -> @counter:U32 -> @+nonce_bytes:List<&2, U32> -> @+plaintext:List<&2, U32> -> Maybe<&2, List<&2, U32>>

chacha20_encrypt(key, counter, nonce, plaintext) (encryption and decryption are the same operation).

def hchacha20 source · line 156 · raw

@+key_bytes:List<&2, U32> -> @+nonce_bytes:List<&2, U32> -> Maybe<&2, List<&2, U32>>

HChaCha20(key, nonce): the 32-byte subkey, or None unless 32 and 16 bytes.

def xchacha20 source · line 160 · raw

@+key_bytes:List<&2, U32> -> @counter:U32 -> @+nonce_bytes:List<&2, U32> -> @+plaintext:List<&2, U32> -> Maybe<&2, List<&2, U32>>

XChaCha20 with a 24-byte nonce.