Documentation
¶
Overview ¶
Package machine is a support library for generic Go primitives.
GooseLang provides models for all of these operations.
Index ¶
- func Assert(c bool)
- func Assume(c bool)
- func Exit(n uint64)
- func Linearize()
- func MapClear[M ~map[K]V, K comparable, V any](m M)
- func RandomUint64() uint64
- func Sleep(ns uint64)
- func TimeNow() uint64
- func UInt32Get(p []byte) uint32
- func UInt32Put(p []byte, n uint32)
- func UInt64Get(p []byte) uint64
- func UInt64Put(p []byte, n uint64)
- func UInt64ToString(x uint64) string
- func WaitTimeout(cond *sync.Cond, timeoutMs uint64)
- type ProphId
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! Note that these are *runtime-checked* assumptions, i.e., the worst-case here is having the program panic in unexpected ways.
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 MapClear ¶
func MapClear[M ~map[K]V, K comparable, V any](m M)
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.
func WaitTimeout ¶
WaitTimeout is like cond.Wait(), but waits for a maximum time of timeoutMs milliseconds.
Not provided by sync.Cond, so we have to (inefficiently) implement this ourselves.
Types ¶
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
Package filesys is a support library providing access to a single directory in the filesystem.
|
Package filesys is a support library providing access to a single directory in the filesystem. |