Skip to main content

🍃 Base58.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

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 valuesimple_encode encoding value = string
      | NoneTrue
      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 valueto_raw value = string
      | NoneTrue
      end)
    t (a := a) (register_encoding prefix length to_raw of_raw wrap).
End Valid.