From fd26d9669e205a8a1eda7ad78a4ff0f76438d3d4 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 07:37:10 +0000 Subject: [PATCH] finish all adder proof for mpn_add_n --- projects/lib/GmpAux.v | 2 +- projects/lib/gmp_proof_manual.v | 291 +++++++++++++++++++++++++++++++- 2 files changed, 289 insertions(+), 4 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 4ece64f..640cbaa 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -51,7 +51,7 @@ Lemma Z_mod_3add_carry11: forall (a b c m: Z), m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> (a + c) mod m < c -> ((a + c) mod m + b) mod m < b -> - a + b + c = ((a + c) mod m + b) mod m + m. + a + b + c = ((a + c) mod m + b) mod m + m * 2. Proof. Admitted. Lemma Z_mod_3add_carry00: forall (a b c m: Z), diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index c062a48..053adc5 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -932,13 +932,298 @@ Proof. Qed. Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2 + UINT_MOD * 2). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry11; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (1 + 1) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry00; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (0 + 0) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2 + UINT_MOD). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry01; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (0 + 1) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. Proof. Admitted.