First proof fails

Stream: Veil

[Mark R. Tuttle]

I'm new to Veil, but can anyone tell me why the following fails to prove?

import Veil

veil module Test

individual x: Nat
#gen_state

after_init  {
  x := 1;
}

action incr = {
  x := x + 1;
}

invariant x >= 1
#check_invariants

end Test

[Ilya Sergey]

Two issues:

• = in the incr action
• missing pragma #gen_spec after all invariants are defined

Corrected file:

import Veil

veil module Test

individual x: Nat

#gen_state

after_init  {
  x := 1;
}

action incr {
  x := x + 1;
}

invariant x >= 1

#gen_spec

#check_invariants

end Test

[Mark R. Tuttle]

Thanks, the missing #gen_spec was the issue. The action syntax seems to require the = with both

#git = "https://github.com/verse-lab/veil.git"
git = "https://github.com/verse-lab/veil/tree/veil-2.0-preview"

[George Pîrlea]

The action syntax seems to require the = with both

@Mark R. Tuttle I suspect you're still using Veil 1.0. To use Veil 2.0, you should have the following in lakefile.toml:

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

Note the use of rev, rather than giving the path to the branch in the git field.

Then run lake update veil.

I've added a version of the usage example for veil-2.0-preview at https://github.com/verse-lab/veil-usage-example/tree/veil-2.0-preview

= in the incr action

To clarify: Veil 1.0's syntax mirrored Ivy (i.e. action foo = {}), but we're moving to action foo { } syntax in Veil 2.0 (without =).

[Mark R. Tuttle]

Thanks. And which version of lean should I be using? The lake update veil updated the toolchain to 27.0.

[George Pîrlea]

v4.27.0 is the correct version, yes.