Paper cuts

Stream: Loom

[Shreyas Srinivas]

I wrote the following #mwe which I think illustrates the kind of paper cuts I get stuck at for a while which I would think lean-auto could solve.

[Shreyas Srinivas]

import Auto

import Loom.MonadAlgebras.NonDetT.Extract
import Loom.MonadAlgebras.WP.Tactic
import Loom.MonadAlgebras.WP.DoNames'

import CaseStudies.Velvet.Std
import CaseStudies.TestingUtil

open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames

set_option auto.smt.trust true
set_option auto.smt true
set_option auto.smt.timeout 2
set_option auto.smt.solver.name "cvc5"

method swapIndex (mut a : Array Int) (i : ℕ) (j : ℕ)
  return (a_swapped : Array Int)
  require i < a.size
  require j < a.size
  ensures a_swapped.size = a.size
  ensures ∀ k : ℕ, k < a_swapped.size →  k ≠ i ∧ k ≠ j → a_swapped[k]! = a[k]!
  ensures a_swapped[i]! = a[j]!
  ensures a_swapped[j]! = a[i]!
  do
  let mut temp := a[i]!
  a[i] := a[j]!
  a[j] := temp
  return a

prove_correct swapIndex by
  loom_solve -- nothing done
  grind

[Shreyas Srinivas]

CC : @George Pîrlea

[Shreyas Srinivas]

why is loom_solve failing here?

[Shreyas Srinivas]

Further, there doesn't seem to be a way to name the requires so that I can use them for correct indexing (within the def)

[Shreyas Srinivas]

I did manage to solve this manually btw:

prove_correct swapIndex by
    loom_solve
    all_goals {
      simp [TArray.set, Array.setIfInBounds, require_1, require_2]
      try grind
    }

[Vladimir Gladstein]

@Shreyas Srinivas hey! Did you try running it with a new version of Loom? If not please run lake update. Now the default automation for Loom is grind.
Also, of you want to use SMT solver tactics , such as auto, please make sure that you have cvc5 installed on your PATH

[Shreyas Srinivas]

Hey I already have cvc5 on my path. I'll update now and try

[Shreyas Srinivas]

One thing I am missing is the ability to name and use the requires and ensures of a procedure call (inside another procedure). I understand that you are generating Anonymous names for these

[Shreyas Srinivas]

Example : if I call swapIndex from inside a (quicksort) partition function, I am not sure how I can get the postcondition for size out of the call

[Vladimir Gladstein]

Also it seems like you have a problem with your post-condition
when you write
ensures a_swapped[i]! = a[j]!
a_swapped refers to a modified array a. But in the same time, because you pass a as a mutable argument (mut a : Array Int), a in the post condition will be referring to a mutated version of a

[Shreyas Srinivas]

Initially I didn't have mut

[Vladimir Gladstein]

you can try the following spec

method swapIndex (mut a : Array Int) (i : ℕ) (j : ℕ)
  return (a_swapped : Array Int)
  require i < a.size
  require j < a.size
  ensures a_swapped.size = a.size
  ensures ∀ k : ℕ, k < a_swapped.size →  k ≠ i ∧ k ≠ j → a_swapped[k]! = a[k]!
  ensures a_swapped[i]! = aOld[j]!
  ensures a_swapped[j]! = aOld[i]!
  do
  let mut temp := a[i]!
  a[i] := a[j]!
  a[j] := temp
  return a

[Vladimir Gladstein]

Shreyas Srinivas said:

Initially I didn't have mut

If you don't have mut then you cannot modify a. So you either need to use mut and then refer to the old variable as aOld or remove mut and create a local mutable variable inside the method

[Vladimir Gladstein]

Shreyas Srinivas said:

One thing I am missing is the ability to name and use the requires and ensures of a procedure call (inside another procedure). I understand that you are generating Anonymous names for these

That's right, we indeed do not support this feature. If you could create a GitHub issue for it, we will add it in a course of the week.

[Shreyas Srinivas]

I noticed that TArray is gone with this update and we now just use normal Lean Arrays. This is a nice change

[Shreyas Srinivas]

Ah I didn't know one could access the old name as aOld. This helps

[Vladimir Gladstein]

Yes, I am planning to do a bunch of other cosmetics changes soon!

[Vladimir Gladstein]

Shreyas Srinivas said:

Ah I didn't know one could access the old name as aOld. This helps

You can refer to this documentation https://github.com/verse-lab/loom/blob/master/CaseStudies/Velvet/velvet_documentation.md