Library airlock
From Coq Require Import Arith.
From FreeSpec.Core Require Import Core CoreFacts.
#[local] Open Scope nat_scope.
Create HintDb airlock.
Inductive door : Type := left | right.
Definition door_eq_dec (d d' : door) : { d = d' } + { ¬ d = d' } :=
ltac:(decide equality).
Inductive DOORS : interface :=
| IsOpen : door → DOORS bool
| Toggle : door → DOORS unit.
Generalizable All Variables.
Definition is_open `{Provide ix DOORS} (d : door) : impure ix bool :=
request (IsOpen d).
Definition toggle `{Provide ix DOORS} (d : door) : impure ix unit :=
request (Toggle d).
Definition open_door `{Provide ix DOORS} (d : door) : impure ix unit :=
let× open := is_open d in
when (negb open) (toggle d).
Definition close_door `{Provide ix DOORS} (d : door) : impure ix unit :=
let× open := is_open d in
when open (toggle d).
Inductive CONTROLLER : interface :=
| Tick : CONTROLLER unit
| RequestOpen (d : door) : CONTROLLER unit.
Definition tick `{Provide ix CONTROLLER} : impure ix unit :=
request Tick.
Definition request_open `{Provide ix CONTROLLER} (d : door) : impure ix unit :=
request (RequestOpen d).
Definition co (d : door) : door :=
match d with
| left ⇒ right
| right ⇒ left
end.
Definition controller `{Provide ix DOORS, Provide ix (STORE nat)}
: component CONTROLLER ix :=
fun _ op ⇒
match op with
| Tick ⇒
let× cpt := get in
when (15 <? cpt) begin
close_door left;;
close_door right;;
put 0
end
| RequestOpen d ⇒
close_door (co d);;
open_door d;;
put 0
end.
Definition Ω : Type := bool × bool.
Definition sel (d : door) : Ω → bool :=
match d with
| left ⇒ fst
| right ⇒ snd
end.
Definition tog (d : door) (ω : Ω) : Ω :=
match d with
| left ⇒ (negb (fst ω), snd ω)
| right ⇒ (fst ω, negb (snd ω))
end.
Lemma tog_equ_1 (d : door) (ω : Ω)
: sel d (tog d ω) = negb (sel d ω).
Proof.
destruct d; reflexivity.
Qed.
Lemma tog_equ_2 (d : door) (ω : Ω)
: sel (co d) (tog d ω) = sel (co d) ω.
Proof.
destruct d; reflexivity.
Qed.
From now on, we will reason about tog using tog_equ_1 and tog_equ_2.
FreeSpec tactics rely heavily on cbn to simplify certain terms, so we use
the simpl never options of the Arguments vernacular command to prevent
cbn from unfolding tog.
This pattern is common in FreeSpec. Later in this example, we will use this
trick to prevent cbn to unfold impure computations covered by intermediary
theorems.
#[local] Opaque tog.
Definition step (ω : Ω) (a : Type) (e : DOORS a) (x : a) :=
match e with
| Toggle d ⇒ tog d ω
| _ ⇒ ω
end.
Inductive doors_o_caller : Ω → ∀ (a : Type), DOORS a → Prop :=
- Given the door d of o system ω, it is always possible to ask for the state of d.
| req_is_open (d : door) (ω : Ω)
: doors_o_caller ω bool (IsOpen d)
- Given the door d of o system ω, if d is closed, then the second door co d has to be closed too for a request to toggle d to be valid.
| req_toggle (d : door) (ω : Ω) (H : sel d ω = false → sel (co d) ω = false)
: doors_o_caller ω unit (Toggle d).
Hint Constructors doors_o_caller : airlock.
Inductive doors_o_callee : Ω → ∀ (a : Type), DOORS a → a → Prop :=
- When a system in a state ω reports the state of the door d, it shall reflect the true state of d.
| doors_o_callee_is_open (d : door) (ω : Ω) (x : bool) (equ : sel d ω = x)
: doors_o_callee ω bool (IsOpen d) x
- There is no particular doors_o_calleeises on the result x of a request for ω to close the door d.
| doors_o_callee_toggle (d : door) (ω : Ω) (x : unit)
: doors_o_callee ω unit (Toggle d) x.
Hint Constructors doors_o_callee : airlock.
Definition doors_contract : contract DOORS Ω :=
make_contract step doors_o_caller doors_o_callee.
Lemma close_door_respectful `{Provide ix DOORS} (ω : Ω) (d : door)
: pre (to_hoare doors_contract (close_door d)) ω.
Proof.
prove impure with airlock; subst; constructor.
inversion o_caller0; ssubst.
now rewrite H3.
Qed.
Hint Resolve close_door_respectful : airlock.
Lemma open_door_respectful `{Provide ix DOORS} (ω : Ω)
(d : door) (safe : sel (co d) ω = false)
: pre (to_hoare doors_contract (open_door (ix := ix) d)) ω.
Proof.
prove impure; repeat constructor; subst.
inversion o_caller0; ssubst.
now rewrite safe.
Qed.
Hint Resolve open_door_respectful : airlock.
Lemma close_door_run `{Provide ix DOORS} (ω : Ω) (d : door) (ω' : Ω) (x : unit)
(run : post (to_hoare doors_contract (close_door d)) ω x ω')
: sel d ω' = false.
Proof.
unroll_post run.
+ rewrite tog_equ_1.
inversion H1; ssubst.
now rewrite H5.
+ now inversion H1; ssubst.
Qed.
Hint Resolve close_door_run : airlock.
#[local] Opaque close_door.
#[local] Opaque open_door.
#[local] Opaque Nat.ltb.
Remark one_door_safe_all_doors_safe (ω : Ω) (d : door)
(safe : sel d ω = false ∨ sel (co d) ω = false)
: ∀ (d' : door), sel d' ω = false ∨ sel (co d') ω = false.
Proof.
intros d'.
destruct d; destruct d'; auto.
+ cbn -[sel].
now rewrite or_comm.
+ cbn -[sel].
fold (co right).
now rewrite or_comm.
Qed.
The objective of this lemma is to prove that, if either the right door or
the left door is closed, then after any respectful run of a computation
p that interacts with doors, this fact remains true.
#[local] Opaque sel.
Lemma respectful_run_inv `{Provide ix DOORS} {a} (p : impure ix a)
(ω : Ω) (safe : sel left ω = false ∨ sel right ω = false)
(x : a) (ω' : Ω) (hpre : pre (to_hoare doors_contract p) ω)
(hpost : post (to_hoare doors_contract p) ω x ω')
: sel left ω' = false ∨ sel right ω' = false.
We reason by induction on the impure computation p:
- Either p is a local, pure computation; in such a case, the doors state
does not change, hence the proof is trivial.
- Or p consists in a request to the doors interface, and a continuation
whose domain satisfies the theorem, i.e. it preserves the invariant that
either the left or the right door is closed. Due to this hypothesis, we
only have to prove that the first request made by p does not break the
invariant. We consider two cases.
- Either the computation asks for the state of a given door (IsOpen), then again the doors state does not change and the proof is trivial.
- Or the computation wants to toggle a door d. We know by hypothesis
that either d is closed or d is open (thanks to the
one_door_safe_all_doors_safe result and the safe hypothesis).
Again, we consider both cases.
- If d is closed —and therefore will be opened—, then because we consider a respectful run, co d is necessarily closed too (it is a requirements of door_contract). Once d is opened, co d is still closed.
- Otherwise, co d is closed, which means once d is toggled (no
matter its initial state), then co d is still closed.
Proof.
fold (co left) in ×.
revert ω hpre hpost safe.
induction p; intros ω hpre run safe.
+ now unroll_post run.
+ unroll_post run.
assert (hpost : post (interface_to_hoare doors_contract β e) ω x0 ω0). {
split; [apply H2|now rewrite H3].
}
apply H1 with (ω:=ω0) (β:=x0); auto; [now apply hpre|].
cbn in ×.
unfold gen_caller_obligation, gen_callee_obligation, gen_witness_update in ×.
destruct (proj_p e) as [e'|].
++ destruct hpost as [o_callee equω].
destruct e' as [d|d].
+++ rewrite H3.
apply safe.
+++ apply one_door_safe_all_doors_safe with (d := d);
apply one_door_safe_all_doors_safe with (d' := d) in safe;
subst.
destruct hpre as [hbefore hafter].
inversion hbefore; ssubst.
cbn.
destruct safe as [safe|safe].
all: right; rewrite tog_equ_2; auto.
++ destruct hpost as [_ equω].
subst.
exact safe.
Qed.
Lemma controller_correct `{StrictProvide2 ix DOORS (STORE nat)}
: correct_component controller
(no_contract CONTROLLER)
doors_contract
(fun _ ω ⇒ sel left ω = false ∨ sel right ω = false).
Proof.
intros ωc ωd pred a e req.
assert (hpre : pre (to_hoare doors_contract (controller a e)) ωd)
by (destruct e; prove impure with airlock).
split; auto.
intros x ωj' run.
cbn.
split.
+ auto with freespec.
+ apply respectful_run_inv in run; auto.
Qed.