Invariants from other isolates are only assumed before actions, not after

[jtassarotti]

The invariant in isolate safety2 in the following example fails:

#lang ivy1.7

relation p
relation r

object actions = {
  after init {
    p := false;
  }

  action toggle1 = {
    p := true;
  }

  export toggle1
}

isolate myaxiom = {
  axiom r
}

isolate safety1 = {
  invariant p -> r
} with actions, myaxiom

isolate safety2 = {
  invariant p -> r
} with actions, safety1

More generally, I expected if isolate A has invariant Q and isolate B has invariant T, then when we use with A on B, the check for B would try to prove that for each action from state s to s', Q(s) /\ T(s) /\ Q(s') -> T(s'), but instead it seems to check Q(s) /\ T(s) -> T(s'). (#19 seemed related but was about initialization.)

If I understand correctly, the way the invariants from A are incorporated is by essentially adding them as assume statements at the beginning of each action -- perhaps they could also soundly be added as assume statements at the end?

[kenmcmil]

Well, Ivy doesn't do that because you could make a circular argument to prove false like this:

isolate safety1 = { invariant false } with actions, safety2

isolate safety2 = { invariant false } with actions, safety1

Notice here that each isolate uses the invariant of the other. To avoid such circularities, Ivy uses an approach called "circular assume/guarantee". This means that the proof of assertion A at time t can assume assertion B at all times less than t, but not at t, which would allow us to use A to prove B and B to prove A. Put another way, all of the assertions are proved by mutual induction over time.

You might say "why not disallow the above case?". In a concurrent system, you may have modules that interact over time, such that each has to assume the specification of the other. Think of a landlord and a tenant: the tenant promises to pay the rent as long as the landlord keeps the heat on, and the landlord promises to keep the heat on as long as the tenant pays the rent. This contract isn't circular because each party gets to assume the other upholds its guarantee in the strict past. Thus, neither can be the first to violate the contract.

The normal use case of one isolate exporting an invariant to another is when isolate A calls isolate B. In this case A gets to assume the invariant of B on return from B (but not on return from A!).

[jtassarotti]

Thanks, that makes sense. I saw the example about circular assume/guarantee in the docs but didn't connect the dots.

I wonder if there's an alternate way to accomplish what I was trying to do. I have identified some invariant P, which is inductive, but doesn't yet imply the safety property I care about. But as I added more clauses to the invariant, checking slowed down. So my hope was to first isolate P, check it independently, then export it to another isolate where I add in yet more. With the option of temporarily turning on "trusted" to avoid re-checking the first isolate as I was developing. (But perhaps the slow down is a signal that I need to go back to the drawing board on the structure of my proof.)

[kenmcmil]

Makes sense. In other words, you want to do an incremental inductive proof. There is a not-so-pretty way to do it. You can wrap isolate A inside isolate B and just have each action of A call the corresponding action of B. The invariant of B can then be used by A in the way that you want. Soon, I hope, there will be a better way to do this using isolate-level tactics.

[odedp]

I've also experienced such slow downs, and I think it would be good to have support for more fine-grained control over which invariants go into the verification conditions. Even if the proof is not incremental (i.e., there is a circular dependence between many invariants), it may still be useful to allow the user to select which invariants to assume in the prestate when proving a given invariant (with the default being to assume all invariants). Such control can also be useful to eliminate some quantifier alternation cycles.

[kenmcmil]

Have a look at the branch isolate_proof. There are some examples of isolate-level tactics there. It would be pretty straightforward to add tactics to break out subsets of the isolate invariants for proof, select subsets to use in the pre-state and also do incremental proofs.

[nano-o]

It would be very useful to have such tactics in my opinion!

[jtassarotti]

Makes sense. In other words, you want to do an incremental inductive proof. There is a not-so-pretty way to do it. You can wrap isolate A inside isolate B and just have each action of A call the corresponding action of B. The invariant of B can then be used by A in the way that you want. Soon, I hope, there will be a better way to do this using isolate-level tactics.

Thanks for the suggestion. I tried that but then I get an error about the external call having a visible effect on p. In particular, with:

#lang ivy1.7

relation p
relation r

isolate a = {
  object actions1 = {
    after init {
      p := false;
    }

    action toggle = {
      p := true;
    }

    export toggle
  }

  isolate myaxiom = {
    axiom r
  }

  isolate safety1 = {
    invariant p -> r
  } with actions1, myaxiom

  isolate b = {
    object actions2 = {
      action wrapped_toggle = {
        call a.actions1.toggle();
      }

      export wrapped_toggle
    }

    isolate safety2 = {
      invariant p -> r
    } with b.actions2, a.safety1
  }

}

then ivy_check gives the error

Isolate a.b.safety2:
ivy_inv_bug_solution.ivy: line 29: error: Call out to a.actions1.toggle may have visible effect on p
ivy_inv_bug_solution.ivy: line 37: referenced here

[kenmcmil]

Maybe I misunderstood what you were trying to do before. I thought you were trying to do incremental induction. Here's a version that does that:

#lang ivy1.7

relation p
relation r

isolate main = {
    after init {
        p := false
    }

    action a = {
        p := true;
    }

    specification {
        invariant p -> r
    }

    private {
        axiom r
    }
}

isolate wrapper = {
    export action a = {
        call main.a
    }

    specification {
        invariant p -> r
    }
} with main

Notice how action wrapper.a wraps action main.a. It can use the invariant of main to prove its own invariant without knowing the axiom r, because it knows p->r on return from main.a.

However, in this proof, the code of main.a is not erased. It seems like what you are trying to do is abstract away the code of toggle when proving safety2. In other words, you want to do a Hoare-style proof. This is not actually possible in Ivy. By design, an isolate in Ivy completely hides its implementation state. On the other hand, both the specification code and state are always visible.

It would be possible to add support for Hoare-style (i.e., procedure-modular) specifications in Ivy (for example, as implemented in Dafny). If you have a good use case for this I would consider it.

[jtassarotti]

Ah, what you did is exactly what I wanted, I just did not understand correctly how to do the wrapping that you had proposed. Thank you for writing out the example in detail, it was very helpful.