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(), which is 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.

For fold, unfold, and unfolding we may specify a permission amount p. In this case, any permission amount in the body of the predicate is multiplied by p. For example, the body of l.Mem() contains acc(l) and l.next.Mem(). After unfold acc(l.Mem()), only acc(l, 1/2) and acc(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. For methods like Remove that modify the List, we still require write access. 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 that the list is not modified. If write permissions were required, the contract would need to explicitly state that the list does not get modified.

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)
}