Questions on "Shared Structs"

[felixlinker]

In Shared Structs there is the example of the Cord struct and permissions given to its field. I don't understand why the Scale function requires permissions to the fields of c. In my mental model, a pointer to a struct like this points to a continuous area of memory for which one must have permissions. So one would only need permissions to access the pointer for the struct but not the ints as permissions to the ints is subsumed by the permission to access the struct.

I wonder whether this is something that may be worth clarifying.

[ArquintL]

Go allows one to obtain the pointers to individual struct fields. For this reason (among others), Gobra uses separate permissions for struct fields. Since Coord.Scale modifies both x and y struct fields, this function requires full permissions to both struct fields.
What probably confuses you is the fact that we often write acc(c) instead, which is syntactic sugar for "forall field of type[*c]. acc(&c.field)". In this example, acc(c) = acc(&c.x) && acc(&c.y).

[felixlinker]

No, I don't think that's my confusion. I know about this equivalence, but it doesn't fit my mental model about permissions.

Why do we need express permissions about things that never can be nil if the struct pointer is nil, but NOT about the struct pointer - which could be nil? If I receive I non-nil pointer to a struct, I'll find a struct where every field will have an "allowed" value. They could be nil, if it's a pointer, but I'd need to reason about that separately.

I guess, maybe in my mental model l think of permissions as being required for things that could or could not be nil. But maybe it's rather correct to say you require permissions for everything that is readable? A struct is not "really" addressable. You cannot read it. You can only read it's values. That does become weird, though, when we nest pointers to structs in structs.

[ArquintL]

Let's see whether this helps a bit:
Ignoring predicates for now, a permission always belongs to an addressable memory entity h on the heap (think a memory entity storing an int). We identify a permission for h via its address, i.e., &h.
In the following example, new allocates such a memory entity to which p will point (think p == &h):

p := new(int)
*p = 42
assert acc(p)

To me, permissions are all about can I or can I not access a particular memory entity. Non-nilness is simply a corollary to me as it's impossible to access a memory entity to which the nil-pointer points (as we agreed to never store a memory entity at address zero).

In the context of structs, it's quite easily gets a bit more complicated, in particular if you think of your example type S struct { arr *[1]int }. However, it helps me sometimes to think of C: calculating the address of a field for a pointer p of type *S does not require permissions as it's pure pointer arithmetic (taking the struct's layout in memory into account; the same holds for calculating the address to an array element). Thus, &p.arr is computed by taking the address p and (probably) adding offset zero to it. Only when we try to read the value stored in this field (which is of type *[1]int), we actually require permissions to do so (namely acc(&p.arr)). Since p.arr is of pointer type, I can either be nil or non-nil. In the latter case, dereferencing the pointer to the array and reading the array's singleton element requires another permission, namely acc(p.arr).

edit: as pointed out by @jcp19, the paragraph above is not entirely correct and is based on Gobra's current behavior. This will however change once we merge Gobra PR #531.

[felixlinker]

After a bit of back-and-forth, I think I finally understood it. I made a suggestion in #51 on how to potentially address this, and I agree, Linard, that the book could introduce permissions for a struct as a short-hand much earlier.