From 6a4c4638b8f8d050bdc6931027085aabdb36062e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:09:03 -0400 Subject: [PATCH 1/2] refactor(probabilistic): one sum of oracle interfaces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define the disjoint sum of two oracle interfaces once, in the new module `Languages/Probabilistic/Sum.lean`: `OracleSpec.sum` (notation `⊕ₒ`, scoped in `Cslib`), `OracleSpec.empty`, the combined handler `OracleComp.sumHandler`, the embeddings `OracleComp.liftLeft`/`liftRight`, and their interpretation lemmas. `probOracleSpec spec` becomes `unifSpec ⊕ₒ spec`. `ProbOracleComp.sample` is the left embedding (`sample_eq_liftLeft`), and `ProbOracleComp.handler` is the sum handler (`handler_eq_sumHandler`). The handler keeps its own case equations, because making it an abbreviation of `sumHandler` exhausts the heartbeat budget in `MAC.lean`'s one-time-filter proof. `ROMSignature.ForgerSpec` becomes a sum. Three abstract audits allow the new foundational module; their statements are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 1 + .../Protocols/Signature/RandomOracle.lean | 7 +- .../Languages/Probabilistic/Oracle.lean | 37 +++-- Complexity/Languages/Probabilistic/Sum.lean | 138 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/OracleSpecSum.lean | 48 ++++++ .../CryptographyAbstract.lean | 3 +- .../ComplexityAbstracts/ShamirAbstract.lean | 3 +- .../ComplexityAbstracts/TodaAbstract.lean | 3 +- 9 files changed, 223 insertions(+), 18 deletions(-) create mode 100644 Complexity/Languages/Probabilistic/Sum.lean create mode 100644 ComplexityTests/OracleSpecSum.lean diff --git a/Complexity.lean b/Complexity.lean index d68129622d..9a95236fc8 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1758,6 +1758,7 @@ public import Complexity.Languages.Probabilistic.RandomOracle.Probabilistic public import Complexity.Languages.Probabilistic.Repeat public import Complexity.Languages.Probabilistic.Selection public import Complexity.Languages.Probabilistic.Simulation +public import Complexity.Languages.Probabilistic.Sum public import Complexity.Languages.Probabilistic.Transcript public import Complexity.Languages.Probabilistic.Traverse public import Complexity.Languages.Probabilistic.UniformNat diff --git a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean index d7ec9b9f49..a5120ef4c6 100644 --- a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean +++ b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean @@ -8,8 +8,8 @@ module -- upstream: candidate public import Complexity.Foundations.Control.Monad.Memoize -public import Complexity.Languages.Probabilistic.Basic public import Complexity.Languages.Probabilistic.QueryCount +public import Complexity.Languages.Probabilistic.Sum public import Cslib.Probability.PMF import Complexity.Probability.PMF @@ -66,9 +66,8 @@ open Probability OracleComp /-- The calls of a forger: a signing call names a message and returns a signature, and a hash call names a point and returns its digest. -/ -abbrev ForgerSpec (M Query Sig Digest : Type) : M ⊕ Query → Type - | .inl _ => Sig - | .inr _ => Digest +abbrev ForgerSpec (M Query Sig Digest : Type) : OracleSpec (M ⊕ Query) := + (fun _ : M => Sig) ⊕ₒ (fun _ : Query => Digest) /-- A signature scheme in the random-oracle model, with public keys `PK`, secret keys `SK`, messages `M`, signatures `Sig`, and oracle `H : Query → Digest`. Signing first draws coins. -/ diff --git a/Complexity/Languages/Probabilistic/Oracle.lean b/Complexity/Languages/Probabilistic/Oracle.lean index 9db5b47b5a..f5132fcfc1 100644 --- a/Complexity/Languages/Probabilistic/Oracle.lean +++ b/Complexity/Languages/Probabilistic/Oracle.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Languages.Probabilistic.Basic +public import Complexity.Languages.Probabilistic.Sum import Complexity.Languages.Probabilistic.Simulation /-! @@ -24,11 +24,15 @@ is not automatically a strict PPT operation. ## Main definitions -* `Cslib.probOracleSpec`: the disjoint sum of the finite-uniform sampling requests and the - external queries of `spec`. +* `Cslib.probOracleSpec`: the disjoint sum `unifSpec ⊕ₒ spec` of the finite-uniform sampling + requests and the external queries of `spec`. * `Cslib.ProbOracleComp`: the sum of the uniform sampling and external oracle interfaces. * `Cslib.ProbOracleComp.sample`, `.query`: closed sampling and typed external calls. -* `Cslib.ProbOracleComp.handler`: combine handlers without introducing another interpreter. +* `Cslib.ProbOracleComp.handler`: the sum handler of sampling and external queries. + +The sampling and external interfaces form the sum `unifSpec ⊕ₒ spec` of +`Languages/Probabilistic/Sum.lean`: `sample` is its left embedding (`sample_eq_liftLeft`) and +`handler` its sum handler (`handler_eq_sumHandler`). ## Main results @@ -55,9 +59,8 @@ namespace Cslib universe v /-- A disjoint sum keeps fresh sampling requests separate from external oracle requests. -/ -abbrev probOracleSpec {Query : Type} (spec : Query → Type) : ℕ ⊕ Query → Type - | .inl n => unifSpec n - | .inr q => spec q +abbrev probOracleSpec {Query : Type} (spec : Query → Type) : OracleSpec (ℕ ⊕ Query) := + unifSpec ⊕ₒ spec /-- A program with separate finite-uniform samples and typed external queries. -/ abbrev ProbOracleComp {Query : Type} (spec : Query → Type) (α : Type) := @@ -72,16 +75,29 @@ def sample (program : ProbComp α) : ProbOracleComp spec α := OracleComp.interpret (spec := unifSpec) (fun n => OracleComp.query (spec := probOracleSpec spec) (Sum.inl n)) program +/-- Sampling is the left embedding into the sum `unifSpec ⊕ₒ spec`. -/ +theorem sample_eq_liftLeft (program : ProbComp α) : + sample (spec := spec) program = OracleComp.liftLeft program := rfl + /-- Make one external call, whose reply may determine later sampling or queries. -/ def query (q : Query) : ProbOracleComp spec (spec q) := OracleComp.query (Sum.inr q) -/-- Combine the two handlers. In particular, memoizing `oracle` does not memoize `random`. -/ +/-- Combine the two handlers. In particular, memoizing `oracle` does not memoize `random`. +This is the sum handler of `unifSpec ⊕ₒ spec` (`handler_eq_sumHandler`), with its own case +equations. -/ def handler {m : Type → Type v} (random : (n : ℕ) → m (Fin (n + 1))) (oracle : (q : Query) → m (spec q)) : (q : ℕ ⊕ Query) → m (probOracleSpec spec q) | .inl n => random n | .inr q => oracle q +/-- The combined handler is the sum handler of the sampling and external interfaces. -/ +theorem handler_eq_sumHandler {m : Type → Type v} (random : (n : ℕ) → m (Fin (n + 1))) + (oracle : (q : Query) → m (spec q)) : + handler random oracle = OracleComp.sumHandler random oracle := by + funext q + cases q <;> rfl + /-- Interpretation distributes over the sampling and external components of a program handler. -/ theorem interpret_handler {Query' : Type} {spec' : Query' → Type} {m : Type → Type v} [Monad m] (target : (q : Query') → m (spec' q)) @@ -90,8 +106,7 @@ theorem interpret_handler {Query' : Type} {spec' : Query' → Type} (fun q => OracleComp.interpret target (handler random oracle q)) = handler (fun k => OracleComp.interpret target (random k)) (fun q => OracleComp.interpret target (oracle q)) := by - funext q - cases q <;> rfl + simp only [handler_eq_sumHandler, OracleComp.interpret_sumHandler] variable {m : Type → Type v} [Monad m] [LawfulMonad m] @@ -106,7 +121,7 @@ variable {m : Type → Type v} [Monad m] [LawfulMonad m] (oracle : (q : Query) → m (spec q)) (program : ProbComp α) : OracleComp.interpret (handler random oracle) (sample program) = OracleComp.interpret random program := by - simp [sample, OracleComp.interpret_interpret, handler] + rw [handler_eq_sumHandler, sample_eq_liftLeft, OracleComp.interpret_sumHandler_liftLeft] /-- Sampling preserves ordinary functional sequencing before any interpretation. -/ @[simp] theorem sample_bind (program : ProbComp α) (next : α → ProbComp β) : diff --git a/Complexity/Languages/Probabilistic/Sum.lean b/Complexity/Languages/Probabilistic/Sum.lean new file mode 100644 index 0000000000..51b9aaa4b9 --- /dev/null +++ b/Complexity/Languages/Probabilistic/Sum.lean @@ -0,0 +1,138 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.Basic + +/-! +# Sums of oracle interfaces + +A program may call two interfaces at once: a query of `spec₁ ⊕ₒ spec₂` is a query of either, +answered as there. A program with private coins is the main instance (`probOracleSpec`), with +uniform sampling on the left; a forger calling a signer and a hash function, and the prover and +verifier oracles of an interactive protocol, are others. + +`OracleComp.sumHandler left right` answers the two kinds of call with handlers in the same monad, +and `OracleComp.liftLeft` and `OracleComp.liftRight` embed a program over one side. Interpreting +an embedded program uses only the corresponding handler (`interpret_sumHandler_liftLeft`). + +## Main definitions + +* `Cslib.OracleSpec.sum`, notation `spec₁ ⊕ₒ spec₂`: the disjoint sum of two interfaces. +* `Cslib.OracleSpec.empty`: the interface without queries. +* `Cslib.OracleComp.sumHandler`: answer the two sides with separate handlers. +* `Cslib.OracleComp.liftLeft`, `Cslib.OracleComp.liftRight`: embed a program over one side. + +## Main results + +* `Cslib.OracleComp.interpret_sumHandler_liftLeft`, `.interpret_sumHandler_liftRight`: an + embedded program uses only its own side's handler. +* `Cslib.OracleComp.interpret_sumHandler`: interpretation distributes over the two sides. +-/ + +@[expose] public section + +namespace Cslib + +universe u v w + +/-- The disjoint sum of two interfaces: a query of either, answered as there. -/ +abbrev OracleSpec.sum {ι₁ ι₂ : Type u} (spec₁ : OracleSpec.{u, v} ι₁) + (spec₂ : OracleSpec.{u, v} ι₂) : OracleSpec.{u, v} (ι₁ ⊕ ι₂) + | .inl q => spec₁ q + | .inr q => spec₂ q + +@[inherit_doc] scoped infixr:65 " ⊕ₒ " => OracleSpec.sum + +/-- The interface without queries, for a party that uses no oracle. -/ +abbrev OracleSpec.empty : OracleSpec.{0, v} Empty := fun q => q.elim + +namespace OracleComp + +variable {ι₁ ι₂ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {spec₂ : OracleSpec.{u, v} ι₂} + {α β : Type v} + +/-- Answer the calls of the left interface with `left` and those of the right with `right`. -/ +abbrev sumHandler {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) + (right : (q : ι₂) → m (spec₂ q)) : (q : ι₁ ⊕ ι₂) → m ((spec₁ ⊕ₒ spec₂) q) + | .inl q => left q + | .inr q => right q + +theorem sumHandler_inl {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) + (right : (q : ι₂) → m (spec₂ q)) (q : ι₁) : sumHandler left right (.inl q) = left q := rfl + +theorem sumHandler_inr {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) + (right : (q : ι₂) → m (spec₂ q)) (q : ι₂) : sumHandler left right (.inr q) = right q := rfl + +/-- A program over the left interface, as a program over the sum. -/ +def liftLeft (program : OracleComp spec₁ α) : OracleComp (spec₁ ⊕ₒ spec₂) α := + interpret (fun q => query (spec := spec₁ ⊕ₒ spec₂) (.inl q)) program + +/-- A program over the right interface, as a program over the sum. -/ +def liftRight (program : OracleComp spec₂ α) : OracleComp (spec₁ ⊕ₒ spec₂) α := + interpret (fun q => query (spec := spec₁ ⊕ₒ spec₂) (.inr q)) program + +@[simp] theorem liftLeft_pure (a : α) : + liftLeft (spec₂ := spec₂) (pure a : OracleComp spec₁ α) = pure a := rfl + +@[simp] theorem liftRight_pure (a : α) : + liftRight (spec₁ := spec₁) (pure a : OracleComp spec₂ α) = pure a := rfl + +@[simp] theorem liftLeft_bind (program : OracleComp spec₁ α) (next : α → OracleComp spec₁ β) : + liftLeft (spec₂ := spec₂) (program >>= next) = + liftLeft program >>= fun a => liftLeft (next a) := + interpret_bind _ _ _ + +@[simp] theorem liftRight_bind (program : OracleComp spec₂ α) (next : α → OracleComp spec₂ β) : + liftRight (spec₁ := spec₁) (program >>= next) = + liftRight program >>= fun a => liftRight (next a) := + interpret_bind _ _ _ + +@[simp] theorem liftLeft_map (f : α → β) (program : OracleComp spec₁ α) : + liftLeft (spec₂ := spec₂) (f <$> program) = f <$> liftLeft program := + interpret_map _ _ _ + +@[simp] theorem liftRight_map (f : α → β) (program : OracleComp spec₂ α) : + liftRight (spec₁ := spec₁) (f <$> program) = f <$> liftRight program := + interpret_map _ _ _ + +@[simp] theorem liftLeft_query (q : ι₁) : + liftLeft (spec₂ := spec₂) (query q) = query (spec := spec₁ ⊕ₒ spec₂) (.inl q) := + interpret_query _ _ + +@[simp] theorem liftRight_query (q : ι₂) : + liftRight (spec₁ := spec₁) (query q) = query (spec := spec₁ ⊕ₒ spec₂) (.inr q) := + interpret_query _ _ + +variable {m : Type v → Type w} [Monad m] [LawfulMonad m] + +/-- An embedded left program uses only the left handler. -/ +@[simp] theorem interpret_sumHandler_liftLeft (left : (q : ι₁) → m (spec₁ q)) + (right : (q : ι₂) → m (spec₂ q)) (program : OracleComp spec₁ α) : + interpret (sumHandler left right) (liftLeft program) = interpret left program := by + simp [liftLeft, interpret_interpret] + +/-- An embedded right program uses only the right handler. -/ +@[simp] theorem interpret_sumHandler_liftRight (left : (q : ι₁) → m (spec₁ q)) + (right : (q : ι₂) → m (spec₂ q)) (program : OracleComp spec₂ α) : + interpret (sumHandler left right) (liftRight program) = interpret right program := by + simp [liftRight, interpret_interpret] + +omit [LawfulMonad m] in +/-- Interpretation distributes over the two sides of a combined handler. -/ +theorem interpret_sumHandler {κ : Type u} {target : OracleSpec.{u, v} κ} + (oracle : (q : κ) → m (target q)) (left : (q : ι₁) → OracleComp target (spec₁ q)) + (right : (q : ι₂) → OracleComp target (spec₂ q)) : + (fun q => interpret oracle (sumHandler left right q)) = + sumHandler (fun q => interpret oracle (left q)) (fun q => interpret oracle (right q)) := by + funext q + cases q <;> rfl + +end OracleComp + +end Cslib diff --git a/ComplexityTests.lean b/ComplexityTests.lean index fdbe278f26..4bbf320633 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -280,6 +280,7 @@ import ComplexityTests.OracleLowness import ComplexityTests.OraclePPT import ComplexityTests.OracleReplay import ComplexityTests.OracleRepresentation +import ComplexityTests.OracleSpecSum import ComplexityTests.OrderedAddition import ComplexityTests.OrderedBitSum import ComplexityTests.OrderedComposition diff --git a/ComplexityTests/OracleSpecSum.lean b/ComplexityTests/OracleSpecSum.lean new file mode 100644 index 0000000000..aa40f46887 --- /dev/null +++ b/ComplexityTests/OracleSpecSum.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Languages.Probabilistic.Oracle +import Complexity.Crypto.Protocols.Signature.RandomOracle + +/-! # Sums of oracle interfaces -/ + +namespace ComplexityTests.OracleSpecSum + +open Cslib + +-- A query of the sum reduces to the response type of its side at reducible transparency. +example : ((fun _ : Unit => Bool) ⊕ₒ (fun _ : ℕ => ℕ)) (.inl ()) = Bool := by with_reducible rfl +example : ((fun _ : Unit => Bool) ⊕ₒ (fun _ : ℕ => ℕ)) (.inr 3) = ℕ := by with_reducible rfl + +-- Programs with private coins and a forger's calls are sums. +example (spec : Bool → Type) : probOracleSpec spec = unifSpec ⊕ₒ spec := rfl +example : Crypto.Protocols.ROMSignature.ForgerSpec Unit Bool ℕ (Fin 2) = + (fun _ : Unit => ℕ) ⊕ₒ (fun _ : Bool => Fin 2) := rfl + +private def left : OracleComp (fun _ : Unit => Bool) Bool := do + let a ← OracleComp.query () + let b ← OracleComp.query () + return a && !b + +-- An embedded program uses only its own side's handler; the other side is never called. +example : + OracleComp.interpret + (OracleComp.sumHandler (spec₁ := fun _ : Unit => Bool) (spec₂ := OracleSpec.empty) + (fun _ => (some true : Option Bool)) (fun q => q.elim)) + (OracleComp.liftLeft left) = some false := by + simp [left] + +-- The combined handler of a program with private coins is the sum handler, and sampling is the +-- left embedding. +example (spec : Bool → Type) (random : (n : ℕ) → Option (Fin (n + 1))) + (oracle : (q : Bool) → Option (spec q)) : + ProbOracleComp.handler random oracle = OracleComp.sumHandler random oracle := + ProbOracleComp.handler_eq_sumHandler random oracle + +example (program : ProbComp Bool) : + ProbOracleComp.sample (spec := fun _ : Bool => Bool) program = OracleComp.liftLeft program := + ProbOracleComp.sample_eq_liftLeft program + +end ComplexityTests.OracleSpecSum diff --git a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean index 943c993fcd..80370c9eeb 100644 --- a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean +++ b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean @@ -217,13 +217,14 @@ abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type := Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool) /-- -info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 21 root declarations, 252 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 21 root declarations, 254 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.CryptographyAbstract allowing [ ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, Complexity.Languages.Probabilistic.Basic, Complexity.Languages.Probabilistic.Oracle, + Complexity.Languages.Probabilistic.Sum, Complexity.Languages.Probabilistic.Oracle.Interaction, Complexity.Computability.Machines.Turing.MultiTape.Machine, Complexity.Computability.Machines.Turing.MultiTape.Machine.Program, diff --git a/abstracts/ComplexityAbstracts/ShamirAbstract.lean b/abstracts/ComplexityAbstracts/ShamirAbstract.lean index 956be8f2c9..0ca5f654d8 100644 --- a/abstracts/ComplexityAbstracts/ShamirAbstract.lean +++ b/abstracts/ComplexityAbstracts/ShamirAbstract.lean @@ -108,7 +108,7 @@ verifier's output and the final prover state for every initial state and respons /-- info: abstract audit passed for `ComplexityTests.Abstracts.ShamirAbstract`: -10 root declarations, 213 dependencies checked +10 root declarations, 215 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.ShamirAbstract allowing [ @@ -118,6 +118,7 @@ info: abstract audit passed for `ComplexityTests.Abstracts.ShamirAbstract`: Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle, Complexity.Languages.Probabilistic.Basic, Complexity.Languages.Probabilistic.Oracle, + Complexity.Languages.Probabilistic.Sum, Complexity.Languages.Probabilistic.Oracle.Interaction ] diff --git a/abstracts/ComplexityAbstracts/TodaAbstract.lean b/abstracts/ComplexityAbstracts/TodaAbstract.lean index 335d11d8bf..27c290a33c 100644 --- a/abstracts/ComplexityAbstracts/TodaAbstract.lean +++ b/abstracts/ComplexityAbstracts/TodaAbstract.lean @@ -149,7 +149,7 @@ The output and final oracle state must agree for every handler, not just for the /-- info: abstract audit passed for `ComplexityTests.Abstracts.TodaAbstract`: -15 root declarations, 238 dependencies checked +15 root declarations, 240 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.TodaAbstract allowing [ @@ -160,6 +160,7 @@ info: abstract audit passed for `ComplexityTests.Abstracts.TodaAbstract`: Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle, Complexity.Languages.Probabilistic.Basic, Complexity.Languages.Probabilistic.Oracle, + Complexity.Languages.Probabilistic.Sum, Complexity.Languages.Probabilistic.Oracle.Interaction ] From 5570b61d394713d32f39dfe8f1c80b9a4ee8fc17 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 01:21:22 -0400 Subject: [PATCH 2/2] doc(probabilistic): qualify the Sum module link from the API root Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Languages/Probabilistic/Oracle.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Complexity/Languages/Probabilistic/Oracle.lean b/Complexity/Languages/Probabilistic/Oracle.lean index f5132fcfc1..639afa77c1 100644 --- a/Complexity/Languages/Probabilistic/Oracle.lean +++ b/Complexity/Languages/Probabilistic/Oracle.lean @@ -31,8 +31,8 @@ is not automatically a strict PPT operation. * `Cslib.ProbOracleComp.handler`: the sum handler of sampling and external queries. The sampling and external interfaces form the sum `unifSpec ⊕ₒ spec` of -`Languages/Probabilistic/Sum.lean`: `sample` is its left embedding (`sample_eq_liftLeft`) and -`handler` its sum handler (`handler_eq_sumHandler`). +`Complexity/Languages/Probabilistic/Sum.lean`: `sample` is its left embedding +(`sample_eq_liftLeft`) and `handler` its sum handler (`handler_eq_sumHandler`). ## Main results