diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v
index 9d2ae7d..2ea2e4c 100755
--- a/projects/lib/GmpNumber.v
+++ b/projects/lib/GmpNumber.v
@@ -358,6 +358,52 @@ Proof.
     - pose proof (Zlength_nonneg l1); lia.
 Qed.
 
+Lemma list_store_Z_compact_bound: forall (l1: list Z) (n: Z),
+  list_store_Z_compact l1 n ->
+  UINT_MOD ^ ((Zlength l1) - 1) <= n < UINT_MOD ^ (Zlength l1).
+Proof.
+  intros.
+  destruct l1.
+  + rewrite Zlength_nil.
+    simpl.
+    unfold list_store_Z_compact; destruct H.
+    simpl in H.
+    lia.
+  + remember (z :: l1) as l eqn: Hl.
+    unfold list_store_Z_compact in H.
+    destruct H, H0.
+    assert (list_store_Z l n). {
+      unfold list_store_Z.
+      tauto.
+    }
+    clear H1 H.
+    split.
+    - pose proof (@nil_cons Z z l1); rewrite <-Hl in H.
+      pose proof (@app_removelast_last Z l 1 ltac:(auto)).
+      clear H.
+      rewrite H1 in H2.
+      apply list_store_Z_split in H2; destruct H2.
+      remember (Zlength (removelast l)) as len_lo eqn:Hlen_lo.
+      remember (n mod UINT_MOD ^ len_lo) as n_lo eqn:Hnlo.
+      remember (n / UINT_MOD ^ len_lo) as n_hi eqn:Hnhi.
+      assert (n = n_lo + n_hi * UINT_MOD ^ len_lo). {
+        pose proof (Z_div_mod_eq_full n (UINT_MOD ^ len_lo)).
+        lia.
+      }
+      unfold list_store_Z in H2; destruct H2.
+      simpl in H2.
+      apply list_store_Z_bound in H.
+      pose proof (@nil_cons Z z l1); rewrite <-Hl in H5.
+      pose proof (Aux.Zlength_removelast l ltac:(auto)).
+      clear H5.
+      rewrite H6 in *.
+      rewrite H2 in H0.
+      rewrite Hlen_lo in *.
+      nia.
+    - apply list_store_Z_bound in H2.
+      lia.
+Qed.
+
 Lemma list_store_Z_nth: forall (l: list Z) (n: Z) (i: Z),
   0 <= i < Zlength l ->
   list_store_Z l n ->
diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v
index 2df150a..13564f5 100755
--- a/projects/lib/gmp_goal.v
+++ b/projects/lib/gmp_goal.v
@@ -3679,6 +3679,215 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2:
 
 Definition mpz_realloc_partial_solve_wit_10 := mpz_realloc_partial_solve_wit_10_pure -> mpz_realloc_partial_solve_wit_10_aux.
 
+(*----- Function mpz_sgn -----*)
+
+Definition mpz_sgn_safety_wit_1 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((( &( "u" ) )) # Ptr  |-> u_pre)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_sgn_safety_wit_2 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size < 0) |] 
+  &&  [| (retval = (-1)) |] 
+  &&  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((( &( "u" ) )) # Ptr  |-> u_pre)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| False |]
+.
+
+Definition mpz_sgn_safety_wit_3 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((( &( "u" ) )) # Ptr  |-> u_pre)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_sgn_safety_wit_4 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size = 0) |] 
+  &&  [| (retval = 0) |] 
+  &&  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((( &( "u" ) )) # Ptr  |-> u_pre)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| False |]
+.
+
+Definition mpz_sgn_safety_wit_5 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size > 0) |] 
+  &&  [| (retval = 1) |] 
+  &&  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((( &( "u" ) )) # Ptr  |-> u_pre)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| False |]
+.
+
+Definition mpz_sgn_return_wit_1_1 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size < 0) |] 
+  &&  [| (retval = (-1)) |] 
+  &&  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  ([| (n < 0) |] 
+  &&  [| (retval = (-1)) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n = 0) |] 
+  &&  [| (retval = 0) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n > 0) |] 
+  &&  [| (retval = 1) |]
+  &&  (store_Z u_pre n ))
+.
+
+Definition mpz_sgn_return_wit_1_2 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size > 0) |] 
+  &&  [| (retval = 1) |] 
+  &&  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  ([| (n < 0) |] 
+  &&  [| (retval = (-1)) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n = 0) |] 
+  &&  [| (retval = 0) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n > 0) |] 
+  &&  [| (retval = 1) |]
+  &&  (store_Z u_pre n ))
+.
+
+Definition mpz_sgn_return_wit_1_3 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
+  [| (size = 0) |] 
+  &&  [| (retval = 0) |] 
+  &&  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  ([| (n < 0) |] 
+  &&  [| (retval = (-1)) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n = 0) |] 
+  &&  [| (retval = 0) |]
+  &&  (store_Z u_pre n ))
+  ||
+  ([| (n > 0) |] 
+  &&  [| (retval = 1) |]
+  &&  (store_Z u_pre n ))
+.
+
+Definition mpz_sgn_partial_solve_wit_1 := 
+forall (u_pre: Z) (n: Z) ,
+  (store_Z u_pre n )
+|--
+  (store_Z u_pre n )
+.
+
+Definition mpz_sgn_partial_solve_wit_2 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_sgn_partial_solve_wit_3 := 
+forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_sgn_which_implies_wit_1 := 
+forall (n: Z) (u: Z) ,
+  (store_Z u n )
+|--
+  (EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr))
+  ||
+  (EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((u)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr))
+.
+
 Module Type VC_Correct.
 
 Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1.
@@ -3810,5 +4019,17 @@ Axiom proof_of_mpz_realloc_partial_solve_wit_9_pure : mpz_realloc_partial_solve_
 Axiom proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9.
 Axiom proof_of_mpz_realloc_partial_solve_wit_10_pure : mpz_realloc_partial_solve_wit_10_pure.
 Axiom proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
+Axiom proof_of_mpz_sgn_safety_wit_1 : mpz_sgn_safety_wit_1.
+Axiom proof_of_mpz_sgn_safety_wit_2 : mpz_sgn_safety_wit_2.
+Axiom proof_of_mpz_sgn_safety_wit_3 : mpz_sgn_safety_wit_3.
+Axiom proof_of_mpz_sgn_safety_wit_4 : mpz_sgn_safety_wit_4.
+Axiom proof_of_mpz_sgn_safety_wit_5 : mpz_sgn_safety_wit_5.
+Axiom proof_of_mpz_sgn_return_wit_1_1 : mpz_sgn_return_wit_1_1.
+Axiom proof_of_mpz_sgn_return_wit_1_2 : mpz_sgn_return_wit_1_2.
+Axiom proof_of_mpz_sgn_return_wit_1_3 : mpz_sgn_return_wit_1_3.
+Axiom proof_of_mpz_sgn_partial_solve_wit_1 : mpz_sgn_partial_solve_wit_1.
+Axiom proof_of_mpz_sgn_partial_solve_wit_2 : mpz_sgn_partial_solve_wit_2.
+Axiom proof_of_mpz_sgn_partial_solve_wit_3 : mpz_sgn_partial_solve_wit_3.
+Axiom proof_of_mpz_sgn_which_implies_wit_1 : mpz_sgn_which_implies_wit_1.
 
 End VC_Correct.
diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v
index dd60026..47026f9 100755
--- a/projects/lib/gmp_proof_auto.v
+++ b/projects/lib/gmp_proof_auto.v
@@ -243,3 +243,27 @@ Proof. Admitted.
 Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
 Proof. Admitted. 
 
+Lemma proof_of_mpz_sgn_safety_wit_1 : mpz_sgn_safety_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_safety_wit_2 : mpz_sgn_safety_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_safety_wit_3 : mpz_sgn_safety_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_safety_wit_4 : mpz_sgn_safety_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_safety_wit_5 : mpz_sgn_safety_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_partial_solve_wit_1 : mpz_sgn_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_partial_solve_wit_2 : mpz_sgn_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_sgn_partial_solve_wit_3 : mpz_sgn_partial_solve_wit_3.
+Proof. Admitted. 
+
diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v
index 0580a17..d4847eb 100755
--- a/projects/lib/gmp_proof_manual.v
+++ b/projects/lib/gmp_proof_manual.v
@@ -1057,3 +1057,68 @@ Proof.
   Intros data.
   entailer!.
 Qed.
+
+Lemma proof_of_mpz_sgn_return_wit_1_1 : mpz_sgn_return_wit_1_1.
+Proof.
+  pre_process.
+  Left; Left.
+  entailer!.
+  unfold store_Z.
+  Exists ptr cap size.
+  Left.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_sgn_return_wit_1_2 : mpz_sgn_return_wit_1_2.
+Proof.
+  pre_process.
+  Right.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  assert (size >= 1). { lia. }
+  clear H H1.
+  entailer!.
+  + unfold store_Z.
+    Exists ptr cap size.
+    Right.
+    unfold mpd_store_Z_compact.
+    Exists data.
+    entailer!.
+  + apply list_store_Z_compact_bound in H3.
+    rewrite <-H4 in *.
+    nia.
+Qed.
+
+Lemma proof_of_mpz_sgn_return_wit_1_3 : mpz_sgn_return_wit_1_3.
+Proof.
+  pre_process.
+  Left; Right.
+  unfold store_Z.
+  Exists ptr cap size.
+  Right.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  Exists data.
+  entailer!.
+  subst.
+  pose proof (Zlength_nil_inv data ltac:(auto)).
+  subst.
+  unfold list_store_Z_compact in H3; destruct H3, H0.
+  unfold list_to_Z in H.
+  lia.
+Qed.
+
+Lemma proof_of_mpz_sgn_which_implies_wit_1 : mpz_sgn_which_implies_wit_1.
+Proof.
+  pre_process.
+  unfold store_Z.
+  Intros ptr cap size.
+  rewrite orp_sepcon_left.
+  Split.
+  + Right.
+    Exists ptr cap size.
+    entailer!.
+  + Left.
+    Exists ptr cap size.
+    entailer!.
+Qed.
diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c
index 43b2ab9..cbff291 100755
--- a/projects/mini-gmp.c
+++ b/projects/mini-gmp.c
@@ -437,7 +437,7 @@ mpz_realloc (mpz_t r, int size)
     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_size == old &&
     r@pre -> _mp_alloc == c &&
     r@pre -> _mp_d == ptr_new
 */
@@ -457,16 +457,37 @@ mpz_realloc (mpz_t r, int size)
 }
 
 /* Realloc for an mpz_t WHAT if it has less than NEEDED limbs.  */
-/*unsigned int *mrz_realloc_if(mpz_t z,int n) {
+/*unsigned int *mrz_realloc_if(mpz_t z,int n) 
+{
   return n > z->_mp_alloc ? mpz_realloc(z, n) : z->_mp_d;
 }*/
 
 /* MPZ comparisons and the like. */
-/*int
+int
 mpz_sgn (const mpz_t u)
+/*@
+  With
+    n
+  Require
+    store_Z(u, n)
+  Ensure
+    store_Z(u@pre, n) &&
+    (n > 0 && __return == 1 || n == 0 && __return == 0 ||
+      n < 0 && __return == -1)
+*/
 {
+  /*@
+    store_Z(u, n)
+    which implies
+    exists ptr cap size,
+      (size < 0 && n < 0 && mpd_store_Z_compact(ptr, -n, -size, cap) ||
+        size >= 0 && n >= 0 && mpd_store_Z_compact(ptr, n, size, cap)) &&
+      u->_mp_size == size && 
+      u->_mp_alloc == cap && 
+      u->_mp_d == ptr
+  */
   return gmp_cmp (u->_mp_size, 0);
-}*/
+}
 
 /*void
 mpz_swap (mpz_t u, mpz_t v)
diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h
index 08af83a..3115e59 100755
--- a/projects/mini-gmp.h
+++ b/projects/mini-gmp.h
@@ -93,7 +93,7 @@ unsigned int mpn_sub (unsigned int *, unsigned int *, int, unsigned int *, int);
 
 void mpz_clear (mpz_t r);
 
-int mpz_sgn (const mpz_t);
+int mpz_sgn (const mpz_t u);
 
 void mpz_neg (mpz_t, const mpz_t);
 void mpz_swap (mpz_t, mpz_t);