Update for MEMOCODE2017 paper

PEDANTIC/ClosureHelper.v

@@ -0,0 +1,87 @@
+(**********************************************************************************
+ * The PEDANTIC (Proof Engine for Deductive Automation using Non-deterministic
+ * Traversal of Instruction Code) verification framework
+ *
+ * Developed by Kenneth Roe
+ * For more information, check out www.cs.jhu.edu/~roe
+ *
+ * ClosureHelper.v
+ *
+ **********************************************************************************)
+
+Require Export SfLib.
+Require Export SfLibExtras.
+Require Export ImpHeap.
+Require Export AbsState.
+Require Export AbsExecute.
+Require Export AbsStateInstance.
+Require Export Simplify.
+Require Export Eqdep.
+Require Export StateImplication.
+Require Export Classical.
+Require Export Unfold.
+Require Export Fold.
+Require Export merge.
+Require Export ProgramTactics.
+
+Theorem breakClosure : forall bindings s state param ss,
+    ss = subStateList state param ->
+    (realizeState (AbsClosure state param) bindings s <-> realizeState ss bindings s).
+Proof.
+    admit.
+Admitted.
+
+Fixpoint breakTopClosure (s : absState) : absState :=
+   match s with
+    | AbsStar s1 s2 => (AbsStar (breakTopClosure s1) (breakTopClosure s2))
+    | AbsOrStar s1 s2 => (AbsOrStar (breakTopClosure s1) (breakTopClosure s2))
+    | AbsExistsT s => AbsExistsT (breakTopClosure s)
+    | AbsExists e s => AbsExists e (breakTopClosure s)
+    | AbsAll e s => AbsAll e (breakTopClosure s)
+    | AbsEach e s => AbsEach e (breakTopClosure s)
+    | AbsEmpty => AbsEmpty
+    | AbsAny => AbsAny
+    | AbsNone => AbsNone
+    | AbsLeaf i ll => AbsLeaf i ll
+    | AbsAccumulate id e1 e2 e3 => AbsAccumulate id e1 e2 e3
+    | AbsMagicWand s1 s2 => AbsMagicWand (breakTopClosure s1) (breakTopClosure s2)
+    | AbsUpdateVar s vv vall => AbsUpdateVar (breakTopClosure s) vv vall
+    | AbsUpdateWithLoc s vv vall => AbsUpdateWithLoc (breakTopClosure s) vv vall
+    | AbsUpdateLoc s vv vall => AbsUpdateLoc (breakTopClosure s) vv vall
+    | AbsUpdState s1 s2 s3 =>  (AbsUpdState (breakTopClosure s1) (breakTopClosure s2) (breakTopClosure s3))
+    | AbsClosure s ll => subStateList s ll
+   end.
+
+Theorem breakTopClosureThm1 : forall bindings s state1 state2,
+    state1 = breakTopClosure state2 ->
+    (realizeState state1 bindings s -> realizeState state2 bindings s).
+Proof.
+    admit.
+Admitted.
+
+Theorem breakTopClosureThm2 : forall bindings s state1 state2,
+    state1 = breakTopClosure state2 ->
+    (realizeState state2 bindings s -> realizeState state1 bindings s).
+Proof.
+    admit.
+Admitted.
+
+Theorem breakLeftClosureThm : forall left1 left2 right m,
+    left1 = breakTopClosure left2 ->
+    mergeStates left1 right m -> mergeStates left2 right m.
+Proof.
+    admit.
+Admitted.
+
+Theorem breakRightClosureThm : forall left right1 right2 m,
+    right1 = breakTopClosure right2 ->
+    mergeStates left right1 m -> mergeStates left right2 m.
+Proof.
+    admit.
+Admitted.
+
+
+
+
+
+

PEDANTIC/Fold.v

@@ -22,7 +22,6 @@ Require Export AbsStateInstance.
 Require Export PickElement.
 Require Export AbsExecute.
 Require Export Coq.Logic.FunctionalExtensionality.
-Opaque unitEval.
 
 (*
  * pickNCells picks out the cells that are to be included in the folded RFun term.  It also generates
@@ -35,24 +34,28 @@ Opaque unitEval.
  *    #4 : absExp - root of folded tree
  *    #5 : list absState - output of the list of cells picked
  *)
-Inductive pickNCells  {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absState ev eq f t ac -> nat -> @absExp ev eq f -> list (@absState ev eq f t ac) -> Prop :=
+Inductive pickNCells : absState -> absState -> nat -> absExp -> list absState -> Prop :=
     | PNCBase : forall state root,
                 pickNCells state state 0 root nil
-    | PNCInductive : forall state state1 state2 size root v cells,
+    | PNCInductive0 : forall state state1 state2 root v cells,
+                     spickElement state (root |-> v) state1 ->
+                     pickNCells state1 state2 0 root cells ->
+                     pickNCells state state2 (S 0) root (cells++(root++++#0 |-> v)::nil)     | PNCInductive : forall state state1 state2 size root v cells,
                      spickElement state (root++++#size |-> v) state1 ->
                      pickNCells state1 state2 size root cells ->
                      pickNCells state state2 (S size) root (cells++(root++++#size |-> v)::nil).
 Hint Constructors pickNCells.
 
-Ltac pickNCells := (eapply PNCBase || (eapply PNCInductive;[solveSPickElement | pickNCells])).
+Ltac pickNCells := (eapply PNCBase || (eapply PNCInductive0;[solveSPickElement | pickNCells]) || (eapply PNCInductive;[solveSPickElement | pickNCells])).
 
-Inductive strip_fields {ev} {eq} {f} : list (@absExp ev eq f) -> list nat -> Prop :=
+Inductive strip_fields : list absExp -> list nat -> Prop :=
     | SFNil : strip_fields nil nil
     | SFCons : forall n r1 r2,
                strip_fields r1 r2 ->
                strip_fields ((#n)::r1) (n::r2).
 Hint Constructors strip_fields.
 
+Ltac stripFields := ((eapply SFCons;stripFields) || eapply SFNil).
 (*
  * pickNHeaps picks out the heaps that are to be included in the folded RFun term.  It also generates
  * a portion of the predicate used to map the original components to the folded components
@@ -66,7 +69,7 @@ Hint Constructors strip_fields.
  *    #6 : list (nat * absState) - output of the list of heaps picked (associated with their field
  *                                 offset)
  *)
-Inductive pickNHeaps {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absState ev eq f t ac -> (list nat) -> nat -> list nat -> list (@absState ev eq f t ac)-> list (nat * (@absState ev eq f t ac)) -> Prop :=
+Inductive pickNHeaps : absState -> absState -> (list nat) -> nat -> list nat -> list (absState)-> list (nat * (absState)) -> Prop :=
     | PNHBase : forall state size fields cells,
                 pickNHeaps state state nil size fields cells nil
     | PNHInductive : forall state state1 state2 base fff r root ff fields cells size heap hr e_fields,
@@ -77,17 +80,17 @@ Inductive pickNHeaps {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absStat
                 pickNHeaps state state2 (fff::r) size e_fields cells ((fff,TREE(base,v(heap),#size,fields))::hr).
 Hint Constructors pickNHeaps.
 
-Ltac pickNHeaps := (eapply PNHInductive;[auto | (simpl;reflexivity) | solveSPickElement | pickNHeaps]) ||
+Ltac pickNHeaps := (eapply PNHInductive;[stripFields | (simpl;reflexivity) | solveSPickElement | pickNHeaps]) ||
                    eapply PNHBase.
 
-Fixpoint folded_heap {ev} {eq} {f} {t} {ac} (v : nat) (heaps : list (nat * (@absState ev eq f t ac))) : option nat :=
+Fixpoint folded_heap (v : nat) (heaps : list (nat * absState)) : option nat :=
    match heaps with
    | ((x,TREE(root,v(h),size,fields))::r) => if beq_nat h v then Some x else folded_heap v r
    | (_::r) => folded_heap v r
    | _ => None
    end.
 
-Fixpoint noFold {ev} {eq} {f} {t} {ac} (e : @absExp ev eq f) (heaps : list (nat * (@absState ev eq f t ac))) : bool :=
+Fixpoint noFold (e : absExp) (heaps : list (nat * absState)) : bool :=
    match e with
    | AbsConstVal v => true
    | AbsVar vv => true
@@ -98,43 +101,57 @@ Fixpoint noFold {ev} {eq} {f} {t} {ac} (e : @absExp ev eq f) (heaps : list (nat
                                 end) l
    end.
 
-Fixpoint foldExp {ev} {eq} {f} {t} {ac} (e : @absExp ev eq f) (heaps : list (nat * (@absState ev eq f t ac))) : @absExp ev eq f :=
+Fixpoint foldExp (e : absExp) (n : nat) (heaps : list (nat * absState)) : absExp :=
    match e with
    | AbsConstVal v => (AbsConstVal v)
    | AbsVar vv => (AbsVar vv)
-   | AbsQVar v => match folded_heap v heaps with None => (AbsQVar (S v)) | Some x => nth(v(0),#(x+1)) end
+   | AbsQVar v => match folded_heap v heaps with None => (AbsQVar v) | Some x => nth(v(n),#(x+1)) end
    | AbsFun i l => AbsFun i ((fix go l := match l with
                                 | nil       => nil
-                                | (a::b)    => (foldExp a heaps)::(go b)
+                                | (a::b)    => (foldExp a n heaps)::(go b)
                                 end) l)
    end.
 
-Fixpoint foldState {ev} {eq} {f} {t} {ac} (s : @absState ev eq f t ac) (heaps : list (nat * (@absState ev eq f t ac))) : @absState ev eq f t ac :=
+Fixpoint addHeaps (heaps : list (nat * absState)) :=
+    map (fun x => (fst x,addStateVar 0 (snd x))) heaps.
+
+Fixpoint foldState (s : absState) (n : nat) (heaps : list (nat * absState)) : absState :=
    match s with
-    | AbsStar s1 s2 => (AbsStar (foldState s1 heaps) (foldState s2 heaps))
-    | AbsOrStar s1 s2 => (AbsOrStar (foldState s1 heaps) (foldState s2 heaps))
-    | AbsExistsT s => AbsExistsT (foldState s heaps)
-    | AbsExists e s => AbsExists (foldExp e heaps) (foldState s heaps)
-    | AbsAll e s => AbsAll (foldExp e heaps) (foldState s heaps)
-    | AbsEach e s => AbsEach (foldExp e heaps) (foldState s heaps)
+    | AbsStar s1 s2 => (AbsStar (foldState s1 n heaps) (foldState s2 n heaps))
+    | AbsOrStar s1 s2 => (AbsOrStar (foldState s1 n heaps) (foldState s2 n heaps))
+    | AbsExistsT s => AbsExistsT (foldState s (S n) (addHeaps heaps))
+    | AbsExists e s => AbsExists (foldExp e n heaps) (foldState s (S n) (addHeaps heaps))
+    | AbsAll e s => AbsAll (foldExp e n heaps) (foldState s (S n) (addHeaps heaps))
+    | AbsEach e s => AbsEach (foldExp e n heaps) (foldState s (S n) (addHeaps heaps))
     | AbsEmpty => AbsEmpty
-    | AbsLeaf i l => AbsLeaf i (map (fun x => foldExp x heaps) l)
-    | AbsAccumulate id e1 e2 e3 => AbsAccumulate id (foldExp e1 heaps) (foldExp e2 heaps) (foldExp e3 heaps)
-    | AbsMagicWand s1 s2 => AbsMagicWand (foldState s1 heaps) (foldState s2 heaps)
-    | AbsUpdateVar s i e => AbsUpdateVar (foldState s heaps) i (foldExp e heaps)
-    | AbsUpdState s1 s2 s3 => AbsUpdState (foldState s1 heaps) (foldState s2 heaps) (foldState s3 heaps)
+    | AbsNone => AbsNone
+    | AbsAny => AbsAny
+    | AbsLeaf i l => AbsLeaf i (map (fun x => foldExp x n heaps) l)
+    | AbsAccumulate id e1 e2 e3 => AbsAccumulate id (foldExp e1 n heaps) (foldExp e2 n heaps) (foldExp e3 n heaps)
+    | AbsMagicWand s1 s2 => AbsMagicWand (foldState s1 n heaps) (foldState s2 n heaps)
+    | AbsUpdateVar s i e => AbsUpdateVar (foldState s n heaps) i (foldExp e n heaps)
+    | AbsUpdateWithLoc s i e => AbsUpdateWithLoc (foldState s n heaps) i (foldExp e n heaps)
+    | AbsUpdateLoc s l e => AbsUpdateLoc (foldState s n heaps) (foldExp l n heaps) (foldExp e n heaps)
+    | AbsUpdState s1 s2 s3 => AbsUpdState (foldState s1 n heaps) (foldState s2 n heaps) (foldState s3 n heaps)
+    | AbsClosure s l => AbsClosure s (map (fun x => foldExp x n heaps) l)
    end.
 
-Fixpoint build_equations {ev} {eq} {f} {t} {ac} (heap : @absExp ev eq f) (cells : list (@absState ev eq f t ac)) (fields : list nat) : @absState ev eq f t ac :=
+Fixpoint build_equations (heap : absExp) (cells : list absState) (fields : list nat) : absState :=
     match cells with
     | nil => AbsEmpty
     | ((l++++#o |-> val)::r) => if mem_nat o fields then
-                                    ([nth(nth(heap,#(o+1)),#0)====(pushAbsVar val)]) ** (build_equations heap r fields)
+                                    ([nth(nth(heap,#(o+1)),#0)====val]) ** (build_equations heap r fields)
                                 else
-                                    ([nth(heap,#(o+1))====(pushAbsVar val)]) ** (build_equations heap r fields)
+                                    ([nth(heap,#(o+1))====val]) ** (build_equations heap r fields)
     | (_::r) => build_equations heap r fields
     end.
 
+Fixpoint getRootLevel (s : absState) : nat :=
+    match s with
+    | AbsExistsT s => S (getRootLevel s)
+    | _ => 0
+    end.
+
 (*
  * This is the main fold function.  It picks out the CellFun and RFun components to be folded and replaces
  * them all with a single RFun component.
@@ -144,21 +161,16 @@ Fixpoint build_equations {ev} {eq} {f} {t} {ac} (heap : @absExp ev eq f) (cells
  *  #1 : absState - state to be folded
  *  #2 : absState - output of folded state
  *)
-Inductive foldHeap {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absState ev eq f t ac -> Prop :=
-    FoldHeap : forall state state2 hvars size fields e_fields cells root r r' r'',
+Inductive foldHeap : absState -> absState -> Prop :=
+    FoldHeap : forall state state2 hvars size fields e_fields cells root r r' r'' rl,
          strip_fields e_fields fields ->
          r = getRoot state ->
          pickNCells r r' size root cells ->
          pickNHeaps r' r'' fields size fields cells hvars ->
-         state2 = AbsExistsT (replaceRoot state ((TREE(root,v(0),#size,e_fields) ** (build_equations (v(0)) cells fields) ** (foldState r'' hvars)))) ->
+         rl = getRootLevel state ->
+         state2 = AbsExistsT (replaceRoot state ((TREE(root,v(rl),#size,e_fields) ** (build_equations (v(rl)) cells fields) ** (foldState r'' rl hvars)))) ->
          foldHeap state state2.
 
-Fixpoint getRootLevel {ev} {eq} {f} {t} {ac} (s : @absState ev eq f t ac) : nat :=
-    match s with
-    | AbsExistsT s => S (getRootLevel s)
-    | _ => 0
-    end.
-
 (*
  * This is an auxiliary definition that folds up absAll definitions corresponding to the
  * TREE that has just been folded by foldHeap.
@@ -168,16 +180,16 @@ Fixpoint getRootLevel {ev} {eq} {f} {t} {ac} (s : @absState ev eq f t ac) : nat
  *  #1 : absState - state to be folded
  *  #2 : absState - output of folded state
  *)
-Inductive foldAll {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absState ev eq f t ac -> Prop :=
+Inductive foldAll : absState -> absState -> Prop :=
     FoldAll : forall state root root' root'' r roott roott' x n np cond cond' cond'' size e_fields fields var y state2,
         root = getRoot state ->
         n = getRootLevel state ->
         spickElement root (AbsAll TreeRecords(nth(v(x),#np)) cond) root' ->
         spickElement root' (TREE(r, v(x), #size, fields)) roott ->
-        spickElement roott ([nth(v(x),y)====var]) roott' ->
+        spickElement roott ([nth(v(x),#y)====var]) roott' ->
         strip_fields fields e_fields ->
-        cond' = replaceStateExp (nth(find(nth(v(x),#np),v(n)),y)) (var) cond ->
-        cond'' = replaceStateExp nth(v(x),#np) v(x) cond ->
+        cond' = removeStateVar 0 (replaceStateExp (nth(find(nth(v(S x),#np),v(0)),#y)) (addExpVar 0 var) cond) ->
+        cond'' = replaceStateExp nth(v(S x),#np) v(S x) cond ->
         spickElement root' cond' root'' ->
         state2 = replaceRoot state (AbsStar (AbsAll TreeRecords(v(x)) cond'') root'') ->
         foldAll state state2.
@@ -187,10 +199,11 @@ Inductive foldAll {ev} {eq} {f} {t} {ac} : @absState ev eq f t ac -> @absState e
  *)
 Ltac foldHeap R F S :=
      eapply FoldHeap with (root := R) (fields := F) (size := S);[
-                auto |
+                stripFields |
                 (simpl; reflexivity) |
                 pickNCells |
                 pickNHeaps |
+                (simpl; reflexivity) |
                 (simpl; reflexivity)].
 
 Ltac foldAll x :=
@@ -199,17 +212,61 @@ Ltac foldAll x :=
          (simpl; reflexivity) |
          solveSPickElement |
          solveSPickElement |
-         (instantiate (3 := #x);solveSPickElement) |
-         auto |
+         (instantiate (3 := x);solveSPickElement) |
+         stripFields |
          (simpl; reflexivity) |
          (simpl; reflexivity) |
          solveSPickElement |
          (simpl; reflexivity)].
 
-Theorem foldSum {ev} {eq} {f} {t} {ac} : forall v e ttt t1 t2 b s e',
-    @realizeState ev eq f t ac (SUM(range(#0,v),e,t1)) b s ->
-    @realizeState ev eq f t ac (SUM(range(v++++#1,ttt),e,t2)) b s ->
+Theorem foldSum : forall v e ttt t1 t2 b s e',
+    realizeState (SUM(range(#0,v),e,t1)) b s ->
+    realizeState (SUM(range(v++++#1,ttt),e,t2)) b s ->
     e' = replaceExpVar (length b) v e ->
-    @realizeState ev eq f t ac (SUM(range(#0,ttt),e,t1++++t2++++e')) b s.
-Proof. admit. Qed.
+    realizeState (SUM(range(#0,ttt),e,t1++++t2++++e')) b s.
+Proof. admit. Admitted.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 

PEDANTIC/ImpHeap.v

@@ -46,9 +46,9 @@ Definition state := prod env heap.
 
 Definition empty_state : state := (empty_env,empty_heap).
 
-Definition env_p := fst.
+Definition env_p (s : state) := fst s.
 
-Definition heap_p := snd.
+Definition heap_p (s : state) := snd s.
 
 
 (* Basic operations on States *)
@@ -449,3 +449,5 @@ Inductive ceval : functions -> state -> com -> state -> result -> Prop :=
 
 
 
+
+