Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import DFS_ml.
Require Import Stdlib.
Require Import TLC.LibListZ.
Require Import Array_proof.
Require Import List_proof.
Require Import DFS_proof.
Open Scope tag_scope.


(*************************************************************************)
(** Verification of a minimal stack *)

Module Import Stack_proof.
Import Stack_ml.

Definition Stack A (L:list A) (p:loc) :=
  p ~~> L.

Lemma create_spec : forall A,
  app create [tt]
     PRE \[]
     POST (fun p => p ~> Stack (@nil A)).
Proof using. xcf_go. Qed.

Hint Extern 1 (RegisterSpec create) => Provide create_spec.

Lemma is_empty_spec : forall A (L:list A) (p:loc),
  app is_empty [p]
     INV (p ~> Stack L)
     POST (fun b => \[b = isTrue (L = nil)]).
Proof using. xcf_go*. xpolymorphic_eq. (* todo: automate *) Qed.

Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.

Lemma pop_spec : forall A (L:list A) (p:loc),
  L <> nil ->
  app pop [p]
     PRE (p ~> Stack L)
     POST (fun x => Hexists L', \[L = x::L'] \* p ~> Stack L').
Proof using. xcf_go*. Qed.

Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.

Lemma push_spec : forall A (L:list A) x p,
  app push [x p]
     PRE (p ~> Stack L)
     POST (# p ~> Stack (x::L)).
Proof using. xcf_go*. Qed.

Hint Extern 1 (RegisterSpec push) => Provide push_spec.

End Stack_proof.


(*************************************************************************)
(** Proof of DFS with a stack *)

(* Note: [E] describes set of edges left to process in the loop *)

(* - [L] describes the contents of the stack 
   - [a] describes the source
   - [n] describes the number of nodes in [G]
   - [E] describes a set of vertices: the neighbors of the currently processed vertex *)

Record inv (G:graph) (n:int) (a:int) (C:list bool) (L:list int) (E:set int) := {
  inv_length_C : length C = n;
  inv_source : C[a] = true;
  inv_stack : forall i, mem i L -> i \in nodes G /\ C[i] = true;
  inv_true_reachable : forall i, i \in nodes G ->
    C[i] = true -> reachable G a i;
  inv_true_edges : forall i j,
    C[i] = true -> has_edge G i j ->
    mem i L \/ C[j] = true \/ j \in E }.

Lemma inv_init : forall G n a C,
  C = LibListZ.make n false -> 
  a \in nodes G ->
  inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
  introv EC Ga. constructors.
  { skip. }
  { skip. }
  { introv H. inverts H as H. skip. inverts H. }
  { introv Gi H. skip_rewrite (i = a).
   exists (nil:path). constructors*. }
  { introv Ci E. skip_rewrite (i = a). left*. }
Qed.

Lemma inv_step_push : forall G n a C L i j js,
  inv G n a C L ('{j} \u js) ->
  C[i] = true -> 
  has_edge G i j ->
  inv G n a (C[i:=true]) (i :: L) js.
Proof.
  introv I Ci M. inverts I. constructors.
  { skip. }
  { skip. }
  { intros i' M'. skip. }
  { skip. (*  extend path with edge at end *) }
  { intros i' j' Ci' E. 
  (* two cases: i is i' or not. If so, wrote true *)
  skip. }
Qed.

Lemma inv_step_skip : forall G n a C L j js,
  inv G n a C L ('{j} \u js) -> 
  C[j] = true ->
  inv G n a C L js.
Proof.
  introv I Cj. inverts I. constructors; auto.
  { intros i' j' Ci' E.
    lets [M|[M|M]]: inv_true_edges0 Ci' E; [ eauto | eauto | ].
    rew_set in M. destruct~ M. subst*. }
Qed.

Lemma inv_end : forall G n a C,
  inv G n a C nil \{} ->
  forall j, j \in nodes G ->
  (reachable G a j <-> C[j] = true).
Proof.
  introv I Gj. iff H.
  { destruct H as [p P]. lets PC: inv_source I. gen P PC.
   generalize a as i. intros i P. induction P.
     { auto. }
     { introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H.
       { inverts M. }
       { auto. }
       { inverts M. } } }
  { applys* inv_true_reachable. }
Qed.

Lemma reachable_imperative_spec : forall g G a b,
  a \in nodes G -> 
  b \in nodes G ->
  app reachable_imperative [g a b]
    INV (g ~> RGraph G) 
    POST (fun (r:bool) => \[r = isTrue (reachable G a b)]).
Proof.
  introv Ga Gb. xcf.
  xapp. intros Gn. xapp. { skip. (* index *) }
  intros C0 HC0.
  xapp. xapp*. xseq. xapp.
  set (hinv := fun E CL =>
    let '(C,L) := CL in
       g ~> RGraph G
    \* c ~> Array C
    \* s ~> Stack L
    \* \[inv G n a C L E]).
  (* TODO: fix termination
    set (W := lexico2 (binary_map (count (= true)) (upto n))
                    (binary_map (fun L:list int => LibList.length L) (downto 0))). *)
  set (K := (fun CL => bool_of (let '(C,L) := CL : array bool * list int in
     L <> nil))).
  xseq (# Hexists C, hinv \{} (C,nil)).
  xwhile_inv_skip (fun (b:bool) => Hexists C L, hinv \{} (C,L) \* \[b = isTrue (L<>nil)]).
  (* TODO: xwhile_inv_basic (hinv \{}) W *) 
  { unfold hinv.
    evar (X:list bool); evar (Y:list int); hsimpl (X,Y); subst X Y; eauto. 
    apply* inv_init. }
  { intros S LS r HS. xpull ;=> C L I Er. (* TODO: why is hinv unfolded ?*)
    (* while condition *)
    xlet. xapps. xret. xpull ;=> E. 
    (* todo: simplify E *)
    xif.
    { (* case loop step *)
       xseq. xapp*. intros L' HL'. subst L.
       xfun as f. forwards~ [Gi Ci]: inv_stack I i.   
       xapp (fun E => Hexists CL, hinv E CL) G.
       { auto. }
       { unfold hinv. intros. skip. (* applys heap_contains_intro. *) }
       { introv N Hij. xpull. intros (C2&L2). xapp_spec Sf.
         skip. (* loop *)  }
       { skip. (* unfold hinv. hsimpl (C,L'). *) }
       { skip. }
       { skip. (*  xapplys HS. *) }
      (* Notes...
             { intros E. xapp_body. clear Sf. intros ?. intro_subst.
              clears W K C. clears L'. unfold hinv at 1. xextract. intros [C L]. xextract as I.
              xapps. skip. xif.
                xapp*. skip. xapp. unfold hinv. hsimpl (C[i:=true],i::L).
                 applys inv_step_push. eauto. skip. (* come from pop of L' *) eauto.
                xret. unfold hinv. hsimpl (C,L). apply* inv_step_skip. *)
    } 
    { (* case loop end *)
      xret. subst L. hsimpl*. { rew_bool_eq*. } } }
  { intros r. hpull ;=> C L E. rew_bool_eq in *. subst L. hsimpl C. }
  { clear hinv K. intros C I. lets: inv_length_C I.
    xapp*. hsimpl. skip. (* TODO affine *) 
    forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. }
Admitted.