Translating programs with `pre` `post` conditions to Lean 4.

Stream: lean4

[Raúl Raja Martínez]

Hi all, I'm new to Lean and currently in my first steps learning about it for about a week now.
I'm new to theorem provers in general and looking more to see what capabilities Lean has around the verification of programs.
I'm trying to encode the following F* lang example in Lean 4 but I'm having trouble expressing pre and post conditions in the increment function.

module Example

let increment (x:int{x > 0}): y:int{y > x} =
    x + 1

let incrementTest = assert (increment 47 = 48)

I tried several approaches without success to encode Type -> Prop and even followed some threads here where folks where discussing Hoare state monads for something similar but I have not been able to get any results yet.

Is this kind of analysis possible with Lean 4? My use case is to provide something similar to what we are doing in https://arrow-kt.io/docs/analysis/ but that instead of using Z3 as backend it uses Lean 4. I'm currently exploring if this is possible and what kind of messages would Lean4 raise when pre/post/invariants are not satisfied.

thanks for any help or pointers in the right direction :)

[Tomas Skrivan]

The function can look like this:

def increment (x : {y : Int // y > 0}) : {y : Int // y > x.1} := ⟨x.1 + 1, sorry⟩

where you replace sorry with a proof of x.1 + 1 > x.1 which is some basic lemma about inequality and addition, but I do not remember the name now.

However, with this approach the pre/post invariants are always satisfied, because you have formal proofs of them. Thus running the assert is kind of meaningless.

[Tomas Skrivan]

But I can imagine that something like the F* example can be cooked up.

Something like:

def TypeWithAssert (T : Type) (P : T -> Prop) := T

def assert {T P} [forall y, Decidable (P y)] (x : TypeWithAssert T P) : Bool := P x

def increment (x : TypeWithAssert Int (forall y, y > 0) : TypeWithAssert Int (forall y, y > x) := x + 1

#eval assert (increment 47) -- true

(I'm on a phone, none of this is tested so it might require some modifications)

[Tomas Skrivan]

I'm pretty sure that some custom notation for binders would allow for notation like (x : Int{ x > 0 }).

One question is if TypeWithAssert should be def or abbrev.

[Wojciech Nawrocki]

It's important to point out that the approach to verification in F⋆ is totally different than in Lean. In F⋆, the condition x+1 > x is checked by Z3, the underlying SMT solver, so you don't have to prove it manually. In Lean you have to do it by filling in the sorry, as Tomas suggested. In Lean the proof is checked by a small, trusted kernel, whereas in F⋆ the Z3 output is trusted. In practice this means that in F⋆ it can often be easier to prove things (it can also be harder when Z3 misbehaves) but any bug in Z3 compromises soundness of the system (in that case the "proofs" are not really proofs), whereas in Lean you have to convince the kernel that your desired properties hold but when you do manage that, they are far less likely to be unsound.

[Wojciech Nawrocki]

The lean-smt project is aiming to take some of the proofs produced by SMT solvers such as Z3 and convince the Lean kernel that they are correct. This would give the best of both worlds - SMT proves properties automatically but the kernel certifies soundness.

[Raúl Raja Martínez]

Thanks @Tomas Skrivan I got your example to compile with this code but the #eval results returns true for -99 which is not bigger than 0. For example:

abbrev TypeWithAssert (T : Type) (P : T -> Prop) := T

def assert {T P} [forall y, Decidable (P y)] (x : TypeWithAssert T P) : Bool := P x

def increment (x : TypeWithAssert Int (fun x : Int => x > 0)) : TypeWithAssert Int (fun y : Int => y > x) := x + 1

#eval assert (increment (-99)) -- true

Thanks @Wojciech Nawrocki I'll check out lean-smt looks like it may help with what I'm trying to achieve.

[Reid Barton]

The true is because -98 > -99.

[Tomas Skrivan]

Ahh yes the assert checks only post condition not the precondition. Maybe the preconditions can be checked in the function body and panic if they are not satisfied. I don't see a way to check preconditions with the assert function as it is right now.

[Raúl Raja Martínez]

Thanks, any idea on how I may encode the check for the pre condition? I tried but not sure how to pull the lambda out of the argument x to evaluate it.

def increment (x : TypeWithAssert Int (fun x : Int => x > 0)) : TypeWithAssert Int (fun y : Int => y > x) :=
    if x.P x then x + 1 else panic "x is not > 0"
    x + 1

invalid field 'P', the environment does not contain 'TypeWithAssert.P'
  x
has type
  TypeWithAssert Int fun x => x > 0

[Reid Barton]

I think you would just want if assert x then ...

[Tomas Skrivan]

and remove the last x+1

[Raúl Raja Martínez]

Thanks! I got it to work with all your recommendations!. Now I'm going to see if I can build something that given the increment function inspects it runs the pre and post conditions and can work with other functions accumulating the failures it finds. Do I need a Monad for this kind of sequential expression and error accumulation or can I do it with some meta programming? Thanks!

[Tomas Skrivan]

Using panic creates an error you can't really recover from.

You can use error monad and throw exceptions instead of panic. Then you can recover from errors more gracefully.

I think the approach depends a lot on what are you trying to achieve.

[Arthur Paulino]

I agree with Tomas. More info about your ultimate goal would be helpful. When I saw your first post, I thought that you wanted to kind of reimplement Lean 4 with some specific DSL. But if that's not the journey you're signing up for, then using Lean's OOTB syntax as Tomas did with subtypes is a way out. If you design your API with required proofs as inputs as well as proofs in the output of your functions, then there's no need for assert, since you can trust your implementations by design (as long as Lean's kernel accepts it and your file compiles)

[Raúl Raja Martínez]

@Arthur Paulino here is my goal.
I have code in kotlin, java and scala with refinement annotations with Pre and Post conditions such as:

@Pre("n > 0")
@Post("result > n")
fun increment(n: Int): Int = n + 1

fun foo() {
  increment(-1) // compile time error in foreign lang with proper message
}

I plan on transpiling kotlin and other langs to a lean encoding that supports pre, post conditions.
I'm starting with writing examples of this programs in Lean4 and trying to extract for the example above a structure like with info such as:

{
    lineInfo : String, // where the unsafe call happens
    pre : List Bool // true or false for failed pre conditions for n args
    post : Bool // result of post condition on the result
    termAnalyzed: ident // terms being subject of the call in this case `foo` calls `increment`
}

Don't care about types mentioned there, they are just examples.

Another example is detect unsafe calls such as:

val x = emptyList().get(2)

e: Example.kt: (1, 18): pre-condition `index within bounds` is not satisfied in `get(2)`
  -> unsatisfiable constraint: `((2 >= 0) && (2 < emptyList<Int>().size))`
  -> `2` bound to param `index` in `kotlin.collections.List.get`
  -> main function body

We are already doings this with SMT in arrow-analysis but I would like to bring this to more languages and use a Lean backend to evaluate the predicates.

I'm also evaluating F* for this same purpose but the smt2 queries F* generates can not really be reasoned about and the error messages do not show properly where it is failing. also my impression so far is that lean is much faster.

[Mario Carneiro]

Note that lean is not a replacement for an SMT solver. Lean isn't a "backend", it is a frontend and makes you ~manually prove all assertions

[Mario Carneiro]

so while you can probably translate the statements of these functions including the pre/post conditions, you can't translate the proofs because there are no proofs to be had unless the SMT solver is proof producing (and approximately 0% of SMT solvers are proof producing)

[Wojciech Nawrocki]

approximately 0% of SMT solvers are proof producing

Perhaps you can argue about whether these outputs are really "proofs" (maybe they are not sound or not possible to check or ..) but the major systems Z3 and CVC can both output proofs

[Mario Carneiro]

yes, they are "proof" producing

[Mario Carneiro]

I don't believe any checker exists for them though so I don't count them as proofs (I don't think it's really possible to develop a proof format without a checker keeping you honest)

[Andrés Goens]

Mario Carneiro said:

I don't believe any checker exists for them though so I don't count them as proofs (I don't think it's really possible to develop a proof format without a checker keeping you honest)

SMTCoq does work as a checker for CVC (and others, but not Z3)

[Tomaz Gomes]

Mario Carneiro said:

I don't believe any checker exists for them though so I don't count them as proofs (I don't think it's really possible to develop a proof format without a checker keeping you honest)

For the Alethe (https://verit.loria.fr/documentation/alethe-spec.pdf) proof format, we have the Carcara (https://github.com/ufmg-smite/carcara) checker

[Mac Malone]

@Tomaz Gomes Are there other proof checkers for Alethe? That is, is it possible to cross-verify a proof in Alethe to ensure that there are also not soundness problems in the checker itself?

[Tomaz Gomes]

It is possible to reconstruct Alethe proofs in Coq (using SMTCoq) and in Isabelle (using Sledgehammer)