proofs/crypto/chacha/proof.bend checks

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

7 imports

import Base
import ../../../src/crypto/chacha/chacha20.bend as I
import ../../../spec/crypto/chacha.bend as R
import ./laws.bend as Laws
import ./stream.bend as T
import ./xchacha.bend as X
import ./involution.bend as V

Laws

law when_true provedsource · line 31 · raw

@+ok:Bool -> @+x:List<&2, U32> -> @+h:{ok == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.when(ok, x) == Some{x} : Maybe<&2, List<&2, U32>>}

law when_false provedsource · line 41 · raw

@+ok:Bool -> @+x:List<&2, U32> -> @+h:{ok == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.when(ok, x) == None{} : Maybe<&2, List<&2, U32>>}

law valid_true provedsource · line 51 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+n:Nat -> @+hk:{List.length(&2, U32, key) == 32n : Nat} -> @+hn:{List.length(&2, U32, nonce) == n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.valid(key, nonce, n) == True{} : Bool}

Definitions

def is_eq_self source · line 59 · raw

@+n:Nat -> {Nat.is_eq(n, n) == True{} : Bool}