Private Specification, Partial Struct Encoding, and Constructor

[vizual1]

1. Added the pvt() function into Gobra that takes an expression and gives a boolean to indicate if it is private within the package (it does not get imported from other packages). Currently, it is used inside the type checker. Additionally, it can be used inside specifications:

requires pvt(E)
preserves pvt(E)
ensures pvt(E)
func foo(E typ)

assert pvt(foo)

are all valid expressions right now. There may be some bugs for pure functions and predicates because they are imported into other packages with the body.

2. Added private specifications for functions and methods. To ensure soundness, a private proof statement is added into the private specification. It is written as:

requires P
ensures Q
private {
  requires p
  ensures q
  proof foo {
    R = foo(A)
  }
}
func foo(A) R

3. Changed how the private fields of structs get encoded (on import), by removing the private fields and changing it into a partial_struct. For example, if we have a struct with private field c and import it into another package:

type S struct { 
  Left, Right, c int 
}

then it would be changed into

type bar.S partial_struct {
  Left, Right int
}

In the viper encoding a partial_struct removes an axiom from the Tuple Domain to disallow the comparison of two partial_structs.

func foo(x, y bar.S) {
  if (x.Left == y.Left && x.Right = y.Right) {
    assert x == y //fail
  }
}

In viper that means:

// if we removed the private field without changing the encoding (struct)
domain Tuple2[A, B] {
  function get0(t: Tuple2[A, B]): A
  function get1(t: Tuple2[A, B]): B
  function create2(a: A, b: B): Tuple2[A, B]

  axiom {
    forall t: Tuple2[A, B] :: {get0(t)} {get1(t)} t == create2(get0(t), get1(t))
  }

  axiom {
    forall a: A, b: B :: {create2(a,b)} get0(create2(a,b)) == a && get1(create2(a,b)) == b
  }
}

get changed to:

// if we removed the private field and change the encoding (partial_struct)
domain Tuple2[A, B] {
  function get0(t: Tuple2[A, B]): A
  function get1(t: Tuple2[A, B]): B
  function create2(a: A, b: B): Tuple2[A, B]

  axiom {
    forall a: A, b: B :: {create2(a,b)} get0(create2(a,b)) == a && get1(create2(a,b)) == b
  }
}

Please check the written code and if additional documentations are needed in some places. (Also there might be some small bits of a constructor, which is not finished yet.)

[Felalolf]

First batch of comments.

[vizual1]

4. Added a construct, dereference, and assignment declaration to be able to define and abstract permission for structs.

type T struct { F, g int }

pred (t *T) Mem() { acc(&t.g) }

ensures acc(&this.F) && this.Mem()
construct &T() {
  fold this.Mem()
}

requires acc(&this.F) && this.Mem()
pure deref &T() {
  return unfolding this.Mem() in *this
}

requires acc(&this.F) && this.Mem()
ensures acc(&this.F) && this.Mem()
ensures *this == rhs //deref(this)
assign &T(rhs T) {
  unfold this.Mem()
  *this = rhs
  fold this.Mem()
}

The specifications need to be public.

[Felalolf]

More comments. I have not yet looked at the desugarer, the ConstructorEncoding, the AssignmentEncoding, and the DerefEncoding

[Felalolf]

I would have expected that for CompleteStruct it is always sh.convertToExclusive(...) and for PartialStruct, it is always the call to the deref function (there is an error if there is no deref function).

[vizual1]

If we always use sh.convertToExclusive(...) for a CompleteStruct, then this statement would fail:

requires acc(&a.Left) && acc(&a.Right) && a.PrivateMem()
func foo(a *Pair) {
  x := *a // fails, not enough permission
}

Since there is no call to dereference, Pair that has fields Left, Right, p does not have access to the field p (within the same package until we unfold a.PrivateMem()). The constructor always gets called once defined, therefore:

x := &Pair{Left: 2, Right: 0, p: 1}
assert(x.PrivateMem()) //constructor ensures x.PrivateMem()

and the assignment y := *x would fail, despite constructing x just before.

The question is if we want to explicitly unfold x.PrivateMem() or just let the dereference handle it.

[Felalolf]

More comments. I have not yet looked at the desugarer, the ConstructorEncoding, the AssignmentEncoding, and the DerefEncoding