goose

README

Goose: a subset of Go with a semantics in Coq

Goose is a subset of Go equipped with a semantics in Coq, as well as translator to automatically convert Go programs written in Go to a model in Coq. The model plugs into Perennial for carrying out verification of concurrent storage systems.

Goose includes a reasonable subset of Go, enough to write serious concurrent programs. The translator and semantics are trusted; you can view the process as giving a semantics to Go. The semantics is given via a translation to GooseLang, an untyped lambda calculus with references and concurrency, including some special support to work for Go.

Demo: an example conversion

To give a flavor of what goose does, let's look at an example:

File append_log.go:

// Append-only, sequential, crash-safe log.
//
// The main interesting feature is that the log supports multi-block atomic
// appends, which are implemented by atomically updating an on-disk header with
// the number of valid blocks in the log.
package append_log

import (
	"sync"

	"github.com/tchajed/marshal"

	"github.com/tchajed/goose/machine/disk"
)

type Log struct {
	m      *sync.Mutex
	sz     uint64
	diskSz uint64
}

func (log *Log) mkHdr() disk.Block {
	enc := marshal.NewEnc(disk.BlockSize)
	enc.PutInt(log.sz)
	enc.PutInt(log.diskSz)
	return enc.Finish()
}

func (log *Log) writeHdr() {
	disk.Write(0, log.mkHdr())
}

func Open() *Log {
	hdr := disk.Read(0)
	dec := marshal.NewDec(hdr)
	sz := dec.GetInt()
	diskSz := dec.GetInt()
	return &Log{m: new(sync.Mutex), sz: sz, diskSz: diskSz}
}

Goose output:

(* autogenerated from append_log *)
From Perennial.goose_lang Require Import prelude.
From Perennial.goose_lang Require Import ffi.disk_prelude.

From Goose Require github_com.tchajed.marshal.

(* Append-only, sequential, crash-safe log.

   The main interesting feature is that the log supports multi-block atomic
   appends, which are implemented by atomically updating an on-disk header with
   the number of valid blocks in the log. *)

Module Log.
  Definition S := struct.decl [
    "m" :: lockRefT;
    "sz" :: uint64T;
    "diskSz" :: uint64T
  ].
End Log.

Definition Log__mkHdr: val :=
  rec: "Log__mkHdr" "log" :=
    let: "enc" := marshal.NewEnc disk.BlockSize in
    marshal.Enc__PutInt "enc" (struct.loadF Log.S "sz" "log");;
    marshal.Enc__PutInt "enc" (struct.loadF Log.S "diskSz" "log");;
    marshal.Enc__Finish "enc".

Definition Log__writeHdr: val :=
  rec: "Log__writeHdr" "log" :=
    disk.Write #0 (Log__mkHdr "log").

Definition Open: val :=
  rec: "Open" <> :=
    let: "hdr" := disk.Read #0 in
    let: "dec" := marshal.NewDec "hdr" in
    let: "sz" := marshal.Dec__GetInt "dec" in
    let: "diskSz" := marshal.Dec__GetInt "dec" in
    struct.new Log.S [
      "m" ::= lock.new #();
      "sz" ::= "sz";
      "diskSz" ::= "diskSz"
    ].

Go support

Goose doesn't support arbitrary Go code; it uses a carefully-selected subset of Go that is still idiomatic Go (for the most part) while being easy to translate. See the implementation design doc for more details.

There are three aspects of the Go model worth mentioning here:

• Assignments are not supported, only bindings. This imposes a "linearity" restriction where each variable is constant after being first defined, which aligns well with how Perennial code works. Mutable variables can still be emulated using pointers and heap allocation.
• Goose supports a few common control flow patterns so code can be written with early returns and some loops.
• Many operations are carefully modeled as being non-linearizable in Perennial, although this area is subtle and hard to reconcile with Go's documented memory model.

Related approaches

Goose solves the problem of using Perennial to verify runnable systems while ensuring some connection between the verification and the code. How else do verification projects get executable code?

Extraction is a popular approach, especially in Coq. Extraction is much like compilation in that Coq code is translated to OCaml or Haskell, relying on many similarities between the languages. (Side note: the reason it's called extraction is that it also does proof erasure, where proofs mixed into Coq code are removed so they don't have to be run.) To get side effects in extracted code the verification engineers write an interpreter in the target language that runs the verified part, using the power of the target language to interact with the outside world (eg, via the console, filesystem, or network stack).

A big disadvantage of extraction is performance. The source code is several steps away from the extracted code and interpreter. This distance makes it hard to debug performance problems and reduces developers' control over what the running code does.

Another approach is to use a deeply-embedded language that closely represents an efficient imperative language, such as C. Then one can write code directly in this language (eg, Cogent), produce it as part of proof-producing synthesis (eg, Fiat Cryptography), import it from normal source code (eg, clightgen for VST). Regardless of how the code in the language is produced, this approach requires a model of the syntax and semantics of the language at a fairly low-level, including modeled function calls, variable bindings, and local stacks, not to mention concurrency and side effects.

Directly modeling a low-level, imperative language (and especially writing in it) gives a great deal of control, which is good for performance. This approach is also well-suited to end-to-end verification: at first, one can pretty-print the imperative language and use any compiler, but eventually one can shift to a verified compiler and push the assumptions down the software stack.

Running goose

Goose requires Go 1.12+.

You can install goose with either go get github.com/tchajed/goose/cmd/goose or from a clone of this repo with go install ./cmd/goose. These install the goose binary to $GOPATH/bin (or ~/go/bin if you don't have GOPATH set).

To run goose on one of the internal examples and update the Coq output in Perennial, run (for the append_log example):

goose -out $perennial/src/goose_lang/examples/append_log.v \
  ./internal/examples/append_log

where $perennial is the path to a clone of Perennial.

Developing goose

The bulk of goose is implemented in goose.go (which translates Go) and internal/coq/coq.go (which has structs to represent Coq and GooseLang code, and code to convert these to strings).

Goose has integration tests that translate example code and compare against a "gold" file in the repo. Changes to these gold files are hand-audited when they are initially created, and then the test ensures that previously-working code continues to translate correctly. To update the gold files after modifying the tests or fixing goose, run go test -update-gold (and manually review the diff before committing).

The tests include internal/examples/unittest, a collection of small examples intended for wide coverage, as well as some real programs in other directories within internal/examples.

The Coq output is separately tested by building it within the Perennial source tree.

Additionally, the internal/examples/semantics package contains a set of semantic tests for checking that translated programs preserve their semantic meaning. The testing infrastructure requires test functions to have the form func test*() bool and return true (that is, they begin with "test", take no arguments, and return a bool expected to always be true). Any helper functions should not follow this pattern.

The cmd/test_gen/main.go file generates the required test files from these functions. The files are:

• A .go file which uses the Go testing package. This is for confirming that tests actually do always return true, as intended. Note that the use of the testing package means that this file must end in _test.go. It should go in the semantics/ directory.
• A .v file that runs using Perennial's semantic interpreter. This file should go in Perennial's goose_lang/interpreter/ directory and can have any name.

To generate these files, the executable takes a required flag of either -go or -coq which specifies the file type, an optional -out argument specifying where to write the output, and finally the path to the semantics package. For example, go run ./cmd/test_gen -coq -out ~/code/perennial/src/goose_lang/interpreter/generated_test.v ./internal/examples/semantics generates the Coq file of semantics tests. (You'll probably need to adjust the path to Perennial.) To re-generate the Go test file you can just run go generate ./....

Documentation

Overview

Package goose implements conversion from Go source to Perennial definitions.

The exposed interface allows converting individual files as well as whole packages to a single Coq Ast with all the converted definitions, which include user-defined structs in Go as Coq records and a Perennial procedure for each Go function.

See the Goose README at https://github.com/tchajed/goose for a high-level overview. The source also has some design documentation at https://github.com/tchajed/goose/tree/master/docs.

Index

• Constants
• type Config
  • func MakeDefaultConfig() Config
  • func (config Config) TranslatePackage(pkgPath string, srcDir string) (coq.File, error)
• type ConversionError
  • func (e *ConversionError) Error() string
• type Ctx
  • func NewCtx(pkgPath string, fset *token.FileSet, config Config) Ctx
  • func (ctx Ctx) Decls(fs ...NamedFile) (decls []coq.Decl, errs []error)
  • func (ctx Ctx) TypeCheck(pkgName string, files []*ast.File) error
• type MultipleErrors
  • func (es MultipleErrors) Error() string
• type NamedFile
  • func (f NamedFile) Name() string
• type StringSet
  • func (s *StringSet) Set(value string) error
  • func (s *StringSet) String() string

Constants

const FfiImportFmt string = "From Perennial.goose_lang Require Import ffi.%s_prelude."

Types

type Config

type Config struct {
	AddSourceFileComments bool
	TypeCheck             bool
	Ffi                   string
	Excludes              StringSet
}

Config holds global configuration for Coq conversion

func MakeDefaultConfig

func MakeDefaultConfig() Config

Returns the default config

func (Config) TranslatePackage

func (config Config) TranslatePackage(pkgPath string, srcDir string) (coq.File, error)

TranslatePackage translates an entire package in a directory to a single Coq Ast with all the declarations in the package.

If the source directory has multiple source files, these are processed in alphabetical order; this must be a topological sort of the definitions or the Coq code will be out-of-order. Realistically files should not have dependencies on each other, although sorting ensures the results are stable and not dependent on map or directory iteration order.

type ConversionError

type ConversionError struct {
	Category string
	// the main description of what went wrong
	Message string
	// the snippet in the source program responsible for the error
	GoCode string
	// (for internal debugging) file:lineno for the goose code that threw the
	// error
	GooseCaller string
	// file:lineno for the source program where GoCode appears
	GoSrcFile string
	// (for systematic tests)
	Pos, End token.Pos
}

A ConversionError is a detailed and structured error encountered while converting Go to Coq.

Errors include a category describing the severity of the error.

The category "unsupported" is the only error that should result from normal usage, when attempting to use a feature goose intentionally does not support.

"todo" and "future" are markers for code that could be supported but is not currently handled.

The categories "impossible(go)" and "impossible(no-examples)" indicate a bug in goose (at the very least these cases should be checked and result in an unsupported error)

func (*ConversionError) Error

func (e *ConversionError) Error() string

type Ctx

type Ctx struct {
	Config
	// contains filtered or unexported fields
}

Ctx is a context for resolving Go code's types and source code

func NewCtx

func NewCtx(pkgPath string, fset *token.FileSet, config Config) Ctx

NewCtx initializes a context

func (Ctx) Decls

func (ctx Ctx) Decls(fs ...NamedFile) (decls []coq.Decl, errs []error)

Decls converts an entire package (possibly multiple files) to a list of decls

func (Ctx) TypeCheck

func (ctx Ctx) TypeCheck(pkgName string, files []*ast.File) error

TypeCheck type-checks a set of files and stores the result in the Ctx

This is needed before conversion to Coq to disambiguate some methods.

type MultipleErrors

type MultipleErrors []error

func (MultipleErrors) Error

func (es MultipleErrors) Error() string

type NamedFile

type NamedFile struct {
	Path string
	Ast  *ast.File
}

func (NamedFile) Name

func (f NamedFile) Name() string

type StringSet

type StringSet map[string]bool

Implement flag.Value for a "set" of strings; used by Config

func (*StringSet) Set

func (s *StringSet) Set(value string) error

func (*StringSet) String

func (s *StringSet) String() string