Behavioral subtypes

Interfaces in Go are defined as a set of method signatures. In Gobra, we can add signatures and contracts to the interface definitions. It must be proven that the implementation is a behavioral subtype of the interface, i.e., it provides not only at least the same methods, but also at least the same behavior:

The precondition of each interface method must imply the precondition of each corresponding implementation method
The postcondition of each implementation method must imply the postcondition of each corresponding interface method.

In this section, we look at interfaces from the image package from the Go standard library. As a first example, we consider the Color interface with a single method RGBA that returns color components for red, green, blue, and alpha.

// 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

	// 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 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
	RGBA() (r, g, b, a uint32)
}

// source: https://cs.opensource.google/go/go/+/refs/tags/go1.24.0:src/image/color/color.go;l=10

We add a contract to the signature that formalizes the docstring, which states that each value falls within the range [0, 0xffff] and "an alpha-premultiplied color component c has been scaled by alpha (a), so has valid values 0 <= c <= a." Furthermore, we add a ghost and pure method Valid to the interface. With Valid, implementations provide an assertion that must hold for the data structure such that a valid color can be returned.

The type Alpha16, which represents a 16-bit alpha color:

// Alpha16 represents a 16-bit alpha color.
type Alpha16 struct {
	A uint16
}

// @ preserves c.Valid()
// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}

In Go, interface implementation is implicit, i.e., the Color interface is implemented by defining an RGBA method. For Gobra, any ghost methods such as Valid must be implemented as well.

/*@
ghost
decreases
pure func (c Alpha16) Valid() bool {
	return 0 <= c.A && c.A <= 0xffff
}
@*/

Gobra checks that Alpha16 is a behavioral subtype of Color only when needed, that is, when an value of interface type has Alpha16 as its underlying type. For example, this occurs when we assign a value to a variable of interface type or pass an argument to a function with an in-parameter of interface type.

The following client verifies since the postcondition of Alpha16's RGBA is equivalent to the postcondition of the interface method.

func client1Alpha() {
	var c Color
	c = Alpha16{0xffff}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

The implementation's postcondition may be stronger. For example, the Constant color guarantees that it always returns the same color components. From this, the postcondition of the interface immediately follows.

type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

/*@
ghost
decreases
pure func (c Constant) Valid() bool {
	return true
}
@*/

func client1Constant() {
	var c Color
	c = Constant{}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

Similarly, the implementation's precondition may be weaker.

Implementation precondition too strong

Gobra reports an error if the precondition of an implementation method might not follow from the precondition of the corresponding interface method.

In the following example, acc(c.p) is required to call RGBA with receivers of type Fail1. The function client has a parameter of interface type, whose concrete type is unknown. When c.RGBA() is called, the precondition of the interface method must hold. However, this does not imply the precondition of Fail1's RGBA. Hence, it would be unsound to allow Fail1 to be used as a value of type Color.

type Fail1 struct {
	p *uint32
}

// @ requires acc(c.p)
// @ requires c.Valid()
// @ ensures r <= 0xffff && g <= 0xffff && b <= 0xffff && a <= 0xffff
func (c Fail1) RGBA() (r, g, b, a uint32) {
	a = *c.p
	return a, a, a, a
}

/*@
ghost
requires acc(c.p)
decreases
pure func (c Fail1) Valid() bool {
	return 0 <= *c.p && *c.p <= 0xffff
}
@*/

func client2(c Color) {
	c = Fail1{new(uint32)}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

ERROR Generated implementation proof (Fail1 implements interface{ RGBA }) failed. Precondition of call to implementation method might not hold. 
Permission to c.p might not suffice.

ERROR Precondition of call c.RGBA() might not hold. 
Assertion Valid() might not hold.

Implementation postcondition too weak

An error is reported if the postcondition of an implementation method might not imply the postcondition of the corresponding interface method.

type Fail2 struct{}

// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a
// @ ensures c.Valid()
func (c Fail2) RGBA() (r, g, b, a uint32) {
	return 255, 255, 255, 255
}

/*@
ghost
decreases
pure func (c Fail2) Valid() bool {
	return true
}
@*/

func client3() {
	var c Color
	c = Fail2{}
}

ERROR Generated implementation proof (Fail2 implements interface{ RGBA }) failed. Postcondition of interface method might not hold. 

Assertion a <= 0xffff might not hold.

In the above example, the postcondition a <= 0xffff is missing from the contract of the implementation. It does not follow from the given postcondition:

// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a

So far, we have relied on generated implementation proofs from Gobra. In a following section, we show how to provide our own implementation proofs.

The precondition of the interface method must imply the precondition of the implementation method.

The postcondition of the implementation method must imply the postcondition of the interface method.

Full section example

package main

// 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

	// 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 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
	RGBA() (r, g, b, a uint32)
}

// source: https://cs.opensource.google/go/go/+/refs/tags/go1.24.0:src/image/color/color.go;l=10

// Alpha16 represents a 16-bit alpha color.
type Alpha16 struct {
	A uint16
}

// @ preserves c.Valid()
// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}


/*@
ghost
decreases
pure func (c Alpha16) Valid() bool {
	return 0 <= c.A && c.A <= 0xffff
}
@*/

func client1Alpha() {
	var c Color
	c = Alpha16{0xffff}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}


type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

/*@
ghost
decreases
pure func (c Constant) Valid() bool {
	return true
}
@*/

func client1Constant() {
	var c Color
	c = Constant{}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

Practical Program Verification in Go with Gobra (alpha)

Behavioral subtypes

Implementation precondition too strong

Implementation postcondition too weak

Full section example