Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Require Import POCS.

Require Import TwoDiskAPI.
Require Import Common.OneDiskAPI.

ReplicatedDisk provides a single-disk API on top of two disks, handling disk failures with replication.

Your job will be to implement the core of the recovery procedure for the replicated disk, and prove that the entire implementation is correct using your recovery procedure. This lab is split into several parts. Unlike in previous labs, the exercises do not proceed in order in the file; you'll first write specifications and admit the correctness proof, and then you'll come back and finish the proof.

Module ReplicatedDisk (td : TwoDiskAPI) <: OneDiskAPI.

  (* EXERCISE (4a): implement read *)
  Definition read (a:addr) : proc block :=
    Ret block0.

  Definition write (a:addr) (b:block) : proc unit :=
    _ <- td.write d0 a b;
    _ <- td.write d1 a b;
    Ret tt.

  Definition size : proc nat :=
    msz <- td.size d0;
    match msz with
    | Working sz => Ret sz
    | Failed =>
      msz <- td.size d1;
      match msz with
      | Working sz => Ret sz
      | Failed => Ret 0
      end
    end.

sizeInit computes the size during initialization; it may return None if the sizes of the underlying disks differ.

  Definition sizeInit : proc (option nat) :=
    sz1 <- td.size d0;
    sz2 <- td.size d1;
    match sz1 with
    | Working sz1 =>
      match sz2 with
      | Working sz2 =>
        if sz1 == sz2 then Ret (Some sz1) else Ret None
      | Failed => Ret (Some sz1)
      end
    | Failed =>
      match sz2 with
      | Working sz2 => Ret (Some sz2)
      | Failed => Ret None
      end
    end.

  (* Recursively initialize block a and below. For simplicity, we make the disks
  match by setting every block to [block0]. *)
  Fixpoint init_at (a:nat) : proc unit :=
    match a with
    | 0 => Ret tt
    | S a =>
      _ <- td.write d0 a block0;
      _ <- td.write d1 a block0;
      init_at a
    end.

  (* Initialize every disk block *)
  Definition init' : proc InitResult :=
    size <- sizeInit;
    match size with
    | Some sz =>
      _ <- init_at sz;
      Ret Initialized
    | None =>
      Ret InitFailed
    end.

  Definition init := then_init td.init init'.

Helper theorems and tactics for proofs.

  Theorem exists_tuple2 : forall A B (P: A * B -> Prop),
      (exists a b, P (a, b)) ->
      (exists p, P p).forall (A B : Type) (P : A * B -> Prop),
(exists (a : A) (b : B), P (a, b)) ->
exists p : A * B, P p
  Proof.forall (A B : Type) (P : A * B -> Prop),
(exists (a : A) (b : B), P (a, b)) ->
exists p : A * B, P p
    intros.A, B:Type
P:A * B -> Prop
H:exists (a : A) (b : B), P (a, b)
exists p : A * B, P p
    repeat deex; eauto.
  Qed.

  (* The [simplify] tactic performs a number of steps that should simplify and
  clean up your goals. *)
  Ltac simplify :=
    repeat match goal with
           | |- forall _, _ => intros
           | _ => deex
           | _ => destruct_tuple
           | [ u: unit |- _ ] => destruct u
           | |- _ /\ _ => split; [ solve [auto] | ]
           | |- _ /\ _ => split; [ | solve [auto] ]
           | |- exists (_: disk*_), _ => apply exists_tuple2
           | _ => progress simpl in *
           | _ => progress safe_intuition
           | _ => progress subst
           | _ => progress autorewrite with upd in *
           end.

  (* The [finish] tactic tries a number of techniques to solve the goal. *)
  Ltac finish :=
    repeat match goal with
           | _ => solve_false
           | _ => congruence
           | _ => solve [ intuition ]
           | _ =>
             (* if we can solve all the side conditions automatically, then it's
             safe to run descend and create existential variables *)
             descend; (intuition eauto);
             lazymatch goal with
             | |- proc_spec _ _ _ _ => idtac
             | _ => fail
             end
           end.

  Ltac step :=
    step_proc; simplify; finish.

Specifications and proofs about our implementation of the replicated disk API,

without considering our recovery.

These intermediate specifications separate reasoning about the

implementations from recovery behavior.

  Theorem both_disks_not_missing : forall (state: TwoDiskBaseAPI.State),
      two_disks_are state missing missing ->
      False.forall state : TwoDiskBaseAPI.State,
two_disks_are state missing missing -> False
  Proof.forall state : TwoDiskBaseAPI.State,
two_disks_are state missing missing -> False
    unfold two_disks_are.forall state : TwoDiskBaseAPI.State,
get_disk d0 state ?|= missing /\
get_disk d1 state ?|= missing -> False
    destruct state; unfold missing; simpl; intuition auto.
  Qed.

  Hint Resolve both_disks_not_missing : false.

  Theorem missing0_implies_any : forall (state: TwoDiskBaseAPI.State) P F,
      two_disks_are state missing F ->
      two_disks_are state P F.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
two_disks_are state missing F ->
two_disks_are state P F
  Proof.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
two_disks_are state missing F ->
two_disks_are state P F
    unfold two_disks_are.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
get_disk d0 state ?|= missing /\
get_disk d1 state ?|= F ->
get_disk d0 state ?|= P /\ get_disk d1 state ?|= F
    destruct state; unfold missing; simpl; intuition auto.
  Qed.

  Theorem missing1_implies_any : forall (state: TwoDiskBaseAPI.State) P F,
      two_disks_are state F missing ->
      two_disks_are state F P.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
two_disks_are state F missing ->
two_disks_are state F P
  Proof.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
two_disks_are state F missing ->
two_disks_are state F P
    unfold two_disks_are.forall (state : TwoDiskBaseAPI.State)
  (P F : disk -> Prop),
get_disk d0 state ?|= F /\
get_disk d1 state ?|= missing ->
get_disk d0 state ?|= F /\ get_disk d1 state ?|= P
    destruct state; unfold missing; simpl; intuition auto.
  Qed.

  Hint Resolve missing0_implies_any : core.
  Hint Resolve missing1_implies_any : core.

  (* EXERCISE (4a): prove this specification for read *)
  Theorem read_int_ok : forall a,
      proc_spec
        (fun d state =>
           {|
             pre := two_disks_are state (eq d) (eq d);
             post :=
               fun r state' =>
                 two_disks_are state' (eq d) (eq d) /\
                 diskGet d a =?= r;
             recovered :=
               fun _ state' =>
                 two_disks_are state' (eq d) (eq d);
           |})
        (read a)
        td.recover
        td.abstr.forall a : addr,
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : block)
             (state' : TwoDiskBaseAPI.State) =>
           two_disks_are state' (eq d) (eq d) /\
           diskGet d a =?= r;
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d) (eq d) |})
  (read a) td.recover td.abstr
  Proof.forall a : addr,
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : block)
             (state' : TwoDiskBaseAPI.State) =>
           two_disks_are state' (eq d) (eq d) /\
           diskGet d a =?= r;
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d) (eq d) |})
  (read a) td.recover td.abstr
    unfold read.forall a : addr,
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : block)
             (state' : TwoDiskBaseAPI.State) =>
           two_disks_are state' (eq d) (eq d) /\
           diskGet d a =?= r;
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d) (eq d) |})
  (Ret block0) td.recover td.abstr

    (* Hint: use step instead of step_proc to take advantage of the new
    automation in this lab. *)

    step.a:addr
a0:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq a0) (eq a0)
Lexec:Marker "post" (Ret block0)
diskGet a0 a =?= block0
  Admitted.

  Hint Resolve read_int_ok : core.

  (* EXERCISE (4a): complete and prove this specification for write *)
  Theorem write_int_ok : forall a b,
      proc_spec
        (fun d state =>
           {|
             pre := two_disks_are state (eq d) (eq d);
             post :=
               fun r state' =>
                 r = tt /\
                 two_disks_are state' (eq (diskUpd d a b)) (eq (diskUpd d a b));
             recovered :=
               fun _ state' =>
                 (* EXERCISE (4a): write the recovered condition for write. Note
                 that this is the two-disk API's recovery, not the replicated
                 disk's recovery, so it should cover all the crash cases for
                 write *)
             True;
           |})
        (write a b)
        td.recover
        td.abstr.forall (a : addr) (b : block),
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : unit)
             (state' : TwoDiskBaseAPI.State) =>
           r = tt /\
           two_disks_are state' (eq (diskUpd d a b))
             (eq (diskUpd d a b));
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (write a b) td.recover td.abstr
  Proof.forall (a : addr) (b : block),
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : unit)
             (state' : TwoDiskBaseAPI.State) =>
           r = tt /\
           two_disks_are state' (eq (diskUpd d a b))
             (eq (diskUpd d a b));
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (write a b) td.recover td.abstr
    unfold write.forall (a : addr) (b : block),
proc_spec
  (fun (d : disk) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d) (eq d);
   post := fun (r : unit)
             (state' : TwoDiskBaseAPI.State) =>
           r = tt /\
           two_disks_are state' (eq (diskUpd d a b))
             (eq (diskUpd d a b));
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (_ <- td.write d0 a b; _ <- td.write d1 a b; Ret tt)
  td.recover td.abstr

  Admitted.

  Hint Resolve write_int_ok : core.

  (* EXERCISE (4a): prove this specification for size *)
  Theorem size_int_ok :
    proc_spec
      (fun '(d_0, d_1) state =>
         {|
           pre := two_disks_are state (eq d_0) (eq d_1) /\
             diskSize d_0 = diskSize d_1;
           post :=
             fun r state' =>
               r = diskSize d_0 /\
               r = diskSize d_1 /\
               two_disks_are state' (eq d_0) (eq d_1);
           recovered :=
             fun _ state' =>
               two_disks_are state' (eq d_0) (eq d_1);
         |})
      (size)
      td.recover
      td.abstr.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          diskSize d_0 = diskSize d_1;
   post := fun (r : nat)
             (state' : TwoDiskBaseAPI.State) =>
           r = diskSize d_0 /\
           r = diskSize d_1 /\
           two_disks_are state' (eq d_0) (eq d_1);
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d_0) (eq d_1) |})
  size td.recover td.abstr
  Proof.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          diskSize d_0 = diskSize d_1;
   post := fun (r : nat)
             (state' : TwoDiskBaseAPI.State) =>
           r = diskSize d_0 /\
           r = diskSize d_1 /\
           two_disks_are state' (eq d_0) (eq d_1);
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d_0) (eq d_1) |})
  size td.recover td.abstr
    unfold size.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          diskSize d_0 = diskSize d_1;
   post := fun (r : nat)
             (state' : TwoDiskBaseAPI.State) =>
           r = diskSize d_0 /\
           r = diskSize d_1 /\
           two_disks_are state' (eq d_0) (eq d_1);
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                two_disks_are state' (eq d_0) (eq d_1) |})
  (msz <- td.size d0;
   match msz with
   | Working sz => Ret sz
   | Failed =>
       msz0 <- td.size d1;
       match msz0 with
       | Working sz => Ret sz
       | Failed => Ret 0
       end
   end) td.recover td.abstr

  Admitted.

  Hint Resolve size_int_ok : core.

  (* We provide a proof for [init]. *)

  Definition equal_after a (d_0 d_1: disk) :=
    diskSize d_0 = diskSize d_1 /\
    forall a', a <= a' -> diskGet d_0 a' = diskGet d_1 a'.

  Theorem le_eq_or_S_le : forall n m,
      n <= m ->
      n = m \/
      S n <= m /\ n <> m.forall n m : nat,
n <= m -> n = m \/ S n <= m /\ n <> m
  Proof.forall n m : nat,
n <= m -> n = m \/ S n <= m /\ n <> m
    intros.n, m:nat
H:n <= m
n = m \/ S n <= m /\ n <> m
    lia.
  Qed.

  Theorem equal_after_diskUpd : forall a d_0 d_1 b,
      equal_after (S a) d_0 d_1 ->
      equal_after a (diskUpd d_0 a b) (diskUpd d_1 a b).forall (a : nat) (d_0 d_1 : disk) (b : block),
equal_after (S a) d_0 d_1 ->
equal_after a (diskUpd d_0 a b) (diskUpd d_1 a b)
  Proof.forall (a : nat) (d_0 d_1 : disk) (b : block),
equal_after (S a) d_0 d_1 ->
equal_after a (diskUpd d_0 a b) (diskUpd d_1 a b)
    unfold equal_after; intuition.a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
diskSize (diskUpd d_0 a b) =
diskSize (diskUpd d_1 a b)
a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
a':nat
H1:a <= a'
diskGet (diskUpd d_0 a b) a' =
diskGet (diskUpd d_1 a b) a'
    -a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
diskSize (diskUpd d_0 a b) =
diskSize (diskUpd d_1 a b) autorewrite with upd; eauto.
    -a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
a':nat
H1:a <= a'
diskGet (diskUpd d_0 a b) a' =
diskGet (diskUpd d_1 a b) a' apply le_eq_or_S_le in H1; intuition subst.d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
diskGet (diskUpd d_0 a' b) a' =
diskGet (diskUpd d_1 a' b) a'
a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
a':nat
H1:S a <= a'
H2:a <> a'
diskGet (diskUpd d_0 a b) a' =
diskGet (diskUpd d_1 a b) a'
      {d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
diskGet (diskUpd d_0 a' b) a' =
diskGet (diskUpd d_1 a' b) a' destruct (lt_dec a' (diskSize d_0)); autorewrite with upd.d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
l:a' < diskSize d_0
Some b = Some b
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
n:~ a' < diskSize d_0
None = None
        +d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
l:a' < diskSize d_0
Some b = Some b assert (a' < diskSize d_1) by congruence; autorewrite with upd; auto.
        +d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
a':nat
H0:forall a'0 : nat,
S a' <= a'0 -> diskGet d_0 a'0 = diskGet d_1 a'0
n:~ a' < diskSize d_0
None = None assert (~a' < diskSize d_1) by congruence; autorewrite with upd; auto.
      }a:nat
d_0, d_1:disk
b:block
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
S a <= a' -> diskGet d_0 a' = diskGet d_1 a'
a':nat
H1:S a <= a'
H2:a <> a'
diskGet (diskUpd d_0 a b) a' =
diskGet (diskUpd d_1 a b) a'
      autorewrite with upd; eauto.
  Qed.

  Hint Resolve equal_after_diskUpd : core.

  Theorem init_at_ok : forall a,
      proc_spec
        (fun '(d_0, d_1) state =>
           {| pre :=
                two_disks_are state (eq d_0) (eq d_1) /\
                equal_after a d_0 d_1;
              post :=
                fun _ state' =>
                  exists d_0' d_1': disk,
                    two_disks_are state' (eq d_0') (eq d_1') /\
                    equal_after 0 d_0' d_1';
              recovered :=
                fun _ state' => True;
           |})
        (init_at a)
        td.recover
        td.abstr.forall a : nat,
proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after a d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr
  Proof.forall a : nat,
proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after a d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr
    induction a; simpl; intros.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after 0 d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret tt) td.recover td.abstr
a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after (S a) d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (_ <- td.write d0 a block0;
   _ <- td.write d1 a block0; init_at a) td.recover
  td.abstr
    -proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after 0 d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret tt) td.recover td.abstr step.
    -a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after (S a) d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (_ <- td.write d0 a block0;
   _ <- td.write d1 a block0; init_at a) td.recover
  td.abstr step.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
r:DiskResult unit
Lexec:Marker "after" (td.write d0 a block0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working _ =>
              two_disks_are state'
                (eq (diskUpd d_0 a block0)) (eq d_1)
          | Failed =>
              two_disks_are state' missing (eq d_1)
          end;
   post := fun (_ : unit)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (_ <- td.write d1 a block0; init_at a) td.recover
  td.abstr

      step.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
r:DiskResult unit
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:match r with
| Working _ =>
    two_disks_are state0
      (eq (diskUpd d_0 a block0)) 
      (eq d_1)
| Failed => two_disks_are state0 missing (eq d_1)
end
exists (a0 : disk) (b : disk -> Prop),
  (Marker "precondition" (td.write d1 a block0) ->
   two_disks_are state0 b (eq a0)) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   two_disks_are state' b (eq (diskUpd a0 a block0)) /\
   a < diskSize a0 \/ two_disks_are state' b (eq a0) ->
   Marker "recovered condition" (td.write d1 a block0) ->
   True) /\
  (forall r : DiskResult unit,
   Marker "after" (td.write d1 a block0) ->
   proc_spec
     (fun (_ : unit) (state' : TwoDiskBaseAPI.State)
      =>
      {|
      pre := match r with
             | Working _ =>
                 two_disks_are state' b
                   (eq (diskUpd a0 a block0))
             | Failed =>
                 two_disks_are state' b missing
             end;
      post := fun (_ : unit)
                (state'' : TwoDiskBaseAPI.State) =>
              exists d_0' d_1' : disk,
                two_disks_are state'' (eq d_0')
                  (eq d_1') /\ equal_after 0 d_0' d_1';
      recovered := fun (_ : unit)
                     (_ : TwoDiskBaseAPI.State) =>
                   True |}) (init_at a) td.recover
     td.abstr)
      destruct r; finish.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
v:unit
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 (eq (diskUpd d_0 a block0))
  (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working _ =>
              two_disks_are state'
                (eq (diskUpd d_0 a block0))
                (eq (diskUpd d_1 a block0))
          | Failed =>
              two_disks_are state'
                (eq (diskUpd d_0 a block0)) missing
          end;
   post := fun (_ : unit)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr
a:nat
IHa:proc_spec
  (fun '(d_0, d_1)
     (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after a d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' 
               (eq d_0') 
               (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) =>
                True |}) 
  (init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working _ =>
              two_disks_are state' missing
                (eq (diskUpd d_1 a block0))
          | Failed =>
              two_disks_are state' missing missing
          end;
   post := fun (_ : unit)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr
      +a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
v:unit
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 (eq (diskUpd d_0 a block0))
  (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working _ =>
              two_disks_are state'
                (eq (diskUpd d_0 a block0))
                (eq (diskUpd d_1 a block0))
          | Failed =>
              two_disks_are state'
                (eq (diskUpd d_0 a block0)) missing
          end;
   post := fun (_ : unit)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr step.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 (eq (diskUpd d_0 a block0))
  (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:match r with
| Working _ =>
    two_disks_are state1
      (eq (diskUpd d_0 a block0))
      (eq (diskUpd d_1 a block0))
| Failed =>
    two_disks_are state1
      (eq (diskUpd d_0 a block0)) missing
end
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
        destruct r; simplify; finish.
      +a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working _ =>
              two_disks_are state' missing
                (eq (diskUpd d_1 a block0))
          | Failed =>
              two_disks_are state' missing missing
          end;
   post := fun (_ : unit)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (init_at a) td.recover td.abstr step.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
r:DiskResult unit
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:match r with
| Working _ =>
    two_disks_are state1 missing
      (eq (diskUpd d_1 a block0))
| Failed => two_disks_are state1 missing missing
end
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
        destruct r; simplify.a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing
  (eq (diskUpd d_1 a block0))
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
a:nat
IHa:proc_spec
  (fun '(d_0, d_1)
     (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1) /\
          equal_after a d_0 d_1;
   post := fun (_ : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' 
               (eq d_0') 
               (eq d_1') /\
             equal_after 0 d_0' d_1';
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) =>
                True |}) 
  (init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing missing
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
        *a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing
  (eq (diskUpd d_1 a block0))
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True) exists (diskUpd d_0 a block0).a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing
  (eq (diskUpd d_1 a block0))
exists b : disk,
  (two_disks_are state1 (eq (diskUpd d_0 a block0))
     (eq b) /\ equal_after a (diskUpd d_0 a block0) b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
          exists (diskUpd d_1 a block0).a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing
  (eq (diskUpd d_1 a block0))
(two_disks_are state1 (eq (diskUpd d_0 a block0))
   (eq (diskUpd d_1 a block0)) /\
 equal_after a (diskUpd d_0 a block0)
   (diskUpd d_1 a block0)) /\
(unit ->
 forall state' : TwoDiskBaseAPI.State,
 (exists d_0' d_1' : disk,
    two_disks_are state' (eq d_0') (eq d_1') /\
    equal_after 0 d_0' d_1') ->
 exists d_0' d_1' : disk,
   two_disks_are state' (eq d_0') (eq d_1') /\
   equal_after 0 d_0' d_1') /\
(unit -> TwoDiskBaseAPI.State -> True -> True)
          finish.
        *a:nat
IHa:proc_spec
(fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
{|
pre := two_disks_are state (eq d_0) (eq d_1) /\ equal_after a d_0 d_1;
post := fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
exists d_0' d_1' : disk,
two_disks_are state' (eq d_0') (eq d_1') /\
equal_after 0 d_0' d_1';
recovered := fun (_ : unit) (_ : TwoDiskBaseAPI.State) => True |})
(init_at a) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
H0:equal_after (S a) d_0 d_1
Lexec:Marker "after" (td.write d0 a block0)
state0:TwoDiskBaseAPI.State
H1:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.write d1 a block0)
state1:TwoDiskBaseAPI.State
H2:two_disks_are state1 missing missing
exists a0 b : disk,
  (two_disks_are state1 (eq a0) (eq b) /\
   equal_after a a0 b) /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   (exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      equal_after 0 d_0' d_1') ->
   exists d_0' d_1' : disk,
     two_disks_are state' (eq d_0') (eq d_1') /\
     equal_after 0 d_0' d_1') /\
  (unit -> TwoDiskBaseAPI.State -> True -> True) finish.
  Qed.

  Hint Resolve init_at_ok : core.

  Theorem sizeInit_ok :
    proc_spec
      (fun '(d_0, d_1) state =>
         {| pre :=
              two_disks_are state (eq d_0) (eq d_1);
            post :=
              fun r state' =>
                exists d_0' d_1',
                  two_disks_are state' (eq d_0') (eq d_1') /\
                  match r with
                  | Some sz => diskSize d_0' = sz /\ diskSize d_1' = sz
                  | None => True
                  end;
            recovered :=
              fun _ state' => True;
         |})
      (sizeInit)
      td.recover
      td.abstr.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : option nat)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             match r with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  sizeInit td.recover td.abstr
  Proof.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : option nat)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             match r with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  sizeInit td.recover td.abstr
    unfold sizeInit.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : option nat)
             (state' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state' (eq d_0') (eq d_1') /\
             match r with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz1 <- td.size d0;
   sz2 <- td.size d1;
   match sz1 with
   | Working sz3 =>
       match sz2 with
       | Working sz4 =>
           if equal_dec sz3 sz4
           then Ret (Some sz3)
           else Ret None
       | Failed => Ret (Some sz3)
       end
   | Failed =>
       match sz2 with
       | Working sz3 => Ret (Some sz3)
       | Failed => Ret None
       end
   end) td.recover td.abstr
    step.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
r:DiskResult nat
Lexec:Marker "after" (td.size d0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working n =>
              two_disks_are state' (eq d_0) (eq d_1) /\
              n = diskSize d_0
          | Failed =>
              two_disks_are state' missing (eq d_1)
          end;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz2 <- td.size d1;
   match r with
   | Working sz1 =>
       match sz2 with
       | Working sz3 =>
           if equal_dec sz1 sz3
           then Ret (Some sz1)
           else Ret None
       | Failed => Ret (Some sz1)
       end
   | Failed =>
       match sz2 with
       | Working sz3 => Ret (Some sz3)
       | Failed => Ret None
       end
   end) td.recover td.abstr
    destruct r.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
v:nat
Lexec:Marker "after" (td.size d0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_0;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz2 <- td.size d1;
   match sz2 with
   | Working sz3 =>
       if equal_dec v sz3
       then Ret (Some v)
       else Ret None
   | Failed => Ret (Some v)
   end) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing (eq d_1);
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz2 <- td.size d1;
   match sz2 with
   | Working sz3 => Ret (Some sz3)
   | Failed => Ret None
   end) td.recover td.abstr
    -d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
v:nat
Lexec:Marker "after" (td.size d0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_0;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz2 <- td.size d1;
   match sz2 with
   | Working sz3 =>
       if equal_dec v sz3
       then Ret (Some v)
       else Ret None
   | Failed => Ret (Some v)
   end) td.recover td.abstr step.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
r:DiskResult nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working n =>
              two_disks_are state' (eq d_0) (eq d_1) /\
              n = diskSize d_1
          | Failed =>
              two_disks_are state' (eq d_0) missing
          end;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  match r with
  | Working sz2 =>
      if equal_dec (diskSize d_0) sz2
      then Ret (Some (diskSize d_0))
      else Ret None
  | Failed => Ret (Some (diskSize d_0))
  end td.recover td.abstr
      destruct r.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (if equal_dec (diskSize d_0) v
   then Ret (Some (diskSize d_0))
   else Ret None) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) missing;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some (diskSize d_0))) td.recover td.abstr
      +d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (if equal_dec (diskSize d_0) v
   then Ret (Some (diskSize d_0))
   else Ret None) td.recover td.abstr destruct (diskSize d_0 == v).d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
e:diskSize d_0 = v
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some (diskSize d_0))) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
n:diskSize d_0 <> v
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret None) td.recover td.abstr
        *d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
e:diskSize d_0 = v
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some (diskSize d_0))) td.recover td.abstr step.
        *d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
n:diskSize d_0 <> v
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret None) td.recover td.abstr step.
      +d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 (eq d_0) (eq d_1)
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' (eq d_0) missing;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some (diskSize d_0))) td.recover td.abstr step.
    -d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing (eq d_1);
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (sz2 <- td.size d1;
   match sz2 with
   | Working sz3 => Ret (Some sz3)
   | Failed => Ret None
   end) td.recover td.abstr step.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 missing (eq d_1)
r:DiskResult nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := match r with
          | Working n =>
              two_disks_are state' missing (eq d_1) /\
              n = diskSize d_1
          | Failed =>
              two_disks_are state' missing missing
          end;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  match r with
  | Working sz2 => Ret (Some sz2)
  | Failed => Ret None
  end td.recover td.abstr
      destruct r.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 missing (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some v)) td.recover td.abstr
d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing missing;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret None) td.recover td.abstr
      +d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 missing (eq d_1)
v:nat
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing (eq d_1) /\
          v = diskSize d_1;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret (Some v)) td.recover td.abstr step.
      +d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" (td.size d0)
state0:TwoDiskBaseAPI.State
H0:two_disks_are state0 missing (eq d_1)
Lexec0:Marker "after" (td.size d1)
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state' missing missing;
   post := fun (r' : option nat)
             (state'' : TwoDiskBaseAPI.State) =>
           exists d_0' d_1' : disk,
             two_disks_are state'' (eq d_0') (eq d_1') /\
             match r' with
             | Some sz =>
                 diskSize d_0' = sz /\
                 diskSize d_1' = sz
             | None => True
             end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret None) td.recover td.abstr step.
  Qed.

  Hint Resolve sizeInit_ok : core.


  Theorem equal_after_0_to_eq : forall d_0 d_1,
      equal_after 0 d_0 d_1 ->
      d_0 = d_1.forall d_0 d_1 : disk,
equal_after 0 d_0 d_1 -> d_0 = d_1
  Proof.forall d_0 d_1 : disk,
equal_after 0 d_0 d_1 -> d_0 = d_1
    unfold equal_after; intuition.d_0, d_1:disk
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
0 <= a' -> diskGet d_0 a' = diskGet d_1 a'
d_0 = d_1
    eapply disk_ext_eq; intros.d_0, d_1:disk
H:diskSize d_0 = diskSize d_1
H0:forall a' : nat,
0 <= a' -> diskGet d_0 a' = diskGet d_1 a'
a:addr
diskGet d_0 a = diskGet d_1 a
    eapply H0; lia.
  Qed.

  Theorem equal_after_size : forall d_0 d_1,
      diskSize d_0 = diskSize d_1 ->
      equal_after (diskSize d_0) d_0 d_1.forall d_0 d_1 : disk,
diskSize d_0 = diskSize d_1 ->
equal_after (diskSize d_0) d_0 d_1
  Proof.forall d_0 d_1 : disk,
diskSize d_0 = diskSize d_1 ->
equal_after (diskSize d_0) d_0 d_1
    unfold equal_after; intuition.d_0, d_1:disk
H:diskSize d_0 = diskSize d_1
a':nat
H0:diskSize d_0 <= a'
diskGet d_0 a' = diskGet d_1 a'
    assert (~a' < diskSize d_0) by lia.d_0, d_1:disk
H:diskSize d_0 = diskSize d_1
a':nat
H0:diskSize d_0 <= a'
H1:~ a' < diskSize d_0
diskGet d_0 a' = diskGet d_1 a'
    assert (~a' < diskSize d_1) by congruence.d_0, d_1:disk
H:diskSize d_0 = diskSize d_1
a':nat
H0:diskSize d_0 <= a'
H1:~ a' < diskSize d_0
H2:~ a' < diskSize d_1
diskGet d_0 a' = diskGet d_1 a'
    autorewrite with upd; eauto.
  Qed.

  Hint Resolve equal_after_size : core.
  Hint Resolve equal_after_0_to_eq : core.

  Theorem init'_ok :
    proc_spec
      (fun '(d_0, d_1) state =>
         {| pre :=
              two_disks_are state (eq d_0) (eq d_1);
            post :=
              fun r state' =>
                match r with
                | Initialized =>
                  exists d_0' d_1',
                  two_disks_are state' (eq d_0') (eq d_1') /\
                  d_0' = d_1'
                | InitFailed =>
                  True
                end;
            recovered :=
              fun _ state' => True;
         |})
      (init')
      td.recover
      td.abstr.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  init' td.recover td.abstr
  Proof.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  init' td.recover td.abstr
    unfold init'.proc_spec
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (size <- sizeInit;
   match size with
   | Some sz => _ <- init_at sz; Ret Initialized
   | None => Ret InitFailed
   end) td.recover td.abstr
    step.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
r:option nat
Lexec:Marker "after" sizeInit
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := exists d_0' d_1' : disk,
            two_disks_are state' (eq d_0') (eq d_1') /\
            match r with
            | Some sz =>
                diskSize d_0' = sz /\
                diskSize d_1' = sz
            | None => True
            end;
   post := fun (r' : InitResult)
             (state'' : TwoDiskBaseAPI.State) =>
           match r' with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state'' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  match r with
  | Some sz => _ <- init_at sz; Ret Initialized
  | None => Ret InitFailed
  end td.recover td.abstr
    destruct r; step.d_0, d_1:disk
state:TwoDiskBaseAPI.State
H:two_disks_are state (eq d_0) (eq d_1)
Lexec:Marker "after" sizeInit
state0:TwoDiskBaseAPI.State
d_0', d_1':disk
H0:two_disks_are state0 (eq d_0') (eq d_1')
H2:diskSize d_1' = diskSize d_0'
r:unit
Lexec0:Marker "after" (init_at (diskSize d_0'))
proc_spec
  (fun (_ : unit) (state' : TwoDiskBaseAPI.State) =>
   {|
   pre := exists d_0' d_1' : disk,
            two_disks_are state' (eq d_0') (eq d_1') /\
            equal_after 0 d_0' d_1';
   post := fun (r' : InitResult)
             (state'' : TwoDiskBaseAPI.State) =>
           match r' with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state'' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (Ret Initialized) td.recover td.abstr
    step.
  Qed.

  Hint Resolve init'_ok : core.

Recovery implementation.

We provide the general structure for recovery: essentially, it consists of

a loop around fixup that terminates after either fixing an out-of-sync

disk block or when a disk has failed.

  (* [fixup] returns a [RecStatus] to implement early termination in [recovery_at]. *)
  Inductive RecStatus :=
  (* continue working, nothing interesting has happened *)
  | Continue
  (* some address has been repaired (or the recovery has exhausted the
     addresses) - only one address can be out of sync and thus only it must be
     recovered. *)
  (* OR, one of the disks has failed, so don't bother continuing recovery since
     the invariant is now trivially satisfied *)
  | RepairDoneOrFailed.

  (* EXERCISE (4c): implement [fixup], which should perform recovery for a
  single address and indicate whether to continue or not. *)
  Definition fixup (a:addr) : proc RecStatus :=
    Ret Continue.

  (* recursively performs recovery at [a-1], [a-2], down to 0 *)
  Fixpoint recover_at (a:addr) : proc unit :=
    match a with
    | 0 => Ret tt
    | S n =>
      s <- fixup n;
      match s with
      | Continue => recover_at n
      | RepairDoneOrFailed => Ret tt
      end
    end.

  Definition Recover : proc unit :=
    sz <- size;
    _ <- recover_at sz;
    Ret tt.

Theorems and recovery proofs.

  Theorem if_lt_dec : forall A n m (a a':A),
      n < m ->
      (if lt_dec n m then a else a') = a.forall (A : Type) (n m : nat) (a a' : A),
n < m -> (if lt_dec n m then a else a') = a
  Proof.forall (A : Type) (n m : nat) (a a' : A),
n < m -> (if lt_dec n m then a else a') = a
    intros.A:Type
n, m:nat
a, a':A
H:n < m
(if lt_dec n m then a else a') = a
    destruct (lt_dec n m); auto.
  Qed.

  Theorem disks_eq_inbounds : forall (d: disk) a v v',
      a < diskSize d ->
      diskGet d a =?= v ->
      diskGet d a =?= v' ->
      v = v'.forall (d : disk) (a : nat) (v v' : block),
a < diskSize d ->
diskGet d a =?= v -> diskGet d a =?= v' -> v = v'
  Proof.forall (d : disk) (a : nat) (v v' : block),
a < diskSize d ->
diskGet d a =?= v -> diskGet d a =?= v' -> v = v'
    intros.d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
v = v'
    case_eq (diskGet d a); intros.d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
b:block
H2:diskGet d a = Some b
v = v'
d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
H2:diskGet d a = None
v = v'
    -d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
b:block
H2:diskGet d a = Some b
v = v' rewrite H2 in *.d:disk
a:nat
v, v':block
H:a < diskSize d
b:block
H0:Some b =?= v
H1:Some b =?= v'
H2:diskGet d a = Some b
v = v' simpl in *.d:disk
a:nat
v, v':block
H:a < diskSize d
b:block
H0:v = b
H1:v' = b
H2:diskGet d a = Some b
v = v' congruence.
    -d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
H2:diskGet d a = None
v = v' exfalso.d:disk
a:nat
v, v':block
H:a < diskSize d
H0:diskGet d a =?= v
H1:diskGet d a =?= v'
H2:diskGet d a = None
False
      eapply disk_inbounds_not_none; eauto.
  Qed.

  (* To make these specifications precise while also covering both the already
   * synced and diverged disks cases, we keep track of which input state we're
   * in from the input and use it to give an exact postcondition. *)
  Inductive DiskStatus :=
  | FullySynced
  | OutOfSync (a:addr) (b:block).

  Theorem diskUpd_maybe_same : forall (d:disk) a b,
      diskGet d a =?= b ->
      diskUpd d a b = d.forall (d : disk) (a : addr) (b : block),
diskGet d a =?= b -> diskUpd d a b = d
  Proof.forall (d : disk) (a : addr) (b : block),
diskGet d a =?= b -> diskUpd d a b = d
    intros.d:disk
a:addr
b:block
H:diskGet d a =?= b
diskUpd d a b = d
    destruct (diskGet d a) eqn:?; simpl in *; subst;
      autorewrite with upd;
      auto.
  Qed.

  Hint Rewrite diskUpd_maybe_same using (solve [ auto ]) : upd.
  Hint Resolve PeanoNat.Nat.lt_neq : core.
  Hint Resolve disks_eq_inbounds : core.


  (* EXERCISE (4c): write and admit a specification for [fixup]. *)
  Theorem fixup_ok : forall a,
      proc_spec
        (fun '(d, s) state =>
           {|
             pre :=
               a < diskSize d /\
               match s with
               | FullySynced => True
               | OutOfSync a' b => True
               end;
             post :=
               fun r state' =>
                 match s with
                 | FullySynced => True
                 | OutOfSync a' b => True
                 end;
             recovered :=
               fun _ state' =>
                 match s with
                 | FullySynced => True
                 | OutOfSync a' b => True
                 end;
           |})
        (fixup a)
        td.recover
        td.abstr.forall a : nat,
proc_spec
  (fun '(d, s) (_ : TwoDiskBaseAPI.State) =>
   {|
   pre := a < diskSize d /\
          match s with
          | FullySynced | _ => True
          end;
   post := fun (_ : RecStatus)
             (_ : TwoDiskBaseAPI.State) =>
           match s with
           | FullySynced | _ => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) =>
                match s with
                | FullySynced | _ => True
                end |}) (fixup a) td.recover td.abstr
  Proof.forall a : nat,
proc_spec
  (fun '(d, s) (_ : TwoDiskBaseAPI.State) =>
   {|
   pre := a < diskSize d /\
          match s with
          | FullySynced | _ => True
          end;
   post := fun (_ : RecStatus)
             (_ : TwoDiskBaseAPI.State) =>
           match s with
           | FullySynced | _ => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) =>
                match s with
                | FullySynced | _ => True
                end |}) (fixup a) td.recover td.abstr
    (* EXERCISE (4d): prove [fixup_ok] *)
  Admitted.

  Hint Resolve fixup_ok : core.

  (* Hint Resolve Lt.lt_n_Sm_le. *)

  (* EXERCISE (4c): specify and prove recover_at *)
  (* Hint: use [induction a] *)
  Theorem recover_at_ok : forall a,
      proc_spec
        (fun (_:unit) state =>
           {|
             pre := True;
             post :=
               fun r state' => True;
             recovered :=
               fun _ state' => True
           |})
        (recover_at a)
        td.recover
        td.abstr.forall a : addr,
proc_spec
  (fun (_ : unit) (_ : TwoDiskBaseAPI.State) =>
   {|
   pre := True;
   post := fun (_ : unit) (_ : TwoDiskBaseAPI.State)
           => True;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (recover_at a) td.recover td.abstr
  Proof.forall a : addr,
proc_spec
  (fun (_ : unit) (_ : TwoDiskBaseAPI.State) =>
   {|
   pre := True;
   post := fun (_ : unit) (_ : TwoDiskBaseAPI.State)
           => True;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (recover_at a) td.recover td.abstr
  Admitted.

  Hint Resolve recover_at_ok : core.

  (* EXERCISE (4b): write a spec for recovery *)
  Definition Recover_spec : Specification _ unit unit TwoDiskBaseAPI.State :=
    fun (_:unit) state =>
      {|
        pre := True;
        post := fun _ state' => True;
        recovered := fun _ state' => True;
      |}.

  (* EXERCISE (4c): prove recovery correct *)
  Theorem Recover_rok :
    proc_spec
      Recover_spec
      (Recover)
      td.recover
      td.abstr.proc_spec Recover_spec Recover td.recover td.abstr
  Proof.proc_spec Recover_spec Recover td.recover td.abstr
  Admitted.

  (* EXERCISE (4b): prove that your recovery specification is idempotent; that
  is, its recovered condition implies its precondition. *)
  Theorem Recover_spec_idempotent :
    idempotent Recover_spec.idempotent Recover_spec
  Proof.idempotent Recover_spec
    unfold idempotent.forall (a : unit) (state : TwoDiskBaseAPI.State),
pre (Recover_spec a state) ->
forall (v : unit) (state' : TwoDiskBaseAPI.State),
recovered (Recover_spec a state) v state' ->
exists a' : unit,
  pre (Recover_spec a' state') /\
  (forall (rv : unit) (state'' : TwoDiskBaseAPI.State),
   post (Recover_spec a' state') rv state'' ->
   post (Recover_spec a state) rv state'')
    intuition; simplify.state:TwoDiskBaseAPI.State
H:True
state':TwoDiskBaseAPI.State
H0:True
exists _ : unit,
  True /\
  (unit -> TwoDiskBaseAPI.State -> True -> True)
  Admitted.

  (* This proof combines your proof that recovery is correct and that its
  specification is idempotent to show recovery is correct even if re-run on
  every crash. *)
  Theorem Recover_ok :
    proc_loopspec
      Recover_spec
      (Recover)
      td.recover
      td.abstr.proc_loopspec Recover_spec Recover td.recover td.abstr
  Proof.proc_loopspec Recover_spec Recover td.recover td.abstr
    eapply idempotent_loopspec; simpl.proc_spec Recover_spec Recover td.recover td.abstr
idempotent Recover_spec
    -proc_spec Recover_spec Recover td.recover td.abstr apply Recover_rok.
    -idempotent Recover_spec apply Recover_spec_idempotent.
  Qed.

  Hint Resolve Recover_ok : core.

  Definition recover: proc unit :=
    _ <- td.recover;
    Recover.

  (* As the final step in giving the correctness of the replicated disk
  operations, we prove recovery specs that include the replicated disk Recover
  function. *)

  Definition rd_abstraction (state: TwoDiskBaseAPI.State) (d:OneDiskAPI.State) : Prop :=
    two_disks_are state (eq d) (eq d).

  Definition abstr : Abstraction OneDiskAPI.State :=
    abstraction_compose td.abstr {| abstraction := rd_abstraction; |}.

  Theorem init_ok : init_abstraction init recover abstr inited_any.init_abstraction init recover abstr inited_any
  Proof.init_abstraction init recover abstr inited_any
    intros.init_abstraction init recover abstr inited_any
    eapply then_init_compose; eauto.proc_spec
  (fun (_ : unit) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := inited_any state;
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists state'' : State,
                 abstraction
                   {| abstraction := rd_abstraction |}
                   state' state'' /\
                 inited_any state''
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  init' td.recover td.abstr
    eapply proc_spec_weaken; eauto.spec_impl
  (fun '(d_0, d_1) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := two_disks_are state (eq d_0) (eq d_1);
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists d_0' d_1' : disk,
                 two_disks_are state' (eq d_0')
                   (eq d_1') /\ d_0' = d_1'
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
  (fun (_ : unit) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := inited_any state;
   post := fun (r : InitResult)
             (state' : TwoDiskBaseAPI.State) =>
           match r with
           | Initialized =>
               exists state'' : State,
                 abstraction
                   {| abstraction := rd_abstraction |}
                   state' state'' /\
                 inited_any state''
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : TwoDiskBaseAPI.State) => True |})
    unfold spec_impl; intros.a:unit
state:TwoDiskBaseAPI.State
H:pre
  {|
  pre := inited_any state;
  post := fun (r : InitResult)
            (state' : TwoDiskBaseAPI.State) =>
          match r with
          | Initialized =>
              exists state'' : State,
                abstraction
                  {|
                  abstraction := rd_abstraction |}
                  state' state'' /\
                inited_any state''
          | InitFailed => True
          end;
  recovered := fun (_ : unit)
                 (_ : TwoDiskBaseAPI.State) =>
               True |}
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) state) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) state) v state' ->
   post
     {|
     pre := inited_any state;
     post := fun (r : InitResult)
               (state'0 : TwoDiskBaseAPI.State) =>
             match r with
             | Initialized =>
                 exists state'' : State,
                   abstraction
                     {|
                     abstraction := rd_abstraction |}
                     state'0 state'' /\
                   inited_any state''
             | InitFailed => True
             end;
     recovered := fun (_ : unit)
                    (_ : TwoDiskBaseAPI.State) => True |}
     v state') /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) state) rv state' ->
   recovered
     {|
     pre := inited_any state;
     post := fun (r : InitResult)
               (state'0 : TwoDiskBaseAPI.State) =>
             match r with
             | Initialized =>
                 exists state'' : State,
                   abstraction
                     {|
                     abstraction := rd_abstraction |}
                     state'0 state'' /\
                   inited_any state''
             | InitFailed => True
             end;
     recovered := fun (_ : unit)
                    (_ : TwoDiskBaseAPI.State) => True |}
     rv state')
    destruct state; simpl in *.a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (BothDisks d_0 d_1)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (BothDisks d_0 d_1)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (BothDisks d_0 d_1)) rv
     state' -> True)
a:unit
d_0:disk
H:inited_any (OnlyDisk0 d_0)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (OnlyDisk0 d_0)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk0 d_0)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk0 d_0)) rv
     state' -> True)
a:unit
d_1:disk
H:inited_any (OnlyDisk1 d_1)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (OnlyDisk1 d_1)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk1 d_1)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk1 d_1)) rv
     state' -> True)

    -a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (BothDisks d_0 d_1)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (BothDisks d_0 d_1)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (BothDisks d_0 d_1)) rv
     state' -> True) exists (d_0, d_1); simpl; intuition.a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
two_disks_are (BothDisks d_0 d_1) (eq d_0) (eq d_1)
a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      {a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
two_disks_are (BothDisks d_0 d_1) (eq d_0) (eq d_1) unfold two_disks_are; simpl; intuition. }a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      unfold rd_abstraction.a:unit
d_0, d_1:disk
H:inited_any (BothDisks d_0 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      two_disks_are state' (eq state'') (eq state'') /\
      inited_any state''
| InitFailed => True
end
      destruct v; simplify; finish.
    -a:unit
d_0:disk
H:inited_any (OnlyDisk0 d_0)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (OnlyDisk0 d_0)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk0 d_0)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk0 d_0)) rv
     state' -> True) exists (d_0, d_0); simplify; intuition.d_0:disk
H:inited_any (OnlyDisk0 d_0)
two_disks_are (OnlyDisk0 d_0) (eq d_0) (eq d_0)
d_0:disk
H:inited_any (OnlyDisk0 d_0)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      {d_0:disk
H:inited_any (OnlyDisk0 d_0)
two_disks_are (OnlyDisk0 d_0) (eq d_0) (eq d_0) unfold two_disks_are; simpl; intuition. }d_0:disk
H:inited_any (OnlyDisk0 d_0)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      unfold rd_abstraction.d_0:disk
H:inited_any (OnlyDisk0 d_0)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      two_disks_are state' (eq state'') (eq state'') /\
      inited_any state''
| InitFailed => True
end
      destruct v; simplify; finish.
    -a:unit
d_1:disk
H:inited_any (OnlyDisk1 d_1)
exists a' : disk * disk,
  pre
    ((let
      '(d_0, d_1) := a' in
       fun state : TwoDiskBaseAPI.State =>
       {|
       pre := two_disks_are state (eq d_0) (eq d_1);
       post := fun (r : InitResult)
                 (state' : TwoDiskBaseAPI.State) =>
               match r with
               | Initialized =>
                   exists d_0' d_1' : disk,
                     two_disks_are state' (eq d_0')
                       (eq d_1') /\ d_0' = d_1'
               | InitFailed => True
               end;
       recovered := fun (_ : unit)
                      (_ : TwoDiskBaseAPI.State) =>
                    True |}) (OnlyDisk1 d_1)) /\
  (forall (v : InitResult)
     (state' : TwoDiskBaseAPI.State),
   post
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk1 d_1)) v
     state' ->
   match v with
   | Initialized =>
       exists state'' : State,
         rd_abstraction state' state'' /\
         inited_any state''
   | InitFailed => True
   end) /\
  (forall (rv : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((let
       '(d_0, d_1) := a' in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := two_disks_are state (eq d_0) (eq d_1);
        post := fun (r : InitResult)
                  (state'0 : TwoDiskBaseAPI.State) =>
                match r with
                | Initialized =>
                    exists d_0' d_1' : disk,
                      two_disks_are state'0 (eq d_0')
                        (eq d_1') /\ d_0' = d_1'
                | InitFailed => True
                end;
        recovered := fun (_ : unit)
                       (_ : TwoDiskBaseAPI.State) =>
                     True |}) (OnlyDisk1 d_1)) rv
     state' -> True) exists (d_1, d_1); simplify; finish; intuition.d_1:disk
H:inited_any (OnlyDisk1 d_1)
two_disks_are (OnlyDisk1 d_1) (eq d_1) (eq d_1)
d_1:disk
H:inited_any (OnlyDisk1 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      {d_1:disk
H:inited_any (OnlyDisk1 d_1)
two_disks_are (OnlyDisk1 d_1) (eq d_1) (eq d_1) unfold two_disks_are; simpl; intuition. }d_1:disk
H:inited_any (OnlyDisk1 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      rd_abstraction state' state'' /\
      inited_any state''
| InitFailed => True
end
      unfold rd_abstraction.d_1:disk
H:inited_any (OnlyDisk1 d_1)
v:InitResult
state':TwoDiskBaseAPI.State
H0:match v with
| Initialized =>
    exists d_0' d_1' : disk,
      two_disks_are state' (eq d_0') (eq d_1') /\
      d_0' = d_1'
| InitFailed => True
end
match v with
| Initialized =>
    exists state'' : State,
      two_disks_are state' (eq state'') (eq state'') /\
      inited_any state''
| InitFailed => True
end
      destruct v; simplify; finish.
  Qed.

  (* EXERCISE (4b): prove that read, write, and size are correct when combined
  with your recovery (using your specification but admitted proof). *)

  Theorem read_ok : forall a, proc_spec (read_spec a) (read a) recover abstr.forall a : addr,
proc_spec (read_spec a) (read a) recover abstr
  Proof.forall a : addr,
proc_spec (read_spec a) (read a) recover abstr
    intros.a:addr
proc_spec (read_spec a) (read a) recover abstr
    apply spec_abstraction_compose; simpl.a:addr
proc_spec
  (fun '(_, state2) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := True /\ rd_abstraction state state2;
   post := fun (v : block)
             (state' : TwoDiskBaseAPI.State) =>
           exists state2' : State,
             (state2' = state2 /\
              diskGet state2 a =?= v) /\
             rd_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                exists state2' : State,
                  state2' = state2 /\
                  rd_abstraction state' state2' |})
  (read a) recover td.abstr
    eapply compose_recovery; eauto; simplify.a:addr
state2:State
state:TwoDiskBaseAPI.State
H:True
H0:rd_abstraction state state2
exists a'' : disk,
  two_disks_are state (eq a'') (eq a'') /\
  (forall (v : block) (state' : TwoDiskBaseAPI.State),
   two_disks_are state' (eq a'') (eq a'') /\
   diskGet a'' a =?= v ->
   exists state2' : State,
     (state2' = state2 /\ diskGet state2 a =?= v) /\
     rd_abstraction state' state2') /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   two_disks_are state' (eq a'') (eq a'') ->
   exists _ : unit,
     True /\
     (unit ->
      forall state'' : TwoDiskBaseAPI.State,
      True ->
      exists state2' : State,
        state2' = state2 /\
        rd_abstraction state'' state2'))
  Admitted.

  Theorem write_ok : forall a v, proc_spec (write_spec a v) (write a v) recover abstr.forall (a : addr) (v : block),
proc_spec (write_spec a v) (write a v) recover abstr
  Proof.forall (a : addr) (v : block),
proc_spec (write_spec a v) (write a v) recover abstr
    intros.a:addr
v:block
proc_spec (write_spec a v) (write a v) recover abstr
    apply spec_abstraction_compose; simpl.a:addr
v:block
proc_spec
  (fun '(_, state2) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := True /\ rd_abstraction state state2;
   post := fun (v0 : unit)
             (state' : TwoDiskBaseAPI.State) =>
           exists state2' : State,
             (v0 = tt /\ state2' = diskUpd state2 a v) /\
             rd_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                exists state2' : State,
                  (state2' = state2 \/
                   state2' = diskUpd state2 a v) /\
                  rd_abstraction state' state2' |})
  (write a v) recover td.abstr
    eapply compose_recovery; eauto; simplify.a:addr
v:block
state2:State
state:TwoDiskBaseAPI.State
H:True
H0:rd_abstraction state state2
exists a'' : disk,
  two_disks_are state (eq a'') (eq a'') /\
  (forall (v0 : unit) (state' : TwoDiskBaseAPI.State),
   v0 = tt /\
   two_disks_are state' (eq (diskUpd a'' a v))
     (eq (diskUpd a'' a v)) ->
   exists state2' : State,
     (v0 = tt /\ state2' = diskUpd state2 a v) /\
     rd_abstraction state' state2') /\
  (unit ->
   TwoDiskBaseAPI.State ->
   True ->
   exists _ : unit,
     True /\
     (unit ->
      forall state'' : TwoDiskBaseAPI.State,
      True ->
      exists state2' : State,
        (state2' = state2 \/
         state2' = diskUpd state2 a v) /\
        rd_abstraction state'' state2'))
  Admitted.

  Theorem size_ok : proc_spec size_spec size recover abstr.proc_spec size_spec size recover abstr
  Proof.proc_spec size_spec size recover abstr
    intros.proc_spec size_spec size recover abstr
    apply spec_abstraction_compose; simpl.proc_spec
  (fun '(_, state2) (state : TwoDiskBaseAPI.State) =>
   {|
   pre := True /\ rd_abstraction state state2;
   post := fun (v : nat)
             (state' : TwoDiskBaseAPI.State) =>
           exists state2' : State,
             (state2' = state2 /\ v = diskSize state2) /\
             rd_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : TwoDiskBaseAPI.State) =>
                exists state2' : State,
                  state2' = state2 /\
                  rd_abstraction state' state2' |})
  size recover td.abstr
    (* simplify is a bit too aggressive about existential variables here, so we
    provide some manual simplification here *)
    eapply compose_recovery; eauto.forall (a : unit * State)
  (state : TwoDiskBaseAPI.State),
pre
  ((let
    '(_, state2) := a in
     fun state0 : TwoDiskBaseAPI.State =>
     {|
     pre := True /\ rd_abstraction state0 state2;
     post := fun (v : nat)
               (state' : TwoDiskBaseAPI.State) =>
             exists state2' : State,
               (state2' = state2 /\
                v = diskSize state2) /\
               rd_abstraction state' state2';
     recovered := fun (_ : unit)
                    (state' : TwoDiskBaseAPI.State) =>
                  exists state2' : State,
                    state2' = state2 /\
                    rd_abstraction state' state2' |})
     state) ->
exists a'' : disk * disk,
  pre
    ((fun '(d_0, d_1) (state0 : TwoDiskBaseAPI.State)
      =>
      {|
      pre := two_disks_are state0 (eq d_0) (eq d_1) /\
             diskSize d_0 = diskSize d_1;
      post := fun (r : nat)
                (state' : TwoDiskBaseAPI.State) =>
              r = diskSize d_0 /\
              r = diskSize d_1 /\
              two_disks_are state' (eq d_0) (eq d_1);
      recovered := fun (_ : unit)
                     (state' : TwoDiskBaseAPI.State)
                   =>
                   two_disks_are state' (eq d_0)
                     (eq d_1) |}) a'' state) /\
  (forall (v : nat) (state' : TwoDiskBaseAPI.State),
   post
     ((fun '(d_0, d_1) (state0 : TwoDiskBaseAPI.State)
       =>
       {|
       pre := two_disks_are state0 (eq d_0) (eq d_1) /\
              diskSize d_0 = diskSize d_1;
       post := fun (r : nat)
                 (state'0 : TwoDiskBaseAPI.State) =>
               r = diskSize d_0 /\
               r = diskSize d_1 /\
               two_disks_are state'0 (eq d_0) (eq d_1);
       recovered := fun (_ : unit)
                      (state'0 : TwoDiskBaseAPI.State)
                    =>
                    two_disks_are state'0 (eq d_0)
                      (eq d_1) |}) a'' state) v state' ->
   post
     ((let
       '(_, state2) := a in
        fun state0 : TwoDiskBaseAPI.State =>
        {|
        pre := True /\ rd_abstraction state0 state2;
        post := fun (v0 : nat)
                  (state'0 : TwoDiskBaseAPI.State) =>
                exists state2' : State,
                  (state2' = state2 /\
                   v0 = diskSize state2) /\
                  rd_abstraction state'0 state2';
        recovered := fun (_ : unit)
                       (state'0 : TwoDiskBaseAPI.State)
                     =>
                     exists state2' : State,
                       state2' = state2 /\
                       rd_abstraction state'0 state2' |})
        state) v state') /\
  (forall (v : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     ((fun '(d_0, d_1) (state0 : TwoDiskBaseAPI.State)
       =>
       {|
       pre := two_disks_are state0 (eq d_0) (eq d_1) /\
              diskSize d_0 = diskSize d_1;
       post := fun (r : nat)
                 (state'0 : TwoDiskBaseAPI.State) =>
               r = diskSize d_0 /\
               r = diskSize d_1 /\
               two_disks_are state'0 (eq d_0) (eq d_1);
       recovered := fun (_ : unit)
                      (state'0 : TwoDiskBaseAPI.State)
                    =>
                    two_disks_are state'0 (eq d_0)
                      (eq d_1) |}) a'' state) v state' ->
   exists a' : unit,
     pre (Recover_spec a' state') /\
     (forall (v' : unit)
        (state'' : TwoDiskBaseAPI.State),
      post (Recover_spec a' state') v' state'' ->
      recovered
        ((let
          '(_, state2) := a in
           fun state0 : TwoDiskBaseAPI.State =>
           {|
           pre := True /\ rd_abstraction state0 state2;
           post := fun (v0 : nat)
                     (state'0 : TwoDiskBaseAPI.State)
                   =>
                   exists state2' : State,
                     (... /\ ...) /\
                     rd_abstraction state'0 state2';
           recovered := fun (_ : unit)
                          (state'0 : TwoDiskBaseAPI.State)
                        =>
                        exists state2' : State,
                          state2' = state2 /\
                          rd_abstraction state'0
                            state2' |}) state) v'
        state''))
    intros; apply exists_tuple2.a:(unit * State)%type
state:TwoDiskBaseAPI.State
H:pre
  ((let
    '(_, state2) := a in
     fun state : TwoDiskBaseAPI.State =>
     {|
     pre := True /\ rd_abstraction state state2;
     post := fun (v : nat)
               (state' : TwoDiskBaseAPI.State) =>
             exists state2' : State,
               (state2' = state2 /\
                v = diskSize state2) /\
               rd_abstraction state' state2';
     recovered := fun (_ : unit)
                    (state' : TwoDiskBaseAPI.State)
                  =>
                  exists 
                  state2' : State,
                    state2' = state2 /\
                    rd_abstraction state' state2' |})
     state)
exists a0 b : disk,
  pre
    {|
    pre := two_disks_are state (eq a0) (eq b) /\
           diskSize a0 = diskSize b;
    post := fun (r : nat)
              (state' : TwoDiskBaseAPI.State) =>
            r = diskSize a0 /\
            r = diskSize b /\
            two_disks_are state' (eq a0) (eq b);
    recovered := fun (_ : unit)
                   (state' : TwoDiskBaseAPI.State) =>
                 two_disks_are state' (eq a0) (eq b) |} /\
  (forall (v : nat) (state' : TwoDiskBaseAPI.State),
   post
     {|
     pre := two_disks_are state (eq a0) (eq b) /\
            diskSize a0 = diskSize b;
     post := fun (r : nat)
               (state'0 : TwoDiskBaseAPI.State) =>
             r = diskSize a0 /\
             r = diskSize b /\
             two_disks_are state'0 (eq a0) (eq b);
     recovered := fun (_ : unit)
                    (state'0 : TwoDiskBaseAPI.State)
                  =>
                  two_disks_are state'0 (eq a0) (eq b) |}
     v state' ->
   post
     ((let
       '(_, state2) := a in
        fun state : TwoDiskBaseAPI.State =>
        {|
        pre := True /\ rd_abstraction state state2;
        post := fun (v0 : nat)
                  (state'0 : TwoDiskBaseAPI.State) =>
                exists state2' : State,
                  (state2' = state2 /\
                   v0 = diskSize state2) /\
                  rd_abstraction state'0 state2';
        recovered := fun (_ : unit)
                       (state'0 : TwoDiskBaseAPI.State)
                     =>
                     exists state2' : State,
                       state2' = state2 /\
                       rd_abstraction state'0 state2' |})
        state) v state') /\
  (forall (v : unit) (state' : TwoDiskBaseAPI.State),
   recovered
     {|
     pre := two_disks_are state (eq a0) (eq b) /\
            diskSize a0 = diskSize b;
     post := fun (r : nat)
               (state'0 : TwoDiskBaseAPI.State) =>
             r = diskSize a0 /\
             r = diskSize b /\
             two_disks_are state'0 (eq a0) (eq b);
     recovered := fun (_ : unit)
                    (state'0 : TwoDiskBaseAPI.State)
                  =>
                  two_disks_are state'0 (eq a0) (eq b) |}
     v state' ->
   exists a' : unit,
     pre (Recover_spec a' state') /\
     (forall (v' : unit)
        (state'' : TwoDiskBaseAPI.State),
      post (Recover_spec a' state') v' state'' ->
      recovered
        ((let
          '(_, state2) := a in
           fun state : TwoDiskBaseAPI.State =>
           {|
           pre := True /\ rd_abstraction state state2;
           post := fun (v0 : nat)
                     (state'0 : TwoDiskBaseAPI.State)
                   =>
                   exists state2' : State,
                     (state2' = state2 /\
                      v0 = diskSize state2) /\
                     rd_abstraction state'0 state2';
           recovered := fun (_ : unit)
                          (state'0 : TwoDiskBaseAPI.State)
                        =>
                        exists state2' : State,
                          state2' = state2 /\
                          rd_abstraction state'0
                            state2' |}) state) v'
        state''))
    destruct a; simpl in *.u:unit
s:State
state:TwoDiskBaseAPI.State
H:True /\ rd_abstraction state s
exists a b : disk,
  (two_disks_are state (eq a) (eq b) /\
   diskSize a = diskSize b) /\
  (forall (v : nat) (state' : TwoDiskBaseAPI.State),
   v = diskSize a /\
   v = diskSize b /\
   two_disks_are state' (eq a) (eq b) ->
   exists state2' : State,
     (state2' = s /\ v = diskSize s) /\
     rd_abstraction state' state2') /\
  (unit ->
   forall state' : TwoDiskBaseAPI.State,
   two_disks_are state' (eq a) (eq b) ->
   exists _ : unit,
     True /\
     (unit ->
      forall state'' : TwoDiskBaseAPI.State,
      True ->
      exists state2' : State,
        state2' = s /\ rd_abstraction state'' state2'))
  Admitted.

  (* This theorem shows that Ret does not modify the abstract state exposed by
  the replicated disk; the interesting part is that if recovery runs, then the
  only effect should be the wipe relation (the trivial relation [no_wipe] in
  this case) *)
  (* EXERCISE (4b): prove this theorem using your recovery spec *)
  Theorem recover_wipe : rec_wipe recover abstr no_wipe.rec_wipe recover abstr no_wipe
  Proof.rec_wipe recover abstr no_wipe
    eapply rec_wipe_compose; eauto; simpl.forall (state0 : TwoDiskBaseAPI.State)
  (state0' : State) (state : TwoDiskBaseAPI.State),
rd_abstraction state0 state0' ->
no_wipe state0 state ->
exists _ : unit,
  True /\
  (forall state' : TwoDiskBaseAPI.State,
   unit ->
   True ->
   exists state2' : State,
     no_wipe state0' state2' /\
     rd_abstraction state' state2')
    autounfold; unfold rd_abstraction, Recover_spec; simplify.state0:TwoDiskBaseAPI.State
state0':State
H:two_disks_are state0 (eq state0') (eq state0')
exists _ : unit,
  True /\
  (forall state' : TwoDiskBaseAPI.State,
   unit ->
   True ->
   exists state2' : State,
     state2' = state0' /\
     two_disks_are state' (eq state2') (eq state2'))
  Admitted.

End ReplicatedDisk.