Separation Logic

Stream: Program verification

[Shreyas Srinivas]

Do we have a library for separation logics in lean? Apparently there are quite a few in Coq. I attended a talk today where the speaker was talking about program synthesis and verifying the synthesised program. For complicated pre and post conditions, their synthesis tool translates to Coq and generates lemmas (and even some proofs). The speaker mentioned that one of the critical issues was that Coq insisted on constructive proofs only and this was an obstacle for proof synthesis.

[Shreyas Srinivas]

I asked if this issue disappears if constructivism is not a constraint. For e.g. : Lean's tactics seem to take a more laissez faire approach with the use of classical logic.

[Shreyas Srinivas]

The speaker said that this might be an interesting question to explore but he was unaware of any library for separation logics in lean.

[Ira Fesefeldt]

I do plan to work on a flavor of separation logic in lean, but I am not aware of any previous work in lean. Most work on separation logic I encountered was either in coq or isabelle.

[Shreyas Srinivas]

I am starting some work on this as well. This might potentially tie into my work on circuits (reinterpreting certain stateful parts of a circuit).

[Mario Carneiro]

https://github.com/larsk21/iris-lean is a separation logic framework in lean

[Sebastian Ullrich]

Shreyas Srinivas said:

Coq insisted on constructive proofs only

For what it's worth, I'm pretty sure "insisted" is way too strong here

[Karl Palmskog]

most high-level proof automation in Coq supports using LEM, for example, itauto uses NNPP whenever the Classical_Prop module is loaded

[Karl Palmskog]

arguably the most famous Coq project, CompCert, uses LEM and some other axioms like functional extensionality (at least last I checked). In my experience, serious Coq users value having the choice of using LEM or not, but if they insist on anything, it's declaring your axiom choices up front (rather than staying constructive in itself)

[Shreyas Srinivas]

Interesting. The speaker did admit to not being aware about the exact place where constructivism was an obstacle (he mentioned that he has a PhD student who does the coq stuff)

[Shreyas Srinivas]

But could this be an issue with specific libraries or tactics?

[Karl Palmskog]

to my knowledge, CoqHammer's sauto (https://coqhammer.github.io/#sauto) was developed from the start as a constructive first-order solver, so LEM is just another axiom to it without much bells and whistles. There are probably some LEM-specific optimizations you can do in a hammer system that weren't done in CoqHammer

[Shreyas Srinivas]

Is it true that this repository is not maintained anymore?
Mario Carneiro said:

https://github.com/larsk21/iris-lean is a separation logic framework in lean

[Mario Carneiro]

It is. It was a student project and the student graduated

[Mario Carneiro]

I would like to see work on it continue though

[Alex Keizer]

I'm quite interested in separation logic and would love to continue that work. I just worry about whether it would be novel enough to incorporate into my PhD topic and would find it hard to find the time to work on it if not

[Ira Fesefeldt]

Mario Carneiro said:

https://github.com/larsk21/iris-lean is a separation logic framework in lean

I have again looked into this project. It seems, it is currently not compatible with mathlib4, since they use incompatible versions. Are there plans to upgrade iris-lean at some point? Maybe when mathlib4 uses a stable lean4 version again?

[Mario Carneiro]

I don't think there is much sense in holding out for a stable version, you might pass a few important stages of life before seeing it happen

[Mario Carneiro]

It just needs periodic upkeep, like any other project

[Ira Fesefeldt]

I am quite weak in this meta programming... But I like to have the power of mathlib for doing real arithmetic with separation logic. So I guess I now either learn how to upgrade this project or switch to coq :D

[Andrés Goens]

I had a quick look and it seems like fairly non-trivial meta programming stuff indeed. Some issues were simple to fix and I started here: https://github.com/goens/iris-lean/commit/fab0b67d3c4a1d65f1e7c51a0e14f0e66500ed03 but I'm also stumped by a timeout and type error I got from it:

error: > LEAN_PATH=./build/lib DYLD_LIBRARY_PATH=/Users/goens/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/lib:./build/lib /Users/goens/.elan.arm/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean ././src//./Iris/BI/Interface.lean -R ././src//. -o ./build/lib/Iris/BI/Interface.olean -i ./build/lib/Iris/BI/Interface.ilean -c ./build/ir/Iris/BI/Interface.c
error: stdout:
././src//./Iris/BI/Interface.lean:52:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
././src//./Iris/BI/Interface.lean:132:67: error: type expected, got
  (Ψ a : car)
././src//./Iris/BI/Interface.lean:133:44: error: type expected, got
  (Ψ a : car)

Maybe @Sebastian Ullrich might have a good overview of what happened, as he also supervised the person who did this?

[Ira Fesefeldt]

Andrés Goens said:

I had a quick look and it seems like fairly non-trivial meta programming stuff indeed. Some issues were simple to fix and I started here: https://github.com/goens/iris-lean/commit/fab0b67d3c4a1d65f1e7c51a0e14f0e66500ed03 but I'm also stumped by a timeout and type error I got from it:

error: > LEAN_PATH=./build/lib DYLD_LIBRARY_PATH=/Users/goens/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/lib:./build/lib /Users/goens/.elan.arm/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean ././src//./Iris/BI/Interface.lean -R ././src//. -o ./build/lib/Iris/BI/Interface.olean -i ./build/lib/Iris/BI/Interface.ilean -c ./build/ir/Iris/BI/Interface.c
error: stdout:
././src//./Iris/BI/Interface.lean:52:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
././src//./Iris/BI/Interface.lean:132:67: error: type expected, got
  (Ψ a : car)
././src//./Iris/BI/Interface.lean:133:44: error: type expected, got
  (Ψ a : car)

Maybe Sebastian Ullrich might have a good overview of what happened, as he also supervised the person who did this?

I believe the code there takes roughly 30 seconds to process. And thus is catched by the timeout of 20 seconds. At least for me, using exactly what is written in the error as solution works. Setting maxHeartbeats to e.g. 400000 solves the error.

[Ira Fesefeldt]

(Although there are still other errors, which I did not solve yet)

[Ira Fesefeldt]

Unfortunately I am also stuck with the next error:

error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=./build/lib /home/phoenix/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean ././src//./Iris/Proofmode/Classes.lean -R ././src//. -o ./build/lib/Iris/Proofmode/Classes.olean -i ./build/lib/Iris/Proofmode/Classes.ilean -c ./build/ir/Iris/Proofmode/Classes.c
error: stdout:
././src//./Iris/Proofmode/Classes.lean:20:11: error: cannot find synthesization order for instance @AsEmpValid1.bi with type
  {φ : outParam Prop} → {PROP : Type} → (P : PROP) → [self : AsEmpValid1 φ P] → BI PROP
all remaining arguments have metavariables:
  @AsEmpValid1 ?φ PROP ?P
././src//./Iris/Proofmode/Classes.lean:21:11: error: cannot find synthesization order for instance AsEmpValid2.bi with type
  (φ : Prop) → {PROP : outParam Type} → {P : outParam PROP} → [self : AsEmpValid2 φ P] → BI PROP
all remaining arguments have metavariables:
  @AsEmpValid2 ?φ PROP ?P
././src//./Iris/Proofmode/Classes.lean:25:2: error: cannot find synthesization order for instance @AsEmpValid.toAsEmpValid1 with type
  {φ : Prop} → {PROP : Type} → {P : PROP} → [self : AsEmpValid φ P] → AsEmpValid1 φ P
all remaining arguments have metavariables:
  @AsEmpValid ?φ PROP P
././src//./Iris/Proofmode/Classes.lean:25:2: error: cannot find synthesization order for instance @AsEmpValid.toAsEmpValid2 with type
  {φ : Prop} → {PROP : Type} → {P : PROP} → [self : AsEmpValid φ P] → AsEmpValid2 φ P
all remaining arguments have metavariables:
  @AsEmpValid φ ?PROP ?P
././src//./Iris/Proofmode/Classes.lean:29:55: error: typeclass instance problem is stuck, it is often due to metavariables
  BIBase ?m.360

What does "cannot find synthesization order for instance" even mean?

[Kevin Buzzard]

You can search this Zulip for that phrase, but it usually means "this is not a good instance because it will never fire" (e.g. because it needs information not available to the typeclass inference system). I didn't look at your exact problem though, so treat this advice with a pinch of salt.

[Ira Fesefeldt]

I just found that too, thanks!

The solution to deactivate the option synthInstance.checkSynthOrder does remove all errors except for the last one. I.e.

error: stdout:
././src//./Iris/Proofmode/Classes.lean:31:55: error: typeclass instance problem is stuck, it is often due to metavariables
  BIBase ?m.360

[Sebastian Ullrich]

We did have to adjust the Coq typeclasses a bit during porting because Coq's typeclass system is much more "free-form", but they might still not quite conform to Lean expectations. We definitely should not ignore those errors.

[Ira Fesefeldt]

That the last exception remains (in a similar form) is also an indicator for me that the errors are not spurious