Merge branch 'dev'

Conflicts:
	AppendOnlyLinkedList.v

Author: csgordon

AppendOnlyLinkedList.v

@@ -27,7 +27,9 @@ Obligation Tactic :=
 Require Import Coq.Program.Tactics.
 
 Global Instance appList_fold : rel_fold appList :=
-  { rgfold := fun R G => appList }. (* TODO: This is technically unsound - need to recursively rewrite tail pointer relations... *)
+  { rgfold := fun R G => appList ; (* TODO: This is technically unsound - need to recursively rewrite tail pointer relations... *)
+    fold := fun R G x => x
+  }.
 
 Global Instance appList_contains : Containment appList. Admitted.
  (* want something like { contains := fun RR => RR = (optset ...) }. but need to handle cons/option shifting *)
@@ -48,7 +50,15 @@ Program Definition alist_append {Γ}(n:nat)(l:alist) : rgref Γ unit Γ :=
                                           | rcons n' tl' => rec tl'
                                         end)
                         end _))) l.
-Next Obligation. compute in *. rewrite H. constructor. Qed. 
+Next Obligation.
+  (* This proof is by no means ideal.  It only works because we can assume
+     that appList_fold's identity behavior matches meta_fold, which is useful
+     but very specific, and won't be true in many cases we care about. *)
+  erewrite deref_conversion with (f' := @meta_fold (option appList)) in *.
+  rewrite H.
+  constructor. 
+  Grab Existential Variables. eauto. eauto.
+Qed. 
 
 Program Example test1 {Γ} : rgref Γ unit Γ :=
   l <- Alloc None;

KnownUnsoundnessExamples.v

@@ -28,8 +28,19 @@ Program Definition BAD_alist_append {Γ}(n:nat)(l:alist) : rgref Γ unit Γ :=
                                           | rcons n' tl' => rec tl'
                                         end)
                         end))) l.
-Next Obligation. compute in Heq_anonymous. compute. rewrite <- Heq_anonymous. constructor. Qed.  
-Next Obligation. compute in *. rewrite <- Heq_anonymous. constructor. Qed.
+Next Obligation. 
+  erewrite deref_conversion with (f' := @meta_fold (option appList)) in *.
+  rewrite <- Heq_anonymous.
+  constructor. 
+  Grab Existential Variables. eauto. eauto.
+Qed.  
+Next Obligation. 
+  erewrite deref_conversion with (f' := @meta_fold (option appList)) in *.
+  rewrite <- Heq_anonymous.
+  constructor. 
+  Grab Existential Variables. eauto. eauto.
+Qed.  
+
 (** The specific issue with this example is that using a match inside a Program Definition
     adds an equality proof to the context for goals inside the match clauses.  In this case,
     in the None branch of the match, the assumption << !tl=None >> is added to the context.

LinkedList.v

@@ -233,7 +233,8 @@ Hint Resolve precise_prepend.
 (* Folding anything into this list container is a no-op: the head already points to a rgrList' with guarantee list_imm,
    so no further restriction is necessary / possible. *)
 Instance lst_cont_fold {P Q}: rel_fold (@list_container P Q) := {
-  rgfold := (fun R => fun G => @list_container P Q)
+  rgfold := (fun R => fun G => @list_container P Q) ;
+  fold := fun _ _ x => x
 }.
 
 Require Import Coq.Program.Tactics.

MonotonicCounter.v

@@ -24,4 +24,4 @@ Program Definition mkCounter { Γ } (u:unit) : rgref Γ monotonic_counter Γ :=
 
 Program Example test_counter { Γ } (u:unit) : rgref Γ unit Γ :=
   x <- mkCounter tt;
-  inc_monotonic x.
+  inc_monotonic x.

PosMonotonicCounter.v

@@ -0,0 +1,30 @@
+Require Import Coq.Arith.Arith.
+Require Import RGref.DSL.DSL.
+
+(** * A Strictly Positive Monotonic Counter
+   A monotonically increasing non-zero counter.
+   A slightly better basic example than the plain monotonic counter since this one has a nontrivial refinement. *)
+
+Definition increasing : hrel nat := (fun n n' _ _ => n <= n').
+Hint Unfold increasing.
+
+Definition pos : hpred nat := (fun n _ => n > 0).
+
+(** We'll give the Program extension some hints for this module *)
+Local Obligation Tactic := intros; eauto with arith; compute; eauto with arith.
+
+(** Now the definition of a verified monotonically increasing counter is
+    barely more work than a completely unchecked counter. *)
+Program Definition posmonotonic_counter := ref{nat|pos}[increasing,increasing].
+
+Program Definition read_counter (c:posmonotonic_counter) : nat := !c.
+
+Program Definition inc_monotonic { Γ } (p:posmonotonic_counter) : rgref Γ unit Γ :=
+  [p]:= !p + 1.
+
+Program Definition mkCounter { Γ } (u:unit) : rgref Γ posmonotonic_counter Γ :=
+  Alloc 1.
+
+Program Example test_counter { Γ } (u:unit) : rgref Γ unit Γ :=
+  x <- mkCounter tt;
+  inc_monotonic x.

RGref/DSL/Core.v

@@ -117,7 +117,9 @@ Definition precise_rel {A:Set}{AR:ImmediateReachability A} (R:hrel A) :=
     is essentially a no-op.  The guarantee, however, still needs to be
     projected and intersected component-wise in any structure. *)
 Class rel_fold (A:Set) :=
-  { rgfold : forall (R G:hrel A), Set }.
+  { rgfold : forall (R G:hrel A), Set ;
+    fold : forall {R G}, A -> rgfold R G
+  }.
 (** In meta-proofs, of things like satisfying a guarantee, we use this
     identity fold instead of the appropriate developer instance so
     G and P don't have to have polymorphic arities and relation arguments
@@ -126,7 +128,9 @@ Class rel_fold (A:Set) :=
 *)
 Section HideMetaFold.
 Local Instance meta_fold {A:Set} : rel_fold A :=
-  { rgfold := fun R G => A }.
+  { rgfold := fun R G => A ;
+    fold := fun _ _ x => x
+  }.
 End HideMetaFold.
 Notation "{{{ e }}}" := (let mfold : forall A, rel_fold A := @meta_fold in e) (at level 50).
 
@@ -153,6 +157,16 @@ Axiom deref : forall {A:Set}{B:Set}`{rel_fold A}{P:hpred A}{R G:hrel A}, hreflex
 (*Axiom deref : forall {A:Set}{P:hpred A}{R G:hrel A}, ref A P R G -> A.*)
 Notation "! e" := (deref _ _ e) (at level 30). (* with reflexivity, add an _ in there *)
 
+(* This axiom asserts that all folds that produce the same result type operate equally on
+   the underlying values. This is fragile if a developer specifies multiple instances for
+   folding the same type.  This is a weaker version of a more general axiom that
+   the relationship between the results of folds of different result types depends on the
+   relationship between results of the fold members of the instances when applied to the
+   same value.  This version is really only useful for equating identity folds with
+   the identity meta_fold instance results. *)
+Axiom deref_conversion : forall (A B:Set)(f f':rel_fold A) P R G  rf1 rf2 fe1 fe2,
+                         @deref A B f P R G rf1 fe1 = @deref A B f' P R G rf2 fe2.
+
 Axiom ptr_eq_deref : forall A P P' R R' G G' h (p:ref{A|P}[R,G]) (r:ref{A|P'}[G',R']), p≡r -> h[p]=h[r].
 Hint Resolve ptr_eq_deref.
 Axiom ptr_eq_update : forall A P P' R R' G G' (p:ref{A|P}[R,G]) (r:ref{A|P'}[G',R']),
@@ -215,16 +229,24 @@ Global Instance ref_contains {A:Set}{P:hpred A}{R G:hrel A} : Containment (ref{A
 
 (** ** Relation Folding *)
 Definition const_rel_fold (A:Set) (R G:hrel A) : Set := A.
-Global Instance nat_fold : rel_fold nat := {rgfold := const_rel_fold nat}.
-Global Instance bool_fold : rel_fold bool := {rgfold := const_rel_fold bool}.
-Global Instance unit_fold : rel_fold unit := {rgfold := const_rel_fold unit}.
+Definition const_id_fold {A:Set}(R G:hrel A)(x:A) := x.
+Global Instance nat_fold : rel_fold nat := {rgfold := const_rel_fold nat; fold := const_id_fold}.
+Global Instance bool_fold : rel_fold bool := {rgfold := const_rel_fold bool; fold := const_id_fold}.
+Global Instance unit_fold : rel_fold unit := {rgfold := const_rel_fold unit; fold := const_id_fold}.
 Global Instance pair_fold `{A:Set,B:Set,FA:rel_fold A,FB:rel_fold B}: rel_fold (A*B) :=
   { rgfold := fun R G => 
     prod (rgfold (fun _ _ _ _ => True) (fun a a' h h' => forall b, G (a,b) (a',b) h h'))
-         (rgfold (fun _ _ _ _ => True) (fun b b' h h' => forall a, G (a,b) (a,b') h h')) }.
+         (rgfold (fun _ _ _ _ => True) (fun b b' h h' => forall a, G (a,b) (a,b') h h')) ;
+    fold := fun R G xy => match xy with (x,y) => (fold x, fold y) end
+  }.
 Global Instance ref_fold `{A:Set,P:hpred A,R:hrel A,G:hrel A} : rel_fold (ref{A|P}[R,G]) :=
   { rgfold := fun R' G' => ref{A|P}[R,G ⋂ (fun a a' h h' => 
-                                             forall (r:ref{A|P}[R,G]), h[r]=a -> h'[r]=a' -> G' r r h h')] }.
+                                             forall (r:ref{A|P}[R,G]), h[r]=a -> h'[r]=a' -> G' r r h h')]
+  }.
+(* We'll admit the runtime fold for references; the semantics for proofs will need an extensional treatment
+   as an axiom. *)
+Admitted.
+
 (** TODO: polymorphic lists *)                             
 
 (** ** Reachability, containment, and folding for pure types *)
@@ -237,7 +259,7 @@ Global Instance pure_reachable `{A:Set,PA:pure_type A} : ImmediateReachability A
 Global Instance pure_contains `{A:Set,PA:pure_type A} : Containment A :=
   { contains := fun _ => True }.
 Global Instance pure_fold `{A:Set,PA:pure_type A} : rel_fold A :=
-  { rgfold := fun _ _ => A }.
+  { rgfold := fun _ _ => A ; fold := const_id_fold }.
 Global Instance nat_pure : pure_type nat.
 Global Instance bool_pure : pure_type bool.
 Global Instance unit_pure : pure_type unit.
@@ -247,4 +269,24 @@ Global Instance list_pure `{A:Set,PA:pure_type A} : pure_type (list A).
     Things like heap dereference being the same between converted and unconverted references, etc. *)
 (** For now we need an explicit subtyping operator *)
 Axiom convert_P : forall {A:Set}{P P':hpred A}{R G}`{ImmediateReachability A},(forall v h, P v h -> P' v h) -> precise_pred P' -> stable P' R -> ref{A|P}[R,G] -> ref{A|P'}[R,G].
-Axiom conversion_P_refeq : forall h A (P P':hpred A) (R G:hrel A)`{ImmediateReachability A} pf1 pf2 pf3 x, h[(@convert_P A P P' R G _ pf1 pf2 pf3 x)]=h[x].
+Axiom conversion_P_refeq : forall h A (P P':hpred A) (R G:hrel A)`{ImmediateReachability A} pf1 pf2 pf3 x, h[(@convert_P A P P' R G _ pf1 pf2 pf3 x)]=h[x].
+Axiom convert : forall {A:Set}{P P':hpred A}{R R' G G':hrel A}`{ImmediateReachability A},
+                ref{A|P}[R,G] ->
+                (forall v h, P v h -> P' v h) ->
+                (G' ⊆ G) -> (R ⊆ R') -> stable P' R' -> 
+                (G' ⊆ R') -> (* <-- self-splitting, this is a pure conversion *)
+                ref{A|P'}[R',G'].
+Axiom convert_equiv : forall {A}{P P':hpred A}{R R' G G':hrel A}`{ImmediateReachability A}
+                             (r:ref{A|P}[R,G]) pfP pfG pfR stab splt,
+                             forall h, h[r]=h[@convert A P P' R R' G G' _ r pfP pfG pfR stab splt].
+
+Axiom refine_ref : forall {A:Set}{P P' R G}{fld : rel_fold A}{rfl : hreflexive G}
+                   (r : ref{A|P}[R,G])
+                   (x : rgfold R G),
+                   stable P' R ->
+                   ((@deref _ _ fld _ _ _ rfl (eq_refl) r) = x) -> (* <-- This is only available in special match statements, and flow is restricted! *)
+                   (forall h, (fold (h[r]))=(deref rfl (eq_refl) r) -> (deref rfl eq_refl r) = x -> P (h[r]) h -> P' (h[r]) h) ->
+                   ref{A|P'}[R,G].
+Axiom refinement_equiv : forall {A P P' R G}{fld : rel_fold A}{rfl : hreflexive G}
+                                (r:ref{A|P}[R,G]) x stab pf refpf,
+                                forall h, h[r] = h[@refine_ref A P P' R G fld rfl r x stab pf refpf].

RGref/DSL/Fields.v

@@ -0,0 +1,71 @@
+Require Import RGref.DSL.DSL.
+Require Import Coq.Vectors.Fin.
+Require Import Coq.Arith.Arith.
+
+(* Field Typing is a tagging mechanism, that fields of T are indexed by F *)
+Class FieldTyping (T : Set) (F : Set) : Set := {}.
+
+Class FieldType (T : Set) (F : Set) `{FieldTyping T F} (f:F) (FT : Set) := {
+  getF : T -> FT;
+  setF : T -> FT -> T
+  (* In theory we could also require a proof that it satisfies the theory
+     of arrays, e.g. forall x v, getF (setF x v) = v. *)
+}.
+
+(* Field-aware heap access primitives *)
+Axiom field_read : forall {T B F Res:Set}{P R G}`{rel_fold T}
+                          `{rgfold R G = B}
+                          `{hreflexive G}
+                          (r:ref{T|P}[R,G]) (f:F)
+                          `{FieldType B F f Res},
+                          Res.
+Check @getF. Check @fold. Check @setF.
+Axiom field_write : forall {Γ}{T F Res:Set}{P R G}{folder:rel_fold T}
+                           (r:ref{T|P}[R,G]) (f:F) (e : Res)
+                           `{FieldTyping T F}
+                           {ft:FieldType T F f Res}
+                           `{forall h v, 
+                               P v h -> 
+                               (forall Post ft' fte' (pf1:rgfold R G = Post) pf2 x y,
+                                   @field_read T Post F Res P R G folder pf1 pf2 r f x y =
+                                   @getF (@rgfold T folder R G) F ft' f Res fte' (@fold T folder R G v)) ->
+                               G v (@setF T F _ f Res ft v e) h (heap_write r (@setF T F _ f Res ft v e) h)},
+                           rgref Γ unit Γ.
+
+Section FieldDemo.
+
+  Inductive D : Set :=
+    mkD : nat -> bool -> D.
+  Inductive deltaD : hrel D :=
+    incCount : forall n n' b h h', n <= n' -> deltaD (mkD n b) (mkD n' b) h h'
+  | setFlag : forall n h h', deltaD (mkD n false) (mkD n true) h h'.
+  Lemma refl_deltaD : hreflexive deltaD. Proof. red. intros. destruct x. apply incCount. eauto with arith. Qed.
+  Hint Resolve refl_deltaD.
+
+  (* I feel like this is reinventing lenses... *)
+  Inductive Dfield : Set := Count | Flag.
+  Instance dfields : FieldTyping D Dfield.
+  Instance dfield_count : FieldType D Dfield Count nat := {
+    getF := fun v => match v with (mkD n b) => n end;
+    setF := fun v fv => match v with (mkD n b) => (mkD fv b) end
+  }.
+  Instance dfield_flag : FieldType D Dfield Flag bool := {
+    getF := fun v => match v with (mkD n b) => b end;
+    setF := fun v fv => match v with (mkD n b) => (mkD n fv) end
+  }.
+
+  Instance pureD : pure_type D.
+  Program Example demo {Γ} (r : ref{D|any}[deltaD,deltaD]) : rgref Γ unit Γ :=
+    @field_write Γ D Dfield nat _ _ _ _ r Count ((@field_read _ D Dfield _ _ _ _ _ _ _ r Count _ _)+1) _ _ _.
+  Next Obligation.
+    unfold demo_obligation_1. unfold demo_obligation_2.
+(*    Check @getF.
+    cut (forall T B (v:B) F Res P R G folder pf1 pf2 r f fs fi ft ftb, 
+           @field_read T B F Res P R G folder pf1 pf2 r f fs fi = 
+                     @getF B F ft f Res ftb v).
+    intros Hfieldstuff.*)
+    destruct v.
+(*    rewrite Hfieldstuff.*) erewrite H0.
+    compute. fold plus. constructor. eauto with arith.
+  Qed.
+End FieldDemo.

RGref/DSL/Theories.v

@@ -67,7 +67,9 @@ Proof. compute. intros. inversion H2; subst; constructor. Qed.
 Hint Resolve optset_precise.
 (* TODO: Contains instance for options *)
 Instance option_fold {A:Set}`{rel_fold A} : rel_fold (option A) :=
-  { rgfold := fun R G => option (rgfold havoc (fun a a' h h' => G (Some a) (Some a') h h')) }.
+  { rgfold := fun R G => option (rgfold havoc (fun a a' h h' => G (Some a) (Some a') h h')) ;
+    fold := fun R G o => match o with None => None | Some o' => Some (fold o') end
+  }.
 Lemma optset_refl : forall (A:Set), hreflexive (optset A).
 Proof. compute; intuition; constructor. Qed.
 Hint Resolve optset_refl.

compile.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 export CORE="RGref/DSL/LinearEnv.v RGref/DSL/DSL.v RGref/DSL/Theories.v RGref/DSL/Core.v RGref/DSL/Monad.v"
-export EXAMPLES="AppendOnlyLinkedList.v MonotonicCounter.v PrependOnlyPureList.v CounterModule.v RCC.v ReferenceImmutability.v LinkedList.v"
+export EXAMPLES="PosMonotonicCounter.v AppendOnlyLinkedList.v MonotonicCounter.v PrependOnlyPureList.v CounterModule.v RCC.v ReferenceImmutability.v LinkedList.v"
 export BUGS="KnownUnsoundnessExamples.v"
 coq_makefile -arg -impredicative-set -R RGref RGref $CORE $EXAMPLES $BUGS > Makefile
 touch .depend