add examples

src/test/resources/regressions/features/pkg_init/byte/byte.go

@@ -0,0 +1,53 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// @ dup pkgInvariant acc(StaticInv(), _)
+
+package byte
+
+type Byte struct {
+	value byte
+}
+
+var byteCache /*@@@*/ [256]*Byte
+
+func init() {
+	// @ invariant 0 <= i && i <= 256 && acc(&byteCache)
+	// @ invariant (forall j, k uint16 :: 0 <= j && j < k && k < i  ==>
+	// @ 	byteCache[j] != byteCache[k])
+	// @ invariant (forall j uint16 :: 0 <= j && j < i ==>
+	// @ 	acc(byteCache[j]) && byteCache[j].value == byte(j) - 128)
+	// @ decreases 256 - i
+	for i := 0; i < 256; i++ {
+		byteCache[i] = alloc(byte(i) - 128)
+	}
+	// @ fold StaticInv()
+}
+
+// @ ensures acc(&res.value) && res.value == val
+// @ decreases
+// @ mayInit
+func alloc(val byte) (res *Byte) {
+	res = new(Byte)
+	res.value = val
+	return res
+}
+
+// @ pure
+// @ requires acc(b.Mem(), _)
+// @ decreases
+func (b *Byte) ByteValue() byte {
+	return /*@ unfolding acc(b.Mem(), _) in @*/ b.value
+}
+
+// @ ensures acc(res.Mem(), _)
+// @ ensures res.ByteValue() == val
+// @ decreases
+func ToVal(val byte) (res *Byte) {
+	// @ assume -128 <= val && val <= 127
+	// @ openDupPkgInv
+	// @ unfold acc(StaticInv(), _)
+	res = byteCache[val+128]
+	// @ fold acc(res.Mem(), _)
+	return res
+}

src/test/resources/regressions/features/pkg_init/byte/byte_spec.gobra

@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package byte
+
+pred StaticInv() {
+	acc(&byteCache, _) &&
+	// for injectivity checks:
+	(forall j, k uint16 :: 0 <= j && j < k && k < 256  ==>
+		byteCache[j] != byteCache[k]) &&
+	(forall i uint16 :: 0 <= i && i < 256 ==>
+		acc(byteCache[i], _) && byteCache[i].value == (byte)(i-128))
+}
+
+pred (b *Byte) Mem() {
+	acc(b, _)
+}

src/test/resources/regressions/features/pkg_init/concfib/fib.go

@@ -0,0 +1,72 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// @ dup pkgInvariant acc(StaticInv(), _)
+
+package concfib
+
+import "sync"
+
+var cache /*@@@*/ map[int]int = make(map[int]int)
+var lock *sync.Mutex = &sync.Mutex{}
+
+func init() {
+	cache[0] = 1
+	cache[1] = 1
+	// @ fold lockInv!<!>()
+	// @ lock.SetInv(lockInv!<!>)
+	// @ fold acc(StaticInv(), _)
+}
+
+// @ requires  0 <= n
+// @ ensures   res == FibSpec(n)
+// termination cannot be proven due to calls to Lock()
+func FibV1(n int) (res int) {
+	// @ openDupPkgInv
+	// @ unfold acc(StaticInv(), _)
+	lock.Lock()
+	// @ unfold lockInv!<!>()
+	if v, ok := cache[n]; ok {
+		// @ fold lockInv!<!>()
+		lock.Unlock()
+		return v
+	}
+	// @ fold lockInv!<!>()
+	lock.Unlock()
+	v := FibV1(n-1) + FibV1(n-2)
+	lock.Lock()
+	// @ unfold lockInv!<!>()
+	cache[n] = v
+	// @ fold lockInv!<!>()
+	lock.Unlock()
+	return v
+}
+
+// @ requires  0 <= n
+// @ ensures   res == FibSpec(n)
+// termination cannot be proven due to calls to Lock()
+func FibV2(n int) (res int) {
+	// @ openDupPkgInv
+	// @ unfold acc(StaticInv(), _)
+	lock.Lock()
+	v := fibImpl(n)
+	lock.Unlock()
+	return v
+}
+
+// @ requires  0 <= n
+// @ preserves lockInv!<!>()
+// @ ensures   res == FibSpec(n)
+// @ decreases n
+func fibImpl(n int) (res int) {
+	// @ unfold lockInv!<!>()
+	// @ defer fold lockInv!<!>()
+	if v, ok := cache[n]; ok {
+		return v
+	}
+	// @ fold lockInv!<!>()
+	v := fibImpl(n-1) + fibImpl(n-2)
+	// @ unfold lockInv!<!>()
+	cache[n] = v
+	return v
+}

src/test/resources/regressions/features/pkg_init/concfib/fib_spec.gobra

@@ -0,0 +1,37 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package concfib
+
+ghost
+pure
+requires 0 <= n
+decreases n
+func FibSpec(n int) int {
+	return n <= 1 ? 1 : FibSpec(n-1) + FibSpec(n-2)
+}
+
+pred lockInv() {
+	acc(&cache, _)     &&
+	acc(cache)         &&
+	0 in domain(cache) &&
+	1 in domain(cache) &&
+	forall i int :: { cache[i] }{ FibSpec(i) }{ i in domain(cache) } i in domain(cache) ==>
+		0 <= i && cache[i] == FibSpec(i)
+}
+
+pred StaticInv() {
+	acc(lock.LockP(), _) &&
+	lock.LockInv() == lockInv!<!>
+}
+
+// Given that we can always implement a ghost method like the one below to gain
+// access to the duplicable static invariants of a package, it is unecessary
+// to pass an import path or a package identifier to `openDupPkgInv`. Instead, we
+// can just define a method like this in every package and call it.
+ghost
+ensures acc(StaticInv(), _)
+decreases
+func AcquireDupPkgInv() {
+	openDupPkgInv
+}

src/test/resources/regressions/features/pkg_init/fib/fib.go

@@ -0,0 +1,31 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// @ pkgInvariant StaticInv()
+
+package fib
+
+var cache /*@@@*/ map[int]int = make(map[int]int)
+
+func init() {
+	cache[0] = 1
+	cache[1] = 1
+	// @ fold StaticInv()
+}
+
+// @ requires  0 <= n
+// @ preserves StaticInv()
+// @ ensures   res == FibSpec(n)
+// @ decreases n
+func Fib(n int) (res int) {
+	// @ unfold StaticInv()
+	// @ defer fold StaticInv()
+	if v, ok := cache[n]; ok {
+		return v
+	}
+	// @ fold StaticInv()
+	v := Fib(n-1) + Fib(n-2)
+	// @ unfold StaticInv()
+	cache[n] = v
+	return v
+}

src/test/resources/regressions/features/pkg_init/fib/fib_spec.gobra

@@ -0,0 +1,21 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package fib
+
+ghost
+pure
+requires 0 <= n
+decreases n
+func FibSpec(n int) int {
+	return n <= 1 ? 1 : FibSpec(n-1) + FibSpec(n-2)
+}
+
+pred StaticInv() {
+	acc(&cache, _)     &&
+	acc(cache)         &&
+	0 in domain(cache) &&
+	1 in domain(cache) &&
+	forall i int :: { cache[i] }{ FibSpec(i) }{ i in domain(cache) } i in domain(cache) ==>
+		0 <= i && cache[i] == FibSpec(i)
+}

src/test/resources/regressions/features/pkg_init/import/main.go

@@ -0,0 +1,97 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// @ dup pkgInvariant acc(DupPkgInv(), _)
+package main
+
+// ##(-I ../)
+
+import (
+	"concfib"
+	"fib"
+)
+
+// @ pred DupPkgInv() { acc(&x) && x == 10 }
+
+var x /*@@@*/ int = valX()
+
+// I am not super happy with having implicit free preconditions (which are sound) for
+// this function (it is incosistent with the design of main, where we
+// must provide the preconditions for main). Nonetheless, having to provide
+// a spec (including termination measures) for this function is a bit excessive.
+// An alternative would be to change the encoding for main.
+func init() {
+	// this function is checked to be mayInit
+	foo()
+
+	// this one is not checked for mayInit, it is imported.
+	y := fib.Fib(3)
+	// also, the call above requires fib.StaticInv(). We can actually
+	// perform this call because the runtime guarantes that the main thread of
+	// different static initializers does not interleave. Gobra checks that the
+	// invariant of all imported packages is preserved.
+
+	// @ assert fib.FibSpec(0) == 1
+	// @ assert fib.FibSpec(1) == 1
+	// @ assert fib.FibSpec(2) == 2
+	// @ assert fib.FibSpec(3) == 3
+	// @ assert y == 3
+	_ = y
+
+	// @ fold DupPkgInv()
+}
+
+func Test() {
+	x := concfib.FibV1(3)
+	// @ assert concfib.FibSpec(0) == 1
+	// @ assert concfib.FibSpec(1) == 1
+	// @ assert concfib.FibSpec(2) == 2
+	// @ assert concfib.FibSpec(3) == 3
+	// @ assert x == 3
+	_ = x
+}
+
+func TestOpenDupInv() {
+	// @ concfib.AcquireDupPkgInv()
+	// @ assert acc(concfib.StaticInv(), _)
+}
+
+// Must be marked with `mayInit`, otherwise Gobra throws an error in the declaration
+// of `x`. `mayInit` signals that a method might be called from the static initializer
+// of the package in which it is declared, and thus, it is not allowed to assume any
+// of its invariants. Notice that this is an implementation detail! This fact is not
+// considered part of the public interface of the function (if there is one). However,
+// we provide this detail with the function spec because we currently do not have any
+// systematic way of adding annotations regarding implementation details to Gobra.
+// @ mayInit
+// @ ensures r == 10
+// @ decreases
+func valX() (r int) {
+	return 10
+}
+
+// termination is necessary, otherwise `foo` cannot be
+// called from the static initializer.
+// @ mayInit
+// @ decreases
+func foo() {}
+
+// We check that no interface methods are annotated with mayInit.
+type I interface {
+	// @ decreases
+	m()
+}
+
+// the following precondition is checked to follow from all the non-duplicable
+// package invariants of all direct imports:
+// @ requires fib.StaticInv()
+// @ decreases
+func main() {
+	x := fib.Fib(3)
+	// @ assert fib.FibSpec(0) == 1
+	// @ assert fib.FibSpec(1) == 1
+	// @ assert fib.FibSpec(2) == 2
+	// @ assert fib.FibSpec(3) == 3
+	// @ assert x == 3
+	_ = x
+}

src/test/resources/regressions/features/pkg_init/invallinstances/client.go

@@ -0,0 +1,42 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// @ pkgInvariant PkgInv()
+
+package invallinstances
+
+// This example demonstrates the ability to have static invariants over all
+// allocated instances of a type (using the New function), as originally demoed
+// in Peter's paper (https://link.springer.com/chapter/10.1007/11526841_4)
+// with the Client class. Interestingly, the proof annotations for the allocator
+// (New) in this version and in the version from Peter are very similar even
+// though one is based in ownership types and the other is based in SL/IDF.
+
+var ids /*@@@*/ int
+
+// @ ghost var allocs@ set[*Client]
+
+func init() {
+	// @ fold PkgInv()
+}
+
+type Client struct {
+	id   int
+	name string
+}
+
+// @ preserves PkgInv()
+// @ ensures   res.Inv()
+// @ ensures   res.Allocated()
+// @ decreases
+func New(name string) (res *Client) {
+	// @ unfold PkgInv()
+	// @ defer fold PkgInv()
+	res = new(Client)
+	res.name = name
+	res.id = ids
+	ids += 1
+	// @ allocs = allocs union set[*Client]{res}
+	// @ fold res.Inv()
+	return res
+}