736 lines
20 KiB
Coq
736 lines
20 KiB
Coq
Require Import Coq.ZArith.ZArith.
|
|
Require Import Coq.Bool.Bool.
|
|
Require Import Coq.Strings.String.
|
|
Require Import Coq.Lists.List.
|
|
Require Import Coq.Classes.RelationClasses.
|
|
Require Import Coq.Classes.Morphisms.
|
|
Require Import Coq.micromega.Psatz.
|
|
Require Import Coq.Sorting.Permutation.
|
|
From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap.
|
|
Require Import SetsClass.SetsClass. Import SetsNotation.
|
|
From SimpleC.SL Require Import Mem SeparationLogic.
|
|
From GmpLib Require Import gmp_goal.
|
|
Require Import GmpLib.GmpNumber. Import Internal.
|
|
Require Import GmpLib.GmpAux. Import Aux.
|
|
Require Import Logic.LogicGenerator.demo932.Interface.
|
|
Local Open Scope Z_scope.
|
|
Local Open Scope sets.
|
|
Local Open Scope string.
|
|
Local Open Scope list.
|
|
Import naive_C_Rules.
|
|
Local Open Scope sac.
|
|
|
|
Lemma proof_of_gmp_abs_return_wit_1_1 : gmp_abs_return_wit_1_1.
|
|
Proof. pre_process. Qed.
|
|
|
|
|
|
Lemma proof_of_gmp_abs_return_wit_1_2 : gmp_abs_return_wit_1_2.
|
|
Proof. pre_process. Qed.
|
|
|
|
Lemma proof_of_gmp_max_return_wit_1_1 : gmp_max_return_wit_1_1.
|
|
Proof.
|
|
pre_process.
|
|
Qed.
|
|
|
|
Lemma proof_of_gmp_max_return_wit_1_2 : gmp_max_return_wit_1_2.
|
|
Proof.
|
|
pre_process.
|
|
Qed.
|
|
|
|
Lemma proof_of_gmp_cmp_return_wit_1_2 : gmp_cmp_return_wit_1_2.
|
|
Proof.
|
|
pre_process.
|
|
repeat rewrite <-derivable1_orp_intros1.
|
|
entailer!.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_copyi_entail_wit_1 : mpn_copyi_entail_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
Exists l2 l_2.
|
|
entailer!.
|
|
pose proof (Zlength_nonneg l_2).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_copyi_entail_wit_2 : mpn_copyi_entail_wit_2.
|
|
Proof.
|
|
pre_process.
|
|
Exists l2' l_3.
|
|
entailer!.
|
|
rewrite replace_Znth_app_r.
|
|
+ rewrite Zlength_sublist0; [ | lia ].
|
|
assert (i - i = 0). { lia. }
|
|
rewrite H15; clear H15.
|
|
assert (replace_Znth 0 (Znth i l_3 0) (a :: nil) = sublist i (i + 1) l_3). {
|
|
unfold replace_Znth, Z.to_nat, replace_nth.
|
|
rewrite (sublist_single i l_3 0); [ reflexivity | ].
|
|
rewrite <-Zlength_correct; lia.
|
|
}
|
|
rewrite H15; clear H15.
|
|
rewrite replace_Znth_nothing.
|
|
- rewrite <-sublist_split; try lia; try reflexivity.
|
|
rewrite <-Zlength_correct; lia.
|
|
- pose proof (Zlength_sublist0 i l_3 ltac:(lia)).
|
|
lia.
|
|
+ pose proof (Zlength_sublist0 i l_3); lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_copyi_which_implies_wit_1 : mpn_copyi_which_implies_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
unfold mpd_store_Z.
|
|
Intros l.
|
|
Exists l.
|
|
unfold mpd_store_list.
|
|
entailer!.
|
|
subst.
|
|
entailer!.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_copyi_which_implies_wit_2 : mpn_copyi_which_implies_wit_2.
|
|
Proof.
|
|
pre_process.
|
|
pose proof (store_uint_array_divide d cap2 l2 0).
|
|
pose proof (Zlength_nonneg l2).
|
|
specialize (H0 ltac:(lia) ltac:(lia)).
|
|
destruct H0 as [H0 _].
|
|
simpl in H0.
|
|
entailer!.
|
|
rewrite (sublist_nil l2 0 0) in H0; [ | lia].
|
|
sep_apply H0.
|
|
entailer!.
|
|
unfold store_uint_array, store_uint_array_rec.
|
|
unfold store_array.
|
|
rewrite (sublist_self l2 cap2); [ | lia ].
|
|
assert (d + 0 = d). { lia. }
|
|
rewrite H2; clear H2.
|
|
assert (cap2 - 0 = cap2). { lia. }
|
|
rewrite H2; clear H2.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_copyi_which_implies_wit_3 : mpn_copyi_which_implies_wit_3.
|
|
Proof.
|
|
pre_process.
|
|
destruct l'. {
|
|
unfold store_uint_array_rec.
|
|
simpl.
|
|
entailer!.
|
|
}
|
|
pose proof (store_uint_array_rec_cons d i cap2 z l' ltac:(lia)).
|
|
sep_apply H2.
|
|
Exists z l'.
|
|
entailer!.
|
|
assert (i = 0 \/ i > 0). { lia. }
|
|
destruct H3.
|
|
+ subst.
|
|
unfold store_uint_array, store_array.
|
|
simpl.
|
|
entailer!.
|
|
+ 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.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.
|
|
assert (d + sizeof(UINT) * 0 = d). { lia. }
|
|
rewrite H5 in H4; clear H5.
|
|
rewrite <-H4.
|
|
sep_apply store_uint_array_rec_tail_merge; [ reflexivity | lia ].
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp_entail_wit_1 : mpn_cmp_entail_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
entailer!.
|
|
assert (n_pre - 1 + 1 = n_pre). { lia. }
|
|
rewrite H8; clear H8.
|
|
pose proof (Zlength_sublist n_pre n_pre l1 ltac:(lia)).
|
|
pose proof (Zlength_nil_inv (sublist n_pre n_pre l1) ltac:(lia)).
|
|
rewrite H9.
|
|
pose proof (Zlength_sublist n_pre n_pre l2 ltac:(lia)).
|
|
pose proof (Zlength_nil_inv (sublist n_pre n_pre l2) ltac:(lia)).
|
|
rewrite H11.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp_entail_wit_2 : mpn_cmp_entail_wit_2.
|
|
Proof.
|
|
pre_process.
|
|
entailer!; try lia.
|
|
assert (n - 1 + 1 = n). { lia. }
|
|
rewrite H17; clear H17.
|
|
assert (n_pre <= Z.of_nat (Datatypes.length l1)). {
|
|
rewrite <-Zlength_correct.
|
|
lia.
|
|
}
|
|
assert (n_pre <= Z.of_nat (Datatypes.length l2)). {
|
|
rewrite <-Zlength_correct.
|
|
lia.
|
|
}
|
|
rewrite (sublist_split n n_pre (n + 1) l1 ltac:(lia) ltac:(lia)).
|
|
rewrite (sublist_split n n_pre (n + 1) l2 ltac:(lia) ltac:(lia)).
|
|
rewrite (sublist_single n l1 0 ltac:(lia)).
|
|
rewrite (sublist_single n l2 0 ltac:(lia)).
|
|
rewrite H.
|
|
rewrite H7.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp_return_wit_1_1 : mpn_cmp_return_wit_1_1.
|
|
Proof.
|
|
pre_process.
|
|
entailer!.
|
|
Left; Left.
|
|
entailer!.
|
|
+ unfold mpd_store_Z_compact.
|
|
Exists l1 l2.
|
|
unfold mpd_store_list.
|
|
entailer!.
|
|
rewrite <-H6, <-H7.
|
|
entailer!.
|
|
+ assert (Znth n l1 0 < Znth n l2 0). { lia. }
|
|
clear H H0.
|
|
apply (list_store_Z_compact_cmp l1 l2 val1 val2 n ltac:(lia) ltac:(lia) H4 H5).
|
|
- rewrite <-H6, <-H7.
|
|
tauto.
|
|
- lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp_return_wit_1_2 : mpn_cmp_return_wit_1_2.
|
|
Proof.
|
|
pre_process.
|
|
Right.
|
|
entailer!.
|
|
+ unfold mpd_store_Z_compact, mpd_store_list.
|
|
Exists l1 l2.
|
|
rewrite <-H6, <-H7.
|
|
entailer!.
|
|
+ pose proof (list_store_Z_compact_cmp l2 l1 val2 val1 n ltac:(lia) ltac:(lia) H5 H4).
|
|
rewrite <-H6, <-H7 in H18.
|
|
rewrite H8 in H18.
|
|
specialize (H18 ltac:(reflexivity) ltac:(lia)).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp_which_implies_wit_1 : mpn_cmp_which_implies_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
unfold mpd_store_Z_compact.
|
|
Intros l1 l2.
|
|
Exists l2 l1.
|
|
unfold mpd_store_list.
|
|
entailer!.
|
|
rewrite <-H0, <-H2.
|
|
entailer!.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp4_return_wit_1_1 : mpn_cmp4_return_wit_1_1.
|
|
Proof.
|
|
pre_process.
|
|
Right.
|
|
unfold mpd_store_Z_compact.
|
|
Intros l1 l2.
|
|
Exists l1 l2.
|
|
entailer!.
|
|
pose proof (list_store_Z_cmp_length l2 l1 val2 val1 ltac:(lia) H9 H7).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp4_return_wit_1_2 : mpn_cmp4_return_wit_1_2.
|
|
Proof.
|
|
pre_process.
|
|
Left; Left.
|
|
unfold mpd_store_Z_compact.
|
|
entailer!.
|
|
Intros l1 l2.
|
|
Exists l1 l2.
|
|
entailer!.
|
|
pose proof (list_store_Z_cmp_length l1 l2 val1 val2 ltac:(lia) H7 H9).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp4_return_wit_2_1 : mpn_cmp4_return_wit_2_1.
|
|
Proof.
|
|
pre_process.
|
|
Right.
|
|
unfold mpd_store_Z_compact.
|
|
Intros l1 l2.
|
|
Exists l1 l2.
|
|
entailer!.
|
|
Qed.
|
|
|
|
|
|
Lemma proof_of_mpn_cmp4_return_wit_2_2 : mpn_cmp4_return_wit_2_2.
|
|
Proof.
|
|
pre_process.
|
|
Left; Right.
|
|
unfold mpd_store_Z_compact.
|
|
Intros l1 l2.
|
|
Exists l1 l2.
|
|
entailer!.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_cmp4_return_wit_2_3 : mpn_cmp4_return_wit_2_3.
|
|
Proof.
|
|
pre_process.
|
|
Left; Left.
|
|
unfold mpd_store_Z_compact.
|
|
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.
|
|
|
|
Lemma proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
Exists l2 nil 0 0 l_2.
|
|
entailer!.
|
|
- unfold list_store_Z.
|
|
split.
|
|
+ simpl. tauto.
|
|
+ simpl. tauto.
|
|
- rewrite (sublist_nil l_2 0 0); try lia.
|
|
unfold list_store_Z.
|
|
split.
|
|
+ simpl. tauto.
|
|
+ simpl. tauto.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2.
|
|
Proof.
|
|
pre_process.
|
|
entailer!.
|
|
Admitted.
|
|
|
|
Lemma proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1.
|
|
Proof.
|
|
pre_process.
|
|
rewrite replace_Znth_app_r.
|
|
- Exists l'''.
|
|
rewrite H14.
|
|
assert (i - i = 0) by lia.
|
|
rewrite H26.
|
|
set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)).
|
|
rewrite replace_Znth_nothing; try lia.
|
|
assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). {
|
|
unfold replace_Znth.
|
|
unfold Z.to_nat.
|
|
unfold replace_nth.
|
|
reflexivity.
|
|
}
|
|
rewrite H27.
|
|
Exists (l'_2 ++ new_b :: nil).
|
|
Exists (val2_2 + new_b * (UINT_MOD^ i)).
|
|
Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)).
|
|
Exists l_3.
|
|
entailer!.
|
|
+ rewrite Zlength_app.
|
|
rewrite H14.
|
|
unfold Zlength.
|
|
unfold Zlength_aux.
|
|
lia.
|
|
+ assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia.
|
|
rewrite H28.
|
|
rewrite <- H13.
|
|
assert (Znth i l_3 0 + b = new_b + UINT_MOD).
|
|
{
|
|
subst new_b.
|
|
unfold unsigned_last_nbits.
|
|
unfold unsigned_last_nbits in H3.
|
|
assert (2^32 = 4294967296). { nia. }
|
|
rewrite H29 in *.
|
|
assert (0 <= Znth i l_3 0 < 4294967296). {
|
|
assert (l_2=l_3).
|
|
{
|
|
pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val).
|
|
apply H30 in H9; try tauto.
|
|
}
|
|
assert (i < Zlength l_3). {
|
|
subst l_3.
|
|
rewrite H17.
|
|
tauto.
|
|
}
|
|
unfold list_store_Z_compact in H9.
|
|
apply list_within_bound_Znth.
|
|
lia.
|
|
tauto.
|
|
}
|
|
apply Z_mod_add_carry; try lia; try tauto.
|
|
}
|
|
assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 1 * 4294967296 ^ (i + 1)).
|
|
{
|
|
subst new_b.
|
|
Search [ Zmult Zplus "distr" ].
|
|
rewrite <- Z.mul_add_distr_r.
|
|
rewrite (Zpow_add_1 4294967296 i); try lia.
|
|
}
|
|
lia.
|
|
+ pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b).
|
|
apply H28 in H12.
|
|
rewrite H14 in H12.
|
|
assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia.
|
|
rewrite H29 in H12.
|
|
tauto.
|
|
subst new_b.
|
|
unfold unsigned_last_nbits.
|
|
assert (2 ^ 32 = 4294967296). { nia. }
|
|
rewrite H29.
|
|
apply Z.mod_pos_bound.
|
|
lia.
|
|
+ assert (l_2=l_3).
|
|
{
|
|
pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val).
|
|
apply H28 in H9; try tauto.
|
|
}
|
|
|
|
assert (i < Zlength l_3). {
|
|
subst l_3.
|
|
rewrite H17.
|
|
tauto.
|
|
}
|
|
|
|
assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). {
|
|
pose proof (sublist_split 0 (i+1) i l_3).
|
|
pose proof (sublist_single i l_3 0).
|
|
rewrite <-H31.
|
|
apply H30.
|
|
lia.
|
|
subst l_3.
|
|
rewrite Zlength_correct in H29.
|
|
lia.
|
|
rewrite Zlength_correct in H29.
|
|
lia.
|
|
}
|
|
rewrite H30.
|
|
pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)).
|
|
apply H31 in H11.
|
|
rewrite Zlength_sublist0 in H11.
|
|
assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia.
|
|
rewrite H32.
|
|
tauto.
|
|
subst l_3.
|
|
rewrite H17.
|
|
lia.
|
|
apply list_within_bound_Znth.
|
|
lia.
|
|
unfold list_store_Z_compact in H9.
|
|
tauto.
|
|
- pose proof (Zlength_sublist0 i l'_2).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2.
|
|
Proof.
|
|
pre_process.
|
|
rewrite replace_Znth_app_r.
|
|
- Exists l'''.
|
|
rewrite H14.
|
|
assert (i - i = 0) by lia.
|
|
rewrite H26.
|
|
set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)).
|
|
rewrite replace_Znth_nothing; try lia.
|
|
assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). {
|
|
unfold replace_Znth.
|
|
unfold Z.to_nat.
|
|
unfold replace_nth.
|
|
reflexivity.
|
|
}
|
|
rewrite H27.
|
|
Exists (l'_2 ++ new_b :: nil).
|
|
Exists (val2_2 + new_b * (UINT_MOD^ i)).
|
|
Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)).
|
|
Exists l_3.
|
|
entailer!.
|
|
+ rewrite Zlength_app.
|
|
rewrite H14.
|
|
unfold Zlength.
|
|
unfold Zlength_aux.
|
|
lia.
|
|
+ assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia.
|
|
rewrite H28.
|
|
rewrite <- H13.
|
|
assert (Znth i l_3 0 + b = new_b).
|
|
{
|
|
subst new_b.
|
|
unfold unsigned_last_nbits.
|
|
unfold unsigned_last_nbits in H3.
|
|
assert (2^32 = 4294967296). { nia. }
|
|
rewrite H29 in *.
|
|
assert (0 <= Znth i l_3 0 < 4294967296). {
|
|
assert (l_2=l_3).
|
|
{
|
|
pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val).
|
|
apply H30 in H9; try tauto.
|
|
}
|
|
assert (i < Zlength l_3). {
|
|
subst l_3.
|
|
rewrite H17.
|
|
tauto.
|
|
}
|
|
unfold list_store_Z_compact in H9.
|
|
apply list_within_bound_Znth.
|
|
lia.
|
|
tauto.
|
|
}
|
|
apply Z_mod_add_uncarry; try lia; try tauto.
|
|
}
|
|
assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 0 * 4294967296 ^ (i + 1)).
|
|
{
|
|
subst new_b.
|
|
Search [ Zmult Zplus "distr" ].
|
|
rewrite <- Z.mul_add_distr_r.
|
|
rewrite (Zpow_add_1 4294967296 i); try lia.
|
|
}
|
|
lia.
|
|
+ pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b).
|
|
apply H28 in H12.
|
|
rewrite H14 in H12.
|
|
assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia.
|
|
rewrite H29 in H12.
|
|
tauto.
|
|
subst new_b.
|
|
unfold unsigned_last_nbits.
|
|
assert (2 ^ 32 = 4294967296). { nia. }
|
|
rewrite H29.
|
|
apply Z.mod_pos_bound.
|
|
lia.
|
|
+ assert (l_2=l_3).
|
|
{
|
|
pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val).
|
|
apply H28 in H9; try tauto.
|
|
}
|
|
|
|
assert (i < Zlength l_3). {
|
|
subst l_3.
|
|
rewrite H17.
|
|
tauto.
|
|
}
|
|
|
|
assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). {
|
|
pose proof (sublist_split 0 (i+1) i l_3).
|
|
pose proof (sublist_single i l_3 0).
|
|
rewrite <-H31.
|
|
apply H30.
|
|
lia.
|
|
subst l_3.
|
|
rewrite Zlength_correct in H29.
|
|
lia.
|
|
rewrite Zlength_correct in H29.
|
|
lia.
|
|
}
|
|
rewrite H30.
|
|
pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)).
|
|
apply H31 in H11.
|
|
rewrite Zlength_sublist0 in H11.
|
|
assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia.
|
|
rewrite H32.
|
|
tauto.
|
|
subst l_3.
|
|
rewrite H17.
|
|
lia.
|
|
apply list_within_bound_Znth.
|
|
lia.
|
|
unfold list_store_Z_compact in H9.
|
|
tauto.
|
|
- pose proof (Zlength_sublist0 i l'_2).
|
|
lia.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
unfold mpd_store_Z_compact.
|
|
unfold mpd_store_list.
|
|
Exists val2.
|
|
pose proof (list_store_Z_compact_reverse_injection l l_2 val val).
|
|
apply H19 in H2; try tauto.
|
|
rewrite <-H2 in H10.
|
|
assert (i = n_pre) by lia.
|
|
rewrite H20 in H4.
|
|
rewrite <- H10 in H4.
|
|
rewrite (sublist_self l (Zlength l)) in H4; try tauto.
|
|
rewrite <-H2 in H12.
|
|
assert (list_store_Z l val). { apply list_store_Z_compact_to_normal. tauto. }
|
|
pose proof (list_store_Z_injection l l val1 val).
|
|
apply H22 in H4; try tauto.
|
|
rewrite H4 in H6.
|
|
entailer!.
|
|
Exists l.
|
|
entailer!.
|
|
entailer!; try rewrite H20; try tauto.
|
|
- rewrite H10.
|
|
entailer!.
|
|
unfold mpd_store_Z.
|
|
unfold mpd_store_list.
|
|
Exists l'.
|
|
rewrite H7.
|
|
subst i.
|
|
entailer!.
|
|
rewrite H20.
|
|
entailer!.
|
|
apply store_uint_array_rec_def2undef.
|
|
- rewrite <- H20. tauto.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1.
|
|
Proof.
|
|
pre_process.
|
|
unfold mpd_store_Z_compact.
|
|
Intros l.
|
|
Exists l.
|
|
unfold mpd_store_list.
|
|
entailer!.
|
|
subst n_pre.
|
|
entailer!.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2.
|
|
Proof.
|
|
pre_process.
|
|
pose proof (store_uint_array_divide rp_pre cap2 l2 0).
|
|
pose proof (Zlength_nonneg l2).
|
|
specialize (H0 ltac:(lia) ltac:(lia)).
|
|
destruct H0 as [H0 _].
|
|
simpl in H0.
|
|
entailer!.
|
|
rewrite (sublist_nil l2 0 0) in H0; [ | lia].
|
|
sep_apply H0.
|
|
entailer!.
|
|
unfold store_uint_array, store_uint_array_rec.
|
|
unfold store_array.
|
|
rewrite (sublist_self l2 cap2); [ | lia ].
|
|
assert (rp_pre + 0 = rp_pre). { lia. }
|
|
rewrite H2; clear H2.
|
|
assert (cap2 - 0 = cap2). { lia. }
|
|
rewrite H2; clear H2.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3.
|
|
Proof. Admitted. |