✒️ Contract_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Inductive t : Set :=
| Implicit : Signature.public_key_hash → t
| Originated : Contract_hash.t → t.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (l1 : t) (l2 : t) : int :=
match (l1, l2) with
| (Implicit pkh1, Implicit pkh2) ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkh1
pkh2
| (Originated h1, Originated h2) ⇒ Contract_hash.compare h1 h2
| (Implicit _, Originated _) ⇒ (-1)
| (Originated _, Implicit _) ⇒ 1
end in
{|
Compare.COMPARABLE.compare := compare
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Inductive t : Set :=
| Implicit : Signature.public_key_hash → t
| Originated : Contract_hash.t → t.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (l1 : t) (l2 : t) : int :=
match (l1, l2) with
| (Implicit pkh1, Implicit pkh2) ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkh1
pkh2
| (Originated h1, Originated h2) ⇒ Contract_hash.compare h1 h2
| (Implicit _, Originated _) ⇒ (-1)
| (Originated _, Implicit _) ⇒ 1
end in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
match function_parameter with
| Implicit _ ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
Cache_memory_helpers.public_key_hash_in_memory_size
| Originated _ ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
Cache_memory_helpers.blake2b_hash_size
end.
Definition to_b58check (function_parameter : t) : string :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) pbk
| Originated h_value ⇒ Contract_hash.to_b58check h_value
end.
Definition implicit_of_b58data (function_parameter : Base58.data)
: option Signature.public_key_hash :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value :=
cast Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload in
Some (Signature.Ed25519Hash h_value)
else if String.eqb tag "Data" then
let h_value :=
cast Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload
in
Some (Signature.Secp256k1Hash h_value)
else if String.eqb tag "Data" then
let h_value :=
cast P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload in
Some (Signature.P256Hash h_value)
else None
end.
Definition originated_of_b58data (function_parameter : Base58.data)
: option Contract_hash.t :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast Contract_hash.t payload in
Some h_value
else None
end.
Definition contract_of_b58data (data : Base58.data) : option t :=
match implicit_of_b58data data with
| Some pkh ⇒ Some (Implicit pkh)
| None ⇒
match originated_of_b58data data with
| Some contract_hash ⇒ Some (Originated contract_hash)
| None ⇒ None
end
end.
Definition of_b58check_gen {A : Set}
(of_b58data : Base58.data → option A) (s_value : string) : M? A :=
match Base58.decode s_value with
| Some data ⇒
match of_b58data data with
| Some c_value ⇒ return? c_value
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_contract_notation" string s_value)
end
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_contract_notation" string s_value)
end.
Definition of_b58check : string → M? t := of_b58check_gen contract_of_b58data.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ppf pbk
| Originated h_value ⇒ Contract_hash.pp ppf h_value
end.
Definition pp_short (ppf : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short) ppf pbk
| Originated h_value ⇒ Contract_hash.pp_short ppf h_value
end.
Definition implicit_case {A : Set}
(proj : A → option Signature.public_key_hash)
(inj : Signature.public_key_hash → A) : Data_encoding.case A :=
Data_encoding.case_value "Implicit" None (Data_encoding.Tag 0)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) proj inj.
Definition originated_case {A : Set}
(proj : A → option Contract_hash.t) (inj : Contract_hash.t → A)
: Data_encoding.case A :=
Data_encoding.case_value "Originated" None (Data_encoding.Tag 1)
(Data_encoding.Fixed.add_padding Contract_hash.encoding 1) proj inj.
Definition cases {A : Set} (is_contract : A → option t) (to_contract : t → A)
: list (Data_encoding.case A) :=
[
implicit_case
(fun (k_value : A) ⇒
match is_contract k_value with
| Some (Implicit k_value) ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Signature.public_key_hash) ⇒
to_contract (Implicit k_value));
originated_case
(fun (k_value : A) ⇒
match is_contract k_value with
| Some (Originated k_value) ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Contract_hash.t) ⇒ to_contract (Originated k_value))
].
Definition encoding_gen {A B C : Set}
(id_extra : string) (title_extra : string) (can_be : string)
(cases : (A → option A) → (B → B) → list (Data_encoding.case C))
(to_b58check : C → string) (of_b58data : Base58.data → option C)
: Data_encoding.encoding C :=
Data_encoding.def (Pervasives.op_caret "contract_id" id_extra)
(Some (Pervasives.op_caret "A contract handle" title_extra))
(Some
(Pervasives.op_caret
"A contract notation as given to an RPC or inside scripts. Can be a base58 "
can_be))
(Data_encoding.splitted
(Data_encoding.conv to_b58check
(fun (s_value : string) ⇒
match of_b58check_gen of_b58data s_value with
| Pervasives.Ok s_value ⇒ s_value
| Pervasives.Error _ ⇒
Data_encoding.Json.cannot_destruct
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid contract notation."
CamlinternalFormatBasics.End_of_format)
"Invalid contract notation.")
end) None Data_encoding.string_value)
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
(cases (fun (x_value : A) ⇒ Some x_value)
(fun (x_value : B) ⇒ x_value)))).
Definition encoding : Data_encoding.encoding t :=
encoding_gen "" ""
"implicit contract hash or a base58 originated contract hash." cases
to_b58check contract_of_b58data.
Definition implicit_encoding
: Data_encoding.encoding Signature.public_key_hash :=
encoding_gen ".implicit" " -- implicit account" "implicit contract hash."
(fun (proj : Signature.public_key_hash → option Signature.public_key_hash)
⇒
fun (inj : Signature.public_key_hash → Signature.public_key_hash) ⇒
[ implicit_case proj inj ])
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
implicit_of_b58data.
Definition originated_encoding : Data_encoding.encoding Contract_hash.t :=
encoding_gen ".originated" " -- originated account"
"originated contract hash."
(fun (proj : Contract_hash.t → option Contract_hash.t) ⇒
fun (inj : Contract_hash.t → Contract_hash.t) ⇒
[ originated_case proj inj ]) Contract_hash.to_b58check
originated_of_b58data.
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
match function_parameter with
| Implicit _ ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
Cache_memory_helpers.public_key_hash_in_memory_size
| Originated _ ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
Cache_memory_helpers.blake2b_hash_size
end.
Definition to_b58check (function_parameter : t) : string :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) pbk
| Originated h_value ⇒ Contract_hash.to_b58check h_value
end.
Definition implicit_of_b58data (function_parameter : Base58.data)
: option Signature.public_key_hash :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value :=
cast Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload in
Some (Signature.Ed25519Hash h_value)
else if String.eqb tag "Data" then
let h_value :=
cast Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload
in
Some (Signature.Secp256k1Hash h_value)
else if String.eqb tag "Data" then
let h_value :=
cast P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload in
Some (Signature.P256Hash h_value)
else None
end.
Definition originated_of_b58data (function_parameter : Base58.data)
: option Contract_hash.t :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast Contract_hash.t payload in
Some h_value
else None
end.
Definition contract_of_b58data (data : Base58.data) : option t :=
match implicit_of_b58data data with
| Some pkh ⇒ Some (Implicit pkh)
| None ⇒
match originated_of_b58data data with
| Some contract_hash ⇒ Some (Originated contract_hash)
| None ⇒ None
end
end.
Definition of_b58check_gen {A : Set}
(of_b58data : Base58.data → option A) (s_value : string) : M? A :=
match Base58.decode s_value with
| Some data ⇒
match of_b58data data with
| Some c_value ⇒ return? c_value
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_contract_notation" string s_value)
end
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_contract_notation" string s_value)
end.
Definition of_b58check : string → M? t := of_b58check_gen contract_of_b58data.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ppf pbk
| Originated h_value ⇒ Contract_hash.pp ppf h_value
end.
Definition pp_short (ppf : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Implicit pbk ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short) ppf pbk
| Originated h_value ⇒ Contract_hash.pp_short ppf h_value
end.
Definition implicit_case {A : Set}
(proj : A → option Signature.public_key_hash)
(inj : Signature.public_key_hash → A) : Data_encoding.case A :=
Data_encoding.case_value "Implicit" None (Data_encoding.Tag 0)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) proj inj.
Definition originated_case {A : Set}
(proj : A → option Contract_hash.t) (inj : Contract_hash.t → A)
: Data_encoding.case A :=
Data_encoding.case_value "Originated" None (Data_encoding.Tag 1)
(Data_encoding.Fixed.add_padding Contract_hash.encoding 1) proj inj.
Definition cases {A : Set} (is_contract : A → option t) (to_contract : t → A)
: list (Data_encoding.case A) :=
[
implicit_case
(fun (k_value : A) ⇒
match is_contract k_value with
| Some (Implicit k_value) ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Signature.public_key_hash) ⇒
to_contract (Implicit k_value));
originated_case
(fun (k_value : A) ⇒
match is_contract k_value with
| Some (Originated k_value) ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Contract_hash.t) ⇒ to_contract (Originated k_value))
].
Definition encoding_gen {A B C : Set}
(id_extra : string) (title_extra : string) (can_be : string)
(cases : (A → option A) → (B → B) → list (Data_encoding.case C))
(to_b58check : C → string) (of_b58data : Base58.data → option C)
: Data_encoding.encoding C :=
Data_encoding.def (Pervasives.op_caret "contract_id" id_extra)
(Some (Pervasives.op_caret "A contract handle" title_extra))
(Some
(Pervasives.op_caret
"A contract notation as given to an RPC or inside scripts. Can be a base58 "
can_be))
(Data_encoding.splitted
(Data_encoding.conv to_b58check
(fun (s_value : string) ⇒
match of_b58check_gen of_b58data s_value with
| Pervasives.Ok s_value ⇒ s_value
| Pervasives.Error _ ⇒
Data_encoding.Json.cannot_destruct
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid contract notation."
CamlinternalFormatBasics.End_of_format)
"Invalid contract notation.")
end) None Data_encoding.string_value)
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
(cases (fun (x_value : A) ⇒ Some x_value)
(fun (x_value : B) ⇒ x_value)))).
Definition encoding : Data_encoding.encoding t :=
encoding_gen "" ""
"implicit contract hash or a base58 originated contract hash." cases
to_b58check contract_of_b58data.
Definition implicit_encoding
: Data_encoding.encoding Signature.public_key_hash :=
encoding_gen ".implicit" " -- implicit account" "implicit contract hash."
(fun (proj : Signature.public_key_hash → option Signature.public_key_hash)
⇒
fun (inj : Signature.public_key_hash → Signature.public_key_hash) ⇒
[ implicit_case proj inj ])
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
implicit_of_b58data.
Definition originated_encoding : Data_encoding.encoding Contract_hash.t :=
encoding_gen ".originated" " -- originated account"
"originated contract hash."
(fun (proj : Contract_hash.t → option Contract_hash.t) ⇒
fun (inj : Contract_hash.t → Contract_hash.t) ⇒
[ originated_case proj inj ]) Contract_hash.to_b58check
originated_of_b58data.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"contract.invalid_contract_notation" "Invalid contract notation"
"A malformed contract notation was given to an RPC or in a script."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid contract notation "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid contract notation %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "notation" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_contract_notation" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_contract_notation" string loc_value).
Definition originated_contract (nonce_value : Origination_nonce.t) : t :=
Originated (Contract_hash.of_nonce nonce_value).
#[bypass_check(guard)]
Definition originated_contracts (function_parameter : Origination_nonce.t)
: Origination_nonce.t → M? (list Contract_hash.t) :=
let '{|
Origination_nonce.t.operation_hash := first_hash;
Origination_nonce.t.origination_index := first
|} := function_parameter in
fun (function_parameter : Origination_nonce.t) ⇒
let
'{|
Origination_nonce.t.operation_hash := last_hash;
Origination_nonce.t.origination_index := last
|} as origination_nonce := function_parameter in
let? '_ :=
Internal_errors.do_assert (Operation_hash.equal first_hash last_hash) in
let fix contracts
(acc_value : list Contract_hash.t) (origination_index : int32)
{struct origination_index} : list Contract_hash.t :=
if origination_index <i32 first then
acc_value
else
let origination_nonce :=
Origination_nonce.t.with_origination_index origination_index
origination_nonce in
let acc_value :=
cons (Contract_hash.of_nonce origination_nonce) acc_value in
contracts acc_value (Int32.pred origination_index) in
return? (contracts nil (Int32.pred last)).
Definition rpc_arg : RPC_arg.arg t :=
let construct := to_b58check in
let destruct (hash_value : string) : Pervasives.result t string :=
Result.map_error
(fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
let '_ := function_parameter in
"Cannot parse contract id") (of_b58check hash_value) in
RPC_arg.make (Some "A contract identifier encoded in b58check.") "contract_id"
destruct construct tt.
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : t) (l_value : list string) : list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string) : M? (option t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg t := rpc_arg.
Definition encoding : Data_encoding.encoding t := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Definition of_b58data : Base58.data → option t := contract_of_b58data.
Error_monad.register_error_kind Error_monad.Permanent
"contract.invalid_contract_notation" "Invalid contract notation"
"A malformed contract notation was given to an RPC or in a script."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid contract notation "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid contract notation %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "notation" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_contract_notation" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_contract_notation" string loc_value).
Definition originated_contract (nonce_value : Origination_nonce.t) : t :=
Originated (Contract_hash.of_nonce nonce_value).
#[bypass_check(guard)]
Definition originated_contracts (function_parameter : Origination_nonce.t)
: Origination_nonce.t → M? (list Contract_hash.t) :=
let '{|
Origination_nonce.t.operation_hash := first_hash;
Origination_nonce.t.origination_index := first
|} := function_parameter in
fun (function_parameter : Origination_nonce.t) ⇒
let
'{|
Origination_nonce.t.operation_hash := last_hash;
Origination_nonce.t.origination_index := last
|} as origination_nonce := function_parameter in
let? '_ :=
Internal_errors.do_assert (Operation_hash.equal first_hash last_hash) in
let fix contracts
(acc_value : list Contract_hash.t) (origination_index : int32)
{struct origination_index} : list Contract_hash.t :=
if origination_index <i32 first then
acc_value
else
let origination_nonce :=
Origination_nonce.t.with_origination_index origination_index
origination_nonce in
let acc_value :=
cons (Contract_hash.of_nonce origination_nonce) acc_value in
contracts acc_value (Int32.pred origination_index) in
return? (contracts nil (Int32.pred last)).
Definition rpc_arg : RPC_arg.arg t :=
let construct := to_b58check in
let destruct (hash_value : string) : Pervasives.result t string :=
Result.map_error
(fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
let '_ := function_parameter in
"Cannot parse contract id") (of_b58check hash_value) in
RPC_arg.make (Some "A contract identifier encoded in b58check.") "contract_id"
destruct construct tt.
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : t) (l_value : list string) : list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string) : M? (option t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg t := rpc_arg.
Definition encoding : Data_encoding.encoding t := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Definition of_b58data : Base58.data → option t := contract_of_b58data.