Adding an element to a set corresponding to a replica fails

[curiousperson-art]

I have an abstract representation of a model where I have two isolates : replica (that contains a set/array) and is totally ordered and another isolate that performs operations on a set belonging to a certain replica. I have an inductive invariant which states that for any two different replicas, if their set sizes are same, the sets have the same elements and in the same order. This fails, but the counter example produced by Ivy is giving a wrong behavior when an element is added to an array. If you look at the picture, we see that there are 3 sets and 2 replicas. The 2 replicas point to two different sets (arr = 0, arr = 1) at first, and after the add operation has been executed at replica R1 points to arr = 2 and the index remains 0. I fail to understand the reason for this behavior. How do I eliminate three sets and make the replica point to the same set as it was pointing before? Here is my code :

#lang ivy1.7
include collections
include order
include deduction

type elem
instance index : unbounded_sequence
instance arr : array(index,elem)

module total_order_properties(t) = 
{
     property [transitivity] X:t < Y & Y < Z -> X < Z
     property [antisymmetry] ~(X:t < Y & Y < X)
     property [totality] X:t < Y | X = Y | Y < X
}


isolate replica = 
{

     type this 
     function setrep(X:replica) : arr
     axiom [inejectivity] setrep(X) = setrep(Y) -> X = Y
     after init
     {
        setrep(X) := arr.create(0,0);
     }
     specification 
     {
        instantiate total_order_properties(this)
     }
     implementation 
     {
         interpret this -> bv[1]
     }
 }


isolate gset_protocol = 
{
    type this
    relation repEqual(R1:replica,R2:replica)
    relation send(R:replica,E:elem) 
    relation member(R:replica,E:elem)
    #v is a replica
    action add(v:replica,e:elem) 
    after init
    {
	#initially no replica has anything set
	send(R,E) := false;
    }
    specification 
    {

	definition member(R:replica,E:elem) = exists Z. 0 <= Z & Z < replica.setrep(R).end & replica.setrep(R).value(Z) = E
        definition repEqual(R1:replica,R2:replica) = (forall Z. 0 <= Z & Z < replica.setrep(R1).end & replica.setrep(R1).value(Z) = replica.setrep(R2).value(Z)) 

	before add 
	{
		send(v,e) := true;
	}
	after add 
	{
		send(R,e) := true;
	}
    }
    implementation 
    {
	implement add(v:replica,e:elem) 
	{
		require send(v,e);
		if (replica.setrep(v).end = 0) | ~member(v,e)
            	{
		 	replica.setrep(v) := arr.resize(replica.setrep(v),replica.setrep(v).end.next,e);
            	}

	}
    }
    private 
    {
          invariant ((R1:replica ~= R2) & (replica.setrep(R1).end = replica.setrep(R2).end) & replica.setrep(R1).end > 0) -> repEqual(R1,R2) 
    }
}with replica

interpret elem -> int
export gset_protocol.add

[kenmcmil]

The problem is that arr is also an isolate. To use the specification of arr.resize, you need to add arr to the "with" clause of gset_protocol.

A few other comments: your isolate 'replica' is not very helpful because it doesn't provide an abstract interface to setrep. That abstract interface is really provided by member and repEqual. So I would suggest moving setrep into the implementation of gset_protocol. Also, move arr into the the implementation of gset_protocol, since it should not be used outside the isolate. Then you don't need to put arr in the "with" clause, since it is a sub-isolate of gset_protocol.

Also, send looks to me like it is intended to be specification state. You probably want to move its declaration and initializer into the specification section. And you probably don't want to put a requirement on send in the implementation, since send if send is not intended to be implementation state. In general, you shouldn't have "require" in the implementation section, since that is a guarantee for the calling isolate, which doesn't see the implementation code. If you really want an assertion in implementation code, you should use "ensure". Then the assertion will be a guarantee for gset_protocol.

Finally, you should be careful about axioms such as injectivity. Axioms are OK temporarily, but they can invalidate your verification. As an example, the axiom is not consistent with the initializer for setrep. As it happens, this will not cause an inconsistency because the "extensionality" property for arrays (saying two arrays are equal when their contents are equal) is not used by default. In general, though, axioms are risky.

[curiousperson-art]

I did the changes that you suggested. I have moved the array definition and setrep inside gset_protocol. But the invariant fails again and I fail to understand why as both sets pertaining to the replicas are containing the same element after add operation (and in this counter example one element only). I still have the injectivity condition and I feel it is needed as on deleting it, i see both replicas pointing to the same arr which i do not want. I want every replica to have their copy of set.