state machine refinement structure

[tjhance]

Currently our refinement structure looks like: we have a bunch of state machines, A, B, C, ... etc. with refinement theorems of the form A_Refines_B.i.dfy. These are all named pretty consistently (although something much less consistent is the state machine invariants; sometimes the invariants for A are in the A file itself, and sometimes they are in separate files).

Sometimes, the A_Refines_B.i.dfy files are interesting, and sometimes they are not. There are a lot of files A_Refines_C which simply compose two existing refinements, A_Refines_B and B_Refines_C. All these 'composition' refinements have nearly the exact same boiler plate. With a "module system" on the horizon, we can start to think about writing a generic refinement composition proof. See this proof-of-concept.

However, there's another issue that needs to be taken care of first, which has to do with the way the refinement theorems are stated.

Here's a typical refinement theorem statement (Betree_Refines_Map.i.dfy):

  lemma RefinesNext(s: Betree.Variables, s':Betree.Variables, uiop: UI.Op)
    requires Inv(s)
    requires Betree.Next(s, s', uiop)
    ensures Inv(s')
    ensures MS.Next(I(s), I(s'), uiop)
  {
    // ...
  }

Note that this has Inv(s) as a pre-condition. Often, the interpretation function in these refinements has Inv as a precondition as well. The consequence of this is that A_Refines_B only composes with B_Refines_C if A.Inv implies B.Inv. This is problematic for a bunch of reasons, including:

• It makes it impossible to write a generic composition proof within the module system (no such proof would be allowed to rely on an SMT condition like A.Inv ==> B.Inv)
• Creates long dependency chains where invariants include other invariants that they don't really need.(*) This is bad for proof isolation.

(*) One (the only?) exception is ByteBlockCacheSystem, which includes the invariants of BlockCacheSystem for nontrivial reasons.

The solution to this is to define our generic refinement theorem without reference to 'Inv'. For example, we could use 'Reachable' instead (i.e., Reachable(s) := exists s0...sn . Init(s) && (forall i . Next(s_i, s_(i+1))) && sn == s). Reachable is the universal invariant which implies Inv for any predicate Inv satisfying the usual inductiveness conditions. We could also use an even more general definition of refinement, like behavior-based refinement. (Actually, this might be desirable for other reasons, as it would let us freely and locally introduce 'history' into state machines, which has come up in a few hypotheticals.) Either way, we need to pick some generic definition of refinement which actually composes properly, but which is implied by our usual TLA-style refinement statement. (Of course, we would define generic module-theorems that transform one style into another, so we'd keep writing proofs as before.)

[jonhnet]

* impossible to write a generic composition proof within the module system (no such proof would be allowed to rely on an SMT condition like A.Inv ==> B.Inv) Why not? Why can't the proof prototype module be abstract, leaving a body-less lemma Inv, so that if you want to instantiate the proof module, you have to supply an implementation of Inv to complete the proof?

On 2021-07-13 08:53, Travis Hance wrote: Currently our refinement structure looks like: we have a bunch of state machines, A, B, C, ... etc. with refinement theorems of the form A_Refines_B.i.dfy. These are all named pretty consistently (although something much less consistent is the state machine invariants; sometimes the invariants for A are in the A file itself, and sometimes they are in separate files). Sometimes, the A_Refines_B.i.dfy files are interesting, and sometimes they are not. There are a lot of files A_Refines_C which simply compose two existing refinements, A_Refines_B and B_Refines_C. All these 'composition' refinements have nearly the exact same boiler plate. With a "module system" on the horizon, we can start to think about writing a generic refinement composition proof. See this proof-of-concept [1]. However, there's another issue that needs to be taken care of first, which has to do with the way the refinement theorems are stated. Here's a typical refinement theorem statement (Betree_Refines_Map.i.dfy): lemma RefinesNext(s: Betree.Variables, s':Betree.Variables, uiop: UI.Op) requires Inv(s) requires Betree.Next(s, s', uiop) ensures Inv(s') ensures MS.Next(I(s), I(s'), uiop) { // ... } Note that this has Inv(s) as a pre-condition. Often, the interpretation function in these refinements has Inv as a precondition as well. The consequence of this is that A_Refines_B only composes with B_Refines_C if A.Inv implies B.Inv. This is problematic for a bunch of reasons, including: * It makes it impossible to write a generic composition proof within the module system (no such proof would be allowed to rely on an SMT condition like A.Inv ==> B.Inv) * Creates long dependency chains where invariants include other invariants that they don't really need.(*) This is bad for proof isolation. (*) One (the only?) exception is ByteBlockCacheSystem, which includes the invariants of BlockCacheSystem for nontrivial reasons. The solution to this is to define our generic refinement theorem without reference to 'Inv'. For example, we could use 'Reachable' instead (i.e., Reachable(s) := exists s0...sn . Init(s) && (forall i . Next(s_i, s_(i+1))) && sn == s). Reachable is the universal invariant which implies Inv for any predicate Inv satisfying the usual inductiveness conditions. We could also use an even more general definition of refinement, like behavior-based refinement. (Actually, this might be desirable for other reasons, as it would let us freely and locally introduce 'history' into state machines, which has come up in a few hypotheticals.) Either way, we need to pick some generic definition of refinement which actually composes properly, but which is implied by our usual TLA-style refinement statement. (Of course, we would define generic module-theorems that transform one style into another, so we'd keep writing proofs as before.) -- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub [2], or unsubscribe [3].

Links: ------ [1] https://github.com/secure-foundations/dafny/blob/mod-params-bryan/Test/modules/StateMachineRefinement.dfy [2] #2 [3] https://github.com/notifications/unsubscribe-auth/AAN3OZEVIWORKP6AWKXFBJ3TXROOTANCNFSM5AJNZ22A

[tjhance]

you're right, you could leave a body-less lemma. But what I want, ideally, is to just instantly create the refinement tower by a giant module functor application. I don't want to have a bunch of boilerplate where I refine each module each step of the way just to instantiate a body-less lemma.

Actually, thinking more about it, there's probably another fairly simple thing to do, which is to make Inv an obligation of the refinement theorem module. (As opposed to having a single canonical Inv for the state machine.) So when you compose two refinements, you could just redeclare Inv to be whatever you need (although this is spiritually the same thing as the Reachable proposal).

[tjhance]

Here's an example of a Refinement definition that should be composable:

abstract module Refinement(ifc: Ifc, A: StateMachine(ifc), B: StateMachine(ifc)) {
  predicate Inv(s: A.Variables)

  lemma InitImpliesInv(s: A.Variables)
  requires A.Init(s)
  ensures Inv(s)

  lemma NextPreservesInv(s: A.Variables, s': A.Variables, op: ifc.Op)
  requires Inv(s)
  requires A.Next(s, s', op)
  ensures Inv(s')

  function I(s: A.Variables) : B.Variables
  requires Inv(s)

  lemma InitRefinesInit(s: A.Variables)
  requires A.Init(s)
  requires Inv(s)
  ensures B.Init(I(s))

  lemma NextRefinesNext(s: A.Variables, s': A.Variables, op: ifc.Op)
  requires Inv(s)
  requires Inv(s')
  requires A.Next(s, s', op)
  ensures B.Next(I(s), I(s'), op)
}

[parno]

In NextRefinesNext, I think you could move the Inv(s') into the ensures clause, no? It should be provable directly from NextPreservesInv. I assume it's necessary in the signature of NextRefinesNext so that in the ensures, Dafny doesn't complain about I(s'), but putting Inv(s') as the first ensures should cover that.

[tjhance]

we already have NextPreservesInv as an obligation, so it's all equivalent

[parno]

As written, any caller of NextRefinesNext will need to invoke NextPreservesInv, whereas if you make the adjustment I suggested, that wouldn't be necessary.