Documentation
¶
Overview ¶
Package machine is a support library for operations on integers.
Goose code can use these additional functions. They have corresponding primitives and a model in the Goose `Heap.v` model of Go's built-in heap data structures, under the `Data` module.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Assert ¶
func Assert(c bool)
Assert induces a proof obligation that `c` is true.
The Go implementation will panic (quit the process in a controlled manner) if `c` is not true. In GooseLang, it will make the machine stuck, i.e., cause UB.
func Assume ¶
func Assume(c bool)
Assume lets the proof assume that `c` is true. *Use with care*, assumptions are trusted and should be justified!
The Go implementation will panic (quit the process in a controlled manner) if `c` is not true. (Not to be confused with GooseLang `Panic` which is UB.) In GooseLang, it will loop infinitely.
func Linearize ¶
func Linearize()
Linearize does nothing.
Translates to an atomic step that supports opening invariants conveniently for the sake of executing a simulation fancy update at the linearization point of a procedure..
func RandomUint64 ¶
func RandomUint64() uint64
RandomUint64 returns a random uint64 using the global seed.
func UInt64Get ¶
UInt64Get converts the first 8 bytes of p to a uint64.
Requires p be at least 8 bytes long.
Happens to decode in little-endian byte order, but this is only relevant as far as the relationship between UInt64Get and UInt64Encode.
func UInt64Put ¶
UInt64Put stores n to the first 8 bytes of p
Requires p to be at least 8 bytes long.
Uses little-endian byte order, but this is only relevant in that it's the inverse of UInt64Get.
func UInt64ToString ¶
UInt64ToString formats a number as a string.
Assumed to be pure and injective in the Coq model.
Types ¶
This section is empty.
Source Files
Directories