Require Import Arith List Omega.


(** * Everyone's favorite 'while' language *)

Definition var := nat.
Definition state := var -> nat.
Definition upd (s : state) (v : var) (n : nat) : state :=
  fun v' => if eq_nat_dec v' v then n else s v'.

Inductive exp : Type :=
| Var : var -> exp
| Const : nat -> exp
| Plus : exp -> exp -> exp
| Minus : exp -> exp -> exp.

Definition pred := state -> Prop.

Inductive prog : Type :=
| Assign : var -> exp -> prog
| Seq : prog -> prog -> prog
| If0 : exp -> prog -> prog -> prog
| WhileNot0 : pred -> exp -> prog -> prog.

(** An example program: Multiplication of variables 0 and 1 into variable 3 *)

Definition mult := Seq (Assign 2 (Var 1))
  (Seq (Assign 3 (Const 0))
    (WhileNot0 (fun st => st 0 * st 1 = st 3 + st 0 * st 2)
      (Var 2)
      (Seq (Assign 3 (Plus (Var 3) (Var 0)))
        (Assign 2 (Minus (Var 2) (Const 1)))))).

(** ** A semantics for the language *)

Fixpoint eval (e : exp) (st : state) : nat :=
  match e with
    | Var v => st v
    | Const n => n
    | Plus e1 e2 => eval e1 st + eval e2 st
    | Minus e1 e2 => eval e1 st - eval e2 st
  end.

Inductive exec : prog -> state -> state -> Prop :=
| ExAssign : forall v e st,
  exec (Assign v e) st (upd st v (eval e st))
| ExSeq : forall p1 p2 st st' st'',
  exec p1 st st'
  -> exec p2 st' st''
  -> exec (Seq p1 p2) st st''
| ExIf0 : forall e p1 p2 st st',
  eval e st = 0
  -> exec p1 st st'
  -> exec (If0 e p1 p2) st st'
| ExIfS : forall e p1 p2 st st',
  eval e st <> 0
  -> exec p2 st st'
  -> exec (If0 e p1 p2) st st'
| ExWhile0 : forall inv e p1 st,
  eval e st = 0
  -> exec (WhileNot0 inv e p1) st st
| ExWhileS : forall inv e p1 st st' st'',
  eval e st <> 0
  -> exec p1 st st'
  -> exec (WhileNot0 inv e p1) st' st''
  -> exec (WhileNot0 inv e p1) st st''.

(** ** Verification condition generation *)

Fixpoint vc (pre : pred) (p : prog) : pred * Prop :=
  match p with
    | Assign v e => (fun st => exists st', pre st' /\ st = upd st' v (eval e st'),
      True)
    | Seq p1 p2 =>
      let (post1, vc1) := vc pre p1 in
        let (post2, vc2) := vc post1 p2 in
          (post2, vc1 /\ vc2)
    | If0 e p1 p2 =>
      let (post1, vc1) := vc (fun st => pre st /\ eval e st = 0) p1 in
        let (post2, vc2) := vc (fun st => pre st /\ eval e st <> 0) p2 in
          (fun st => post1 st \/ post2 st, vc1 /\ vc2)
    | WhileNot0 inv e p1 =>
      let (post1, vc1) := vc (fun st => inv st /\ eval e st <> 0) p1 in
        (fun st => inv st /\ eval e st = 0, vc1
          /\ (forall st, pre st -> inv st)
          /\ (forall st, post1 st -> inv st))
  end.

Theorem vc_correct : forall p st st', exec p st st'
  -> forall pre, (let (post, vc) := vc pre p in
    pre st -> vc -> post st').
  induction 1; simpl in *; intuition;
    repeat match goal with
             | [ |- context[vc ?pre ?p] ] =>
               repeat match goal with
                        | [ IH : forall pre : pred, match vc pre p with (_, _) => _ end |- _ ] =>
                          specialize (IH pre)
                      end;
               destruct (vc pre p)
           end; firstorder.
Qed.

(** ** Verifying multiplication *)

(** Two useful lemmas about arithmetic *)

Lemma decrement : forall x u v w,
  x = w + u * v
  -> v <> 0
  -> x = w + u + u * (v - 1).
  destruct v; simpl; intuition; subst;
    rewrite <- minus_n_O; ring.
Qed.

Lemma mult0 : forall u v w x,
  v = x + u * w
  -> w = 0
  -> x = v.
  intros; subst; ring.
Qed.

Hint Immediate decrement mult0.

(** The verification itself *)

Theorem multOk : forall st st', exec mult st st'
  -> st' 3 = st' 0 * st' 1.
  intros;
    match goal with
      | [ H : exec _ _ _ |- _ ] =>
        generalize (vc_correct _ _ _ H (fun _ => True)); simpl; intuition
    end;
    match goal with
      | [ H : _ -> _ |- _ ] => destruct H; firstorder; subst; unfold upd; simpl
    end; eauto.
Qed.


(** * A toy separation logic *)

(** The type of basic separation logic formulas *)
Parameter atomicFormula : Type.

(** The type of n-ary separating conjunctiosn of atomic formulas *)
Definition formula := list atomicFormula.

(** What it means for one formula to imply another, in any state *)
Parameter imply : formula -> formula -> Prop.

(** A trivial case of reflexivity *)
Axiom done : imply nil nil.

(** A principle for crossing out a formula on both sides of an implication *)
Axiom cancel : forall pre1 p1 post1 pre2 p2 post2,
  p1 = p2
  -> imply (pre1 ++ post1) (pre2 ++ post2)
  -> imply (pre1 ++ p1 :: post1) (pre2 ++ p2 :: post2).

Ltac cancel :=
  match goal with
    | [ |- imply ?ls1 ?ls2 ] =>
      let rec loop1 pre1 post1 :=
        match post1 with
          | ?p :: ?post1 =>
            let rec loop2 pre2 post2 :=
              match post2 with
                | ?p' :: ?post2 => (apply (cancel (rev pre1) p post1 (rev pre2) p' post2); [
                  solve [ eauto ] | simpl] )
                  || loop2 (p' :: pre2) post2
              end in
              loop2 (@nil atomicFormula) ls2
              || loop1 (p :: pre1) post1
        end in
        loop1 (@nil atomicFormula) ls1
  end.

Ltac sep := intros; repeat cancel; try apply done.

Theorem ex1 : forall (P Q R S : atomicFormula),
  imply (P :: Q :: R :: S :: nil) (S :: R :: P :: Q :: nil).
  sep.
Qed.

(** A principle for expanding a definition *)
Definition implyEx T ps1 ps2 := exists v : T, imply ps1 (ps2 v).

Axiom expand : forall p pre1 post1 T' ps2 T ps,
  implyEx T (p :: nil) ps
  -> (forall v : T, implyEx T' (pre1 ++ ps v ++ post1) ps2)
  -> implyEx T' (pre1 ++ p :: post1) ps2.

(** Some atomic predicates *)
Definition addr := nat.
Parameter ptsTo : addr -> nat -> atomicFormula.
Parameter linkedList : addr -> atomicFormula.

(** Two basic expansion laws for linked lists *)

Axiom linkedListEmpty : forall a,
  a = 0
  -> implyEx unit (linkedList a :: nil) (fun _ => nil).

Axiom linkedListNonempty : forall a,
  a <> 0
  -> implyEx (nat * addr) (linkedList a :: nil)
    (fun p => ptsTo a (fst p) :: ptsTo (a+1) (snd p) :: linkedList (snd p) :: nil).

Hint Resolve linkedListEmpty linkedListNonempty : expand.

Hint Extern 1 (_ = _) => omega.
Hint Extern 1 (_ <> _) => omega.

Ltac expand :=
  match goal with
    | [ |- implyEx _ ?ls _ ] =>
      let rec loop pre post :=
        match post with
          | ?p :: ?post =>
            (eapply (expand p (rev pre) post); [
              solve [ eauto with expand ]
              | simpl; intro ])
            || loop (p :: pre) post
        end in
        loop (@nil atomicFormula) ls
  end.

Theorem exists_pair : forall T1 T2 (f : T1 * T2 -> Prop),
  (exists x, exists y, f (x, y))
  -> ex f.
  firstorder.
Qed.

Ltac sep' := intros; repeat expand; try apply exists_pair; simpl; repeat eexists;
  repeat cancel; try apply done.

Theorem ex2 : forall a1 v n a2,
  a1 + 1 - 1 > 6
  -> a2 = a2 - 2
  -> implyEx (nat * addr)
  (linkedList a1 :: ptsTo v n :: linkedList a2 :: nil)
  (fun p => ptsTo v n :: linkedList (snd p) :: ptsTo a1 (fst p) :: ptsTo (a1+1) (snd p) :: nil).
  sep'.
Qed.