Skip to content

refactor(probabilistic): state the oracle-program core with OracleComp.sumHandler #2201

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 3 commits into from
Nov 2, 2026
Merged

refactor(probabilistic): state the oracle-program core with OracleComp.sumHandler #2201

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c419ef9
refactor(probabilistic): state the oracle-program core with OracleCom…
SamuelSchlesinger Nov 1, 2026
a9abcea
refactor(crypto): migrate the remaining Crypto clients to OracleComp.…
SamuelSchlesinger Nov 1, 2026
40e94a9
Merge remote-tracking branch 'origin/main' into refactor/oraclecomp-s…
SamuelSchlesinger Nov 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Complexity/Computability/Complexity/Classes/IP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ interacts with `P` starting from the prover state `s`. Private coins are fresh f
noncomputable def run (program : WordOracleComp Operation α) (s : P.State) :
PMF (α × P.State) :=
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) P.respond)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) P.respond)
program).run s

/-- `Prover.run` is the run against the prover as a stateful oracle with word queries and
Expand Down
8 changes: 4 additions & 4 deletions Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ variable {S : Type} (oracle : Operation × List Bool → StateT S PMF (List Bool

/-- The handler of the private coins and of the prover `o`. -/
local notation "handler" o =>
ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) o
OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) o

/-- An instruction with a fixed coin makes the requests of `coinStep`. -/
private theorem run_interpret_finiteStep_pure (t : ℕ)
Expand Down Expand Up @@ -188,10 +188,10 @@ the programs of fixed coins. -/
theorem acceptProb_eq_sum {V : WordOracleComp Operation Bool} {t : ℕ} {x : List Bool}
(hV : ∀ (S : Type) (oracle : Operation × List Bool → StateT S PMF (List Bool)) s,
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(Turing.MultiTapeTM.encBool <$> V)).run s =
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(M.runOracle t x)).run s)
(P : Prover Operation) :
acceptProb V P =
Expand All @@ -201,7 +201,7 @@ theorem acceptProb_eq_sum {V : WordOracleComp Operation Bool} {t : ℕ} {x : Lis
(hV P.State P.respond P.init)
rw [OracleComp.interpret_map, StateT.run_map, run_interpret_runOracle_eq_coins,
_root_.PMF.monad_map_eq_map, PMF.map_comp] at h
have hl : acceptProb V P = ((OracleComp.interpret (ProbOracleComp.handler
have hl : acceptProb V P = ((OracleComp.interpret (OracleComp.sumHandler
(fun n => StateT.lift (ProbComp.unifOracle n)) P.respond) V).run P.init).map
((fun z => decide (z.1 = [true])) ∘ fun p => (Turing.MultiTapeTM.encBool p.1, p.2))
true := by
Expand Down
4 changes: 2 additions & 2 deletions Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -562,10 +562,10 @@ theorem mem_iff_two_pow_lt_value {V : α → WordOracleComp Unit Bool} {A : Set
{M : MultiTapePTM k Bool Control Unit} {fuel : α → ℕ}
(hV : ∀ a (S : Type) (oracle : Unit × List Bool → StateT S PMF (List Bool)) s,
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(encBool <$> V a)).run s =
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(M.runOracle (fuel a) (enc a))).run s)
(hA : IsInteractiveProof V A (2 / 3) (1 / 3)) (a : α) :
a ∈ A ↔ 2 ^ fuel a < 2 * value (coinFamily M (fuel a) (enc a)) (fuel a) (fuel a) [] := by
Expand Down
4 changes: 2 additions & 2 deletions Complexity/Computability/Complexity/Classes/Oracle/Deterministic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ oracle's state. -/
private theorem run_interpret_interpret_query {σ : Type}
(answer : Operation × List Bool → List Bool)
(program : WordQueryComp Operation β) (s : σ) :
(OracleComp.interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n))
(OracleComp.interpret (OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n))
(fun q s => PMF.pure (answer q, s)))
(OracleComp.interpret ProbOracleComp.query program)).run s =
PMF.pure (OracleComp.interpret (m := Id) answer program, s) := by
Expand Down Expand Up @@ -123,7 +123,7 @@ theorem exists_run_pure_false {program : α → WordQueryComp Operation β}
(c * ((input a).length + 1) ^ d) (machine.initialConfig (input a))
have hmem' : (OracleComp.interpret (m := Id) answer (machine.run (pure false)
(fun op word => OracleComp.query (op, word)) (c * ((input a).length + 1) ^ d) (input a)),
()) ∈ ((OracleComp.interpret (ProbOracleComp.handler
()) ∈ ((OracleComp.interpret (OracleComp.sumHandler
(fun n => StateT.lift (ProbComp.unifOracle n)) (fun q s => PMF.pure (answer q, s)))
(machine.runOracle (c * ((input a).length + 1) ^ d) (input a))).run ()).support := by
simp only [MultiTapePTM.runOracle, MultiTapePTM.run, MultiTapePTM.runFrom,
Expand Down
4 changes: 2 additions & 2 deletions Complexity/Computability/Complexity/Classes/Oracle/Exponential.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,17 +80,17 @@
the full interaction with every shared stateful oracle: `Cslib.Probability.IsOraclePPTOn` with the
polynomial clock replaced by `2 ^ O(n)`. The oracle's computation is external; request
construction and reply access are ordinary machine work. -/
def IsOracleExpTimeOn {Operation α β : Type} [DecidableEq Operation]

Check notice on line 83 in Complexity/Computability/Complexity/Classes/Oracle/Exponential.lean

View workflow job for this annotation

GitHub Actions / ci-checks

Possible parallel definition 

`Cslib.Probability.IsOracleExpTimeOn` and `Cslib.Probability.IsOraclePPTOn` (Complexity/Computability/Probabilistic/Oracle.lean:63) share a 367-node subterm, 46% of the smaller body, built from `PMF`, `StateT.run`, `Cslib.OracleComp.interpret`, `Sum`, `Cslib.OracleSpec.sum`, `StateT`. Advisory only; see the job summary.
(input : α ↪ List Bool) (output : β ↪ List Bool)
(program : α → WordOracleComp Operation β) : Prop :=
Finite Operation ∧ ∃ (k : ℕ) (Control : Type) (_ : Finite Control)
(machine : Turing.MultiTapePTM k Bool Control Operation) (c d : ℕ),
∀ a (State : Type) (oracle : Operation × List Bool → StateT State PMF (List Bool)) s,
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(output <$> program a)).run s =
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(machine.runOracle (c * 2 ^ (d * (input a).length)) (input a))).run s

namespace IsOracleExpTimeOn
Expand Down
2 changes: 1 addition & 1 deletion Complexity/Computability/Complexity/Classes/Oracle/Monotone.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ theorem ComputableInPolyTimeWithOracle.of_polyTimeReducible {A B : Set (List Boo
fun a State oracle s => ?_
congr 2
rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret]
have hH : (fun q : Unit × List Bool => OracleComp.interpret (ProbOracleComp.handler
have hH : (fun q : Unit × List Bool => OracleComp.interpret (OracleComp.sumHandler
(fun n => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n)))
(fun (q : Unit × List Bool) (_ : Unit) => (fun r => (r, ())) <$> (List.take 1 <$>
ProbOracleComp.query (spec := fun _ : Unit × List Bool => List Bool) ((), g q.2))))
Expand Down
2 changes: 1 addition & 1 deletion Complexity/Computability/Complexity/Classes/Oracle/PP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -404,7 +404,7 @@ theorem PWithSharpPOracle_subset_PWithPPOracle : PWithSharpPOracle enc ⊆ PWith
fun a State oracle s => ?_
congr 2
rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret]
have hH : (fun q : Unit × List Bool => OracleComp.interpret (ProbOracleComp.handler
have hH : (fun q : Unit × List Bool => OracleComp.interpret (OracleComp.sumHandler
(fun n => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n)))
(fun (q : Unit × List Bool) (_ : Unit) => (fun reply => (reply, ())) <$>
OracleComp.interpret ProbOracleComp.query (bitQuery r q)))
Expand Down
2 changes: 1 addition & 1 deletion Complexity/Computability/Interactive/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ variable {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV}

/-- Lift a prover computation into the joint oracles. -/
def liftProver {α : Type} : ProbOracleComp oP α → ProbOracleComp (oP ⊕ₒ oV) α :=
OracleComp.interpret (ProbOracleComp.handler
OracleComp.interpret (OracleComp.sumHandler
(fun n => OracleComp.query (spec := probOracleSpec (oP ⊕ₒ oV)) (.inl n))
(fun q => ProbOracleComp.query (spec := oP ⊕ₒ oV) (.inl q)))

Expand Down
14 changes: 7 additions & 7 deletions Complexity/Computability/Interactive/Plain.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,30 +45,30 @@ open Spec

/-- The law of a program without external oracles: its private coins are fair. -/
noncomputable def plainLaw {α : Type} (p : ProbOracleComp OracleSpec.empty α) : PMF α :=
OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun e => e.elim) p
OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle fun e => e.elim) p

/-- The law of a joint program in the plain model. -/
private noncomputable def runLaw {α : Type}
(p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) : PMF α :=
OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle
OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle
(OracleComp.sumHandler (fun e => e.elim) fun e => e.elim)) p

private theorem plain_eval {α : Type}
(p : ProbOracleComp (OracleSpec.empty ⊕ₒ OracleSpec.empty) α) :
World.plain.eval p = runLaw p := by
have h := OracleComp.run_interpret_stateless (m := PMF) (State := Unit)
(ProbOracleComp.handler ProbComp.unifOracle
(OracleComp.sumHandler ProbComp.unifOracle
(OracleComp.sumHandler (fun e => e.elim) fun e => e.elim)) p ()
have hh : (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n))
have hh : (OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n))
World.plain.impl) =
fun q s => (fun a => (a, s)) <$> ProbOracleComp.handler ProbComp.unifOracle
fun q s => (fun a => (a, s)) <$> OracleComp.sumHandler ProbComp.unifOracle
(OracleComp.sumHandler (fun e => e.elim) fun e => e.elim) q := by
funext q s
rcases q with n | e | e
· rfl
· exact e.elim
· exact e.elim
unfold World.eval ProbOracleComp.runWith
unfold World.eval ProbOracleComp.runWith OracleComp.runWith
erw [hh, h]
exact (PMF.map_comp _ _ _).trans (PMF.map_id _)

Expand All @@ -78,7 +78,7 @@ private theorem runLaw_liftProver {α : Type} (p : ProbOracleComp OracleSpec.emp
congr 1
funext q
rcases q with n | e
· simp [ProbOracleComp.handler]
· simp [OracleComp.sumHandler]
· exact e.elim


Expand Down
10 changes: 5 additions & 5 deletions Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IterateWhile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ theorem RunsWords.iterateWhileRound {tm : MultiTapePTM k Bool State Operation} (
(oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(s : OracleState) (w' : List Bool) (s' : OracleState),
(w', s') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
program).run s).support → w'.length ≤ l) (out₀ : List Bool) :
(tm.iterateWhileRound mark).RunsWords x (words vp v) out₀
(3 * vp.length + 6 * v.length + 16 + (t + l + 6)) program (fun v' => words v v')
Expand Down Expand Up @@ -287,7 +287,7 @@ public theorem ComputesTidily.iterateWhile {tm : MultiTapePTM k Bool State Opera
∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(s s' : OracleState) (w' : List Bool),
(w', s') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(step w)).run s).support → invariant (n + 1) w' ∧ w' ≠ [])
(hlast : ∀ w, invariant r w → tm.ComputesTidily w t (pure []))
(hlength : ∀ n ≤ r, ∀ w, invariant n w → w.length ≤ L) :
Expand All @@ -305,7 +305,7 @@ public theorem ComputesTidily.iterateWhile {tm : MultiTapePTM k Bool State Opera
∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(st st' : OracleState) (p' : List Bool × List Bool),
(p', st') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(step' p)).run st).support →
inv (n + 1) p' ∧ words (k := k) p'.1 p'.2 (nextTape k) ≠ [] := by
intro n hn p hp _ oracle st st' p' hp'
Expand All @@ -324,7 +324,7 @@ public theorem ComputesTidily.iterateWhile {tm : MultiTapePTM k Bool State Opera
(oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(s : OracleState) (w' : List Bool) (s' : OracleState),
(w', s') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(step p.2)).run s).support → w'.length ≤ L :=
fun _ oracle s w' s' hw' =>
hlength (n + 1) hn w' (hpreserve n hn p.2 hp.1 _ oracle s s' w' hw').1
Expand Down Expand Up @@ -356,7 +356,7 @@ public theorem ComputesTidily.iterateWhile {tm : MultiTapePTM k Bool State Opera
(oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(s s' : OracleState) (p : List Bool × List Bool),
(p, s') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.iterate r step' ([], w₀) >>= last)).run s).support →
p.2 = [] ∧ p.1.length ≤ L := by
intro _ oracle s s' p hp
Expand Down
34 changes: 17 additions & 17 deletions Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Loop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,21 +144,21 @@ absorbed because the remaining loop halts within its own clock. -/
theorem run_interpret_runOracleConfigFrom_add (cfg : Config k Bool State Operation x)
(fuel rest : ℕ) (s : OracleState)
(hrest : ∀ result ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom fuel cfg)).run s).support,
∀ final ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
((repeatUntilBlank i body).runOracleConfigFrom rest (runConfig result.1))).run
result.2).support,
final.1.tapes.state = none) :
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
((repeatUntilBlank i body).runOracleConfigFrom (fuel + rest) (runConfig cfg))).run s =
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom fuel cfg)).run s).bind (fun result =>
(OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
((repeatUntilBlank i body).runOracleConfigFrom rest (runConfig result.1))).run
result.2) := by
induction fuel generalizing cfg s with
Expand Down Expand Up @@ -266,7 +266,7 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
(h₂ : ∀ a (OracleState : Type)
(oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState),
(a, s') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
prog₁).run s).support →
(fromCheck i body).RunsWords x (ws₁ a) (out₀ ++ emit₁ a) t₂ (prog₂ a) (ws₂ a) (emit₂ a)) :
(repeatUntilBlank i body).RunsWords x ws₀ out₀ (t₁ + t₂)
Expand All @@ -291,10 +291,10 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
simp only [runConfig, hmid, f, mapState_wordsCfg, Option.elim_none]
rfl
have hrest : ∀ result ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom t₁ cfg₀)).run s).support,
∀ final ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
((repeatUntilBlank i body).runOracleConfigFrom t₂ (runConfig result.1))).run
result.2).support,
final.1.tapes.state = none := by
Expand All @@ -311,7 +311,7 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
PMF (Cfg k Bool (RepeatUntilBlankState State) x × OracleState) :=
if h : ∃ a, p.1 = f a then
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(prog₂ (Classical.choose h))).run p.2).map
(fun (b, s₂) =>
(wordsCfg x none (ws₂ (Classical.choose h) b)
Expand All @@ -320,7 +320,7 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
have hg (a : α) (s₁ : OracleState) :
g (f a, s₁) =
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(prog₂ a)).run s₁).map
(fun (b, s₂) =>
(wordsCfg x none (ws₂ a b) (out₀ ++ (emit₁ a ++ emit₂ a b)), s₂)) := by
Expand All @@ -330,16 +330,16 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
simp only [hex, ↓reduceDIte, hchoose]
have hcongr :
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom t₁ cfg₀)).run s).bind
(fun result =>
PMF.map (fun (final, s') => (final.tapes, s'))
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
((repeatUntilBlank i body).runOracleConfigFrom t₂
(runConfig result.1))).run result.2)) =
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom t₁ cfg₀)).run s).bind
(fun result => g (result.1.tapes, result.2)) := by
apply PMF.bind_congr_on_support
Expand All @@ -356,11 +356,11 @@ theorem RunsWords.repeatUntilBlank_round (i : Fin k) {body : MultiTapePTM k Bool
rw [hcongr]
have hmapBind :
((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom t₁ cfg₀)).run s).bind
(fun result => g (result.1.tapes, result.2)) =
(((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(body.runOracleConfigFrom t₁ cfg₀)).run s).map
(fun (final, s') => (final.tapes, s'))).bind g := by
rw [PMF.bind_map]
Expand Down Expand Up @@ -396,13 +396,13 @@ theorem RunsWords.repeatUntilBlank (i : Fin k) {body : MultiTapePTM k Bool State
∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(st st' : OracleState) (s' : σ),
(s', st') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(step s)).run st).support → invariant (n + 1) s' ∧ ws s' i ≠ [])
(hstop : ∀ s, invariant rounds s →
∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool))
(st st' : OracleState) (s' : σ),
(s', st') ∈ ((OracleComp.interpret
(ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
(last s)).run st).support → ws s' i = []) :
(repeatUntilBlank i body).RunsWords x (ws s₀) out₀ ((rounds + 1) * (t + 1))
(OracleComp.iterate rounds step s₀ >>= last) ws (fun _ => []) := by
Expand Down
Loading
Loading