# POCS.Lab3.LogImpl

# Implementation of the atomic append-only log.

Axiom addr_to_block : addr -> proc block.

Axiom block_to_addr : block -> addr.

Definition addr_to_block_spec State a : Specification unit block unit State :=

fun (_ : unit) state => {|

pre := True;

post := fun r state' => state' = state /\ block_to_addr r = a;

recovered := fun _ state' => state' = state

|}.

Axiom addr_to_block_ok : forall State a recover abstr,

proc_spec (@addr_to_block_spec State a) (addr_to_block a) recover abstr.

Hint Resolve addr_to_block_ok : core.

For this lab, we provide a notation for diskUpd. Not only can you use this
to write diskUpd d a b as d [a |-> b] but you will also see this notation
in goals. This should especially make it easier to read goals with many
updates of the same disk.
Remember that the code still uses diskUpd underneath, so the same theorems
apply. We recommend using autorewrite with upd or autorewrite with upd
in * in this lab to simplify diskGet/diskUpd expressions, rather than
using the theorems manually.

Notation "d [ a |-> b ]" := (diskUpd d a b) (at level 8, left associativity).

Notation "d [ a |=> bs ]" := (diskUpds d a bs) (at level 8, left associativity).

Opaque diskGet.

Notation "d [ a |=> bs ]" := (diskUpds d a bs) (at level 8, left associativity).

Opaque diskGet.

In this lab, you will likely be doing reasoning about
the contents of various disk blocks. The following
theorem will help you do so.

Theorem diskGet_eq_values : forall d a b b',

diskGet d a =?= b ->

diskGet d a =?= b' ->

a < diskSize d ->

b = b'.

Proof.

(* Fill in your proof here. *)

Admitted.

diskGet d a =?= b ->

diskGet d a =?= b' ->

a < diskSize d ->

b = b'.

Proof.

(* Fill in your proof here. *)

Admitted.

We use the above theorem to implement the eq_values
tactic. eq_values can be used when you have hypotheses
like:
H1: diskGet d a =?= eq b
H2: diskGet d a =?= eq b'
In this context, the tactic proves b = b'.

Ltac eq_values :=

match goal with

| [ H: diskGet ?d ?a =?= ?b,

H': diskGet ?d ?a =?= ?b' |- _ ] =>

assert (b = b') by (apply (@diskGet_eq_values d a b b'); try lia; auto);

subst

end.

Module Log (d : OneDiskAPI) <: LogAPI.

match goal with

| [ H: diskGet ?d ?a =?= ?b,

H': diskGet ?d ?a =?= ?b' |- _ ] =>

assert (b = b') by (apply (@diskGet_eq_values d a b b'); try lia; auto);

subst

end.

Module Log (d : OneDiskAPI) <: LogAPI.

Fill in your implementation and proof here, replacing
the placeholder statements below with your own definitions
and theorems as appropriate. Feel free to introduce helper
procedures and helper theorems to structure your implementation
and proof.

Definition init : proc InitResult := Ret Initialized.

Definition get : proc (list block) := Ret nil.

Definition append (bs : list block) : proc bool := Ret true.

Definition reset : proc unit := Ret tt.

Definition recover : proc unit := Ret tt.

Axiom abstr : Abstraction State.

Axiom init_ok : init_abstraction init recover abstr inited_any.

Axiom get_ok : proc_spec get_spec get recover abstr.

Axiom append_ok : forall v, proc_spec (append_spec v) (append v) recover abstr.

Axiom reset_ok : proc_spec reset_spec reset recover abstr.

Axiom recover_wipe : rec_wipe recover abstr no_wipe.

End Log.

It's possible to layer the log from this lab on top
of the bad-block remapper from the previous lab.
The statements below do that, just as a sanity check.

Require Import Lab2.BadBlockImpl.

Require Import Lab2.RemappedDiskImpl.

Module bad_disk := BadBlockDisk.

Module remapped_disk := RemappedDisk bad_disk.

Module log := Log remapped_disk.

Print Assumptions log.append_ok.