Distribution Semantics for Computations with Bit Vectors

This file contains lemmas for probEvent and probOutput of computations involving BitVec.

@[simp]

theorem OracleComp.probOutput_bitVec_ofFin_map {ι : Type} {spec : OracleSpec ι} [spec.FiniteRange] {n : ℕ} (oa : OracleComp spec (Fin (2 ^ n))) (x : BitVec n) : [=x|BitVec.ofFin <$> oa] = [=x.toFin|oa]

@[simp]

theorem OracleComp.probOutput_bitVec_toFin_map {ι : Type} {spec : OracleSpec ι} [spec.FiniteRange] {n : ℕ} (oa : OracleComp spec (BitVec n)) (x : Fin (2 ^ n)) : [=x|BitVec.toFin <$> oa] = [={ toFin := x }|oa]

instance OracleComp.instSelectableTypeBitVec (n : ℕ) : SelectableType (BitVec n)

Choose a random bit-vector by converting a random number in number between 0 and 2 ^ n

Equations

• OracleComp.instSelectableTypeBitVec n = { selectElem := BitVec.ofFin <$> ($ᵗFin (2 ^ n)), mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯, probFailure_selectElem := ⋯ }