From 0fdf4fc328c91d132d5890b604bfd8ea3ebb9437 Mon Sep 17 00:00:00 2001
From: ZhuangYumin <zhuangyumin@sjtu.edu.cn>
Date: Sun, 22 Jun 2025 07:25:46 +0000
Subject: [PATCH] finish proof_of_mpn_add_n_entail_wit_3_1

---
 projects/lib/GmpAux.v           | 28 ++++++++++++++++++++++++++++
 projects/lib/gmp_proof_manual.v | 24 ++++++++++++++++++++++--
 2 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v
index 7bbdf01..4ece64f 100755
--- a/projects/lib/GmpAux.v
+++ b/projects/lib/GmpAux.v
@@ -33,6 +33,34 @@ Lemma Z_mod_add_uncarry: forall (a b m: Z),
   a + b = (a + b) mod m.
 Proof. Admitted.
 
+Lemma Z_mod_3add_carry10: 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.
+Proof. Admitted.
+
+Lemma Z_mod_3add_carry01: 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.
+Proof. Admitted.
+
+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.
+Proof. Admitted.
+
+Lemma Z_mod_3add_carry00: 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.
+Proof. Admitted.
+
 Lemma Z_of_nat_succ: forall (n: nat),
   Z.of_nat (S n) = Z.of_nat n + 1.
 Proof. lia. Qed.
diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v
index 16d0213..c062a48 100755
--- a/projects/lib/gmp_proof_manual.v
+++ b/projects/lib/gmp_proof_manual.v
@@ -871,7 +871,27 @@ Proof.
     Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)).
     Exists l_b_2 l_a_2.
     entailer!.
-    + admit.
+    + 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_carry10; 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 + 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.
@@ -909,7 +929,7 @@ Proof.
       tauto.
   - pose proof (Zlength_sublist0 i l_r_prefix_2).
     lia.
-Admitted. 
+Qed.
 
 Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2.
 Proof. Admitted.