feat(mpz_clear & mpz_realloc): Proved correctness of mpz_clear and mpz_realloc

projects/lib/GmpNumber.v

@@ -597,20 +597,10 @@ Record bigint_ent: Type := {
     sign: Prop;
 }.
 
-Definition store_bigint_ent (x: addr) (n: bigint_ent): Assertion :=
-    EX size, 
-      &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size &&
-      ([| size < 0 |] && [| sign n |] && [| size = -Zlength (data n) |] ||
-        [| size >= 0 |] && [| ~(sign n) |] && [| size = Zlength (data n) |]) **
-    &(x # "__mpz_struct" ->ₛ "_mp_alloc") # Int |-> cap n **
-    EX p, 
-      &(x # "__mpz_struct" ->ₛ "_mp_d") # Ptr |-> p **
-    Internal.mpd_store_list p (data n) (cap n).
-
-Definition bigint_ent_store_Z (n: bigint_ent) (x: Z): Assertion :=
-  [| sign n |] && [| Internal.list_store_Z (data n) (-x) |] ||
-    [| ~(sign n) |] && [| Internal.list_store_Z (data n) x |].
-
 Definition store_Z (x: addr) (n: Z): Assertion :=
-  EX ent,
+  EX (ptr: addr) (cap size: Z),
-    store_bigint_ent x ent && bigint_ent_store_Z ent n.
+    (([| size < 0 |] && [| n < 0 |] && Internal.mpd_store_Z_compact ptr (-n) (-size) cap) ||
+      ([| size >= 0 |] && [| n >= 0 |] && Internal.mpd_store_Z_compact ptr n size cap)) **
+    &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size **
+    &(x # "__mpz_struct" ->ₛ "_mp_alloc") # Int |-> cap **
+    &(x # "__mpz_struct" ->ₛ "_mp_d") # Ptr |-> ptr.

projects/lib/gmp_proof_auto.v

@@ -141,3 +141,66 @@ Proof. Admitted.
 Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2.
 Proof. Admitted. 
 
+Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_return_wit_1_4 : mpz_clear_return_wit_1_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_1 : mpz_clear_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_2 : mpz_clear_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_3 : mpz_clear_partial_solve_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_1 : mpz_realloc_safety_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_2 : mpz_realloc_safety_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_3 : mpz_realloc_safety_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_4 : mpz_realloc_safety_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_5 : mpz_realloc_safety_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_6 : mpz_realloc_safety_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_1 : mpz_realloc_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_2 : mpz_realloc_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_3 : mpz_realloc_partial_solve_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_4 : mpz_realloc_partial_solve_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_5 : mpz_realloc_partial_solve_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_6 : mpz_realloc_partial_solve_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_7 : mpz_realloc_partial_solve_wit_7.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_8 : mpz_realloc_partial_solve_wit_8.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
+Proof. Admitted. 
+

projects/lib/gmp_proof_manual.v

@@ -410,4 +410,299 @@ Proof.
     entailer!.
   + rewrite sublist_self; try lia.
     tauto.
-Qed.
+Qed.
+
+
+Lemma proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  unfold mpd_store_list.
+  subst.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_return_wit_1_2 : mpz_clear_return_wit_1_2.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  unfold mpd_store_list.
+  entailer!.
+  assert (size_2 = 0). {
+    pose proof (Zlength_nonneg data).
+    lia.
+  }
+  rewrite H6 in *.
+  rewrite <-H3 in *.
+  unfold store_uint_array, store_undef_uint_array_rec.
+  unfold store_array.
+  assert (cap_2 - 0 = 0). { lia. }
+  rewrite H7; clear H7.
+  pose proof (Zlength_nil_inv data ltac:(lia)).
+  rewrite H7 in *; clear H7.
+  simpl.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+Qed.
+
+
+Lemma proof_of_mpz_clear_return_wit_1_4 : mpz_clear_return_wit_1_4.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_which_implies_wit_1 : mpz_clear_which_implies_wit_1.
+Proof.
+  pre_process.
+  unfold store_Z.
+  Intros ptr cap size.
+  entailer!.
+  rewrite orp_sepcon_left.
+  Split.
+  + Right.
+    Exists ptr cap size.
+    entailer!.
+  + Left.
+    Exists ptr cap size.
+    entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_1 : mpz_realloc_return_wit_1_1.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  entailer!.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_2 : mpz_realloc_return_wit_1_2.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_3 : mpz_realloc_return_wit_1_3.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact.
+    Intros data.
+    Exists data.
+    unfold mpd_store_list, store_undef_uint_array_rec.
+    entailer!.
+    - assert (Zlength data = 0). {
+        pose proof (Zlength_nonneg data).
+        lia.
+      }
+      rewrite H8 in *.
+      simpl.
+      entailer!.
+      pose proof (Zlength_nil_inv data H8).
+      repeat subst.
+      unfold store_uint_array, store_array; simpl; entailer!.
+      unfold store_undef_uint_array, store_undef_array.
+      rewrite Z.sub_0_r.
+      reflexivity.
+    - unfold Zmax in *.
+      assert (size_pre < 1 \/ size_pre >= 1). { lia. }
+      destruct H8.
+      * rewrite (Z.max_r size_pre 1 ltac:(lia)); lia.
+      * rewrite (Z.max_l size_pre 1 ltac:(lia)); lia.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_4 : mpz_realloc_return_wit_1_4.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data.
+    Exists data.
+    assert (Zlength data = 0). {
+      pose proof (Zlength_nonneg data).
+      lia.
+    }
+    rewrite H8 in *; clear H2.
+    pose proof (Zlength_nil_inv data H8).
+    rewrite H2 in *; clear H2 H8.
+    unfold store_uint_array, store_array.
+    simpl.
+    entailer!.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_5 : mpz_realloc_return_wit_1_5.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data.
+    Exists data.
+    unfold store_uint_array, store_array.
+    simpl.
+    entailer!.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_6 : mpz_realloc_return_wit_1_6.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  subst.
+  entailer!.
+  + unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data; Exists data.
+    unfold store_uint_array, store_array.
+    assert (Zlength data = 0). {
+      pose proof (Zlength_nonneg data).
+      lia.
+    }
+    rewrite H8 in *; clear H2.
+    pose proof (Zlength_nil_inv data H8).
+    rewrite H2 in *; clear H2 H8.
+    unfold store_undef_uint_array, store_undef_uint_array_rec, store_undef_array.
+    subst.
+    simpl.
+    entailer!.
+    - rewrite Z.sub_0_r.
+      entailer!.
+    - pose proof (Z.le_max_r size_pre 1).
+      simpl in H.
+      unfold Zmax in *.
+      lia.
+  + unfold Zmax in *.
+    pose proof (Z.le_max_l size_pre 1).
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_7 : mpz_realloc_return_wit_1_7.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  subst.
+  unfold Zmax in *.
+  rewrite (Z.abs_neq old ltac:(lia)) in H.
+  pose proof (Z.le_max_l size_pre 1).
+  unfold mpd_store_Z_compact.
+  Intros data; entailer!.
+  unfold mpd_store_list.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_8 : mpz_realloc_return_wit_1_8.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  subst.
+  unfold Zmax in *.
+  rewrite (Z.abs_eq old ltac:(lia)) in H.
+  pose proof (Z.le_max_l size_pre 1).
+  unfold mpd_store_Z_compact.
+  Intros data; entailer!.
+  unfold mpd_store_list.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_3_pure : mpz_realloc_partial_solve_wit_3_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_4_pure : mpz_realloc_partial_solve_wit_4_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_5_pure : mpz_realloc_partial_solve_wit_5_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_6_pure : mpz_realloc_partial_solve_wit_6_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_7_pure : mpz_realloc_partial_solve_wit_7_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_8_pure : mpz_realloc_partial_solve_wit_8_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_9_pure : mpz_realloc_partial_solve_wit_9_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_10_pure : mpz_realloc_partial_solve_wit_10_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.

projects/mini-gmp.c

@@ -323,15 +323,53 @@ mpn_sub (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn)
 
 /* MPZ interface */
 
-/*void
+void
 mpz_clear (mpz_t r)
+/*@
+  With
+    n
+  Require
+    store_Z(r, n)
+  Ensure
+    exists size cap ptr,
+      r@pre -> _mp_size == size && r@pre -> _mp_alloc == cap && r@pre -> _mp_d == ptr
+*/
 {
+  /*@
+    store_Z(r@pre, n)
+    which implies
+    exists ptr size cap,
+      (size < 0 && n < 0 && mpd_store_Z_compact(ptr, -n, -size, cap) ||
+        size >= 0 && n >= 0 && mpd_store_Z_compact(ptr, n, size, cap)) &&
+      r@pre -> _mp_size == size &&
+      r@pre -> _mp_alloc == cap &&
+      r@pre -> _mp_d == ptr
+  */
   if (r->_mp_alloc)
     gmp_free_limbs (r->_mp_d, r->_mp_alloc);
-}*/
+}
 
-/*static unsigned int *
+static unsigned int *
 mpz_realloc (mpz_t r, int size)
+/*@
+  With
+    ptr old cap n
+  Require
+    size >= cap && size <= 100000000 && cap >= 0 && cap <= 100000000 &&
+    (old < 0 && n < 0 && mpd_store_Z_compact(ptr, -n, -old, cap) ||
+        old >= 0 && n >= 0 && mpd_store_Z_compact(ptr, n, old, cap)) &&
+      r -> _mp_size == old &&
+      r -> _mp_alloc == cap &&
+      r -> _mp_d == ptr
+  Ensure
+    exists c ptr_new,
+    c >= size@pre && 
+    (n < 0 && mpd_store_Z_compact(ptr_new, -n, -old, c) ||
+      n >= 0 && mpd_store_Z_compact(ptr_new, n, old, c)) &&
+    r -> _mp_size == old &&
+    r@pre -> _mp_alloc == c &&
+    r@pre -> _mp_d == ptr_new
+*/
 {
   size = gmp_max (size, 1);
 
@@ -345,7 +383,7 @@ mpz_realloc (mpz_t r, int size)
     r->_mp_size = 0;
 
   return r->_mp_d;
-}*/
+}
 
 /* Realloc for an mpz_t WHAT if it has less than NEEDED limbs.  */
 /*unsigned int *mrz_realloc_if(mpz_t z,int n) {
@@ -363,7 +401,7 @@ mpz_sgn (const mpz_t u)
 mpz_swap (mpz_t u, mpz_t v)
 {
   int_swap (u->_mp_alloc, v->_mp_alloc);
-  unsigned int *_swap(u->_mp_d, v->_mp_d);
+  mp_ptr_swap(u->_mp_d, v->_mp_d);
   int_swap (u->_mp_size, v->_mp_size);
 }*/
 

projects/mini-gmp.h

@@ -1,4 +1,16 @@
-typedef struct
+/*@ 
+  Extern Coq (Zabs : Z -> Z) 
+             (Zmax : Z -> Z -> Z)
+             (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion)
+             (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion)
+             (mpd_store_list : Z -> list Z -> Z -> Assertion)
+             (store_Z: Z -> Z -> Assertion)
+             (list_store_Z : list Z -> Z -> Prop)
+             (list_store_Z_compact: list Z -> Z -> Prop)
+             (last: list Z -> Z -> Z)
+*/
+
+typedef struct __mpz_struct
 {
   int _mp_alloc;		/* Number of *limbs* allocated and pointed
 				   to by the _mp_d field.  */
@@ -16,7 +28,14 @@ typedef const __mpz_struct *mpz_srcptr;
 /* BEGIN Given Functions */
 
 /* Swap functions. */
-void int_swap(int x, int y);
+void int_swap(int x, int y)
+/*@
+  Require
+    emp
+  Ensure
+    x == y@pre && y == x@pre
+*/
+;
 
 void mp_ptr_swap(unsigned int *x, unsigned int *y);
 
@@ -24,13 +43,37 @@ void mpz_srcptr_swap(mpz_srcptr x, mpz_srcptr y);
 
 /* Memory allocation functions. */
 static unsigned int *
-gmp_alloc_limbs (int size);
+gmp_alloc_limbs (int size)
+/*@
+  Require
+    size >= 0
+  Ensure
+    store_undef_uint_array(__return, size)
+*/;
 
 static unsigned int *
-gmp_realloc_limbs (unsigned int *old, int old_size, int size);
+gmp_realloc_limbs (unsigned int *old, int old_size, int size)
+/*@
+  With
+    len n
+  Require
+    old_size >= 0 && size >= old_size &&
+    mpd_store_Z_compact(old, n, len, old_size)
+  Ensure
+    mpd_store_Z_compact(__return, n, len, size)
+*/;
 
 static void
-gmp_free_limbs (unsigned int *old, int size);
+gmp_free_limbs (unsigned int *old, int size)
+/*@
+  With
+    n len
+  Require
+    mpd_store_Z_compact(old, n, len, size)
+  Ensure
+    emp
+*/
+;
 
 /* END Given Functions  */
 
@@ -46,7 +89,7 @@ unsigned int mpn_sub_1 (unsigned int *, unsigned int *, int, unsigned int);
 unsigned int mpn_sub_n (unsigned int *, unsigned int *, unsigned int *, int);
 unsigned int mpn_sub (unsigned int *, unsigned int *, int, unsigned int *, int);
 
-void mpz_clear (mpz_t);
+void mpz_clear (mpz_t r);
 
 int mpz_sgn (const mpz_t);
 
@@ -58,13 +101,3 @@ void mpz_sub (mpz_t, const mpz_t, const mpz_t);
 
 void mpz_set (mpz_t, const mpz_t);
 
-/*@ 
-  Extern Coq (Zabs : Z -> Z) 
-             (Zmax : Z -> Z -> Z)
-             (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion)
-             (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion)
-             (mpd_store_list : Z -> list Z -> Z -> Assertion)
-             (list_store_Z : list Z -> Z -> Prop)
-             (list_store_Z_compact: list Z -> Z -> Prop)
-             (last: list Z -> Z -> Z)
-*/