Loom discussion

Stream: Loom

[Jeremy Tan]

cf. #announce > Loom: framework for Multi Modal program verifiers in Lean @ 💬

I have to admit, I'm part of this lab (but I just joined, so no work from me in Loom yet).

This is the discussion thread for Loom.

[(deleted)]

Amazing. Are SMT proofs compiled into Lean or are they just blindly trusted :eyes:

[(deleted)]

If everything is verified by the Lean kernel then I'm using Loom

[Shreyas Srinivas]

I think you can do both, based on working with Veil 1.0. Proof reconstruction would be slower

[Shreyas Srinivas]

Question : I already asked this once in a video chat and got a positive-ish but brief answer back then. So I’ll ask again to hopefully get a detailed answer. It appears that one could in principle reason about resource usage by using the right kind of monad here. Possibly time and space complexity as well. Is this right?

[Shreyas Srinivas]

Another question, slightly related : this seems like a good candidate language for use with CSLib. Is this so?

[Jeremy Tan]

The main thing I intend to do in my PhD is formalising computational complexity, and apply the tools thus produced to CLRS. The resulting proofs may or may not enter CSLib

[Jeremy Tan]

Huỳnh Trần Khanh said:

Amazing. Are SMT proofs compiled into Lean or are they just blindly trusted :eyes:

Loom uses the auto package for SMT, so auto.smt enables or disables SMT use, and auto.smt.rconsProof allows you to reconstruct the proof in pure Lean (assuming the SMT backend supports it)

[Shreyas Srinivas]

Jeremy Tan said:

The main thing I intend to do in my PhD is formalising computational complexity,

Then we have something in common. Once you allow monadic reasoning with some notion of ghost states, reasoning about computational complexity becomes feasible for many but not all computational models (i.e. not just a specific RAM model)

[Vladimir Gladstein]

Huỳnh Trần Khanh said:

Amazing. Are SMT proofs compiled into Lean or are they just blindly trusted :eyes:

Hey! I guess your question has been responded already but let me add something. Loom is agnostic to the automation tactic which is called on produced goals. In Velvet we use lean auto and lean smt. The latter one supports proof reconstruction reducing TCB to Lean kernel.
You can also dynamically link the automation tactic to grind or aesop too. In our latest experience grind solves almost all our goals. More information you can find in github README

[Vladimir Gladstein]

Shreyas Srinivas said:

Question : I already asked this once in a video chat and got a positive-ish but brief answer back then. So I’ll ask again to hopefully get a detailed answer. It appears that one could in principle reason about resource usage by using the right kind of monad here. Possibly time and space complexity as well. Is this right?

Great question! We are doing some preliminary research in this direction. For example we have already verified complexity of merge sort. I hope soon we will release this part of project too

[Vladimir Gladstein]

Shreyas Srinivas said:

Another question, slightly related : this seems like a good candidate language for use with CSLib. Is this so?

I think CSLib is not yet completely sure what framework to use. But as far as I know they might have done some experiments using Velvet :muscle:

[Shreyas Srinivas]

Vladimir Gladstein said:

Shreyas Srinivas said:

Question : I already asked this once in a video chat and got a positive-ish but brief answer back then. So I’ll ask again to hopefully get a detailed answer. It appears that one could in principle reason about resource usage by using the right kind of monad here. Possibly time and space complexity as well. Is this right?

Great question! We are doing some preliminary research in this direction. For example we have already verified complexity of merge sort. I hope soon we will release this part of project too

Will it feature the ability to choose a custom cost model? In the CSLib presentations about Boole, it was mentioned that the cost model was fixed. In research level TCS, being able to count a selection of operations is very useful. Things like “This procedure makes O(f(n)) matrix multiplication calls” and so we can connect things to the matrix multiplication constant (which we still only have upper and lower bounds for).

[Vladimir Gladstein]

Shreyas Srinivas said:

Vladimir Gladstein said:

Shreyas Srinivas said:

Question : I already asked this once in a video chat and got a positive-ish but brief answer back then. So I’ll ask again to hopefully get a detailed answer. It appears that one could in principle reason about resource usage by using the right kind of monad here. Possibly time and space complexity as well. Is this right?

Great question! We are doing some preliminary research in this direction. For example we have already verified complexity of merge sort. I hope soon we will release this part of project too

Will it feature the ability to choose a custom cost model? In the CSLib presentations about Boole, it was mentioned that the cost model was fixed. In research level TCS, being able to count a selection of operations is very useful. Things like “This procedure makes O(f(n)) matrix multiplication calls”

Honestly, I cannot tell for sure at this point. But thanks for the question! We will definitely consider accounting for different cost models

[Shreyas Srinivas]

Another question : I recall that a key feature was the ability to prove functional equivalence between the imperative and functional definitions of a function, which makes the invariants nicer. Is this in one of the examples in the repository?

[Vladimir Gladstein]

Shreyas Srinivas said:

Another question : I recall that a key feature was the ability to prove functional equivalence between the imperative and functional definitions of a function, which makes the invariants nicer. Is this in one of the examples in the repository?

Yes, you can check out chapter 8 of the paper and look for this file https://github.com/verse-lab/loom/blob/master/CaseStudies/Velvet/VelvetExamples/SpMSpV_Example.lean

[Shreyas Srinivas]

One more question: Where can I find Veil 2.0?

[Vladimir Gladstein]

Shreyas Srinivas said:

One more question: Where can I find Veil 2.0?

@George Pîrlea ?

[Vladimir Gladstein]

Shreyas Srinivas said:

One more question: Where can I find Veil 2.0?

@George Pîrlea ?

[George Pîrlea]

@Shreyas Srinivas If you want to look at the version of Veil submitted along with the POPL paper, check out the popl26-artifact branch in the Veil repo.

That said, Veil 2.0 is not yet publicly released — we are working on more features (and UX polish) compared to the POPL version and our plan is to release it in the new few weeks, hopefully by the end of the month.

There will be a separate announcement about that :slight_smile:

[Bas Spitters]

How does Loom compare/relate to std.do ? And to iris-lean ?
I didn't have time to read the paper yet...

[Vladimir Gladstein]

Bas Spitters said:

How does Loom compare/relate to std.do ?

Hey! In the announcement tried briefly mention the biggest difference between Loom and std.do: In Loom we focus on intrinsic (annotations based) proofs whereas std.do develops the whole set of tactics and a custom proof-mode to reason about monadic computations extrinsically.
Broadly speaking, on the metatheory level Loom complements std.do with first 4 new features mentioned in announcement: multi-modal verification, intrinsic proof style, reasoning about termination and monad transformer for non-determinism. Please refer to the announcement for more details.
That's said two frameworks are not compatible at this point, but we are exploring ways for possible collaboration.

And to iris-lean ?

As far as I am concerned, the main goal of iris-lean is optimising for iris level of generality. In Loom, our main concern is automation. For example, Loom doesn't support concurrency at this point, but VCs it generates are SMT-friendly. Of course, we are working towards framework generalisations, but our main priority is reducing manual proof effort to minimum.

[Markus de Medeiros]

So exciting! I saw a demo of this a couple months ago and I've been waiting to play around with it ever since.

I concur with your comparison to iris-lean--more specifically, a fairly central difference is that Iris-style logics can support deeply-embedded languages (ie. small-step semantics) that might not easily fit into the monadic framework. There is some work on automating some parts of Iris with SMT, but I have the sense that a tool as cohesive as Loom would not be possible in Iris's complete generality.

I asked Ilya about this a while ago but I'm wondering if there's any new info: have you folks experimented with using noncomputable monads in this framework? Specifically, something like a probability monad?

[Bas Spitters]

Thanks @Vladimir Gladstein ! Hi @George Pîrlea ! This looks interesting.

Do I understand correctly that your definition of "intrinsic" means fully automatible? (https://verse-lab.github.io/papers/loom-preprint.pdf)
In that case, could you help me understand your preference for SMT-solvers in Lean?
I understand the wish for automation, but I believe one of the motivations for Lean was precisely a more fluent combination between SMT and ITP.
This has, at least partially, been realized by lean-smt, grind, hammer, ...
So, there appears to be a fragment where @Sebastian Graf 's std.do is "intrinsic", but I may be misreading your paper.

This may be related to your comparison with Dijkstra Monads (https://verse-lab.github.io/papers/loom-preprint.pdf#page=25.12). You say that they are not always SMT-friendly.
Did you consider the more general question of whether it is automation-friendly (e.g. using hammer)?

Incidentally, we've been working on Hax, a "multimodal" framework for Rust verification, which has a {F*,Rocq,lean} backends, but also connects to the Dijkstra monad framework with SSProve. https://hax.cryspen.com/publications/

[George Pîrlea]

@Markus de Medeiros We haven't done much work in this regard yet, but we're planning to look at probability in the near future. We have a decent idea of how it would work. @Vladimir Gladstein would be the one to ask for specific details if you're interested.

[Bas Spitters]

@Markus de Medeiros which probability monad? We have them in the Dijkstra monad framework in SSProve (https://github.com/SSProve/ssprove). In Rocq, but the theory should carry over to Lean. The discrete probabilities is computable, so maybe you are interested in continuous distributions?

[Shreyas Srinivas]

I think Markus might be talking about https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/ProbabilityMassFunction/Monad.html

[Shreyas Srinivas]

But even otherwise, there are many situations where it is important and useful to reason with programs that use certain noncomputable operations as primitives

[Shreyas Srinivas]

Geometric computations with Real RAM and continuous fair division problems come to mind as examples. Oracle computations where we don’t know or care about the implementation of the oracles might be another example.

[George Pîrlea]

@Bas Spitters By intrinsic we mean that the annotations (pre-post specifications and loop invariants) are inline with the program source. This is often closely like with full automation, but strictly speaking is a different concept. In particular, auto-active verifiers like Dafny often require additional "helper" assertions to guide the SMT solver towards finding the proof in particular cases. Instead, with Velvet (the Dafny-like verifier built on Loom), you'd get these cases as goals you can solve interactively.

[George Pîrlea]

And we do use grind, which sometimes solves goals on which CVC5 times out. aesop also proves useful from time to time.

[George Pîrlea]

FWIW, here's an interesting blog post talking about the 'intrinsic' vs 'extrinsic' terminology: https://joomy.korkutblech.com/posts/2024-10-30-intrinsic-vs-extrinsic-verification.html

[Bas Spitters]

Thanks @Shreyas Srinivas ! These PMF/ discrete probabilities appear to be computable, althought the particular formalization in (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/ProbabilityMassFunction/Basic.html#Probability-mass-functions) may not be.

[George Pîrlea]

In that case, could you help me understand your preference for SMT-solvers in Lean?

To answer this more directly: we do not have a preference for SMT over other kinds of automation. Any automation that works is great in our book, and we're very excited about grind in particular :slight_smile:

[Shreyas Srinivas]

Bas Spitters said:

Thanks Shreyas Srinivas ! These PMF/ discrete probabilities appear to be computable, althought the particular formalization in (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/ProbabilityMassFunction/Basic.html#Probability-mass-functions) may not be.

So the implementation relies on expressing probabilities in terms of mathlib docs#ENNReal

[Shreyas Srinivas]

Operations on this type are almost always noncomputable in the lean sense as well as decidability sense

[Bas Spitters]

Thanks @George Pîrlea. I was aware of the distinction in type theory, but I didn't remember the terminology extended to imperative languages.

[Bas Spitters]

@Shreyas Srinivas yes, I agree, the mathematical concept of PMF is computable, but the mathlib formalization is not.

[Sebastian Graf]

FWIW, MPL (the prototype library that inspired Std.Do) used to have prototypical intrinsic verification syntax for do as well:

abbrev fib_spec : Nat → Nat
| 0 => 0
| 1 => 1
| n+2 => fib_spec n + fib_spec (n+1)

def fib_impl (n : Nat) : Idd Nat
  ensures r => r = fib_spec n
:= do
  if n = 0 then return 0
  let mut a := 0
  let mut b := 1
  invariant xs => a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)
  for _ in [1:n] do
    let a' := a
    a := b
    b := a' + b
  return b

However, the implementation is a huge hack. At the FRO we decided to postpone having intrinsic verification syntax until do elaboration becomes extensible. Hence I'll be working on a rewrite of the do elaborator this quarter, allowing users to extend do notation by writing custom do element elaborators such as for invariant above.

We are also planning towards generalizing the semantic foundations (i.e., WPMonad, Assertion) of Std.Do enough so that Loom won't need to rewrite everything from scratch. Probabilistic assertions (α -> Real instead of α -> Prop) are on our radar, too.

[Shreyas Srinivas]

@Sebastian Graf : concretely, what does making do notation more extensible mean? What will we be able to do?

[Sebastian Graf]

It means you can define custom do elaborators. Roughly

syntax (name := doIf) "if " term " then " doSeq (" else " doSeq)? : doElem

@[doElem_elab doIf]
meta def elabElem (syn : Syntax) (k : DoElemCont) : DoElabM Expr :=
  match syn with
  | `(dooElem| if $cond then $thenDooSeq $[else $elseDooSeq?]?) =>
    k.withDuplicableCont fun k => do
      let then_ ← elabElems1 (getDooElems thenDooSeq) k
      let else_ ← match elseDooSeq? with
        | none => k.continueWithUnit dooElem
        | some elseDooSeq => elabElems1 (getDooElems elseDooSeq) k
      let then_ ← Term.exprToSyntax then_
      let else_ ← Term.exprToSyntax else_
      Term.elabTerm (← `(if $cond then $then_ else $else_)) none
  | _ => throwUnsupportedSyntax

DoElabM builds on TermElabM and allows for duplicating continuations (i.e., introducing join points as needed), getting a hold of the let mut vars, etc.

[Vladimir Gladstein]

Markus de Medeiros said:

a fairly central difference is that Iris-style logics can support deeply-embedded languages (ie. small-step semantics) that might not easily fit into the monadic framework.

That’s right! I guess monadic frameworks can do deep embeddings to some extent with iTress like in https://maxv.dk/program_logics_a_la_carte.pdf. But of course you need to do extra work if you want to embed your language into monadic framework.

as for non-computational monads: you can read on section 6 of the paper where we work with non-determinism monads. Basically you can instantiate Loom whenever your assertion language is Complete Lattice. As far as I know, pre-expectations is a Complete Lattice, so I don’t immediately see obstacles to work with Probabilities. Thats said, we have not tried it yet! But we are looking into it rn

[Notification Bot]

This topic was moved here from #general > Loom discussion by Kim Morrison.