RemappedDiskImpl.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 OneDiskAPI.
Require Import BadBlockAPI.


Module RemappedDisk (bd : BadBlockAPI) <: OneDiskAPI.

  Import ListNotations.

  Definition read (a : addr) : proc block :=
    bs <- bd.getBadBlock;
    if a == bs then
      len <- bd.size;
      r <- bd.read (len-1);
      Ret r
    else
      r <- bd.read a;
    Ret r.

  Definition write (a : addr) (b : block) : proc unit :=
    Ret tt.

  Definition size : proc nat :=
    len <- bd.size;
    Ret (len - 1).

  Definition init' : proc InitResult :=
    len <- bd.size;
    if len == 0 then
      Ret InitFailed
    else
      bs <- bd.getBadBlock;
      if (lt_dec bs len) then
        Ret Initialized
      else
        Ret InitFailed.

  Definition init := then_init bd.init init'.

  Definition recover: proc unit :=
    bd.recover.


  Inductive remapped_abstraction (bs_state : BadBlockAPI.State) (rd_disk : OneDiskAPI.State) : Prop :=
    | RemappedAbstraction :
      let bs_disk := stateDisk bs_state in
      let bs_addr := stateBadBlock bs_state in
      forall
        (* Fill in the rest of your abstraction here. *)
        (* To refer to the contents of disk [d] at address [a], you can write [diskGet a] *)
        (* To refer to the size of disk [d], you can write [diskSize d] *)
        (* You can try to prove [read_ok] to discover what you need from this abstraction *)

        (* Hint 1: What should be true about the non-bad blocks?   Replace [True] with what needs to be true *)
        (Hgoodblocks : True)
        (* Hint 2: What should be true about the bad block? *)
        (Hbadblock : True)

        (* when writing the above,  *)
        (* Hint 3: What if the bad block address is the last address? *)
        (Hsize : diskSize bs_disk = diskSize rd_disk + 1),
      remapped_abstraction bs_state rd_disk.

  Hint Constructors remapped_abstraction : core.

  Definition abstr : Abstraction OneDiskAPI.State :=
    abstraction_compose bd.abstr {| abstraction := remapped_abstraction |}.

  (* Note that these examples aren't trivial to prove, even if you have the
     right abstraction relation. They should help you think about whether your
     abstraction relation makes sense (although you may need to modify it to
     actually prove the implementation correct). *)

  Example abst_1_ok : forall Hinbounds,
    remapped_abstraction (BadBlockAPI.mkState [block1;block0;block0] 0 Hinbounds) [block0;block0].forall
  Hinbounds : 0 < diskSize [block1; block0; block0],
remapped_abstraction
  {|
  stateDisk := [block1; block0; block0];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |}
  [block0; block0]
  Proof.forall
  Hinbounds : 0 < diskSize [block1; block0; block0],
remapped_abstraction
  {|
  stateDisk := [block1; block0; block0];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |}
  [block0; block0]
    constructor; auto.
    Admitted.

  Example abst_2_ok : forall Hinbounds,
    remapped_abstraction (BadBlockAPI.mkState [block1;block0] 0 Hinbounds) [block0].forall Hinbounds : 0 < diskSize [block1; block0],
remapped_abstraction
  {|
  stateDisk := [block1; block0];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
  Proof.forall Hinbounds : 0 < diskSize [block1; block0],
remapped_abstraction
  {|
  stateDisk := [block1; block0];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
    constructor; auto.
    Admitted.

  Example abst_3_ok : forall Hinbounds,
    remapped_abstraction (BadBlockAPI.mkState [block0;block0] 1 Hinbounds) [block0].forall Hinbounds : 1 < diskSize [block0; block0],
remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block0]
  Proof.forall Hinbounds : 1 < diskSize [block0; block0],
remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block0]
    constructor; auto.
    Admitted.

  Example abst_4_nok : forall Hinbounds,
    ~ remapped_abstraction (BadBlockAPI.mkState [block0;block0] 1 Hinbounds) [block1].forall Hinbounds : 1 < diskSize [block0; block0],
~
remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block1]
  Proof.forall Hinbounds : 1 < diskSize [block0; block0],
~
remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block1]
    intros.Hinbounds:1 < diskSize [block0; block0]
~
remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block1]
    intro.Hinbounds:1 < diskSize [block0; block0]
H:remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block1]
False
    inversion H; simpl in *.Hinbounds:1 < 2
H:remapped_abstraction
  {|
  stateDisk := [block0; block0];
  stateBadBlock := 1;
  stateBadBlockInBounds := Hinbounds |} [block1]
bs_disk:=[block0; block0]:disk
bs_addr:=1:addr
Hgoodblocks, Hbadblock:True
Hsize:2 = 2
False
    Admitted.

  Example abst_5_nok : forall Hinbounds,
    ~ remapped_abstraction (BadBlockAPI.mkState [block1;block1] 0 Hinbounds) [block0].forall Hinbounds : 0 < diskSize [block1; block1],
~
remapped_abstraction
  {|
  stateDisk := [block1; block1];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
  Proof.forall Hinbounds : 0 < diskSize [block1; block1],
~
remapped_abstraction
  {|
  stateDisk := [block1; block1];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
    intros.Hinbounds:0 < diskSize [block1; block1]
~
remapped_abstraction
  {|
  stateDisk := [block1; block1];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
    intro.Hinbounds:0 < diskSize [block1; block1]
H:remapped_abstraction
  {|
  stateDisk := [block1; block1];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
False
    inversion H; simpl in *.Hinbounds:0 < 2
H:remapped_abstraction
  {|
  stateDisk := [block1; block1];
  stateBadBlock := 0;
  stateBadBlockInBounds := Hinbounds |} [block0]
bs_disk:=[block1; block1]:disk
bs_addr:=0:addr
Hgoodblocks, Hbadblock:True
Hsize:2 = 2
False
    Admitted.

  (* Due to how remapped_abstraction is defined (as an inductive), it cannot be
  unfolded. This tactic identifies abstraction relations in the hypotheses and
  breaks them apart with [inversion], and also does some cleanup. *)
  Ltac invert_abstraction :=
    match goal with
    | H : remapped_abstraction _ _ |- _ => inversion H; clear H; subst; subst_var
    end.

  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
    eapply then_init_compose; eauto.proc_spec
  (fun (_ : unit) (state : State) =>
   {|
   pre := inited_any state;
   post := fun (r : InitResult) (state' : State) =>
           match r with
           | Initialized =>
               exists state'' : OneDiskAPI.State,
                 abstraction
                   {|
                   abstraction := remapped_abstraction |}
                   state' state'' /\
                 inited_any state''
           | InitFailed => True
           end;
   recovered := fun (_ : unit) (_ : State) => True |})
  init' bd.recover bd.abstr
    step_proc.a':unit
state:State
H:inited_any state
r:nat
Lexec:Marker "after" bd.size
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\
          r = diskSize (stateDisk state);
   post := fun (r' : InitResult) (state'' : State) =>
           match r' with
           | Initialized =>
               exists state''0 : OneDiskAPI.State,
                 remapped_abstraction state'' state''0 /\
                 inited_any state''0
           | InitFailed => True
           end;
   recovered := fun (_ : unit) (_ : State) => True |})
  (if equal_dec r 0
   then Ret InitFailed
   else
    bs <- bd.getBadBlock;
    (if lt_dec bs r
     then Ret Initialized
     else Ret InitFailed)) bd.recover bd.abstr
  Admitted.

  Theorem read_ok : forall a, proc_spec (OneDiskAPI.read_spec a) (read a) recover abstr.forall a : addr,
proc_spec (OneDiskAPI.read_spec a) (read a) recover
  abstr
  Proof.forall a : addr,
proc_spec (OneDiskAPI.read_spec a) (read a) recover
  abstr
    unfold read.forall a : addr,
proc_spec (OneDiskAPI.read_spec a)
  (bs <- bd.getBadBlock;
   (if equal_dec a bs
    then len <- bd.size; r <- bd.read (len - 1); Ret r
    else r <- bd.read a; Ret r)) recover abstr
    intros.a:addr
proc_spec (OneDiskAPI.read_spec a)
  (bs <- bd.getBadBlock;
   (if equal_dec a bs
    then len <- bd.size; r <- bd.read (len - 1); Ret r
    else r <- bd.read a; Ret r)) recover abstr

    apply spec_abstraction_compose; simpl.a:addr
proc_spec
  (fun '(_, state2) (state : State) =>
   {|
   pre := True /\ remapped_abstraction state state2;
   post := fun (v : block) (state' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= v) /\
             remapped_abstraction state' state2';
   recovered := fun (_ : unit) (state' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state' state2' |})
  (bs <- bd.getBadBlock;
   (if equal_dec a bs
    then len <- bd.size; r <- bd.read (len - 1); Ret r
    else r <- bd.read a; Ret r)) recover bd.abstr
    step_proc; eauto.a:addr
a0:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:addr
Lexec:Marker "after" bd.getBadBlock
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\ r = stateBadBlock state;
   post := fun (r' : block) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= r') /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (if equal_dec a r
   then len <- bd.size; r <- bd.read (len - 1); Ret r
   else r <- bd.read a; Ret r) recover bd.abstr

    destruct (a == r).a:addr
a0:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:addr
Lexec:Marker "after" bd.getBadBlock
e:a = r
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\ r = stateBadBlock state;
   post := fun (r' : block) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= r') /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (len <- bd.size; r <- bd.read (len - 1); Ret r)
  recover bd.abstr
a:addr
a0:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:addr
Lexec:Marker "after" bd.getBadBlock
n:a <> r
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\ r = stateBadBlock state;
   post := fun (r' : block) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= r') /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (r <- bd.read a; Ret r) recover bd.abstr
    -a:addr
a0:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:addr
Lexec:Marker "after" bd.getBadBlock
e:a = r
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\ r = stateBadBlock state;
   post := fun (r' : block) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= r') /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (len <- bd.size; r <- bd.read (len - 1); Ret r)
  recover bd.abstr admit.
    -a:addr
a0:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:addr
Lexec:Marker "after" bd.getBadBlock
n:a <> r
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\ r = stateBadBlock state;
   post := fun (r' : block) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\
              diskGet state2 a =?= r') /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (r <- bd.read a; Ret r) recover bd.abstr admit.
  Admitted.


  Theorem bad_block_inbounds :
    forall state,
      stateBadBlock state < diskSize (stateDisk state).forall state : State,
stateBadBlock state < diskSize (stateDisk state)
  Proof.forall state : State,
stateBadBlock state < diskSize (stateDisk state)
    intros.state:State
stateBadBlock state < diskSize (stateDisk state)
    destruct state.stateDisk:disk
stateBadBlock:addr
stateBadBlockInBounds:stateBadBlock <
diskSize stateDisk
BadBlockAPI.stateBadBlock
  {|
  stateDisk := stateDisk;
  stateBadBlock := stateBadBlock;
  stateBadBlockInBounds := stateBadBlockInBounds |} <
diskSize
  (BadBlockAPI.stateDisk
     {|
     stateDisk := stateDisk;
     stateBadBlock := stateBadBlock;
     stateBadBlockInBounds := stateBadBlockInBounds |})
    simpl.stateDisk:disk
stateBadBlock:addr
stateBadBlockInBounds:stateBadBlock <
diskSize stateDisk
stateBadBlock < diskSize stateDisk
    exact stateBadBlockInBounds.
  Qed.

  Theorem remapped_abstraction_diskUpd_remap : forall state state' s v,
    remapped_abstraction state s ->
    stateBadBlock state' = stateBadBlock state ->
    stateDisk state' = diskUpd (stateDisk state) (diskSize (stateDisk state) - 1) v ->
    remapped_abstraction state' (diskUpd s (stateBadBlock state) v).forall (state state' : State) (s : OneDiskAPI.State)
  (v : block),
remapped_abstraction state s ->
stateBadBlock state' = stateBadBlock state ->
stateDisk state' =
diskUpd (stateDisk state)
  (diskSize (stateDisk state) - 1) v ->
remapped_abstraction state'
  (diskUpd s (stateBadBlock state) v)
  Proof.forall (state state' : State) (s : OneDiskAPI.State)
  (v : block),
remapped_abstraction state s ->
stateBadBlock state' = stateBadBlock state ->
stateDisk state' =
diskUpd (stateDisk state)
  (diskSize (stateDisk state) - 1) v ->
remapped_abstraction state'
  (diskUpd s (stateBadBlock state) v)
    (* Hint: you may find it useful to use the [pose proof (bad_block_inbounds state)]
       if you need [lia] to make use of the fact that the bad block is in-bounds. *)
    Admitted.


  Theorem remapped_abstraction_diskUpd_noremap : forall state state' s a v,
    remapped_abstraction state s ->
    a <> diskSize (stateDisk state) - 1 ->
    a <> stateBadBlock state ->
    stateBadBlock state' = stateBadBlock state ->
    stateDisk state' = diskUpd (stateDisk state) a v ->
    remapped_abstraction state' (diskUpd s a v).forall (state state' : State) (s : OneDiskAPI.State)
  (a : nat) (v : block),
remapped_abstraction state s ->
a <> diskSize (stateDisk state) - 1 ->
a <> stateBadBlock state ->
stateBadBlock state' = stateBadBlock state ->
stateDisk state' = diskUpd (stateDisk state) a v ->
remapped_abstraction state' (diskUpd s a v)
  Proof.forall (state state' : State) (s : OneDiskAPI.State)
  (a : nat) (v : block),
remapped_abstraction state s ->
a <> diskSize (stateDisk state) - 1 ->
a <> stateBadBlock state ->
stateBadBlock state' = stateBadBlock state ->
stateDisk state' = diskUpd (stateDisk state) a v ->
remapped_abstraction state' (diskUpd s a v)
    Admitted.

  Hint Resolve remapped_abstraction_diskUpd_remap : core.
  Hint Resolve remapped_abstraction_diskUpd_noremap : core.

  Theorem write_ok : forall a v, proc_spec (OneDiskAPI.write_spec a v) (write a v) recover abstr.forall (a : addr) (v : block),
proc_spec (OneDiskAPI.write_spec a v) (write a v)
  recover abstr
  Proof.forall (a : addr) (v : block),
proc_spec (OneDiskAPI.write_spec a v) (write a v)
  recover abstr
    unfold write.forall (a : addr) (v : block),
proc_spec (OneDiskAPI.write_spec a v) (Ret tt) recover
  abstr
    intros.a:addr
v:block
proc_spec (OneDiskAPI.write_spec a v) (Ret tt) recover
  abstr

    apply spec_abstraction_compose; simpl.a:addr
v:block
proc_spec
  (fun '(_, state2) (state : State) =>
   {|
   pre := True /\ remapped_abstraction state state2;
   post := fun (v0 : unit) (state' : State) =>
           exists state2' : OneDiskAPI.State,
             (v0 = tt /\ state2' = diskUpd state2 a v) /\
             remapped_abstraction state' state2';
   recovered := fun (_ : unit) (state' : State) =>
                exists state2' : OneDiskAPI.State,
                  (state2' = state2 \/
                   state2' = diskUpd state2 a v) /\
                  remapped_abstraction state' state2' |})
  (Ret tt) recover bd.abstr
    Admitted.

  Theorem size_ok : proc_spec OneDiskAPI.size_spec size recover abstr.proc_spec OneDiskAPI.size_spec size recover abstr
  Proof.proc_spec OneDiskAPI.size_spec size recover abstr
    unfold diskSize.proc_spec OneDiskAPI.size_spec size recover abstr
    intros.proc_spec OneDiskAPI.size_spec size recover abstr

    apply spec_abstraction_compose; simpl.proc_spec
  (fun '(_, state2) (state : State) =>
   {|
   pre := True /\ remapped_abstraction state state2;
   post := fun (v : nat) (state' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\ v = diskSize state2) /\
             remapped_abstraction state' state2';
   recovered := fun (_ : unit) (state' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state' state2' |})
  size recover bd.abstr

    step_proc; eauto.a:unit
state2:OneDiskAPI.State
state:State
H:True
H0:remapped_abstraction state state2
r:nat
Lexec:Marker "after" bd.size
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := state' = state /\
          r = diskSize (stateDisk state);
   post := fun (r' : nat) (state'' : State) =>
           exists state2' : OneDiskAPI.State,
             (state2' = state2 /\ r' = diskSize state2) /\
             remapped_abstraction state'' state2';
   recovered := fun (_ : unit) (state'' : State) =>
                exists state2' : OneDiskAPI.State,
                  state2' = state2 /\
                  remapped_abstraction state'' state2' |})
  (Ret (r - 1)) recover bd.abstr
    Admitted.

  (* This proof proves that recovery corresponds to no_wipe. *)
  Theorem recover_wipe : rec_wipe recover abstr no_wipe.rec_wipe recover abstr no_wipe
  Proof.rec_wipe recover abstr no_wipe
    unfold rec_wipe.forall (T : Type) (v : T),
proc_spec
  (fun (_ : unit) (state : OneDiskAPI.State) =>
   {|
   pre := True;
   post := fun (r : T) (state' : OneDiskAPI.State) =>
           r = v /\ state' = state;
   recovered := fun (_ : unit)
                  (state' : OneDiskAPI.State) =>
                no_wipe state state' |}) (Ret v)
  recover abstr
    intros.T:Type
v:T
proc_spec
  (fun (_ : unit) (state : OneDiskAPI.State) =>
   {|
   pre := True;
   post := fun (r : T) (state' : OneDiskAPI.State) =>
           r = v /\ state' = state;
   recovered := fun (_ : unit)
                  (state' : OneDiskAPI.State) =>
                no_wipe state state' |}) (Ret v)
  recover abstr

    apply spec_abstraction_compose; simpl.T:Type
v:T
proc_spec
  (fun '(_, state2) (state : State) =>
   {|
   pre := True /\ remapped_abstraction state state2;
   post := fun (v0 : T) (state' : State) =>
           exists state2' : OneDiskAPI.State,
             (v0 = v /\ state2' = state2) /\
             remapped_abstraction state' state2';
   recovered := fun (_ : unit) (state' : State) =>
                exists state2' : OneDiskAPI.State,
                  no_wipe state2 state2' /\
                  remapped_abstraction state' state2' |})
  (Ret v) recover bd.abstr
    step_proc; eauto.
  Qed.

End RemappedDisk.


Require Import BadBlockImpl.
Module x := RemappedDisk BadBlockDisk.
Print Assumptions x.write_ok.Axioms:
x.write_ok
  : forall (a : addr) (v : block),
    proc_spec (OneDiskAPI.write_spec a v)
      (x.write a v) x.recover x.abstr