Documentation

VCVio.EvalDist.BitVec

Evaluation Distributions of Computations with BitVec #

Lemmas about probOutput involving BitVec, generic over any monad m with [MonadLiftT m SPMF].

The SampleableType (BitVec n) instance is defined in VCVio.OracleComp.Constructions.SampleableType.

source
@[simp]
theorem probOutput_ofFin_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [EvalDistCompatible m] {n : ℕ} (mx : m (Fin (2 ^ n))) (x : BitVec n) :
Pr[= x | BitVec.ofFin <$> mx] = Pr[= x.toFin | mx]
source
@[simp]
theorem probOutput_bitVec_toFin_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [EvalDistCompatible m] {n : ℕ} (mx : m (BitVec n)) (x : Fin (2 ^ n)) :
Pr[= x | BitVec.toFin <$> mx] = Pr[= { toFin := x } | mx]
source
@[simp]
theorem probOutput_xor_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {n : ℕ} (mx : m (BitVec n)) (x y : BitVec n) :
Pr[= y | (fun (x_1 : BitVec n) => x ^^^ x_1) <$> mx] = Pr[= x ^^^ y | mx]