Predicates and fractional permissions

Predicate instances are resources, i.e., permissions are used to track access to them. So far, we have been using l.Mem(), a shorthand for specifying a permission amount of 1 to the predicate instance l.Mem(). Equivalently, we can write acc(l.Mem()) or acc(l.Mem(), 1) using the access predicate.

We may specify a permission amount' pforfold, unfold, and unfolding. In this case, any permission amount in the body of the predicate is multiplied by p. For example, the body of l.Mem()containsacc(l)andl.next.Mem(). After unfold acc(l.Mem()), only acc(l, 1/2)andacc(l.next.Mem(), 1/2)` are held.

func fractional() {
	l := New(1, Empty())
	// @ assert l.Mem()
	// @ assert acc(l.Mem())
	// @ assert acc(l.Mem(), 1)

	// @ unfold acc(l.Mem(), 1/2)
	// @ assert acc(l.Mem(), 1/2)
	// @ assert acc(l, 1/2) && acc(l.next.Mem(), 1/2)
	// @ fold acc(l.Mem(), 1/2)
	// @ assert l.Mem()
}

List methods such as Head and Get do not need write permissions. Hence, we change their contracts to only require acc(l.Mem(), 1/2), and update any fold operations to use the correct permission amount. We still require write access for methods like Remove that modify the List. For now, disregard l.View() in the contracts.

// Head returns the value of the first element in the list.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ requires !l.IsEmpty()
// @ ensures value == l.View()[0]
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l.Value
}

// Get returns the element at index i in the list.
// @ preserves acc(l.Mem(), 1/2)
// @ preserves 0 <= i && i < len(l.View())
// @ ensures value == l.View()[i]
// @ decreases l.Mem()
func (l *List) Get(i int) (value int) {
	// @ unfold acc(l.Mem(), 1/2)
	if i == 0 {
		value = l.Value
	} else {
		value = l.next.Get(i - 1)
	}
	// @ fold acc(l.Mem(), 1/2)
	return
}

// Remove returns the list with the element at index i deleted.
// @ requires l.Mem()
// @ requires 0 <= i && i < len(l.View())
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[:i] ++ l.View()[i+1:])
func (l *List) Remove(i int) (out *List) {
	// @ unfold l.Mem()
	if i == 0 {
		return l.next
	}
	l.next = l.next.Remove(i - 1)
	// @ fold l.Mem()
	return l
}

Fractional permissions are crucial to frame properties. When retaining a positive permission amount across a call of Get, we know the list is not modified. If write permissions were required, the contract would need to state that the list does not get modified explicitly.

For pointers, acc(x, 2) implies false. For predicates, we may have permission amounts larger than 1. For example, we can have acc(p2(l), 2), which denotes access to two predicate instances p2(l).

/*@
pred p2(l *List) {
	acc(&l.next, 1/2) && (l.next != nil ==> p2(l.next))
}
@*/

func client2() {
	l := &List{Value: 1, next: nil}
	// @ fold p2(l)
	// @ assert acc(p2(l), 1)
	// @ fold p2(l)
	// @ assert acc(p2(l), 2)
}