Abstracting memory with predicate interface members

In Gobra we can include predicate signatures within an interface. This feature is particularly significant for abstracting memory, as interfaces define methods rather than fields, so we cannot specify access to concrete fields. Each implementation must define its own predicate to abstract memory access. Consequently, an interface can specify required behaviors without imposing constraints on the underlying data representation.

As an example, we consider the Image interface from the Go standard library. It includes methods to retrieve the color Model (which itself is an interface) as well as a method to obtain a valid Color (also an interface) for a given pixel at coordinates (x, y).

The predicate Mem represents memory access and the ghost and pure function Inv represents an invariant that holds for the data structure storing the image.

// Image is a finite rectangular grid of [Color] values taken from a color
// model.
type Image interface {
	// Mem represents the access to the memory of the Image
	// @ pred Mem()	// <----- Predicate member

	// Invariant that holds for valid images
	// @ ghost
	// @ pure
	// @ requires acc(Mem(), _)
	// @ decreases
	// @ Inv() bool

	// ColorModel returns the Image's color model.
	ColorModel() Model

	// Bounds returns the domain for which At can return non-zero color.
	// The bounds do not necessarily contain the point (0, 0).
	// @ requires acc(Mem(), _)
	// @ pure
	// @ decreases
	Bounds() (r Rectangle)

	// At returns the color of the pixel at (x, y).
	// At(Bounds().Min.X, Bounds().Min.Y) returns the upper-left pixel of the grid.
	// At(Bounds().Max.X-1, Bounds().Max.Y-1) returns the lower-right one.
	// @ preserves acc(Mem(), 1/2)
	// @ preserves Inv()
	// @ ensures c != nil && c.Valid()
	// @ ensures !Point{x, y}.In(Bounds()) ==> (c.RGBASpec() == rgba{})
	At(x, y int) (c Color)
}

// A Point is an X, Y coordinate pair. The axes increase right and down.
type Point struct {
	X, Y int
}

// In reports whether p is in r.
// @ pure
// @ decreases
func (p Point) In(r Rectangle) (res bool) {
	return r.Min.X <= p.X && p.X < r.Max.X &&
		r.Min.Y <= p.Y && p.Y < r.Max.Y
}

// A Rectangle contains the points with Min.X <= X < Max.X, Min.Y <= Y < Max.Y.
// It is well-formed if Min.X <= Max.X and likewise for Y. Points are always
// well-formed. A rectangle's methods always return well-formed outputs for
// well-formed inputs.
//
// A Rectangle is also an [Image] whose bounds are the rectangle itself. At
// returns color.Opaque for points in the rectangle and color.Transparent
// otherwise.
type Rectangle struct {
	Min, Max Point
}

Additionally, the boundaries of an image are encapsulated within a Rectangle struct, retrievable with the Bounds method. For points not contained in this rectangle, At must return zero color. We define zero color in terms of the RGBA method, or more precisely the corresponding pure and ghost method RGBASpec. Since pure methods must have exactly one parameter, we cannot return r, g, b, a. Instead, we define the ghost type rgba. So, rgba{} represents the zero color.

/*@
ghost type rgba ghost struct {
	r, g, b, a uint32
}

ghost
pure
decreases
func (c rgba) ColorRange() bool {
	return 0 <= c.r && c.r <= c.a && 0 <= c.g && c.g <= c.a &&
		0 <= c.b && c.b <= c.a && c.a <= 0xffff
}
@*/

// Color can convert itself to alpha-premultiplied 16-bits per channel RGBA.
// The conversion may be lossy.
type Color interface {
	// Returns true if the implementation holds a valid color.
	// @ ghost
	// @ pure
	// @ decreases
	// @ Valid() bool

	// @ ghost
	// @ requires Valid()
	// @ ensures c.ColorRange()
	// @ pure
	// @ decreases
	// @ RGBASpec() (ghost c rgba)

	// RGBA returns the alpha-premultiplied red, green, blue and alpha values
	// for the color. Each value ranges within [0, 0xffff], but is represented
	// by a uint32 so that multiplying by a blend factor up to 0xffff will not
	// overflow.
	//
	// An alpha-premultiplied color component c has been scaled by alpha (a),
	// so has valid values 0 <= c <= a.
	// @ preserves Valid()
	// @ ensures RGBASpec() == rgba{r, g, b, a}
	RGBA() (r, g, b, a uint32)
}

The type *Alpha16Image implements the Image interface. To implement the interface any predicates defined for the interface must be implemented. Here, the Mem predicate's body contains access to all fields of the struct, especially the elements of the Pix slice holding the image's pixel values.


// Alpha16Image is an in-memory image whose At method returns [color.Alpha16] values.
type Alpha16Image struct {
	// Pix holds the image's pixels, as alpha values in big-endian format. The pixel at
	// (x, y) starts at Pix[(y-Rect.Min.Y)*Stride + (x-Rect.Min.X)*2].
	Pix []uint8
	// Stride is the Pix stride (in bytes) between vertically adjacent pixels.
	Stride int
	// Rect is the image's bounds.
	Rect Rectangle
}

/*@
pred (p *Alpha16Image) Mem() {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/

The pure and ghost function Inv represents an invariant that has to hold for the image. This invariant states that the entire entire size of the pixel slice is given by the stride times the height of the image: p.Stride*(p.Rect.Max.Y-p.Rect.Min.Y) == len(p.Pix), where the stride is the distance in bytes between vertically adjacent pixels. Note that the factor 2 in p.Stride == 2*(p.Rect.Max.X-p.Rect.Min.X) is due to the fact that each pixel uses 2 elements of the Pix slice for storage. Additionally, the elements of the pixel slice are of type uint8, so they have values in the range from 0 to 0xff. While this could be inferred from the type alone, we have to state this due to a current limitation in Gobra.

/*@
ghost
requires acc(p.Mem(), _)
pure
decreases
func (p *Alpha16Image) Inv() bool {
	return unfolding acc(p.Mem(), _) in (2*(p.Rect.Max.X-p.Rect.Min.X) == p.Stride &&
    	p.Stride * (p.Rect.Max.Y-p.Rect.Min.Y) == len(p.Pix)) &&
    	forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> 0 <= p.Pix[i] && p.Pix[i] <= 0xff
}
@*/

Please note that the annotations of the implementation and the interface must match. A method defined as ghost in the interface, must also be implemented as ghost. The same applies to pure methods. An error is reported, for example, when we leave out pure for Inv:

ERROR  *Alpha16Image does not implement the interface Image
	reason: For member Inv, the 'pure' annotation for implementation and interface does not match
(*Alpha16Image) implements Image
^

The remaining methods:

ColorModel is trivially implemented.
For Bounds, we unfold the Mem predicate to obtain the concrete permission to read the field p.Rect.
The method At is the trickiest to verify as we have to prove that the offset in the Pix array is within bounds, which we explain below.


func (p *Alpha16Image) ColorModel() Model { return Alpha16Model }

// @ requires acc(p.Mem(), _)
// @ pure
// @ decreases
func (p *Alpha16Image) Bounds() (r Rectangle) {
	return /*@ unfolding acc(p.Mem(), _) in @*/ p.Rect
}

// @ requires acc(p.Mem(), 1/2)
// @ requires p.Inv()
// @ ensures acc(p.Mem(), 1/2)
// @ ensures p.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures !Point{x, y}.In(p.Bounds()) ==> (c.RGBASpec() == rgba{})
func (p *Alpha16Image) At(x, y int) (c Color) {
	// @ unfold acc(p.Mem(), 1/2)
	if !(Point{x, y}.In(p.Rect)) {
		// @ fold acc(p.Mem(), 1/2)
		return Alpha16{}
	}
	// @ fold acc(p.Mem(), 1/2)
	i := p.PixOffset(x, y)
	// @ unfold acc(p.Mem(), 1/2)
	c = Alpha16{uint16(p.Pix[i+0])*256 + uint16(p.Pix[i+1])}
	// @ fold acc(p.Mem(), 1/2)
	return
}

// PixOffset returns the index of the first element of Pix that corresponds to
// the pixel at (x, y).
// @ requires acc(p.Mem(), 1/4)
// @ requires p.Inv()
// @ requires Point{x, y}.In(p.Bounds())
// @ ensures acc(p.Mem(), 1/4)
// @ ensures p.Inv()
// @ ensures unfolding acc(p.Mem(), 1/4) in 0 <= offset && offset < len(p.Pix)-1
func (p *Alpha16Image) PixOffset(x, y int) (offset int) {
	// @ unfold acc(p.Mem(), 1/4)
	offset = (y-p.Rect.Min.Y)*p.Stride + (x-p.Rect.Min.X)*2
	// @ LemmaMulPos(y-p.Rect.Min.Y, p.Rect.Max.Y-p.Rect.Min.Y-1, p.Stride)
	// @ fold acc(p.Mem(), 1/4)
	return
}

/*@
ghost
requires a <= b
requires c >= 0
ensures a * c <= b * c
decreases
func LemmaMulPos(a, b, c int) {}
@*/

Due to current limitations with bit operations, we replaced the bit-shift (<<) and bitwise OR (|) operations with arithmetic operations. The original source used the following line.

c = Alpha16{uint16(p.Pix[i+0])<<8 | uint16(p.Pix[i+1])}

Note that the rewrite works because p.Pix has elements of type uint8.

We must show that PixOffset returns an offset satisfying 0 <= offset && offset < len(p.Pix) - 1. As Point{x, y} is contained in the rectangle p.Rect, (y-p.Rect.Min.Y) >= 0 and (x-p.Rect.Min.X) >= 0. Since stride is non-negative, 0 <= offset immediately follows.

TODO @João note about non-linear arithmetic

To prove offset < len(p.Pix) - 1, we help Gobra by providing proof annotations. For the sake of explanation, we give verbose annotations. Please note that they are not strictly necessary. In the body of PixOffset above, a reduced proof is given.

We will need the assertions from Inv:

assert 2 * (p.Rect.Max.X - p.Rect.Min.X) == p.Stride && p.Stride * (p.Rect.Max.Y - p.Rect.Min.Y) == len(p.Pix)

First, we define a few ghost variables as abbreviations to simplify the offset calculation. We can assert upper bounds on dx and dy, again since the point is contained in the rectangle.

offset = (y-p.Rect.Min.Y)*p.Stride + (x-p.Rect.Min.X)*2
ghost var height = p.Rect.Max.Y - p.Rect.Min.Y
ghost var dy = y-p.Rect.Min.Y
ghost var dx = (x-p.Rect.Min.X) * 2
assert offset == dy * p.Stride + dx
assert 0 <= dx && 0 <= dy && 0 <= offset
assert dy <= height - 1
assert dx <= p.Stride - 2

Next, we make use of the simple arithmetic fact that for \(a, b, c \in \mathbb{N}\) the following holds: \(a \leq b \implies a \cdot c \leq b \cdot c \). We define this lemma as a ghost function and invoke it with the appropriate arguments.

LemmaMulPos(y-p.Rect.Min.Y, p.Rect.Max.Y-p.Rect.Min.Y-1, p.Stride)

Afterwards, we can rewrite the inequality and arrive at the desired fact.

assert dy * p.Stride + dx <= (height - 1) * p.Stride + dx
assert offset <= (height - 1) * p.Stride + p.Stride - 2
assert offset <= len(p.Pix) - 2

The following example uses *Alpha16Image as an Image:

func clientAlpha() {
	var i Image
	a := &Alpha16Image{
		Pix:    []uint8{0x0, 0x0, 0xff, 0xff, 0xff, 0xff, 0x0, 0x0},
		Stride: 4,
		Rect:   Rectangle{Point{0, 0}, Point{2, 2}},
	}
	// @ fold a.Mem()
	i = a
	i.ColorModel()
	// @ assert i.Inv()
	c := i.At(-1, 0)
	// @ assert(c.RGBASpec() == rgba{})
}

Implementation without memory footprint

A Rectangle is also an Image, with bounds equal to the rectangle itself. For points within the rectangle, Opaque color is returned and Transparent color otherwise. No memory access is required in this case, and no invariant must be preserved. The predicate Mem and the function Inv still have to be defined to implement Image. We simply have true as the body and the return value respectively.

/*@
// Mem implements the [Image] interface.
pred (r Rectangle) Mem() {
	true
}

// Inv implements the [Image] interface.
ghost
decreases
pure func (r Rectangle) Inv() bool {
	return true
}
@*/

// ColorModel implements the [Image] interface.
func (r Rectangle) ColorModel() Model {
	return Alpha16Model
}

// Bounds implements the [Image] interface.
// @ requires acc(r.Mem(), _)
// @ pure
// @ decreases
func (r Rectangle) Bounds() (res Rectangle) {
	return r
}

// At implements the [Image] interface.
// @ preserves acc(r.Mem(), 1/2)
// @ preserves r.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures Point{x, y}.In(r.Bounds()) == (c.RGBASpec() != rgba{})
func (r Rectangle) At(x, y int) (c Color) {
	if (Point{x, y}).In(r) {
		return Alpha16{0xffff} // Opaque
	}
	return Alpha16{0} // Transparent
}

// @ Rectangle implements Image

The full example with all image related interfaces can be found here.

Practical Program Verification in Go with Gobra (alpha)

Abstracting memory with predicate interface members

Implementation without memory footprint