🦏 Sc_rollup_inbox_message_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.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let msg := "Failed to encode a rollup management protocol inbox message value"
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.error_encoding_inbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_encode_inbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_encode_inbox_message" unit tt) in
let msg := "Failed to decode a rollup management protocol inbox message value"
in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.error_decoding_inbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_decode_inbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_decode_inbox_message" unit tt).
let msg := "Failed to encode a rollup management protocol inbox message value"
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.error_encoding_inbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_encode_inbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_encode_inbox_message" unit tt) in
let msg := "Failed to decode a rollup management protocol inbox message value"
in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.error_decoding_inbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_decode_inbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_decode_inbox_message" unit tt).
Records for the constructor parameters
Module ConstructorRecords_internal_inbox_message.
Module internal_inbox_message.
Module Transfer.
Record record {payload sender source destination : Set} : Set := Build {
payload : payload;
sender : sender;
source : source;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_payload {t_payload t_sender t_source t_destination}
payload (r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination payload r.(sender)
r.(source) r.(destination).
Definition with_sender {t_payload t_sender t_source t_destination} sender
(r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) sender
r.(source) r.(destination).
Definition with_source {t_payload t_sender t_source t_destination} source
(r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) r.(sender)
source r.(destination).
Definition with_destination {t_payload t_sender t_source t_destination}
destination (r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) r.(sender)
r.(source) destination.
End Transfer.
Definition Transfer_skeleton := Transfer.record.
Module Info_per_level.
Record record {timestamp predecessor : Set} : Set := Build {
timestamp : timestamp;
predecessor : predecessor;
}.
Arguments record : clear implicits.
Definition with_timestamp {t_timestamp t_predecessor} timestamp
(r : record t_timestamp t_predecessor) :=
Build t_timestamp t_predecessor timestamp r.(predecessor).
Definition with_predecessor {t_timestamp t_predecessor} predecessor
(r : record t_timestamp t_predecessor) :=
Build t_timestamp t_predecessor r.(timestamp) predecessor.
End Info_per_level.
Definition Info_per_level_skeleton := Info_per_level.record.
End internal_inbox_message.
End ConstructorRecords_internal_inbox_message.
Import ConstructorRecords_internal_inbox_message.
Reserved Notation "'internal_inbox_message.Transfer".
Reserved Notation "'internal_inbox_message.Info_per_level".
Inductive internal_inbox_message : Set :=
| Transfer : 'internal_inbox_message.Transfer → internal_inbox_message
| Start_of_level : internal_inbox_message
| End_of_level : internal_inbox_message
| Info_per_level :
'internal_inbox_message.Info_per_level → internal_inbox_message
where "'internal_inbox_message.Transfer" :=
(internal_inbox_message.Transfer_skeleton Script_repr.expr Contract_hash.t
Signature.public_key_hash Sc_rollup_repr.Address.t)
and "'internal_inbox_message.Info_per_level" :=
(internal_inbox_message.Info_per_level_skeleton Time.t Block_hash.t).
Module internal_inbox_message.
Include ConstructorRecords_internal_inbox_message.internal_inbox_message.
Definition Transfer := 'internal_inbox_message.Transfer.
Definition Info_per_level := 'internal_inbox_message.Info_per_level.
End internal_inbox_message.
Definition internal_inbox_message_encoding
: Data_encoding.encoding internal_inbox_message :=
let kind_value (name : string) : Data_encoding.field unit :=
Data_encoding.req None None "internal_inbox_message_kind"
(Data_encoding.constant name) in
Data_encoding.union None
[
Data_encoding.case_value "Transfer" None (Data_encoding.Tag 0)
(Data_encoding.obj5 (kind_value "transfer")
(Data_encoding.req None None "payload" Script_repr.expr_encoding)
(Data_encoding.req None None "sender" Contract_hash.encoding)
(Data_encoding.req None None "source"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Sc_rollup_repr.Address.encoding))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
|
Transfer {|
internal_inbox_message.Transfer.payload := payload;
internal_inbox_message.Transfer.sender := sender;
internal_inbox_message.Transfer.source := source;
internal_inbox_message.Transfer.destination :=
destination
|} ⇒ Some (tt, payload, sender, source, destination)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Script_repr.expr × Contract_hash.t ×
Signature.public_key_hash × Sc_rollup_repr.Address.t) ⇒
let '(_, payload, sender, source, destination) :=
function_parameter in
Transfer
{| internal_inbox_message.Transfer.payload := payload;
internal_inbox_message.Transfer.sender := sender;
internal_inbox_message.Transfer.source := source;
internal_inbox_message.Transfer.destination :=
destination; |});
Data_encoding.case_value "Start_of_level" None (Data_encoding.Tag 1)
(Data_encoding.obj1 (kind_value "start_of_level"))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
| Start_of_level ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Start_of_level);
Data_encoding.case_value "End_of_level" None (Data_encoding.Tag 2)
(Data_encoding.obj1 (kind_value "end_of_level"))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
| End_of_level ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
End_of_level);
Data_encoding.case_value "Info_per_level" None (Data_encoding.Tag 3)
(Data_encoding.obj3 (kind_value "info_per_level")
(Data_encoding.req None None "timestamp" Time.encoding)
(Data_encoding.req None None "predecessor" Block_hash.encoding))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
|
Info_per_level {|
internal_inbox_message.Info_per_level.timestamp := timestamp;
internal_inbox_message.Info_per_level.predecessor :=
predecessor
|} ⇒ Some (tt, timestamp, predecessor)
| _ ⇒ None
end)
(fun (function_parameter : unit × Time.t × Block_hash.t) ⇒
let '(_, timestamp, predecessor) := function_parameter in
Info_per_level
{|
internal_inbox_message.Info_per_level.timestamp :=
timestamp;
internal_inbox_message.Info_per_level.predecessor :=
predecessor; |})
].
Inductive t : Set :=
| Internal : internal_inbox_message → t
| External : string → t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
(Data_encoding.union None
[
Data_encoding.case_value "Internal" None (Data_encoding.Tag 0)
internal_inbox_message_encoding
(fun (function_parameter : t) ⇒
match function_parameter with
| Internal internal_message ⇒ Some internal_message
| External _ ⇒ None
end)
(fun (internal_message : internal_inbox_message) ⇒
Internal internal_message);
Data_encoding.case_value "External" None (Data_encoding.Tag 1)
(Data_encoding._Variable.string' Data_encoding.Hex)
(fun (function_parameter : t) ⇒
match function_parameter with
| External msg ⇒ Some msg
| Internal _ ⇒ None
end) (fun (msg : string) ⇒ External msg)
]).
Definition serialized : Set := string.
Definition serialize (msg : t) : M? string :=
match Data_encoding.Binary.to_string_opt None encoding msg with
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_encode_inbox_message" unit tt)
| Some str ⇒ return? str
end.
Definition deserialize (s_value : string) : M? t :=
match Data_encoding.Binary.of_string_opt encoding s_value with
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_decode_inbox_message" unit tt)
| Some msg ⇒ return? msg
end.
Definition unsafe_of_string {A : Set} (s_value : A) : A := s_value.
Definition unsafe_to_string {A : Set} (s_value : A) : A := s_value.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "239" (String.String "012" "")))).
Module Hash.
Definition prefix : string := "scib3".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "serialized_message_hash" in
let title :=
"The hash of a serialized message of the smart contract rollup inbox."
in
let b58check_prefix := hash_prefix in
let size_value {A : Set} : option A :=
None in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Module internal_inbox_message.
Module Transfer.
Record record {payload sender source destination : Set} : Set := Build {
payload : payload;
sender : sender;
source : source;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_payload {t_payload t_sender t_source t_destination}
payload (r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination payload r.(sender)
r.(source) r.(destination).
Definition with_sender {t_payload t_sender t_source t_destination} sender
(r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) sender
r.(source) r.(destination).
Definition with_source {t_payload t_sender t_source t_destination} source
(r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) r.(sender)
source r.(destination).
Definition with_destination {t_payload t_sender t_source t_destination}
destination (r : record t_payload t_sender t_source t_destination) :=
Build t_payload t_sender t_source t_destination r.(payload) r.(sender)
r.(source) destination.
End Transfer.
Definition Transfer_skeleton := Transfer.record.
Module Info_per_level.
Record record {timestamp predecessor : Set} : Set := Build {
timestamp : timestamp;
predecessor : predecessor;
}.
Arguments record : clear implicits.
Definition with_timestamp {t_timestamp t_predecessor} timestamp
(r : record t_timestamp t_predecessor) :=
Build t_timestamp t_predecessor timestamp r.(predecessor).
Definition with_predecessor {t_timestamp t_predecessor} predecessor
(r : record t_timestamp t_predecessor) :=
Build t_timestamp t_predecessor r.(timestamp) predecessor.
End Info_per_level.
Definition Info_per_level_skeleton := Info_per_level.record.
End internal_inbox_message.
End ConstructorRecords_internal_inbox_message.
Import ConstructorRecords_internal_inbox_message.
Reserved Notation "'internal_inbox_message.Transfer".
Reserved Notation "'internal_inbox_message.Info_per_level".
Inductive internal_inbox_message : Set :=
| Transfer : 'internal_inbox_message.Transfer → internal_inbox_message
| Start_of_level : internal_inbox_message
| End_of_level : internal_inbox_message
| Info_per_level :
'internal_inbox_message.Info_per_level → internal_inbox_message
where "'internal_inbox_message.Transfer" :=
(internal_inbox_message.Transfer_skeleton Script_repr.expr Contract_hash.t
Signature.public_key_hash Sc_rollup_repr.Address.t)
and "'internal_inbox_message.Info_per_level" :=
(internal_inbox_message.Info_per_level_skeleton Time.t Block_hash.t).
Module internal_inbox_message.
Include ConstructorRecords_internal_inbox_message.internal_inbox_message.
Definition Transfer := 'internal_inbox_message.Transfer.
Definition Info_per_level := 'internal_inbox_message.Info_per_level.
End internal_inbox_message.
Definition internal_inbox_message_encoding
: Data_encoding.encoding internal_inbox_message :=
let kind_value (name : string) : Data_encoding.field unit :=
Data_encoding.req None None "internal_inbox_message_kind"
(Data_encoding.constant name) in
Data_encoding.union None
[
Data_encoding.case_value "Transfer" None (Data_encoding.Tag 0)
(Data_encoding.obj5 (kind_value "transfer")
(Data_encoding.req None None "payload" Script_repr.expr_encoding)
(Data_encoding.req None None "sender" Contract_hash.encoding)
(Data_encoding.req None None "source"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Sc_rollup_repr.Address.encoding))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
|
Transfer {|
internal_inbox_message.Transfer.payload := payload;
internal_inbox_message.Transfer.sender := sender;
internal_inbox_message.Transfer.source := source;
internal_inbox_message.Transfer.destination :=
destination
|} ⇒ Some (tt, payload, sender, source, destination)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Script_repr.expr × Contract_hash.t ×
Signature.public_key_hash × Sc_rollup_repr.Address.t) ⇒
let '(_, payload, sender, source, destination) :=
function_parameter in
Transfer
{| internal_inbox_message.Transfer.payload := payload;
internal_inbox_message.Transfer.sender := sender;
internal_inbox_message.Transfer.source := source;
internal_inbox_message.Transfer.destination :=
destination; |});
Data_encoding.case_value "Start_of_level" None (Data_encoding.Tag 1)
(Data_encoding.obj1 (kind_value "start_of_level"))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
| Start_of_level ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Start_of_level);
Data_encoding.case_value "End_of_level" None (Data_encoding.Tag 2)
(Data_encoding.obj1 (kind_value "end_of_level"))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
| End_of_level ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
End_of_level);
Data_encoding.case_value "Info_per_level" None (Data_encoding.Tag 3)
(Data_encoding.obj3 (kind_value "info_per_level")
(Data_encoding.req None None "timestamp" Time.encoding)
(Data_encoding.req None None "predecessor" Block_hash.encoding))
(fun (function_parameter : internal_inbox_message) ⇒
match function_parameter with
|
Info_per_level {|
internal_inbox_message.Info_per_level.timestamp := timestamp;
internal_inbox_message.Info_per_level.predecessor :=
predecessor
|} ⇒ Some (tt, timestamp, predecessor)
| _ ⇒ None
end)
(fun (function_parameter : unit × Time.t × Block_hash.t) ⇒
let '(_, timestamp, predecessor) := function_parameter in
Info_per_level
{|
internal_inbox_message.Info_per_level.timestamp :=
timestamp;
internal_inbox_message.Info_per_level.predecessor :=
predecessor; |})
].
Inductive t : Set :=
| Internal : internal_inbox_message → t
| External : string → t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
(Data_encoding.union None
[
Data_encoding.case_value "Internal" None (Data_encoding.Tag 0)
internal_inbox_message_encoding
(fun (function_parameter : t) ⇒
match function_parameter with
| Internal internal_message ⇒ Some internal_message
| External _ ⇒ None
end)
(fun (internal_message : internal_inbox_message) ⇒
Internal internal_message);
Data_encoding.case_value "External" None (Data_encoding.Tag 1)
(Data_encoding._Variable.string' Data_encoding.Hex)
(fun (function_parameter : t) ⇒
match function_parameter with
| External msg ⇒ Some msg
| Internal _ ⇒ None
end) (fun (msg : string) ⇒ External msg)
]).
Definition serialized : Set := string.
Definition serialize (msg : t) : M? string :=
match Data_encoding.Binary.to_string_opt None encoding msg with
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_encode_inbox_message" unit tt)
| Some str ⇒ return? str
end.
Definition deserialize (s_value : string) : M? t :=
match Data_encoding.Binary.of_string_opt encoding s_value with
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_decode_inbox_message" unit tt)
| Some msg ⇒ return? msg
end.
Definition unsafe_of_string {A : Set} (s_value : A) : A := s_value.
Definition unsafe_to_string {A : Set} (s_value : A) : A := s_value.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "239" (String.String "012" "")))).
Module Hash.
Definition prefix : string := "scib3".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "serialized_message_hash" in
let title :=
"The hash of a serialized message of the smart contract rollup inbox."
in
let b58check_prefix := hash_prefix in
let size_value {A : Set} : option A :=
None in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Inclusion of the module [H]
Definition t := H.(S.HASH.t).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
End Hash.
Definition hash_serialized_message (payload : serialized) : Hash.t :=
Hash.hash_string None [ payload ].
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
End Hash.
Definition hash_serialized_message (payload : serialized) : Hash.t :=
Hash.hash_string None [ payload ].