ready to prove four carry and uncarry in mpn_add_n

2025-06-22 05:12:16 +00:00
parent 94581ea60d
commit 1e3c1ea7ec
1 changed files with 22 additions and 2 deletions
--- 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.