🦏 Sc_rollup_commitment_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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Definition hash_prefix : string :=
String.String "017" (String.String "144" (String.String "021" "d")).
Module Hash.
Definition prefix : string := "scc1".
Definition encoded_size : int := 54.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "commitment_hash" in
let title := "The hash of a commitment of a smart contract rollup" 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
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Definition hash_prefix : string :=
String.String "017" (String.String "144" (String.String "021" "d")).
Module Hash.
Definition prefix : string := "scc1".
Definition encoded_size : int := 54.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "commitment_hash" in
let title := "The hash of a commitment of a smart contract rollup" 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.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Inclusion of the module [Path_encoding_Make_hex_include]
Definition to_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Hash.
Module V1.
Module t.
Record record : Set := Build {
compressed_state : Sc_rollup_repr.State_hash.t;
inbox_level : Raw_level_repr.t;
predecessor : Hash.t;
number_of_ticks : Sc_rollup_repr.Number_of_ticks.t;
}.
Definition with_compressed_state compressed_state (r : record) :=
Build compressed_state r.(inbox_level) r.(predecessor)
r.(number_of_ticks).
Definition with_inbox_level inbox_level (r : record) :=
Build r.(compressed_state) inbox_level r.(predecessor)
r.(number_of_ticks).
Definition with_predecessor predecessor (r : record) :=
Build r.(compressed_state) r.(inbox_level) predecessor
r.(number_of_ticks).
Definition with_number_of_ticks number_of_ticks (r : record) :=
Build r.(compressed_state) r.(inbox_level) r.(predecessor)
number_of_ticks.
End t.
Definition t := t.record.
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.compressed_state := compressed_state;
t.inbox_level := inbox_level;
t.predecessor := predecessor;
t.number_of_ticks := number_of_ticks
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "compressed_state: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "inbox_level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "predecessor: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"number_of_ticks: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))))))))))
"compressed_state: %a@,inbox_level: %a@,predecessor: %a@,number_of_ticks: %Ld")
Sc_rollup_repr.State_hash.pp compressed_state Raw_level_repr.pp
inbox_level Hash.pp predecessor
(Sc_rollup_repr.Number_of_ticks.to_value number_of_ticks).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.compressed_state := compressed_state;
t.inbox_level := inbox_level;
t.predecessor := predecessor;
t.number_of_ticks := number_of_ticks
|} := function_parameter in
(compressed_state, inbox_level, predecessor, number_of_ticks))
(fun (function_parameter :
Sc_rollup_repr.State_hash.t × Raw_level_repr.t × Hash.t ×
Sc_rollup_repr.Number_of_ticks.t) ⇒
let '(compressed_state, inbox_level, predecessor, number_of_ticks) :=
function_parameter in
{| t.compressed_state := compressed_state; t.inbox_level := inbox_level;
t.predecessor := predecessor; t.number_of_ticks := number_of_ticks; |})
None
(Data_encoding.obj4
(Data_encoding.req None None "compressed_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "predecessor" Hash.encoding)
(Data_encoding.req None None "number_of_ticks"
Sc_rollup_repr.Number_of_ticks.encoding)).
Definition hash_uncarbonated (commitment : t) : Hash.t :=
let commitment_bytes :=
Data_encoding.Binary.to_bytes_exn None encoding commitment in
Hash.hash_bytes None [ commitment_bytes ].
Definition genesis_commitment {A : Set}
(origination_level : Raw_level_repr.t)
(genesis_state_hash : Sc_rollup_repr.State_hash.t)
: Pervasives.result t A :=
let number_of_ticks := Sc_rollup_repr.Number_of_ticks.zero in
return?
{| t.compressed_state := genesis_state_hash;
t.inbox_level := origination_level; t.predecessor := Hash.zero;
t.number_of_ticks := number_of_ticks; |}.
Module genesis_info.
Record record : Set := Build {
level : Raw_level_repr.t;
commitment_hash : Hash.t;
}.
Definition with_level level (r : record) :=
Build level r.(commitment_hash).
Definition with_commitment_hash commitment_hash (r : record) :=
Build r.(level) commitment_hash.
End genesis_info.
Definition genesis_info := genesis_info.record.
Definition genesis_info_encoding : Data_encoding.encoding genesis_info :=
Data_encoding.conv
(fun (function_parameter : genesis_info) ⇒
let '{|
genesis_info.level := level;
genesis_info.commitment_hash := commitment_hash
|} := function_parameter in
(level, commitment_hash))
(fun (function_parameter : Raw_level_repr.t × Hash.t) ⇒
let '(level, commitment_hash) := function_parameter in
{| genesis_info.level := level;
genesis_info.commitment_hash := commitment_hash; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "commitment_hash" Hash.encoding)).
End V1.
Inductive versioned : Set :=
| V1 : V1.t → versioned.
Definition versioned_encoding : Data_encoding.encoding versioned :=
Data_encoding.union None
[
Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
(fun (function_parameter : versioned) ⇒
let 'V1 commitment := function_parameter in
Some commitment) (fun (commitment : V1.t) ⇒ V1 commitment)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 commitment := function_parameter in
commitment.
Definition to_versioned (commitment : V1.t) : versioned := V1 commitment.
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Hash.
Module V1.
Module t.
Record record : Set := Build {
compressed_state : Sc_rollup_repr.State_hash.t;
inbox_level : Raw_level_repr.t;
predecessor : Hash.t;
number_of_ticks : Sc_rollup_repr.Number_of_ticks.t;
}.
Definition with_compressed_state compressed_state (r : record) :=
Build compressed_state r.(inbox_level) r.(predecessor)
r.(number_of_ticks).
Definition with_inbox_level inbox_level (r : record) :=
Build r.(compressed_state) inbox_level r.(predecessor)
r.(number_of_ticks).
Definition with_predecessor predecessor (r : record) :=
Build r.(compressed_state) r.(inbox_level) predecessor
r.(number_of_ticks).
Definition with_number_of_ticks number_of_ticks (r : record) :=
Build r.(compressed_state) r.(inbox_level) r.(predecessor)
number_of_ticks.
End t.
Definition t := t.record.
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.compressed_state := compressed_state;
t.inbox_level := inbox_level;
t.predecessor := predecessor;
t.number_of_ticks := number_of_ticks
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "compressed_state: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "inbox_level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "predecessor: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"number_of_ticks: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)))))))))))
"compressed_state: %a@,inbox_level: %a@,predecessor: %a@,number_of_ticks: %Ld")
Sc_rollup_repr.State_hash.pp compressed_state Raw_level_repr.pp
inbox_level Hash.pp predecessor
(Sc_rollup_repr.Number_of_ticks.to_value number_of_ticks).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.compressed_state := compressed_state;
t.inbox_level := inbox_level;
t.predecessor := predecessor;
t.number_of_ticks := number_of_ticks
|} := function_parameter in
(compressed_state, inbox_level, predecessor, number_of_ticks))
(fun (function_parameter :
Sc_rollup_repr.State_hash.t × Raw_level_repr.t × Hash.t ×
Sc_rollup_repr.Number_of_ticks.t) ⇒
let '(compressed_state, inbox_level, predecessor, number_of_ticks) :=
function_parameter in
{| t.compressed_state := compressed_state; t.inbox_level := inbox_level;
t.predecessor := predecessor; t.number_of_ticks := number_of_ticks; |})
None
(Data_encoding.obj4
(Data_encoding.req None None "compressed_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
(Data_encoding.req None None "predecessor" Hash.encoding)
(Data_encoding.req None None "number_of_ticks"
Sc_rollup_repr.Number_of_ticks.encoding)).
Definition hash_uncarbonated (commitment : t) : Hash.t :=
let commitment_bytes :=
Data_encoding.Binary.to_bytes_exn None encoding commitment in
Hash.hash_bytes None [ commitment_bytes ].
Definition genesis_commitment {A : Set}
(origination_level : Raw_level_repr.t)
(genesis_state_hash : Sc_rollup_repr.State_hash.t)
: Pervasives.result t A :=
let number_of_ticks := Sc_rollup_repr.Number_of_ticks.zero in
return?
{| t.compressed_state := genesis_state_hash;
t.inbox_level := origination_level; t.predecessor := Hash.zero;
t.number_of_ticks := number_of_ticks; |}.
Module genesis_info.
Record record : Set := Build {
level : Raw_level_repr.t;
commitment_hash : Hash.t;
}.
Definition with_level level (r : record) :=
Build level r.(commitment_hash).
Definition with_commitment_hash commitment_hash (r : record) :=
Build r.(level) commitment_hash.
End genesis_info.
Definition genesis_info := genesis_info.record.
Definition genesis_info_encoding : Data_encoding.encoding genesis_info :=
Data_encoding.conv
(fun (function_parameter : genesis_info) ⇒
let '{|
genesis_info.level := level;
genesis_info.commitment_hash := commitment_hash
|} := function_parameter in
(level, commitment_hash))
(fun (function_parameter : Raw_level_repr.t × Hash.t) ⇒
let '(level, commitment_hash) := function_parameter in
{| genesis_info.level := level;
genesis_info.commitment_hash := commitment_hash; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "commitment_hash" Hash.encoding)).
End V1.
Inductive versioned : Set :=
| V1 : V1.t → versioned.
Definition versioned_encoding : Data_encoding.encoding versioned :=
Data_encoding.union None
[
Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
(fun (function_parameter : versioned) ⇒
let 'V1 commitment := function_parameter in
Some commitment) (fun (commitment : V1.t) ⇒ V1 commitment)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 commitment := function_parameter in
commitment.
Definition to_versioned (commitment : V1.t) : versioned := V1 commitment.