From 1e3c1ea7ec06d4b5211468c7bcc8fea952c84d41 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 05:12:16 +0000 Subject: [PATCH] ready to prove four carry and uncarry in mpn_add_n --- projects/lib/gmp_proof_manual.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index fd3b8d4..dd5256f 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -808,10 +808,30 @@ Proof. Qed. Lemma proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1. -Proof. Admitted. +Proof. + pre_process. + Exists l_r nil 0 0 0. + Exists l_b_2 l_a_2. + entailer!. + - unfold list_store_Z. + simpl. + tauto. + - rewrite sublist_nil; try lia; try tauto. + unfold list_store_Z. + simpl. + tauto. + - rewrite sublist_nil; try lia; try tauto. + unfold list_store_Z. + simpl. + tauto. +Qed. Lemma proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2. -Proof. Admitted. +Proof. + pre_process. + prop_apply (store_uint_range &("cy") cy). + entailer!. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1. Proof. Admitted.