std

README

Verified Goose standard library

Written in Goose for verification in Iris.

To translate with goose (in the repo directory):

goose -out ~/code/perennial/external/Goose

To makes changes you'll need to submit a pull request so that CI can run first.

Documentation

Index

• func Assert(b bool)
• func BytesClone(b []byte) []byte
• func BytesEqual(x []byte, y []byte) bool
• func Multipar(num uint64, op func(uint64))
• func SignedSumAssumeNoOverflow(x int, y int) int
• func Skip()
• func SliceSplit[T any](xs []T, n uint64) ([]T, []T)
• func SumAssumeNoOverflow(x uint64, y uint64) uint64
• func SumNoOverflow(x uint64, y uint64) bool
• type JoinHandle
  • func Spawn(f func()) *JoinHandle
  • func (h *JoinHandle) Join()

Functions

func Assert

func Assert(b bool)

Assert(b) panics if b doesn't hold

func BytesClone

func BytesClone(b []byte) []byte

See the reference.

func BytesEqual

func BytesEqual(x []byte, y []byte) bool

BytesEqual returns if the two byte slices are equal.

func Multipar

func Multipar(num uint64, op func(uint64))

Multipar runs op(0) ... op(num-1) in parallel and waits for them all to finish.

Implementation note: does not use a done channel (which is the standard pattern in Go) because this is not supported by Goose. Instead uses mutexes and condition variables since these are modeled in Goose

func SignedSumAssumeNoOverflow

func SignedSumAssumeNoOverflow(x int, y int) int

func Skip

func Skip()

Skip is a no-op that can be useful in proofs.

Occasionally a proof may need to open an invariant and perform a ghost update across a step in the operational semantics. The GooseLang model may not have a convenient step, but it is always sound to insert more. Calling std.Skip() is a simple way to do so - the model always requires one step to reduce this application to a value.

func SliceSplit

func SliceSplit[T any](xs []T, n uint64) ([]T, []T)

SliceSplit splits xs at n into two slices.

The capacity of the first slice overlaps with the second, so afterward it is no longer safe to append to the first slice.

func SumAssumeNoOverflow

func SumAssumeNoOverflow(x uint64, y uint64) uint64

SumAssumeNoOverflow returns x + y, `Assume`ing that this does not overflow.

*Use with care* - if the assumption is violated this function will panic.

func SumNoOverflow

func SumNoOverflow(x uint64, y uint64) bool

Returns true if x + y does not overflow

Types

type JoinHandle

type JoinHandle struct {
	// contains filtered or unexported fields
}

JoinHandle is a mechanism to wait for a goroutine to finish. Calling `Join()` on the handle returned by `Spawn(f)` will wait for f to finish.

func Spawn

func Spawn(f func()) *JoinHandle

Spawn runs `f` in a parallel goroutine and returns a handle to wait for it to finish.

Due to Goose limitations we do not return anything from the function, but it could return an `interface{}` value or be generic in the return value with essentially the same implementation, replacing `done` with a pointer to the result value.

func (*JoinHandle) Join

func (h *JoinHandle) Join()