Pure functions and permissions

Recall that pure functions have no side effects. Hence, they must not leak any permissions and implicitly return all permissions mentioned in the precondition. While pure functions can require write permission, they cannot actually modify values, as this would be a side effect.

The pure and ghost function allZero returns whether all elements of an array behind a pointer are zero. After allocation with new, the array is filled with zero values, and this can be asserted.

package ghostpure

const N = 42
/*@
ghost
requires forall i int :: 0 <= i && i < len(*s) ==> acc(&((*s)[i]))
decreases
pure func allZero(s *[N]int) bool {
    return forall i int :: 0 <= i && i < len(*s) ==> (*s)[i] == 0
}
@*/

func client() {
    xs := new([N]int)
    // @ assert allZero(xs)
    // implicitly transferred back
    // @ assert acc(xs)
}

Pure functions implicitly return all permissions mentioned in the precondition.