spec/crypto/chacha.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/chacha.bend as Chacha
1 import
import Base
Definitions
def get source · line 19 · raw
@xs:List<&2, U32> -> @i:Nat -> U32
Element i of a list, 0 past its end.
def put source · line 26 · raw
@xs:List<&2, U32> -> @i:Nat -> @y:U32 -> List<&2, U32>
The list with element i replaced (unchanged past its end).
def rotl source · line 35 · raw
@+x:U32 -> @+n:Nat -> U32
x <<< n: rotation of a 32-bit word left by n bits (0 < n < 32).
def quarter source · line 43 · raw
@+s:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> List<&2, U32>
2.2: QUARTERROUND(a, b, c, d) applied to the state at those positions: a += b; d ^= a; d <<<= 16; c += d; b ^= c; b <<<= 12; a += b; d ^= a; d <<<= 8; c += d; b ^= c; b <<<= 7;
def inner_block source · line 57 · raw
@s:List<&2, U32> -> List<&2, U32>
inner_block: four column rounds, then four diagonal rounds.
def inner_blocks source · line 68 · raw
@n:Nat -> @s:List<&2, U32> -> List<&2, U32>
n applications of inner_block (ChaCha20: n = 10, twenty rounds).
def word source · line 74 · raw
@b0:U32 -> @b1:U32 -> @b2:U32 -> @b3:U32 -> U32
A little-endian word from the low 8 bits of four bytes.
def words source · line 79 · raw
@bytes:List<&2, U32> -> List<&2, U32>
The words of a byte list, four bytes each (a partial tail is dropped).
def octets source · line 85 · raw
@+w:U32 -> List<&2, U32>
The four little-endian bytes of a word.
def serialize source · line 89 · raw
@ws:List<&2, U32> -> List<&2, U32>
def constants source · line 95 · raw
List<&2, U32>
"expa" "nd 3" "2-by" "te k"
def state source · line 101 · raw
@+k:List<&2, U32> -> @counter:U32 -> @+n:List<&2, U32> -> List<&2, U32>
The initial state: constants, key (eight words), block counter, nonce (three words). Missing key or nonce words read as 0 (the public API rejects other lengths before this is reached).
def add_words source · line 106 · raw
@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>
def block_body source · line 113 · raw
@+n:Nat -> @+key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> List<&2, U32>
chacha20_block with n double rounds: working state after n inner blocks, added to the initial state, serialized little-endian (64 bytes).
def block_rounds source · line 120 · raw
@+n:Nat -> @key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> List<&2, U32>
The same, entered through a match on the key's first cell. Both arms are block_body; the match only keeps the proof checker from evaluating the rounds on a symbolic key (it compares types by evaluating them).
def block source · line 125 · raw
@+key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> List<&2, U32>
def prefix source · line 131 · raw
@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>
The first n bytes of a list, and the rest.
def suffix source · line 137 · raw
@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>
def blocks source · line 146 · raw
@fuel:Nat -> @+xs:List<&2, U32> -> List<&2, List<&2, U32>>
The plaintext cut into 64-byte blocks; the last one may be shorter (and there is none for the empty plaintext). fuel bounds the number of blocks (the length of the plaintext is enough).
def xor_bytes source · line 153 · raw
@xs:List<&2, U32> -> @ks:List<&2, U32> -> List<&2, U32>
Byte-wise XOR of a block with the keystream (as long as the block).
def encrypt_blocks source · line 159 · raw
@bs:List<&2, List<&2, U32>> -> @+n:Nat -> @+key:List<&2, U32> -> @+counter:U32 -> @+nonce:List<&2, U32> -> List<&2, U32>
for j = 0 .. : block j is XORed with chacha20_block(key, counter + j, nonce).
def encrypt_rounds source · line 167 · raw
@+n:Nat -> @+key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>
chacha20_encrypt(key, counter, nonce, plaintext) with n double rounds.
def encrypt source · line 170 · raw
@+key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>
def hstate source · line 178 · raw
@+k:List<&2, U32> -> @+n:List<&2, U32> -> List<&2, U32>
HChaCha20 (draft-irtf-cfrg-xchacha-03 section 2.2): the state is set up as for ChaCha20 with the 16-byte nonce in words 12..15; after twenty rounds (no feed-forward) words 0..3 and 12..15 are the 32-byte subkey.
def hchacha_body source · line 183 · raw
@+n:Nat -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> List<&2, U32>
def hchacha_rounds source · line 188 · raw
@+n:Nat -> @key:List<&2, U32> -> @+nonce:List<&2, U32> -> List<&2, U32>
Entered through a match on the key, as block_rounds.
def hchacha20 source · line 193 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> List<&2, U32>
def xsubkey source · line 198 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> List<&2, U32>
Section 2.3: XChaCha20 is ChaCha20 under the HChaCha20 subkey of the first 16 nonce bytes, with the nonce 0x00000000 || nonce[16..24].
def xnonce source · line 201 · raw
@+nonce:List<&2, U32> -> List<&2, U32>
def xencrypt source · line 204 · raw
@+key:List<&2, U32> -> @counter:U32 -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>