Easy program verification advice

Stream: new members

[V S]

Hello! I hope this is the right channel for the question (a little bit intimidated to post in Program Verification since all the questions there seem very advanced and out of reach for me now).
So, I've been given a task by one of my professors - to verify an easy sorting algorithm on paper (which I have no problem with) and using a prover (which is where I need advice, since I've never done program verification and only now started slowly learning how to do it). I know the basic things in Lean and enjoy working with it and briefly remember Rocq. From what I've seen on Zulip, Lean is not as used in program verification since there are many Rocq extensions for that purpose and not all necessary packages are in Lean (is this is not true, please correct me, I'm extremely new to this), and I've also seen something that looks like a rocq verified file with the proof(?), although I couldn't really understand what was going on due to my lack of knowledge in the subject.
Now to my questions - 1) would you say that most (or at least easy) program verification is better done in Rocq and I should try and do the task only in rocq or is Lean also a very good option?
2) How hard would it be to take an algorithm (in whatever form is better suited for the verification), rewrite it in Lean and provide the proper verification?
3) Are there any helpful resources for this in Lean? I briefly remember seeing something like a manual here, but couldn't find it (or anything in google) now or in the other Lean manuals. Maybe a template or anything, really, since I have no clue on what to do or what examples to look for and recent enough post on Program verification mostly mention something scary-sounding and probably harder than what I'm going for

[Anthony Wang]

If you're verifying functional programs, Lean will probably work fine. But for imperative programs, you'll probably have a much easier time using a different proof assistant, such as Dafny which is specifically designed for that use case. It is also possible to verify imperative programs using Lean (see https://markushimmel.de/blog/my-first-verified-imperative-program/) but more complicated than doing it in Dafny.

[(deleted)]

Dafny is very bad

[(deleted)]

It relies on an SMT solver, and you need a lot of tinkering for assertions to go through

[(deleted)]

Lean is perfectly fine for program verification

[(deleted)]

Even for imperative programs

[(deleted)]

Just learn how to write programs in Lean. You'll do just fine.

[(deleted)]

If you get stuck, you can always post another question here. Good luck!

[(deleted)]

Yeah the link posted above is a very good starting point.

[V S]

Thank you both for the advice, will try and understand the blog post and write here if there are any more questions (or close once I get it completely :))

[Anthony Wang]

Huỳnh Trần Khanh said:

Dafny is very bad

I'm well aware of Dafny's flaws (I even discovered a major soundness bug in Dafny a few months ago that still hasn't been fixed yet), but it's still a very useful tool for program verification and much easier to learn and use than Lean.

[Anthony Wang]

Huỳnh Trần Khanh said:

It relies on an SMT solver, and you need a lot of tinkering for assertions to go through

I'd argue that Lean needs a lot of tinkering for tactic-based proofs to go through :upside_down:

[Anthony Wang]

But I guess this Dafny debate is getting a bit off-topic since this is the Lean Zulip after all.

[Shreyas Srinivas]

I can’t say much now, but in a few weeks or months there will be a few different ways to verify imperative programs in lean . That being said, the monadic verification framework might be worth a try right now

[Shreyas Srinivas]

I would argue that verifying a functional programming spec of this sorting procedure is bound to be valuable regardless of the developments on the imperative side

[V S]

So, yeah, I feel like I need to learn about the basics of monads to even write what program I want to verify :melting_face:
I've tried to formalize an easy bubble sort, but the function must return not Int or Bool, but List, and a quick search did nothing.
So I try to write

import Mathlib
def BubbleSort (l : List Real) : Id List Real := do

and get

Application type mismatch: In the application
  Id List
the argument
  List
has type
  Type ?u.6 → Type ?u.6 : Type (?u.6 + 1)
but is expected to have type
  Type ?u.5 : Type (?u.5 + 1)

Can you please recommend something to learn the basics for this? I've checked some books about Lean and none had a proper theory about monads (although mentioned them)

[Kenny Lau]

@V S Id (List Real)

[V S]

And when I tried to copy the program from the link above

import Mathlib

def pairsSumToZero (l : List Int) : Id Bool := do

  let mut seen : HashSet Int := ∅

  for x in l do

    if -x ∈ seen then

      return true

    seen := seen.insert x

  return false

I get

unknown identifier 'HashSet'

.

[Kenny Lau]

put open Std on a newline in Line 2

[V S]

@Kenny Lau Thank you so much!

[V S]

For my next attempt, I have

import Mathlib
open Std

def BubbleSort (l : List Real) : Id (List Real) := do
  let n := l.length()
  let a : Real := 0
  for i in List.range (n - 1) do
    for j in List.range (n - i - 1) do
      if l[j]! > l[j + 1]! then
        a := l[j]!
        l[j]! := l[j + 1]!
        l[j + 1]! := l[j]!
  return l

Which provides me with

type mismatch
  a = l[j]!
has type
  Prop : Type
but is expected to have type
  Id PUnit.{1} : Type

Which seems weird. Also, when trying to understand how to access the i-th element, I've seen a topic about proving that it's valid, but was also unable to understand how to prove that it's valid exactly.
I hope I'm not bombarding the topic with stupid questions :melting_face:

[Kenny Lau]

@V S your code does not result in your posted error

[Kenny Lau]

also you don't net () for length, this isn't java, everything is a function here

[V S]

Kenny Lau said:

V S your code does not result in your posted error

Unfortunately, I can't use the live.lean-lang.org playground and lean.math.hhu.de returns an abysmal error for import Mathlib, so I'm using the version on my pc which does give this error. I have the last lean Vscode extension, do I need to do the usual lake ... stuff to try and get rid of it?

[Kenny Lau]

V S said:

I can't use the live.lean-lang.org playground

why?

[V S]

Kenny Lau said:

V S said:

I can't use the live.lean-lang.org playground

why?

It won't load on any of my devices (with or without proxy) so I've kinda given up on it and usually have no trouble with using either lean.math.hhu.de or a local version on pc, this is the first time something like this happened

[Julia Scheaffer]

Is lean on your PC out of date?

[V S]

I think the .de Duper mode works? and it gives me the unsupported pattern in syntax match l[j]! error after I changed let mut a : Real := 0, is it the same as what the .org playground says? (I also tried to use let mut r := l and do everything for r, but it didn't help)

[Julia Scheaffer]

It is, yes

[V S]

Julia Scheaffer said:

It is, yes

Ok, thank you! Will use it then until the Lean on my pc updates

[Kenny Lau]

@V S the function to change one element of a list is List.set

[V S]

Kenny Lau said:

V S the function to change one element of a list is List.set

This gives

type mismatch
  l.set j l[j + 1]!
has type
  List ℝ : Type
but is expected to have type
  Id PUnit.{1} : Type

. Is it a valid error or do I have to find an alternative to Duper too?

MWE (the latest version so that the code is available):

import Mathlib
open Std

def BubbleSort (l : List Real) : Id (List Real) := do
  let mut r := l
  let n := l.length()
  let mut a : Real := 0
  for i in List.range (n - 1) do
    for j in List.range (n - i - 1) do
      if r[j]! > r[j + 1]! then
        a := r[j]!
        r := r.set j r[j+1]!
        r := r.set (j + 1) a
  return r

[Kenny Lau]

can you post full code?

[Kenny Lau]

List.set returns a list, not unit

[Kenny Lau]

(return unit is the equivalent of java's "void method")

[Julia Scheaffer]

You would need to use l := l.set ... right?

[V S]

IT WORKED!!!

[V S]

Thank you everyone so much! Off I go to work with Hoare triples

[Anthony Wang]

To swap two elements, you can also use l := l.swap j (j + 1) instead of manually swapping with a temporary variable.

[V S]

Anthony Wang said:

To swap two elements, you can also use l := l.swap j (j + 1) instead of manually swapping with a temporary variable.

It gives

invalid field 'swap', the environment does not contain 'List.swap'
  r
has type
  List ℝ

and I can't find it in Mathlib

[Anthony Wang]

Oh my bad, swap only works on arrays, not lists.

[Robin Arnez]

You're probably better off using Arrays still because on List indexing is O(n)

[V S]

Robin Arnez said:

You're probably better off using Arrays still because on List indexing is O(n)

Rewriting with arrays now! By the way, how do you properly prove that the indices are correct to use? r[j] ⟨by decide⟩ or something like that does not work

[Aaron Liu]

V S said:

Robin Arnez said:

You're probably better off using Arrays still because on List indexing is O(n)

Rewriting with arrays now! By the way, how do you properly prove that the indices are correct to use? r[j] ⟨by decide⟩ or something like that does not work

You need to pull the proofs into the loop with for hi : i in ...

[Aaron Liu]

You also need to encode the length of the arrays into their type with docs#Vector or similar so they can't change length on you

[Aaron Liu]

Then you can probably use r[i]'(by grind)

[Julia Scheaffer]

I am learning so much in this thread :smile:

[V S]

Aaron Liu said:

You also need to encode the length of the arrays into their type with docs#Vector or similar so they can't change length on you

I unfortunately don't really get how to encode the length :( The last MWE is:

import Mathlib
open Std Real List

def BubbleSort (l : Array Real) : Id (Array Real) := do
  let mut a : Real := 0
  let mut r := l
  let n := l.size
  for hi: i in List.range (n - 1) do
    for hj: j in List.range (n - i - 1) do
      if r[j]'(by grind) > r[j + 1]'(by grind) then
        r := r.swap j (j+1)
  return r

and it returns errors even with hi

[V S]

There is Array.toVector, but I don't really get how it makes the length constant

[Anthony Wang]

You need to use Vector Real n instead of Array Real.

[Anthony Wang]

(deleted)

[Julia Scheaffer]

Here's a version I got working based on @V S 's

import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      if a[j]'(by grind) > a[j + 1]'(by grind) then
        a := a.swap j (j+1) (by grind) (by grind)
  return a.toArray

#eval BubbleSort #[3, 8, 5]

[Julia Scheaffer]

lots of grinding, but that can be optimized

[Julia Scheaffer]

Now just to try and prove that it produces sorted arrays :sweat_smile:

[V S]

Julia Scheaffer said:

Here's a version I got working based on V S 's

import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      if a[j]'(by grind) > a[j + 1]'(by grind) then
        a := a.swap j (j+1) (by grind) (by grind)
  return a.toArray

#eval BubbleSort #[3, 8, 5]

That's great! Unfortunately, Duper does not like this grinding, but I trust that it's correct (guess I will try and hope that it works at least somewhere on my devices :smiling_face_with_tear: )

[Julia Scheaffer]

I am trying to make a version that doesn't use grind now

[Julia Scheaffer]

Got it working without grinding

import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hi
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

#eval BubbleSort #[3, 8, 5]

[Julia Scheaffer]

Just needed to enter some facts about i and j into the context

[Julia Scheaffer]

Does that version run on your machine @V S ?

[V S]

Julia Scheaffer said:

Does that version run on your machine V S ?

It absolutely does!

[Julia Scheaffer]

I was looking at the docs on List.Vector and many of the definitions seems to have links to Vector instead of List.Vector (example: List.Vector.«term_::ᵥ_» ) is this a bug in the docs?

[Kenny Lau]

yes

[Julia Scheaffer]

It it a known bug or is there somewhere i should report it?

[Kenny Lau]

you could probably discuss this in #general

[Julia Scheaffer]

Should I just move my message to a new thread in #general then?

[Julia Scheaffer]

Sorry, i am sort of new to Zulip

[Kenny Lau]

Just copy the message manually.

[Ruben Van de Velde]

You can create a PR directly

[V S]

Ok, I am back with questions. I started to follow the link again. My latest attempt (formulation of the theorem) is:

import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hi
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

theorem BubbleSort_corr {α} [LT α] [DecidableLT α] (a: Array α) : ⦃a.size >= 0⦄ BubbleSort a ⦃∀ i j : ℕ, i <= a.size - 1 ∧ j <= i -> a[j] <= a[i]⦄ := by
  mvcgen [BubbleSort]

since the ⦃Precondition⦄ is that the size of the array is >= 0 and the ⦃Postcondition⦄ has 2 conditions:

1. The result is a permutation of the original array which I have no idea how to formalize since we have the .toVector (edit: I missed that we have the .toArray at the end so something like 'for each element of a, there is an unique element of the result such that they are equivalent')
2. The result is ordered which I wrote as above

I get unexpected token '>='; expected ':' (and if I copy ⦃⌜True⌝⦄ like from the link, it also gives an error of a missing token, which is confusing). So I am once again asking for help with the first of conditions (it seems obvious but I feel like it would be cheating just to omit it) and with the syntax error

[Kenny Lau]

@V S if you look at the link in your link that says "Click here to open the online Lean playground pre-filled with the proof", you will see open Std Do on Line 4, which you also need to do to enable that notation.

[Anthony Wang]

This fixes some of your problems (although Lean is still complaining about the array indices):

import Std.Tactic.Do
import Mathlib

open Std.Do

def BubbleSort' {α} [LT α] [DecidableLT α] (a: Array α) : Id (Array α) := do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hi
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

theorem BubbleSort_corr {α} [LT α] [DecidableLT α] (a: Array α) : ⦃⌜True⌝⦄ BubbleSort' a ⦃⇓ r => ⌜∀ i j : ℕ, i < r.size ∧ j <= i -> ¬(r[j] > r[i])⌝⦄ := by
  mvcgen

However I suspect even if you prove the array indices are in bounds, you'll run into the problem #new members > mvcgen doesn't produce any invariant goals.

[V S]

Kenny Lau said:

V S if you look at the link in your link that says "Click here to open the online Lean playground pre-filled with the proof", you will see open Std Do on Line 4, which you also need to do to enable that notation.

Thank you! I completely missed the 'link in the link'

[V S]

Anthony Wang said:

This fixes some of your problems (although Lean is still complaining about the array indices):

import Std.Tactic.Do
import Mathlib

open Std.Do

def BubbleSort' {α} [LT α] [DecidableLT α] (a: Array α) : Id (Array α) := do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for hi : i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hi
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

theorem BubbleSort_corr {α} [LT α] [DecidableLT α] (a: Array α) : ⦃⌜True⌝⦄ BubbleSort' a ⦃⇓ r => ⌜∀ i j : ℕ, i < r.size ∧ j <= i -> ¬(r[j] > r[i])⌝⦄ := by
  mvcgen

However I suspect even if you prove the array indices are in bounds, you'll run into the problem #new members > mvcgen doesn't produce any invariant goals.

That's a little bit disheartening, I'll follow your discussion and hope that we will get our answers or hints soon...

[Anthony Wang]

My recommendation would be to use Dafny instead of Lean since in your original post since you mentioned you didn't need to specifically use Lean for your task. It seems like Lean's mvcgen still has some limitations and definitely isn't as user-friendy as Dafny.

[V S]

Anthony Wang said:

My recommendation would be to use Dafny instead of Lean since in your original post since you mentioned you didn't need to specifically use Lean for your task. It seems like Lean's mvcgen still has some limitations and definitely isn't as user-friendy as Dafny.

I'll definitely check it out! Do you know whether it's explicitly stated or discussed on what level Dafny is 'trustable', similar to https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html?

[Ruben Van de Velde]

That seems like an odd comment to make when people ask for help on the lean zulip, but okay

[Anthony Wang]

V S said:

I'll definitely check it out! Do you know whether it's explicitly stated or discussed on what level Dafny is 'trustable', similar to https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html?

You should probably ask this on the Dafny Zulip to get a better answer, but the short answer is that Dafny is not very trustworthy since it doesn't satisfy the de Bruijn criterion and Dafny has had many soundness bugs which often take a while to get fixed.