diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 326dbc1..c3ff11a 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -114,7 +114,7 @@ Qed. Lemma list_last_cons: forall (a: Z) (l: list Z), l <> nil -> - last (a :: l) 0 = last l 0. + last (a :: l) 1 = last l 1. Proof. intros. destruct l. @@ -125,11 +125,11 @@ Qed. Lemma list_last_to_Znth: forall (l: list Z), l <> nil -> - last l 0 = Znth ((Zlength l) - 1) l 0. + last l 1 = Znth ((Zlength l) - 1) l 0. Proof. intros. induction l. - + auto. + + contradiction. + destruct l. - simpl. rewrite Znth0_cons. @@ -236,8 +236,8 @@ Proof. sep_apply store_array_rec_false; [ entailer! | lia ]. Qed. -Lemma store_uarray_rec_equals_store_uarray: forall x lo hi l, - lo < hi -> +Lemma uint_array_rec_to_uint_array: forall x lo hi l, + lo <= hi -> store_uint_array_rec x lo hi l --||-- store_uint_array (x + sizeof(UINT) * lo) (hi - lo) l. Proof. @@ -258,5 +258,88 @@ Proof. + sep_apply H1. entailer!. Qed. - + +Lemma store_uint_array_single: forall x n a, + store_uint_array_rec x n (n + 1) [a] --||-- + (x + n * sizeof(UINT)) # UInt |-> a. +Proof. + intros. + unfold store_uint_array_rec. + simpl. + split; entailer!. +Qed. + +Lemma store_undef_uint_array_single: forall x n a, + (x + n * sizeof(UINT)) # UInt |-> a |-- + store_undef_uint_array_rec x n (n + 1). +Proof. + intros. + unfold store_undef_uint_array_rec. + assert (Z.to_nat (n + 1 - n) = S O). { lia. } + rewrite H; clear H. + simpl. + entailer!. + sep_apply store_uint_undef_store_uint. + entailer!. +Qed. + +Lemma store_uint_array_single_to_undef: forall x n a, + store_uint_array_rec x n (n + 1) [a] |-- + store_undef_uint_array_rec x n (n + 1). +Proof. + intros. + pose proof (store_uint_array_single x n a). + destruct H as [H _]. + sep_apply H. + sep_apply store_undef_uint_array_single. + entailer!. +Qed. + +Lemma store_uint_array_divide_rec: forall x n l m, + 0 <= m <= n -> + Zlength l = n -> + store_uint_array x n l --||-- + store_uint_array x m (sublist 0 m l) ** + store_uint_array_rec x m n (sublist m n l). +Proof. + intros. + pose proof (store_uint_array_divide x n l m H H0). + pose proof (uint_array_rec_to_uint_array x m n (sublist m n l) ltac:(lia)). + destruct H2 . + destruct H1. + rewrite Z.mul_comm in H2, H3. + rewrite H3 in H1. + rewrite <-H2 in H4. + clear H2 H3. + split; tauto. +Qed. + +Lemma store_undef_uint_array_rec_divide: forall x l mid r, + 0 <= l <= r -> + l <= mid <= r -> + store_undef_uint_array_rec x l r --||-- + store_undef_uint_array_rec x l mid ** store_undef_uint_array_rec x mid r. +Proof. + intros. + unfold store_undef_uint_array_rec. + pose proof (store_undef_array_divide (x + l * sizeof(UINT)) (r - l) (mid - l) (sizeof(UINT)) + (fun x => x # UInt |->_) + (fun x0 lo => (x0 + lo * sizeof(UINT)) # UInt |->_) ltac:(lia) ltac:(reflexivity)). + unfold store_undef_array in H1. + pose (fun (l: Z) (n: Z) (len: nat) => store_undef_array_rec_base x 0 l n len (sizeof(UINT)) + (fun x => x # UInt |->_) + (fun x0 lo => (x0 + lo * sizeof(UINT)) # UInt |->_) ltac:(reflexivity)). + rewrite <-(l0 l r (Z.to_nat (r - l))) in H1. + rewrite <-(l0 l mid (Z.to_nat (mid - l))) in H1. + assert (r - l - (mid - l) = r - mid). { lia. } + rewrite H2 in H1; clear H2. + rewrite <-Z.add_assoc, <-Z.mul_add_distr_r in H1. + assert (l + (mid - l) = mid). { lia. } + rewrite H2 in H1; clear H2. + rewrite <-(l0 mid r (Z.to_nat (r - mid))) in H1. + repeat rewrite Z.add_0_l in H1. + clear l0. + rewrite H1. + split; entailer!. +Qed. End Aux. \ No newline at end of file diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 8c2e754..787c79e 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -28,7 +28,7 @@ Module Internal. Definition mpd_store_list (ptr: addr) (data: list Z) (cap: Z): Assertion := [| Zlength data <= cap |] && [| cap <= LENGTH_MAX |] && store_uint_array ptr (Zlength data) data ** - store_undef_uint_array_rec ptr ((Zlength data) + 1) cap. + store_undef_uint_array_rec ptr (Zlength data) cap. Fixpoint list_to_Z (data: list Z): Z := match data with @@ -50,7 +50,7 @@ Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := [| list_store_Z data n |] && [| size = Zlength data |] && mpd_store_list ptr data cap. Definition list_store_Z_compact (data: list Z) (n: Z): Prop := - list_to_Z data = n /\ last data 0 >= 1 /\ list_within_bound data. + list_to_Z data = n /\ last data 1 >= 1 /\ list_within_bound data. Definition mpd_store_Z_compact (ptr: addr) (n size cap: Z): Assertion := EX data, @@ -58,7 +58,7 @@ Definition mpd_store_Z_compact (ptr: addr) (n size cap: Z): Assertion := Lemma list_store_Z_normal_to_compact: forall (data: list Z) (n: Z), list_store_Z data n -> - last data 0 >= 1 -> + last data 1 >= 1 -> list_store_Z_compact data n. Proof. unfold list_store_Z_compact, list_store_Z. @@ -122,6 +122,29 @@ Proof. tauto. Qed. +Lemma list_within_bound_Znth: forall (l: list Z) (i: Z), + 0 <= i < Zlength l -> + list_within_bound l -> + 0 <= Znth i l 0 < UINT_MOD. +Proof. + intros. + revert i H. + induction l; intros. + + rewrite Zlength_nil in H. + lia. + + assert (i = 0 \/ i > 0). { lia. } + destruct H1. + - rewrite H1. + rewrite (Znth0_cons a l 0). + simpl in H0. + lia. + - rewrite Znth_cons; try lia. + simpl in H0; destruct H0. + rewrite Zlength_cons in H; unfold Z.succ in H. + specialize (IHl H2 (i - 1) ltac:(lia)). + lia. +Qed. + Lemma __list_within_bound_split_r: forall (l1: list Z) (a: Z), list_within_bound (l1 ++ [a]) -> list_within_bound l1 /\ 0 <= a < UINT_MOD. @@ -516,7 +539,7 @@ Proof. auto. } pose proof (list_store_Z_bound l2 n2 H1) as Hn2. - pose proof (@app_removelast_last Z l2 0 H4). + pose proof (@app_removelast_last Z l2 1 H4). rewrite H5 in H1. apply list_store_Z_split in H1; destruct H1. rewrite (Aux.Zlength_removelast l2) in H1, H6; try auto. diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 39ce9b4..bbb692e 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -194,7 +194,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "s" ) )) # Ptr |-> s_pre) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) |-- [| (0 <= INT_MAX) |] && [| ((INT_MIN) <= 0) |] @@ -225,7 +225,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** ((( &( "d" ) )) # Ptr |-> d) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** ((( &( "s" ) )) # Ptr |-> s) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| ((i + 1 ) <= INT_MAX) |] && [| ((INT_MIN) <= (i + 1 )) |] @@ -243,7 +243,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && (store_uint_array_rec d_pre 0 cap2 l2 ) ** (store_uint_array d_pre 0 nil ) ** (store_uint_array s_pre n_pre l_2 ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) |-- EX (l': (@list Z)) (l: (@list Z)) , [| (0 <= 0) |] @@ -259,7 +259,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** (store_uint_array d_pre 0 (sublist (0) (0) (l)) ) ** (store_uint_array_rec d_pre 0 cap2 l' ) . @@ -285,7 +285,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) && (store_uint_array d (i + 1 ) (replace_Znth (i) ((Znth i l_3 0)) ((app ((sublist (0) (i) (l_3))) ((cons (a) (nil)))))) ) ** (store_uint_array s n l_3 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- EX (l': (@list Z)) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -301,7 +301,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d (i + 1 ) (sublist (0) ((i + 1 )) (l)) ) ** (store_uint_array_rec d (i + 1 ) cap2 l' ) . @@ -322,7 +322,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d i (sublist (0) (i) (l)) ) ** (store_uint_array_rec d i cap2 l' ) |-- @@ -354,7 +354,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "s" ) )) # Ptr |-> s_pre) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** ((( &( "d" ) )) # Ptr |-> d_pre) ** (store_uint_array d_pre cap2 l2 ) |-- @@ -370,7 +370,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** (store_uint_array d_pre cap2 l2 ) |-- [| ((Zlength (l2)) = cap2) |] @@ -382,7 +382,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| (cap2 >= n_pre) |] && (store_uint_array d_pre cap2 l2 ) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) . Definition mpn_copyi_partial_solve_wit_2 := mpn_copyi_partial_solve_wit_2_pure -> mpn_copyi_partial_solve_wit_2_aux. @@ -406,7 +406,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) ** ((( &( "n" ) )) # Int |-> n) ** ((( &( "s" ) )) # Ptr |-> s) ** (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** ((( &( "d" ) )) # Ptr |-> d) ** (store_uint_array d i (sublist (0) (i) (l)) ) ** (store_uint_array_rec d i cap2 l' ) @@ -432,7 +432,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d i (sublist (0) (i) (l_2)) ) ** (store_uint_array_rec d i cap2 l' ) |-- @@ -455,7 +455,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array_rec d i cap2 l' ) ** (store_uint_array d i (sublist (0) (i) (l_2)) ) ** (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_partial_solve_wit_3 := mpn_copyi_partial_solve_wit_3_pure -> mpn_copyi_partial_solve_wit_3_aux. @@ -481,7 +481,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) ** (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| (l' = (cons (a) (l2'))) |] && [| (i < n) |] @@ -503,7 +503,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** (store_uint_array_missing_i_rec s i 0 n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_partial_solve_wit_5 := @@ -527,7 +527,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array s n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| (l' = (cons (a) (l2'))) |] && [| (i < n) |] @@ -549,7 +549,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** (store_uint_array_missing_i_rec d i 0 (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) ** (store_uint_array s n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_which_implies_wit_1 := @@ -562,7 +562,7 @@ forall (cap1: Z) (val: Z) (n: Z) (s: Z) , && [| (cap1 <= 100000000) |] && [| (list_store_Z l val ) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_which_implies_wit_2 := @@ -606,8 +606,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) @@ -637,8 +637,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && ((( &( "n" ) )) # Int |-> n) ** (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -670,8 +670,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -702,8 +702,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -735,8 +735,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -767,8 +767,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -798,8 +798,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && ((( &( "n" ) )) # Int |-> n) ** (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -820,8 +820,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| ((-1) <= (n_pre - 1 )) |] && [| ((n_pre - 1 ) < n_pre) |] @@ -841,8 +841,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_entail_wit_2 := @@ -867,8 +867,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| ((-1) <= (n - 1 )) |] && [| ((n - 1 ) < n_pre) |] @@ -888,8 +888,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_return_wit_1_1 := @@ -915,8 +915,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| ((-1) = (-1)) |] @@ -957,8 +957,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| (1 = (-1)) |] @@ -997,8 +997,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| (0 = (-1)) |] @@ -1056,8 +1056,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| (n >= 0) |] && [| ((-1) <= n) |] @@ -1079,8 +1079,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (((ap_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l1 0)) ** (store_uint_array_missing_i_rec ap_pre n 0 n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_partial_solve_wit_3 := @@ -1104,8 +1104,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| (n >= 0) |] && [| ((-1) <= n) |] @@ -1127,8 +1127,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (((bp_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l2 0)) ** (store_uint_array_missing_i_rec bp_pre n 0 n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_which_implies_wit_1 := @@ -1143,8 +1143,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n_pre = (Zlength (l2))) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . (*----- Function mpn_cmp4 -----*) @@ -1475,6 +1475,284 @@ forall (bn_pre: Z) (an_pre: Z) (cap2: Z) , && emp . +(*----- Function mpn_normalized_size -----*) + +Definition mpn_normalized_size_safety_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_normalized_size_safety_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| ((n - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n - 1 )) |] +. + +Definition mpn_normalized_size_safety_wit_3 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_normalized_size_safety_wit_4 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_normalized_size_safety_wit_5 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) = 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| ((n - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n - 1 )) |] +. + +Definition mpn_normalized_size_entail_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) , + [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n_pre (sublist (0) (n_pre) (l)) ) + ** (store_undef_uint_array_rec xp_pre n_pre cap ) +|-- + [| (n_pre >= 0) |] + && [| (n_pre <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n_pre (sublist (0) (n_pre) (l)) ) + ** (store_undef_uint_array_rec xp_pre n_pre cap ) +. + +Definition mpn_normalized_size_entail_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) = 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| ((n - 1 ) >= 0) |] + && [| ((n - 1 ) <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) ((n - 1 )) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre (n - 1 ) (sublist (0) ((n - 1 )) (l)) ) + ** (store_undef_uint_array_rec xp_pre (n - 1 ) cap ) +. + +Definition mpn_normalized_size_return_wit_1_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n <= 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (0 <= n) |] + && [| (n <= cap) |] + && (mpd_store_Z_compact xp_pre val n cap ) +. + +Definition mpn_normalized_size_return_wit_1_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) <> 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (0 <= n) |] + && [| (n <= cap) |] + && (mpd_store_Z_compact xp_pre val n cap ) +. + +Definition mpn_normalized_size_partial_solve_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) , + [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (mpd_store_Z xp_pre val n_pre cap ) +|-- + [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (mpd_store_Z xp_pre val n_pre cap ) +. + +Definition mpn_normalized_size_partial_solve_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (((xp_pre + ((n - 1 ) * sizeof(UINT) ) )) # UInt |-> (Znth (n - 1 ) (sublist (0) (n) (l)) 0)) + ** (store_uint_array_missing_i_rec xp_pre (n - 1 ) 0 n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +. + +Definition mpn_normalized_size_which_implies_wit_1 := +forall (xp_pre: Z) (val: Z) (cap: Z) (n: Z) , + (mpd_store_Z xp_pre val n cap ) +|-- + EX (l: (@list Z)) , + [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| ((Zlength (l)) = n) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -1533,5 +1811,17 @@ Axiom proof_of_mpn_cmp4_partial_solve_wit_1 : mpn_cmp4_partial_solve_wit_1. Axiom proof_of_mpn_cmp4_partial_solve_wit_2_pure : mpn_cmp4_partial_solve_wit_2_pure. Axiom proof_of_mpn_cmp4_partial_solve_wit_2 : mpn_cmp4_partial_solve_wit_2. Axiom proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. +Axiom proof_of_mpn_normalized_size_safety_wit_1 : mpn_normalized_size_safety_wit_1. +Axiom proof_of_mpn_normalized_size_safety_wit_2 : mpn_normalized_size_safety_wit_2. +Axiom proof_of_mpn_normalized_size_safety_wit_3 : mpn_normalized_size_safety_wit_3. +Axiom proof_of_mpn_normalized_size_safety_wit_4 : mpn_normalized_size_safety_wit_4. +Axiom proof_of_mpn_normalized_size_safety_wit_5 : mpn_normalized_size_safety_wit_5. +Axiom proof_of_mpn_normalized_size_entail_wit_1 : mpn_normalized_size_entail_wit_1. +Axiom proof_of_mpn_normalized_size_entail_wit_2 : mpn_normalized_size_entail_wit_2. +Axiom proof_of_mpn_normalized_size_return_wit_1_1 : mpn_normalized_size_return_wit_1_1. +Axiom proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_wit_1_2. +Axiom proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1. +Axiom proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. +Axiom proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1. End VC_Correct. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 92895cf..153a2b3 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -117,3 +117,27 @@ Proof. Admitted. Lemma proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. Proof. Admitted. +Lemma proof_of_mpn_normalized_size_safety_wit_1 : mpn_normalized_size_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_2 : mpn_normalized_size_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_3 : mpn_normalized_size_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_4 : mpn_normalized_size_safety_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_5 : mpn_normalized_size_safety_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_entail_wit_1 : mpn_normalized_size_entail_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 2f1ddf3..8aedbd0 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -134,14 +134,14 @@ Proof. unfold store_uint_array, store_array. simpl. entailer!. - + pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 i (sublist 0 i l) ltac:(lia)). + + pose proof (Aux.uint_array_rec_to_uint_array d 0 i (sublist 0 i l) ltac:(lia)). destruct H4 as [_ H4]. assert (d + sizeof(UINT) * 0 = d). { lia. } rewrite H5 in H4; clear H5. assert (i - 0 = i). { lia. } rewrite H5 in H4; clear H5. sep_apply H4; clear H4. - pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 (i + 1) (sublist 0 i l ++ z :: nil) ltac:(lia)). + pose proof (Aux.uint_array_rec_to_uint_array d 0 (i + 1) (sublist 0 i l ++ z :: nil) ltac:(lia)). destruct H4 as [H4 _]. assert (i + 1 - 0 = i + 1). { lia. } rewrite H5 in H4; clear H5. @@ -151,11 +151,6 @@ Proof. sep_apply store_uint_array_rec_tail_merge; [ reflexivity | lia ]. Qed. -Lemma proof_of_mpn_cmp_safety_wit_1 : mpn_cmp_safety_wit_1. -Proof. - pre_process. -Qed. - Lemma proof_of_mpn_cmp_entail_wit_1 : mpn_cmp_entail_wit_1. Proof. pre_process. @@ -296,4 +291,123 @@ Proof. Intros l1 l2. Exists l1 l2. entailer!. +Qed. + +Lemma proof_of_mpn_normalized_size_entail_wit_2 : mpn_normalized_size_entail_wit_2. +Proof. + pre_process. + entailer!. + + pose proof (store_uint_array_divide_rec + xp_pre n (sublist 0 n l) (n - 1) ltac:(lia)). + rewrite (Zlength_sublist0 n l ltac:(lia)) in H12. + specialize (H12 ltac:(lia)). + destruct H12 as [H12 _]. + rewrite H12; clear H12. + rewrite (sublist_sublist00 (n - 1) n l ltac:(lia)). + rewrite (sublist_sublist0 n n (n - 1) l ltac:(lia) ltac:(lia)). + pose proof (Aux.uint_array_rec_to_uint_array xp_pre 0 (n - 1) (sublist 0 (n - 1) l) ltac:(lia)). + destruct H12 as [H12 _]. + rewrite Z.mul_0_r, Z.add_0_r, Z.sub_0_r in H12. + rewrite H12; clear H12. + entailer!. + assert (n - 1 < Z.of_nat (Datatypes.length l)). { + rewrite <-Zlength_correct. + lia. + } + pose proof (sublist_single (n - 1) l 0 ltac:(lia)). + clear H12. + pose proof (Aux.store_uint_array_single_to_undef xp_pre (n - 1) (Znth (n - 1) l 0)). + assert (n - 1 + 1 = n). { lia. } + rewrite H14 in H12, H13; clear H14. + rewrite H13, H12; clear H13 H12. + pose proof (Aux.store_undef_uint_array_rec_divide xp_pre (n - 1) n cap ltac:(lia) ltac:(lia)). + rewrite <-H12. + entailer!. + + assert (n <= Z.of_nat (Datatypes.length l)). { + rewrite <-Zlength_correct. + lia. + } + pose proof (sublist_split 0 n (n - 1) l ltac:(lia) ltac:(lia)). + clear H12. + rewrite H13 in H6. + apply (list_store_Z_split) in H6; destruct H6. + assert (Z.of_nat (Datatypes.length l) = Zlength l). { + rewrite (Zlength_correct l); reflexivity. + } + pose proof (sublist_single (n - 1) l 0 ltac:(lia)). + assert (n - 1 + 1 = n). { lia. } + rewrite H16 in H15; clear H16. + rewrite H15 in H12. + unfold list_store_Z in H12; destruct H12. + simpl in H12. + rewrite Znth_sublist0 in H; try lia. + rewrite H in H12. + rewrite (Zlength_sublist0 (n - 1) l) in *; try lia. + pose proof (Z_div_mod_eq_full val (UINT_MOD ^ (n - 1))). + rewrite <-H12, Z.mul_0_r, Z.add_0_l in H17. + rewrite <-H17 in H6. + tauto. +Qed. + +Lemma proof_of_mpn_normalized_size_return_wit_1_1 : mpn_normalized_size_return_wit_1_1. +Proof. + pre_process. + assert (n = 0). { lia. } + clear H H0. + rewrite H11 in *. + unfold mpd_store_Z_compact, mpd_store_list. + Exists nil. + entailer!. + + rewrite Zlength_nil. + lia. + + unfold list_store_Z_compact. + simpl. + rewrite sublist_nil in H5; try lia. + unfold list_store_Z in H5; simpl in H5. + destruct H5. + lia. +Qed. + +Lemma proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_wit_1_2. +Proof. + pre_process. + unfold mpd_store_Z_compact, mpd_store_list. + Exists (sublist 0 n l). + entailer!. + + rewrite Zlength_sublist0; try lia. + entailer!. + + rewrite Zlength_sublist0; lia. + + rewrite Zlength_sublist0; lia. + + unfold list_store_Z_compact. + unfold list_store_Z in H6. + destruct H6. + rewrite Aux.list_last_to_Znth. + - rewrite Zlength_sublist0; try lia. + repeat split; try tauto. + pose proof (list_within_bound_Znth (sublist 0 n l) (n - 1)). + rewrite Zlength_sublist0 in H13; try lia. + specialize (H13 ltac:(lia) H12). + lia. + - assert (sublist 0 n l = nil \/ sublist 0 n l <> nil). { tauto. } + destruct H13. + * pose proof (Zlength_sublist0 n l ltac:(lia)). + rewrite H13 in H14. + rewrite Zlength_nil in H14. + lia. + * tauto. +Qed. + +Lemma proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1. +Proof. + pre_process. + unfold mpd_store_Z. + Intros l. + Exists l. + unfold mpd_store_list. + entailer!. + + rewrite H0. + rewrite sublist_self; try lia. + entailer!. + + rewrite sublist_self; try lia. + tauto. Qed. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 96859ec..8b9dd25 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -59,7 +59,7 @@ mpn_copyi (unsigned int *d, unsigned int *s, int n) Zlength(l) == n && cap1 <= 100000000 && store_uint_array(s, n, l) * - store_undef_uint_array_rec(s, n + 1, cap1) && + store_undef_uint_array_rec(s, n, cap1) && list_store_Z(l, val) */ /*@ @@ -74,7 +74,7 @@ mpn_copyi (unsigned int *d, unsigned int *s, int n) 0 <= i && i <= n && Zlength(l) == n && list_store_Z(l, val) && n <= cap1 && store_uint_array(s, n, l) * - store_undef_uint_array_rec(s, n + 1, cap1) * + store_undef_uint_array_rec(s, n, cap1) * store_uint_array(d, i, sublist(0, i, l)) * store_uint_array_rec(d, i, cap2, l') */ @@ -119,8 +119,8 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) which implies exists l1 l2, store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * - store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * - store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && + store_undef_uint_array_rec(ap@pre, n@pre, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre, cap2) && list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) */ @@ -131,8 +131,8 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) /*@Inv -1 <= n && n < n@pre && store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * - store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * - store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && + store_undef_uint_array_rec(ap@pre, n@pre, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre, cap2) && list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) && sublist(n + 1, n@pre, l1) == sublist(n + 1, n@pre, l2) @@ -186,13 +186,41 @@ mpn_cmp4 (unsigned int *ap, int an, unsigned int *bp, int bn) /*返回非0的位数*/ -/*static int +static int mpn_normalized_size (unsigned int *xp, int n) +/*@ + With cap val + Require + mpd_store_Z(xp, val, n, cap) && + 0 <= n && n <= cap && cap <= 100000000 + Ensure + 0 <= __return && __return <= cap && + mpd_store_Z_compact(xp@pre, val, __return, cap) +*/ { + /*@ + mpd_store_Z(xp@pre, val, n, cap) + which implies + exists l, + list_store_Z(sublist(0, n, l), val) && + Zlength(l) == n && + store_uint_array(xp@pre, n, sublist(0, n, l)) * + store_undef_uint_array_rec(xp@pre, n, cap) + */ + /*@ + Given l + */ + /*@Inv + n >= 0 && n <= n@pre && + n@pre >= 0 && n@pre <= cap && cap <= 100000000 && + list_store_Z(sublist(0, n, l), val) && + store_uint_array(xp@pre, n, sublist(0, n, l)) * + store_undef_uint_array_rec(xp@pre, n, cap) + */ while (n > 0 && xp[n-1] == 0) --n; return n; -}*/ +} /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ /*unsigned int