ready to finalize proof_of_mpn_add_1_entail_wit_2_1

projects/lib/gmp_proof_manual.v

@@ -407,13 +407,119 @@ Proof.
 Qed.
 
 Lemma proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1.
-Proof. Admitted. 
+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_1 : mpn_add_1_entail_wit_2_1.
-Proof. Admitted. 
+Proof.
+  pre_process.
+  rewrite replace_Znth_app_r.
+  - Exists l'''.
+    rewrite H12.
+    assert (i - i = 0) by lia.
+    rewrite H24.
+    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 H25.
+    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 H12.
+      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 H26.
+      rewrite <- H11.
+      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 H27 in *.
+        admit.
+      }
+      admit.
+    + pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b).
+      apply H26 in H10.
+      rewrite H12 in H10.
+      assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia.
+      rewrite H27 in H10.
+      tauto.
+      subst new_b.
+      unfold unsigned_last_nbits.
+      assert (2 ^ 32 = 4294967296). { nia. }
+      rewrite H27.
+      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 H26 in H7; try tauto.
+        }
+
+        assert (i < Zlength l_3). {
+          subst l_3.
+          rewrite H15.
+          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 <-H29.
+          apply H28.
+          lia.
+          subst l_3.
+          rewrite Zlength_correct in H27.
+          lia.
+          rewrite Zlength_correct in H27.
+          lia.
+        }
+        rewrite H28.
+        pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)).
+        apply H29 in H9.
+        rewrite Zlength_sublist0 in H9.
+        assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia.
+        rewrite H30.
+        tauto.
+        subst l_3.
+        rewrite H15.
+        lia.
+        apply list_within_bound_Znth.
+        lia.
+        unfold list_store_Z_compact in H7.
+        tauto.
+  - pose proof (Zlength_sublist0 i l'_2).
+    lia.
+Admitted. 
 
 Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2.
-Proof. Admitted. 
+Proof.
+  pre_process.
+Admitted. 
 
 Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1.
 Proof.
@@ -455,4 +561,7 @@ Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1.
 Proof. Admitted. 
 
 Lemma proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3.
 Proof. Admitted.