🦏 Sc_rollup_inbox_merkelized_payload_hashes_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.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.merkelized_payload_hashes_proof_error"
"Internal error: error occurred during proof production or validation"
"A merkelized payload hashes proof error."
(Some
(fun (ppf : Format.formatter) ⇒
fun (e_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Proof error: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format)) "Proof error: %s")
e_value))
(Data_encoding.obj1
(Data_encoding.req None None "error" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Merkelized_payload_hashes_proof_error" then
let e_value := cast string payload in
Some e_value
else None
end)
(fun (e_value : string) ⇒
Build_extensible "Merkelized_payload_hashes_proof_error" string e_value).
Module Skip_list_parameters.
Definition basis : int := 2.
(* Skip_list_parameters *)
Definition module :=
{|
Skip_list_repr.S_Parameters.basis := basis
|}.
End Skip_list_parameters.
Definition Skip_list_parameters := Skip_list_parameters.module.
Definition Skip_list := Skip_list_repr.Make Skip_list_parameters.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "238" (String.String "238" "")))).
Module Hash.
Definition prefix : string := "scib2".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "merkelized_payload_hashes_hash" in
let title :=
"The merkelized payload hashes' hash 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
|}).
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox_message_repr.merkelized_payload_hashes_proof_error"
"Internal error: error occurred during proof production or validation"
"A merkelized payload hashes proof error."
(Some
(fun (ppf : Format.formatter) ⇒
fun (e_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Proof error: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format)) "Proof error: %s")
e_value))
(Data_encoding.obj1
(Data_encoding.req None None "error" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Merkelized_payload_hashes_proof_error" then
let e_value := cast string payload in
Some e_value
else None
end)
(fun (e_value : string) ⇒
Build_extensible "Merkelized_payload_hashes_proof_error" string e_value).
Module Skip_list_parameters.
Definition basis : int := 2.
(* Skip_list_parameters *)
Definition module :=
{|
Skip_list_repr.S_Parameters.basis := basis
|}.
End Skip_list_parameters.
Definition Skip_list_parameters := Skip_list_parameters.module.
Definition Skip_list := Skip_list_repr.Make Skip_list_parameters.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "238" (String.String "238" "")))).
Module Hash.
Definition prefix : string := "scib2".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "merkelized_payload_hashes_hash" in
let title :=
"The merkelized payload hashes' hash 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 t : Set :=
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t.
Definition equal
: Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→ bool :=
Skip_list.(Skip_list_repr.S.equal) Hash.equal
Sc_rollup_inbox_message_repr.Hash.equal.
Definition hash_value
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
: Hash.t :=
let payload_hash := Skip_list.(Skip_list_repr.S.content) merkelized in
let back_pointers_hashes :=
Skip_list.(Skip_list_repr.S.back_pointers) merkelized in
Hash.hash_bytes None
(cons (Sc_rollup_inbox_message_repr.Hash.to_bytes payload_hash)
(List.map Hash.to_bytes back_pointers_hashes)).
Definition pp
: Format.formatter →
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→ unit :=
Skip_list.(Skip_list_repr.S.pp) Hash.pp Sc_rollup_inbox_message_repr.Hash.pp.
Definition encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Hash.encoding
Sc_rollup_inbox_message_repr.Hash.encoding.
Module merkelized_and_payload.
Record record : Set := Build {
merkelized : t;
payload : Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_merkelized merkelized (r : record) :=
Build merkelized r.(payload).
Definition with_payload payload (r : record) :=
Build r.(merkelized) payload.
End merkelized_and_payload.
Definition merkelized_and_payload := merkelized_and_payload.record.
Definition equal_merkelized_and_payload
(function_parameter : merkelized_and_payload)
: merkelized_and_payload → bool :=
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
fun (mp2 : merkelized_and_payload) ⇒
(equal merkelized mp2.(merkelized_and_payload.merkelized)) &&
(String.equal payload mp2.(merkelized_and_payload.payload)).
Definition pp_merkelized_and_payload
(fmt : Format.formatter) (function_parameter : merkelized_and_payload)
: unit :=
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hv 2>"
CamlinternalFormatBasics.End_of_format) "<hv 2>"))
(CamlinternalFormatBasics.String_literal "merkelized:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "payload: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))
"@[<hv 2>merkelized:@,%a@,payload: %a@]") pp merkelized
Format.pp_print_string payload.
Definition merkelized_and_payload_encoding
: Data_encoding.encoding merkelized_and_payload :=
Data_encoding.conv
(fun (function_parameter : merkelized_and_payload) ⇒
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
(merkelized, payload))
(fun (function_parameter : t × string) ⇒
let '(merkelized, payload) := function_parameter in
{| merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload :=
Sc_rollup_inbox_message_repr.unsafe_of_string payload; |}) None
(Data_encoding.merge_objs encoding
(Data_encoding.obj1
(Data_encoding.req None None "payload" Data_encoding.string_value))).
Module History.
Definition Bounded_history_repr_Make_include :=
Bounded_history_repr.Make
(let name := "level_inbox_history" in
let _sig_NAME := tt in
{|
Bounded_history_repr.NAME.name := name;
Bounded_history_repr.NAME._sig_NAME := _sig_NAME
|})
(let t : Set := Hash.t in
let compare := Hash.compare in
let pp := Hash.pp in
let encoding := Hash.encoding in
let _sig_KEY := tt in
{|
Bounded_history_repr.KEY.compare := compare;
Bounded_history_repr.KEY.pp := pp;
Bounded_history_repr.KEY.encoding := encoding;
Bounded_history_repr.KEY._sig_KEY := _sig_KEY
|})
(let t : Set := merkelized_and_payload in
let pp := pp_merkelized_and_payload in
let equal := equal_merkelized_and_payload in
let encoding := merkelized_and_payload_encoding in
{|
Bounded_history_repr.VALUE.equal := equal;
Bounded_history_repr.VALUE.pp := pp;
Bounded_history_repr.VALUE.encoding := encoding
|}).
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
End Hash.
Definition t : Set :=
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t.
Definition equal
: Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→ bool :=
Skip_list.(Skip_list_repr.S.equal) Hash.equal
Sc_rollup_inbox_message_repr.Hash.equal.
Definition hash_value
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
: Hash.t :=
let payload_hash := Skip_list.(Skip_list_repr.S.content) merkelized in
let back_pointers_hashes :=
Skip_list.(Skip_list_repr.S.back_pointers) merkelized in
Hash.hash_bytes None
(cons (Sc_rollup_inbox_message_repr.Hash.to_bytes payload_hash)
(List.map Hash.to_bytes back_pointers_hashes)).
Definition pp
: Format.formatter →
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
→ unit :=
Skip_list.(Skip_list_repr.S.pp) Hash.pp Sc_rollup_inbox_message_repr.Hash.pp.
Definition encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Hash.encoding
Sc_rollup_inbox_message_repr.Hash.encoding.
Module merkelized_and_payload.
Record record : Set := Build {
merkelized : t;
payload : Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_merkelized merkelized (r : record) :=
Build merkelized r.(payload).
Definition with_payload payload (r : record) :=
Build r.(merkelized) payload.
End merkelized_and_payload.
Definition merkelized_and_payload := merkelized_and_payload.record.
Definition equal_merkelized_and_payload
(function_parameter : merkelized_and_payload)
: merkelized_and_payload → bool :=
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
fun (mp2 : merkelized_and_payload) ⇒
(equal merkelized mp2.(merkelized_and_payload.merkelized)) &&
(String.equal payload mp2.(merkelized_and_payload.payload)).
Definition pp_merkelized_and_payload
(fmt : Format.formatter) (function_parameter : merkelized_and_payload)
: unit :=
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hv 2>"
CamlinternalFormatBasics.End_of_format) "<hv 2>"))
(CamlinternalFormatBasics.String_literal "merkelized:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "payload: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))
"@[<hv 2>merkelized:@,%a@,payload: %a@]") pp merkelized
Format.pp_print_string payload.
Definition merkelized_and_payload_encoding
: Data_encoding.encoding merkelized_and_payload :=
Data_encoding.conv
(fun (function_parameter : merkelized_and_payload) ⇒
let '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload
|} := function_parameter in
(merkelized, payload))
(fun (function_parameter : t × string) ⇒
let '(merkelized, payload) := function_parameter in
{| merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload :=
Sc_rollup_inbox_message_repr.unsafe_of_string payload; |}) None
(Data_encoding.merge_objs encoding
(Data_encoding.obj1
(Data_encoding.req None None "payload" Data_encoding.string_value))).
Module History.
Definition Bounded_history_repr_Make_include :=
Bounded_history_repr.Make
(let name := "level_inbox_history" in
let _sig_NAME := tt in
{|
Bounded_history_repr.NAME.name := name;
Bounded_history_repr.NAME._sig_NAME := _sig_NAME
|})
(let t : Set := Hash.t in
let compare := Hash.compare in
let pp := Hash.pp in
let encoding := Hash.encoding in
let _sig_KEY := tt in
{|
Bounded_history_repr.KEY.compare := compare;
Bounded_history_repr.KEY.pp := pp;
Bounded_history_repr.KEY.encoding := encoding;
Bounded_history_repr.KEY._sig_KEY := _sig_KEY
|})
(let t : Set := merkelized_and_payload in
let pp := pp_merkelized_and_payload in
let equal := equal_merkelized_and_payload in
let encoding := merkelized_and_payload_encoding in
{|
Bounded_history_repr.VALUE.equal := equal;
Bounded_history_repr.VALUE.pp := pp;
Bounded_history_repr.VALUE.encoding := encoding
|}).
Inclusion of the module [Bounded_history_repr_Make_include]
Definition t := Bounded_history_repr_Make_include.(Bounded_history_repr.S.t).
Definition key :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.key).
Definition value :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.value).
Definition empty :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.empty).
Definition encoding :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.encoding).
Definition pp :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.pp).
Definition find :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.find).
Definition remember :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.remember).
Definition no_history : t := empty 0.
End History.
Definition remember
(history_value : History.t)
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
(payload : Sc_rollup_inbox_message_repr.serialized) : M? History.t :=
let prev_cell_ptr := hash_value merkelized in
History.remember prev_cell_ptr
{| merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload; |} history_value.
Definition genesis
(history_value : History.t)
(payload : Sc_rollup_inbox_message_repr.serialized)
: M?
(History.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let payload_hash :=
Sc_rollup_inbox_message_repr.hash_serialized_message payload in
let merkelized := Skip_list.(Skip_list_repr.S.genesis) payload_hash in
Error_monad.Result_syntax.op_letplus
(remember history_value merkelized payload)
(fun history_value ⇒ (history_value, merkelized)).
Definition add_payload
(history_value : History.t)
(prev_merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
(payload : Sc_rollup_inbox_message_repr.serialized)
: M?
(History.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let prev_merkelized_ptr := hash_value prev_merkelized in
let merkelized :=
Skip_list.(Skip_list_repr.S.next) prev_merkelized prev_merkelized_ptr
(Sc_rollup_inbox_message_repr.hash_serialized_message payload) in
let? history_value := remember history_value merkelized payload in
return? (history_value, merkelized).
Definition get_payload_hash {A B : Set}
: Skip_list.(Skip_list_repr.S.cell) A B → A :=
Skip_list.(Skip_list_repr.S.content).
Definition get_index {A B : Set}
: Skip_list.(Skip_list_repr.S.cell) A B → int :=
Skip_list.(Skip_list_repr.S.index_value).
Definition proof : Set := list t.
Definition pp_proof
: Format.formatter →
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) → unit := Format.pp_print_list None pp.
Definition proof_encoding
: Data_encoding.encoding
(list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t)) := Data_encoding.list_value None encoding.
Definition produce_proof
(history_value : History.t) (index_value : int)
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
: option (merkelized_and_payload × list t) :=
let deref (ptr : History.key) : option t :=
let× '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := _
|} := History.find ptr history_value in
return× merkelized in
let current_ptr := hash_value merkelized in
let lift_ptr :=
let fix aux (acc_value : list t) (function_parameter : list History.key)
: option (merkelized_and_payload × list t) :=
match function_parameter with
| [] ⇒ None
| cons last_ptr [] ⇒
Error_monad.Option_syntax.op_letplus
(History.find last_ptr history_value)
(fun function_parameter ⇒
let
'{| merkelized_and_payload.merkelized := merkelized |} as
merkelized_and_payload := function_parameter in
(merkelized_and_payload, (List.rev (cons merkelized acc_value))))
| cons ptr rest ⇒
let× merkelized := deref ptr in
aux (cons merkelized acc_value) rest
end in
aux nil in
let× ptr_path :=
Skip_list.(Skip_list_repr.S.back_path) deref current_ptr index_value in
lift_ptr ptr_path.
Definition verify_proof
(inclusion_proof :
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t))
: M?
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let? cell_value :=
match inclusion_proof with
| cons cell_value _ ⇒ return? cell_value
| [] ⇒
Error_monad.error_value
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"inclusion proof is empty")
end in
let fix aux
(hash_map_ptr_list :
Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) × list Hash.t)
(l_value :
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t))
: M?
(Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) × list Hash.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t × Hash.t) :=
let '(hash_map, ptr_list) := hash_map_ptr_list in
match l_value with
| [] ⇒
Error_monad.error_value
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"inclusion proof is empty")
| cons target [] ⇒
let target_ptr := hash_value target in
let hash_map :=
Hash.H.(HASH.Map).(S.INDEXES_MAP.add) target_ptr target hash_map in
let ptr_list := List.rev (cons target_ptr ptr_list) in
return? (hash_map, ptr_list, target, target_ptr)
| cons merkelized tail ⇒
let ptr := hash_value merkelized in
aux
((Hash.H.(HASH.Map).(S.INDEXES_MAP.add) ptr merkelized hash_map),
(cons ptr ptr_list)) tail
end in
let? '(hash_map, ptr_list, target, target_ptr) :=
aux (Hash.H.(HASH.Map).(S.INDEXES_MAP.empty), nil) inclusion_proof in
let deref (ptr : Hash.H.(S.HASH.t))
: option
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
Hash.H.(HASH.Map).(S.INDEXES_MAP.find) ptr hash_map in
let cell_ptr := hash_value cell_value in
let? '_ :=
Error_monad.error_unless
(Skip_list.(Skip_list_repr.S.valid_back_path) Hash.equal deref cell_ptr
target_ptr ptr_list)
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"invalid inclusion proof") in
return? (target, cell_value).
Definition key :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.key).
Definition value :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.value).
Definition empty :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.empty).
Definition encoding :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.encoding).
Definition pp :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.pp).
Definition find :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.find).
Definition remember :=
Bounded_history_repr_Make_include.(Bounded_history_repr.S.remember).
Definition no_history : t := empty 0.
End History.
Definition remember
(history_value : History.t)
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
(payload : Sc_rollup_inbox_message_repr.serialized) : M? History.t :=
let prev_cell_ptr := hash_value merkelized in
History.remember prev_cell_ptr
{| merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := payload; |} history_value.
Definition genesis
(history_value : History.t)
(payload : Sc_rollup_inbox_message_repr.serialized)
: M?
(History.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let payload_hash :=
Sc_rollup_inbox_message_repr.hash_serialized_message payload in
let merkelized := Skip_list.(Skip_list_repr.S.genesis) payload_hash in
Error_monad.Result_syntax.op_letplus
(remember history_value merkelized payload)
(fun history_value ⇒ (history_value, merkelized)).
Definition add_payload
(history_value : History.t)
(prev_merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
(payload : Sc_rollup_inbox_message_repr.serialized)
: M?
(History.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let prev_merkelized_ptr := hash_value prev_merkelized in
let merkelized :=
Skip_list.(Skip_list_repr.S.next) prev_merkelized prev_merkelized_ptr
(Sc_rollup_inbox_message_repr.hash_serialized_message payload) in
let? history_value := remember history_value merkelized payload in
return? (history_value, merkelized).
Definition get_payload_hash {A B : Set}
: Skip_list.(Skip_list_repr.S.cell) A B → A :=
Skip_list.(Skip_list_repr.S.content).
Definition get_index {A B : Set}
: Skip_list.(Skip_list_repr.S.cell) A B → int :=
Skip_list.(Skip_list_repr.S.index_value).
Definition proof : Set := list t.
Definition pp_proof
: Format.formatter →
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) → unit := Format.pp_print_list None pp.
Definition proof_encoding
: Data_encoding.encoding
(list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t)) := Data_encoding.list_value None encoding.
Definition produce_proof
(history_value : History.t) (index_value : int)
(merkelized :
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
: option (merkelized_and_payload × list t) :=
let deref (ptr : History.key) : option t :=
let× '{|
merkelized_and_payload.merkelized := merkelized;
merkelized_and_payload.payload := _
|} := History.find ptr history_value in
return× merkelized in
let current_ptr := hash_value merkelized in
let lift_ptr :=
let fix aux (acc_value : list t) (function_parameter : list History.key)
: option (merkelized_and_payload × list t) :=
match function_parameter with
| [] ⇒ None
| cons last_ptr [] ⇒
Error_monad.Option_syntax.op_letplus
(History.find last_ptr history_value)
(fun function_parameter ⇒
let
'{| merkelized_and_payload.merkelized := merkelized |} as
merkelized_and_payload := function_parameter in
(merkelized_and_payload, (List.rev (cons merkelized acc_value))))
| cons ptr rest ⇒
let× merkelized := deref ptr in
aux (cons merkelized acc_value) rest
end in
aux nil in
let× ptr_path :=
Skip_list.(Skip_list_repr.S.back_path) deref current_ptr index_value in
lift_ptr ptr_path.
Definition verify_proof
(inclusion_proof :
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t))
: M?
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
let? cell_value :=
match inclusion_proof with
| cons cell_value _ ⇒ return? cell_value
| [] ⇒
Error_monad.error_value
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"inclusion proof is empty")
end in
let fix aux
(hash_map_ptr_list :
Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) × list Hash.t)
(l_value :
list
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t))
: M?
(Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) × list Hash.t ×
Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t × Hash.t) :=
let '(hash_map, ptr_list) := hash_map_ptr_list in
match l_value with
| [] ⇒
Error_monad.error_value
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"inclusion proof is empty")
| cons target [] ⇒
let target_ptr := hash_value target in
let hash_map :=
Hash.H.(HASH.Map).(S.INDEXES_MAP.add) target_ptr target hash_map in
let ptr_list := List.rev (cons target_ptr ptr_list) in
return? (hash_map, ptr_list, target, target_ptr)
| cons merkelized tail ⇒
let ptr := hash_value merkelized in
aux
((Hash.H.(HASH.Map).(S.INDEXES_MAP.add) ptr merkelized hash_map),
(cons ptr ptr_list)) tail
end in
let? '(hash_map, ptr_list, target, target_ptr) :=
aux (Hash.H.(HASH.Map).(S.INDEXES_MAP.empty), nil) inclusion_proof in
let deref (ptr : Hash.H.(S.HASH.t))
: option
(Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
Hash.t) :=
Hash.H.(HASH.Map).(S.INDEXES_MAP.find) ptr hash_map in
let cell_ptr := hash_value cell_value in
let? '_ :=
Error_monad.error_unless
(Skip_list.(Skip_list_repr.S.valid_back_path) Hash.equal deref cell_ptr
target_ptr ptr_list)
(Build_extensible "Merkelized_payload_hashes_proof_error" string
"invalid inclusion proof") in
return? (target, cell_value).