Library CFML.CFApp

Set Implicit Arguments.
Require Import LibCore LibEpsilon Shared.
Require Import CFHeaps.

Hint Extern 1 (_ ===> _) => apply refl_rel_incl'.

CFML exports an axiomatic operation eval f v h v' h' which describes th e big-step evaluation of a one-argument function on the entire heap.

Based on eval, we define app_basic f x H Q, which is a like eval modulo frame and weakening and garbage collection.

On top of app_basic, we define app f xs H Q, which describes the evaluation of a call to f on the arguments described by the list xs.

We also define a predicate curried n f which asserts that the function f is a curried function with n arguments, hence its n-1 first applications are partial.

The characteristic formula generated for a function application f x y z is "app f x y z".

The characteristic formula generated for a function definition let f x y z = t is: curried 3 f /\ (forall x y z H Q, CF(t) H Q -> app f [x y z] H Q).

These definitions are correct and sufficient to reasoning about all function calls, including partial and over applications.

This file also contains axiomatization of record operations.

Note: these axioms could in theory be realized by constructing a deep embedding of the target programming language. See Arthur Chargueraud's PhD thesis for full details.

The type Func, used to represent functions

Axiom func : Type.

The type Func is inhabited

Axiom func_inhab : Inhab func.

Existing Instance func_inhab.

The evaluation predicate for functions: eval f v h v' h', asserts that the evaluation of the application of f to v in a heap h terminates and produces a value v' in a heap h'.

Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.

The primitive predicate app_basic, which makes a local version of eval.

Definition app_basic (f:func) A (x:A) B (H:hprop) (Q:B ->hprop) :=
  forall h i, \# h i -> H h ->
    exists v' h' g, \# h' g i /\ Q v' h' /\
      eval f x (h \+ i) v' (h' \+ g \+ i).

app_basic f x is a local formula

Lemma app_basic_local : forall A B f (x:A),
  is_local (@app_basic f A x B).
Proof using.
  asserts Hint1: (forall h1 h2, \# h1 h2 -> \# h2 h1).
    intros. auto.
  asserts Hint2: (forall h1 h2 h3, \# h1 h2 -> \# h1 h3 -> \# h1 (heap_union h2 h3 )).
    intros. rew_disjoint*.
  asserts Hint3: (forall h1 h2 h3, \# h1 h2 -> \# h2 h3 -> \# h1 h3 -> \# h1 h2 h3) .
    intros. rew_disjoint*.
  intros. hnf. extens. intros H Q. iff M. apply~ local_erase.
  introv Dhi Hh. destruct (M h Hh) as (H1&H2&Q'&D12&N&HQ).
  destruct D12 as (h1&h2&?&?&?&?).
  destruct~ (N h1 (heap_union i h2)) as (v'&h1'&i'&?&HQ'&E).
  subst h. rew_disjoint*.
  sets h': (heap_union h1' h2).
  forwards Hh': (HQ v' h'). subst h'. exists h1' h2. rew_disjoint*.
  destruct Hh' as (h3'&h4'&?&?&?&?).
  asserts Hint4: (forall h : heap, \# h h1' -> \# h h2 -> \# h h3').
    intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'.
     rew_disjoint*. rewrite H10 in K. rew_disjoint*.
  asserts Hint5: (forall h : heap, \# h h1' -> \# h h2 -> \# h h4').
    intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'.
     rew_disjoint*. rewrite H10 in K. rew_disjoint*.
  exists v' h3' (heap_union h4' i'). splits.
    subst h h'. rew_disjoint*.
    auto.
    subst h h'. rew_disjoint. intuition. applys_eq E 1 3.
      rewrite* <- heap_union_assoc. rewrite~ (@heap_union_comm h2).
      do 2 rewrite* (@heap_union_assoc h3'). rewrite <- H10.
      do 2 rewrite <- heap_union_assoc. fequal.
      rewrite heap_union_comm. rewrite~ <- heap_union_assoc. rew_disjoint*.
Qed.

Hint Resolve app_basic_local.

Local Notation "'Dyn' x" := (@dyn _ x) (at level 0).

Notation "[ x1 ]" := ((dyn x1)::nil)
  (at level 0, x1 at level 0) : dynlist.
Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
  (at level 0, x1 at level 0, x2 at level 0) : dynlist.
Notation "[ x1 x2 x3 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil)
  (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : dynlist.

Delimit Scope dynlist with dynlist.

Definition of app f xs, recursive. Can be written, e.g. Notation app f [x y z] H Q

Fixpoint app_def (f:func) (xs:list dynamic) {B} (H:hprop) (Q:B ->hprop) : Prop :=
  match xs with
  | nil => False
  | (dyn x)::nil => app_basic f x H Q
  | (dyn x)::xs =>
     app_basic f x H
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q ])
  end.

Notation "'app' f xs" :=
  (@app_def f (xs)%dynlist _)
  (at level 80, f at level 0, xs at level 0) : charac.
Open Scope charac.

app_keep f xs H Q is the same as app f xs H (Q \*+ H)

Notation "'app_keep' f xs H Q" :=
(app f xs H%h (Q \*+ H))
(at level 80, f at level 0, xs at level 0, H at level 0) : charac.

Reformulation of the definition

Lemma app_ge_2_unfold :
  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B ->hprop),
  (xs <> nil ) ->
    app f ((dyn x )::xs ) H Q
  = app_basic f x H
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q ]).
Proof using.
  intros. destruct xs. false. auto.
Qed.

Lemma app_ge_2_unfold' :
  forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B ->hprop),
  (length xs >= 1)%nat ->
    app f ((dyn x )::xs ) H Q
  = app_basic f x H
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q ]).
Proof using.
  intros. rewrite~ app_ge_2_unfold. destruct xs; rew_list in *.
  math.
  introv N. false.
Qed.

Lemma app_ge_2_unfold_extens :
  forall (f:func) A (x:A) (xs:list dynamic) B,
  (xs <> nil ) ->
    app_def f ((dyn x )::xs) (B:=B)
  = (fun H Q => app_basic f x H
       (fun g => Hexists H', H' \* \[ app_def g xs H' Q ])).
Proof using.
  introv N. applys fun_ext_2. intros H Q. rewrite~ app_ge_2_unfold.
Qed.

Weaken-frame-gc for app -- auxiliary lemma for app_local.

Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B ->hprop),
  app f xs H1 Q1 ->
  H ==> (H1 \* H2 ) ->
  (Q1 \*+ H2 ) ===> (Q \*+ \GC ) ->
  app f xs H Q.
Proof using.
  intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false.
  tests E: (xs = nil).
    simpls. applys~ local_frame_gc M.
    rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
     applys~ local_frame M. intros g.
     hpull as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
Qed.

Lemma app_weaken : forall B f xs H (Q Q':B ->hprop),
  app f xs H Q ->
  Q ===> Q' ->
  app f xs H Q'.
Proof using.
  introv M W. applys* app_wgframe. hsimpl. intros r.
  hchange W. hsimpl.
Qed.

Local property for app

Lemma app_local : forall f xs B,
  xs <> nil -> is_local (app_def f xs (B:=B)).
Proof using.
  introv N. apply is_local_prove. intros H Q.
  destruct xs as [|[A1 x1] xs]; tryfalse.
  destruct xs as [|[A2 x2] xs].
  { simpl. rewrite~ <- app_basic_local. iff*. }
  { rewrite app_ge_2_unfold_extens; auto_false.
    iff M.
    apply local_erase. auto.
    rewrite app_basic_local.
    intros h Hh. specializes M Hh.
    destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits.
    eauto. eauto.
    intros g. hpull as H' L. hsimpl (H' \* H2).
    applys app_wgframe L. hsimpl. hchange R3. hsimpl. }
Qed.

Hint Resolve app_local.

curried n f asserts that n-1 first applications of f are total

Fixpoint curried (n:nat) (f:func) : Prop :=
  match n with
  | O => False
  | S O => True
  | S n => forall A (x:A),
     app_basic f x \[]
       (fun g => \[ curried n g
          /\ forall xs B H (Q:B ->hprop), length xs = n ->
               app f ((dyn x )::xs ) H Q -> app g xs H Q ])
  end.

Unfolding lemma for curried

Lemma curried_ge_2_unfold : forall n f,
  (n > 1)%nat ->
    curried n f
  = forall A (x:A), app_basic f x \[]
    (fun g => \[ curried (pred n) g
                 /\ forall xs B H (Q:B ->hprop), length xs = (pred n ) ->
                       app f ((dyn x )::xs ) H Q -> app g xs H Q ]).
Proof using.
  introv N. destruct n. math. destruct n. math. auto.
Qed.

app f (xs++ys) can be expressed as app f xs that returns a function g such that the behavior is that of app g ys.

Lemma app_over_app : forall xs ys f B H (Q:B ->hprop),
  (length xs > 0)%nat -> (length ys > 0)%nat ->
    app f (xs ++ys ) H Q
  = app f xs H (fun g => Hexists H', H' \*
                                   \[ app g ys H' Q ]).
Proof using.
  induction xs. rew_list. math. introv N1 N2. rew_list.
  destruct a as [A x].
  destruct xs.
    rew_list. simpl. destruct ys. rew_list in *. math. auto.
  sets_eq xs': (d :: xs). do 2 (rewrite app_ge_2_unfold;
   [ | subst; rew_list; auto_false ]).
  fequal. apply fun_ext_1. intros g.
  apply args_eq_1. auto. apply fun_ext_1. intros H'.
  fequal. fequal. apply IHxs. subst. rew_list. math. math.
Qed.

Alternative formulation

Lemma app_over_take : forall n xs f B H (Q:B ->hprop),
  (0 < n < length xs)%nat ->
    app f xs H Q
  = app f (take n xs ) H (fun g => Hexists H', H' \*
                                   \[ app g (drop n xs ) H' Q ]).
Proof using.
  introv N.
  forwards* (M&E1&E2): take_app_drop_spec n xs. math.
  set (xs' := xs) at 1. change xs with xs' in M. rewrite M.
  subst xs'. rewrite app_over_app; try math. auto.
Qed.

When curried n f holds and the number of the arguments xs is less than n, then app f xs is a function g such that app g ys has the same behavior as app f (xs++ys).

Lemma app_partial : forall n xs f,
  curried n f -> (0 < length xs < n)%nat ->
  app f xs \[] (fun g => \[
    curried (n - length xs)%nat g /\
    forall ys B H (Q:B ->hprop), (length xs + length ys = n)%nat ->
      app f (xs ++ys ) H Q -> app g ys H Q ]).
Proof using.
  intros n. induction_wf IH: lt_wf n. introv C N.
  destruct xs as [|[A x] zs]. rew_list in N. math.
  rewrite curried_ge_2_unfold in C; [|math].
  tests E: (zs = nil).
  { unfold app_def at 1. eapply local_weaken_post. auto. applys (rm C).
    intros g. hpull as [M1 M2]. hsimpl. split.
      rew_list. applys_eq M1 2. math.
      introv E AK. rew_list in *. applys M2. math. auto. }
  { asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. }
    rew_list in N. rewrite~ app_ge_2_unfold.
    eapply local_weaken_post. auto. applys (rm C). clear C.     intros h. hpull as [M1 M2]. hsimpl.
    applys app_weaken. applys (rm IH) M1. math. math. clear IH.
    intros g. hpull as [N1 N2]. hsimpl. split.
    { rew_list. applys_eq N1 2. math. }
    { introv P1 P2. rew_list in P1.
      applys N2. math.
      applys M2. rew_list; math.
      rew_list in P2. applys P2. } }
Qed.

spec f n P asserts that curried f n is true and that the proposition P is a valid specification for f. This formulation is useful for conciseness and tactics.

Definition spec (f:func) (n:nat) (P:Prop) :=
curried n f /\ P.

Global Opaque app_def curried.

Representation predicate r ~> record_repr L, where L is an association list from fields (natural numbers) to dependent pairs (a value accompanied with its type).

Definition record_descr := list (field * dynamic).

Definition record_repr_one (f:field) A (v:A) (r:loc) : hprop :=
  heap_is_single r f v.

Lemma affine_record_repr_one : forall f A (v:A) r,
  affine (record_repr_one f v r).
Proof.
  intros. unfold record_repr_one. affine.
Qed.

Hint Transparent field : affine.
Hint Resolve affine_record_repr_one : affine.

Fixpoint record_repr (L:record_descr) (r:loc) : hprop :=
  match L with
  | nil => \[]
  | (f, dyn v)::L' => r ~> record_repr_one f v \* r ~> record_repr L'
  end.

Lemma affine_record_repr : forall L r,
  affine (record_repr L r).
Proof.
  induction L as [| [? [? ?]] ?]; intros; simpl; affine.
Qed.

Hint Transparent record_descr : affine.
Hint Resolve affine_record_repr : affine.

Definition app_record_new (L:loc -> record_descr) : ~~loc :=
  local (fun H Q => (fun r => H \* r ~> record_repr (L r)) ===> Q).

Axiom record_get : func.

Axiom record_get_spec : forall (r:loc) (f:field) A (v:A),
  app_keep record_get [r f ]
    (r ~> record_repr_one f v )
    \[= v ].

Axiom record_set : func.

Axiom record_set_spec : forall (r:loc) (f:field) A B (v:A) (w:B),
  app record_set [r f w ]
    (r ~> record_repr_one f v)
    (# r ~> record_repr_one f w).

Notation for the contents of the fields

Notation "`{ f1 := x1 }'" :=
  ((f1, dyn x1)::nil)
  (at level 0, f1 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::nil)
  (at level 0, f1 at level 0, f2 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::(f7, dyn x7)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0, f7 at level 0)
  : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }'" :=
  ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::
   (f6, dyn x6)::(f7, dyn x7)::(f8, dyn x8)::nil)
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
  : record_scope.

Delimit Scope record_scope with record.
Open Scope record_scope.

Notation "'rec' L" :=
  (@record_repr (L)%record)
  (at level 69) : charac.

Open Scope charac.

Notation for characteristic formulae

Notation "`{ f1 := x1 }" :=
  (rec `{ f1 := x1 }')
  (at level 0, f1 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 }" :=
  (rec `{ f1 := x1 ; f2 := x2 }')
  (at level 0, f1 at level 0, f2 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5;
  f6 := x6 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5;
   f6 := x6 ; f7 := x7 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0, f7 at level 0)
  : charac.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }" :=
  (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5;
   f6 := x6 ; f7 := x7 ; f8 := x8 }')
  (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
   f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
  : charac.

Fixpoint record_get_compute_dyn (f:field) (L:record_descr) : option dynamic :=
  match L with
  | nil => None
  | (f',d')::T' =>
     if Nat.eq_dec f f'
       then Some d'
       else record_get_compute_dyn f T'
  end.

Definition record_get_compute_spec (f:field) (L:record_descr) : option Prop :=
  match record_get_compute_dyn f L with
  | None => None
  | Some (dyn v) => Some (forall r,
     app_keep record_get [r f ] (r ~> record_repr L ) \[= v])
  end.

Lemma record_get_compute_spec_correct : forall f L (P:Prop),
  record_get_compute_spec f L = Some P -> P.
Proof using.
  introv M. unfolds record_get_compute_spec.
  sets_eq <- do E: (record_get_compute_dyn f L).
  destruct do as [[T v]|]; inverts M.
  induction L as [|[f' [D' d']] T']; [false|].
  simpl in E.
  intros r. do 2 xunfold record_repr at 1. simpl. case_if in E.   { subst. inverts E.
    eapply local_frame.
    { apply app_local. auto_false. }
    { apply record_get_spec. }
    { hsimpl. }
    { hsimpl~. } }
  { specializes IHT' (rm E).
    eapply local_frame.
    { apply app_local. auto_false. }
    { apply IHT'. }
    { hsimpl. }
    { hsimpl~. } }
Qed.
Fixpoint record_set_compute_dyn (f:field) (d:dynamic) (L:record_descr) : option record_descr :=
  match L with
  | nil => None
  | (f',d')::T' =>
     if Nat.eq_dec f f'
       then Some ((f ,d )::T')
       else match record_set_compute_dyn f d T' with
            | None => None
            | Some L' => Some ((f',d')::L')
            end
  end.

Definition record_set_compute_spec (f:field) A (w:A) (L:record_descr) : option Prop :=
  match record_set_compute_dyn f (dyn w) L with
  | None => None
  | Some L' => Some (forall r,
     app record_set [r f w ] (r ~> record_repr L) (# r ~> record_repr L'))
  end.

Lemma record_set_compute_spec_correct : forall f A (w:A) L (P:Prop),
  record_set_compute_spec f w L = Some P -> P.
Proof using.
  introv M. unfolds record_set_compute_spec.
  sets_eq <- do E: (record_set_compute_dyn f (dyn w) L).
  destruct do as [L'|]; inverts M.
  gen L'. induction L as [|[f' [T' v']] T]; intros; [false|].
  simpl in E.
  xunfold record_repr at 1. simpl. case_if.   { subst. inverts E.
    eapply local_frame.
    { apply app_local. auto_false. }
    { apply record_set_spec. }
    { hsimpl. }
    { xunfold record_repr at 2. simpl. hsimpl~. } }
  { cases (record_set_compute_dyn f Dyn (w) T) as C'; [|false].
    inverts E. specializes~ IHT r.
    eapply local_frame.
    { apply app_local. auto_false. }
    { apply IHT. }
    { hsimpl. }
    { xunfold record_repr at 2. simpl. hsimpl~. } }
Qed.

Global Opaque record_repr.