Skip to main content

🍃 S.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.RPC_arg.

Module MINIMAL_HASH.
  Definition to_Compare_S {t} (H : S.MINIMAL_HASH (t := t))
    : Compare.S (t := t) := {|
      Compare.S.op_eq := H.(S.MINIMAL_HASH.op_eq);
      Compare.S.op_ltgt := H.(S.MINIMAL_HASH.op_ltgt);
      Compare.S.op_lt := H.(S.MINIMAL_HASH.op_lt);
      Compare.S.op_lteq := H.(S.MINIMAL_HASH.op_lteq);
      Compare.S.op_gteq := H.(S.MINIMAL_HASH.op_gteq);
      Compare.S.op_gt := H.(S.MINIMAL_HASH.op_gt);
      Compare.S.compare := H.(S.MINIMAL_HASH.compare);
      Compare.S.equal := H.(S.MINIMAL_HASH.equal);
      Compare.S.max := H.(S.MINIMAL_HASH.max);
      Compare.S.min := H.(S.MINIMAL_HASH.min);
    |}.

    Module Valid.
      Record t {t} {H : S.MINIMAL_HASH (t := t)} : Prop := {
        Compare_S : Compare.S.Valid.t (to_Compare_S H);
      }.
      Arguments t {_}.
    End Valid.
End MINIMAL_HASH.

Module RAW_DATA.
  Module Valid.
    Record t {t} {R : S.RAW_DATA (t := t)} : Prop := {
      of_bytes_opt_to_bytes v :
        R.(S.RAW_DATA.of_bytes_opt) (R.(S.RAW_DATA.to_bytes) v) =
        Some v;
      to_bytes_of_bytes_opt bytes :
        match R.(S.RAW_DATA.of_bytes_opt) bytes with
        | Some vR.(S.RAW_DATA.to_bytes) v = bytes
        | NoneTrue
        end;
    }.
    Arguments t {_}.
  End Valid.
End RAW_DATA.

Module B58_DATA.
  Module Valid.
    Record t {t} (B : S.B58_DATA (t := t)) : Prop := {
      of_to_b58_check value :
        B.(S.B58_DATA.of_b58check_opt) (B.(S.B58_DATA.to_b58check) value) =
        Some value;
      to_of_b58_check string :
        match B.(S.B58_DATA.of_b58check_opt) string with
        | Some valueB.(S.B58_DATA.to_b58check) value = string
        | NoneTrue
        end;
    }.
  End Valid.
End B58_DATA.

Module ENCODER.
  Module Valid.
    Record t {t : Set} {domain} {E : S.ENCODER (t := t)} : Prop := {
      encoding : Data_encoding.Valid.t (fun _True) E.(S.ENCODER.encoding);
      rpc_arg : RPC_arg.Valid.t domain E.(S.ENCODER.rpc_arg);
    }.
    Arguments t {_}.
  End Valid.
End ENCODER.

Module HASH.
  Definition to_MINIMAL_HASH {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.MINIMAL_HASH (t := t) := {|
      S.MINIMAL_HASH.name := H.(S.HASH.name);
      S.MINIMAL_HASH.title := H.(S.HASH.title);
      S.MINIMAL_HASH.pp := H.(S.HASH.pp);
      S.MINIMAL_HASH.pp_short := H.(S.HASH.pp_short);
      S.MINIMAL_HASH.op_eq := H.(S.HASH.op_eq);
      S.MINIMAL_HASH.op_ltgt := H.(S.HASH.op_ltgt);
      S.MINIMAL_HASH.op_lt := H.(S.HASH.op_lt);
      S.MINIMAL_HASH.op_lteq := H.(S.HASH.op_lteq);
      S.MINIMAL_HASH.op_gteq := H.(S.HASH.op_gteq);
      S.MINIMAL_HASH.op_gt := H.(S.HASH.op_gt);
      S.MINIMAL_HASH.compare := H.(S.HASH.compare);
      S.MINIMAL_HASH.equal := H.(S.HASH.equal);
      S.MINIMAL_HASH.max := H.(S.HASH.max);
      S.MINIMAL_HASH.min := H.(S.HASH.min);
      S.MINIMAL_HASH.hash_bytes := H.(S.HASH.hash_bytes);
      S.MINIMAL_HASH.hash_string := H.(S.HASH.hash_string);
      S.MINIMAL_HASH.zero := H.(S.HASH.zero);
    |}.

  Definition to_RAW_DATA {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.RAW_DATA (t := t) := {|
      S.RAW_DATA.size_value := H.(S.HASH.size_value);
      S.RAW_DATA.to_bytes := H.(S.HASH.to_bytes);
      S.RAW_DATA.of_bytes_opt := H.(S.HASH.of_bytes_opt);
      S.RAW_DATA.of_bytes_exn := H.(S.HASH.of_bytes_exn);
    |}.

  Definition to_B58_DATA {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.B58_DATA (t := t) := {|
      S.B58_DATA.to_b58check := H.(HASH.to_b58check);
      S.B58_DATA.to_short_b58check := H.(HASH.to_short_b58check);
      S.B58_DATA.of_b58check_exn := H.(HASH.of_b58check_exn);
      S.B58_DATA.of_b58check_opt := H.(HASH.of_b58check_opt);
      S.B58_DATA.b58check_encoding := H.(HASH.b58check_encoding);
    |}.

  Definition to_ENCODER {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.ENCODER (t := t) := {|
      S.ENCODER.encoding := H.(S.HASH.encoding);
      S.ENCODER.rpc_arg := H.(S.HASH.rpc_arg);
    |}.

  Definition to_INDEXES {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.INDEXES (t := t) := {|
      S.INDEXES._Set := H.(S.HASH._Set);
      S.INDEXES.Map := H.(S.HASH.Map);
    |}.

  Module Valid.
    Record t {t Set_t Map_t} {domain}
      {H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} : Prop := {
      MINIMAL_HASH : MINIMAL_HASH.Valid.t (to_MINIMAL_HASH H);
      RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA H);
      B58_DATA : B58_DATA.Valid.t (to_B58_DATA H);
      ENCODER : ENCODER.Valid.t domain (to_ENCODER H);
    }.
    Arguments t {_ _ _}.
  End Valid.
End HASH.

Module MERKLE_TREE.
  Definition to_HASH {elt t Set_t Map_t path}
    (M : S.MERKLE_TREE
      (elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path))
    : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t) := {|
      S.HASH.name := M.(S.MERKLE_TREE.name);
      S.HASH.title := M.(S.MERKLE_TREE.title);
      S.HASH.pp := M.(S.MERKLE_TREE.pp);
      S.HASH.pp_short := M.(S.MERKLE_TREE.pp_short);
      S.HASH.op_eq := M.(S.MERKLE_TREE.op_eq);
      S.HASH.op_ltgt := M.(S.MERKLE_TREE.op_ltgt);
      S.HASH.op_lt := M.(S.MERKLE_TREE.op_lt);
      S.HASH.op_lteq := M.(S.MERKLE_TREE.op_lteq);
      S.HASH.op_gteq := M.(S.MERKLE_TREE.op_gteq);
      S.HASH.op_gt := M.(S.MERKLE_TREE.op_gt);
      S.HASH.compare := M.(S.MERKLE_TREE.compare);
      S.HASH.equal := M.(S.MERKLE_TREE.equal);
      S.HASH.max := M.(S.MERKLE_TREE.max);
      S.HASH.min := M.(S.MERKLE_TREE.min);
      S.HASH.hash_bytes := M.(S.MERKLE_TREE.hash_bytes);
      S.HASH.hash_string := M.(S.MERKLE_TREE.hash_string);
      S.HASH.zero := M.(S.MERKLE_TREE.zero);
      S.HASH.size_value := M.(S.MERKLE_TREE.size_value);
      S.HASH.to_bytes := M.(S.MERKLE_TREE.to_bytes);
      S.HASH.of_bytes_opt := M.(S.MERKLE_TREE.of_bytes_opt);
      S.HASH.of_bytes_exn := M.(S.MERKLE_TREE.of_bytes_exn);
      S.HASH.to_b58check := M.(S.MERKLE_TREE.to_b58check);
      S.HASH.to_short_b58check := M.(S.MERKLE_TREE.to_short_b58check);
      S.HASH.of_b58check_exn := M.(S.MERKLE_TREE.of_b58check_exn);
      S.HASH.of_b58check_opt := M.(S.MERKLE_TREE.of_b58check_opt);
      S.HASH.b58check_encoding := M.(S.MERKLE_TREE.b58check_encoding);
      S.HASH.encoding := M.(S.MERKLE_TREE.encoding);
      S.HASH.rpc_arg := M.(S.MERKLE_TREE.rpc_arg);
      S.HASH._Set := M.(S.MERKLE_TREE._Set);
      S.HASH.Map := M.(S.MERKLE_TREE.Map);
    |}.

  Module Valid.
    Record t {elt t Set_t Map_t path} {domain}
      {M : S.MERKLE_TREE
        (elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path)}
      : Prop := {
      HASH : HASH.Valid.t domain (to_HASH M);
      path_encoding :
        Data_encoding.Valid.t (fun _True) M.(S.MERKLE_TREE.path_encoding);
    }.
    Arguments t {_ _ _ _ _}.
  End Valid.
End MERKLE_TREE.

Module SIGNATURE_PUBLIC_KEY_HASH.
  Definition to_Compare_S {t Set_t Map_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    Compare.S (t := t) := {|
      Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq);
      Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_ltgt);
      Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lt);
      Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lteq);
      Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gteq);
      Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gt);
      Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY_HASH.compare);
      Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY_HASH.equal);
      Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY_HASH.max);
      Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY_HASH.min);
    |}.

  Definition to_RAW_DATA {t Set_t Map_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    S.RAW_DATA (t := t) := {|
      S.RAW_DATA.size_value := S.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value);
      S.RAW_DATA.to_bytes := S.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
      S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt);
      S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_exn);
    |}.

  Definition to_B58_DATA {t Set_t Map_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    S.B58_DATA (t := t) := {|
      S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_b58check);
      S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_short_b58check);
      S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_exn);
      S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt);
      S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY_HASH.b58check_encoding);
    |}.

  Definition to_ENCODER {t Set_t Map_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    S.ENCODER (t := t) := {|
      S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding);
      S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg);
    |}.

  Definition to_INDEXES {t Set_t Map_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    S.INDEXES (t := t) := {|
      S.INDEXES._Set := S.(S.SIGNATURE_PUBLIC_KEY_HASH._Set);
      S.INDEXES.Map := S.(S.SIGNATURE_PUBLIC_KEY_HASH.Map);
    |}.

  Module Valid.
    Record t {t Set_t Map_t} {domain}
      {S :
        S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} :
      Prop := {
      Compare_S : Compare.S.Valid.t (to_Compare_S S);
      RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
      B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
      ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
    }.
    Arguments t {_ _ _}.
  End Valid.
End SIGNATURE_PUBLIC_KEY_HASH.

Module SIGNATURE_PUBLIC_KEY.
  Definition to_Compare_S {t public_key_hash_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
    Compare.S (t := t) := {|
      Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY.op_eq);
      Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY.op_ltgt);
      Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY.op_lt);
      Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY.op_lteq);
      Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY.op_gteq);
      Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY.op_gt);
      Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY.compare);
      Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY.equal);
      Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY.max);
      Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY.min);
    |}.

  Definition to_B58_DATA {t public_key_hash_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
    S.B58_DATA (t := t) := {|
      S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY.to_b58check);
      S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY.to_short_b58check);
      S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY.of_b58check_exn);
      S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY.of_b58check_opt);
      S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY.b58check_encoding);
    |}.

  Definition to_ENCODER {t public_key_hash_t}
    (S :
      S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
    S.ENCODER (t := t) := {|
      S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY.encoding);
      S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY.rpc_arg);
    |}.

  Module Valid.
    Record t {t public_key_hash_t} {domain}
      {S :
        S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)} :
      Prop := {
      Compare_S : Compare.S.Valid.t (to_Compare_S S);
      B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
      ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
    }.
    Arguments t {_ _}.
  End Valid.
End SIGNATURE_PUBLIC_KEY.

Module SIGNATURE.
  Definition to_RAW_DATA {pkh pkh_set pkh_map pk t watermark}
    (S : S.SIGNATURE
      (Public_key_hash_t := pkh)
      (Public_key_hash_Set_t := pkh_set)
      (Public_key_hash_Map_t := pkh_map)
      (Public_key_t := pk)
      (t := t)
      (watermark := watermark)
    ) :
    S.RAW_DATA (t := t) := {|
      S.RAW_DATA.size_value := S.(S.SIGNATURE.size_value);
      S.RAW_DATA.to_bytes := S.(S.SIGNATURE.to_bytes);
      S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE.of_bytes_opt);
      S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE.of_bytes_exn);
    |}.

  Definition to_Compare_S {pkh pkh_set pkh_map pk t watermark}
    (S : S.SIGNATURE
      (Public_key_hash_t := pkh)
      (Public_key_hash_Set_t := pkh_set)
      (Public_key_hash_Map_t := pkh_map)
      (Public_key_t := pk)
      (t := t)
      (watermark := watermark)
    ) :
    Compare.S (t := t) := {|
      Compare.S.op_eq := S.(S.SIGNATURE.op_eq);
      Compare.S.op_ltgt := S.(S.SIGNATURE.op_ltgt);
      Compare.S.op_lt := S.(S.SIGNATURE.op_lt);
      Compare.S.op_lteq := S.(S.SIGNATURE.op_lteq);
      Compare.S.op_gteq := S.(S.SIGNATURE.op_gteq);
      Compare.S.op_gt := S.(S.SIGNATURE.op_gt);
      Compare.S.compare := S.(S.SIGNATURE.compare);
      Compare.S.equal := S.(S.SIGNATURE.equal);
      Compare.S.max := S.(S.SIGNATURE.max);
      Compare.S.min := S.(S.SIGNATURE.min);
    |}.

  Definition to_B58_DATA {pkh pkh_set pkh_map pk t watermark}
    (S : S.SIGNATURE
      (Public_key_hash_t := pkh)
      (Public_key_hash_Set_t := pkh_set)
      (Public_key_hash_Map_t := pkh_map)
      (Public_key_t := pk)
      (t := t)
      (watermark := watermark)
    ) :
    S.B58_DATA (t := t) := {|
      S.B58_DATA.to_b58check := S.(SIGNATURE.to_b58check);
      S.B58_DATA.to_short_b58check := S.(SIGNATURE.to_short_b58check);
      S.B58_DATA.of_b58check_exn := S.(SIGNATURE.of_b58check_exn);
      S.B58_DATA.of_b58check_opt := S.(SIGNATURE.of_b58check_opt);
      S.B58_DATA.b58check_encoding := S.(SIGNATURE.b58check_encoding);
    |}.

  Definition to_ENCODER {pkh pkh_set pkh_map pk t watermark}
    (S : S.SIGNATURE
      (Public_key_hash_t := pkh)
      (Public_key_hash_Set_t := pkh_set)
      (Public_key_hash_Map_t := pkh_map)
      (Public_key_t := pk)
      (t := t)
      (watermark := watermark)
    ) :
    S.ENCODER (t := t) := {|
      S.ENCODER.encoding := S.(S.SIGNATURE.encoding);
      S.ENCODER.rpc_arg := S.(S.SIGNATURE.rpc_arg);
    |}.

  Module Valid.
    Record t {pkh pkh_set pkh_map pk t watermark} {domain}
      {S : S.SIGNATURE
        (Public_key_hash_t := pkh)
        (Public_key_hash_Set_t := pkh_set)
        (Public_key_hash_Map_t := pkh_map)
        (Public_key_t := pk)
        (t := t)
        (watermark := watermark)
       } :
      Prop := {
      Public_key_hash :
        SIGNATURE_PUBLIC_KEY_HASH.Valid.t (fun _True)
          S.(S.SIGNATURE.Public_key_hash);
      Public_key :
        SIGNATURE_PUBLIC_KEY.Valid.t (fun _True)
          S.(S.SIGNATURE.Public_key);
      RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
      Compare_S : Compare.S.Valid.t (to_Compare_S S);
      B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
      ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
    }.
    Arguments t {_ _ _ _ _ _}.
  End Valid.
End SIGNATURE.