feat(Query): add query complexity framework

[kim-em]

This PR adds infrastructure for proving upper bounds on the number of queries
(comparisons, oracle calls, etc.) an algorithm makes, using monad parametricity to ensure validity of the bounds.

• TickT m monad transformer with tick counting, Costs predicate, and combinators
  (Costs.pure, Costs.bind, Costs.monadLift, Costs.ite, etc.)
• RunsIn/RunsInT predicates packaging the parametricity argument
• Demo: insertion sort with quadratic query bound
• Demo: monadic mapSum with functional correctness under tick instrumentation

Quoting from the module doc for RunsIn:

---

RunsIn f bound (and its generalization RunsInT) assert that a monad-generic algorithm f
makes at most bound x queries on input x.

An algorithm like

def insertionSort [Monad m] (cmp : α × α → m Bool) : List α → m (List α) := ...

is written generically over the monad m. To measure its query complexity, we specialize
m to TickM (or TickT n for algorithms with additional effects) and provide a
cmp implementation that calls tick once per invocation.

Because insertionSort is parametric in m, it cannot observe the tick instrumentation.
It must call cmp the same number of times regardless of which monad it runs in.
Therefore any upper bound proved via TickM is a true bound on query count in all monads.

---

🤖 Prepared with Claude Code

[kim-em]

I have intentionally kept this at the level of "single tick" counting of costs. It is a fairly straightforward change to make this more flexible, which I have not done here to ease reviewing of the essential idea of using monad parametricity.

[kim-em]

I would like to make this private, but this breaks a proof below in a way I haven't yet understood.

[sgraf812]

I think you reported this issue to me in Dec (I hope it's the same one). I handed over the following reproducer to @Kha:

module

public structure State where
  private count : Nat

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  set_option trace.Meta.Tactic.simp true in
  set_option trace.Debug.Meta.Tactic.simp true in
  set_option trace.Debug.Meta.Tactic.simp.congr true in
  set_option trace.Meta.realizeConst true in
  simp [*]

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  omega

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  grind

we traced the crash down to mkCongrSimp?, IIRC it was due to getFunInfo. But I think we never fixed it; should have kept better track of this.

[sgraf812]

Actually no, it appears this issue has been fixed! At least the reproducer works, and the following works as well (but proofs are broken on latest Mathlib due to DefEq changes...)

module

public import Std.Do.Triple.Basic
import Std.Tactic.Do

open Std.Do

public section

structure TickM.State where
  private count : Nat

@[expose] def TickM (α : Type) := StateM TickM.State α

namespace TickM

instance : Monad TickM := inferInstanceAs (Monad (StateM TickM.State))
instance : LawfulMonad TickM := inferInstanceAs (LawfulMonad (StateM TickM.State))
instance : Std.Do.WP TickM (.arg TickM.State .pure) := inferInstanceAs (Std.Do.WP (StateM TickM.State) _)

def tick : TickM Unit := fun s => ⟨(), ⟨s.count + 1⟩⟩

@[spec]
private theorem tick_spec {Q : PostCond Unit (.arg TickM.State .pure)} :
    Triple tick (fun s => Q.1 () ⟨s.count+1⟩) Q := by
  simp [tick, Triple, wp, Id.run]

So maybe try again to make the field private?

[eric-wieser]

This is effectively identical to TimeM Nat

[kim-em]

I've now integrated / replaced the existing material using TimeM (renaming everything in this PR from Tick back to Time).

In particular, in this last commit I've added all the theorems about mergeSort's spec and runtime bounds using this framework.

[sgraf812]

Nice! It would be great if we could prove specs about Costs using mvcgen, though. Can take a look once I'm back from PTO

[sgraf812]

I think you reported this issue to me in Dec (I hope it's the same one). I handed over the following reproducer to @Kha:

module

public structure State where
  private count : Nat

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  set_option trace.Meta.Tactic.simp true in
  set_option trace.Debug.Meta.Tactic.simp true in
  set_option trace.Debug.Meta.Tactic.simp.congr true in
  set_option trace.Meta.realizeConst true in
  simp [*]

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  omega

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  grind

we traced the crash down to mkCongrSimp?, IIRC it was due to getFunInfo. But I think we never fixed it; should have kept better track of this.

[sgraf812]

From my past (limited) experience with defeq abuse, it may make sense to make TickT @[irreducible] and add an explicit injection/projection pair.

[sgraf812]

(defeq abuse, but probably fine if you formulate your lemmas about .run.)

[sgraf812]

This function suggests the existence of counted2 [Monad m] (f : α → β → γ) (a : α) (b : β) : TickT m γ etc., similar to liftA<n> in Haskell. It's probably convenient to have counted, but I think it would be convenient to have counted2 and counted3 as well.

Although it would be reasonable for callers to just uncurry their functions before using counted. I think it doesn't scale if we also provide variants of RunsInT below.

[kim-em]

I think I'd prefer to leave the uncurried API for later, to reduce surface area here.

[sgraf812]

Neat!!

• I think you need to add somewhere (maybe to the top-level comment) that relying on parametricity is only credible when everything is computable. Otherwise you can have if h : α = Nat then ... else ... by Classical.choice.
• I wonder if callers can provide an f that uses higher-order constructs such as for loops in do notation. Can't quite play it out in my head right now, but I think it's one of the reasons that the IteratorLoop class is so complicated.

[kim-em]

Done in 3737e39 — added a "Computability caveat" section to the RunsIn module doc-string, noting that a noncomputable algorithm could use Classical.choice to subvert instrumentation, and that this framework targets upper bounds, not lower bounds.

[sgraf812]

I guess it would be nice to use mvcgen for this kind of proof. Can take a look when I'm back from PTO! You shouldn't need to replicate your own reasoning framework with Costs.pure/Costs.bind etc.

[sgraf812]

My gut says it yields simpler VCs if you write specs that are schematic in the post (like tick_spec) rather than the precondition

[sgraf812]

This sounds to me like it could be expressed as a loop invariant lemma, similar to Spec.forIn_list etc.

[Shreyas4991]

@kim-em : This is duplicating #372 (refinement of #275) is it not? Also there I have a specific meaning of queries which are pre-declared inductive types there. I think the reuse of the word query might cause confusion here.

@sgraf812 : Related question, could we set up mvcgen for the framework in #372 ? Essentially it runs code in Id monad and measures complexity in TimeM (which is just an additive writer monad).

[Shreyas4991]

You say
"Because insertionSort is parametric in m, it cannot observe the tick instrumentation.
It must call cmp the same number of times regardless of which monad it runs in.
Therefore any upper bound proved via TickM is a true bound on query count in all monads."

But you could just as easily use a pure function version of cmp. So you can still sneak in a 0-cost comparison in this model. Same in other examples. The basic limitation of using monadic DSLs applies here too. Anything can be snuck into pure in-principle.

[Shreyas4991]

If your counter-argument here is the absence of BEq, we already use that in the linearSearch example in #372

[kim-em]

I think you are misunderstanding this PR. I'm offline for the weekend, but see if you can subvert it! I claim you can't write any monad polymorphic function from lists to lists that sorts, and has a "too small" RunsIn.

[Shreyas4991]

I see that you simply take a comparison function as a parameter. In this case our models have the same security from misuse of return. However I have noted the strong limitations of this approach as opposed to mine below. In my case, I only interpret this function concretely in my model.

[kim-em]

This is duplicating #372 (refinement of #275) is it not?

No, I am proposing that this is a better alternative.

[Shreyas4991]

This is duplicating #372 (refinement of #275) is it not?

No, I am proposing that this is a better alternative.

I strongly disagree. You don't state your queries up front in your model. So you can't state reductions, lower bounds etc. all this makes use of explicit queries and custom cost functions. Instead you use a lean function as a parameter. This is a huge limitation in algorithms theory and complexity.

In the model of #372, one can formally state multiple RAM models and even DSLs for Turing machines and circuits from circuit complexity. Therefore we can already define uniform circuit classes in complexity which involves writing programs in two different models with two different cost models (TMs and circuits). The fact that I can write circuits tells me that I can also encode parallel algorithms and the equivalence between circuits and parallel algorithms (there are several standard equivalences between these models). I have kept my pr limited to simple examples to keep it focused (the maintainers explicitly asked this). In fact it can even talk about lower bounds.

In summary : the other PR allows for a comprehensive top down treatment of the multitude of models in algorithms and the relationships between them(one of the standard models like RAM and TM could be sink nodes in this relationship network).

What this PR is doing is equivalent to compressing the process of defining a query and an evaluation function (and a cost function) in my PR, by directly providing the interpreted version as a parameter (cmp). But it is losing a lot in the process. So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m and adding mvcgen machinery. While this might be a positive, it could just as easily have been done on top of #372, with all the benefits of that approach. This suggests (per project contribution guidelines), that at the very least this PR should have been:

1. Discussed in Zulip first

However, for any major development, it is strongly recommended to discuss first on Zulip (or via a GitHub issue) so that the scope, dependencies, and placement in the library are aligned.

2. Build on top of the existing PR feat: query complexity model for algorithms theory #372 mentioned above.

New definitions should instantiate existing abstractions whenever appropriate

[kim-em]

So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m

@Shreyas4991, you are misunderstanding the purpose of this PR, and how we achieve security against cost manipulation via parametricity.

New definitions should instantiate existing abstractions whenever appropriate

#372 doesn't "exist" for the purposes of that suggestion, as it hasn't been merged. I suggest comparison between #376 and #372 stay on Zulip, rather than in the PR discussions.

[Shreyas4991]

So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m

@Shreyas4991, you are misunderstanding the purpose of this PR, and how we achieve security against cost manipulation via parametricity.

In this instance I am certain I do. I am the domain expert here as far as algorithms is concerned. This is merely short-circuiting my approach and shares the exact same limitation mine does, with write-queries, and with a less than optimal design for the purposes my PR serves. The "generalization" is merely trying to hide the evaluation behind an arbitrary monad instead of a free monad with an uninterpreted query.

[Shreyas4991]

New definitions should instantiate existing abstractions whenever appropriate

#372 doesn't "exist" for the purposes of that suggestion, as it hasn't been merged. I suggest comparison between

There is no suggestion in that guidelines that a contributing PRs work can be overriden without discussion if it isn't merged already. It is also a core principle of open source etiquette to discuss an idea first, especially if someone is already working on it before making one's own contribution. This ensures that the work and effort of contributors is not devalued or outright erased. I have adhered to this principle with my PR from the beginning via zulip discussions. This PR has violated it.

Open source guides:

Before doing anything, do a quick check to make sure your idea hasn’t been discussed elsewhere. Skim the project’s README, issues (open and closed), mailing list, and Stack Overflow. You don’t have to spend hours going through everything, but a quick search for a few key terms goes a long way.

[kim-em]

@Shreyas4991, you mentioned that "our models have the same security from misuse of return." I don't think that's the case. Here's a fully computable algorithm in the framework of #372 that "sorts in zero queries":

/-- Sorting with zero queries. -/
def freeSort {α : Type} (le : α → α → Prop) [DecidableRel le]
    (l : List α) : Prog (SortOpsInsertHead α) (List α) :=
  .pure (l.insertionSort le)

theorem freeSort_correct {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).eval (sortModel le) = l.insertionSort le := by
  simp [freeSort]

theorem freeSort_free {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).time (sortModel le) = 0 := by
  simp [freeSort]

These theorems together assert that sorting can be done correctly with zero comparisons. The root cause: sortModel le requires [DecidableRel le] to interpret queries, and that same instance gives algorithms direct access to comparisons via pure, bypassing the query mechanism entirely.

In the monad-parametric approach of #376, the comparison is an opaque parameter (α × α → m Bool). The cost theorem insertionSort_runsIn : RunsIn insertionSort (fun xs => xs.length * xs.length) has no DecidableRel, Ord, or BEq in its statement — the algorithm has no way to compare elements except through the provided function, and every such call is counted.

To be clear about the limitations of #376: because Lean has classical logic, a noncomputable algorithm could in principle use Classical.choice to distinguish TickM from other monads and cheat. This means we can't use RunsIn to prove lower bounds (a noncomputable counterexample would always exist). But that's not the goal here — the goal is proving upper bounds for specific algorithms. For computable (monad-polymorphic) algorithms, parametricity holds: they can't observe which monad they're running in, so every comparison genuinely goes through cmp, and the RunsIn bound is valid.

The exploit above is not about classical logic — freeSort is fully computable. The issue is structural: the free monad approach necessarily puts [DecidableRel le] in scope (because the model needs it), and nothing prevents algorithms from using it directly.

[Shreyas4991]

@Shreyas4991, you mentioned that "our models have the same security from misuse of return." I don't think that's the case. Here's a fully computable algorithm in the framework of #372 that "sorts in zero queries":

/-- Sorting with zero queries. -/
def freeSort {α : Type} (le : α → α → Prop) [DecidableRel le]
    (l : List α) : Prog (SortOpsInsertHead α) (List α) :=
  .pure (l.insertionSort le)

theorem freeSort_correct {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).eval (sortModel le) = l.insertionSort le := by
  simp [freeSort]

theorem freeSort_free {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).time (sortModel le) = 0 := by
  simp [freeSort]

These theorems together assert that sorting can be done correctly with zero comparisons. The root cause: sortModel le requires [DecidableRel le] to interpret queries, and that same instance gives algorithms direct access to comparisons via pure, bypassing the query mechanism entirely.

In the monad-parametric approach of #376, the comparison is an opaque parameter (α × α → m Bool). The cost theorem insertionSort_runsIn : RunsIn insertionSort (fun xs => xs.length * xs.length) has no DecidableRel, Ord, or BEq in its statement — the algorithm has no way to compare elements except through the provided function, and every such call is counted.

To be clear about the limitations of #376: because Lean has classical logic, a noncomputable algorithm could in principle use Classical.choice to distinguish TickM from other monads and cheat. This means we can't use RunsIn to prove lower bounds (a noncomputable counterexample would always exist). But that's not the goal here — the goal is proving upper bounds for specific algorithms. For computable (monad-polymorphic) algorithms, parametricity holds: they can't observe which monad they're running in, so every comparison genuinely goes through cmp, and the RunsIn bound is valid.

The exploit above is not about classical logic — freeSort is fully computable. The issue is structural: the free monad approach necessarily puts [DecidableRel le] in scope (because the model needs it), and nothing prevents algorithms from using it directly.

It's not an exploit because you are including an instance that the model explicitly does not require . You can do this in your model as well. Concretely take your decidable LE instance and lift, choose a specific monad with a liftM function and you can also lift "let cmp := liftM fun x y => decide <| LE.le x y) into your monad. I use these instances because I find the trade off between the simplicity of these algorithms and detection of cheating trivial.

You are inserting an extra typeclass instance into my def. I can conversely insert a special monad into yours and erase the parametricity. Neither of these are "exploits"

If providing extra instances is fair game then so is specializing the monad parameter to yours. And to be clear, based on my discussion with type theorists, adding proper foolproof parametric polymorhism to a dependently typed system is an open problem (concretely something like ML style modules). Rocq's module system has been mentioned to me as an example (and they just uncovered a soundness bug there yesterday). So if you solve parametricity in lean, please submit it to POPL.

[Shreyas4991]

@kim-em to be clear, a Prog should never have typeclass instances. That's the easiest red flag to catch.

please see the actual linearSearch example. It explicitly avoids giving DecidableEq instances and uses a Bool predicate. We can absolutely make this change for the sorting models as well. Nothing about this example is specific to my model and not yours. It is about the specific choice of type for the cmp operation. Your correctness theorem doesn't prove sorting yet. I found it convenient to use List.Pairwise to prove sortedness. In your PR you don't prove this yet. So this is not even a point that we can meaningfully compare on. If someone wrote a function with le : \a -> \a -> Prop in your model, they will face the exact same issue.

Secondly you made a claim about your goals. They are not my goals. The query model is a model that I am building based on what I know will work for algorithms theory. I am working on something that I can use for algorithms theory. The code verification stuff can be handled by Boole and is not my issue. It's arguably better suited for the problem.

Thirdly this PR is just reinventing WriterT monad transformer

[Shreyas4991]

Lastly parametric polymorphism requires that I should not be able to supply an explicit m. In Lean you can always do this. So this is not even "parametric polymorphism". That requires something like ML modules. I should have caught this before. Typeclasses implement ad-hoc polymorphism viz the exact opposite.

[Shreyas4991]

@kim-em : Update, I just changed the Prop model to a Bool le model for my sorting query and algorithms in cslib#372 . So no [Decidable le] instances are needed anymore. This has absolutely nothing to do with Free Monads and everything to do with me picking a convenient approach.

But as I have mentioned before, nothing stops someone from writing
def insertionSort ... (le : a -> a -> Prop) [DecidableRel le] in your model either (after all now you need to insert the Prop and DecidableRel version as extra parameters in mine now that I have completely switched all my examples to Bool).

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

Also (and this is exactly why I think this PR is misguided from a contribution guidelines standpoint), you could have just made a PR to change my model to a ProgT, which would put my queries behind a monad parameter m, if you felt that my method lacked enough safety.

Concretely, in a proper approach, you would have to make a PR on top of #372 :

1. Write a monad transformer version of TimeM (that's your TickT)
2. Write a monad transformer version of FreeM.
3. generalize Prog to ProgT.
4. change queries and models to evaluate to this monadic type.

Instead your PR lays claim to the idea of query complexity in the title, an idea that I have been promoting since even before the debate formalization, and then squanders the power of my model by losing its explicit inductive query types (while also depriving all of us authors the authorship credit that is due), which I have crafted to handle a huge chunk of algorithms theory literature in a top down fashion.

[kim-em]

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

You continue to misunderstand this PR. I'd prefer to leave this to reviewers at this point. I appreciate you don't like my implicit criticism of #372 here.

[Shreyas4991]

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

You continue to misunderstand this PR. I'd prefer to leave this to reviewers at this point. I appreciate you don't like my implicit criticism of #372 here.

I would prefer criticism that was accurate and constructive and that actually improved my PR. Seeing as this was neither, and also making false claims about the problem being inherent to a free monad approach, but so blatantly supplying an instance to a Prog, yes I object. I also object to claims that this PR is better than 372 when 372's objectives are misunderstood.

[Shreyas4991]

This PR should be deleting other models and their examples. These can actually be used.

[Shreyas4991]

This should be a writer monad. A time counting monad is an additive log.

[Shreyas4991]

Again. This PR is deleting a file based on the presumption that it is no longer needed. I don't believe we have settled on deleting all other models in favour of this PR. My model builds on top of this PR. So this deletion rests on undecided assumptions and breaks other models.