Tidy combinators for probabilistic oracle machines

This module lifts the deterministic tidy-machine combinators (comp, append, and branch/ite) to MultiTapePTM specifications in RunsWords and ComputesTidily, re-exporting the foundational phase specifications (RunsWords) and word-redirection combinators (Tidy/Redirect). Every combinator preserves the exact joint distribution of tape words, emitted output and external oracle state, and maintains clean query buffers at phase boundaries.

Main definitions

• Turing.MultiTapePTM.tidyComp: sequential composition of tidy probabilistic machines.
• Turing.MultiTapePTM.appendPTM: concatenate the outputs of two tidy probabilistic machines.
• Turing.MultiTapePTM.branch: branch on whether a work tape is blank without executing the unselected branch.
• Turing.MultiTapePTM.itePTM: tidy case distinction on a work tape word.

Main results

• Turing.MultiTapePTM.ComputesTidily.comp: tidy sequential composition.
• Turing.MultiTapePTM.ComputesTidily.append: tidy output concatenation.
• Turing.MultiTapePTM.ComputesTidily.ite: tidy conditional execution.

References

Adapts the deterministic tidy-machine combinators of Christian Reitwiessner's crei:crei/tidy-universal @7f7c0696 (Combinators/Comp, Combinators/Append, and Combinators/Ite) to the probabilistic oracle machines of the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

Composing tidy probabilistic machines (tidyComp and appendPTM)

noncomputable def Turing.MultiTapePTM.tidyComp {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} (tm₂ : MultiTapePTM k₂ Bool State₂ Operation) (tm₁ : MultiTapePTM k₁ Bool State₁ Operation) (mark : Bool) : MultiTapePTM (max k₁ k₂ + 2) Bool ((State₁ ⊕ MultiTapeTM.RewindWorkState) ⊕ (MultiTapeTM.MarkWorkState ⊕ State₂ ⊕ MultiTapeTM.MarkWorkState) ⊕ Unit ⊕ MultiTapeTM.RewindWorkState) Operation

Run tm₁ with its output written to work tape Fin.natAdd (max k₁ k₂) 0, then run tm₂ reading its input from that tape (using mark on the last work tape), and finally clear that tape.

theorem Turing.MultiTapePTM.ComputesTidily.comp_of_le {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {tm₁ : MultiTapePTM k₁ Bool State₁ Operation} {tm₂ : MultiTapePTM k₂ Bool State₂ Operation} {t₁ t₂ l : ℕ} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} {prog₂ : List Bool → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (mark : Bool) (h₁ : tm₁.ComputesTidily x t₁ prog₁) (hl : ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) (w : List Bool) (s' : OracleState), (w, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → w.length ≤ l) (h₂ : ∀ (w : List Bool) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (w, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → tm₂.ComputesTidily w t₂ (prog₂ w)) : (tm₂.tidyComp tm₁ mark).ComputesTidily x (t₁ + t₂ + 4 * l + 9) (prog₁ >>= prog₂)

If tm₁ computes prog₁ tidily on x in t₁ steps with outputs of length at most l, and tm₂ computes prog₂ w tidily on every supported output w of prog₁ in t₂ steps, then tm₂.tidyComp tm₁ mark computes prog₁ >>= prog₂ tidily on x in t₁ + t₂ + 4 * l + 9 steps.

theorem Turing.MultiTapePTM.ComputesTidily.comp {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {tm₁ : MultiTapePTM k₁ Bool State₁ Operation} {tm₂ : MultiTapePTM k₂ Bool State₂ Operation} {t₁ t₂ : ℕ} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} {prog₂ : List Bool → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (mark : Bool) (h₁ : tm₁.ComputesTidily x t₁ prog₁) (h₂ : ∀ (w : List Bool) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (w, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → tm₂.ComputesTidily w t₂ (prog₂ w)) : (tm₂.tidyComp tm₁ mark).ComputesTidily x (5 * t₁ + t₂ + 9) (prog₁ >>= prog₂)

Unconditional tidy sequential composition using h₁.length_output_le.

def Turing.MultiTapePTM.appendPTM {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} (tm₁ : MultiTapePTM k₁ Bool State₁ Operation) (tm₂ : MultiTapePTM k₂ Bool State₂ Operation) : MultiTapePTM (max k₁ k₂) Bool (State₁ ⊕ State₂) Operation

Run tm₁ and then tm₂ on the same input, both padded to max k₁ k₂ work tapes.

theorem Turing.MultiTapePTM.ComputesTidily.append {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {tm₁ : MultiTapePTM k₁ Bool State₁ Operation} {tm₂ : MultiTapePTM k₂ Bool State₂ Operation} {t₁ t₂ : ℕ} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} {prog₂ : List Bool → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (h₁ : tm₁.ComputesTidily x t₁ prog₁) (h₂ : ∀ (w₁ : List Bool) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (w₁, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → tm₂.ComputesTidily x t₂ (prog₂ w₁)) : (tm₁.appendPTM tm₂).ComputesTidily x (t₁ + t₂) do let w₁ ← prog₁ (fun (w₂ : List Bool) => w₁ ++ w₂) <$> prog₂ w₁

If tm₁ computes prog₁ tidily in t₁ steps and tm₂ computes prog₂ w₁ tidily in t₂ steps on the same input x, then appendPTM tm₁ tm₂ computes prog₁ >>= fun w₁ => (fun w₂ => w₁ ++ w₂) <$> prog₂ w₁ tidily in t₁ + t₂ steps.

theorem Turing.MultiTapePTM.ComputesTidily.prefix {k₁ k₂ : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {prep : MultiTapeTM k₁ Bool State₁} {source : MultiTapePTM k₂ Bool State₂ Operation} {pre : List Bool} {t₁ s₁ t₂ : ℕ} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (hprep : prep.ComputesTidilyInTimeAndSpace x pre t₁ s₁) (hsource : source.ComputesTidily x t₂ program) : ((ofDeterministic prep).appendPTM source).ComputesTidily x (t₁ + t₂) ((fun (y : List Bool) => pre ++ y) <$> program)

Prepend a deterministically computed prefix word before a tidy probabilistic computation.

Conditional branching (branch and itePTM)

def Turing.MultiTapePTM.branch {k : ℕ} {State₁ State₂ Operation : Type} (i : Fin k) (tm₁ : MultiTapePTM k Bool State₁ Operation) (tm₂ : MultiTapePTM k Bool State₂ Operation) : MultiTapePTM k Bool (Option (State₁ ⊕ State₂)) Operation

Read the cell under the head of work tape i, moving no head and writing nothing, then run tm₁ if the cell is not blank and tm₂ if it is.

theorem Turing.MultiTapePTM.Branch.runOracleConfigFrom_mapState {k : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {i : Fin k} {tm₁ : MultiTapePTM k Bool State₁ Operation} {tm₂ : MultiTapePTM k Bool State₂ Operation} {S : Type} {tm : MultiTapePTM k Bool S Operation} {f : S → Option (State₁ ⊕ State₂)} (htr : ∀ (q : S) (inp : Option Bool) (work : Fin k → Option Bool) (answer : Operation → Option Bool) (bit : Bool), (branch i tm₁ tm₂).tr (f q) inp work answer bit = MultiTapeMachine.Action.mapState f (tm.tr q inp work answer bit)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Bool S Operation x) : (branch i tm₁ tm₂).runOracleConfigFrom fuel (MultiTapeMachine.Config.mapState f cfg) = MultiTapeMachine.Config.mapState f <$> tm.runOracleConfigFrom fuel cfg

If branch i tm₁ tm₂ acts on f q by mapping tm's actions through f, then its clocked run from Config.mapState f cfg maps tm's clocked run through Config.mapState f.

theorem Turing.MultiTapePTM.RunsWords.branch_nil {k : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) (tm₁ : MultiTapePTM k Bool State₁ Operation) {tm₂ : MultiTapePTM k Bool State₂ Operation} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {t₂ : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (hi : ws₀ i = []) (h₂ : tm₂.RunsWords x ws₀ out₀ t₂ program ws₁ emit) : (branch i tm₁ tm₂).RunsWords x ws₀ out₀ (t₂ + 1) program ws₁ emit

When tape i is empty, branch i tm₁ tm₂ transitions in 1 step to tm₂ and never executes tm₁.

theorem Turing.MultiTapePTM.RunsWords.branch_ne_nil {k : ℕ} {State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) {tm₁ : MultiTapePTM k Bool State₁ Operation} (tm₂ : MultiTapePTM k Bool State₂ Operation) {ws₀ : Fin k → List Bool} {out₀ : List Bool} {t₁ : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (hi : ws₀ i ≠ []) (h₁ : tm₁.RunsWords x ws₀ out₀ t₁ program ws₁ emit) : (branch i tm₁ tm₂).RunsWords x ws₀ out₀ (t₁ + 1) program ws₁ emit

When tape i is non-empty, branch i tm₁ tm₂ transitions in 1 step to tm₁ and never executes tm₂.

noncomputable def Turing.MultiTapePTM.itePTM {k₀ k₁ k₂ : ℕ} {State₀ State₁ State₂ Operation : Type} (tmc : MultiTapePTM k₀ Bool State₀ Operation) (tm₁ : MultiTapePTM k₁ Bool State₁ Operation) (tm₂ : MultiTapePTM k₂ Bool State₂ Operation) : MultiTapePTM (max k₀ (max k₁ k₂) + 1) Bool ((State₀ ⊕ MultiTapeTM.RewindWorkState) ⊕ Option (State₁ ⊕ State₂) ⊕ Unit ⊕ MultiTapeTM.RewindWorkState) Operation

Run tmc with its output on a new last work tape, then tm₁ if that word is non-empty and tm₂ otherwise, and clear the tape.

theorem Turing.MultiTapePTM.ComputesTidily.ite {k₀ k₁ k₂ : ℕ} {State₀ State₁ State₂ Operation : Type} {x : List Bool} [DecidableEq Operation] {tmc : MultiTapePTM k₀ Bool State₀ Operation} {tm₁ : MultiTapePTM k₁ Bool State₁ Operation} {tm₂ : MultiTapePTM k₂ Bool State₂ Operation} {w : List Bool} {tc t₁ t₂ : ℕ} {prog₁ prog₂ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (hc : tmc.ComputesTidily x tc (pure w)) (h₁ : w ≠ [] → tm₁.ComputesTidily x t₁ prog₁) (h₂ : w = [] → tm₂.ComputesTidily x t₂ prog₂) : (tmc.itePTM tm₁ tm₂).ComputesTidily x ((tc + if w = [] then t₂ else t₁) + 4 * w.length + 6) (if w = [] then prog₂ else prog₁)

If tmc computes the test word w from x tidily, tm₁ computes prog₁ tidily when w ≠ [] and tm₂ computes prog₂ tidily when w = [], then itePTM tmc tm₁ tm₂ computes if w = [] then prog₂ else prog₁ tidily within the bounds of tmc plus those of the active branch, never executing the unselected branch.