🍃 Base58.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Module Valid.
  Record t {a} {encoding : Base58.encoding a} : Prop := {
    simple_decode_encode value :
      simple_decode encoding (simple_encode encoding value) = Some value;
    simepl_encode_decode string :
      match simple_decode encoding string with
      | Some value ⇒ simple_encode encoding value = string
      | None ⇒ True
      end
  }.
  Arguments t {_}.

  Axiom register_encoding : ∀ {a : Set} {prefix length to_raw of_raw wrap},
    (∀ value, of_raw (to_raw value) = Some value) →
    (∀ string,
      match of_raw string with
      | Some value ⇒ to_raw value = string
      | None ⇒ True
      end) →
    t (a := a) (register_encoding prefix length to_raw of_raw wrap).
End Valid.