Add option to verify inductive invariants

[bugarela]

I'm exploring inductive invariants in Quint with Apalache, and it seems to be achieavable with some tweaks to the interface and mode verification for Init. See this example (from the Apalache manual):

/// A spec based on the y2k TLA+ specification from Igor Konnov [1]
///
/// [1]: https://github.com/informalsystems/apalache/blob/main/test/tla/y2k.tla
module y2k {
  const birth_year: int
  const license_age: int

  var year: int
  var has_license: bool

  val age = year - birth_year

  pure def increment_year(old_year: int): int = {
    (old_year + 1) % 100 // Only two digits were used to store the year!
  }

  action new_year = all {
    year' = increment_year(year),
    has_license' = has_license
  }

  action issue_license = all {
    age >= license_age,
    has_license' = true,
    year' = year,
  }

  action init = all {
    year' = birth_year,
    has_license' = false,
  }

  action step = any {
    new_year,
    issue_license,
  }

  val safety = has_license implies (age >= license_age)

  val inv = year.in(0.to(99)) and has_license.in(Bool)

  action inv_as_action = all {
    nondet y = 0.to(99).oneOf()
    year' = y,
    nondet b = Bool.oneOf()
    has_license' = b,
  }
}

module y2k_instance {
  import y2k(birth_year=80, license_age=18).*
}

IndInit:

$ quint verify --init=init --invariant=inv --max-steps=0 --main=y2k_instance inductive_invariant.qnt
[ok] No violation found (83ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.

IndNext:

$ quint verify --init=inv_as_action --invariant=inv --max-steps=1 --main=y2k_instance inductive_invariant.qnt
[ok] No violation found (121ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.

IndProp:

$ quint verify --init=inv_as_action --invariant=safety --max-steps=0 --main=y2k_instance inductive_invariant.qnt
An example execution:

[State 0] { y2k_instance::y2k::has_license: true, y2k_instance::y2k::year: 0 }

[violation] Found an issue (145ms).
error: found a counterexample

The worst part of it is that we need to write an action version of inv to be used as init in IndNext and IndProp, which might not be trivial. The thing is, we can simply remove some restrictions from Quint, and use the predicate directly, since apalache does accept that.

So my idea is:

• Create a command that verifies inductive invariants
  • take init, inv and prop (optional) as arguments.
  • call Apalache 2-3 times verifying each part
  • if there is an error, properly report it with information about at which stage the error occurred.

[josef-widder]

The thing is, we can simply remove some restrictions from Quint, and use the predicate directly, since apalache does accept that

I am not sure I understand this completely. By "restrictions" do you mean that init must be a step in Quint? Or is there something else

[bugarela]

I mean that, in this new command, quint shouldn't complain if your init is actually a predicate. Currently, Quint expects init to be an action and will complain if you give an invariant as init. We can remove this check from quint, and apalache should accept it normally. Makes sense?

[josef-widder]

Makes sense. Thanks! This is what I thought I understood, but I wasn't sure. I just wanted to be sure ;-)