Stateful query implementations

QueryImpl.Stateful I E σ is a thin abbreviation for handlers that implement an export interface E by running StateT σ (OracleComp I). It is the unbundled stateful-handler layer used by state-separating proofs: the handler and initial state are supplied separately instead of being bundled in a package record.

def QueryImpl.Stateful {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} (I : OracleSpec ιᵢ) (E : OracleSpec ιₑ) (σ : Type v) : Type (max uₑ v (max v vᵢ) uᵢ)

A stateful implementation of export queries E using import queries I.

QueryImpl.Stateful I E σ is the raw handler shape QueryImpl E (StateT σ (OracleComp I)): each export query may inspect and update private state σ, while making import queries in I.

The surrounding QueryImpl.Stateful namespace develops the state-separating composition API for these handlers. Composition can use the canonical product state, via link and par, or an explicit Frame that describes how two component states are embedded as separated lawful state lenses inside a larger state.

State frames

structure QueryImpl.Stateful.Frame (σ σ₁ σ₂ : Type v) : Type v

A frame specifying how two component states sit inside a larger state.

The component projections are state lenses in the sense of PFunctor.Lens.State: each one has a getter and a putter satisfying the standard very-well-behaved lens laws. The separated field says the two lenses are non-interfering: each update leaves the other view unchanged, and the two updates commute. Composition operators such as linkWith and parSumWith use this explicit frame to run handlers over a larger state than the canonical product state.

• left : PFunctor.Lens.State σ σ₁

  Lens selecting and updating the left component state.

• right : PFunctor.Lens.State σ σ₂

  Lens selecting and updating the right component state.

• left_isVeryWellBehaved : self.left.IsVeryWellBehaved

  The left component lens satisfies PutGet, GetPut, and PutPut.

• right_isVeryWellBehaved : self.right.IsVeryWellBehaved

  The right component lens satisfies PutGet, GetPut, and PutPut.

• separated : self.left.IsSeparated self.right

  The two component lenses are non-interfering separated views of the source state.

def QueryImpl.Stateful.Frame.prod (σ₁ σ₂ : Type v) : Frame (σ₁ × σ₂) σ₁ σ₂

The canonical product-state frame.

instance QueryImpl.Stateful.Frame.instLeftIsVeryWellBehaved {σ σ₁ σ₂ : Type v} (F : Frame σ σ₁ σ₂) : F.left.IsVeryWellBehaved

instance QueryImpl.Stateful.Frame.instRightIsVeryWellBehaved {σ σ₁ σ₂ : Type v} (F : Frame σ σ₁ σ₂) : F.right.IsVeryWellBehaved

instance QueryImpl.Stateful.Frame.instSeparated {σ σ₁ σ₂ : Type v} (F : Frame σ σ₁ σ₂) : F.left.IsSeparated F.right

@[reducible]

def QueryImpl.Stateful.Frame.linkReshape {σ σ₁ σ₂ α : Type v} (F : Frame σ σ₁ σ₂) (s : σ) : (α × σ₁) × σ₂ → α × σ

Reshape the result of a linked handler run back into the source state described by a frame.

The input carries an output value, the updated left component state, and the updated right component state. The frame writes those component states back into the original source state s.

Basic handlers and evaluation

def QueryImpl.Stateful.id {ιₑ : Type uₑ} (E : OracleSpec ιₑ) : Stateful E E PUnit.{v + 1}

The identity stateful handler forwards each query to the same interface, threading a trivial state.

def QueryImpl.Stateful.ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} (h : QueryImpl E (OracleComp I)) : Stateful I E PUnit.{v + 1}

Lift a stateless implementation into a stateful implementation with trivial state.

def QueryImpl.Stateful.run {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (h : Stateful I E σ) (s₀ : σ) (A : OracleComp E α) : OracleComp I α

Run a stateful handler from an explicit initial state, discarding the final state.

def QueryImpl.Stateful.run₀ {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} [Inhabited σ] (h : Stateful I E σ) (A : OracleComp E α) : OracleComp I α

Run a stateful handler from the default initial state, discarding the final state. This is convenient for heap states, where default = Heap.empty, and for product states assembled from default components.

def QueryImpl.Stateful.runState {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (h : Stateful I E σ) (s₀ : σ) (A : OracleComp E α) : OracleComp I (α × σ)

Run a stateful handler from an explicit initial state, keeping the final state.

def QueryImpl.Stateful.runState₀ {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} [Inhabited σ] (h : Stateful I E σ) (A : OracleComp E α) : OracleComp I (α × σ)

Run a stateful handler from the default initial state, keeping the final state.

@[simp]

theorem QueryImpl.Stateful.runState_ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {α : Type v} (h : QueryImpl E (OracleComp I)) (A : OracleComp E α) : (ofStateless h).runState PUnit.unit A = (fun (x : α) => (x, PUnit.unit)) <$> simulateQ h A

@[simp]

theorem QueryImpl.Stateful.run_ofStateless {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {α : Type v} (h : QueryImpl E (OracleComp I)) (A : OracleComp E α) : (ofStateless h).run PUnit.unit A = simulateQ h A

@[simp]

theorem QueryImpl.Stateful.run_pure {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (h : Stateful I E σ) (s₀ : σ) (x : α) : h.run s₀ (pure x) = pure x

@[simp]

theorem QueryImpl.Stateful.runState_pure {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α : Type v} (h : Stateful I E σ) (s₀ : σ) (x : α) : h.runState s₀ (pure x) = pure (x, s₀)

@[simp]

theorem QueryImpl.Stateful.runState_bind {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ α β : Type v} (h : Stateful I E σ) (s₀ : σ) (A : OracleComp E α) (f : α → OracleComp E β) : h.runState s₀ (A >>= f) = do let x ← h.runState s₀ A match x with | (a, s) => (simulateQ h (f a)).run s

theorem QueryImpl.Stateful.simulateQ_liftComp_run_of_query {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {σ : Type v} {I₀ : OracleSpec ιᵢ} {M₀ : OracleSpec ιₘ} [MonadLiftT (OracleQuery I₀) (OracleQuery M₀)] (h : Stateful I₀ M₀ σ) (hquery : ∀ (t : I₀.Domain) (s : σ), (simulateQ h ((liftM (OracleSpec.query t)).liftComp M₀)).run s = (fun (a : I₀.Range t) => (a, s)) <$> liftM (OracleSpec.query t)) {α : Type v} (oa : OracleComp I₀ α) (s : σ) : (simulateQ h (oa.liftComp M₀)).run s = (fun (a : α) => (a, s)) <$> oa

A stateful handler that transparently forwards lifted queries also forwards every lifted computation.

The hypothesis is query-local: each lifted input query runs as the same query in the base interface and leaves the state unchanged. The conclusion lifts this to all computations by free-monad induction.

def QueryImpl.Stateful.transportState {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ σ' : Type v} (h : Stateful I E σ) (φ : σ ≃ σ') : Stateful I E σ'

Transport a stateful handler along a state equivalence.

@[simp]

theorem QueryImpl.Stateful.transportState_apply_run {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {E : OracleSpec ιₑ} {σ σ' : Type v} (h : Stateful I E σ) (φ : σ ≃ σ') (t : E.Domain) (s' : σ') : (h.transportState φ t).run s' = Prod.map id ⇑φ <$> (h t).run (φ.symm s')

Sequential composition

def QueryImpl.Stateful.linkWith {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ σ₁ σ₂ : Type v} (F : Frame σ σ₁ σ₂) (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) : Stateful I E σ

Sequential composition of two stateful handlers using an explicit state frame.

The frame specifies how the outer state σ₁ and inner state σ₂ are viewed and updated inside the combined state σ. The linked handler reads both component states from the source state, runs the usual nested simulation, then writes back the updated outer and inner states through the frame lenses.

@[simp]

theorem QueryImpl.Stateful.linkWith_apply_run {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ σ₁ σ₂ : Type v} (F : Frame σ σ₁ σ₂) (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) (t : E.Domain) (s : σ) : (linkWith F outer inner t).run s = F.linkReshape s <$> (simulateQ inner ((outer t).run (F.left.get s))).run (F.right.get s)

def QueryImpl.Stateful.link {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ : Type v} (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) : Stateful I E (σ₁ × σ₂)

Sequential composition of two stateful handlers. The outer handler exports E and imports M; the inner handler exports M and imports I.

theorem QueryImpl.Stateful.link_impl_apply_run {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ : Type v} (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) (t : E.Domain) (s₁ : σ₁) (s₂ : σ₂) : (outer.link inner t).run (s₁, s₂) = (Frame.prod σ₁ σ₂).linkReshape (s₁, s₂) <$> (simulateQ inner ((outer t).run s₁)).run s₂

theorem QueryImpl.Stateful.simulateQ_linkWith_run {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ σ₁ σ₂ α : Type v} (F : Frame σ σ₁ σ₂) (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) (A : OracleComp E α) (s : σ) : (simulateQ (linkWith F outer inner) A).run s = F.linkReshape s <$> (simulateQ inner ((simulateQ outer A).run (F.left.get s))).run (F.right.get s)

Structural form of linked simulation through an explicit state frame.

theorem QueryImpl.Stateful.simulateQ_link_run {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ α : Type v} (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) (A : OracleComp E α) (s₁ : σ₁) (s₂ : σ₂) : (simulateQ (outer.link inner) A).run (s₁, s₂) = (Frame.prod σ₁ σ₂).linkReshape (s₁, s₂) <$> (simulateQ inner ((simulateQ outer A).run s₁)).run s₂

Structural form of linked simulation as nested simulations.

def QueryImpl.Stateful.shiftLeft {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} (outer : Stateful M E σ₁) (s₀ : σ₁) {α : Type v} (A : OracleComp E α) : OracleComp M α

Absorb a stateful outer handler and starting state into the client computation.

@[simp]

theorem QueryImpl.Stateful.shiftLeft_pure {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} (outer : Stateful M E σ₁) (s₀ : σ₁) {α : Type v} (x : α) : outer.shiftLeft s₀ (pure x) = pure x

theorem QueryImpl.Stateful.shiftLeft_map {ιₘ : Type uₘ} {ιₑ : Type uₑ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ : Type v} (outer : Stateful M E σ₁) (s₀ : σ₁) {α β : Type v} (f : α → β) (A : OracleComp E α) : outer.shiftLeft s₀ (f <$> A) = f <$> outer.shiftLeft s₀ A

theorem QueryImpl.Stateful.run_link_eq_run_shiftLeft {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₁ σ₂ α : Type v} (outer : Stateful M E σ₁) (inner : Stateful I M σ₂) (s₁ : σ₁) (s₂ : σ₂) (A : OracleComp E α) : (outer.link inner).run (s₁, s₂) A = inner.run s₂ (outer.shiftLeft s₁ A)

Program-level linked-game reduction with explicit initial states.

theorem QueryImpl.Stateful.run_link_left_ofStateless {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {σ₂ α : Type v} (h : QueryImpl E (OracleComp M)) (inner : Stateful I M σ₂) (s₂ : σ₂) (A : OracleComp E α) : ((ofStateless h).link inner).run (PUnit.unit, s₂) A = inner.run s₂ (simulateQ h A)

@[simp]

theorem QueryImpl.Stateful.run_link_ofStateless {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} {I : OracleSpec ιᵢ} {M : OracleSpec ιₘ} {E : OracleSpec ιₑ} {α : Type v} (hP : QueryImpl E (OracleComp M)) (hQ : QueryImpl M (OracleComp I)) (A : OracleComp E α) : ((ofStateless hP).link (ofStateless hQ)).run (PUnit.unit, PUnit.unit) A = simulateQ hQ (simulateQ hP A)

Parallel composition

structure QueryImpl.Stateful.ExportRoute {ιₑ : Type uₑ} (E : OracleSpec ιₑ) {ιₑ₁ : Type uₑ} (E₁ : OracleSpec ιₑ₁) {ιₑ₂ : Type uₑ} (E₂ : OracleSpec ιₑ₂) : Type (max uₑ v)

A typed routing of a named export interface into a two-component parallel composition.

Each external query is owned by exactly one component. The equivalence transports between the external response type and the selected component response type.

• route (t : E.Domain) : (t₁ : E₁.Domain) × (E.Range t ≃ E₁.Range t₁) ⊕ (t₂ : E₂.Domain) × (E.Range t ≃ E₂.Range t₂)

def QueryImpl.Stateful.ExportRoute.target {ιₑ₁ ιₑ₂ : Type uₑ} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} (R : ExportRoute E E₁ E₂) (t : E.Domain) : E₁.Domain ⊕ E₂.Domain

The tagged component query selected by an export route.

def QueryImpl.Stateful.ExportRoute.sum {ιₑ₁ ιₑ₂ : Type uₑ} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} : ExportRoute (E₁ + E₂) E₁ E₂

The canonical route for the sum of two export interfaces.

structure QueryImpl.Stateful.LawfulExportRoute {ιₑ : Type uₑ} (E : OracleSpec ιₑ) {ιₑ₁ : Type uₑ} (E₁ : OracleSpec ιₑ₁) {ιₑ₂ : Type uₑ} (E₂ : OracleSpec ιₑ₂) extends QueryImpl.Stateful.ExportRoute E E₁ E₂ : Type (max uₑ v)

An export route with no aliases.

This says the named external interface is injective into the tagged component query space. It is the right assumption for transporting query-count predicates from a routed interface to its component interfaces without double-counting aliases.

• route (t : E.Domain) : (t₁ : E₁.Domain) × (E.Range t ≃ E₁.Range t₁) ⊕ (t₂ : E₂.Domain) × (E.Range t ≃ E₂.Range t₂)
• target_injective : Function.Injective self.target

  The route does not alias two external query names to one tagged component query.

structure QueryImpl.Stateful.ExportRouteEquiv {ιₑ : Type uₑ} (E : OracleSpec ιₑ) {ιₑ₁ : Type uₑ} (E₁ : OracleSpec ιₑ₁) {ιₑ₂ : Type uₑ} (E₂ : OracleSpec ιₑ₂) extends QueryImpl.Stateful.ExportRoute E E₁ E₂ : Type (max uₑ v)

A named export interface that is equivalent to the sum of two component interfaces.

This is the strongest route law: every component query is exposed exactly once, and every external query is a named presentation of a tagged component query.

• route (t : E.Domain) : (t₁ : E₁.Domain) × (E.Range t ≃ E₁.Range t₁) ⊕ (t₂ : E₂.Domain) × (E.Range t ≃ E₂.Range t₂)
• targetEquiv : E.Domain ≃ E₁.Domain ⊕ E₂.Domain

  The query-domain equivalence induced by the route.

• target_eq (t : E.Domain) : self.target t = self.targetEquiv t

  The route's tagged target agrees with targetEquiv.

def QueryImpl.Stateful.ExportRouteEquiv.toLawfulExportRoute {ιₑ₁ ιₑ₂ : Type uₑ} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} (R : ExportRouteEquiv E E₁ E₂) : LawfulExportRoute E E₁ E₂

Forget an equivalence route to a no-alias lawful route.

def QueryImpl.Stateful.ExportRouteEquiv.sum {ιₑ₁ ιₑ₂ : Type uₑ} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} : ExportRouteEquiv (E₁ + E₂) E₁ E₂

The canonical equivalence route for the sum of two export interfaces.

def QueryImpl.Stateful.parRouteWith {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} (F : Frame σ σ₁ σ₂) (R : ExportRoute E E₁ E₂) [MonadLiftT (OracleQuery I₁) (OracleQuery I)] [MonadLiftT (OracleQuery I₂) (OracleQuery I)] (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful I E σ

Parallel composition of two stateful handlers over a named export interface using an explicit state frame and ambient import interface.

The frame specifies where each side's private state lives in the shared source state. A left query updates only the left view, and a right query updates only the right view. The frame's separation law records that these two updates are non-interfering.

def QueryImpl.Stateful.parRoute {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} (R : ExportRoute E E₁ E₂) [MonadLiftT (OracleQuery I₁) (OracleQuery I)] [MonadLiftT (OracleQuery I₂) (OracleQuery I)] (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful I E (σ₁ × σ₂)

Parallel composition of two stateful handlers over a named export interface and canonical product state.

def QueryImpl.Stateful.parWithImports {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} (F : Frame σ σ₁ σ₂) [MonadLiftT (OracleQuery I₁) (OracleQuery I)] [MonadLiftT (OracleQuery I₂) (OracleQuery I)] (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful I (E₁ + E₂) σ

Parallel composition of two stateful handlers using an explicit state frame and ambient import interface. The export interface is the canonical sum.

def QueryImpl.Stateful.parRouteSeparatedWith {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} {ιᵢ : Type uᵢ} {I : OracleSpec ιᵢ} {ιₑ : Type uₑ} {E : OracleSpec ιₑ} (F : Frame σ σ₁ σ₂) (R : ExportRoute E E₁ E₂) [I₁ ⊂ₒ I] [I₁.LawfulSubSpec I] [I₂ ⊂ₒ I] [I₂.LawfulSubSpec I] [I₁.DisjointSubSpec I₂ I] (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful I E σ

Routed parallel composition over an ambient import interface whose two component import embeddings are known to have disjoint query images. The implementation is the same as parRouteWith; the extra hypothesis is available to downstream proofs that need sum-like import separation.

def QueryImpl.Stateful.parSumWith {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (F : Frame σ σ₁ σ₂) (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful (I₁ + I₂) (E₁ + E₂) σ

Parallel composition of two stateful handlers using an explicit state frame and disjoint sum import and export interfaces.

@[simp]

theorem QueryImpl.Stateful.parSumWith_apply_inl_run {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (F : Frame σ σ₁ σ₂) (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) (t : E₁.Domain) (s : σ) : (parSumWith F h₁ h₂ (Sum.inl t)).run s = (Prod.map id fun (s₁' : σ₁) => F.left.put s₁' s) <$> ((h₁ t).run (F.left.get s)).liftComp (I₁ + I₂)

@[simp]

theorem QueryImpl.Stateful.parSumWith_apply_inr_run {σ σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (F : Frame σ σ₁ σ₂) (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) (t : E₂.Domain) (s : σ) : (parSumWith F h₁ h₂ (Sum.inr t)).run s = (Prod.map id fun (s₂' : σ₂) => F.right.put s₂' s) <$> ((h₂ t).run (F.right.get s)).liftComp (I₁ + I₂)

def QueryImpl.Stateful.parSum {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) : Stateful (I₁ + I₂) (E₁ + E₂) (σ₁ × σ₂)

Parallel composition of two stateful handlers over disjoint sum interfaces.

@[simp]

theorem QueryImpl.Stateful.parSum_apply_inl_run {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) (t : E₁.Domain) (s₁ : σ₁) (s₂ : σ₂) : (h₁.parSum h₂ (Sum.inl t)).run (s₁, s₂) = (Prod.map id fun (x : σ₁) => (x, s₂)) <$> ((h₁ t).run s₁).liftComp (I₁ + I₂)

@[simp]

theorem QueryImpl.Stateful.parSum_apply_inr_run {σ₁ σ₂ : Type v} {ιᵢ₁ ιᵢ₂ : Type uᵢ} {ιₑ₁ ιₑ₂ : Type uₑ} {I₁ : OracleSpec ιᵢ₁} {I₂ : OracleSpec ιᵢ₂} {E₁ : OracleSpec ιₑ₁} {E₂ : OracleSpec ιₑ₂} (h₁ : Stateful I₁ E₁ σ₁) (h₂ : Stateful I₂ E₂ σ₂) (t : E₂.Domain) (s₁ : σ₁) (s₂ : σ₂) : (h₁.parSum h₂ (Sum.inr t)).run (s₁, s₂) = (Prod.map id fun (x : σ₂) => (s₁, x)) <$> ((h₂ t).run s₂).liftComp (I₁ + I₂)