This is the first step towards supporting reasoning about distributed systems: we add a type global_state to the language interface, which is threaded through everywhere together with the (per-machine) state; and we add a global_state_interp as state interpretation for this new state. This is separate from state_interp because the latter will be per-machine in the adequacy proof, while global_state is, well, global.

goose_lang for now picks global_state := () and global_state_interp g := True. Later, this will be extensible via FFI in the same manner as state. Independently of that I will work on adding a notion of "executing a distributed system" and a corresponding adequacy theorem, but that should hopefully not incur further breakage elsewhere in Perennial.

@upamanyus @krawthekrow if you have anything not in ShouldBuild, it might be broken more or less horribly by this... @jtassarotti please check what I did in jrnl_ffi and more generally around the refinement and twophase stuff; I got it to build but I am not sure if my choice of definitions is always right. In particular in jrnl_ffi.v I sometimes destruct g to exploit that global_state is () and thus cannot possibly have changed.

This is an incomparable definition; it's weaker in that allocating a crash invariant now requires proving persistently(Q -* P) now instead of later, but it's stronger in that a crash invariant now implies persistently(Q -* P) now.

Note that if the guarantee P is timeless the later in the definition doesn't matter.

A wrong instance involving option unit was found otherwise at intros ?%elem_of_singleton. It seems the SemiSet (in stdpp?) modes are not set correctly, as this declaration is necessary for an unambiguous typeclass resolution in the proof script below. I'd be happy if you could merge this fix here and later submit it to upstream so as to not delay https://github.com/coq/coq/pull/10858 any further. The fix should be backwards compatible of course.

Hi, this PR adapts to Coq PR coq/coq#13512 which makes the naming in the presence of the % introduction pattern compatible with name mangling. As a result, an H0 is now named H in perennial's file src/goose_lang/lib/struct/struct.v.

We fix the corresponding proof in a backward-compatible by not letting Coq generate the name. If you agree with the fix, it can be merged as soon as now.

Could you please update the submodules to stdpp@607ee2b1 and iris@5070f7f5 ? I've found a slowdown in perennial due to the change in stdpp for coq/coq#13969, which should be fixed now.

This is the Perennial side of https://github.com/tchajed/goose/pull/28. I re-goosed most things, except for perennial-examples which is not in a clean state currently (something related to async).

In typing.v there are some predicates that seem to be used only in the logrel; originally I meant ptrT to be consistent with structRefT but that imposes some new proof obligations in logical_reln_fund so instead of made ptrT return false for all of those... @jtassarotti is that okay?

Due do coq/coq#14392, only heads of applications should not be evars for ! to match a term during typeclass resolution. This makes the iris automation more powerful, resulting in a breakage in the script.

Before the mentioned Coq PR, "rewrite foo in H *" with ssreflect rewrite and a setoid equality would leave the goal with H reverted.

Instead we manually revert H and don't use "in".

Added a tactic wp_pure1_credit "HcredName" that takes a single pure step and introduces a hypothesis with a later credit with the name "HcredName".

I minimal changes while enabling credit generation for pure steps. So, for instance, if we want later credit generation in the wp_load lemma in the future, we'll need to expose later credit generation in several additional wp_* lemmas in the various lifting.v files.

Adds a little script and CI job to re-run Goose and check that git diff remains clean.

For now, Goose and the Go code repos are pinned to a particular commit each, but we could pin them to a branch as well.

I confirmed that before https://github.com/mit-pdos/perennial/commit/06834cebd125ceef376e547e471f80f770700f87, this indeed failed.

Ralf wrote a comment explaining the explicit scope annotations on Mattermost and I thought it would make for good documentation (we might use this file in Aneris).

The lemma wptp_recv_strong_normal_adequacy quantifies over an argument ns. But, if ns is not the empty list the first assumption is false and the lemma is pretty vacuous.

This PR changes the lemma by, essentially, inlining ns = []. This simplifies the statement, its proof, and the places where the lemma is used.

I've wanted to improve compile times for a while. So far my attempts to do so have failed because I don't know exactly what is slow, other than program proofs.

The first problem is getting data: what's slow about compilation? We have per-file information, but we need some other measurement. Is it Ltac? If it's Ltac, is it something about the proof mode? Is it typeclass resolution?

Some things we can try:

• Figure out how much time per file goes into Ltac vs everything else.
• Attempt to get a whole-project Ltac profile.
• Look at an OCaml profile of Coq compiling the whole project.

If it's the proof mode, one piece of useful infrastructure would be a synthetic benchmark that tests performance as some scaling factor increases, like the number of hypotheses or size of terms in the environment. Jason's projects (like reification by parametricity) are extremely good about these, which let them both track performance and identify asymptotic inefficiencies.

On top of the new async_inode, which implements an inode whose specification includes in-memory buffering, we should develop a resource-based specification for individual offsets in the inode.

Resources

• A points-to fact for an offset in the inode. These are persistent because offsets don't change. We can think of the inode as being just a single block (the latest appended one), except that it persists all old versions; this makes the inode resemble the transaction system much more closely.
• A monotonic durable lower-bound that specifies which index is persisted.

Rules for manipulating these resources

First, a points-to fact together with a lower-bound above that index should be durable, in some sense, in that it can be reconstructed after a crash. This may involve explicitly lifting from one "epoch" number to another, so that we can really relate one crash state to the next without destroying any state.

Secondly, it should be true that if one offset is present after a crash all previous ones are as well. This seems to involve some post-crash resource that says which index we crashed to; even if it was non-deterministically chosen, it's fixed after the initial choice.

We should set this up to start understanding how to deal with these non-deterministic crashes, particularly building up the right proof principles. The best test case would be to prove the simplest write-ahead log on top of an asynchronous disk and expose a synchronous, transactional API that doesn't have buffered writes.

The model is fairly easy: each disk block has a list of buffered possible crash values. Reads observe the latest write, and on crash we non-deterministically pick a buffered write to be the new value. This also gives a natural starting point for the resource algebra, which is just a current value and a set of crash values, per address.

The various allocation methods (ref, ref_to, NewSlice, NewMap) sometimes get unfolded and then the nice typed theorems about them don't apply. We should make sure they use opaque representations which are values (in some cases they were incorrectly made expressions, which have to be simplified to substitute through them).

The slice library is rather large, which makes it painful to shadow and re-export everything with types.

I think perhaps a better design is to think of a slice as naming a set of locations, without owning pointers for those locations. Then, we can instantiate a predicate per location; this subsumes the current is_slice_small and updates_slice, and similar notions. Subslicing just changes the set of locations. If this turns out to be difficult or not useful, we can revert to essentially the untyped slice library but ported to have types.

This involves doing the following:

• [ ] try out a new is_slice predicate that does not consume space but can be combined with a predicate per location
• [ ] implement the current API using the new predicate
• [ ] port all users of the untyped library to the typed version
• [ ] rename is_slice_small to is_slice and is_slice to is_slice_append
• [ ] use slice_cap separately where possible