Perennial

Perennial's goose framework and program proofs, in Lean 4 on top of iris-lean. This branch (lean) is the primary branch. It covers Go programs translated by goose, with a crash semantics and crash adequacy theorem but no crash program logic.

Guides: docs/PERENNIAL_PROOF_TUTORIAL.md, docs/PERENNIAL_PROOF_REFERENCE.md, docs/IRIS_PROOF_MODE.md.

Design decisions

• One library, Perennial. Framework directories are UpperCamelCase (Perennial/Golang/Theory/Slice.lean); generated, spec and proof directories follow Go package paths (Perennial/Proof/github_com/tchajed/marshal.lean).

• One spec per Go function, in its own file. Perennial/Spec/<pkg>/<F>.lean holds the one Hoare triple of Go function F (T__M for a method), and Perennial/Proof/<pkg>/<F>.lean its proof, which takes the specs of its callees as hypotheses and imports only their Spec files; Perennial/Proof/<pkg>/Link.lean (generated by etc/gen-link.py) applies each proof to its callees' results, as <pkg>.wp_<F>, and Perennial/Proof/<pkg>.lean is the module clients import. See docs/PERENNIAL_PROOF_REFERENCE.md, "Layout of the program proofs".

• Standard WP, crashes in the semantics and adequacy only. GooseLang is an instance of iris-lean's Language, and proofs use iris-lean's wp, which has later credits and numLatersPerStep; there is no crash WP (wpc). The local and global state (state × GlobalState) form the single iris-lean State, CfgState. A crash and restart of the node (Crash, GooseLang/Lang.lean) kills every thread, gives the restarted program an arbitrary heap and a fresh Go runtime (no package initialized), and crashes each extension's local state by the extension's own relation (ExtSemantics.crash); the global state is kept. goose_crash_adequacy (GooseLang/CrashAdequacy.lean) is about executions with crashes (RealCrashNsteps, GooseLang/CrashLang.lean) of a boot program, which runs at the start and after every crash: each generation is proved with the standard WP, under the shared global ghost state and its own local ghost state (GooseLocalGS), from a client-chosen precondition P L of the generation's local ghost state L, which each generation's proof guarantees for the next generation after its crash, from its persistent crashed token (exclusive with the notCrashed that its state interpretation owns, GooseLang/CrashToken.lean). There are no crash reasoning principles yet (no crash_own). End-to-end example: the Go package goose/testdata/examples/crashfs, a boot program on a toy filesystem (GooseLang/Ext/Fs, Go side crashfs/fsext; not a sound model of a Linux filesystem, see GooseLang/Ext/Fs/Impl.lean) whose panic assertions never fire however many times the node crashes (crash_safety, Perennial/Proof/github_com/mit_pdos/perennial/goose/testdata/examples/crashfs/Results.lean).

• Distributed systems. A distributed system (GooseLang/DistLang.lean) is a list of nodes, each with its own thread pool and local state, sharing the global state; a step is a real thread-pool step of one node. goose_dist_adequacy (GooseLang/DistAdequacy.lean) is about its executions: each node's program is proved with the standard WP, under the shared global ghost state and its own local ghost state (nodeWp), after a global setup that may allocate the invariants the nodes share. There is no distributed program logic. With crashes (DistCrashNsteps), a node crashes at any time and restarts from a crashed local state with its boot program, the one program it has (no separate recovery procedure); goose_dist_crash_adequacy combines this with crash adequacy: each generation of each node is proved with the standard WP from a client-chosen precondition P i L, which it guarantees for the node's next generation, as in goose_crash_adequacy. End-to-end example: the Go package goose/testdata/examples/netfs, three nodes on a toy network (GooseLang/Ext/Net, Go side netfs/netext, whose primitives are stubs: the extension is a specification of a network) and the toy filesystem, where a node's reply after a reboot depends on the durability and order of its earlier writes, and whose panic assertions never fire however often the nodes crash (netfs_crash_safety, Perennial/Proof/github_com/mit_pdos/perennial/goose/testdata/examples/netfs/Results.lean).

• Bounded layer, time receipts and thread tokens. The trusted semantics BaseStep (and its iris-lean language gooseRealEctxiLang, GooseLang/Lang.lean) is the model of Go, but the language instance used by the program logic is a separate bounded layer (GooseLang/BoundedLang.lean): its state adds a fuel ⟨steps, threads⟩. Once the step fuel is exhausted, Go instructions stutter instead of stepping; this supports time receipts (Mével, Jourdan, Pottier, ESOP 2019; GooseLang/Receipts.lean): ⧗ n/⧖ n, with ⧗ N ⊢ False for the bound N = receiptBound GF. Once the thread fuel is exhausted, Fork stutters; a thread's exit returns thread fuel. This supports thread tokens (GooseLang/Threads.lean): threadToks n, one per live thread, with threadToks T ⊢ False for the bound T = threadBound GF, so that a counter backed by one token per pending goroutine (a sync.WaitGroup's) is below T, and that a stock of T - 1 copies of a resource lent to threads for their thread tokens never runs out (Proof/ThreadPool.lean; e.g. an RWMutex's reader tokens, Proof/sync/RWMutexThreads.lean). A token splits into T levels (levelTok l), each with its own T - 1 tokens, so that a thread can lend part of its token and keep the rest (sync.tokJoinL, pools at a level); the levels are ghost state only. For this the trusted semantics counts the live threads (state.threads): Fork e spawns e ;; ThreadExit and increments it, and the no-op ThreadExit decrements it. The bounds are unspecified parameters, not constants: they are fields of the ghost state ReceiptGS GF/ThreadGS GF (parts of GooseGlobalGS and of the per-generation GooseLocalGS, hence of HeapGS), so downstream files, whose sections already assume HeapGS, need no new argument, and the language instance and its PureExec/Atomic instances do not depend on them. A proof that needs a bound to be small takes a premise (wp_clock_incr in ProgramLogic/TimeReceiptsTest.lean takes receiptBound GF ≤ 2 ^ 64; wp_counter_register in ProgramLogic/ThreadTokensTest.lean takes threadBound GF ≤ 2 ^ 31). The adequacy theorems (goose_adequacy N T, goose_invariance N T, and the grove/disk ones) hold for every N and T: they allocate the ghost state with receiptBound GF = N and threadBound GF = T (hypotheses of the WP premise Hwp, which also receives the main thread's token, and from which the client discharges the proof's premises about the bounds; the main thread's postcondition must exclude panics, see "Panics" below) and are about real executions of fewer than N steps along which fewer than T threads are live, explicit hypotheses. See docs/PERENNIAL_PROOF_REFERENCE.md, "Time receipts" and "Thread tokens".

• Iris substrate. iris-lean provides the BI, proof mode, invariants, ghost maps, later credits and the WP. General-purpose libraries that iris-lean lacks (finite maps and sets, machine words, list lemmas) live in Perennial/Std.

  • Finite maps are Perennial.gmap K V (Perennial/Std/GMap.lean): finite partial functions, extensional so = is equality of bindings, needing only DecidableEq K. gset K = gmap K Unit. It is an iris-lean LawfulFiniteMap, so iris-lean's ghost_map/gen_heap apply.
  • Machine words are BitVec n (w64 = BitVec 64, ...). uint.Z x is (x.toNat : Int) and sint.Z x is x.toInt. Arithmetic side conditions are discharged with word, omega and bv_omega. Do not use bv_decide/native_decide: they trust native code (Lean.ofReduceBool); prove bitwise facts via toNat.
  • GoString is List w8.

• 64-bit platform. The Go semantics assumes a 64-bit platform: the word-sized types int, uint and uintptr are 64-bit (values w64). uintptr (go.UintptrSemantics, Perennial/Golang/Defn/Predeclared.lean) is an integer type like uint64. Pointer/unsafe.Pointer to/from uintptr conversions are not modelled: they are stuck.

• Integers and floats are bytes. A value of an integer or float type of w bytes (go.IsPlainScalar, Perennial/Golang/Defn/Predeclared.lean) is w heap cells holding its little-endian bytes, allocated together (AllocBytes) at any address. Loads and stores go byte by byte, and are stuck on a cell that is not a byte. The integer atomics of sync/atomic and the semaphores are byte atomics of their width (LoadBytes, SwapBytes, AddBytes, CmpXchgBytes, GooseLang/Lang.lean), at any address: a misaligned atomic is assumed not to tear (docs/KNOWN_LIMITATIONS.md). bool, string, pointers and the other non-plain values stay one opaque cell (docs/design/unsafe-memory.md, R1, R2 and R5).

• Plain types have gc's layout. A plain type (go.PlainLayout, Perennial/Golang/Defn/Plain.lean: integers and floats, arrays of at least one plain element, non-empty structs of plain non-blank fields with no padding, and named types of these) has gc's size and field offsets, and at a positive address its element and field addresses are concrete (go.PlainSemantics): arrayIndexRef V i l = l + i·size and structFieldRef V f l = l + offset. Other addresses stay abstract. Every allocation, and every heap points-to, is at a positive address.

• Model assumptions (overflow). Where Go panics on an overflow that a real program cannot reach (it would run out of memory first), the model assumes the overflow does not happen, with assume (Golang/Defn/Assume.lean: an assume that fails loops forever, so the proofs cover the executions where it holds):

  • append's new length (sumAssumeNoOverflowSigned, Golang/Defn/Slice.lean). Known to be reachable, not yet fixed: with zero-size elements no memory bounds the length, and Go panics where the model assumes: x := make([]struct{}, 1<<62); x = append(x, x...) panics with "growslice: len out of range". A program with that bug verifies.

  Only a length that must exist in memory may be assumed away; a length Go computes and checks before allocating is reachable. Overflows that a program can reach are not assumed away. strings.Join is one: Go sums the elements' lengths and panics before allocating anything, so a few gigabytes of aliased elements (make([]string, 1<<30+1) with a long separator) reach the panic. Known, not yet fixed: Join is still a trusted model that omits that panic, and strings.wp_Join has no premise excluding it (a fix that translates the real Join is on branch join-translation; its model of strings.Builder.String must first be made stuck where Go's String aliases the builder's buffer). sync.WaitGroup's int32 counter is another (two Add(1 << 30) calls panic in Go): WaitGroup.Add is Goose's translation, and WaitGroup.wp_Add asks its caller to bound the new counter by 2^31. A caller whose counter is backed by one goroutine per unit discharges the bound with thread tokens (above): n tokens give n < threadBound GF, and the client assumes threadBound GF ≤ 2^31 at adequacy time (ProgramLogic/ThreadTokensTest.lean, docs/PERENNIAL_PROOF_REFERENCE.md "Thread tokens").

• Panics. A panic outcome is a value, PanicV p, that unwinds every evaluation frame but that of Catch e h k (GooseLang/Lang.lean); panic(p) steps to it, a function with defers runs its body under a Catch (Golang/Defn/Defer.lean), and recover() (Goose translates it only directly in a deferred function literal) reads and clears the panic. A postcondition receives panics too, a spec {{ P }} e {{ RET v; Q }} excludes them, and a goroutine must not panic (wp_fork: forkPost). The adequacy theorems (goose_adequacy and the grove/disk ones) require the main thread's postcondition φ to exclude panics (hφ : ∀ p, ¬ φ (PanicV p), a pure fact about φ) and conclude that no thread of the execution has an unrecovered panic (UnrecoveredPanic, GooseLang/BoundedLang.lean): no thread is PanicV p, and none is unwinding a panic through frames none of which is a Catch, so a verified program does not die of a panic within the step bound. Run-time panics of builtins (Panic "msg") are stuck. See docs/PERENNIAL_PROOF_REFERENCE.md, "Panics".

• Trusted package-variable initializers. A package variable listed in a goose config's trusted gets its initializer X.init (allocation included) from Perennial/TrustedCode. Accepted for now, to remove later: five such models are trusted although goose translates the real source, so the review-trusted rule R2 grades them REWORK; they were accepted (2026-10-19) to finish the standard library's init proofs, and later reviews and soundness work should translate them away: crypto/ed25519.cryptocustomrand and time.asynctimerchan (no-ops; the fix translates internal/godebug, trusting its runtime hooks setUpdate and setNewIncNonDefault, with internal/bisect and internal/godebugs), log.std (no-op; needs os.Stderr, so os's initialization), log's init (no-op; it writes log/internal.DefaultOutput, and no ownership of another package's variable reaches an init proof: a program-logic gap), and crypto/rand.Reader (stores a value of Go's dynamic type with a placeholder inside; needs crypto/internal/rand and drbg, whose init runs a FIPS self-test). The no-ops for errors.errorType (a reflection type descriptor), math.useFMA and math/big.hasADX (CPU features the runtime detects) model irreducible behaviour. Each model's docstring says why it is faithful.

• sync.Pool. Get and Put are trusted (TrustedCode/sync.lean): the real ones rely on runtime pinning to a P, pointer arithmetic and eface layout reinterpretation (Perennial/Code/sync.toml has the goose run). They keep Go's Put(nil) and New handling and replace the per-P pools by the Go model goose/model/pool, a lock-protected multiset in the pool's field local, where Put may drop its value and Get may ignore the pool. That is more nondeterministic than gc's pools, victim cache and GC clearing. As with the channel and string models, the model's translation is part of go.Semantics (pool_sem).

• Method sets. Whether a type implements an interface (go.typeSetContains, used by type assertions and conversions) is decided by methodSet, an uninterpreted function of the semantics constrained by go.MethodSetIs t ms facts (Golang/Defn/MethodSet.lean): "the method set of t is exactly ms". goose emits them, for each named type T of a translated package, for T and *T in T.TypeAssumptions (method_set, ptr_method_set), from the Go type checker (go/types.NewMethodSet: value and pointer receivers, methods promoted through embedded fields with Go's depth and ambiguity rules, methods that are not translated, the same at every instantiation of a generic type); the semantics (InterfaceSemantics.method_set_no_methods) gives the empty method sets of the types that have no methods in Go (go.NoMethods). A method set is a property of a type's declaration that the type checker fixes, like its underlying type, which goose also emits: computing promotion in Lean would duplicate the type checker's rules, with nothing to check it against. A method is named by its Go id: an unexported method's name qualified by its package path ("context.cancel"), in method sets and in interface types (go.MethodElem) alike, since in Go an unexported method of one package never implements an interface of another. goose writes an interface type as all its methods (go/types' method set of the interface, embedded interfaces included), so that typeSetContains needs no recursion through embedded named interfaces; embedded constraint elements (unions, comparable) stay as type terms. A type a signature mentions that the translation cannot name (a named type of a package it does not import, an alias it does not translate) is written as what it denotes (go.Named "<path>.<Name>" args, the aliased type), so that an interface type has the same term, up to unfolding descriptors and aliases, in every package that writes it: Go's type identity, which = on go.GoType must agree with wherever interface types are compared (in signatures, as element types). Nothing is claimed beyond what is known: a method whose signature has a type goose does not support is an entry without a signature ((id, none): it exists), and the method set of any other type (a struct type literal with embedded fields, a type declared in a function, a type of an untranslated package) is unconstrained. Two limits of the model's type identity (= on go.GoType) apply here as to type assertions: struct tags are not part of go.StructType, and the unexported field names of struct type literals are not qualified by package. goose loads code with the build tag goose: a method declared only in files excluded by it (or included only by it) would make the emitted method set differ from the real build's. go_type_set (Golang/Theory/TypeSet.lean) decides typeSetContains goals.

• Generated code comes from goose. The translator in goose/ emits Perennial/Code/** and Perennial/GeneratedProof/**; regenerate with etc/update-goose-new.py rather than editing them by hand.

Layering (bottom up)

Directory	Contents
Perennial/Std	general libraries (gmap, words, lists, bytes)
Perennial/Algebra	cameras and ghost-state algebra
Perennial/GooseLang	GooseLang: semantics, lifting, bounded-step layer, receipts
Perennial/GooseLang/Ext	GooseLang extensions (new primitives): grove
Perennial/Golang/Defn	the Go model
Perennial/Golang/Theory	its program logic and spec lemmas
Perennial/Ghost	ghost-state libraries
Perennial/TrustedCode	trusted (hand-written) models of Go code
Perennial/Code	GooseLang code (generated by goose)
Perennial/GeneratedProof	generated proof boilerplate (generated by proofgen)
Perennial/Spec	the specs of the proved Go functions, one per file
Perennial/Proof	their proofs, one per file, linked in <pkg>/Link.lean

Status

Run etc/lean-ci.sh + etc/lean-audit.py for the build and soundness audit (sorry roots, axioms and opaques). etc/trusted-delta.py [commit | A..B] prints what a change adds to the trusted base (semantics, goose, trusted models, trust lists, assumes); the review-trusted skill (.agents/skills/review-trusted/) reviews it.

Conventions

• Follow the naming of the surrounding code (wp_load, isMutex, ownSlice). Quote names that are not legal Lean identifiers with «» (e.g. «unsafe», «_»).
• Sealing: def fooDef, @[irreducible] def foo := fooDef, theorem foo_unseal : foo = fooDef. To make an existing definition opaque, use attribute [irreducible] foo.
• GooseLang code notation (Perennial/GooseLang/Notation.lean): λ: "x", e, let: "x" := e1 in e2, e1 ;; e2, if: c then a else b, rec: "f" "x" := e, Go operators e1 +⟨t⟩ e2 etc. Method calls are rcvr @!! T @!! m.
• Everything lives in namespace Perennial.
• Every file is a module of Lean's module system: module, then its public imports, then @[expose] public section, so that all declarations are public with their bodies exposed.
• An unfinished proof is sorry, with a comment saying what is missing if it is not obvious. Do not add new axioms without discussing it first.
• Notation: #x is intoVal x; m !! k, <[k := v]> m, {[k := v]} work on both gmap and List (on lists they are l[i]? and l.set i v); the set-valued domain of a map is domSet m; go!"abc" is a GoString literal; l +ₗ i is location offset.
• Equality on GooseLang syntax and go.GoType is decided classically (noncomputable instance).
• An extension (GooseExt) has a name (by convention the path of the Go package it implements). Its operations are named by strings, ExternalOp ext op e (the extension's name and the operation's; an extension's step is defined on the operation's name), and its opaque values by its name and their encoding (ExtCode, extVal E v), so that neither the syntax nor goose depends on the program's list of extensions: the trusted model of a Go function implemented with an extension is ExternalOp E.name "Op" ..., with no assumption, and ElemExt E/HasExt E (proofs about E) are propositions, proved by computation when a program is closed off. Goose knows nothing of extensions.
• An extension (GooseExt) requires Pos.Countable of its Val, and Loc, GoSlice, val, Expr, GoFunc, GoInterface, go.GoType, ... are Pos.Countable (Perennial/GooseLang/Countable.lean, via an injection into GenTree), so ghost state can store values containing code.
• Check a file with lake build Perennial.Path.To.Module (from the repo root).
• The proof automation is compiled to native code: lakefile.toml declares a second library, PerennialMeta, with precompileModules, listing the modules that define tactics, elaborators, notation or simprocs and everything they import (about 150 modules, rooted at the generated PerennialMeta.lean). After adding such a module, or changing the imports of one, run etc/meta-lib.py and commit the result; etc/lean-ci.sh and etc/land.sh prepare fail until the list is up to date. Editing one of these modules relinks the library and rebuilds everything that loads it. The first build also compiles iris, batteries and Qq to native code (once).