Documentation

VCVio.EvalDist.BitVec

Evaluation Distributions of Computations with BitVec #

File for lemmas about evalDist and support involving BitVec.

@[simp]
theorem probOutput_ofFin_map {m : TypeType u_1} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {n : } (mx : m (Fin (2 ^ n))) (x : BitVec n) :
@[simp]
theorem probOutput_bitVec_toFin_map {m : TypeType u_1} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {n : } (mx : m (BitVec n)) (x : Fin (2 ^ n)) :
Pr[=x | BitVec.toFin <$> mx] = Pr[={ toFin := x } | mx]