Implement an asynchronous disk FFI and corresponding resources

[tchajed]

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.