proofs/crypto/chacha/stream.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as Stream

6 imports

import Base
import ../../../src/crypto/chacha/core.bend as C
import ../../../src/crypto/chacha/chacha20.bend as I
import ../../../spec/crypto/chacha.bend as R
import ../../lib/nat.bend as N
import ./core.bend as K

Laws

law words_eq provedsource · line 14 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.words(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.words(xs) : List<&2, U32>}

law key_eq provedsource · line 29 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key_words(ws) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.K{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 3n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 4n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 5n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 6n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 7n)} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.Key}

law nonce_eq provedsource · line 45 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce_words(ws) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.N{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 2n)} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.Nonce}

law hnonce_eq provedsource · line 57 · raw

@+ws:List<&2, U32> -> {[0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.at(ws, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.at(ws, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.at(ws, 2n), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.at(ws, 3n)] == [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.get(ws, 3n)] : List<&2, U32>}

The four HChaCha20 nonce words.

law state_eq provedsource · line 71 · raw

@+ks:List<&2, U32> -> @+c:U32 -> @+ns:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/core.vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.state(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key_words(ks), c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce_words(ns))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.state(ks, c, ns) : List<&2, U32>}

law hstate_eq provedsource · line 84 · raw

@+ks:List<&2, U32> -> @+ns:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/core.vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.hstate(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key_words(ks), ns)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.hstate(ks, ns) : List<&2, U32>}

law body_correct provedsource · line 107 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.keystream(r, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key(kb), c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce(nb)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_body(r, kb, c, nb) : List<&2, U32>}

law keystream_correct provedsource · line 127 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.keystream(r, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key(kb), c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce(nb)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, kb, c, nb) : List<&2, U32>}

law block_rounds_correct provedsource · line 139 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.block_rounds(r, kb, c, nb) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, kb, c, nb) : List<&2, U32>}

law bytes_length provedsource · line 152 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.State -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.bytes(s)) == 64n : Nat}

64 keystream bytes.

law block_length provedsource · line 160 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, kb, c, nb)) == 64n : Nat}

law xor_front_eq provedsource · line 173 · raw

@+ks:List<&2, U32> -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xor_front(ks, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.prefix(List.length(&2, U32, ks), xs), ks) : List<&2, U32>}

law skip_eq provedsource · line 187 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.skip(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.suffix(n, xs) : List<&2, U32>}

law take_eq provedsource · line 198 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.take(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.prefix(n, xs) : List<&2, U32>}

law front_correct provedsource · line 212 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.xor_front(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.keystream(r, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key(kb), c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce(nb)), xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.xor_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.prefix(64n, xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.block_rounds(r, kb, c, nb)) : List<&2, U32>}

One block of the stream: the XORed front is the spec's.

law stream_correct provedsource · line 228 · raw

@+fuel:Nat -> @+xs:List<&2, U32> -> @+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.stream(fuel, xs, r, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.key(kb), c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.nonce(nb)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_blocks(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.blocks(fuel, xs), r, kb, c, nb) : List<&2, U32>}

law encrypt_correct provedsource · line 254 · raw

@+r:Nat -> @+kb:List<&2, U32> -> @+c:U32 -> @+nb:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.encrypt_rounds(r, kb, c, nb, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.encrypt_rounds(r, kb, c, nb, pt) : List<&2, U32>}

Definitions

def hsl source · line 89 · raw

@+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @l:List<&2, U32> -> List<&2, U32>

def sblock source · line 114 · raw

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