(* * Seplog is an implementation of separation logic (an extension of Hoare * logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the * Coq proof assistant (version 8, http://coq.inria.fr) together with a * sample verification of the heap manager of the Topsy operating system * (version 2, http://www.topsy.net). More information is available at * http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog. * * Copyright (c) 2005, 2006 Reynald Affeldt and Nicolas Marti * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA *) Load seplog_header. Open Local Scope Z_scope. (****************************************************************************) (* GCD *) (****************************************************************************) Require Import Znumtheory. Definition gcd_prog a b x y := x <- int_e a; y <- int_e b; while (var_e x =/= var_e y) ( ifte (var_e y >> var_e x) thendo (y <- var_e y -e var_e x) elsedo (x <- var_e x -e var_e y) ). Lemma gcd_verif : forall a b x y, var.set (x::y::nil) -> {{ fun s h => 0 < a /\ 0 < b }} gcd_prog a b x y {{ fun s h => exists vx, exists vy, exists d, store.lookup x s = vx /\ store.lookup y s = vy /\ Zis_gcd vx vy d /\ Zis_gcd a b d }}. intros. unfold gcd_prog. (******************** x <- int_e a; ********************) apply semax_assign'' with (fun s (_:heap.h) => 0 < a /\ 0 < b /\ store.lookup x s = a). red; intros; red. rewrite store.lookup_update'. tauto. (******************** x <- int_e b; ********************) apply semax_assign'' with (fun s (_:heap.h) => 0 < a /\ 0 < b /\ store.lookup x s = a /\ store.lookup y s = b). red; intros; red. elim store.lookup_update. rewrite store.lookup_update'. tauto. simpl in H; tauto. (******************** while (var_e x =/= var_e y) ********************) apply semax_strengthen_pre with (fun s (_:heap.h) => exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\ store.lookup x s = vx /\ store.lookup y s = vy /\ Zis_gcd vx vy d /\ Zis_gcd a b d). red; intros. exists a; exists b. generalize (Zgcd_spec a b); intro X; inversion_clear X as [d]. exists d; tauto. apply semax_weaken_post with (fun s (_:heap.h) => (exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\ store.lookup x s = vx /\ store.lookup y s = vy /\ Zis_gcd vx vy d /\ Zis_gcd a b d) /\ eval_b (var_e x =/= var_e y) s = false ). red; intros. inversion_clear H0. inversion_clear H1 as [vx]. inversion_clear H0 as [vy]. inversion_clear H1 as [d]. exists vx; exists vy; exists d. tauto. apply semax_while with (P:=fun s (_:heap.h) => (exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\ store.lookup x s = vx /\ store.lookup y s = vy /\ Zis_gcd vx vy d /\ Zis_gcd a b d)). (******************** ifte var_e y >> var_e x ********************) apply semax_ifte. (******************** y <- var_e y -e var_e x ********************) apply semax_assign'. red; intros. inversion_clear H0. inversion_clear H1. inversion_clear H0 as [vx]. inversion_clear H1 as [vy]. inversion_clear H0 as [d]. decompose [and] H1; clear H1. red. exists vx; exists (vy-vx); exists d. elim store.lookup_update. rewrite store.lookup_update'. split; trivial. split. simpl in H2. assert (vy > vx). apply Zgt_bool_true. rewrite <-H4; rewrite <-H6; assumption. omega. split; trivial. split. simpl. rewrite <-H4; rewrite <-H6; reflexivity. split; trivial. cutrewrite (vy-vx = vx * (-1) + vy); [idtac | ring]. apply Zis_gcd_for_euclid2. apply Zis_gcd_sym. assumption. simpl in H; tauto. (********************* }x <- var_e x -e var_e y ********************) apply semax_assign'. red; intros. inversion_clear H0. inversion_clear H1. inversion_clear H0 as [vx]. inversion_clear H1 as [vy]. inversion_clear H0 as [d]. decompose [and] H1; clear H1. red. exists (vx-vy); exists vy; exists d. rewrite store.lookup_update'. elim store.lookup_update. split. assert (vy < vx). apply Zle_neq_lt. simpl in H2; simpl in H3. apply Zgt_bool_false. rewrite <-H4; rewrite <-H6; assumption. apply Zeq_bool_false'. apply negb_true_is_false. rewrite Zeq_bool_sym. rewrite <-H4; rewrite <-H6; assumption. omega. split; trivial. split. simpl. rewrite <-H4; rewrite <-H6; reflexivity. split; trivial. split; trivial. apply Zis_gcd_sym. cutrewrite (vx - vy = vy * (-1) + vx); [idtac | ring]. apply Zis_gcd_for_euclid2. assumption. simpl in H. firstorder. Qed. (****************************************************************************) (* Factorial *) (****************************************************************************) (* Axiomatic definition of the factorial function *) Axiom facto : Z -> Z. Axiom facto_neg : forall z, z < 0 -> (facto z)=1. Axiom facto_zero : (facto 0)=1. Axiom facto_pos : forall z, z > 0 -> (facto z)=z*(facto (z - 1)). Lemma factorial : forall n, 0 <= n -> forall x m, var.set (x::m::nil) -> {{ fun s h => store.lookup m s = n /\ store.lookup x s = 1 }} while (var_e m =/= int_e 0%Z) ( x <- var_e x *e var_e m; m <- var_e m -e int_e 1 ) {{ fun s h => store.lookup x s = facto n }}. intros n n_pos x m Hvars. apply semax_strengthen_pre with (fun s (_:heap.h) => store.lookup x s * facto (store.lookup m s) = facto n /\ store.lookup m s >= 0). red; intros. inversion_clear H. rewrite H0. rewrite H1. omega. apply semax_weaken_post with (fun s (_:heap.h) => (store.lookup x s * facto (store.lookup m s) = facto n /\ store.lookup m s >= 0) /\ eval_b (var_e m =/= int_e 0) s = false). red; intros. decompose [and] H; clear H. assert (store.lookup m s = 0). Omega_exprb. rewrite H in H2. rewrite facto_zero in H2. unfold val. omega. apply semax_while with (P:=fun s (_:heap.h) => store.lookup x s * facto (store.lookup m s) = facto n /\ store.lookup m s >= 0). apply semax_assign'' with (fun s (_:heap.h) => store.lookup x s * facto (store.lookup m s - 1) = facto n /\ store.lookup m s - 1 >= 0 ). red; intros. red. simpl. decompose [and] H; clear H. rewrite store_lookup_update'. rewrite (store_lookup_update m x). rewrite <-H2. pattern (facto (store.lookup m s)). rewrite facto_pos. split. ring. Omega_exprb. Omega_exprb. simpl in Hvars; intuition. apply semax_assign'. red; intros. red. rewrite (store_lookup_update x m). rewrite store_lookup_update'. auto. simpl in Hvars; intuition. Qed. Open Local Scope vc_scope. Lemma vc_factorial : forall n, n >= 0 -> forall x m, var.set (x::m::nil) -> {{ fun s (_:heap.h) => store.lookup m s = n /\ store.lookup x s = 1 }} proj_cmd (while' ((var_e m) =/= int_e 0) (fun s (_:heap.h) => store.lookup x s * facto (store.lookup m s) = facto n /\ store.lookup m s >= 0) (x <- var_e x *e var_e m; m <- var_e m -e int_e 1)) {{ fun s (_:heap.h) => store.lookup x s = facto n }}. intros n Hpos x m Hvars. apply wp_vc_util. intros. (* vc *) simpl. unfold update_store2. simpl. rewrite store_lookup_update'. rewrite (store_lookup_update x m). rewrite store_lookup_update'. rewrite (store_lookup_update m x). split. intros. decompose [and] H; clear H. rewrite <-H2. assert (Zeq_bool (store.lookup m s) 0 = true). apply negb_false_is_true; auto. rewrite (Zeq_bool_true _ _ H). rewrite facto_zero. unfold val; ring. split. intros. decompose [and] H; clear H. rewrite <-H2. split. pattern (facto (store.lookup m s)). rewrite facto_pos. ring. assert (store.lookup m s <> 0). assert (Zeq_bool (store.lookup m s) 0 = false). apply negb_true_is_false; auto. generalize (Zeq_bool_false (store.lookup m s) 0); intro X; inversion_clear X; auto. generalize H3 H; clear H3 H; unfold val; intros; omega. assert (store.lookup m s <> 0). assert (Zeq_bool (store.lookup m s) 0 = false). apply negb_true_is_false; auto. generalize (Zeq_bool_false (store.lookup m s) 0); intro X; inversion_clear X; auto. generalize H3 H; clear H3 H; unfold val; intros; omega. unfold TT; auto. simpl in Hvars; intuition. simpl in Hvars; intuition. (* wp *) intros. simpl. split. inversion_clear H. rewrite H0. rewrite H1. ring. inversion_clear H; subst n; auto. Qed. Close Local Scope vc_scope. (***********************************************************************) (* Swap *) (***********************************************************************) Lemma swap: forall x y z v a b, var.set (x::y::z::v::nil) -> {{ (var_e x |-> int_e a) ** (var_e y |-> int_e b) }} z <-* var_e x; v <-* var_e y; var_e x *<- var_e v; var_e y *<- var_e z {{ (var_e x |-> int_e b) ** (var_e y |-> int_e a) }}. intros. apply semax_lookup_backwards'' with (fun s h => ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\ eval (var_e z) s = a ). red; intros. Decompose_sepcon H0 h1 h2. exists (int_e a). Compose_sepcon h1 h2. auto. Intro_sepimp h1' h'. red. split. Compose_sepcon h1' h2. Mapsto. Mapsto. Store_update. apply semax_lookup_backwards'' with (fun s h => ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\ eval (var_e z) s = a /\ eval (var_e v) s = b ). red; intros. inversion_clear H0. Decompose_sepcon H1 h1 h2. simpl in H2. exists (int_e b). Compose_sepcon h2 h1. auto. Intro_sepimp h2' h'. red. split. Compose_sepcon h1 h2'. Mapsto. Mapsto. split; [Store_update | Store_update]. apply semax_mutation_backwards'' with (fun s h => ((var_e x |-> int_e b) ** (var_e y |-> int_e b)) s h /\ eval (var_e z) s = a /\ eval (var_e v) s = b ). red; intros. decompose [and] H0; clear H0. Decompose_sepcon H1 h1 h2. exists (int_e a). Compose_sepcon h1 h2. auto. Intro_sepimp h1' h'. split. Compose_sepcon h1' h2. Mapsto. Mapsto. auto. apply semax_mutation_backwards'. red; intros. decompose [and] H0; clear H0. Decompose_sepcon H1 h1 h2. exists (int_e b). Compose_sepcon h2 h1. auto. Intro_sepimp h2' h'. Compose_sepcon h1 h2'. Mapsto. Mapsto. Qed. Open Local Scope vc_scope. Lemma vc_swap: forall x y z v a b, var.set (x::y::z::v::nil) -> {{ (var_e x |-> int_e a) ** (var_e y |-> int_e b) }} proj_cmd (z <-*var_e x; v <-* var_e y; var_e x *<- var_e v; var_e y *<- var_e z) {{ (var_e x |-> int_e b) ** (var_e y |-> int_e a) }}. intros. apply wp_vc_util. (* vc *) intros. simpl. unfold TT. intuition. (* wp *) intros. simpl. exists (int_e a). generalize H0; clear H0. apply sep.monotony. split. auto. intros. generalize H0; clear H0. apply sep.adjunction. intros. red. exists (int_e b). simpl. assert (((var_e y |-> int_e b) ** (var_e x |-> int_e a)) (store.update z (eval (int_e a) s) s) h0). apply inde_update_store. apply inde_sep_con. apply inde_mapsto. simpl. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inde_mapsto. simpl. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. auto. generalize H1; clear H1. apply sep.monotony. split. auto. intros. generalize H1; clear H1. apply sep.adjunction. intros. red. simpl. exists (int_e a). assert (((var_e x |-> int_e a) ** (var_e y |-> int_e b)) (store.update v b (store.update z a s)) h1). apply inde_update_store. apply inde_sep_con. apply inde_mapsto. simpl. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inde_mapsto. simpl. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. apply inter_weak. apply inter_nil. simpl. simpl in H; intuition. auto. generalize H2; clear H2. apply sep.monotony. split. auto. intros. generalize H2; clear H2. apply sep.adjunction. intros. exists (int_e b). generalize H2; clear H2. apply sep.monotony. split. auto. intros. generalize H2; clear H2. apply sep.adjunction. intros. inversion_clear H2. inversion_clear H3. decompose [and] H2; clear H2. inversion_clear H4. inversion_clear H2. exists x0. inversion_clear H7. inversion_clear H2. exists x1. split; auto. split; auto. split. exists x2. split; auto. simpl. simpl in H6. rewrite H6. rewrite store_lookup_update'. auto. simpl in H8. red. exists x3. simpl; simpl in H7. split; auto. rewrite H8. rewrite (store_lookup_update z v). rewrite store_lookup_update'. auto. Var_uneq. Qed. Close Local Scope vc_scope. (***********************************************************************) (* Buffer overflow *) (***********************************************************************) (* for (c1=buf, c2=s; ( *c1++ = *c2++ )!=0) *) Definition buffer_overflow c1 c2 buf str str_tmp := c1 <- var_e buf; c2 <- var_e str; str_tmp <-* var_e c2; while (var_e str_tmp =/= int_e 0) ( var_e c1 *<- var_e str_tmp; c1 <- var_e c1 +e int_e 1; c2 <- var_e c2 +e int_e 1; str_tmp <-* var_e c2 ).