Library imp

imp: a formalisation of the IMP programming language on top of KAT



From RelationAlgebra Require Import kat prop rel comparisons kat_tac.

Section s.
identifiers for memory locations
Variable loc: Set.
abstract state (or memory)
Variable state: Set.
updating the state
Variable update: loc → nat → state → state.

Definition of the languague

programs

Inductive prog :=
| skp
| aff (x: loc) (e: state → nat)
| seq (p q: prog)
| ite (t: dset state) (p q: prog)
| whl (t: dset state) (p: prog).

notations
Declare Scope imp_scope.
Bind Scope imp_scope with prog.
Delimit Scope imp_scope with imp.
Notation "x <- y" := (aff x y) (at level 90): imp_scope.
Notation "p ;; q" := (seq p%imp q%imp) (left associativity, at level 101): imp_scope.
Arguments ite _%ra _%imp _%imp.
Arguments whl _%ra _%imp.

Big step semantics

corresponding functional relation
Notation upd x e := (frel (fun s ⇒ update x (e s) s)).

using KAT expressions in the model of relations

the semantics can then be given by induction on the program, using a simple fixpoint

Fixpoint bstep (p: prog): hrel state state :=
  match p with
    | skp ⇒ 1
    | aff x e ⇒ upd x e
    | seq p q ⇒ bstep p ⋅ bstep q
    | ite b p q ⇒ [b] ⋅ bstep p + [!b] ⋅ bstep q
    | whl b p ⇒ ([b] ⋅ bstep p)^* ⋅ [!b]
  end.

using an inductive predicate, as in standard textbooks


Inductive bstep': prog → hrel state state :=
| s_skp: ∀ s, bstep' skp s s
| s_aff: ∀ x e s, bstep' (x <- e) s (update x (e s) s)
| s_seq: ∀ p q s s' s'', bstep' p s s' → bstep' q s' s'' → bstep' (p ;; q) s s''
| s_ite_ff: ∀ (b: dset state) p q s s', b s = false → bstep' q s s' → bstep' (ite b p q) s s'
| s_ite_tt: ∀ (b: dset state) p q s s', b s = true → bstep' p s s' → bstep' (ite b p q) s s'
| s_whl_ff: ∀ (b: dset state) p s, b s = false → bstep' (whl b p) s s
| s_whl_tt: ∀ (b: dset state) p s s', b s = true → bstep' (p ;; whl b p) s s' → bstep' (whl b p) s s'.

equivalence between the two definitions


Lemma bstep_eq p: bstep' p ≡ bstep p.
Proof.
  apply antisym.
  - intros s s'. induction 1.
     reflexivity.
     reflexivity.
     eexists; eassumption.
     right. eexists. split. reflexivity. simpl; now rewrite H. assumption.
     left. eexists. split. reflexivity. assumption. assumption.
     ∃ s. apply (str_refl ([b] ⋅ bstep p)). reflexivity.
      simpl. unfold hrel_inj. simpl. now rewrite H.
     destruct IHbstep' as [t ? [t' ? ?]]. ∃ t'. 2: assumption.
     apply (str_cons ([b] ⋅ bstep p)). ∃ t. 2: assumption.
     eexists; eauto. now split.
  - induction p; unfold bstep; fold bstep.
     intros ? ? <-. constructor.
     intros ? ? →. constructor.
     intros ? ? [? H1 H2]. econstructor. apply IHp1, H1. apply IHp2, H2.
     intros ? ? [[? [<- H] H']|[? [<- H] H']].
      apply s_ite_tt. assumption. apply IHp1, H'.
      apply s_ite_ff. now apply Bool.negb_true_iff. apply IHp2, H'.
     apply str_ind_l'.
      intros ? ? [<- H]. apply s_whl_ff. now apply Bool.negb_true_iff.
      rewrite <-dotA. intros s s'' [? [<- H] [s' H' H'']]. apply s_whl_tt. assumption.
      econstructor. apply IHp, H'. assumption.
Qed.

Some program equivalences

two programs are said to be equivalent if they have the same semantics
Notation "p ~ q" := (bstep p ≡ bstep q) (at level 80).

ad-hoc simplification tactic
Ltac simp := unfold bstep; fold bstep.

denesting nested loops

Lemma two_loops b p:
  whl b (whl b p) ¬ whl b p.
Proof. simp. kat. Qed.

folding a loop

Lemma fold_loop b p:
  whl b (p ;; ite b p skp) ¬
  whl b p.
Proof. simp. kat. Qed.

eliminating deadcode

Lemma dead_code b p q r:
  (whl b p ;; ite b q r) ¬
  (whl b p ;; r).
Proof. simp. kat. Qed.

Lemma dead_code' a b p q r:
  (whl (a ⊔ b) p ;; ite b q r) ¬
  (whl (a ⊔ b) p ;; r).
Proof. simp. kat. Qed.

Reasoning about assignations

(higher-order style) substitution in formulas and expressions
Definition subst x v (A: dset state): dset state :=
  fun s ⇒ A (update x (v s) s).
Definition esubst x v (e: state → nat): state → nat :=
  fun s ⇒ e (update x (v s) s).

is x fresh in the expression e
Definition fresh x (e: state → nat) := ∀ v s, e (update x v s) = e s.

Hypothesis update_twice: ∀ x i j s, update x j (update x i s) = update x j s.
Hypothesis update_comm: ∀ x y i j s, x≠y → update x i (update y j s) = update y j (update x i s).

stacking assignations


Lemma aff_stack x e f:
  (x <- e ;; x <- f) ¬
  (x <- esubst x e f).
Proof.
  simp. rewrite frel_comp.
  apply frel_weq; intro s.
  apply update_twice.
Qed.

removing duplicates


Lemma aff_idem x e: fresh x e → (x <- e ;; x <- e) ¬ (x <- e).
Proof.
  intro. rewrite aff_stack.
  intros s s'. cbv. rewrite (H (e s)). tauto.
Qed.

commuting assignations


Lemma aff_comm x y e f: x≠y → fresh y e →
  (x <- e ;; y <- f) ¬ (y <- esubst x e f ;; x <- e).
Proof.
  intros Hx Hy. simp. rewrite 2frel_comp. apply frel_weq; intro s.
  rewrite update_comm by congruence.
  now rewrite (Hy _).
Qed.

delaying choices

in the above example, we cannot exploit KAT since this is just about assignations. In the following example, we show how to perform a mixed proof: once we assert that the test t somehow commutes with the assignation x<-e, hkat can make use of this assumption to close the goal

Lemma aff_ite x e t p q:
  (x <- e ;; ite t p q)
  ¬
  (ite (subst x e t) (x <- e ;; p) (x <- e ;; q)).
Proof.
  simp.
  assert (H: upd x e ⋅ [t] ≡ [subst x e t] ⋅ upd x e)
   by (cbv; firstorder; subst; eauto).
  hkat.
Qed.

Embedding Hoare logic for partial correctness

Hoare triples for partial correctness can be expressed really easily using KAT:
Notation Hoare A p B := ([A] ⋅ bstep p ⋅ [!B] ≦ 0).

correspondence w.r.t. the standard interpretation of Hoare triples

Lemma Hoare_eq A p B:
  Hoare A p B ↔
  ∀ s s', A s → bstep p s s' → B s'.
Proof.
  split.
  - intros H s s' HA Hp. case_eq (B s'). reflexivity. intro HB.
    destruct (H s s'). ∃ s'. ∃ s.
    now split. assumption. split. reflexivity. simpl. now rewrite HB.
  - intros H s s' [? [? [<- HA] Hp] [-> HB]]. simpl in HB.
    rewrite (H _ _ HA Hp) in HB. discriminate.
Qed.

deriving Hoare logic rules using the hkat tactic

Hoare triples are encoded as propositions of the shape x ≦ 0 ; therefore, they can always be eliminated by hkat, so that all rules of Hoare logic can be proved automatically (except for the assignation rule, of course)
This idea come from the following paper: Dexter Kozen. On Hoare logic and Kleene algebra with tests. Trans. Computational Logic, 1(1):60-76, July 2000.
The fact that we have an automatic tactic makes it trivial to formalise it.

Lemma weakening (A A' B B': dset state) p:
  A' ≦ A → Hoare A p B → B ≦ B' → Hoare A' p B'.
Proof. hkat. Qed.

Lemma rule_skp A: Hoare A skp A.
Proof. simp. kat. Qed.

Lemma rule_seq A B C p q:
  Hoare A p B →
  Hoare B q C →
  Hoare A (p;;q) C.
Proof. simp. hkat. Qed.

Lemma rule_ite A B t p q:
  Hoare (A ⊓ t) p B →
  Hoare (A ⊓ !t) q B →
  Hoare A (ite t p q) B.
Proof. simp. hkat. Qed.

Lemma rule_whl A t p:
  Hoare (A ⊓ t) p A →
  Hoare A (whl t p) (A ⊓ neg t).
Proof. simp. hkat. Qed.

Lemma rule_aff x v (A: dset state): Hoare (subst x v A) (x <- v) A.
Proof.
  rewrite Hoare_eq. intros s s' HA H.
  now inversion_clear H.
Qed.

Lemma wrong_rule_whl A t p:
  Hoare (A ⊓ !t) p A →
  Hoare A (whl t p) (A ⊓ !t).
Proof. simp. Fail hkat. Abort.

Lemma rule_whl' (I A: dset state) t p:
  Hoare (I ⊓ t) p I →
  I ⊓ !t ≦ A →
  Hoare I (whl t p) A.
Proof. eauto 3 using weakening, rule_whl. Qed.

End s.