TwoDiskImpl.v

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 TwoDiskBaseAPI.


Module TwoDisk (b : TwoDiskBaseAPI) <: TwoDiskAPI.

  Definition init := b.init.
  Definition read := b.read.
  Definition write := b.write.
  Definition size := b.size.
  Definition recover:= b.recover.

  Definition abstr := b.abstr.

  Ltac inv_step :=
    match goal with
    | [ H: op_step _ _ _ _ |- _ ] =>
      inversion H; subst; clear H;
      repeat sigT_eq;
      safe_intuition
    end.

  Ltac inv_bg :=
    match goal with
    | [ H: bg_failure _ _ |- _ ] =>
      inversion H; subst; clear H
    end.

  Theorem maybe_holds_stable : forall state state' F0 F1,
    disk0 state ?|= F0 ->
    disk1 state ?|= F1 ->
    bg_failure state state' ->
    disk0 state' ?|= F0 /\
    disk1 state' ?|= F1.forall (state state' : State) (F0 F1 : disk -> Prop),
disk0 state ?|= F0 ->
disk1 state ?|= F1 ->
bg_failure state state' ->
disk0 state' ?|= F0 /\ disk1 state' ?|= F1
  Proof.forall (state state' : State) (F0 F1 : disk -> Prop),
disk0 state ?|= F0 ->
disk1 state ?|= F1 ->
bg_failure state state' ->
disk0 state' ?|= F0 /\ disk1 state' ?|= F1
    intros.state, state':State
F0, F1:disk -> Prop
H:disk0 state ?|= F0
H0:disk1 state ?|= F1
H1:bg_failure state state'
disk0 state' ?|= F0 /\ disk1 state' ?|= F1
    inv_bg; simpl in *; eauto.
  Qed.

  Ltac cleanup :=
    repeat match goal with
           | [ |- forall _, _ ] => intros
           | |- _ /\ _ => split; [ solve [ eauto || congruence ] | ]
           | |- _ /\ _ => split; [ | solve [ eauto || congruence ] ]
           | [ H: Working _ = Working _ |- _ ] => inversion H; subst; clear H
           | [ H: bg_failure _ _ |- _ ] =>
             eapply maybe_holds_stable in H;
             [ | solve [ eauto ] | solve [ eauto ] ]; destruct_ands
           | [ H: _ ?|= eq _, H': _ = Some _ |- _ ] =>
                    pose proof (holds_some_inv_eq _ H' H); clear H
           | [ H: ?A * ?B |- _ ] => destruct H
           | [ H: DiskResult _ |- _ ] => destruct H
           | _ => deex
           | _ => destruct_tuple
           | _ => progress unfold pre_step in *
           | _ => progress autounfold in *
           | _ => progress simpl in *
           | _ => progress subst
           | _ => progress safe_intuition
           | _ => solve [ eauto ]
           | _ => congruence
           | _ => inv_step
           | H: context[match ?expr with _ => _ end] |- _ =>
             destruct expr eqn:?; [ | solve [ repeat cleanup ] ]
           | H: context[match ?expr with _ => _ end] |- _ =>
             destruct expr eqn:?; [ solve [ repeat cleanup ] | ]
           end.

  Ltac prim :=
    intros;
    eapply proc_spec_weaken; [ eauto | unfold spec_impl ]; exists tt;
    intuition eauto; cleanup;
    intuition eauto; cleanup.

  Hint Resolve holds_in_some_eq : core.
  Hint Resolve holds_in_none_eq : core.
  Hint Resolve pred_missing : core.

  Hint Unfold combined_step : core.


  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
    eauto.
  Qed.

  Theorem read0_ok : forall a, proc_spec (read0_spec a) (read d0 a) recover abstr.forall a : addr,
proc_spec (read0_spec a) (read d0 a) recover abstr
  Proof.forall a : addr,
proc_spec (read0_spec a) (read d0 a) recover abstr
    unfold read0_spec.forall a : addr,
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state (eq d) F;
   post := fun (r : DiskResult block) (state' : State)
           =>
           match r with
           | Working v =>
               two_disks_are state' (eq d) F /\
               diskGet d a ?|= eq v
           | Failed => two_disks_are state' missing F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state' (eq d) F |})
  (read d0 a) recover abstr
    unfold two_disks_are.forall a : addr,
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= eq d /\
          get_disk d1 state ?|= F;
   post := fun (r : DiskResult block) (state' : State)
           =>
           match r with
           | Working v =>
               (get_disk d0 state' ?|= eq d /\
                get_disk d1 state' ?|= F) /\
               diskGet d a ?|= eq v
           | Failed =>
               get_disk d0 state' ?|= missing /\
               get_disk d1 state' ?|= F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                get_disk d0 state' ?|= eq d /\
                get_disk d1 state' ?|= F |})
  (read d0 a) recover abstr
    prim.
  Qed.

  Theorem read1_ok : forall a, proc_spec (read1_spec a) (read d1 a) recover abstr.forall a : addr,
proc_spec (read1_spec a) (read d1 a) recover abstr
  Proof.forall a : addr,
proc_spec (read1_spec a) (read d1 a) recover abstr
    unfold read1_spec.forall a : addr,
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state F (eq d);
   post := fun (r : DiskResult block) (state' : State)
           =>
           match r with
           | Working v =>
               two_disks_are state' F (eq d) /\
               diskGet d a ?|= eq v
           | Failed => two_disks_are state' F missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state' F (eq d) |})
  (read d1 a) recover abstr
    unfold two_disks_are.forall a : addr,
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= F /\
          get_disk d1 state ?|= eq d;
   post := fun (r : DiskResult block) (state' : State)
           =>
           match r with
           | Working v =>
               (get_disk d0 state' ?|= F /\
                get_disk d1 state' ?|= eq d) /\
               diskGet d a ?|= eq v
           | Failed =>
               get_disk d0 state' ?|= F /\
               get_disk d1 state' ?|= missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                get_disk d0 state' ?|= F /\
                get_disk d1 state' ?|= eq d |})
  (read d1 a) recover abstr
    prim.
  Qed.

  Ltac destruct_all :=
    repeat match goal with
           | _ => solve [ auto ]
           | [ i: diskId |- _ ] => destruct i
           | [ |- context[match ?s with
                         | BothDisks _ _ => _
                         | OnlyDisk0 _ => _
                         | OnlyDisk1 _ => _
                         end] ] => destruct s
           | _ => simpl in *
           end.

  Theorem write0_ok : forall a v, proc_spec (write0_spec a v) (write d0 a v) recover abstr.forall (a : addr) (v : block),
proc_spec (write0_spec a v) (write d0 a v) recover
  abstr
  Proof.forall (a : addr) (v : block),
proc_spec (write0_spec a v) (write d0 a v) recover
  abstr
    unfold write0_spec.forall (a : addr) (v : block),
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state (eq d) F;
   post := fun (r : DiskResult unit) (state' : State)
           =>
           match r with
           | Working _ =>
               two_disks_are state'
                 (eq (diskUpd d a v)) F
           | Failed => two_disks_are state' missing F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state'
                  (eq (diskUpd d a v)) F /\
                a < diskSize d \/
                two_disks_are state' (eq d) F |})
  (write d0 a v) recover abstr
    unfold two_disks_are.forall (a : addr) (v : block),
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= eq d /\
          get_disk d1 state ?|= F;
   post := fun (r : DiskResult unit) (state' : State)
           =>
           match r with
           | Working _ =>
               get_disk d0 state'
               ?|= eq (diskUpd d a v) /\
               get_disk d1 state' ?|= F
           | Failed =>
               get_disk d0 state' ?|= missing /\
               get_disk d1 state' ?|= F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                (get_disk d0 state'
                 ?|= eq (diskUpd d a v) /\
                 get_disk d1 state' ?|= F) /\
                a < diskSize d \/
                get_disk d0 state' ?|= eq d /\
                get_disk d1 state' ?|= F |})
  (write d0 a v) recover abstr
    prim; try solve [ destruct_all ].a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= eq (diskUpd d0 a v) /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= P
    destruct (le_dec (S a) (diskSize d0)).a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
l:S a <= diskSize d0
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= eq (diskUpd d0 a v) /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= P
a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= eq (diskUpd d0 a v) /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= P
    *a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
l:S a <= diskSize d0
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= eq (diskUpd d0 a v) /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= P destruct_all.
    *a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= eq (diskUpd d0 a v) /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks (diskUpd d0 a v) d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 (diskUpd d0 a v)
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks (diskUpd d0 a v) d_1
  end ?|= P rewrite diskUpd_oob_noop by lia.a:addr
v:block
P:disk -> Prop
state:State
d0:disk
H:disk0 state ?|= eq d0
H2:disk1 state ?|= P
state'0:State
Heqo:disk0 state'0 = Some d0
H3:disk1 state'0 ?|= P
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 d0
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks d0 d_1
   end ?|= eq d0 /\
 disk1
   match state'0 with
   | OnlyDisk0 _ => OnlyDisk0 d0
   | BothDisks _ d_1 | OnlyDisk1 d_1 =>
       BothDisks d0 d_1
   end ?|= P) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 d0
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks d0 d_1
  end ?|= eq d0 /\
disk1
  match state'0 with
  | OnlyDisk0 _ => OnlyDisk0 d0
  | BothDisks _ d_1 | OnlyDisk1 d_1 =>
      BothDisks d0 d_1
  end ?|= P
      destruct_all.
  Qed.

  Theorem write1_ok : forall a v, proc_spec (write1_spec a v) (write d1 a v) recover abstr.forall (a : addr) (v : block),
proc_spec (write1_spec a v) (write d1 a v) recover
  abstr
  Proof.forall (a : addr) (v : block),
proc_spec (write1_spec a v) (write d1 a v) recover
  abstr
    unfold write1_spec.forall (a : addr) (v : block),
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state F (eq d);
   post := fun (r : DiskResult unit) (state' : State)
           =>
           match r with
           | Working _ =>
               two_disks_are state' F
                 (eq (diskUpd d a v))
           | Failed => two_disks_are state' F missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state' F
                  (eq (diskUpd d a v)) /\
                a < diskSize d \/
                two_disks_are state' F (eq d) |})
  (write d1 a v) recover abstr
    unfold two_disks_are.forall (a : addr) (v : block),
proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= F /\
          get_disk d1 state ?|= eq d;
   post := fun (r : DiskResult unit) (state' : State)
           =>
           match r with
           | Working _ =>
               get_disk d0 state' ?|= F /\
               get_disk d1 state'
               ?|= eq (diskUpd d a v)
           | Failed =>
               get_disk d0 state' ?|= F /\
               get_disk d1 state' ?|= missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                (get_disk d0 state' ?|= F /\
                 get_disk d1 state'
                 ?|= eq (diskUpd d a v)) /\
                a < diskSize d \/
                get_disk d0 state' ?|= F /\
                get_disk d1 state' ?|= eq d |})
  (write d1 a v) recover abstr
    prim; try solve [ destruct_all ].a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= eq (diskUpd d0 a v)) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= eq d0
    destruct (le_dec (S a) (diskSize d0)).a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
l:S a <= diskSize d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= eq (diskUpd d0 a v)) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= eq d0
a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= eq (diskUpd d0 a v)) /\ 
S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= eq d0
    *a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
l:S a <= diskSize d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= eq (diskUpd d0 a v)) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= eq d0 destruct_all.
    *a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 (diskUpd d0 a v)
   | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
   end ?|= eq (diskUpd d0 a v)) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 (diskUpd d0 a v)
  | OnlyDisk1 _ => OnlyDisk1 (diskUpd d0 a v)
  end ?|= eq d0 rewrite diskUpd_oob_noop by lia.a:addr
v:block
P:disk -> Prop
state:State
H:disk0 state ?|= P
d0:disk
H2:disk1 state ?|= eq d0
state'0:State
H0:disk0 state'0 ?|= P
Heqo:disk1 state'0 = Some d0
n:~ S a <= diskSize d0
(disk0
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 d0
   | OnlyDisk1 _ => OnlyDisk1 d0
   end ?|= P /\
 disk1
   match state'0 with
   | BothDisks d_0 _ | OnlyDisk0 d_0 =>
       BothDisks d_0 d0
   | OnlyDisk1 _ => OnlyDisk1 d0
   end ?|= eq d0) /\ S a <= diskSize d0 \/
disk0
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 d0
  | OnlyDisk1 _ => OnlyDisk1 d0
  end ?|= P /\
disk1
  match state'0 with
  | BothDisks d_0 _ | OnlyDisk0 d_0 =>
      BothDisks d_0 d0
  | OnlyDisk1 _ => OnlyDisk1 d0
  end ?|= eq d0
      destruct_all.
  Qed.

  Theorem size0_ok : proc_spec size0_spec (size d0) recover abstr.proc_spec size0_spec (size d0) recover abstr
  Proof.proc_spec size0_spec (size d0) recover abstr
    unfold size0_spec.proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state (eq d) F;
   post := fun (r : DiskResult nat) (state' : State)
           =>
           match r with
           | Working n =>
               two_disks_are state' (eq d) F /\
               n = diskSize d
           | Failed => two_disks_are state' missing F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state' (eq d) F |})
  (size d0) recover abstr
    unfold two_disks_are.proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= eq d /\
          get_disk d1 state ?|= F;
   post := fun (r : DiskResult nat) (state' : State)
           =>
           match r with
           | Working n =>
               (get_disk d0 state' ?|= eq d /\
                get_disk d1 state' ?|= F) /\
               n = diskSize d
           | Failed =>
               get_disk d0 state' ?|= missing /\
               get_disk d1 state' ?|= F
           end;
   recovered := fun (_ : unit) (state' : State) =>
                get_disk d0 state' ?|= eq d /\
                get_disk d1 state' ?|= F |}) (size d0)
  recover abstr
    prim.
  Qed.

  Theorem size1_ok : proc_spec size1_spec (size d1) recover abstr.proc_spec size1_spec (size d1) recover abstr
  Proof.proc_spec size1_spec (size d1) recover abstr
    unfold size1_spec.proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := two_disks_are state F (eq d);
   post := fun (r : DiskResult nat) (state' : State)
           =>
           match r with
           | Working n =>
               two_disks_are state' F (eq d) /\
               n = diskSize d
           | Failed => two_disks_are state' F missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                two_disks_are state' F (eq d) |})
  (size d1) recover abstr
    unfold two_disks_are.proc_spec
  (fun '(d, F) (state : State) =>
   {|
   pre := get_disk d0 state ?|= F /\
          get_disk d1 state ?|= eq d;
   post := fun (r : DiskResult nat) (state' : State)
           =>
           match r with
           | Working n =>
               (get_disk d0 state' ?|= F /\
                get_disk d1 state' ?|= eq d) /\
               n = diskSize d
           | Failed =>
               get_disk d0 state' ?|= F /\
               get_disk d1 state' ?|= missing
           end;
   recovered := fun (_ : unit) (state' : State) =>
                get_disk d0 state' ?|= F /\
                get_disk d1 state' ?|= eq d |})
  (size d1) recover abstr
    prim.
  Qed.

  Theorem recover_wipe : rec_wipe recover abstr no_wipe.rec_wipe recover abstr no_wipe
  Proof.rec_wipe recover abstr no_wipe
    eauto.
  Qed.

End TwoDisk.