Can invariant be proven from other invariants?

[marcelotaube]

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]

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.