Update number/string conversions

To updated version of https://github.com/coq/coq/pull/6597

6 files changed, 531 insertions, 429 deletions

diff --git a/src/Util/Strings/Binary.v b/src/Util/Strings/Binary.v
deleted file mode 100644
index 955c6c8f6..000000000
--- a/src/Util/Strings/Binary.v
+++ /dev/null
@@ -1,72 +0,0 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String.
-Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Util.Strings.Equality.
-Require Crypto.Util.Pos.
-Import BinPosDef.
-
-Local Open Scope positive_scope.
-Local Open Scope string_scope.
-
-Fixpoint bin_string_of_pos' (p : positive) (rest : string) : string
-  := match p with
-     | 1 => String "1" rest
-     | p'~0 => bin_string_of_pos' p' (String "0" rest)
-     | p'~1 => bin_string_of_pos' p' (String "1" rest)
-     end.
-Definition bin_string_of_pos (p : positive) : string
-  := String "0" (String "b" (bin_string_of_pos' p "")).
-
-Local Notation default := 1.
-
-Fixpoint pos_of_bin_string' (s : string) (rest : option positive)
-  : option positive
-  := match s with
-     | "" => rest
-     | String ch s'
-       => pos_of_bin_string'
-            s'
-            (if ascii_beq ch "0"
-             then option_map xO rest
-             else if ascii_beq ch "1"
-                  then match rest with
-                       | Some p => Some (xI p)
-                       | None => Some xH
-                       end
-                  else None)
-     end.
-Definition pos_of_bin_string (s : string) : positive
-  := match s with
-     | String s0 (String sb s)
-       => if ascii_beq s0 "0"
-          then if ascii_beq sb "b"
-               then match pos_of_bin_string' s None with
-                    | Some p => p
-                    | None => default
-                    end
-               else default
-          else default
-     | _ => default
-     end.
-
-Lemma pos_of_bin_string_of_pos' (p : positive)
-      (base : option positive)
-      (rest : string)
-  : pos_of_bin_string' (bin_string_of_pos' p rest) base
-    = pos_of_bin_string' rest (match base with
-                               | None => Some p
-                               | Some v => Some (Pos.app v p)
-                               end).
-Proof.
-  revert base rest; induction p, base; intros; try reflexivity;
-    cbn; rewrite IHp; reflexivity.
-Qed.
-
-Lemma pos_of_bin_string_of_pos (p : positive)
-  : pos_of_bin_string (bin_string_of_pos p) = p.
-Proof.
-  cbn; rewrite pos_of_bin_string_of_pos'; reflexivity.
-Qed.
-
-Example bin_string_of_pos_1 : bin_string_of_pos 1 = "0b1" := eq_refl.
-Example bin_string_of_pos_2 : bin_string_of_pos 2 = "0b10" := eq_refl.
-Example bin_string_of_pos_3 : bin_string_of_pos 3 = "0b11" := eq_refl.
diff --git a/src/Util/Strings/BinaryString.v b/src/Util/Strings/BinaryString.v
new file mode 100644
index 000000000..26c18ed51
--- /dev/null
+++ b/src/Util/Strings/BinaryString.v
@@ -0,0 +1,139 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Coq.Numbers.BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Definition ascii_to_digit (ch : ascii) : option N
+  := (if ascii_dec ch "0" then Some 0
+      else if ascii_dec ch "1" then Some 1
+      else None)%N.
+
+Fixpoint pos_bin_app (p q:positive) : positive :=
+  match q with
+  | q~0 => (pos_bin_app p q)~0
+  | q~1 => (pos_bin_app p q)~1
+  | 1 => p~1
+  end.
+
+Module Raw.
+  Fixpoint of_pos (p : positive) (rest : string) : string
+    := match p with
+       | 1 => String "1" rest
+       | p'~0 => of_pos p' (String "0" rest)
+       | p'~1 => of_pos p' (String "1" rest)
+       end.
+
+  Fixpoint to_N (s : string) (rest : N)
+    : N
+    := match s with
+       | "" => rest
+       | String ch s'
+         => to_N
+              s'
+              match ascii_to_digit ch with
+              | Some v => N.add v (N.double rest)
+              | None => N0
+              end
+       end.
+
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+    : to_N (of_pos p rest) base
+      = to_N rest match base with
+                  | N0 => N.pos p
+                  | Npos v => Npos (pos_bin_app v p)
+                  end.
+  Proof.
+    destruct p as [p|p|]; destruct base; try reflexivity;
+      cbn; rewrite to_N_of_pos; reflexivity.
+  Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+  := String "0" (String "b" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+  := match n with
+     | N0 => "0b0"
+     | Npos p => of_pos p
+     end.
+Definition of_Z (z : Z) : string
+  := match z with
+     | Zneg p => String "-" (of_pos p)
+     | Z0 => "0b0"
+     | Zpos p => of_pos p
+     end.
+Definition of_nat (n : nat) : string
+  := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+  := match s with
+     | String s0 (String sb s)
+       => if ascii_dec s0 "0"
+          then if ascii_dec sb "b"
+               then Raw.to_N s N0
+               else N0
+          else N0
+     | _ => N0
+     end.
+Definition to_pos (s : string) : positive
+  := match to_N s with
+     | N0 => 1
+     | Npos p => p
+     end.
+Definition to_Z (s : string) : Z
+  := let '(is_neg, n) := match s with
+                         | String s0 s'
+                           => if ascii_dec s0 "-"
+                              then (true, to_N s')
+                              else (false, to_N s)
+                         | EmptyString => (false, to_N s)
+                         end in
+     match n with
+     | N0 => Z0
+     | Npos p => if is_neg then Zneg p else Zpos p
+     end.
+Definition to_nat (s : string) : nat
+  := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+  : to_N (of_N n)
+    = n.
+Proof.
+  destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma Z_of_of_Z (z : Z)
+  : to_Z (of_Z z)
+    = z.
+Proof.
+  cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+    try reflexivity;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+  : to_nat (of_nat n)
+    = n.
+Proof.
+  cbv [to_nat of_nat];
+    rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+  : to_pos (of_pos p)
+    = p.
+Proof.
+  cbv [of_pos to_pos to_N]; cbn;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0b1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0b10" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0b11" := eq_refl.
+Example of_N_0 : of_N 0 = "0b0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0b0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0b1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0b0" := eq_refl.
diff --git a/src/Util/Strings/Hex.v b/src/Util/Strings/Hex.v
deleted file mode 100644
index 62919901a..000000000
--- a/src/Util/Strings/Hex.v
+++ /dev/null
@@ -1,219 +0,0 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String.
-Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Util.Strings.Equality.
-Require Crypto.Util.Pos.
-Import BinPosDef.
-
-Local Open Scope bool_scope.
-Local Open Scope positive_scope.
-Local Open Scope string_scope.
-
-Fixpoint hex_string_of_pos' (p : positive) (rest : string) : string
-  := match p with
-     | 1 => String "1" rest
-     | 2 => String "2" rest
-     | 3 => String "3" rest
-     | 4 => String "4" rest
-     | 5 => String "5" rest
-     | 6 => String "6" rest
-     | 7 => String "7" rest
-     | 8 => String "8" rest
-     | 9 => String "9" rest
-     | 10 => String "a" rest
-     | 11 => String "b" rest
-     | 12 => String "c" rest
-     | 13 => String "d" rest
-     | 14 => String "e" rest
-     | 15 => String "f" rest
-     | p'~0~0~0~0 => hex_string_of_pos' p' (String "0" rest)
-     | p'~0~0~0~1 => hex_string_of_pos' p' (String "1" rest)
-     | p'~0~0~1~0 => hex_string_of_pos' p' (String "2" rest)
-     | p'~0~0~1~1 => hex_string_of_pos' p' (String "3" rest)
-     | p'~0~1~0~0 => hex_string_of_pos' p' (String "4" rest)
-     | p'~0~1~0~1 => hex_string_of_pos' p' (String "5" rest)
-     | p'~0~1~1~0 => hex_string_of_pos' p' (String "6" rest)
-     | p'~0~1~1~1 => hex_string_of_pos' p' (String "7" rest)
-     | p'~1~0~0~0 => hex_string_of_pos' p' (String "8" rest)
-     | p'~1~0~0~1 => hex_string_of_pos' p' (String "9" rest)
-     | p'~1~0~1~0 => hex_string_of_pos' p' (String "a" rest)
-     | p'~1~0~1~1 => hex_string_of_pos' p' (String "b" rest)
-     | p'~1~1~0~0 => hex_string_of_pos' p' (String "c" rest)
-     | p'~1~1~0~1 => hex_string_of_pos' p' (String "d" rest)
-     | p'~1~1~1~0 => hex_string_of_pos' p' (String "e" rest)
-     | p'~1~1~1~1 => hex_string_of_pos' p' (String "f" rest)
-     end.
-Definition hex_string_of_pos (p : positive) : string
-  := String "0" (String "x" (hex_string_of_pos' p "")).
-
-Local Notation default := 1.
-
-Fixpoint pos_of_hex_string' (s : string) (rest : option positive)
-  : option positive
-  := match s with
-     | "" => rest
-     | String ch s'
-       => pos_of_hex_string'
-            s'
-            (if ascii_beq ch "0"
-             then match rest with
-                  | Some p => Some (p~0~0~0~0)
-                  | None => None
-                  end
-             else if ascii_beq ch "1"
-             then match rest with
-                  | Some p => Some (p~0~0~0~1)
-                  | None => Some 1
-                  end
-             else if ascii_beq ch "2"
-             then match rest with
-                  | Some p => Some (p~0~0~1~0)
-                  | None => Some 2
-                  end
-             else if ascii_beq ch "3"
-             then match rest with
-                  | Some p => Some (p~0~0~1~1)
-                  | None => Some 3
-                  end
-             else if ascii_beq ch "4"
-             then match rest with
-                  | Some p => Some (p~0~1~0~0)
-                  | None => Some 4
-                  end
-             else if ascii_beq ch "5"
-             then match rest with
-                  | Some p => Some (p~0~1~0~1)
-                  | None => Some 5
-                  end
-             else if ascii_beq ch "6"
-             then match rest with
-                  | Some p => Some (p~0~1~1~0)
-                  | None => Some 6
-                  end
-             else if ascii_beq ch "7"
-             then match rest with
-                  | Some p => Some (p~0~1~1~1)
-                  | None => Some 7
-                  end
-             else if ascii_beq ch "8"
-             then match rest with
-                  | Some p => Some (p~1~0~0~0)
-                  | None => Some 8
-                  end
-             else if ascii_beq ch "9"
-             then match rest with
-                  | Some p => Some (p~1~0~0~1)
-                  | None => Some 9
-                  end
-             else if ascii_beq ch "a" || ascii_beq ch "A"
-             then match rest with
-                  | Some p => Some (p~1~0~1~0)
-                  | None => Some 10
-                  end
-             else if ascii_beq ch "b" || ascii_beq ch "B"
-             then match rest with
-                  | Some p => Some (p~1~0~1~1)
-                  | None => Some 11
-                  end
-             else if ascii_beq ch "c" || ascii_beq ch "C"
-             then match rest with
-                  | Some p => Some (p~1~1~0~0)
-                  | None => Some 12
-                  end
-             else if ascii_beq ch "d" || ascii_beq ch "D"
-             then match rest with
-                  | Some p => Some (p~1~1~0~1)
-                  | None => Some 13
-                  end
-             else if ascii_beq ch "e" || ascii_beq ch "E"
-             then match rest with
-                  | Some p => Some (p~1~1~1~0)
-                  | None => Some 14
-                  end
-             else if ascii_beq ch "f" || ascii_beq ch "F"
-             then match rest with
-                  | Some p => Some (p~1~1~1~1)
-                  | None => Some 15
-                  end
-             else None)
-     end.
-Definition pos_of_hex_string (s : string) : positive
-  := match s with
-     | String s0 (String sb s)
-       => if ascii_beq s0 "0"
-          then if ascii_beq sb "x"
-               then match pos_of_hex_string' s None with
-                    | Some p => p
-                    | None => default
-                    end
-               else default
-          else default
-     | _ => default
-     end.
-
-Fixpoint pos_hex_app (p q:positive) : positive :=
-  match q with
-  | 1 => p~0~0~0~1
-  | 2 => p~0~0~1~0
-  | 3 => p~0~0~1~1
-  | 4 => p~0~1~0~0
-  | 5 => p~0~1~0~1
-  | 6 => p~0~1~1~0
-  | 7 => p~0~1~1~1
-  | 8 => p~1~0~0~0
-  | 9 => p~1~0~0~1
-  | 10 => p~1~0~1~0
-  | 11 => p~1~0~1~1
-  | 12 => p~1~1~0~0
-  | 13 => p~1~1~0~1
-  | 14 => p~1~1~1~0
-  | 15 => p~1~1~1~1
-  | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0
-  | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1
-  | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0
-  | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1
-  | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0
-  | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1
-  | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0
-  | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1
-  | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0
-  | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1
-  | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0
-  | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1
-  | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0
-  | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1
-  | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0
-  | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1
-  end.
-
-Fixpoint pos_of_hex_string_of_pos' (p : positive)
-      (base : option positive)
-      (rest : string)
-  : pos_of_hex_string' (hex_string_of_pos' p rest) base
-    = pos_of_hex_string' rest (match base with
-                               | None => Some p
-                               | Some v => Some (pos_hex_app v p)
-                               end).
-Proof.
-  do 4 try destruct p as [p|p|]; destruct base; try reflexivity;
-    cbn; rewrite pos_of_hex_string_of_pos'; reflexivity.
-Qed.
-
-Lemma pos_of_hex_string_of_pos (p : positive)
-  : pos_of_hex_string (hex_string_of_pos p) = p.
-Proof.
-  cbn; rewrite pos_of_hex_string_of_pos'; reflexivity.
-Qed.
-
-Example hex_string_of_pos_1 : hex_string_of_pos 1 = "0x1" := eq_refl.
-Example hex_string_of_pos_2 : hex_string_of_pos 2 = "0x2" := eq_refl.
-Example hex_string_of_pos_3 : hex_string_of_pos 3 = "0x3" := eq_refl.
-Example hex_string_of_pos_7 : hex_string_of_pos 7 = "0x7" := eq_refl.
-Example hex_string_of_pos_8 : hex_string_of_pos 8 = "0x8" := eq_refl.
-Example hex_string_of_pos_9 : hex_string_of_pos 9 = "0x9" := eq_refl.
-Example hex_string_of_pos_10 : hex_string_of_pos 10 = "0xa" := eq_refl.
-Example hex_string_of_pos_11 : hex_string_of_pos 11 = "0xb" := eq_refl.
-Example hex_string_of_pos_12 : hex_string_of_pos 12 = "0xc" := eq_refl.
-Example hex_string_of_pos_13 : hex_string_of_pos 13 = "0xd" := eq_refl.
-Example hex_string_of_pos_14 : hex_string_of_pos 14 = "0xe" := eq_refl.
-Example hex_string_of_pos_15 : hex_string_of_pos 15 = "0xf" := eq_refl.
-Example hex_string_of_pos_16 : hex_string_of_pos 16 = "0x10" := eq_refl.
diff --git a/src/Util/Strings/HexString.v b/src/Util/Strings/HexString.v
new file mode 100644
index 000000000..a6c9b04d4
--- /dev/null
+++ b/src/Util/Strings/HexString.v
@@ -0,0 +1,221 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Coq.Numbers.BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Local Notation "a || b"
+  := (if a then true else if b then true else false).
+Definition ascii_to_digit (ch : ascii) : option N
+  := (if ascii_dec ch "0" then Some 0
+      else if ascii_dec ch "1" then Some 1
+      else if ascii_dec ch "2" then Some 2
+      else if ascii_dec ch "3" then Some 3
+      else if ascii_dec ch "4" then Some 4
+      else if ascii_dec ch "5" then Some 5
+      else if ascii_dec ch "6" then Some 6
+      else if ascii_dec ch "7" then Some 7
+      else if ascii_dec ch "8" then Some 8
+      else if ascii_dec ch "9" then Some 9
+      else if ascii_dec ch "a" || ascii_dec ch "A" then Some 10
+      else if ascii_dec ch "b" || ascii_dec ch "B" then Some 11
+      else if ascii_dec ch "c" || ascii_dec ch "C" then Some 12
+      else if ascii_dec ch "d" || ascii_dec ch "D" then Some 13
+      else if ascii_dec ch "e" || ascii_dec ch "E" then Some 14
+      else if ascii_dec ch "f" || ascii_dec ch "F" then Some 15
+      else None)%N.
+
+Fixpoint pos_hex_app (p q:positive) : positive :=
+  match q with
+  | 1 => p~0~0~0~1
+  | 2 => p~0~0~1~0
+  | 3 => p~0~0~1~1
+  | 4 => p~0~1~0~0
+  | 5 => p~0~1~0~1
+  | 6 => p~0~1~1~0
+  | 7 => p~0~1~1~1
+  | 8 => p~1~0~0~0
+  | 9 => p~1~0~0~1
+  | 10 => p~1~0~1~0
+  | 11 => p~1~0~1~1
+  | 12 => p~1~1~0~0
+  | 13 => p~1~1~0~1
+  | 14 => p~1~1~1~0
+  | 15 => p~1~1~1~1
+  | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0
+  | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1
+  | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0
+  | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1
+  | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0
+  | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1
+  | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0
+  | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1
+  | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0
+  | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1
+  | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0
+  | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1
+  | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0
+  | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1
+  | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0
+  | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1
+  end.
+
+Module Raw.
+  Fixpoint of_pos (p : positive) (rest : string) : string
+    := match p with
+       | 1 => String "1" rest
+       | 2 => String "2" rest
+       | 3 => String "3" rest
+       | 4 => String "4" rest
+       | 5 => String "5" rest
+       | 6 => String "6" rest
+       | 7 => String "7" rest
+       | 8 => String "8" rest
+       | 9 => String "9" rest
+       | 10 => String "a" rest
+       | 11 => String "b" rest
+       | 12 => String "c" rest
+       | 13 => String "d" rest
+       | 14 => String "e" rest
+       | 15 => String "f" rest
+       | p'~0~0~0~0 => of_pos p' (String "0" rest)
+       | p'~0~0~0~1 => of_pos p' (String "1" rest)
+       | p'~0~0~1~0 => of_pos p' (String "2" rest)
+       | p'~0~0~1~1 => of_pos p' (String "3" rest)
+       | p'~0~1~0~0 => of_pos p' (String "4" rest)
+       | p'~0~1~0~1 => of_pos p' (String "5" rest)
+       | p'~0~1~1~0 => of_pos p' (String "6" rest)
+       | p'~0~1~1~1 => of_pos p' (String "7" rest)
+       | p'~1~0~0~0 => of_pos p' (String "8" rest)
+       | p'~1~0~0~1 => of_pos p' (String "9" rest)
+       | p'~1~0~1~0 => of_pos p' (String "a" rest)
+       | p'~1~0~1~1 => of_pos p' (String "b" rest)
+       | p'~1~1~0~0 => of_pos p' (String "c" rest)
+       | p'~1~1~0~1 => of_pos p' (String "d" rest)
+       | p'~1~1~1~0 => of_pos p' (String "e" rest)
+       | p'~1~1~1~1 => of_pos p' (String "f" rest)
+       end.
+
+  Fixpoint to_N (s : string) (rest : N)
+    : N
+    := match s with
+       | "" => rest
+       | String ch s'
+         => to_N
+              s'
+              match ascii_to_digit ch with
+              | Some v => N.add v (N.mul 16 rest)
+              | None => N0
+              end
+       end.
+
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+    : to_N (of_pos p rest) base
+      = to_N rest match base with
+                  | N0 => N.pos p
+                  | Npos v => Npos (pos_hex_app v p)
+                  end.
+  Proof.
+    do 4 try destruct p as [p|p|]; destruct base; try reflexivity;
+      cbn; rewrite to_N_of_pos; reflexivity.
+  Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+  := String "0" (String "x" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+  := match n with
+     | N0 => "0x0"
+     | Npos p => of_pos p
+     end.
+Definition of_Z (z : Z) : string
+  := match z with
+     | Zneg p => String "-" (of_pos p)
+     | Z0 => "0x0"
+     | Zpos p => of_pos p
+     end.
+Definition of_nat (n : nat) : string
+  := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+  := match s with
+     | String s0 (String so s)
+       => if ascii_dec s0 "0"
+          then if ascii_dec so "x"
+               then Raw.to_N s N0
+               else N0
+          else N0
+     | _ => N0
+     end.
+Definition to_pos (s : string) : positive
+  := match to_N s with
+     | N0 => 1
+     | Npos p => p
+     end.
+Definition to_Z (s : string) : Z
+  := let '(is_neg, n) := match s with
+                         | String s0 s'
+                           => if ascii_dec s0 "-"
+                              then (true, to_N s')
+                              else (false, to_N s)
+                         | EmptyString => (false, to_N s)
+                         end in
+     match n with
+     | N0 => Z0
+     | Npos p => if is_neg then Zneg p else Zpos p
+     end.
+Definition to_nat (s : string) : nat
+  := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+  : to_N (of_N n)
+    = n.
+Proof.
+  destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma to_Z_of_Z (z : Z)
+  : to_Z (of_Z z)
+    = z.
+Proof.
+  cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+    try reflexivity;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+  : to_nat (of_nat n)
+    = n.
+Proof.
+  cbv [to_nat of_nat];
+    rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+  : to_pos (of_pos p)
+    = p.
+Proof.
+  cbv [of_pos to_pos to_N]; cbn;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0x1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0x2" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0x3" := eq_refl.
+Example of_pos_7 : of_pos 7 = "0x7" := eq_refl.
+Example of_pos_8 : of_pos 8 = "0x8" := eq_refl.
+Example of_pos_9 : of_pos 9 = "0x9" := eq_refl.
+Example of_pos_10 : of_pos 10 = "0xa" := eq_refl.
+Example of_pos_11 : of_pos 11 = "0xb" := eq_refl.
+Example of_pos_12 : of_pos 12 = "0xc" := eq_refl.
+Example of_pos_13 : of_pos 13 = "0xd" := eq_refl.
+Example of_pos_14 : of_pos 14 = "0xe" := eq_refl.
+Example of_pos_15 : of_pos 15 = "0xf" := eq_refl.
+Example of_pos_16 : of_pos 16 = "0x10" := eq_refl.
+Example of_N_0 : of_N 0 = "0x0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0x0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0x1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0x0" := eq_refl.
diff --git a/src/Util/Strings/Octal.v b/src/Util/Strings/Octal.v
deleted file mode 100644
index 43f006008..000000000
--- a/src/Util/Strings/Octal.v
+++ /dev/null
@@ -1,138 +0,0 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String.
-Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Util.Strings.Equality.
-Require Crypto.Util.Pos.
-Import BinPosDef.
-
-Local Open Scope positive_scope.
-Local Open Scope string_scope.
-
-Fixpoint oct_string_of_pos' (p : positive) (rest : string) : string
-  := match p with
-     | 1 => String "1" rest
-     | 2 => String "2" rest
-     | 3 => String "3" rest
-     | 4 => String "4" rest
-     | 5 => String "5" rest
-     | 6 => String "6" rest
-     | 7 => String "7" rest
-     | p'~0~0~0 => oct_string_of_pos' p' (String "0" rest)
-     | p'~0~0~1 => oct_string_of_pos' p' (String "1" rest)
-     | p'~0~1~0 => oct_string_of_pos' p' (String "2" rest)
-     | p'~0~1~1 => oct_string_of_pos' p' (String "3" rest)
-     | p'~1~0~0 => oct_string_of_pos' p' (String "4" rest)
-     | p'~1~0~1 => oct_string_of_pos' p' (String "5" rest)
-     | p'~1~1~0 => oct_string_of_pos' p' (String "6" rest)
-     | p'~1~1~1 => oct_string_of_pos' p' (String "7" rest)
-     end.
-Definition oct_string_of_pos (p : positive) : string
-  := String "0" (String "o" (oct_string_of_pos' p "")).
-
-Local Notation default := 1.
-
-Fixpoint pos_of_oct_string' (s : string) (rest : option positive)
-  : option positive
-  := match s with
-     | "" => rest
-     | String ch s'
-       => pos_of_oct_string'
-            s'
-            (if ascii_beq ch "0"
-             then match rest with
-                  | Some p => Some (p~0~0~0)
-                  | None => None
-                  end
-             else if ascii_beq ch "1"
-             then match rest with
-                  | Some p => Some (p~0~0~1)
-                  | None => Some 1
-                  end
-             else if ascii_beq ch "2"
-             then match rest with
-                  | Some p => Some (p~0~1~0)
-                  | None => Some 2
-                  end
-             else if ascii_beq ch "3"
-             then match rest with
-                  | Some p => Some (p~0~1~1)
-                  | None => Some 3
-                  end
-             else if ascii_beq ch "4"
-             then match rest with
-                  | Some p => Some (p~1~0~0)
-                  | None => Some 4
-                  end
-             else if ascii_beq ch "5"
-             then match rest with
-                  | Some p => Some (p~1~0~1)
-                  | None => Some 5
-                  end
-             else if ascii_beq ch "6"
-             then match rest with
-                  | Some p => Some (p~1~1~0)
-                  | None => Some 6
-                  end
-             else if ascii_beq ch "7"
-             then match rest with
-                  | Some p => Some (p~1~1~1)
-                  | None => Some 7
-                  end
-             else None)
-     end.
-Definition pos_of_oct_string (s : string) : positive
-  := match s with
-     | String s0 (String sb s)
-       => if ascii_beq s0 "0"
-          then if ascii_beq sb "o"
-               then match pos_of_oct_string' s None with
-                    | Some p => p
-                    | None => default
-                    end
-               else default
-          else default
-     | _ => default
-     end.
-
-Fixpoint pos_oct_app (p q:positive) : positive :=
-  match q with
-  | 1 => p~0~0~1
-  | 2 => p~0~1~0
-  | 3 => p~0~1~1
-  | 4 => p~1~0~0
-  | 5 => p~1~0~1
-  | 6 => p~1~1~0
-  | 7 => p~1~1~1
-  | q~0~0~0 => (pos_oct_app p q)~0~0~0
-  | q~0~0~1 => (pos_oct_app p q)~0~0~1
-  | q~0~1~0 => (pos_oct_app p q)~0~1~0
-  | q~0~1~1 => (pos_oct_app p q)~0~1~1
-  | q~1~0~0 => (pos_oct_app p q)~1~0~0
-  | q~1~0~1 => (pos_oct_app p q)~1~0~1
-  | q~1~1~0 => (pos_oct_app p q)~1~1~0
-  | q~1~1~1 => (pos_oct_app p q)~1~1~1
-  end.
-
-Fixpoint pos_of_oct_string_of_pos' (p : positive)
-      (base : option positive)
-      (rest : string)
-  : pos_of_oct_string' (oct_string_of_pos' p rest) base
-    = pos_of_oct_string' rest (match base with
-                               | None => Some p
-                               | Some v => Some (pos_oct_app v p)
-                               end).
-Proof.
-  do 3 try destruct p as [p|p|]; destruct base; try reflexivity;
-    cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
-Qed.
-
-Lemma pos_of_oct_string_of_pos (p : positive)
-  : pos_of_oct_string (oct_string_of_pos p) = p.
-Proof.
-  cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
-Qed.
-
-Example oct_string_of_pos_1 : oct_string_of_pos 1 = "0o1" := eq_refl.
-Example oct_string_of_pos_2 : oct_string_of_pos 2 = "0o2" := eq_refl.
-Example oct_string_of_pos_3 : oct_string_of_pos 3 = "0o3" := eq_refl.
-Example oct_string_of_pos_7 : oct_string_of_pos 7 = "0o7" := eq_refl.
-Example oct_string_of_pos_8 : oct_string_of_pos 8 = "0o10" := eq_refl.
diff --git a/src/Util/Strings/OctalString.v b/src/Util/Strings/OctalString.v
new file mode 100644
index 000000000..e771ad592
--- /dev/null
+++ b/src/Util/Strings/OctalString.v
@@ -0,0 +1,171 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Coq.Numbers.BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Definition ascii_to_digit (ch : ascii) : option N
+  := (if ascii_dec ch "0" then Some 0
+      else if ascii_dec ch "1" then Some 1
+      else if ascii_dec ch "2" then Some 2
+      else if ascii_dec ch "3" then Some 3
+      else if ascii_dec ch "4" then Some 4
+      else if ascii_dec ch "5" then Some 5
+      else if ascii_dec ch "6" then Some 6
+      else if ascii_dec ch "7" then Some 7
+      else None)%N.
+
+Fixpoint pos_oct_app (p q:positive) : positive :=
+  match q with
+  | 1 => p~0~0~1
+  | 2 => p~0~1~0
+  | 3 => p~0~1~1
+  | 4 => p~1~0~0
+  | 5 => p~1~0~1
+  | 6 => p~1~1~0
+  | 7 => p~1~1~1
+  | q~0~0~0 => (pos_oct_app p q)~0~0~0
+  | q~0~0~1 => (pos_oct_app p q)~0~0~1
+  | q~0~1~0 => (pos_oct_app p q)~0~1~0
+  | q~0~1~1 => (pos_oct_app p q)~0~1~1
+  | q~1~0~0 => (pos_oct_app p q)~1~0~0
+  | q~1~0~1 => (pos_oct_app p q)~1~0~1
+  | q~1~1~0 => (pos_oct_app p q)~1~1~0
+  | q~1~1~1 => (pos_oct_app p q)~1~1~1
+  end.
+
+Module Raw.
+  Fixpoint of_pos (p : positive) (rest : string) : string
+    := match p with
+       | 1 => String "1" rest
+       | 2 => String "2" rest
+       | 3 => String "3" rest
+       | 4 => String "4" rest
+       | 5 => String "5" rest
+       | 6 => String "6" rest
+       | 7 => String "7" rest
+       | p'~0~0~0 => of_pos p' (String "0" rest)
+       | p'~0~0~1 => of_pos p' (String "1" rest)
+       | p'~0~1~0 => of_pos p' (String "2" rest)
+       | p'~0~1~1 => of_pos p' (String "3" rest)
+       | p'~1~0~0 => of_pos p' (String "4" rest)
+       | p'~1~0~1 => of_pos p' (String "5" rest)
+       | p'~1~1~0 => of_pos p' (String "6" rest)
+       | p'~1~1~1 => of_pos p' (String "7" rest)
+       end.
+
+  Fixpoint to_N (s : string) (rest : N)
+    : N
+    := match s with
+       | "" => rest
+       | String ch s'
+         => to_N
+              s'
+              match ascii_to_digit ch with
+              | Some v => N.add v (N.mul 8 rest)
+              | None => N0
+              end
+       end.
+
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+    : to_N (of_pos p rest) base
+      = to_N rest match base with
+                  | N0 => N.pos p
+                  | Npos v => Npos (pos_oct_app v p)
+                  end.
+  Proof.
+    do 3 try destruct p as [p|p|]; destruct base; try reflexivity;
+      cbn; rewrite to_N_of_pos; reflexivity.
+  Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+  := String "0" (String "o" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+  := match n with
+     | N0 => "0o0"
+     | Npos p => of_pos p
+     end.
+Definition of_Z (z : Z) : string
+  := match z with
+     | Zneg p => String "-" (of_pos p)
+     | Z0 => "0o0"
+     | Zpos p => of_pos p
+     end.
+Definition of_nat (n : nat) : string
+  := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+  := match s with
+     | String s0 (String so s)
+       => if ascii_dec s0 "0"
+          then if ascii_dec so "o"
+               then Raw.to_N s N0
+               else N0
+          else N0
+     | _ => N0
+     end.
+Definition to_pos (s : string) : positive
+  := match to_N s with
+     | N0 => 1
+     | Npos p => p
+     end.
+Definition to_Z (s : string) : Z
+  := let '(is_neg, n) := match s with
+                         | String s0 s'
+                           => if ascii_dec s0 "-"
+                              then (true, to_N s')
+                              else (false, to_N s)
+                         | EmptyString => (false, to_N s)
+                         end in
+     match n with
+     | N0 => Z0
+     | Npos p => if is_neg then Zneg p else Zpos p
+     end.
+Definition to_nat (s : string) : nat
+  := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+  : to_N (of_N n)
+    = n.
+Proof.
+  destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma to_Z_of_Z (z : Z)
+  : to_Z (of_Z z)
+    = z.
+Proof.
+  cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+    try reflexivity;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+  : to_nat (of_nat n)
+    = n.
+Proof.
+  cbv [to_nat of_nat];
+    rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+  : to_pos (of_pos p)
+    = p.
+Proof.
+  cbv [of_pos to_pos to_N]; cbn;
+    rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0o1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0o2" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0o3" := eq_refl.
+Example of_pos_7 : of_pos 7 = "0o7" := eq_refl.
+Example of_pos_8 : of_pos 8 = "0o10" := eq_refl.
+Example of_N_0 : of_N 0 = "0o0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0o0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0o1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0o0" := eq_refl.