Skip to main content

🐾 Path_encoding.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.

Require TezosOfOCaml.Environment.V8.Proofs.Hex.

Module S.
  Module Valid.
    Record t {t : Set} {P : Path_encoding.S (t := t)} : Prop := {
      to_path_postfix v postfix :
        P.(Path_encoding.S.to_path) v postfix =
        List.app (P.(Path_encoding.S.to_path) v []) postfix;
      of_path_to_path v :
        P.(Path_encoding.S.of_path) (P.(Path_encoding.S.to_path) v []) =
        return? Some v;
      to_path_of_path path :
        letP? p := P.(Path_encoding.S.of_path) path in
        match p with
        | Some vP.(Path_encoding.S.to_path) v [] = path
        | NoneTrue
        end;
      to_path_path_length v :
        letP? path_length := P.(Path_encoding.S.path_length) in
        List.length (P.(Path_encoding.S.to_path) v []) = path_length;
    }.
    Arguments t {_}.
  End Valid.
End S.

Module ENCODING.
  Module Valid.
    Record t {t : Set} {E : Path_encoding.ENCODING (t := t)} : Prop := {
      of_bytes_opt_to_bytes v :
        E.(Path_encoding.ENCODING.of_bytes_opt)
          (E.(Path_encoding.ENCODING.to_bytes) v) =
        Some v;
      to_bytes_of_bytes_opt bytes :
        match E.(Path_encoding.ENCODING.of_bytes_opt) bytes with
        | Some vE.(Path_encoding.ENCODING.to_bytes) v = bytes
        | NoneTrue
        end;
    }.
    Arguments t {_}.
  End Valid.
End ENCODING.

Lemma Make_hex_is_valid : {t : Set}
  (E : Path_encoding.ENCODING (t := t)),
  Path_encoding.ENCODING.Valid.t E
  Path_encoding.S.Valid.t (Path_encoding.Make_hex E).
Proof.
  intros t E H; constructor; intros; cbv - [List.app List.length].
  { now destruct (Hex.of_bytes _ _). }
  { destruct (Hex.of_bytes _ _) eqn:H_eq.
    rewrite <- H_eq.
    rewrite Hex.to_bytes_of_bytes.
    now rewrite H.(Path_encoding.ENCODING.Valid.of_bytes_opt_to_bytes).
  }
  { destruct path as [|bytes[]]; trivial.
    assert (H_hex := Hex.of_bytes_to_bytes (Hex.Hex bytes)).
    destruct (Hex.to_bytes _) as [bytes'|]; trivial.
    assert (H_bytes :=
      H.(Path_encoding.ENCODING.Valid.to_bytes_of_bytes_opt) bytes'
    ).
    destruct (E.(Path_encoding.ENCODING.of_bytes_opt) _); trivial.
    cbv in ×.
    now rewrite H_bytes; rewrite H_hex.
  }
  { now destruct (Hex.of_bytes _ _). }
Qed.