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 VariablesAPI.
Require Import StatDbAPI.

An implementation of StatDB

StatDB is built on top of the Variables API, which maintains variables X, Y, and Z. StatDB reads and writes these variables using the API provided in the VarsAPI module. Here, we use VarX to store the number of integers seen so far, and VarY to store their sum. The mean is then just VarY/VarX, as long as VarX is not zero.

Module StatDB (v : VarsAPI) <: StatDbAPI.

  Import ListNotations.

  Definition add (v : nat) : proc unit :=
    sum <- v.read VarY;
    count <- v.read VarX;
    _ <- v.write VarY (sum + v);
    _ <- v.write VarX (count + 1);
    Ret tt.

Exercise : complete the implementation of mean

  Definition mean : proc (option nat) :=
    Ret None.

  Definition init' : proc InitResult :=
    _ <- v.write VarX 0;
    _ <- v.write VarY 0;
    Ret Initialized.

  Definition init := then_init v.init init'.

  Definition recover : proc unit :=
    v.recover.

Exercise : complete the implementation of the abstraction function:

  Definition statdb_abstraction (vars_state : VariablesAPI.State) (statdb_state : StatDbAPI.State) : Prop :=
    True.

  Definition abstr : Abstraction StatDbAPI.State :=
    abstraction_compose
      v.abstr
      {| abstraction := statdb_abstraction |}.

  Example abstr_1_ok : statdb_abstraction (VariablesAPI.mkState 1 3 0) [3].statdb_abstraction
  {| StateX := 1; StateY := 3; StateZ := 0 |} [3]
  Proof.statdb_abstraction
  {| StateX := 1; StateY := 3; StateZ := 0 |} [3]
    unfold statdb_abstraction; simpl.True
    lia. (* this works for our abstraction relation *)
  Qed.

Exercise : complete the proof for the following admitted examples

  Example abstr_2_ok : statdb_abstraction (VariablesAPI.mkState 2 3 0) [1; 2].statdb_abstraction
  {| StateX := 2; StateY := 3; StateZ := 0 |} [1; 2]
  Proof.statdb_abstraction
  {| StateX := 2; StateY := 3; StateZ := 0 |} [1; 2]
    unfold statdb_abstraction; simpl.True
  Admitted.

  Example abstr_3_ok : statdb_abstraction (VariablesAPI.mkState 0 0 0) nil.statdb_abstraction
  {| StateX := 0; StateY := 0; StateZ := 0 |} []
  Proof.statdb_abstraction
  {| StateX := 0; StateY := 0; StateZ := 0 |} []
  Admitted.

  Example abstr_4_nok : ~ statdb_abstraction (VariablesAPI.mkState 1 0 0) [2].~
statdb_abstraction
  {| StateX := 1; StateY := 0; StateZ := 0 |} [2]
  Proof.~
statdb_abstraction
  {| StateX := 1; StateY := 0; StateZ := 0 |} [2]
    unfold statdb_abstraction; simpl.~ True
  Admitted.

  Example abstr_5_nok : ~ statdb_abstraction (VariablesAPI.mkState 1 0 0) nil.~
statdb_abstraction
  {| StateX := 1; StateY := 0; StateZ := 0 |} []
  Proof.~
statdb_abstraction
  {| StateX := 1; StateY := 0; StateZ := 0 |} []
    unfold statdb_abstraction; simpl.~ True
  Admitted.

  Theorem init_ok : init_abstraction init recover abstr inited.init_abstraction init recover abstr inited
  Proof.init_abstraction init recover abstr inited
    eapply then_init_compose; eauto.proc_spec
  (fun (_ : unit) (state : VariablesAPI.State) =>
   {|
   pre := inited_any state;
   post := fun (r : InitResult)
             (state' : VariablesAPI.State) =>
           match r with
           | Initialized =>
               exists state'' : State,
                 abstraction
                   {|
                   abstraction := statdb_abstraction |}
                   state' state'' /\ inited state''
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : VariablesAPI.State) => True |})
  init' v.recover v.abstr
    unfold init'.proc_spec
  (fun (_ : unit) (state : VariablesAPI.State) =>
   {|
   pre := inited_any state;
   post := fun (r : InitResult)
             (state' : VariablesAPI.State) =>
           match r with
           | Initialized =>
               exists state'' : State,
                 abstraction
                   {|
                   abstraction := statdb_abstraction |}
                   state' state'' /\ inited state''
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : VariablesAPI.State) => True |})
  (_ <- v.write VarX 0;
   _ <- v.write VarY 0; Ret Initialized) v.recover
  v.abstr

    step_proc.a':unit
state:VariablesAPI.State
H:inited_any state
r:unit
Lexec:Marker "after" (v.write VarX 0)
proc_spec
  (fun (_ : unit) (state' : VariablesAPI.State) =>
   {|
   pre := r = tt /\
          state' =
          {|
          StateX := 0;
          StateY := StateY state;
          StateZ := StateZ state |};
   post := fun (r' : InitResult)
             (state'' : VariablesAPI.State) =>
           match r' with
           | Initialized =>
               exists state''0 : State,
                 statdb_abstraction state'' state''0 /\
                 inited state''0
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : VariablesAPI.State) => True |})
  (_ <- v.write VarY 0; Ret Initialized) v.recover
  v.abstr
    step_proc.a':unit
state:VariablesAPI.State
H:inited_any state
Lexec:Marker "after" (v.write VarX 0)
a'0, r:unit
Lexec0:Marker "after" (v.write VarY 0)
proc_spec
  (fun (_ : unit) (state' : VariablesAPI.State) =>
   {|
   pre := r = tt /\
          state' =
          {|
          StateX := StateX
                      {|
                      StateX := 0;
                      StateY := StateY state;
                      StateZ := StateZ state |};
          StateY := 0;
          StateZ := StateZ
                      {|
                      StateX := 0;
                      StateY := StateY state;
                      StateZ := StateZ state |} |};
   post := fun (r' : InitResult)
             (state'' : VariablesAPI.State) =>
           match r' with
           | Initialized =>
               exists state''0 : State,
                 statdb_abstraction state'' state''0 /\
                 inited state''0
           | InitFailed => True
           end;
   recovered := fun (_ : unit)
                  (_ : VariablesAPI.State) => True |})
  (Ret Initialized) v.recover v.abstr
    step_proc.a':unit
state:VariablesAPI.State
H:inited_any state
Lexec:Marker "after" (v.write VarX 0)
a'0:unit
Lexec0:Marker "after" (v.write VarY 0)
a:unit
Lexec1:Marker "post" (Ret Initialized)
exists state'' : State,
  statdb_abstraction
    {|
    StateX := 0;
    StateY := 0;
    StateZ := StateZ state |} state'' /\
  inited state''
    exists nil.a':unit
state:VariablesAPI.State
H:inited_any state
Lexec:Marker "after" (v.write VarX 0)
a'0:unit
Lexec0:Marker "after" (v.write VarY 0)
a:unit
Lexec1:Marker "post" (Ret Initialized)
statdb_abstraction
  {|
  StateX := 0;
  StateY := 0;
  StateZ := StateZ state |} [] /\ inited []
    unfold statdb_abstraction, inited.a':unit
state:VariablesAPI.State
H:inited_any state
Lexec:Marker "after" (v.write VarX 0)
a'0:unit
Lexec0:Marker "after" (v.write VarY 0)
a:unit
Lexec1:Marker "post" (Ret Initialized)
True /\ [] = []
    intuition.
  Qed.

Exercise : complete the proof of add

  Theorem add_ok : forall v, proc_spec (add_spec v) (add v) recover abstr.forall v : nat,
proc_spec (add_spec v) (add v) recover abstr
  Proof.forall v : nat,
proc_spec (add_spec v) (add v) recover abstr
    unfold add.forall v : nat,
proc_spec (add_spec v)
  (sum <- v.read VarY;
   count <- v.read VarX;
   _ <- v.write VarY (sum + v);
   _ <- v.write VarX (count + 1); Ret tt) recover
  abstr
    intros.v:nat
proc_spec (add_spec v)
  (sum <- v.read VarY;
   count <- v.read VarX;
   _ <- v.write VarY (sum + v);
   _ <- v.write VarX (count + 1); Ret tt) recover
  abstr

    apply spec_abstraction_compose; simpl.v:nat
proc_spec
  (fun '(_, state2) (state : VariablesAPI.State) =>
   {|
   pre := True /\ statdb_abstraction state state2;
   post := fun (v0 : unit)
             (state' : VariablesAPI.State) =>
           exists state2' : State,
             (v0 = tt /\ state2' = v :: state2) /\
             statdb_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : VariablesAPI.State) =>
                exists state2' : State,
                  False /\
                  statdb_abstraction state' state2' |})
  (sum <- v.read VarY;
   count <- v.read VarX;
   _ <- v.write VarY (sum + v);
   _ <- v.write VarX (count + 1); Ret tt) recover
  v.abstr
  Admitted.

  Opaque Nat.div.

Exercise : complete the proof of mean

  Theorem mean_ok : proc_spec mean_spec mean recover abstr.proc_spec mean_spec mean recover abstr
  Proof.proc_spec mean_spec mean recover abstr
    unfold mean.proc_spec mean_spec (Ret None) recover abstr
    intros.proc_spec mean_spec (Ret None) recover abstr

    apply spec_abstraction_compose; simpl.proc_spec
  (fun '(_, state2) (state : VariablesAPI.State) =>
   {|
   pre := True /\ statdb_abstraction state state2;
   post := fun (v : option nat)
             (state' : VariablesAPI.State) =>
           exists state2' : State,
             (state2' = state2 /\
              (state2 = [] /\ v = None \/
               state2 <> [] /\
               v =
               Some
                 (fold_right Init.Nat.add 0 state2 /
                  length state2))) /\
             statdb_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : VariablesAPI.State) =>
                exists state2' : State,
                  False /\
                  statdb_abstraction state' state2' |})
  (Ret None) recover v.abstr

  Admitted.


  Theorem recover_wipe : rec_wipe recover abstr no_crash.rec_wipe recover abstr no_crash
  Proof.rec_wipe recover abstr no_crash
    unfold rec_wipe.forall (T : Type) (v : T),
proc_spec
  (fun (_ : unit) (state : State) =>
   {|
   pre := True;
   post := fun (r : T) (state' : State) =>
           r = v /\ state' = state;
   recovered := fun (_ : unit) (state' : State) =>
                no_crash state state' |}) (Ret v)
  recover abstr
    intros.T:Type
v:T
proc_spec
  (fun (_ : unit) (state : State) =>
   {|
   pre := True;
   post := fun (r : T) (state' : State) =>
           r = v /\ state' = state;
   recovered := fun (_ : unit) (state' : State) =>
                no_crash state state' |}) (Ret v)
  recover abstr

    apply spec_abstraction_compose; simpl.T:Type
v:T
proc_spec
  (fun '(_, state2) (state : VariablesAPI.State) =>
   {|
   pre := True /\ statdb_abstraction state state2;
   post := fun (v0 : T) (state' : VariablesAPI.State)
           =>
           exists state2' : State,
             (v0 = v /\ state2' = state2) /\
             statdb_abstraction state' state2';
   recovered := fun (_ : unit)
                  (state' : VariablesAPI.State) =>
                exists state2' : State,
                  no_crash state2 state2' /\
                  statdb_abstraction state' state2' |})
  (Ret v) recover v.abstr
    step_proc.T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
exists state2' : State,
  (v = v /\ state2' = state2) /\
  statdb_abstraction state state2'
T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
state':VariablesAPI.State
H1:False
r:unit
exists state2' : State,
  False /\ statdb_abstraction state' state2'
    {T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
exists state2' : State,
  (v = v /\ state2' = state2) /\
  statdb_abstraction state state2' exists state2.T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
(v = v /\ state2 = state2) /\
statdb_abstraction state state2 eauto. }T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
state':VariablesAPI.State
H1:False
r:unit
exists state2' : State,
  False /\ statdb_abstraction state' state2'
    {T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
state':VariablesAPI.State
H1:False
r:unit
exists state2' : State,
  False /\ statdb_abstraction state' state2' exfalso.T:Type
v:T
a0:unit
state2:State
state:VariablesAPI.State
H:True
H0:statdb_abstraction state state2
Lexec:Marker "post" (Ret v)
state':VariablesAPI.State
H1:False
r:unit
False eauto. }
  Qed.

End StatDB.


Require Import VariablesImpl.
Module StatDBImpl := StatDB Vars.
Print Assumptions StatDBImpl.abstr_2_ok.Axioms:
StatDBImpl.abstr_2_ok
  : StatDBImpl.statdb_abstraction
      {| StateX := 2; StateY := 3; StateZ := 0 |}
      (1 :: 2 :: nil)
Print Assumptions StatDBImpl.abstr_3_ok.Axioms:
StatDBImpl.abstr_3_ok
  : StatDBImpl.statdb_abstraction
      {| StateX := 0; StateY := 0; StateZ := 0 |} nil
Print Assumptions StatDBImpl.abstr_4_nok.Axioms:
StatDBImpl.abstr_4_nok
  : ~
    StatDBImpl.statdb_abstraction
      {| StateX := 1; StateY := 0; StateZ := 0 |}
      (2 :: nil)
Print Assumptions StatDBImpl.abstr_5_nok.Axioms:
StatDBImpl.abstr_5_nok
  : ~
    StatDBImpl.statdb_abstraction
      {| StateX := 1; StateY := 0; StateZ := 0 |} nil
Print Assumptions StatDBImpl.add_ok.Axioms:
StatDBImpl.add_ok
  : forall v : nat,
    proc_spec (add_spec v) (StatDBImpl.add v)
      StatDBImpl.recover StatDBImpl.abstr
Print Assumptions StatDBImpl.mean_ok.Axioms:
StatDBImpl.mean_ok
  : proc_spec mean_spec StatDBImpl.mean
      StatDBImpl.recover StatDBImpl.abstr