Deterministic machines inside probabilistic programs

The embedding ignores each coin and never submits a query. With a stateless coin interpretation, it preserves the entire communication state and every oracle's private state. The number of instructions, ordinary tapes and output agree exactly with the upstream deterministic run.

Adapted from the cslib crypto branch's Oracle/Deterministic.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8, for the common machine and typed program interface.

Main definitions

• Turing.MultiTapePTM.ofDeterministic: repeat the deterministic action on both coin branches.

Main results

• Turing.MultiTapePTM.run_interpret_ofDeterministic: preserve joint output and private state.
• Turing.MultiTapePTM.eval_runClosed_ofDeterministic: the closed deterministic run distribution.

noncomputable def Turing.MultiTapePTM.ofDeterministic {k : ℕ} {Symbol State Oracle : Type} (machine : MultiTapeTM k Symbol State) : MultiTapePTM k Symbol State Oracle

Ignore the coin and oracle channels, retaining the deterministic states and ordinary tapes.

theorem Turing.MultiTapePTM.run_interpret_runConfigFrom_ofDeterministic {k : ℕ} {Symbol State Oracle Query OracleState : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeTM k Symbol State) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (coinLaw : PMF Bool) (hcoin : ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) coinLaw) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (s : OracleState) : (Cslib.OracleComp.interpret oracle ((ofDeterministic machine).runConfigFrom coin query fuel cfg)).run s = PMF.pure ({ tapes := MultiTapeTM.runFrom cfg.tapes fuel, channels := cfg.channels }, s)

A deterministic embedding leaves all channels and the oracle's private state unchanged. The coin may have any fixed distribution, provided drawing it has no effect on private state.

theorem Turing.MultiTapePTM.run_interpret_ofDeterministic {k : ℕ} {Symbol State Oracle Query OracleState : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapeTM k Symbol State) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (coinLaw : PMF Bool) (hcoin : ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) coinLaw) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (s : OracleState) : (Cslib.OracleComp.interpret oracle ((ofDeterministic machine).runFrom coin query fuel cfg)).run s = PMF.pure ((MultiTapeTM.runFrom cfg.tapes fuel).output, s)

The output of a deterministic embedding agrees with upstream and leaves private state intact.

theorem Turing.MultiTapePTM.eval_runClosed_ofDeterministic {k : ℕ} {Symbol State : Type} (machine : MultiTapeTM k Symbol State) (fuel : ℕ) (input : List Symbol) : ((ofDeterministic machine).runClosed fuel input).eval = PMF.pure (MultiTapeTM.runFrom (machine.initCfg input) fuel).output

Closed fair-coin execution of a deterministic embedding has a point-mass output distribution.