1 files changed, 72 insertions, 0 deletions
diff --git a/src/Util/Strings/Binary.v b/src/Util/Strings/Binary.v
new file mode 100644
index 000000000..955c6c8f6
--- /dev/null
+++ b/src/Util/Strings/Binary.v
@@ -0,0 +1,72 @@
+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.