Brittle invariance checking in the initial state

Stream: Veil

[Mark R. Tuttle]

I'm struggling to prove that invariants are true in the initial state.

The attached file Basic.lean my current best minimization of the problem. All six invariants fail to prove in the initial state. In the initial state, p2c_tail=0 and c2p_tail=0, so the conjuncts N < p2c_tail and N < c2p_tail in the antecedents should be false, so the implications should be true.

• If I delete the unused type value, they prove.
• If I delete the last of the six invariants, they prove.
• If I add the invariant p2c_tail = 0, they prove.

Any advice?

My lakefile.toml includes

[[require]]
name = "veil"
git = "https://github.com/verse-lab/veil.git"
rev = "veil-2.0-preview"

My lean-toolchain is

leanprover/lean4:v4.27.0

PS: When I insert to prove iteratively and delete the sorrys, they all prove immediately, but I can't see yet how to use those successful proofs with #check_invariants.

[George Pîrlea]

@Mark R. Tuttle This is unfortunately a bug, and it appears to be a bug in one of our dependencies, lean-smt.

Behind the scenes, when Veil solves a goal, it uses one of two tactics (that we defined), veil_solve_wp (for the kind of goals you get when you Cmd + Click) or veil_solve_tr (Cmd + Shift + Click).

You can use set_option veil.desugarTactic true to see what those 'mean', in terms of lower- level tactics. It looks like this:

set_option veil.desugarTactic true

theorem initializer_inv_0 /- parameters elided -/ :
    Veil.VeilM.meetsSpecificationIfSuccessfulAssuming
      (@initializer.ext ρ σ value value_dec_eq value_inhabited χ χ_rep χ_rep_lawful σ_sub ρ_sub)
      (@Assumptions ρ value value_dec_eq value_inhabited ρ_sub)
      (@Invariants ρ σ value value_dec_eq value_inhabited χ χ_rep χ_rep_lawful σ_sub ρ_sub)
      (@inv_0 ρ σ value value_dec_eq value_inhabited χ χ_rep χ_rep_lawful σ_sub ρ_sub) :=
  by
  veil_intros
  veil_wp
  veil_concretize_wp
  veil_fol
  veil_smt -- `simp` failed: maximum number of steps exceeded

This is the error message displayed in the InfoView: image.png

The problem is in the smt's tactic embedding step (which performs simplifications to rewrite Bool into Prop and Nat into Int, such that proofs returned by cvc5 can be reconstructed). In this case, these simplifications go into a loop.

All these goals are true and can be solved by grind.

PS: When I insert to prove iteratively and delete the sorrys, they all prove immediately, but I can't see yet how to use those successful proofs with #check_invariants.

We haven't yet implemented a way to hook back theorems proven interactively into the InfoView UI. The plan is you'll tag the relevant theorems with the @[veil] tag and the results will automatically update in the InfoView.

Let me take a deeper look later today (Singapore time) and see if I can push a quick fix for this.

[George Pîrlea]

@Mark R. Tuttle I've pushed a workaround (commit 06552a5) for now, that does more simplification on our side before we send the goals to Lean SMT.

If you're running in a repository based on the veil-usage-example template, run lake update && lake build. If you're operating in a clone of the Veil repo on the veil-2.0-preview branch, run git pull first.

Please let me know if this doesn't work for you or if you run into another issues!

We'll be working with the upstream maintainers of Lean SMT to get this properly fixed before the Veil 2.0 release. (There are also big performance issues with the embedding step which we hope to ameliorate.)

[Mark R. Tuttle]

@George Pîrlea Thanks. I learned a lot from your answer. The bug fix does work on the minimized example I sent you, but still fails in the same way on the full model. I'll go ahead and append the full model. Basic.lean

This version has most actions commented out. If you uncomment them you can see I"m not done. I'm going to ignore the initial state proofs and continue work on the other actions.

[George Pîrlea]

@Mark R. Tuttle I've reported the issue upstream: https://github.com/ufmg-smite/lean-smt/issues/215

I'm writing my dissertation now, so unfortunately I don't have much time to go debugging. Sorry for the trouble!

[George Pîrlea]

I suspect the issue is particularly with the Lean SMT's embedding of Nat.

[George Pîrlea]

@Mark R. Tuttle Please try lake update && lake build again.

It seems there's no actual loop in the simp rules for Lean SMT's embedding — it just has to do more rewrites than simp allows by default. I've pushed a fix on our fork of lean-smt.

This makes the proofs go through for me on your full model.

[Mark R. Tuttle]

@George Pîrlea Thanks. The invariants do pass with that fix. In the mean time, I had rewritten the model to be relational as we discussed in a different thread and I'm getting simp errors on that model, but I may have done something stupid.

[George Pîrlea]

@Mark R. Tuttle I would have to see the model to figure out exactly what's going on, but it's probably another bug.