Develop an asynchronous inode resource to reason about buffered state

[tchajed]

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.