Credits are now a linear resource

We can now have a negative number of credits (and this doesn't imply False), but
garbage-collection of resources has been restricted: only a positive number of
credits can be discarded.

lib/coq/CFApp.v

@@ -210,7 +210,7 @@ Qed.
 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 \*+ (Hexists H', H')) ->
+  (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.
@@ -223,10 +223,11 @@ 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. hsimpl~ \[].
+  Q ===> Q' ->
+  app f xs H Q'.
+Proof using.
+  introv M W. applys* app_wgframe. hsimpl. intros r.
+  hchange W. hsimpl.
 Qed.
 
 (* DEPRECATED

lib/coq/CFLibCredits.v

@@ -28,17 +28,14 @@ Implicit Types x y z : int.
 (********************************************************************)
 (** Additional lemmas on credits *)
 
-Definition credits_nat_eq := 
-  args_eq_1 heap_is_credits_nat. 
-  (* todo: state as a lemma instead *)
-
-Lemma credits_nat_zero_eq_prove : forall (n:nat),
-  n = 0%nat -> \$_nat n = \[].
-Proof. intros. subst. apply credits_nat_zero_eq. Qed.
+Lemma credits_eq : forall x y,
+  x = y ->
+  \$ x = \$ y.
+Proof. apply (args_eq_1 heap_is_credits). Qed.
 
 Lemma credits_int_zero_eq_prove : forall (x:int),
   x = 0 -> \$ x = \[].
-Proof. intros. subst. apply credits_int_zero_eq. Qed.
+Proof. intros. subst. apply credits_zero_eq. Qed.
 
 
 

lib/coq/CFTactics.v

@@ -505,6 +505,7 @@ Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 Ltac xgc_remove_hprop H :=
   eapply (@local_gc_pre_on H);
     [ try xlocal
+    | try affine
     | hsimpl
     | xtag_pre_post ].
 
@@ -557,6 +558,7 @@ Ltac xgc_post_if_not_evar_then cont :=
 
 Lemma local_gc_pre_all : forall B Q (F:~~B) H,
   is_local F ->
+  affine H ->
   F \[] Q ->
   F H Q.
 Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
@@ -1618,7 +1620,7 @@ Lemma xret_lemma : forall B (v:B) H (Q:B->hprop),
   local (fun H' Q' => H' ==> Q' v) H Q.
 Proof using.
   introv W. eapply (@local_gc_pre_on (\GC)).
-  auto. hchanges W. apply~ local_erase. hsimpl.
+  auto. affine. hchanges W. apply~ local_erase. hsimpl.
 Qed.
 
 (* Lemma used by [xret] and [xret_no_gc]
@@ -3832,15 +3834,11 @@ Tactic Notation "xname_post" ident(X) :=
     used before a credit split operation, e.g. to replace
     [$n] with [$a \* $b], when [n = a + b].
 
-    LATER: add demos for this tactic. 
+    LATER: add demos for this tactic.
   *)
 
 Ltac xcredit goal :=
   match goal with
-  | |- context[\$_nat goal] =>
-      idtac (* no need to rewrite *)
-  | |- context[\$_nat ?n] =>
-      math_rewrite (n = goal :> nat)
   | |- context[\$ goal] =>
       idtac (* no need to rewrite *)
   | |- context[\$ ?n] =>
@@ -3867,15 +3865,11 @@ Ltac xpay_start tt :=
 Ltac xpay_core tt :=
   xpay_start tt; [ unfold pay_one; hsimpl | ].
 
-Ltac xpay_nat_core tt :=
-  xpay_start tt; [ rewrite pay_one_nat; hsimpl | ].
-
 Tactic Notation "xpay" := xpay_core tt.
 
 Ltac xpay_on_impl goal :=
   xcredit goal;
-  first [ rewrite credits_int_split_eq 
-        | rewrite credits_nat_split_eq ];
+  first [ rewrite credits_split_eq ];
   xpay.
 
 Tactic Notation "xpay" constr(goal) :=
@@ -3913,12 +3907,22 @@ Tactic Notation "xpay_skip" := xpay_fake tt.
 Ltac xgc_credit_core HP :=
   let H := fresh in
   let E := fresh in
-  destruct (credits_nat_le_rest HP) as (H&E);
-  xchange E; [ chsimpl | xgc H; clear H E ].
+  destruct (credits_le_rest HP) as (H&HA&E);
+  xchange E; [ xgc H; clear H HA E; hclean ].
 
 Tactic Notation "xgc_credit" constr(HP) :=
   xgc_credit_core HP.
 
+Goal forall m n B (F : ~~B) Q,
+  m <= n ->
+  is_local F ->
+  F (\$m) Q ->
+  F (\$n) Q.
+Proof.
+  introv H L HH.
+  xgc_credit_core H.
+  assumption.
+Qed.
 
 (*--------------------------------------------------------*)
 (* ** [xskip_credits] *)

lib/stdlib/Array_proof.v

@@ -32,6 +32,10 @@ Parameter Array : forall A, list A -> loc -> hprop.
      the ownership of single cells, each of which being
      described using heap_is_single. *)
 
+Parameter Array_affine : forall A t (L: list A), affine (t ~> Array L).
+  (* TODO: prove this *)
+Hint Resolve Array_affine : affine.
+
 (* -------------------------------------------------------------------------- *)
 
 (* The length of an array is at most [Sys.max_array_length]. This could be

lib/stdlib/Pervasives_proof.v

@@ -260,6 +260,10 @@ Qed.
 Notation "r '~~>' v" := (hdata (Ref v) r)
   (at level 32, no associativity) : heap_scope.
 
+(* TODO: prove it and/or generalize wrt Heapdata *)
+Parameter Ref_affine : forall A r (v: A), affine (r ~~> v).
+Hint Resolve Ref_affine : affine.
+
 Lemma ref_spec : forall A (v:A),
   app ref [v]
     PRE \[]