Proof incrementality

[volodeyka]

Right now, each time we change something in the program, Velvet has to reprove all the goals from scratch. It would be nice to add some simple goal caching to avoid that and make Velvet proofs more incremental. Maybe find something like that on Lean Zulip?

[MantasBaksys]

Here's an example for where proof caching would be very useful. loom_solve here takes >5s each time and each incremental tactic on the 4 goals left after seems to re-run loom_solve

import Auto
import Lean
import Mathlib


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


import CaseStudies.Velvet.Std
import CaseStudies.TestingUtil


open TotalCorrectness DemonicChoice

set_option auto.smt.trust true
set_option auto.smt true
set_option auto.smt.timeout 1
set_option auto.smt.solver.name "cvc5"
set_option maxHeartbeats 1000000

attribute [solverHint] Array.multiset_swap
attribute [solverHint] Array.get_set_c

method BubbleSort (mut a : Array Int) return (unit: PUnit)
  require 1 ≤ a.size
  ensures forall k l, 0 ≤ k ∧ k < l ∧ l <= a.size - 1 → a[k]! ≤ a[l]!
  do
    let a₀ := a
    let n := a.size
    let mut i := n - 1
    while i > 0
    invariant i < n
    invariant i >= 0
    invariant forall k l, i < k ∧ k < l ∧ l < n → a[k]! ≤ a[l]!
    invariant forall k l, 0 ≤ k ∧ k ≤ i ∧ i < l ∧ l < n → a[k]! ≤ a[l]!
    decreasing i
    do
      let mut j := 0
      while j < i
      invariant j ≤ i
      invariant i < n
      invariant j >= 0
      invariant forall k l, i < k ∧ k < l ∧ l < n → a[k]! ≤ a[l]!
      invariant forall k l, 0 ≤ k ∧ k ≤ i ∧ i < l ∧ l < n → a[k]! ≤ a[l]!
      invariant forall k, 0 ≤ k ∧ k ≤ j → a[k]! ≤ a[j]!
      decreasing i - j
      do
        if a[j]! > a[j+1]! then
          swap! a[j]! a[j+1]!
        j := j + 1
      i := i - 1
    return

macro_rules
  | `(tactic| loom_solver) =>
    `(tactic| loom_auto)

-- 4 goals left after `loom_solve` but too slow to interactively work on
prove_correct BubbleSort by
  loom_solve
  sorry

[volodeyka]

Hey Mantas! Your issue seems to be incrementality relates. It seems like it is broken again :(
Basically, you don't want Lean to re-run loom_solve every time you edit the proof
I hope we can fix it

[volodeyka]

@MantasBaksys
In general if you do

loom_solve
{
  <code here>
}

Then, if you edit code inside { }, Lean should not re-run loom_solve. And it does not do that for smaller examples...
Must be a bug in Lean. Let us try to minimize the example

[volodeyka]

As this an incrementality issue, I will change the title. @F47-503 agreed to look into it

[F47-503]

Although not directly related to the issue, please note that invariants about sizes for mutable Arrays are likely to be necessary for this program to verify, for example: invariant a.size = n @MantasBaksys

[volodeyka]

@MantasBaksys as a temporary solution, we are implementing a
prove_correct? <method_name> command. Basically, this command should generate you a method correctness theorem as a Lean theorem statement. Then you can prove it using the same tactics (i.e. loom_solve). As it is going to be a native Lean theorem syntax, so it would have incrementality working and Lean will not be re-evaluating loom_solve every time you edit the proof script.
We already have a PR for this feature, so it should land in a couple of days.
If it is critical for you right now, you can use
set_option trace.Loom true
This will print the theorem corresponding to prove_correct Then you can copy paste it into the file and continue with the proof.