Goose tutorial

11/2/25literate

Goose tutorial

Use this as a reference, as well as a guide for the Rocq-specific details of how Goose works.

Basic setup

The prelude here wraps New.proof.proof_prelude, which gives the basics needed for program proofs.

Goose supports an "FFI" for defining custom external operations and state (used to model the file system and distributed systems, for example). Most Perennial proofs don't use any FFI features, so they are generic in the FFI (it's an additional Context parameter in the proofs). In sys_verif to simplify the context a bit we instead use a fixed "empty" FFI with no operations.

From sys_verif.program_proof Require Import prelude empty_ffi.

All our proofs have a convention for where they are stored, both because goose requires it (to know where to import dependencies) and to make program proofs easier to navigate. They are all based on putting the proof for a Go package at a systematic directory. For example, the Go package github.com/tchajed/marshal will use the path github_com/tchajed/marshal.v.

Goose first translates that package in two parts, one trusted (generated by the goose binary) and one untrusted (generated by the proofgen binary). You generally won't interact with the translation process because the output is committed to the repo, but the script ./etc/update-goose.sh will re-run the translation in case you want to try out some new code.

The trusted code goes in the Rocq path New.code.<package path>, the untrusted proofs go in New.generatedproof.<package path>, and finally we put the program proofs in New.proof.<package path>. (This repo breaks this last convention.)

(You might wonder how our proofs end up in the New namespace in Rocq. This is because this is a logical path, and the _CoqProject is able to map both Perennial and this repo's directories to New.)

Our code is in the Go path sys_verif_code/heap, as defined by go/go.mod, so that's where we'll import it from. The code is re-exported from the generated proof, so technically you only need to import that.

From New.code.sys_verif_code Require Import heap.
From New.generatedproof.sys_verif_code Require Import heap.

The heap package we're demoing a proof of depends on std, the verified "Goose standard library".

From New.proof Require Import std.

This base file sets a few global Rocq settings.

From Perennial Require Import base.

(* Some boilerplate is needed to set up a proof. These are assumptions that are
dispatched by initialization, a process that runs before any other program code. *)
Section proof.
Context `{hG: !heapGS Σ}.
Context `{!globalsGS Σ} {go_ctx: GoContext}.

Every Go package must define its initialization predicate, a proposition that should hold after it is initialized. Goose has a global variable that holds the body of every function and method, which is used to dispatch function and method calls (this allows arbitrary recursion). Part of initialization is setting up those global variables. Next, global variables are initialized to their initialization expressions (constants are handled by the goose translator and do not need initialization). Finally, packages can include an init() function, which runs last.

Initialization predicates are only needed for global variables and init() functions, which are relatively rare, so we typically just need to give an instance of this typeclass that says the initialization predicate is True.

These initialization predicates should only be defined once, but multiple files prove different subsets of the heap package, so the correct thing to do is to factor out the initialization (as we do in heap_init.v).

#[global] Instance : IsPkgInit heap := define_is_pkg_init True%I.
#[global] Instance : GetIsPkgInitWf heap := build_get_is_pkg_init_wf.

A first program proof

Now we are ready to state a specification for an example function!

The code we'll specify and verify is

func ExampleA(x *bool, y *uint64, z uint64) {
	if *x {
		*y = z
	} else {
		*y = 0
	}
}

Since Perennial specifications use weakest preconditions ("WPs") under the hood, we have a convention of verifying the function Foo as a lemma called wp_Foo.

The first interesting aspect of this specification is the function expression being verified. We write @! heap.ExampleA #x_l #y_l #z0. The @! heap.ExampleA represents a function call to ExampleA from the heap package. This is actually going to look up the code for that function, and this will only work due to the is_pkg_init heap precondition. The function arguments are all written by using # on some Gallina (pure Rocq) value. You will pervasively see in Perennial that we use a Galina type to represent program data, but then convert it to a GooseLang value with #x. The example below uses this for three different types: loc (the type of locations, used for pointer values), bool, and w64 (a 64-bit machine word).

Now let's look at the precondition. First we need is_pkg_init heap to be able to call the function. Then we have two points-to assertions, since the function takes two pointers and reads from both. These don't need #x0 and #y0 because it would be redundant; the points-to always takes the Gallina value.

Lemma wp_ExampleA (x_l: loc) (x0: bool) (y_l: loc) (y0: w64) (z0: w64) :
  {{{ is_pkg_init heap ∗ x_l ↦ x0 ∗ y_l ↦ y0 }}}
    @! heap.ExampleA #x_l #y_l #z0
  {{{ RET #(); x_l ↦ x0 ∗ y_l ↦ (if x0 then z0 else W64 0) }}}.
Proof.

Recall that a Hoare triple {P} e {Q} actually means $\forall Φ, P \wand (Q \wand Φ) \wand wp(e, Φ)$ . wp_start introduces the $Φ$ , precondition, and wand for the postcondition. If you give it an intro pattern, it uses that to destruct the precondition.

wp_start is also smart and automatically introduces is_pkg_init facts and puts them away, so you don't need to mention them in the intro pattern.

  wp_start as "[Hx Hy]".

  (* `wp_auto` handles must allocations, but you will need to use `wp_alloc` if
  names conflict or if the allocation doesn't have a name in the Go code. *)
  wp_alloc z as "z".
  (* `wp_pures` is run by `wp_auto` (the latter also handles loads and stores) *)
  wp_pures.
  wp_alloc y as "y".
  wp_pures.
  wp_alloc x as "x".
  wp_pures.
  (* `wp_load` should essentially not be needed since you can use `wp_auto`.
  However, if things aren't working this tactic will report a better error message. *)
  wp_load.
  wp_load.

  (* Use this when the next expression is an `if` to split the proof into the
  two branches. *)
  wp_if_destruct.

Goal

  x_l, y_l : loc
  y0, z0 : w64
  Φ : val → iPropI Σ
  z, y, x : loc
  ============================
  _ : is_pkg_init heap
  --------------------------------------□
  "Hx" : x_l ↦ true
  "Hy" : y_l ↦ z0
  "HΦ" : x_l ↦ true ∗ y_l ↦ z0 -∗ Φ (# ())
  "z" : z ↦ z0
  "y" : y ↦ y_l
  "x" : x ↦ x_l
  --------------------------------------∗
  Φ (# ())

  - (* start bullets for the two cases of wp_if_destruct *)

At the end of the function, we will always need to prove Φ v where v is the return value on that branch. In this case, that return value is #() - that is, the conversion of the empty tupe () to a Goose value. Since Φ is arbitrary, you're always going to prove this with HΦ, the assumption we made as part of the Hoare triple definition.

    iApply "HΦ".
    iFrame.
  - (* wp_finish just does `iApply "HΦ"` followed by some very simple automation
    if the resulting postcondition is easy to solve. *)
    wp_finish.
Qed.

A list of useful tactics

WP tactics (for program proofs):

name	description
`wp_start`, `wp_start as "ipat"`	Begin a proof of a separation logic triple
`wp_pures`	"Step through" any pure computation steps
`wp_auto`	`wp_pures` plus `wp_load` and `wp_auto` for load and store operations
`wp_pure`	Single step of `wp_pure` (needed for slice operations)
`wp_bind`	Find the next expression that will execute and use the bind rule to "focus" it
`wp_apply`	Wrapper around `iApply` that uses `wp_bind`
`wp_if_destruct`	If the goal is about an `if:` expression, attempt to destruct the condition
`iAssert ... as "IH"`, `wp_for "IH"`	Typical pattern for stating the loop invariant and then starting a proof about a loop.
`wp_for_post`	Handles a goal of the form `for_postcondition`

IPM tactics:

You will need to understand what an ipat is (an intro pattern) and what an spat is (a specialization pattern).

ipat includes "[H1 H2]", %H, and (H1 & H2 & H3) (this being sugar for "[H1 [H2 H3]]").

spat includes "[H1 H2]" (note this now selects H1 and H2, it's not destructing), "[$H]", and "H".

tactic
`iIntros ipat`
`iDestruct "H" as ipat`
`iDestruct (lemma with spat) as ipat`
`iSplitL hyps`
`iSplitR hyps`
`iFrame`
`iPureIntro`

Some Rocq tactics:

name
`word`
`congruence`
`done`
`destruct`
`intros`
`simpl`
`rewrite`

Some useful lemmas:

lemma	description
`own_slice_len`	If you have `s ↦* xs` (an own_slice assertion), used to relate `slice.len_f s` to `length xs`. See the wp_SliceSwap example.
`bool_decide_eq_true_2`, `bool_decide_eq_false_2`	Used to prove `bool_decide P = true` or `bool_decide P = false`
`wp_load_slice_elem`, `wp_store_slice_elem`	Use with `wp_apply` to reason about loading/storing slice elements
`struct_fields_split`	Split a struct pointsto `x_l ↦ x` (where `x` is a struct) into fields points-to facts of the form `x_l ↦s[StructName :: "field"] a`.

Note that you won't get much out of the theorem statement for struct_fields_split - its behavior is to split a struct points-to into individual field points-to's, but the exact theorem statement is defined automatically by proofgen for each struct.

End proof.