Enforce safety of proof principles for higher-order store

Author: csgordon

AppendOnlyLinkedList.v

@@ -16,8 +16,11 @@ Require Import Coq.Program.Equality.
 
 Inductive appList : Set :=
   | rcons : nat -> ref{option appList|any}[optset appList,optset appList] -> appList.
+Global Instance pure_applist : pure_type appList.
+Global Instance pure_option {A:Set}`{pure_type A} : pure_type (@option A).
 
 Definition alist := ref{option appList|any}[optset appList, optset appList].
+Global Instance pure_alist : pure_type alist.
 
 (** A remarkable number of the generated proof goals can be solved by
     firstorder reasoning or basic proof search. *)

LinkedList.v

@@ -61,6 +61,7 @@ Inductive list_imm : hrel rgrList' :=
   | imm_cons : forall h h' P R G n (tl:ref{rgrList'|P}[R,G]),
                list_imm (h[tl]) (h'[tl]) h h' ->
                list_imm (rgrl_cons' rgrList' P R G n tl) (rgrl_cons' rgrList' P R G n tl) h h'.
+Instance pure_rgrlist : pure_type rgrList'.
 (** Ideally we'd like to enforce correct instantiation of 
     the recursive components via a predicate like this:
 <<
@@ -197,7 +198,7 @@ Next Obligation. firstorder. eapply plumb_precise; eauto. firstorder. Qed. (** D
 Program Definition cons { Γ P Q}`{precise_pred P} n (tl meta_tl:@list P Q) 
   : rgref Γ (list P _ (* (fun l h=> locally_const list_imm->l=rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ tl))*)) Γ :=
   (*Alloc! (rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ tl)).*)
-  alloc' _ _ _ (rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ tl)) (rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ meta_tl)) _ _ _ _ _.
+  alloc' _ _ _ (rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ tl)) (rgrl_cons' rgrList' P list_imm list_imm n (convert_P _ _ _ meta_tl)) _ _ _ _ _ _.
 Next Obligation. firstorder. eapply plumb_stable; eauto. firstorder. eapply stable_P_hack; eauto. Qed.
 (** Again, previous goal is solved by things the obligation tactic should be doing... *)
 Next Obligation. constructor.
@@ -209,6 +210,7 @@ Check cons.
 Notation "'RGCons' n tl ::" := (@cons _ _ _ _ n tl ({{{tl}}})) (at level 100).
 
 Record list_container {P Q} := mkList {head : @list P Q}.
+Instance pure_container {P Q}: pure_type (@list_container P Q).
 
 Inductive reach_list_head : forall {Q Q'}{T:Set}{P R G} (p:ref{T|P}[R,G]) (a:@list_container Q Q'), Prop :=
   | reach_container_head : forall Q Q' T P R G p lst, @reach_list_head Q Q' T P R G p (mkList Q Q' lst).

MemoTable.v

@@ -0,0 +1,58 @@
+Require Import RGref.DSL.DSL.
+Require Import Coq.Arith.Arith.
+
+Section MemoTable.
+
+  (* Apparently the instances below stick around after the section ends... *)
+  Variable B : nat -> Set.
+  Variable f : forall (x:nat), B x.
+  Parameter safe_f : Safe f.
+  Existing Instance safe_f.
+  Parameter safe_B : Safe B.
+  Existing Instance safe_B.
+
+  Definition prefernat {P:nat->Set}(g:forall x:nat, P x)(a:nat) : forall x:nat, P x.
+    refine(let v := g a in
+             (fun x => if eq_nat_dec x a then _ else g x)).
+    subst. exact v.
+  Defined.
+  Print prefernat.
+
+  Definition obs_equiv {A:Set}{P:A->Set}(f g:forall x, P x)(_ _:heap) :=
+    forall x, f x = g x.
+  Lemma obs_eq_refl : forall A P, hreflexive (@obs_equiv A P).
+  Proof. intros; red. compute. eauto. Qed.
+  Hint Resolve obs_eq_refl.
+  Lemma precise_obs_equiv : precise_rel (@obs_equiv nat (fun _ => nat)).
+  Proof. compute. intuition. Qed.
+  Hint Resolve precise_obs_equiv.
+
+  Instance safe_prefernat : Safe (@prefernat).
+(*  Instance prior_safe (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat)
+    : Safe (@prefernat B (@deref _ _ _ _ _ _ (obs_eq_refl _ _) eq_refl r) n). *)
+  Instance prior_safe (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat)
+                              : ESafe 0 (@prefernat B f n).
+    repeat solve_applications.
+  Defined.
+    
+  Program Definition prioritize {Γ} (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat) : rgref Γ unit Γ :=
+    [r]:= prefernat (!r) n.
+  Next Obligation.
+    repeat solve_applications.
+  Qed.
+  Next Obligation.
+    red. unfold prefernat. intros. induction (eq_nat_dec x n); intuition; eauto.
+    subst. compute. eauto.
+  Qed.
+(* Doesn't (and shouldn't!) typecheck *)
+  Program Example should_not_typecheck {Γ} (r:ref{nat|any}[havoc,havoc]) : rgref Γ (ref{nat->nat|any}[havoc,havoc]) Γ :=
+    Alloc (fun x => !r). (*;
+    prioritize _ r 0.
+  (*Print should_not_typecheck.*)
+*)
+  Next Obligation. compute; eauto. Defined.
+  Next Obligation.
+    (* Cannot typecheck because (λ x:N. !r) is in fact not safe! *)
+  Admitted.
+
+End MemoTable.

RCC.v

@@ -35,13 +35,14 @@ Module Type RCC.
                                {pres:(forall h, P meta_x h -> P meta_e (hwrite x meta_e h))}
                                , rgref Γ unit Γ.
 *)
-  Parameter rcc_write : forall {Γ Γ'}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}{l:lock}{w:var}{pf:tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ}(x:rccref A P R G l)(e:rgref Γ A Γ')
+  Parameter rcc_write : forall {Γ Γ'}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}{l:lock}{w:var}{pf:tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ}(x:rccref A P R G l)(e:rgref Γ A Γ')`{ESafe 0 _ e}
                                (meta_x_deref:rgref Γ A Γ') (meta_e_fold:rgref Γ A Γ')
                                {guar:forall h env, G (valueOf _ _ _ env h meta_x_deref) (valueOf _ _ _ env h e) h (hwrite x (valueOf _ _ _ env h e) h)}
                                {pres:(forall h env, P (valueOf _ _ _ env h meta_x_deref) h -> P (valueOf _ _ _ env h meta_e_fold) (hwrite x (valueOf _ _ _ env h meta_e_fold) h))}
                                , rgref Γ unit Γ'.
 
   Parameter rcc_alloc : forall {Γ}{T:Set}{RT:ImmediateReachability T}{CT:Containment T}{FT:rel_fold T} P R G (l:lock) (e:T), 
+                `(ESafe 0 e) ->
                 stable P R ->        (* predicate is stable *)
                 (forall h, P e h) -> (* predicate is true *)
                 precise_pred P ->    (* P precise *)
@@ -76,21 +77,22 @@ Module RCCImpl : RCC.
                                {pres:(forall h, P meta_x h -> P meta_e (heap_write x meta_e h))}
                                : rgref Γ unit Γ :=
       @write' Γ A _ P R G _ x e meta_x meta_e _ _.*)
-  Program Definition rcc_write {Γ Γ'}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}{l:lock}{w:var}{pf:tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ}(x:rccref A P R G l)(e:rgref Γ A Γ')
+  Program Definition rcc_write {Γ Γ'}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}{l:lock}{w:var}{pf:tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ}(x:rccref A P R G l)(e:rgref Γ A Γ')`{ESafe 0 _ e}
                                (meta_x_deref:rgref Γ A Γ') (meta_e_fold:rgref Γ A Γ')
                                {guar:forall h env, G (valueOf _ _ _ env h meta_x_deref) (valueOf _ _ _ env h e) h (hwrite l _ _ _ _ x (valueOf _ _ _ env h e) h)}
                                {pres:(forall h env, P (valueOf _ _ _ env h meta_x_deref) h -> P (valueOf _ _ _ env h meta_e_fold) (hwrite _ _ _ _ _ x (valueOf _ _ _ env h meta_e_fold) h))}
                                : rgref Γ unit Γ' :=
-                               @write_imp_exp Γ Γ' A _ P R G _ x e meta_x_deref meta_e_fold guar pres.
+                               @write_imp_exp Γ Γ' A _ P R G _ x e _ meta_x_deref meta_e_fold guar pres.
 
   Program Definition rcc_alloc {Γ}{T:Set}{RT:ImmediateReachability T}{CT:Containment T}{FT:rel_fold T} P R G (l:lock) (e:T) 
+                `(ESafe 0 _ e)
                 `(stable P R)        (* predicate is stable *)
                 `((forall h, P e h)) (* predicate is true *)
                 `(precise_pred P)    (* P precise *)
                 `(precise_rel R)     (* R precise *)
                 `(precise_rel G)     (* G precise *)
                 : rgref Γ (rccref T P R G l) Γ :=
-      alloc _ _ _ e _ _ _ _ _.
+      alloc _ _ _ e _ _ _ _ _ _.
   Parameter acquire : forall {Γ}(w:var)(l:lock), rgref Γ unit (w:ref{lockwitness l | locked}[empty,locked-->unlocked],Γ).
   Parameter release : forall {Γ}{l:lock}(w:var){pf:(tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ)}, rgref Γ unit (tyrem pf).
 End RCCImpl.
@@ -113,13 +115,13 @@ Section RaceFreeMonotonicCounter.
   Program Definition read_counter {Γ}{l:lock}{w:var}{pf:tymember w (ref{lockwitness l | locked}[empty,locked-->unlocked]) Γ}
     (c:rf_monotonic_counter l) : rgref Γ nat Γ :=
     @rcc_read _ _ _ _ _ _ _ l w _ c _ _.
-  Check @rcc_write.
   Local Obligation Tactic := intros; compute [increasing hreflexive]; eauto; try apply natsp.
   Program Definition inc_monotonic {Γ l}{w:var}{pf:tymember w (ref{lockwitness l|locked}[empty,locked-->unlocked]) Γ} (p:rf_monotonic_counter l) : rgref Γ unit Γ :=
     (*rccwrite p <:= ((rcc_read p _ _) + 1).*)
     (* We can't directly add to the read result because that result is monadic.  Instead we have to use pureApp. *)
     @rcc_write Γ Γ nat _ any increasing increasing _ l _ _ p
         (@pureApp _ _ _ _ _ (plus 1) (@rcc_read Γ _ _ _ _ _ _ l w pf p _ _))
+        _
         ({{{@rcc_read Γ _ _ _ _ _ _ l w pf p _ _}}})
         ({{{pureApp _ _ _ _ _ (plus 1) (@rcc_read Γ _ _ _ _ _ _ l w pf p _ _)}}}) _ _.
   Next Obligation.
@@ -136,7 +138,7 @@ Section RaceFreeMonotonicCounter.
   Local Obligation Tactic := intros; eauto with arith; compute; auto with arith; repeat constructor.
   Program Definition mkRFCounter {Γ} (l:lock) : rgref Γ (rf_monotonic_counter l) Γ :=
     (*RCCAlloc l 0.*)
-    rcc_alloc _ _ _ l 0 _ _ _ _ _.
+    rcc_alloc _ _ _ l 0 _ _ _ _ _ _.
   (** Again, remember that the lock witness should really be in a monadic context *)
   Parameter w : var.
   Program Example test_counter {Γ} (l:lock) : rgref Γ unit Γ :=

RGref/DSL/Core.v

@@ -246,6 +246,11 @@ Global Instance ref_fold `{A:Set,P:hpred A,R:hrel A,G:hrel A} : rel_fold (ref{A|
 (* We'll admit the runtime fold for references; the semantics for proofs will need an extensional treatment
    as an axiom. *)
 Admitted.
+Global Instance fn_fold {T : Set}{B : T -> Set} : rel_fold (forall x : T, B x) := {
+    rgfold := fun _ _ => (forall x : T, B x);
+    fold := fun _ _ x => x
+  }.
+
 
 (** TODO: polymorphic lists *)                             
 

RGref/DSL/Monad.v

@@ -35,6 +35,45 @@ Axiom rgret : forall {Γ:tyenv}{A:Set}(a:A), rgref Γ A Γ .
 
 Axiom dropvar : forall {Γ} (v:var) (t:Set) (tm:tymember v t Γ), rgref Γ unit (tyrem tm).
 
+(** * Higher-Order Safety *)
+(** The following typeclass network prohibits latent dereference expressions in the heap, alleviating the need for
+    extra caution in proof principles, and removing the need for the type-sensitive semantics in the PLDI'13 paper.
+    It is the subject of a submission to POPL'14. *)
+(* Some background stuff... *)
+  Instance n2n : ImmediateReachability (nat -> nat) := { imm_reachable_from_in := fun _ _ _ _ _ _ => False }.
+  Print Containment.
+  Instance n2nc : Containment (nat -> nat) := {contains := fun _ => False}.
+
+  Instance n2n' : ImmediateReachability (forall x : nat, (fun _ : nat => nat) x) := { imm_reachable_from_in := fun _ _ _ _ _ _ => False }.
+
+
+Class Library {T:Type}(o:T) : Prop := {}.
+Class Safe {T:Type}(t:T) : Prop := {}.
+Class SafeType (T:Type) : Prop := {}.
+Instance safe_lib {T:Type}{o:T}`{Library T o} : Safe o.
+Instance val_of_safe_type {T:Type}`{SafeType T}(t:T) : Safe t.
+Instance imp_of_safe_type {T:Set}`{SafeType T}{Γ}(t : rgref Γ T Γ) : Safe t.
+Instance puretype_safe {T:Set}`{pure_type T} : SafeType T.
+
+Class ESafe (n:nat){T:Type}(t:T) : Prop := { force_proof : False }.
+Instance safe_esafe {T:Type}(t:T){n:nat}`{Safe _ t} : ESafe n t. Admitted.
+Instance esafe_ind {A:Type}{B:A->Type}{n:nat}(f:forall x:A, B x)`{forall a:A, Safe a -> ESafe n (f a)} : ESafe (S n) f.
+Admitted.
+Instance deref_esafe {A B:Set}{P R G}`{rel_fold A}(r:ref{A|P}[R,G]){a b} : ESafe 0 (@deref A B _ P R G a b r).
+Admitted.
+Instance esafe_app {A:Type}{B:A->Type}(f:forall x:A, B x)(a:A){n:nat}`{ESafe (S n) _ f}`{ESafe 0 _ a} : ESafe n (f a).
+Admitted.
+
+Ltac solve_applications :=
+  match goal with
+  | [ |- @ESafe _ _ (?g _ _ _) ] => eapply @esafe_app with (f := g _ _)
+  | [ |- @ESafe _ _ (?g _ _) ] => eapply @esafe_app with (f := g _)
+  | [ |- @ESafe _ _ (?g _) ] => eapply @esafe_app with (f := g)
+  end; eauto with typeclass_instances.
+
+
+
+
 (** The core problem with folding here is that we want the user (and automated provers!) to see the same dereference on either side of
     G's state.  But G applies to elements of A, not [R,G]>>A.  We could introduce an internal "cheat_deref" that skipped
     folding, but then the two sides aren't equal, and many automated tactics that treat !e as essentially an uninterpreted
@@ -63,15 +102,15 @@ Axiom dropvar : forall {Γ} (v:var) (t:Set) (tm:tymember v t Γ), rgref Γ unit
                    G (!l) e h (heap_write l e h)}
                  {pres:(forall h (l:ref{A|P}[R,G]), P (!l) h -> P e (heap_write l e h))}
                  , rgref Γ unit Γ.*)
-Program Axiom write' : forall {Γ:tyenv}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}(x:ref{A|P}[R,G])(e:A)
+Program Axiom write' : forall {Γ:tyenv}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}(x:ref{A|P}[R,G])(e:A)`{ESafe 0 A e}
                       (meta_x_deref:A) (meta_e_fold:A) 
                       (** These meta args are notationally expanded x and e using the identity relation folding *)
                  (*{guar:forall h, G (!x) e h (heap_write x e h)} *)
                  {guar:forall h, (forall A (fa:rel_fold A), fa = meta_fold) -> G (meta_x_deref) e h (heap_write x e h)}
                  (** temporarily not using meta_e_fold... the cases where I needed the "nop" behavior are once where the types are actually equal *)
                  {pres:(forall h, P meta_x_deref h -> P meta_e_fold (heap_write x meta_e_fold h))}
                  , rgref Γ unit Γ.
-Notation "[ x ]:= e" := (@write' _ _ _ _ _ _ _ x e ({{{!x}}}) ({{{e}}}) _ _) (at level 70).
+Notation "[ x ]:= e" := (@write' _ _ _ _ _ _ _ x e _ ({{{!x}}}) ({{{e}}}) _ _) (at level 70).
 (** TODO: heap writes that update the predicate.  Because of the monadic style, we'll actually
    need a new axiom and syntax support for this, to rebind the variable at the strengthened type *)
 
@@ -99,6 +138,7 @@ Program Axiom read_imp : forall {Γ}{A B:Set}`{rel_fold A}{P R G}`{hreflexive G}
 
 (* Writing with an impure source expression (and direct ref value) *)
 Program Axiom write_imp_exp : forall {Γ Γ'}{A:Set}`{rel_fold A}{P R G}`{hreflexive G}(x:ref{A|P}[R,G])(e:rgref Γ A Γ')
+                              `{ESafe 0 _ e}
                               (meta_x_deref:rgref Γ A Γ') (meta_e_fold:rgref Γ A Γ')
                               {guar:forall h env, G (valueOf _ _ _ env h meta_x_deref) (valueOf _ _ _ env h e) h (heap_write x (valueOf _ _ _ env h e) h)}
                               {pres:(forall h env, P (valueOf _ _ _ env h meta_x_deref) h -> P (valueOf _ _ _ env h meta_e_fold) (heap_write x (valueOf _ _ _ env h meta_e_fold) h))}
@@ -109,36 +149,39 @@ Definition locally_const {A:Set} (R:hrel A) := forall a a' h h', R a a' h h' ->
 
 
 Axiom alloc : forall {Γ}{T:Set}{RT:ImmediateReachability T}{CT:Containment T}{FT:rel_fold T} P R G (e:T), 
+                ESafe 0 e ->
                 stable P R ->        (* predicate is stable *)
                 (forall h, P e h) -> (* predicate is true *)
                 precise_pred P ->    (* P precise *)
                 precise_rel R ->     (* R precise *)
                 precise_rel G ->     (* G precise *)
                 rgref Γ (ref{T|P}[R,G]) Γ.
-Notation "'Alloc' e" := (alloc _ _ _ e _ _ _ _ _) (at level 70).
+Notation "'Alloc' e" := (alloc _ _ _ e _ _ _ _ _ _) (at level 70).
 (** Sometimes it is useful to refine P to give equality with the allocated value, which
     propagates assumptions and equalities across "statements." *)
 Axiom alloc' : forall {Γ}{T:Set}{RT:ImmediateReachability T}{CT:Containment T}{FT:rel_fold T} P R G (e:T) (meta_e:T),
+                ESafe 0 e ->
                 stable P R ->        (* predicate is stable *)
                 (forall h, P e h) -> (* predicate is true *)
                 precise_pred P ->    (* P precise *)
                 precise_rel R ->     (* R precise *)
                 precise_rel G ->     (* G precise *)
                  rgref Γ (ref{T|P ⊓ (fun t=>fun h=> (locally_const R -> t=meta_e))}[R,G]) Γ.
-Notation "Alloc! e" := (alloc' _ _ _ e ({{{e}}}) _ _ _ _ _) (at level 70).
+Notation "Alloc! e" := (alloc' _ _ _ e ({{{e}}}) _ _ _ _ _ _) (at level 70).
 
 
 
 Notation "x <- M ; N" := (rgref_bind M (fun x => N)) (at level 49, right associativity).
 
 Axiom varalloc' : forall {Γ}{T:Set}{RT:ImmediateReachability T}{CT:Containment T}{FT:rel_fold T} P R G (v:var) (e:T) (meta_e:T),
+                ESafe 0 e ->
                 stable P R ->        (* predicate is stable *)
                 (forall h, P e h) -> (* predicate is true *)
                 precise_pred P ->    (* P precise *)
                 precise_rel R ->     (* R precise *)
                 precise_rel G ->     (* G precise *)
                  rgref Γ unit (v:ref{T|P ⊓ (fun t=>fun h=> (locally_const R -> t=meta_e))}[R,G],Γ).
-Notation "VarAlloc! v e" := (varalloc' _ _ _ v e ({{{e}}}) _ _ _ _ _) (at level 70).
+Notation "VarAlloc! v e" := (varalloc' _ _ _ v e ({{{e}}}) _ _ _ _ _ _) (at level 70).
 
 
 

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="PosMonotonicCounter.v 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 MemoTable.v"
 export BUGS="KnownUnsoundnessExamples.v"
 coq_makefile -arg -impredicative-set -R RGref RGref $CORE $EXAMPLES $BUGS > Makefile
 touch .depend