Lab 2 discussion &c
===================

lab 2
  write impl
    get bad block, size
    check for out-of-bounds; do nothing if so
    check for bad block; go to size-1 if so
  abstraction relation
    size differs by 1
    good in-bound blocks
    bad block is remapped, as long as it's not the last block
    do we need to describe out-of-bound blocks?
  init_ok
    prohibit zero-sized disk
    prohibit bad sector being out-of-bounds
    can carry along these facts in the abstraction relation
    as a result, don't need to worry about handling these cases
    need to construct initial abstract state using [exists]
    need a name for the remapped block
  read_ok
    no changes to the state, so proving abstraction is easy
    handle out-of-bound reads
    use abstraction relation to show we return the correct value
  lemmas proving abstraction after update
    useful pattern: factor out lemmas to keep the [write_ok] proof small
    what are the possible ways to update the code state, and
      how does the abstract state change as a result?
    1. write to a good sector that is not remapped: updates same sector
    2. write to the remapped sector: updates the bad sector
    3. write out-of-bounds: no change to code state since OOB writes are nop
      no change to the abstract state either, then
    don't need to consider writes to the bad sector: should never happen
  write_ok
    use lemmas
    comment out [Hint Resolve] to see where they are used
    [eexists]?
  size_ok

lab 2 extraction
  src/Lab2/RemappedServer.v
  src/Common/NbdServer.v

  remap-nbd/extract/RemappedServer.hs
    serverLoop at top

  remap-nbd/lib/BadBlockEnv/Ops.hs
    corresponds to src/Lab2/BadBlockImpl.v (which implements BadBlockAPI.v)

  ./bin/remap-nbd init
  ls -l disk.img
  ./bin/remap-nbd start &

  modprobe nbd
  nbd-client localhost /dev/nbd0

  dd if=/dev/urandom | dd of=/dev/nbd0 bs=4096 oflag=direct
    ## performance seems ok
  hexdump /dev/nbd0 | less
  hexdump disk.img | less

  mkfs -t ext4 /dev/nbd0
  mount /dev/nbd0 /mnt/x
  cd /mnt/x

  echo hello world > test.txt
  sync
  strings disk.img

  umount /mnt/x
  nbd-client -d /dev/nbd0

lab 3
  AtomicPairAPI.v
    state: two blocks
    get
    put
    inited_any

  recovered condition: put is atomic with respect to crashes!

  several ways to implement
    logging
    two copies

  logging requires recovery code
    apply log after crash
    slightly tricky to reason about
    go this route if you want more of a challenge

  two-copy plan needs no recovery

  recovered condition will show up in proof obligations at every [step_proc]