Signed primitive integers

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

5 files changed, 462 insertions, 5 deletions

diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 7bb725538b..a3ebe67325 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -205,6 +205,7 @@ Qed.
 Corollary to_Z_bounded : forall x, (0 <= φ  x  < wB)%Z.
 Proof. apply to_Z_rec_bounded. Qed.
 
+
 (* =================================================== *)
 Local Open Scope Z_scope.
 (* General arithmetic results *)
@@ -1904,6 +1905,22 @@ Qed.
 Lemma lxor0_r i : i lxor 0 = i.
 Proof. rewrite lxorC; exact (lxor0 i). Qed.
 
+Lemma opp_to_Z_opp (x : int) :
+    φ x mod wB <> 0 ->
+  (- φ (- x)) mod wB = (φ x) mod wB.
+Proof.
+  intros neqx0.
+  rewrite opp_spec.
+  rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption.
+  rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded.
+  rewrite <- Z.add_opp_l.
+  rewrite Z.opp_add_distr, Z.opp_involutive.
+  replace (- wB) with (-1 * wB) by easy.
+  rewrite Z_mod_plus by easy.
+  now rewrite Z.mod_small by apply to_Z_bounded.
+Qed.
+
+
 Module Export Int63Notations.
   Local Open Scope int63_scope.
   #[deprecated(since="8.13",note="use infix mod instead")]
diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v
index 64c1b862c7..98127ef0ac 100644
--- a/theories/Numbers/Cyclic/Int63/PrimInt63.v
+++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v
@@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp.
 
 Primitive int := #int63_type.
 Register int as num.int63.type.
+Variant pos_neg_int63 := Pos (d:int) | Neg (d:int).
+Register pos_neg_int63 as num.int63.pos_neg_int63.
 Declare Scope int63_scope.
 Definition id_int : int -> int := fun x => x.
-Declare ML Module "int63_syntax_plugin".
-
-Module Export Int63NotationsInternalA.
+Record int_wrapper := wrap_int {int_wrap : int}.
+Register wrap_int as num.int63.wrap_int.
+Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x).
+Definition parser (x : pos_neg_int63) : option int :=
+  match x with
+  | Pos p => Some p
+  | Neg _ => None
+  end.
+Number Notation int parser printer : int63_scope.
+
+Module Import Int63NotationsInternalA.
 Delimit Scope int63_scope with int63.
 Bind Scope int63_scope with int.
 End Int63NotationsInternalA.
@@ -37,6 +47,9 @@ Primitive lor := #int63_lor.
 
 Primitive lxor := #int63_lxor.
 
+
+Primitive asr := #int63_asr.
+
 (* Arithmetic modulo operations *)
 Primitive add := #int63_add.
 
@@ -50,6 +63,10 @@ Primitive div := #int63_div.
 
 Primitive mod := #int63_mod.
 
+Primitive divs := #int63_divs.
+
+Primitive mods := #int63_mods.
+
 (* Comparisons *)
 Primitive eqb := #int63_eq.
 
@@ -57,6 +74,10 @@ Primitive ltb := #int63_lt.
 
 Primitive leb := #int63_le.
 
+Primitive ltsb := #int63_lts.
+
+Primitive lesb := #int63_les.
+
 (** Exact arithmetic operations *)
 
 Primitive addc := #int63_addc.
@@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv.
 (** Comparison *)
 Primitive compare := #int63_compare.
 
+Primitive compares := #int63_compares.
+
 (** Exotic operations *)
 
 Primitive head0 := #int63_head0.
 Primitive tail0 := #int63_tail0.
+
+Module Export PrimInt63Notations.
+  Export Int63NotationsInternalA.
+End PrimInt63Notations.
diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v
new file mode 100644
index 0000000000..c0239ae3db
--- /dev/null
+++ b/theories/Numbers/Cyclic/Int63/Sint63.v
@@ -0,0 +1,407 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ZArith.
+Import Znumtheory.
+Require Export Int63.
+Require Import Lia.
+
+Declare Scope sint63_scope.
+Definition printer (x : int_wrapper) : pos_neg_int63 :=
+  if (int_wrap x <? 4611686018427387904)%int63 then (* 2^62 *)
+    Pos (int_wrap x)
+  else
+    Neg ((int_wrap x) lxor max_int + 1)%int63.
+Definition parser (x : pos_neg_int63) : option int :=
+  match x with
+  | Pos p => if (p <? 4611686018427387904)%int63 then Some p else None
+  | Neg n => if (n <=? 4611686018427387904)%int63
+             then Some ((n - 1) lxor max_int)%int63 else None
+  end.
+Number Notation int parser printer : sint63_scope.
+
+
+Module Import Sint63NotationsInternalA.
+Delimit Scope sint63_scope with sint63.
+Bind Scope sint63_scope with int.
+End Sint63NotationsInternalA.
+
+
+Module Import Sint63NotationsInternalB.
+Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope.
+(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *)
+Infix ">>" := asr (at level 30, no associativity) : sint63_scope.
+Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope.
+Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope.
+Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope.
+Infix "+" := Int63.add : sint63_scope.
+Infix "-" := Int63.sub : sint63_scope.
+Infix "*" := Int63.mul : sint63_scope.
+Infix "/" := divs : sint63_scope.
+Infix "mod" := mods (at level 40, no associativity) : sint63_scope.
+Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope.
+Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope.
+Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope.
+Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope.
+Notation "- x" := (opp x) : sint63_scope.
+Notation "n ?= m" := (compares n m) (at level 70, no associativity) : sint63_scope.
+End Sint63NotationsInternalB.
+
+Definition min_int := Eval vm_compute in (lsl 1 62).
+Definition max_int := Eval vm_compute in (min_int - 1)%sint63.
+
+(** Translation to and from Z *)
+Definition to_Z (i:int) :=
+  if (i <? min_int)%int63 then
+    φ i%int63
+  else
+    (- φ (- i)%int63)%Z.
+
+Lemma to_Z_0 : to_Z 0 = 0.
+Proof. easy. Qed.
+
+Lemma to_Z_min : to_Z min_int = - (wB / 2).
+Proof. easy. Qed.
+
+Lemma to_Z_max : to_Z max_int = wB / 2 - 1.
+Proof. easy. Qed.
+
+Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z.
+Proof.
+  intros x; unfold to_Z.
+  case ltbP; [> lia | intros _].
+  case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H].
+  rewrite opp_spec.
+  rewrite Z_mod_nz_opp_full by easy.
+  rewrite Z.mod_small by apply Int63.to_Z_bounded.
+  case ltbP.
+  - intros ltxmin; split.
+    + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded].
+    + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin.
+      * lia.
+      * now compute.
+  - rewrite Z.nlt_ge; intros leminx.
+    rewrite opp_spec.
+    rewrite Z_mod_nz_opp_full.
+    + rewrite Z.mod_small by apply Int63.to_Z_bounded.
+      split.
+      * rewrite <- Z.opp_le_mono.
+        now rewrite <- Z.sub_le_mono_l.
+      * transitivity 0%Z; [>| now apply Int63.to_Z_bounded].
+        rewrite Z.opp_nonpos_nonneg.
+        apply Zle_minus_le_0.
+        apply Z.lt_le_incl.
+        now apply Int63.to_Z_bounded.
+    + rewrite Z.mod_small by apply Int63.to_Z_bounded.
+      now intros eqx0; rewrite eqx0 in leminx.
+Qed.
+
+Lemma of_to_Z : forall x, of_Z (to_Z x) = x.
+Proof.
+  unfold to_Z, of_Z.
+  intros x.
+  generalize (Int63.to_Z_bounded x).
+  case ltbP.
+  - intros ltxmin [leq0x _].
+    generalize (Int63.of_to_Z x).
+    destruct (φ x%int63).
+    + now intros <-.
+    + now intros <-; unfold Int63.of_Z.
+    + now intros _.
+  - intros nltxmin leq0xltwB.
+    rewrite (opp_spec x).
+    rewrite Z_mod_nz_opp_full.
+    + rewrite Zmod_small by easy.
+      destruct (wB - φ x%int63) eqn: iswbmx.
+      * lia.
+      * simpl.
+        apply to_Z_inj.
+        rewrite opp_spec.
+        generalize (of_Z_spec (Z.pos p)).
+        simpl Int63.of_Z; intros ->.
+        rewrite <- iswbmx.
+        rewrite <- Z.sub_0_l.
+        rewrite <- (Zmod_0_l wB).
+        rewrite <- Zminus_mod.
+        replace (0 - _) with (φ x%int63 - wB) by ring.
+        rewrite <- Zminus_mod_idemp_r.
+        rewrite Z_mod_same_full.
+        rewrite Z.sub_0_r.
+        now rewrite Z.mod_small.
+      * lia.
+    + rewrite Z.mod_small by easy.
+      intros eqx0; revert nltxmin; rewrite eqx0.
+      now compute.
+Qed.
+
+Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y.
+Proof. exact (fun e => can_inj of_to_Z e). Qed.
+
+Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63.
+Proof.
+  unfold to_Z.
+  case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |].
+  rewrite Z.nlt_ge; intros gexmin.
+  rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded.
+  - easy.
+  - now intros neqx0; rewrite neqx0 in gexmin.
+Qed.
+
+
+(** Centered modulo *)
+Definition cmod (x d : Z) : Z :=
+  (x + d / 2) mod d - (d / 2).
+
+Lemma cmod_mod (x d : Z) :
+  cmod (x mod d) d = cmod x d.
+Proof.
+  now unfold cmod; rewrite Zplus_mod_idemp_l.
+Qed.
+
+Lemma cmod_small (x d : Z) :
+  - (d / 2) <= x < d / 2 -> cmod x d = x.
+Proof.
+  intros bound.
+  unfold cmod.
+  rewrite Zmod_small; [> lia |].
+  split; [> lia |].
+  rewrite Z.lt_add_lt_sub_r.
+  apply (Z.lt_le_trans _ (d / 2)); [> easy |].
+  now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le.
+Qed.
+
+Lemma to_Z_cmodwB (x : int) :
+  to_Z x = cmod (φ x%int63) wB.
+Proof.
+  unfold to_Z, cmod.
+  case ltbP; change φ (min_int)%int63 with (wB / 2).
+  - intros ltxmin.
+    rewrite Z.mod_small; [> lia |].
+    split.
+    + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded.
+    + change wB with (wB / 2 + wB / 2) at 2; lia.
+  - rewrite Z.nlt_ge; intros gexmin.
+    rewrite Int63.opp_spec.
+    rewrite Z_mod_nz_opp_full.
+    + rewrite Z.mod_small by apply Int63.to_Z_bounded.
+      rewrite <- (Z_mod_plus_full _ (-1)).
+      change (-1 * wB) with (- (wB / 2) - wB / 2).
+      rewrite <- Z.add_assoc, Zplus_minus.
+      rewrite Z.mod_small.
+      * change wB with (wB / 2 + wB / 2) at 1; lia.
+      * split; [> lia |].
+        apply Z.lt_sub_lt_add_r.
+        transitivity wB; [>| easy].
+        now apply Int63.to_Z_bounded.
+    + rewrite Z.mod_small by now apply Int63.to_Z_bounded.
+      now intros not0; rewrite not0 in gexmin.
+Qed.
+
+Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB.
+Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed.
+
+Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z.
+Proof. now rewrite <- of_Z_spec, of_to_Z. Qed.
+
+Lemma is_int (z : Z) :
+    to_Z min_int <= z <= to_Z max_int ->
+  z = to_Z (of_Z z).
+Proof.
+  rewrite to_Z_min, to_Z_max.
+  intros bound; rewrite of_Z_spec, cmod_small; lia.
+Qed.
+
+(** Specification of operations that differ on signed and unsigned ints *)
+
+Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p).
+
+Axiom div_spec : forall x y,
+    to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z ->
+  to_Z (x / y) = Z.quot (to_Z x) (to_Z y).
+
+Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y).
+
+Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y.
+
+Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y.
+
+Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y).
+
+(** Specification of operations that coincide on signed and unsigned ints *)
+
+Lemma add_spec (x y : int) :
+  to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB.
+Proof.
+  rewrite to_Z_cmodwB, Int63.add_spec.
+  rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy.
+  now rewrite cmod_mod.
+Qed.
+
+Lemma sub_spec (x y : int) :
+  to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB.
+Proof.
+  rewrite to_Z_cmodwB, Int63.sub_spec.
+  rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy.
+  now rewrite cmod_mod.
+Qed.
+
+Lemma mul_spec (x y : int) :
+  to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB.
+Proof.
+  rewrite to_Z_cmodwB, Int63.mul_spec.
+  rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy.
+  now rewrite cmod_mod.
+Qed.
+
+Lemma succ_spec (x : int) :
+  to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB.
+Proof. now unfold succ; rewrite add_spec. Qed.
+
+Lemma pred_spec (x : int) :
+  to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB.
+Proof. now unfold pred; rewrite sub_spec. Qed.
+
+Lemma opp_spec (x : int) :
+  to_Z (- x)%sint63 = cmod (- to_Z x) wB.
+Proof.
+  rewrite to_Z_cmodwB, Int63.opp_spec.
+  rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r.
+  now rewrite cmod_mod.
+Qed.
+
+(** Behaviour when there is no under or overflow *)
+
+Lemma add_bounded (x y : int) :
+    to_Z min_int <= to_Z x + to_Z y <= to_Z max_int ->
+  to_Z (x + y) = to_Z x + to_Z y.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite add_spec, cmod_small; [>| lia].
+Qed.
+
+Lemma sub_bounded (x y : int) :
+    to_Z min_int <= to_Z x - to_Z y <= to_Z max_int ->
+  to_Z (x - y) = to_Z x - to_Z y.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite sub_spec, cmod_small; [>| lia].
+Qed.
+
+Lemma mul_bounded (x y : int) :
+    to_Z min_int <= to_Z x * to_Z y <= to_Z max_int ->
+  to_Z (x * y) = to_Z x * to_Z y.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite mul_spec, cmod_small; [>| lia].
+Qed.
+
+Lemma succ_bounded (x : int) :
+    to_Z min_int <= to_Z x + 1 <= to_Z max_int ->
+  to_Z (succ x) = to_Z x + 1.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite succ_spec, cmod_small; [>| lia].
+Qed.
+
+Lemma pred_bounded (x : int) :
+    to_Z min_int <= to_Z x - 1 <= to_Z max_int ->
+  to_Z (pred x) = to_Z x - 1.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite pred_spec, cmod_small; [>| lia].
+Qed.
+
+Lemma opp_bounded (x : int) :
+    to_Z min_int <= - to_Z x <= to_Z max_int ->
+  to_Z (- x) = - to_Z x.
+Proof.
+  rewrite to_Z_min, to_Z_max; intros bound.
+  now rewrite opp_spec, cmod_small; [>| lia].
+Qed.
+
+(** Relationship with of_Z *)
+
+Lemma add_of_Z (x y : int) :
+  (x + y)%sint63 = of_Z (to_Z x + to_Z y).
+Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed.
+
+Lemma sub_of_Z (x y : int) :
+  (x - y)%sint63 = of_Z (to_Z x - to_Z y).
+Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed.
+
+Lemma mul_of_Z (x y : int) :
+  (x * y)%sint63 = of_Z (to_Z x * to_Z y).
+Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed.
+
+Lemma succ_of_Z (x : int) :
+  (succ x)%sint63 = of_Z (to_Z x + 1).
+Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed.
+
+Lemma pred_of_Z (x : int) :
+  (pred x)%sint63 = of_Z (to_Z x - 1).
+Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed.
+
+Lemma opp_of_Z (x : int) :
+  (- x)%sint63 = of_Z (- to_Z x).
+Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed.
+
+(** Comparison *)
+Import Bool.
+
+Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63.
+Proof.
+  apply iff_reflect; rewrite Int63.eqb_spec.
+  now split; [> apply to_Z_inj | apply f_equal].
+Qed.
+
+Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63.
+Proof. now apply iff_reflect; symmetry; apply ltb_spec. Qed.
+
+Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63.
+Proof. now apply iff_reflect; symmetry; apply leb_spec. Qed.
+
+(** ASR *)
+Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63.
+Proof. now apply to_Z_inj; rewrite asr_spec. Qed.
+
+Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i.
+Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed.
+
+Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63.
+Proof.
+  intros ltn0.
+  apply to_Z_inj.
+  rewrite asr_spec, Z.pow_neg_r by assumption.
+  now rewrite Zdiv_0_r.
+Qed.
+
+Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63.
+Proof.
+  apply to_Z_inj; rewrite asr_spec.
+  case eqbP; [> now intros -> | intros neqn0].
+  case (lebP 0 n).
+  - intros le0n.
+    apply Z.div_1_l; apply Z.pow_gt_1; [> easy |].
+    rewrite to_Z_0 in *; lia.
+  - rewrite Z.nle_gt; intros ltn0.
+    now rewrite Z.pow_neg_r.
+Qed.
+
+Notation asr := asr (only parsing).
+Notation div := divs (only parsing).
+Notation rem := mods (only parsing).
+Notation ltb := ltsb (only parsing).
+Notation leb := lesb (only parsing).
+Notation compare := compares (only parsing).
+
+Module Export Sint63Notations.
+  Export Sint63NotationsInternalA.
+  Export Sint63NotationsInternalB.
+End Sint63Notations.
diff --git a/theories/dune b/theories/dune
index 18e000cfe1..90e9522b7b 100644
--- a/theories/dune
+++ b/theories/dune
@@ -15,7 +15,6 @@
    coq.plugins.firstorder
 
    coq.plugins.number_string_notation
-   coq.plugins.int63_syntax
    coq.plugins.float_syntax
 
    coq.plugins.btauto
diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v
index 7f7b4af98d..1949a1a9d8 100644
--- a/theories/extraction/ExtrOCamlInt63.v
+++ b/theories/extraction/ExtrOCamlInt63.v
@@ -10,7 +10,7 @@
 
 (** Extraction to OCaml of native 63-bit machine integers. *)
 
-From Coq Require Int63 Extraction.
+From Coq Require Int63 Sint63 Extraction.
 
 (** Basic data types used by some primitive operators. *)
 
@@ -26,6 +26,7 @@ Extraction Inline Int63.int.
 
 Extract Constant Int63.lsl => "Uint63.l_sl".
 Extract Constant Int63.lsr => "Uint63.l_sr".
+Extract Constant Sint63.asr => "Uint63.a_sr".
 Extract Constant Int63.land => "Uint63.l_and".
 Extract Constant Int63.lor => "Uint63.l_or".
 Extract Constant Int63.lxor => "Uint63.l_xor".
@@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul".
 Extract Constant Int63.mulc => "Uint63.mulc".
 Extract Constant Int63.div => "Uint63.div".
 Extract Constant Int63.mod => "Uint63.rem".
+Extract Constant Sint63.div => "Uint63.divs".
+Extract Constant Sint63.rem => "Uint63.rems".
+
 
 Extract Constant Int63.eqb => "Uint63.equal".
 Extract Constant Int63.ltb => "Uint63.lt".
 Extract Constant Int63.leb => "Uint63.le".
+Extract Constant Sint63.ltb => "Uint63.lts".
+Extract Constant Sint63.leb => "Uint63.les".
 
 Extract Constant Int63.addc => "Uint63.addc".
 Extract Constant Int63.addcarryc => "Uint63.addcarryc".
@@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21".
 Extract Constant Int63.addmuldiv => "Uint63.addmuldiv".
 
 Extract Constant Int63.compare => "Uint63.compare".
+Extract Constant Sint63.compare => "Uint63.compares".
 
 Extract Constant Int63.head0 => "Uint63.head0".
 Extract Constant Int63.tail0 => "Uint63.tail0".