Lightweight algorithms in CSLib :Cslib#275

Stream: CSLib

[Shreyas Srinivas]

Hi all,
After chasing some paper deadlines, I am back to finishing cslib#275. I am pruning the current code and reorganizing it so that we can review, merge, and use it soon. Concretely the PR will contain:

1. The Free Monad based query model
2. A standard query type for the Word RAM model
3. Example algorithms : OrderedInsert for lists, InsertionSort for lists, and MergeSort.

[Shreyas Srinivas]

I need some help getting this PR done, and there is room for contributions.

[Shreyas Srinivas]

I need help on two issues:

1. Help with aesop/grind annotations to simplify a bunch of proofs that consist of simp_all[<Monad or Free monad theorems>]
2. Help fixing a merge conflict that arises from a re-organisation

[Shreyas Srinivas]

3. If you can finish some of the complexity proofs, that is also great.

[Shreyas Srinivas]

Contributions can be made by PR to my PR branch. I prefer many smaller PRs to one large PR.

[Shreyas Srinivas]

The current status:

1. I now require Cost types to be AddCommSemigroups

[Shreyas Srinivas]

2. the ordered insert example requires completion of proofs
3. the merge part of mergeSort is mostly done. The proofs for mergesort remain

I also plan to reject unfiltered and unprocessed AI slop PRs . If you submit a proof, please be sure you can explain what's happening and please produce a readable and concise proofs. In that case and that case alone, I am open to AI use. In other words, controlled AI use is fine, especially for proofs. Uncontrolled use is not. If AI generates a big proof, try to factor it into smaller more abstract lemmas.

[Shreyas Srinivas]

actually never mind insertion sort. I am done with that. Only mergeSort remains.

[Johannes Tantow]

So, I opened two PRs, but you commited yourself later a result I PRed. I think however that the time complexity for merge should be xs.length + ys.length - 1 instead of your proposal as there are no comparisions when both are empty.

[Shreyas Srinivas]

I’m seeking help to get this done fast. But the idea is if I finish something, I’m taking that

[Shreyas Srinivas]

We are not only counting comparisons

[Shreyas Srinivas]

We are also counting pure operations.

[Shreyas Srinivas]

Also, fwiw I don’t see your PRs

[Shreyas Srinivas]

I think I’ll finish merge sort today if nobody else does.

[Johannes Tantow]

https://github.com/Shreyas4991/cslib/pull/2

[Shreyas Srinivas]

Why are you changing ListOrderedInsert

[Shreyas Srinivas]

I am done with that

[Johannes Tantow]

I wrote that yesterday

[Shreyas Srinivas]

I do like the brevity of some of your proofs

[Shreyas Srinivas]

But you only get them by changing purecost to 0

[Shreyas Srinivas]

I tried that. By I absolutely want to penalise pureCost by default

[Shreyas Srinivas]

That’s what makes many of these proofs tedious, but I am making a point that pure operations cannot sneak by

[Shreyas Srinivas]

The hbind pattern you see in my proof is repetitive

[Shreyas Srinivas]

So that’s going to become a lemma

[Shreyas Srinivas]

I consider it a plus of my approach that we spotted how badly the proofs behave when there is a nonzero purecost (which technically breaks monadic laws as far as Prog.time goes ). So now we know what extra API we need

[Johannes Tantow]

I don't really get how operations are counted in your model then. The return operation seems to count, but removing the head of the list does not count.

[Shreyas Srinivas]

It can’t count what goes on between monadic operations ofc. That limitation never goes away in any lightweight DSL

[Shreyas Srinivas]

My point is, somewhere along the way, you have to return the result.

[Shreyas Srinivas]

And we can count (or more accurately record) these returns. We could also log them in-principle.

[Shreyas Srinivas]

SortOpsCosts.pure could easily just be a log of what is returned at any point.

[Shreyas Srinivas]

pureCost allows a sanity check.

[Shreyas Srinivas]

I don’t mind scoped instances to keep purecost 0 for mergeSort. It’s more monadic and the three Prog.time lemmas kick in with grind and simp easily.

[Shreyas Srinivas]

But I would not have discovered that we need additional API lemmas if I hadn’t set them to non zero values

[Eric Wieser]

Shreyas Srinivas said:

The current status:

1. I now require Cost types to be AddCommSemigroups

What cost does pure have without a zero?

[Eric Wieser]

This PR also seems to have made a bad merge somewhere along the way and accidentally reverted a bunch of unrelated changes. I don't think it is a good use of time to review or improve this PR until you yourself have ensured that the diff contains nothing more than you intended.

[Shreyas Srinivas]

Eric Wieser said:

Shreyas Srinivas said:

The current status:

1. I now require Cost types to be AddCommSemigroups

What cost does pure have without a zero?

1 for basic number types by default. A slightly more sophisticated example is in ListOrderedInsert, where I explicitly count pures separately. In principle, this can be a logging type for pure operations

[Shreyas Srinivas]

Or even ListLinearSearch

[Shreyas Srinivas]

I'll first clean this PR up of every change that is not explicitly a part of it.

[Shreyas Srinivas]

I explicitly avoid AddCommMonoid because I want to allow non-zero pure costs as in the examples above.

[Shreyas Srinivas]

Where a zero is needed, we can always use an AddCommMonoid instance

[Eric Wieser]

Assigning a non-zero cost to pure makes your monad not lawful, right?

[Shreyas Srinivas]

For timing yes

[Shreyas Srinivas]

For evaluation, it’s still lawful

[Shreyas Srinivas]

I am open to the possibility of switching to 0 purecost by default while allowing nonzero costs when users wants it. But this means we still keep AddCommSemigroup.

[Eric Wieser]

I'm making the claim that no user should ever want a non-zero cost for pure, since the point in oracle computations is that only calling the oracle has a cost.

[Shreyas Srinivas]

my claim is that it’s beneficial to log pure operations or some function on them

[Shreyas Srinivas]

It’s a safeguard.

[Shreyas Srinivas]

It violates monad rules for time, but it gets us this ability to catch bad uses of pure.

[Eric Wieser]

Not really, since you can replace pure (pureFunc x) with irrelevantOracleCall >>= fun _ => pureFunc x if the cost of irrelevantOracleCall is less than pureCost

[Shreyas Srinivas]

It would have to be irrelevantOracleCall >>= fun _ => pure (pureFunc x) to be type correct wouldn’t it?

[Shreyas Srinivas]

The return type of the function on the rhs of >>= has to be a monad.

[Shreyas Srinivas]

Okay I’ll do one thing. I’ll set purecost to zero by default. I’ll leave insertionSort with its non-zero pure costs untouched for now, since they already work and serve as a good example.

[Shreyas Srinivas]

And I’ll also fix the PR mess.

[Shreyas Srinivas]

I want to get this merged asap. I am also including a canonical parametric word ram model. That’ll be like the final boss model. If someone is keen to show an implementable version on this model they can use reduceProg

[Shreyas Srinivas]

Most algorithms folks will be content with not going that far

[Eric Wieser]

I don't think adding more things to a contentious PR is an effective strategy for getting it merged ASAP

[Shreyas Srinivas]

Okay I’ll get to that later

[Shreyas Srinivas]

The PR is complete

[Shreyas Srinivas]

and ready for review.

[Shreyas Srinivas]

I have removed all mentions of pureCost for now. The main content is in the folder Cslib.AlgorithmsTheory. The old time monad is in a subfolder called Lean (as before)

[Shreyas Srinivas]

There are 4 complete examples:

1. Linear search in lists with the ListSearch query type.
2. Ordered Insertion in Lists using SortOps. This is used later in insertionSort
3. Insertion Sort in Lists using SortOps
4. Merge Sort in Lists using SortOps.

Other examples of queries and programs can be found in CslibTests. These are meant to be illustrative examples.

[Shreyas Srinivas]

The CI seems to be taking its time here : https://github.com/leanprover/cslib/actions/runs/22213745658/job/64253121530?pr=275

[Shreyas Srinivas]

The CI is stuck here for 5 minutes now. CSLib linters have already approved this PR. This seems to be a different set of linters:
Screenshot from 2026-02-20 07-32-38.png

[Shreyas Srinivas]

I don't know what's taking so long at file 32/119 in batteries

[Shreyas Srinivas]

Update

I have addressed all code-quality review comments. There are a couple of opinion-based design choices that have been brought up in the review. I'd like to keep Prog self-contained and I think trying to generalize TimeM to CostM and reducing Prog to CostM is not a good idea for three reasons:

1. Changes to TimeM are not in scope for this PR.
2. Even with this change Prog's models are more general than TimeM, see the example models of lists equipped with find when find is implemented respectively by linear search and binary search. Their complexity can depend on input size. Later we can reduce them to smaller models by reductions if someone likes that, but that's not strictly necessary. There is no option for this in either TimeM or the hypothetical CostM. This is a highlight of the query model in that I can encode complex queries whose cost is dependent on input size. It allows me to reason about algorithms using opaque queries to flow or cut algorithms in graphs for example and just substitute their known complexities.
3. Even if point 2 could be addressed, it would be a needless layer of indirection between Prog and its models, that adds nothing meaningful to Prog.

[Shreyas Srinivas]

About CI

It seems CI runs of preceding commits are not cancelled when a new commit lands in a PR. See example below @Chris Henson :
Screenshot from 2026-02-20 14-56-17.png

[Shreyas Srinivas]

I only see downsides in linking Prog to TimeM or its renamed version CostM.

[Shreyas Srinivas]

I personally vote for keeping Prog self-contained as it is already.

[Chris Henson]

For CI, we haven't set cancel-in-progress, but we can easily do so. The action for the text based linters is just slow to build, it's been on my todo list.

I'd like to emphasize that this is not my area of expertise, and I will mostly defer to @Eric Wieser and others who are more knowledgeable. It seems there are some ongoing discussions in the review.

That said, this seems to be something different from what we have previously discussed. Previously it seemed to me that you were suggesting that this would directly generalize and subsume TimeM, and I suggested scoping the PR to this change to cleanly show this. It has since grown to almost 1500 LoC, and proofs about merge sort are duplicated in this new framework. I personally might have opened a PR like this with just merge sort since this is all TimeM has. It also seems like this file (Cslib/AlgorithmsTheory/Lean/MergeSort/MergeSort.lean) is quite a bit longer than the TimeM equivalent.

I think it would be helpful to have a succinct description of exactly how these are meant to interact.

[Shreyas Srinivas]

They are not meant to interact. Prog makes no use of TimeM

[Shreyas Srinivas]

The mergeSort file is longer because I follow a proof style based on refinement. I take my programs and show that they are equivalent to functional-programming style lean versions, as far as correctness goes. For example merge and mergeNaive act on their inputs identically

[Shreyas Srinivas]

I am emphasising this style over a seemingly simpler approach because I think

1. it’s a healthy separation of concerns. Proofs of correctness of merge and mergeSort directly follow from their “naive” counterparts.

2. It emphasises the utility of proving correctness of functional versions of algorithms. If we already had the correctness proofs for mergeSort in pure lean code, all we’d need is to show their equivalence to the Prog version. I have been emphasising the need for correctness theorems for pure lean code algorithms for some time now. I hope this spurs the initiative now.

[Shreyas Srinivas]

Chris Henson said:

That said, this seems to be something different from what we have previously discussed. Previously it seemed to me that you were suggesting that this would directly generalize and subsume TimeM

Currently it does exactly that. In fact I prefer to keep it independent on TimeM, since it strictly supersedes it anyway.

[Shreyas Srinivas]

You can entirely delete TimeM and this PR would be perfectly fine.

[Shreyas Srinivas]

I just haven't done this because it is not my code. I leave it to you all to decide what happens to that code first.

[Shreyas Srinivas]

The 1500 lines of code come from several sources:

1. I provide a number of examples of query types and Progs in the CslibTests folder to teach this model
2. I have 3 additional fully worked out algorithms.
3. There is some code in specifying custom models, espcecially cost models.

[Shreyas Srinivas]

I hope that clarifies everything @Chris Henson

[Shreyas Srinivas]

I believe this model is sufficiently new to justify illustrating it with more than one example. We want these algorithms anyway.

[Eric Wieser]

I am of the belief that we should not be avoiding TimeM; we should be lifting into it with FreeM.liftM in order to compute outputs and costs simultaneously.

[Shreyas Srinivas]

As I have argued before, TimeM is not general enough and is pointless indirection.

[Shreyas Srinivas]

And it leaves us with two different lightweight methods of formalizing algorithms

[Eric Wieser]

Then let's first generalize TimeM, which is probably a 50 line diff

[Shreyas Srinivas]

From an algorithms theory perspective, I want to retain the flexibility to say "I am making calls to this opaque procedures with such and such inputs of such and such size". Like "make cut queries on this subgraph of this size", or "compute max flows in this subgraph"

[Shreyas Srinivas]

Even your generalized TimeM won't meet that. And I still maintain that this indirection is bad.

[Eric Wieser]

Why is the indirection worse than duplicating the logic of FreeM.liftM and TimeM inside your Prog code?

[Shreyas Srinivas]

I don't understand your question mark

[Eric Wieser]

The message seems irrelevant to the point; you get what it asks for with Prog whether or not we use TimeM as an intermediary.

[Shreyas Srinivas]

I want time complexity to depend on input size to the query. I don't see how to make that happen in TimeM. The model is designed to increment its cost by a constant amount.

[Shreyas Srinivas]

And the way I see it, Prog is currently completely self-contained. It sits on top of FreeM.

[Eric Wieser]

Non-constant amounts work just fine with TimeM. It will be easy to show you with an example once we generalize TimeM to AddCommMonoid, and the diff will be smaller than this conversation

[Eric Wieser]

(which to be very clear, I'm advocating we do in a separate PR, first)

[Shreyas Srinivas]

Well, I don't know how to make it work. I spent a lot of time figuring out the exact type signature of queries and evalQuery and cost

[Eric Wieser]

If it turns out you're right after all and TimeM is an annoyance we can always delete it later after generalizing

[Shreyas Srinivas]

Sounds complicated :sweat_smile:

[Shreyas Srinivas]

We have a fully working solution now that .... works well.

[Eric Wieser]

"I have already written my code and I like it" is not a particularly compelling defense in isolation

[Shreyas Srinivas]

I am not a fan of the TimeM approach because it allows arbitrary annotations in the first place.

[Shreyas Srinivas]

That's a huge issue that I am trying to mitigate here. Relying on TimeM also means keeping the ability to write code with ticks (pun intended).

[Shreyas Srinivas]

I have already covered the mergeSort example that TimeM has. At this point my PR is a strict super set of TimeM, even in terms of algorithms we have in the repository. Whatever decision we reach w.r.t TimeM, we make it harder by introducing unnecessary downstream dependencies.

[Shreyas Srinivas]

Eric Wieser said:

"I have already written my code and I like it" is not a particularly compelling defense in isolation

This is about not introducing unnecessary dependencies. Especially having a more general concept depend on a less general one.

[Shreyas Srinivas]

If anything, TimeM should be refactored as a special case of Prog, with the mergeSort example implemented in it...which I have already done (i.e. implemented mergeSort).

[Shreyas Srinivas]

At least, I don't see any reason to take a perfectly functional approach Prog and bend it backwards just because we want to use an existing piece of code, which is clearly not necessary for Prog. It's a pointless dependency and therefore bad design.

[Shreyas Srinivas]

If someone wants to pursue this complication and potential revert, please do so and feel free to refactor this PR. I'd like to preserve the current state somehow (EDIT : done ). As far as I am concerned, it has reached a point of Pareto-optimality in design for its purposes with just the right amount of simplicity, generality, and underlying dependencies. It has kept its promise of being a strict superset of TimeM without depending on it, and allowing things TimeM doesn’t.

[Shreyas Srinivas]

If we create a dependency on TimeM, we will continue to get PRs on top of it. This is an unnecessary doubling of effort.

[Eric Wieser]

Eric Wieser said:

Non-constant amounts work just fine with TimeM. It will be easy to show you with an example once we generalize TimeM to AddCommMonoid, and the diff will be smaller than this conversation

https://github.com/leanprover/cslib/pull/357 does the generalization

[Shreyas Srinivas]

Refactoring cslib#275 might prove a headache. I still don't see why we need to go through another Monad.

[Eric Wieser]

I think it will be trivial and the refactor will make the code shorter

[Shreyas Srinivas]

Also this directly contradicts my guarantee that TimeM is strictly superseded

[Shreyas Srinivas]

Because @Chris Henson at one point wanted to fix on default model for lightweight algorithms

[Shreyas Srinivas]

Now we are going to end up with two.

[Eric Wieser]

The total number of models after CSLib#357 is still one.

[Shreyas Srinivas]

That's because there Prog hasn't been merged

[Shreyas Srinivas]

The tick model is still a more loose model and it will now exist side-by-side with Prog once that is merged. So people will be duplicating work in two models.

[Shreyas Srinivas]

anyway, I am not doing this refactor. I hope the test models in CslibTests/QueryModel work. I included them explicitly as an example of how the same query type can have two different models with two different costs for the same operation.

[Shreyas Srinivas]

My preferred solution is to delete TimeM and stick withProg (or maybe delete Prog and stick with TimeM, naturally I am biased towards my approach, albeit with sound reasons).

[Shreyas Srinivas]

Two lightweight models = either

1. Duplication of algorithms, or
2. People pick the easier one, at the cost of formalization quality/usability in algorithms code.

[Shreyas Srinivas]

Fwiw I made a separate frozen branch called query-complexity-model-ideal-state to preserve what I did : https://github.com/Shreyas4991/cslib/tree/query-complexity-model-ideal-state

[Chris Henson]

(link to Eric's PR is cslib#357)

[Shreyas Srinivas]

I can see optimizations in the time complexity side of cslib#275 if your PR goes through, because we may not need all those FreeM composition lemmas (or maybe we need lifting lemmas for FreeM.liftBind, bind, and pure). I still maintain linking Prog to TimeM is a terrible idea. A strictly better solution that still allows those optimizations would be to have Prog.time lift Model.cost to Writer Cost. It will still leave us independent of TimeM, and maybe give us access to more lemmas.

[Shreyas Srinivas]

The biggest optimizations in the proof length can come from golfing my existing proofs since I have a habit of writing lean proofs like a late-2024 LLM anyway.

[Eric Wieser]

WriterT is probably too annoying to use since it forces the cost to be multiplicative. If we fix that in mathlib then I agree that it could replace TimeM

[Shreyas Srinivas]

I can make that PR. I don't know how long it will linger in mathlib's review queue. Typical wait time seems to be 1 month.

[Shreyas Srinivas]

It was easy : https://github.com/leanprover-community/mathlib4/pull/35578
Only the Cont monad uses WriterT in mathlib

[Eric Wieser]

I think you need consensus on Zulip that it's a good idea first

[Eric Wieser]

Maybe ping the previous thread you made now that the PR exists

[Shreyas Srinivas]

Okay. I don't recall making one. But I don't see why this should be a controversial change. This is the meaning of a writer monad.

[Eric Wieser]

Both the current and proposed versions are, the difference is a mathlib-ism

[Eric Wieser]

Let's not discuss this here, please try to find your old thread

[Shreyas Srinivas]

I am willing to go to some lengths to avoid dependency on TimeM because whatever decision is reached on its fate (whether it will be "the" model of lightweight algorithms or the opposite), I don't want the decision to be linked to its usage in Prog. Further as I have said before, conceptually the dependency is both extraneous and flawed.

[Shreyas Srinivas]

I also promised @Chris Henson that Prog doesn't need TimeM and as far as I can help it, I have kept it.

[Shreyas Srinivas]

I think we have optimised cslib#275 substantially now

[Shreyas Srinivas]

It has gone from ~1500 lines to about ~1100 lines

[Shreyas Srinivas]

It now piggybacks off the TimeM infrastructure as if it were the writer monad (tick = tell)

[Eric Wieser]

This PR is starting to become unwieldy with the number of review comments, especially as I don't have the pemission to resolve the ones that have been addressed.

[Chris Henson]

Hey, Eric. Thanks so much for the review work. I didn't realize you didn't already have permission to even resolve comments. I'm going to ping the maintainer channel about this.

[Shreyas Srinivas]

Update : This PR has been thoroughly vetted and refined. I hope we can get this merged fast. I can’t see any technical reasons to wait.

I hope to continue building on it with confirmation that it has been merged. There are several obvious further additions for subsequent PRs that I hope to pursue very soon after the merge. For one thing: a RAM model type parametrised by a word type.

[Shreyas Srinivas]

It has exactly what it needs to start collecting algorithms and models and even reductions between models.

[Shreyas Srinivas]

Another update

Here's a compressed PR with no comment history for ease of further reviewing : cslib#372

[Shreyas Srinivas]

CC : @Chris Henson

[Shreyas Srinivas]

I hope this speeds up review and merge. This PR has been pending for a while. It would be greatly helpful to me if we could get this done asap.

[Shreyas Srinivas]

Update

@Chris Henson has approved this PR and I have addressed his and Eric's comments. Is there anything I can do to accelerate to a merge? CC : @Fabrizio Montesi

[Tanner Duve]

Great work!I'm happy to see this

[Shreyas Srinivas]

Thanks. I have plans for future PRs that this approach specifically allows us to explore. I would love to invite everyone to contribute.

1. Defining a query type for RAM models parametrised by a word type.
2. Instantiations to $\mathbb{R}$ and bitvecs of a fixed size w to get the Real RAM and w-word RAM models

[Shreyas Srinivas]

3. Reductions from custom queries all the way down to one of these models.

4. Straight-Line programs as a query type for circuits (Boolean/arithmetic)

5. a TM query type for Turing machines.

6. Basic algorithms in sufficiently abstract and minimal query types chosen per the problem setting.

[Shreyas Srinivas]

A careful formulation of the RAM model should also allow discussing space complexity in this framework. This in turn might suggest ways to work with space complexity (by allowing only the use of allocated objects, and cost functions that assign space depending on object allocated)

[Tanner Duve]

Sounds good I can definitely contribute to this

[Shreyas Srinivas]

I am hoping it gets merged soon. I still have my code for straight line circuits and ID marked progrms that I deleted from the PR to keep it small.

[Fabrizio Montesi]

I'm happy to look at this again in the coming week. I need to sort out where to put some things (that's minor). I'd also like a high level overview of all the proposed approaches, to direct people effectively. I'll open a separate thread for that.

[Shreyas Srinivas]

It’s ready for merging fwiw. I hope we can start inviting contributors already

[Shreyas Srinivas]

I am at workshop where people are interested in doing so.