search

microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
225 stars 80 forks source link

Can invariant be proven from other invariants? #19

Open marcelotaube opened 6 years ago

marcelotaube commented 6 years ago

This example does not check in ivy:

#lang ivy1.7

type node
isolate nset = {
    type this
    relation member(N:node, S:this)
    individual emptyset : nset
    invariant ~member(N, emptyset)
    implementation {

        relation _member(N:node, S:this)
        definition member(N, S) = _member(N, S)
        after init {
            _member(N, emptyset) := false;
        }
    }
}
with node

object localstate = {
    individual my_voters : nset
    invariant ~nset.member(VOTER, my_voters) 
    after init {
        my_voters := nset.emptyset;
    }
} #localstate

isolate ilocalstate = localstate with nset, node

The problem seems to be invariant ~nset.member(VOTER, my_voters):

$ ivy_check test.ivy 

Isolate ilocalstate:

    The inductive invariant consists of the following conjectures:
        test.ivy: line 22: localstate.invar4

    The following initializers are present:
        test.ivy: line 23: localstate.init[after5]

    Initialization must establish the invariant
        test.ivy: line 22: localstate.invar4 ... FAIL

This is strange because invariant ~member(N, emptyset) passes correctly and is exactly the same content, I expected to prove one from the other.

Notice that if I expose all the code from nset (without using the implement keyword) the code passes:

#lang ivy1.7

type node
isolate nset = {
    type this
    relation member(N:node, S:this)
    individual emptyset : nset
    invariant ~member(N, emptyset)
    #implementation {
        relation _member(N:node, S:this)
        definition member(N, S) = _member(N, S)
        after init {
            _member(N, emptyset) := false;
        }
    #}
}
with node

object localstate = {
    individual my_voters : nset
    invariant ~nset.member(VOTER, my_voters) 
    after init {
        my_voters := nset.emptyset;
    }
} #localstate

isolate ilocalstate = localstate with nset, node
kenmcmil commented 6 years ago

This behavior is correct according to the current semantics. That is, an invariant is only established after the initialization phase. That means you can't rely on it in an initializer. Instead, you can add an "after init" specification, like this:

 #lang ivy1.7

type node
isolate nset = {
    type this
    relation member(N:node, S:this)
    individual emptyset : nset
    invariant ~member(N, emptyset)
    implementation {

        relation _member(N:node, S:this)
        definition member(N, S) = _member(N, S)
        after init {
            _member(N, emptyset) := false;
        }
    }

    specification {
        after init {
           ensure ~member(N, emptyset)
        }
    }
}
with node

object localstate = {
    individual my_voters : nset
    invariant ~nset.member(VOTER, my_voters) 
    after init {
        my_voters := nset.emptyset;
    }
} #localstate

isolate ilocalstate = localstate with nset, node

The ensure executes after the initialization of _member but before the initialization of my_voters.