list_rev : in M2 simplify with only one footprint. Coq proofs

examples/programs/list_rev.mlw

@@ -5,30 +5,112 @@ module M
   use import module ref.Ref
   use import map.Map
 
+  (** Memory model and definition of is_list *)
   type pointer
-
+  type next = map pointer pointer
   logic null : pointer
 
   parameter value : ref (map pointer int)
-  parameter next : ref (map pointer pointer)
+  parameter next : ref (next)
 
-  inductive is_list (next : map pointer pointer) (p : pointer) =
+  inductive is_list (next : next) (p : pointer) =
     | is_list_null: 
-        forall next : map pointer pointer, p : pointer. 
+        forall next : next, p : pointer. 
         p = null -> is_list next p
     | is_list_next: 
-        forall next : map pointer pointer, p : pointer. 
+        forall next : next, p : pointer. 
         p <> null -> is_list next (get next p) -> is_list next p
 
-  logic sep_list_list (next : map pointer pointer) (p1 p2 : pointer)
+  (** Frame for is_list *)
+  type ft 'a
+  logic in_ft pointer (ft pointer)
+  logic list_ft (next : next) (p : pointer) : ft pointer
+
+  axiom frame_list :
+    forall next : next, p : pointer, q : pointer, v : pointer
+      [is_list (set next q v) p].
+    (~ in_ft q (list_ft next p)) -> is_list next p
+      -> is_list (set next q v) p
+
+  (** Definition of sep_node_list *)
+  logic sep_node_list (next : next) (p1 p2 : pointer) =
+    ~in_ft p1 (list_ft next p2)
+
+  axiom list_ft_node_null :
+      forall next : next, q : pointer, p : pointer.
+      q=null -> ~ in_ft p (list_ft next q)
+
+  axiom list_ft_node_next1 :
+      forall next : next, q : pointer, p : pointer.
+      q<>null -> is_list next (get next q) ->
+      in_ft p (list_ft next (get next q)) ->
+      in_ft p (list_ft next q)
+
+  axiom list_ft_node_next2 :
+      forall next : next, q : pointer.
+      q<>null -> is_list next (get next q) ->
+      in_ft q (list_ft next q)
+
+  axiom list_ft_node_next_inv :
+      forall next : next, q : pointer, p : pointer.
+      q<>null -> is_list next (get next q) ->
+      q <> p ->
+      in_ft p (list_ft next q) ->
+      in_ft p (list_ft next (get next q))
+
+  (** Frame for list_ft *)
+  axiom frame_list_ft :
+    forall next : next, p : pointer, q : pointer, v : pointer.
+    (~ in_ft q (list_ft next p)) ->
+      list_ft next p = list_ft (set next q v) p
+
+  (** Definition of sep_list_list *)
+
+  inductive list_disj (ft : ft pointer) (next : next)
+  (p : pointer) =
+    | list_disj_null:
+        forall ft : ft pointer, next : next, p : pointer.
+        p=null -> list_disj ft next p
+    | list_disj_next:
+        forall ft : ft pointer, next : next, p : pointer.
+        p<>null -> is_list next (get next p) -> (~in_ft p ft) ->
+        list_disj ft next (get next p) -> list_disj ft next p
+
+  logic sep_list_list (next : next) (p1 p2 : pointer) =
+    list_disj (list_ft next p1) next p2 /\ list_disj (list_ft next p2) next p1
+
+  axiom list_ft_disj_null :
+      forall next : next, q : pointer, p : pointer.
+      q=null -> list_disj (list_ft next q) next p
+
+  axiom list_ft_disj_next :
+      forall next : next, p : pointer, q : pointer.
+        q <> null -> is_list next (get next q) ->
+        (~in_ft q (list_ft next p)) ->
+        q <> p ->
+        list_disj (list_ft next (get next q)) next p ->
+        list_disj (list_ft next q) next p
 
-  axiom sep_list_list_p_null:
-    forall next : map pointer pointer, p : pointer. 
-    sep_list_list next p null
+  axiom list_ft_disj_next_inv :
+      forall next : next, p : pointer, q : pointer.
+        q <> null -> is_list next (get next q) ->
+        list_disj (list_ft next q) next p ->
+        list_disj (list_ft next (get next q)) next p
 
-  axiom sep_list_list_null_p:
-    forall next : map pointer pointer, p : pointer. 
-    sep_list_list next null p
+  (** Frame for list_disj *)
+  axiom frame_list_disj :
+    forall ft : ft pointer, next : next,
+        p1 : pointer, p2 : pointer, q : pointer, v : pointer
+        [list_disj (list_ft (set next q v) p1) (set next q v) p2].
+      (~ in_ft q (list_ft next p1)) -> (~ in_ft q (list_ft next p2))
+      -> list_disj (list_ft next p1) next p2
+      -> list_disj (list_ft (set next q v) p1) (set next q v) p2
+
+  lemma acyclic_list : forall next : next, p : pointer.
+    p <> null -> is_list next p -> sep_node_list next p (get next p)
+
+  goal consistent : forall next : next, p: pointer, q: pointer.
+    is_list next p -> is_list next q -> false
 
   let list_rev (p : ref pointer) =
     { is_list next p }
@@ -43,6 +125,223 @@ module M
     q
     { is_list next result }
 
+  (** behavior *)
+
+  use import list.Append
+  use import list.Reverse
+
+  logic model (next : next) (p : pointer) : list pointer
+  (* axiom model_def : forall next : next, p : pointer. *)
+  (*   model next p = *)
+  (*       if p = null then Nil else Cons p (model next (get next p)) *)
+
+  axiom model_def1 : forall next : next, p : pointer[model next p].
+    p = null -> model next p = Nil
+
+  axiom model_def2 : forall next : next, p : pointer[model next p].
+    p <> null -> model next p = Cons p (model next (get next p))
+
+  lemma reverse_append : forall l1 : list 'a, l2 : list 'a, x : 'a
+    [(reverse (Cons x l1)) ++ l2|(reverse l1) ++ (Cons x l2)].
+  (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2)
+
+  (** frame model *)
+  axiom frame_model :
+    forall ft : ft pointer, next : next,
+    p : pointer, q : pointer, v : pointer[model (set next q v) p].
+    (~ in_ft q (list_ft next p))
+    -> model next p = model (set next q v) p
+
+  let list_rev_behv (p : ref pointer) =
+    { is_list next p }
+    let old_next = !next in
+    let old_p = !p in
+    let q = ref null in
+    while !p <> null do
+      invariant { is_list next p /\ is_list next q
+                  /\ sep_list_list next p q /\
+      reverse (model (old_next) (old_p)) =
+       (reverse (model next p)) ++ (model next q)}
+      let tmp = get !next !p in
+      let bak_next = !next in
+      next := set !next !p !q;
+      assert { (reverse (Cons p (model next tmp))) ++ (model next q) =
+               (reverse (model next tmp)) ++ (Cons p (model next q))};
+      q := !p;
+      p:= tmp
+    done;
+    q
+    { is_list next result /\ reverse (model (old next) (old p)) =
+        model next result}
+
+
+end
+
+
+module M2
+
+  use import int.Int
+  use import module ref.Ref
+  use import map.Map
+
+  (** Memory model and definition of is_list *)
+  type pointer
+
+  axiom pointer_dec : forall p1:pointer, p2 : pointer. p1 = p2 or p1 <> p2
+
+  type next = map pointer pointer
+  logic null : pointer
+
+  parameter value : ref (map pointer int)
+  parameter next : ref (next)
+
+  inductive is_list (next : next) (p : pointer) =
+    | is_list_null:
+        forall next : next, p : pointer.
+        p = null -> is_list next p
+    | is_list_next:
+        forall next : next, p : pointer.
+        p <> null -> is_list next (get next p) -> is_list next p
+
+  (** Frame for is_list *)
+  type ft 'a
+
+  logic in_ft (p:pointer) (ft:ft pointer)
+
+  axiom set_eq : forall ft1: ft pointer, ft2: ft pointer
+    [in_ft null ft1,in_ft null ft1].
+    (forall q : pointer. in_ft q ft1 <-> in_ft q ft2) -> ft1 = ft2
+
+  logic list_ft (next : next) (p : pointer) : ft pointer
+
+  (* axiom list_ft_node_null : *)
+  (*     forall next : next, q : pointer. *)
+  (*     q=null -> list_ft next q = S.empty *)
+
+  (* axiom list_ft_node_next : *)
+  (*     forall next : next, q : pointer. *)
+  (*     q<>null -> is_list next (get next q) -> *)
+  (*     S.add q (list_ft next (get next q)) =  (list_ft next q) *)
+
+  axiom list_ft_node_null_cor :
+      forall next : next, q : pointer,p : pointer.
+      q=null -> ~in_ft p (list_ft next q)
+
+  axiom list_ft_node_next1 :
+      forall next : next, q : pointer, p : pointer.
+      q<>null -> is_list next (get next q) ->
+      in_ft p (list_ft next (get next q)) ->
+      in_ft p (list_ft next q)
+
+  axiom list_ft_node_next2 :
+      forall next : next, q : pointer.
+      q<>null -> is_list next (get next q) ->
+      in_ft q (list_ft next q)
+
+  axiom list_ft_node_next_inv :
+      forall next : next, q : pointer, p : pointer.
+      q<>null -> is_list next (get next q) ->
+      q <> p ->
+      in_ft p (list_ft next q) ->
+      in_ft p (list_ft next (get next q))
+
+  lemma frame_list :
+    forall next : next, p : pointer, q : pointer, v : pointer
+      [is_list (set next q v) p].
+    (~ in_ft q (list_ft next p)) -> is_list next p
+      -> is_list (set next q v) p
+
+  (** Definition of sep_node_list *)
+  logic sep_node_list (next : next) (p1 p2 : pointer) =
+    ~in_ft p1 (list_ft next p2)
+
+  (** Frame for list_ft *)
+  lemma frame_list_ft :
+    forall next : next, p : pointer, q : pointer, v : pointer.
+    (~ in_ft q (list_ft next p)) -> is_list next p ->
+      list_ft next p = list_ft (set next q v) p
+
+  (** Definition of sep_list_list *)
+
+  (* logic sep_list_list (next : next) (p1 p2 : pointer) = *)
+  (*     S.inter (list_ft next p1) (list_ft next p2) = S.empty *)
+
+  logic sep_list_list (next : next) (p1 p2 : pointer) =
+     forall q : pointer.
+       (~ in_ft q (list_ft next p1)) \/ (~in_ft q (list_ft next p2))
+
+  lemma acyclic_list : forall next : next, p : pointer.
+    p <> null -> is_list next p -> sep_node_list next p (get next p)
+
+  goal consistent : forall next : next, p: pointer, q: pointer.
+    is_list next p -> is_list next q -> false
+
+  let list_rev (p : ref pointer) =
+    { is_list next p }
+    let q = ref null in
+    while !p <> null do
+      invariant { is_list next p /\ is_list next q /\ sep_list_list next p q }
+      let tmp = get !next !p in
+      next := set !next !p !q;
+      q := !p;
+      p:= tmp
+    done;
+    q
+    { is_list next result }
+
+  (** behavior *)
+
+  use import list.Append
+  use import list.Reverse
+
+  (* meta "encoding : lskept" logic Cons *)
+  (* meta "encoding : lskept" logic Nil *)
+
+  logic model (next : next) (p : pointer) : list pointer
+  (* axiom model_def : forall next : next, p : pointer[model next p]. *)
+  (*   model next p = *)
+  (*       if p = null then Nil else Cons p (model next (get next p)) *)
+
+  axiom model_def1 : forall next : next, p : pointer[model next p].
+    p = null -> model next p = Nil
+
+  axiom model_def2 : forall next : next, p : pointer[model next p].
+    p <> null -> model next p = Cons p (model next (get next p))
+
+  (** frame model *)
+  lemma frame_model :
+    forall ft : ft pointer, next : next,
+    p : pointer, q : pointer, v : pointer[model (set next q v) p].
+    is_list next p ->
+    (~ in_ft q (list_ft next p)) ->
+    model next p = model (set next q v) p
+
+  goal consistent_behv : forall next : next, p: pointer, q: pointer.
+    is_list next p -> is_list next q -> false
+
+  let list_rev_behv (p : ref pointer) =
+    { is_list next p }
+    let old_next = !next in
+    let old_p = !p in
+    let q = ref null in
+    while !p <> null do
+      invariant { is_list next p /\ is_list next q
+                  /\ sep_list_list next p q /\
+      reverse (model (old_next) (old_p)) =
+       (reverse (model next p)) ++ (model next q)}
+      let tmp = get !next !p in
+      let bak_next = !next in
+      next := set !next !p !q;
+      (* assert { (reverse (Cons p (model next tmp))) ++ (model next q) = *)
+      (*          (reverse (model next tmp)) ++ (Cons p (model next q))}; *)
+      q := !p;
+      p:= tmp
+    done;
+    q
+    { is_list next result /\ reverse (model (old next) (old p)) =
+        model next result}
+
+
 end
 
 (*

examples/programs/list_rev/list_rev.mlw_M2_frame_list_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Parameter ref : forall (a:Type), Type.
+
+Parameter t : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (t a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b  -> (t a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t a b)), forall (a1:a)
+  (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(t a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter create_const: forall (b:Type) (a:Type), b  -> (t a b).
+
+Set Contextual Implicit.
+Implicit Arguments create_const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (create_const(b1):(t a b)) a1) = b1).
+
+Parameter pointer : Type.
+
+Definition next  := (t pointer pointer).
+
+Parameter null:  pointer.
+
+
+Parameter value:  (t pointer Z).
+
+
+Parameter next1:  (t pointer pointer).
+
+
+Inductive is_list : (t pointer pointer) -> pointer -> Prop :=
+  | is_list_null : forall (next2:(t pointer pointer)) (p:pointer),
+      (p = (null )) -> (is_list next2 p)
+  | is_list_next : forall (next3:(t pointer pointer)) (p:pointer),
+      (~ (p = (null ))) -> ((is_list next3 (get next3 p)) -> (is_list next3
+      p)).
+
+Parameter ft : forall (a:Type), Type.
+
+Parameter in_ft: pointer -> (ft pointer)  -> Prop.
+
+
+Parameter list_ft: (t pointer pointer) -> pointer  -> (ft pointer).
+
+
+Axiom list_ft_node_null_cor : forall (next4:(t pointer pointer)) (q:pointer)
+  (p:pointer), (q = (null )) -> ~ (in_ft p (list_ft next4 q)).
+
+Axiom list_ft_node_next1 : forall (next5:(t pointer pointer)) (q:pointer)
+  (p:pointer), (~ (q = (null ))) -> ((is_list next5 (get next5 q)) ->
+  ((in_ft p (list_ft next5 (get next5 q))) -> (in_ft p (list_ft next5 q)))).
+
+Axiom list_ft_node_next2 : forall (next6:(t pointer pointer)) (q:pointer),
+  (~ (q = (null ))) -> ((is_list next6 (get next6 q)) -> (in_ft q
+  (list_ft next6 q))).
+
+Axiom list_ft_node_next_inv : forall (next7:(t pointer pointer)) (q:pointer)
+  (p:pointer), (~ (q = (null ))) -> ((is_list next7 (get next7 q)) ->
+  ((~ (q = p)) -> ((in_ft p (list_ft next7 q)) -> (in_ft p (list_ft next7
+  (get next7 q)))))).
+
+Theorem frame_list : forall (next8:(t pointer pointer)) (p:pointer)
+  (q:pointer) (v:pointer), (~ (in_ft q (list_ft next8 p))) -> ((is_list next8
+  p) -> (is_list (set next8 q v) p)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros.
+induction H0.
+apply (is_list_null _ _ H0).
+apply (is_list_next _ _ H0).
+assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H1)).
+rewrite (Select_neq _ _ _ _ _ _ H2).
+apply IHis_list.
+contradict H.
+exact (list_ft_node_next1 _ _ _ H0 H1 H).
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/list_rev/list_rev.mlw_M2_frame_list_ft_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Definition ref (a:Type) := a.
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b  -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter create_const: forall (b:Type) (a:Type), b  -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments create_const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (create_const(b1):(map a b)) a1) = b1).
+
+Parameter pointer : Type.
+
+Axiom pointer_dec : forall (p1:pointer) (p2:pointer), (p1 = p2) \/
+  ~ (p1 = p2).
+
+Definition next  := (map pointer pointer).
+
+Parameter null:  pointer.
+
+
+Parameter value:  (map pointer Z).
+
+
+Parameter next1:  (map pointer pointer).
+
+
+Inductive is_list : (map pointer pointer) -> pointer -> Prop :=
+  | is_list_null : forall (next2:(map pointer pointer)) (p:pointer),
+      (p = (null )) -> (is_list next2 p)
+  | is_list_next : forall (next2:(map pointer pointer)) (p:pointer),
+      (~ (p = (null ))) -> ((is_list next2 (get next2 p)) -> (is_list next2
+      p)).
+
+Parameter ft : forall (a:Type), Type.
+
+Parameter in_ft: pointer -> (ft pointer)  -> Prop.
+
+
+Axiom set_eq : forall (ft1:(ft pointer)) (ft2:(ft pointer)),
+  (forall (q:pointer), (in_ft q ft1) <-> (in_ft q ft2)) -> (ft1 = ft2).
+
+Parameter list_ft: (map pointer pointer) -> pointer  -> (ft pointer).
+
+
+Axiom list_ft_node_null_cor : forall (next2:(map pointer pointer))
+  (q:pointer) (p:pointer), (q = (null )) -> ~ (in_ft p (list_ft next2 q)).
+
+Axiom list_ft_node_next1 : forall (next2:(map pointer pointer)) (q:pointer)
+  (p:pointer), (~ (q = (null ))) -> ((is_list next2 (get next2 q)) ->
+  ((in_ft p (list_ft next2 (get next2 q))) -> (in_ft p (list_ft next2 q)))).
+
+Axiom list_ft_node_next2 : forall (next2:(map pointer pointer)) (q:pointer),
+  (~ (q = (null ))) -> ((is_list next2 (get next2 q)) -> (in_ft q
+  (list_ft next2 q))).
+
+Axiom list_ft_node_next_inv : forall (next2:(map pointer pointer))
+  (q:pointer) (p:pointer), (~ (q = (null ))) -> ((is_list next2 (get next2
+  q)) -> ((~ (q = p)) -> ((in_ft p (list_ft next2 q)) -> (in_ft p
+  (list_ft next2 (get next2 q)))))).
+
+Axiom frame_list : forall (next2:(map pointer pointer)) (p:pointer)
+  (q:pointer) (v:pointer), (~ (in_ft q (list_ft next2 p))) -> ((is_list next2
+  p) -> (is_list (set next2 q v) p)).
+
+Definition sep_node_list(next2:(map pointer pointer)) (p1:pointer)
+  (p2:pointer): Prop := ~ (in_ft p1 (list_ft next2 p2)).
+
+Theorem frame_list_ft : forall (next2:(map pointer pointer)) (p:pointer)
+  (q:pointer) (v:pointer), (~ (in_ft q (list_ft next2 p))) -> ((is_list next2
+  p) -> ((list_ft next2 p) = (list_ft (set next2 q v) p))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros.
+apply set_eq.
+intros.
+split;intro.
+(** First part *)
+induction H0.
+apply (list_ft_node_null_cor _ _ _ H0) in H1;contradiction.
+(* some asserts *)
+assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H2)).
+assert  (H2' : is_list (set next2 q v) (get (set next2 q v) p))
+by (rewrite (Select_neq _ _ _ _ _ v H3);refine (frame_list _ _ _ _ _ H2);contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H)).
+(* *)
+destruct (pointer_dec p q0).
+rewrite <- H4.
+exact (list_ft_node_next2 _ p H0 H2').
+(* p <> q0 *)
+apply (list_ft_node_next1 _ _ _ H0 H2').
+rewrite (Select_neq _ _ _ _ _ _ H3).
+apply IHis_list.
+contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H).
+exact (list_ft_node_next_inv _ _ _ H0 H2 H4 H1).
+(** Second part *)
+induction H0.
+apply (list_ft_node_null_cor _ _ _ H0) in H1;contradiction.
+(* some asserts *)
+assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H2)).
+assert  (H2' : is_list (set next2 q v) (get (set next2 q v) p))
+by (rewrite (Select_neq _ _ _ _ _ v H3);refine (frame_list _ _ _ _ _ H2);contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H)).
+(* *)