~/bend-docscommunity

proofs/crypto/chacha/xchacha.bend checks

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

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 ./core.bend as K
import ./stream.bend as T

Laws

law hbody_correct provedsource · line 16 · raw

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

law hchacha_rounds_correct provedsource · line 34 · raw

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

law hchacha20_correct provedsource · line 45 · raw

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

law xencrypt_correct provedsource · line 53 · raw

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

Definitions

def hout source · line 13 · raw

@+l:List<&2, U32> -> List<&2, U32>

def xenc source · line 60 · raw

@+kb:List<&2, U32> -> @+c:U32 -> @+sub:List<&2, U32> -> @+nn:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>