🦏 Sc_rollup_inbox_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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
A Merkelized inbox represents a list of messages. This list
is decomposed into sublists of messages, one for each Tezos level greater
than the level where SCORU is activated.
This module is designed to:
1. provide a space-efficient representation for proofs of inbox
inclusions (only for inboxes obtained at the end of block
validation) ;
2. offer an efficient function to add a new batch of messages in the
inbox at the current level.
To solve (1), we use a proof tree H which is implemented by a merkelized skip
list allowing for compact inclusion proofs (See {!skip_list_repr.ml}).
To solve (2), we maintain a separate proof tree C witnessing the contents of
messages of the current level also implemented by a merkelized skip list for
the same reason.
The protocol maintains the hashes of the head of H and C.
The rollup node needs to maintain a full representation for C and a
partial representation for H back to the level of the LCC.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.invalid_level_add_messages"
"Internal error: Trying to add a message to an inbox from the past"
"An inbox can only accept messages for its current level or for the next levels."
None
(Data_encoding.obj1
(Data_encoding.req None None "level" Raw_level_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_level_add_messages" then
let level := cast Raw_level_repr.t payload in
Some level
else None
end)
(fun (level : Raw_level_repr.raw_level) ⇒
Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.inbox_proof_error"
"Internal error: error occurred during proof production or validation"
"An inbox proof error."
(Some
(fun (ppf : Format.formatter) ⇒
fun (e_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inbox proof error: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Inbox 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 "Inbox_proof_error" then
let e_value := cast string payload in
Some e_value
else None
end)
(fun (e_value : string) ⇒
Build_extensible "Inbox_proof_error" string e_value) in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.add_zero_messages"
"Internal error: trying to add zero messages"
"Message adding functions must be called with a positive number of messages"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Tried to add zero messages"
CamlinternalFormatBasics.End_of_format)
"Tried to add zero messages"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tried_to_add_zero_messages" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tried_to_add_zero_messages" unit tt).
Definition Int64_map :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "238" (String.String "208" "")))).
Module Hash.
Definition prefix : string := "scib1".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "inbox_hash" in
let title := "The hash of an inbox 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
|}).
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.invalid_level_add_messages"
"Internal error: Trying to add a message to an inbox from the past"
"An inbox can only accept messages for its current level or for the next levels."
None
(Data_encoding.obj1
(Data_encoding.req None None "level" Raw_level_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_level_add_messages" then
let level := cast Raw_level_repr.t payload in
Some level
else None
end)
(fun (level : Raw_level_repr.raw_level) ⇒
Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.inbox_proof_error"
"Internal error: error occurred during proof production or validation"
"An inbox proof error."
(Some
(fun (ppf : Format.formatter) ⇒
fun (e_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inbox proof error: "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Inbox 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 "Inbox_proof_error" then
let e_value := cast string payload in
Some e_value
else None
end)
(fun (e_value : string) ⇒
Build_extensible "Inbox_proof_error" string e_value) in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.add_zero_messages"
"Internal error: trying to add zero messages"
"Message adding functions must be called with a positive number of messages"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Tried to add zero messages"
CamlinternalFormatBasics.End_of_format)
"Tried to add zero messages"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tried_to_add_zero_messages" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tried_to_add_zero_messages" unit tt).
Definition Int64_map :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Definition hash_prefix : string :=
String.String "003"
(String.String "250"
(String.String "174" (String.String "238" (String.String "208" "")))).
Module Hash.
Definition prefix : string := "scib1".
Definition encoded_size : int := 55.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "inbox_hash" in
let title := "The hash of an inbox 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 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.S (cell := _) :=
Skip_list_repr.Make Skip_list_parameters.
Module V1.
Module level_proof.
Record record : Set := Build {
hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t;
level : Raw_level_repr.t;
}.
Definition with_hash hash (r : record) :=
Build hash r.(level).
Definition with_level level (r : record) :=
Build r.(hash) level.
End level_proof.
Definition level_proof := level_proof.record.
Definition level_proof_encoding : Data_encoding.encoding level_proof :=
Data_encoding.conv
(fun (function_parameter : level_proof) ⇒
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
(hash_value, level))
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t × Raw_level_repr.t)
⇒
let '(hash_value, level) := function_parameter in
{| level_proof.hash := hash_value; level_proof.level := level; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "hash"
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.encoding)
(Data_encoding.req None None "level" Raw_level_repr.encoding)).
Definition equal_level_proof (function_parameter : level_proof)
: level_proof → bool :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
fun (level_proof_2 : level_proof) ⇒
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal hash_value
level_proof_2.(level_proof.hash)) &&
(Raw_level_repr.equal level level_proof_2.(level_proof.level)).
Definition history_proof : Set :=
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t.
Definition hash_history_proof
(cell_value : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
: Hash.t :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
Skip_list.(Skip_list_repr.S.content) cell_value in
let back_pointers_hashes :=
Skip_list.(Skip_list_repr.S.back_pointers) cell_value in
Hash.hash_bytes None
(cons
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.to_bytes hash_value)
(cons
(Bytes.of_string (Int32.to_string (Raw_level_repr.to_int32 level)))
(List.map Hash.to_bytes back_pointers_hashes))).
Definition equal_history_proof
: Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t →
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t → bool :=
Skip_list.(Skip_list_repr.S.equal) Hash.equal equal_level_proof.
Definition history_proof_encoding : Data_encoding.t history_proof :=
Skip_list.(Skip_list_repr.S.encoding) Hash.encoding level_proof_encoding.
Definition pp_level_proof
(fmt : Format.formatter) (function_parameter : level_proof) : unit :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "level: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))
"hash: %a@,level: %a")
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.pp hash_value
Raw_level_repr.pp level.
Definition pp_history_proof
(fmt : Format.formatter)
(history_proof : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
: unit :=
Skip_list.(Skip_list_repr.S.pp) Hash.pp pp_level_proof fmt history_proof.
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 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.S (cell := _) :=
Skip_list_repr.Make Skip_list_parameters.
Module V1.
Module level_proof.
Record record : Set := Build {
hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t;
level : Raw_level_repr.t;
}.
Definition with_hash hash (r : record) :=
Build hash r.(level).
Definition with_level level (r : record) :=
Build r.(hash) level.
End level_proof.
Definition level_proof := level_proof.record.
Definition level_proof_encoding : Data_encoding.encoding level_proof :=
Data_encoding.conv
(fun (function_parameter : level_proof) ⇒
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
(hash_value, level))
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t × Raw_level_repr.t)
⇒
let '(hash_value, level) := function_parameter in
{| level_proof.hash := hash_value; level_proof.level := level; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "hash"
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.encoding)
(Data_encoding.req None None "level" Raw_level_repr.encoding)).
Definition equal_level_proof (function_parameter : level_proof)
: level_proof → bool :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
fun (level_proof_2 : level_proof) ⇒
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal hash_value
level_proof_2.(level_proof.hash)) &&
(Raw_level_repr.equal level level_proof_2.(level_proof.level)).
Definition history_proof : Set :=
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t.
Definition hash_history_proof
(cell_value : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
: Hash.t :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
Skip_list.(Skip_list_repr.S.content) cell_value in
let back_pointers_hashes :=
Skip_list.(Skip_list_repr.S.back_pointers) cell_value in
Hash.hash_bytes None
(cons
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.to_bytes hash_value)
(cons
(Bytes.of_string (Int32.to_string (Raw_level_repr.to_int32 level)))
(List.map Hash.to_bytes back_pointers_hashes))).
Definition equal_history_proof
: Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t →
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t → bool :=
Skip_list.(Skip_list_repr.S.equal) Hash.equal equal_level_proof.
Definition history_proof_encoding : Data_encoding.t history_proof :=
Skip_list.(Skip_list_repr.S.encoding) Hash.encoding level_proof_encoding.
Definition pp_level_proof
(fmt : Format.formatter) (function_parameter : level_proof) : unit :=
let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "level: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))
"hash: %a@,level: %a")
Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.pp hash_value
Raw_level_repr.pp level.
Definition pp_history_proof
(fmt : Format.formatter)
(history_proof : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
: unit :=
Skip_list.(Skip_list_repr.S.pp) Hash.pp pp_level_proof fmt history_proof.
Construct an inbox [history] with a given [capacity]. If you
are running a rollup node, [capacity] needs to be large enough to
remember any levels for which you may need to produce proofs.
Definition History :
Bounded_history_repr.S (t := _) (key := Hash.t) (value := history_proof) :=
Bounded_history_repr.Make
(let name := "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 := history_proof in
let pp := pp_history_proof in
let equal := equal_history_proof in
let encoding := history_proof_encoding in
{|
Bounded_history_repr.VALUE.equal := equal;
Bounded_history_repr.VALUE.pp := pp;
Bounded_history_repr.VALUE.encoding := encoding
|}).
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
nb_messages_in_commitment_period : int64;
current_level_proof : unit → level_proof;
old_levels_messages : history_proof;
}.
Definition with_level level (r : record) :=
Build level r.(nb_messages_in_commitment_period) r.(current_level_proof)
r.(old_levels_messages).
Definition with_nb_messages_in_commitment_period
nb_messages_in_commitment_period (r : record) :=
Build r.(level) nb_messages_in_commitment_period r.(current_level_proof)
r.(old_levels_messages).
Definition with_current_level_proof current_level_proof (r : record) :=
Build r.(level) r.(nb_messages_in_commitment_period) current_level_proof
r.(old_levels_messages).
Definition with_old_levels_messages old_levels_messages (r : record) :=
Build r.(level) r.(nb_messages_in_commitment_period)
r.(current_level_proof) old_levels_messages.
End t.
Definition t := t.record.
Definition equal (inbox1 : t) (inbox2 : t) : bool :=
let '{|
t.level := level;
t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := inbox1 in
(Raw_level_repr.equal level inbox2.(t.level)) &&
((Compare.Int64.(Compare.S.equal) nb_messages_in_commitment_period
inbox2.(t.nb_messages_in_commitment_period)) &&
((equal_level_proof (current_level_proof tt)
(inbox2.(t.current_level_proof) tt)) &&
(equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.level := level;
t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "{ level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"current messages hash = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"nb_messages_in_commitment_period = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"old_levels_messages = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Char_literal
"}" % char
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))
"@[<hov 2>{ level = %a@;current messages hash = %a@;nb_messages_in_commitment_period = %s@;old_levels_messages = %a@;}@]")
Raw_level_repr.pp level pp_level_proof (current_level_proof tt)
(Int64.to_string nb_messages_in_commitment_period) pp_history_proof
old_levels_messages.
Definition inbox_level (inbox_value : t) : Raw_level_repr.t :=
inbox_value.(t.level).
Definition old_levels_messages (inbox_value : t) : history_proof :=
inbox_value.(t.old_levels_messages).
Definition current_level_proof (inbox_value : t) : level_proof :=
inbox_value.(t.current_level_proof) tt.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.nb_messages_in_commitment_period :=
nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
(nb_messages_in_commitment_period, level, (current_level_proof tt),
old_levels_messages))
(fun (function_parameter :
int64 × Raw_level_repr.t × level_proof × history_proof) ⇒
let
'(nb_messages_in_commitment_period, level, current_level_proof,
old_levels_messages) := function_parameter in
{| t.level := level;
t.nb_messages_in_commitment_period :=
nb_messages_in_commitment_period;
t.current_level_proof :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
current_level_proof; t.old_levels_messages := old_levels_messages;
|}) None
(Data_encoding.obj4
(Data_encoding.req None None "nb_messages_in_commitment_period"
Data_encoding.int64_value)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "current_level_proof" level_proof_encoding)
(Data_encoding.req None None "old_levels_messages"
history_proof_encoding)).
Definition number_of_messages_during_commitment_period (inbox_value : t)
: int64 := inbox_value.(t.nb_messages_in_commitment_period).
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 inbox_value := function_parameter in
Some inbox_value) (fun (inbox_value : V1.t) ⇒ V1 inbox_value)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 inbox_value := function_parameter in
inbox_value.
Definition to_versioned (inbox_value : V1.t) : versioned := V1 inbox_value.
Definition serialized_proof : Set := string.
Definition serialized_proof_encoding : Data_encoding.encoding string :=
Data_encoding.string' None Data_encoding.Hex.
Module level_tree_proof.
Record record : Set := Build {
proof : Sc_rollup_inbox_merkelized_payload_hashes_repr.proof;
payload : option Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_proof proof (r : record) :=
Build proof r.(payload).
Definition with_payload payload (r : record) :=
Build r.(proof) payload.
End level_tree_proof.
Definition level_tree_proof := level_tree_proof.record.
Definition level_tree_proof_encoding
: Data_encoding.encoding level_tree_proof :=
Data_encoding.conv
(fun (function_parameter : level_tree_proof) ⇒
let '{|
level_tree_proof.proof := proof_value;
level_tree_proof.payload := payload
|} := function_parameter in
(proof_value, payload))
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.proof × option string) ⇒
let '(proof_value, payload) := function_parameter in
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload :=
Option.map Sc_rollup_inbox_message_repr.unsafe_of_string payload; |})
None
(Data_encoding.obj2
(Data_encoding.req None None "proof"
Sc_rollup_inbox_merkelized_payload_hashes_repr.proof_encoding)
(Data_encoding.opt None None "payload" Data_encoding.string_value)).
Definition add_message
(inbox_value : t) (payload : Sc_rollup_inbox_message_repr.serialized)
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(level_tree : Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M?
(Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
let? '(level_tree_history, level_tree) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.add_payload
level_tree_history level_tree payload in
let nb_messages_in_commitment_period :=
Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
let inbox_value :=
V1.t.with_nb_messages_in_commitment_period nb_messages_in_commitment_period
inbox_value in
return? (level_tree_history, level_tree, inbox_value).
Bounded_history_repr.S (t := _) (key := Hash.t) (value := history_proof) :=
Bounded_history_repr.Make
(let name := "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 := history_proof in
let pp := pp_history_proof in
let equal := equal_history_proof in
let encoding := history_proof_encoding in
{|
Bounded_history_repr.VALUE.equal := equal;
Bounded_history_repr.VALUE.pp := pp;
Bounded_history_repr.VALUE.encoding := encoding
|}).
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
nb_messages_in_commitment_period : int64;
current_level_proof : unit → level_proof;
old_levels_messages : history_proof;
}.
Definition with_level level (r : record) :=
Build level r.(nb_messages_in_commitment_period) r.(current_level_proof)
r.(old_levels_messages).
Definition with_nb_messages_in_commitment_period
nb_messages_in_commitment_period (r : record) :=
Build r.(level) nb_messages_in_commitment_period r.(current_level_proof)
r.(old_levels_messages).
Definition with_current_level_proof current_level_proof (r : record) :=
Build r.(level) r.(nb_messages_in_commitment_period) current_level_proof
r.(old_levels_messages).
Definition with_old_levels_messages old_levels_messages (r : record) :=
Build r.(level) r.(nb_messages_in_commitment_period)
r.(current_level_proof) old_levels_messages.
End t.
Definition t := t.record.
Definition equal (inbox1 : t) (inbox2 : t) : bool :=
let '{|
t.level := level;
t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := inbox1 in
(Raw_level_repr.equal level inbox2.(t.level)) &&
((Compare.Int64.(Compare.S.equal) nb_messages_in_commitment_period
inbox2.(t.nb_messages_in_commitment_period)) &&
((equal_level_proof (current_level_proof tt)
(inbox2.(t.current_level_proof) tt)) &&
(equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.level := level;
t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "{ level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"current messages hash = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"nb_messages_in_commitment_period = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
"old_levels_messages = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Char_literal
"}" % char
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))
"@[<hov 2>{ level = %a@;current messages hash = %a@;nb_messages_in_commitment_period = %s@;old_levels_messages = %a@;}@]")
Raw_level_repr.pp level pp_level_proof (current_level_proof tt)
(Int64.to_string nb_messages_in_commitment_period) pp_history_proof
old_levels_messages.
Definition inbox_level (inbox_value : t) : Raw_level_repr.t :=
inbox_value.(t.level).
Definition old_levels_messages (inbox_value : t) : history_proof :=
inbox_value.(t.old_levels_messages).
Definition current_level_proof (inbox_value : t) : level_proof :=
inbox_value.(t.current_level_proof) tt.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.nb_messages_in_commitment_period :=
nb_messages_in_commitment_period;
t.current_level_proof := current_level_proof;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
(nb_messages_in_commitment_period, level, (current_level_proof tt),
old_levels_messages))
(fun (function_parameter :
int64 × Raw_level_repr.t × level_proof × history_proof) ⇒
let
'(nb_messages_in_commitment_period, level, current_level_proof,
old_levels_messages) := function_parameter in
{| t.level := level;
t.nb_messages_in_commitment_period :=
nb_messages_in_commitment_period;
t.current_level_proof :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
current_level_proof; t.old_levels_messages := old_levels_messages;
|}) None
(Data_encoding.obj4
(Data_encoding.req None None "nb_messages_in_commitment_period"
Data_encoding.int64_value)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "current_level_proof" level_proof_encoding)
(Data_encoding.req None None "old_levels_messages"
history_proof_encoding)).
Definition number_of_messages_during_commitment_period (inbox_value : t)
: int64 := inbox_value.(t.nb_messages_in_commitment_period).
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 inbox_value := function_parameter in
Some inbox_value) (fun (inbox_value : V1.t) ⇒ V1 inbox_value)
].
Include V1.
Definition of_versioned (function_parameter : versioned) : V1.t :=
let 'V1 inbox_value := function_parameter in
inbox_value.
Definition to_versioned (inbox_value : V1.t) : versioned := V1 inbox_value.
Definition serialized_proof : Set := string.
Definition serialized_proof_encoding : Data_encoding.encoding string :=
Data_encoding.string' None Data_encoding.Hex.
Module level_tree_proof.
Record record : Set := Build {
proof : Sc_rollup_inbox_merkelized_payload_hashes_repr.proof;
payload : option Sc_rollup_inbox_message_repr.serialized;
}.
Definition with_proof proof (r : record) :=
Build proof r.(payload).
Definition with_payload payload (r : record) :=
Build r.(proof) payload.
End level_tree_proof.
Definition level_tree_proof := level_tree_proof.record.
Definition level_tree_proof_encoding
: Data_encoding.encoding level_tree_proof :=
Data_encoding.conv
(fun (function_parameter : level_tree_proof) ⇒
let '{|
level_tree_proof.proof := proof_value;
level_tree_proof.payload := payload
|} := function_parameter in
(proof_value, payload))
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.proof × option string) ⇒
let '(proof_value, payload) := function_parameter in
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload :=
Option.map Sc_rollup_inbox_message_repr.unsafe_of_string payload; |})
None
(Data_encoding.obj2
(Data_encoding.req None None "proof"
Sc_rollup_inbox_merkelized_payload_hashes_repr.proof_encoding)
(Data_encoding.opt None None "payload" Data_encoding.string_value)).
Definition add_message
(inbox_value : t) (payload : Sc_rollup_inbox_message_repr.serialized)
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(level_tree : Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M?
(Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
let? '(level_tree_history, level_tree) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.add_payload
level_tree_history level_tree payload in
let nb_messages_in_commitment_period :=
Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
let inbox_value :=
V1.t.with_nb_messages_in_commitment_period nb_messages_in_commitment_period
inbox_value in
return? (level_tree_history, level_tree, inbox_value).
[initialize_level_tree_when_needed level_tree_history inbox level_tree
payloads] creates a new [level_tree] with the first element of [payloads] if
[level_tree] is None.
Definition initialize_level_tree_when_needed
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(inbox_value : t)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
: M?
(t × Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
list Sc_rollup_inbox_message_repr.serialized) :=
match level_tree with
| Some level_tree ⇒
return? (inbox_value, level_tree_history, level_tree, payloads)
| None ⇒
let? '(first_payload, payloads) :=
match payloads with
| cons hd tl ⇒ return? (hd, tl)
| [] ⇒
Error_monad.error_value
(Build_extensible "Tried_to_add_zero_messages" unit tt)
end in
let? '(level_tree_history, level_tree) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis level_tree_history
first_payload in
let nb_messages_in_commitment_period :=
Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
let inbox_value :=
V1.t.with_nb_messages_in_commitment_period
nb_messages_in_commitment_period inbox_value in
return? (inbox_value, level_tree_history, level_tree, payloads)
end.
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(inbox_value : t)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
: M?
(t × Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
list Sc_rollup_inbox_message_repr.serialized) :=
match level_tree with
| Some level_tree ⇒
return? (inbox_value, level_tree_history, level_tree, payloads)
| None ⇒
let? '(first_payload, payloads) :=
match payloads with
| cons hd tl ⇒ return? (hd, tl)
| [] ⇒
Error_monad.error_value
(Build_extensible "Tried_to_add_zero_messages" unit tt)
end in
let? '(level_tree_history, level_tree) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis level_tree_history
first_payload in
let nb_messages_in_commitment_period :=
Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
let inbox_value :=
V1.t.with_nb_messages_in_commitment_period
nb_messages_in_commitment_period inbox_value in
return? (inbox_value, level_tree_history, level_tree, payloads)
end.
[no_history] creates an empty history with [capacity] set to
zero---this makes the [remember] function a no-op. We want this
behaviour in the protocol because we don't want to store
previous levels of the inbox.
Definition no_history : V1.History.(Bounded_history_repr.S.t) :=
History.(Bounded_history_repr.S.empty) 0.
Definition take_snapshot (inbox_value : t) : history_proof :=
inbox_value.(V1.t.old_levels_messages).
Definition form_history_proof
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
: M?
(V1.History.(Bounded_history_repr.S.t) ×
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t) :=
let prev_cell := inbox_value.(V1.t.old_levels_messages) in
let prev_cell_ptr := hash_history_proof prev_cell in
let? history_value :=
History.(Bounded_history_repr.S.remember) prev_cell_ptr prev_cell
history_value in
let level_proof := current_level_proof inbox_value in
let cell_value :=
Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr level_proof in
return? (history_value, cell_value).
History.(Bounded_history_repr.S.empty) 0.
Definition take_snapshot (inbox_value : t) : history_proof :=
inbox_value.(V1.t.old_levels_messages).
Definition form_history_proof
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
: M?
(V1.History.(Bounded_history_repr.S.t) ×
Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t) :=
let prev_cell := inbox_value.(V1.t.old_levels_messages) in
let prev_cell_ptr := hash_history_proof prev_cell in
let? history_value :=
History.(Bounded_history_repr.S.remember) prev_cell_ptr prev_cell
history_value in
let level_proof := current_level_proof inbox_value in
let cell_value :=
Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr level_proof in
return? (history_value, cell_value).
[archive_if_needed level_tree_history history inbox new_level level_tree]
is responsible for ensuring that the {!add_messages} function
below has a correctly set-up [level_tree] to which to add the
messages. If [new_level] is a higher level than the current inbox,
we create a new inbox level tree at that level in which to start
adding messages, and archive the earlier levels depending on the
[history] parameter's [capacity]. If [level_tree] is [None] (this
happens when the inbox is first created) we similarly create a new
empty level tree.
This function is the only place we begin new level trees.
Definition archive_if_needed
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
(new_level : Raw_level_repr.raw_level)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
: M?
(V1.History.(Bounded_history_repr.S.t) × t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
list Sc_rollup_inbox_message_repr.serialized) :=
if Raw_level_repr.op_eq inbox_value.(V1.t.level) new_level then
match level_tree with
| Some tree_value ⇒
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads)
| None ⇒
let? '(inbox_value, level_tree_history, tree_value, payloads) :=
initialize_level_tree_when_needed level_tree_history inbox_value
level_tree payloads in
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads)
end
else
let? '(history_value, old_levels_messages) :=
form_history_proof history_value inbox_value in
let? '(inbox_value, level_tree_history, tree_value, payloads) :=
initialize_level_tree_when_needed level_tree_history inbox_value
level_tree payloads in
let inbox_value :=
{| V1.t.level := new_level;
V1.t.nb_messages_in_commitment_period :=
inbox_value.(V1.t.nb_messages_in_commitment_period);
V1.t.current_level_proof := inbox_value.(V1.t.current_level_proof);
V1.t.old_levels_messages := old_levels_messages; |} in
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads).
Definition add_messages
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
(level : Raw_level_repr.raw_level)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M?
(Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
V1.History.(Bounded_history_repr.S.t) × t) :=
let? '_ :=
Error_monad.error_when
match payloads with
| [] ⇒ true
| _ ⇒ false
end (Build_extensible "Tried_to_add_zero_messages" unit tt) in
let? '_ :=
Error_monad.error_when (Raw_level_repr.op_lt level inbox_value.(V1.t.level))
(Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level) in
let?
'(history_value, inbox_value, level_tree_history, level_tree, payloads) :=
archive_if_needed level_tree_history history_value inbox_value level
level_tree payloads in
let? '(level_tree_history, level_tree, inbox_value) :=
List.fold_left_e
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) ⇒
let '(level_tree_history, level_tree, inbox_value) := function_parameter
in
fun (payload : Sc_rollup_inbox_message_repr.serialized) ⇒
add_message inbox_value payload level_tree_history level_tree)
(level_tree_history, level_tree, inbox_value) payloads in
let current_level_proof (function_parameter : unit) : level_proof :=
let '_ := function_parameter in
let hash_value :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value level_tree in
{| V1.level_proof.hash := hash_value; V1.level_proof.level := level; |} in
return?
(level_tree_history, level_tree, history_value,
(V1.t.with_current_level_proof current_level_proof inbox_value)).
Definition add_messages_no_history
(inbox_value : t) (level : Raw_level_repr.raw_level)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M? (Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
Error_monad.Result_syntax.op_letplus
(add_messages
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.no_history
no_history inbox_value level payloads level_tree)
(fun function_parameter ⇒
let '(_, level_tree, _, inbox_value) := function_parameter in
(level_tree, inbox_value)).
Definition inclusion_proof : Set := list history_proof.
Definition inclusion_proof_encoding
: Data_encoding.encoding (list history_proof) :=
Data_encoding.list_value None history_proof_encoding.
Definition pp_inclusion_proof
(fmt : Format.formatter)
(proof_value : list (Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t))
: unit := Format.pp_print_list None pp_history_proof fmt proof_value.
Definition number_of_proof_steps {A : Set} (proof_value : list A) : int :=
List.length proof_value.
Definition lift_ptr_path {A B : Set} (deref : A → option B) (ptr_path : list A)
: option (list B) :=
let fix aux (accu_value : list B) (function_parameter : list A)
: option (list B) :=
match function_parameter with
| [] ⇒ Some (List.rev accu_value)
| cons x_value xs ⇒
Option.bind (deref x_value)
(fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
end in
aux nil ptr_path.
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
(new_level : Raw_level_repr.raw_level)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
: M?
(V1.History.(Bounded_history_repr.S.t) × t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
list Sc_rollup_inbox_message_repr.serialized) :=
if Raw_level_repr.op_eq inbox_value.(V1.t.level) new_level then
match level_tree with
| Some tree_value ⇒
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads)
| None ⇒
let? '(inbox_value, level_tree_history, tree_value, payloads) :=
initialize_level_tree_when_needed level_tree_history inbox_value
level_tree payloads in
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads)
end
else
let? '(history_value, old_levels_messages) :=
form_history_proof history_value inbox_value in
let? '(inbox_value, level_tree_history, tree_value, payloads) :=
initialize_level_tree_when_needed level_tree_history inbox_value
level_tree payloads in
let inbox_value :=
{| V1.t.level := new_level;
V1.t.nb_messages_in_commitment_period :=
inbox_value.(V1.t.nb_messages_in_commitment_period);
V1.t.current_level_proof := inbox_value.(V1.t.current_level_proof);
V1.t.old_levels_messages := old_levels_messages; |} in
return?
(history_value, inbox_value, level_tree_history, tree_value, payloads).
Definition add_messages
(level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
(level : Raw_level_repr.raw_level)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M?
(Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
V1.History.(Bounded_history_repr.S.t) × t) :=
let? '_ :=
Error_monad.error_when
match payloads with
| [] ⇒ true
| _ ⇒ false
end (Build_extensible "Tried_to_add_zero_messages" unit tt) in
let? '_ :=
Error_monad.error_when (Raw_level_repr.op_lt level inbox_value.(V1.t.level))
(Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level) in
let?
'(history_value, inbox_value, level_tree_history, level_tree, payloads) :=
archive_if_needed level_tree_history history_value inbox_value level
level_tree payloads in
let? '(level_tree_history, level_tree, inbox_value) :=
List.fold_left_e
(fun (function_parameter :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) ⇒
let '(level_tree_history, level_tree, inbox_value) := function_parameter
in
fun (payload : Sc_rollup_inbox_message_repr.serialized) ⇒
add_message inbox_value payload level_tree_history level_tree)
(level_tree_history, level_tree, inbox_value) payloads in
let current_level_proof (function_parameter : unit) : level_proof :=
let '_ := function_parameter in
let hash_value :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value level_tree in
{| V1.level_proof.hash := hash_value; V1.level_proof.level := level; |} in
return?
(level_tree_history, level_tree, history_value,
(V1.t.with_current_level_proof current_level_proof inbox_value)).
Definition add_messages_no_history
(inbox_value : t) (level : Raw_level_repr.raw_level)
(payloads : list Sc_rollup_inbox_message_repr.serialized)
(level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
: M? (Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
Error_monad.Result_syntax.op_letplus
(add_messages
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.no_history
no_history inbox_value level payloads level_tree)
(fun function_parameter ⇒
let '(_, level_tree, _, inbox_value) := function_parameter in
(level_tree, inbox_value)).
Definition inclusion_proof : Set := list history_proof.
Definition inclusion_proof_encoding
: Data_encoding.encoding (list history_proof) :=
Data_encoding.list_value None history_proof_encoding.
Definition pp_inclusion_proof
(fmt : Format.formatter)
(proof_value : list (Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t))
: unit := Format.pp_print_list None pp_history_proof fmt proof_value.
Definition number_of_proof_steps {A : Set} (proof_value : list A) : int :=
List.length proof_value.
Definition lift_ptr_path {A B : Set} (deref : A → option B) (ptr_path : list A)
: option (list B) :=
let fix aux (accu_value : list B) (function_parameter : list A)
: option (list B) :=
match function_parameter with
| [] ⇒ Some (List.rev accu_value)
| cons x_value xs ⇒
Option.bind (deref x_value)
(fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
end in
aux nil ptr_path.
Records for the constructor parameters
Module ConstructorRecords_proof.
Module proof.
Module Single_level.
Record record {inc message_proof : Set} : Set := Build {
inc : inc;
message_proof : message_proof;
}.
Arguments record : clear implicits.
Definition with_inc {t_inc t_message_proof} inc
(r : record t_inc t_message_proof) :=
Build t_inc t_message_proof inc r.(message_proof).
Definition with_message_proof {t_inc t_message_proof} message_proof
(r : record t_inc t_message_proof) :=
Build t_inc t_message_proof r.(inc) message_proof.
End Single_level.
Definition Single_level_skeleton := Single_level.record.
Module Next_level.
Record record {lower_message_proof inc : Set} : Set := Build {
lower_message_proof : lower_message_proof;
inc : inc;
}.
Arguments record : clear implicits.
Definition with_lower_message_proof {t_lower_message_proof t_inc}
lower_message_proof (r : record t_lower_message_proof t_inc) :=
Build t_lower_message_proof t_inc lower_message_proof r.(inc).
Definition with_inc {t_lower_message_proof t_inc} inc
(r : record t_lower_message_proof t_inc) :=
Build t_lower_message_proof t_inc r.(lower_message_proof) inc.
End Next_level.
Definition Next_level_skeleton := Next_level.record.
End proof.
End ConstructorRecords_proof.
Import ConstructorRecords_proof.
Reserved Notation "'proof.Single_level".
Reserved Notation "'proof.Next_level".
Inductive proof : Set :=
| Single_level : 'proof.Single_level → proof
| Next_level : 'proof.Next_level → proof
where "'proof.Single_level" :=
(proof.Single_level_skeleton inclusion_proof level_tree_proof)
and "'proof.Next_level" :=
(proof.Next_level_skeleton level_tree_proof inclusion_proof).
Module proof.
Include ConstructorRecords_proof.proof.
Definition Single_level := 'proof.Single_level.
Definition Next_level := 'proof.Next_level.
End proof.
Definition pp_proof (fmt : Format.formatter) (proof_value : proof) : unit :=
match proof_value with
| Single_level _ ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Single_level inbox proof"
CamlinternalFormatBasics.End_of_format) "Single_level inbox proof")
| Next_level _ ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Next_level inbox proof"
CamlinternalFormatBasics.End_of_format) "Next_level inbox proof")
end.
Definition proof_encoding : Data_encoding.encoding proof :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Single_level" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "inclusion_proof"
inclusion_proof_encoding)
(Data_encoding.req None None "message_proof"
level_tree_proof_encoding))
(fun (function_parameter : proof) ⇒
match function_parameter with
|
Single_level {|
proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof
|} ⇒ Some (inc, message_proof)
| _ ⇒ None
end)
(fun (function_parameter : inclusion_proof × level_tree_proof) ⇒
let '(inc, message_proof) := function_parameter in
Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |});
Data_encoding.case_value "Next_level" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "lower_message_proof"
level_tree_proof_encoding)
(Data_encoding.req None None "inclusion_proof"
inclusion_proof_encoding))
(fun (function_parameter : proof) ⇒
match function_parameter with
|
Next_level {|
proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc
|} ⇒ Some (lower_message_proof, inc)
| _ ⇒ None
end)
(fun (function_parameter : level_tree_proof × inclusion_proof) ⇒
let '(lower_message_proof, inc) := function_parameter in
Next_level
{|
proof.Next_level.lower_message_proof :=
lower_message_proof; proof.Next_level.inc := inc; |})
].
Definition of_serialized_proof : string → option proof :=
Data_encoding.Binary.of_string_opt proof_encoding.
Definition to_serialized_proof : proof → string :=
Data_encoding.Binary.to_string_exn None proof_encoding.
Module proof.
Module Single_level.
Record record {inc message_proof : Set} : Set := Build {
inc : inc;
message_proof : message_proof;
}.
Arguments record : clear implicits.
Definition with_inc {t_inc t_message_proof} inc
(r : record t_inc t_message_proof) :=
Build t_inc t_message_proof inc r.(message_proof).
Definition with_message_proof {t_inc t_message_proof} message_proof
(r : record t_inc t_message_proof) :=
Build t_inc t_message_proof r.(inc) message_proof.
End Single_level.
Definition Single_level_skeleton := Single_level.record.
Module Next_level.
Record record {lower_message_proof inc : Set} : Set := Build {
lower_message_proof : lower_message_proof;
inc : inc;
}.
Arguments record : clear implicits.
Definition with_lower_message_proof {t_lower_message_proof t_inc}
lower_message_proof (r : record t_lower_message_proof t_inc) :=
Build t_lower_message_proof t_inc lower_message_proof r.(inc).
Definition with_inc {t_lower_message_proof t_inc} inc
(r : record t_lower_message_proof t_inc) :=
Build t_lower_message_proof t_inc r.(lower_message_proof) inc.
End Next_level.
Definition Next_level_skeleton := Next_level.record.
End proof.
End ConstructorRecords_proof.
Import ConstructorRecords_proof.
Reserved Notation "'proof.Single_level".
Reserved Notation "'proof.Next_level".
Inductive proof : Set :=
| Single_level : 'proof.Single_level → proof
| Next_level : 'proof.Next_level → proof
where "'proof.Single_level" :=
(proof.Single_level_skeleton inclusion_proof level_tree_proof)
and "'proof.Next_level" :=
(proof.Next_level_skeleton level_tree_proof inclusion_proof).
Module proof.
Include ConstructorRecords_proof.proof.
Definition Single_level := 'proof.Single_level.
Definition Next_level := 'proof.Next_level.
End proof.
Definition pp_proof (fmt : Format.formatter) (proof_value : proof) : unit :=
match proof_value with
| Single_level _ ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Single_level inbox proof"
CamlinternalFormatBasics.End_of_format) "Single_level inbox proof")
| Next_level _ ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Next_level inbox proof"
CamlinternalFormatBasics.End_of_format) "Next_level inbox proof")
end.
Definition proof_encoding : Data_encoding.encoding proof :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Single_level" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "inclusion_proof"
inclusion_proof_encoding)
(Data_encoding.req None None "message_proof"
level_tree_proof_encoding))
(fun (function_parameter : proof) ⇒
match function_parameter with
|
Single_level {|
proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof
|} ⇒ Some (inc, message_proof)
| _ ⇒ None
end)
(fun (function_parameter : inclusion_proof × level_tree_proof) ⇒
let '(inc, message_proof) := function_parameter in
Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |});
Data_encoding.case_value "Next_level" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "lower_message_proof"
level_tree_proof_encoding)
(Data_encoding.req None None "inclusion_proof"
inclusion_proof_encoding))
(fun (function_parameter : proof) ⇒
match function_parameter with
|
Next_level {|
proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc
|} ⇒ Some (lower_message_proof, inc)
| _ ⇒ None
end)
(fun (function_parameter : level_tree_proof × inclusion_proof) ⇒
let '(lower_message_proof, inc) := function_parameter in
Next_level
{|
proof.Next_level.lower_message_proof :=
lower_message_proof; proof.Next_level.inc := inc; |})
].
Definition of_serialized_proof : string → option proof :=
Data_encoding.Binary.of_string_opt proof_encoding.
Definition to_serialized_proof : proof → string :=
Data_encoding.Binary.to_string_exn None proof_encoding.
[verify_level_tree_proof {proof; payload} head_cell_hash n label] handles
all the verification needed for a particular message proof at a particular
level.
First it checks that [proof] is a valid inclusion of [payload_cell] in
[head_cell] and that [head_cell] hash is [head_cell_hash].
Then there is two cases,
- either [n] is superior to the index of [head_cell] then the provided
[payload] must be empty (and [payload_cell = head_cell]);
- or [0 < n < max_index head_cell] then the provided payload must exist and
the payload hash must equal the content of the [payload_cell].
Definition verify_level_tree_proof (function_parameter : level_tree_proof)
: Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t → Z.t → string →
M? (option Sc_rollup_inbox_message_repr.serialized) :=
let '{|
level_tree_proof.proof := proof_value;
level_tree_proof.payload := payload
|} := function_parameter in
fun (head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t)
⇒
fun (n_value : Z.t) ⇒
fun (label : string) ⇒
let? '(payload_cell, head_cell) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.verify_proof
proof_value in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal
head_cell_hash
(Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value
head_cell))
(Build_extensible "Inbox_proof_error" string
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "message_proof ("
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
") does not match history"
CamlinternalFormatBasics.End_of_format)))
"message_proof (%s) does not match history") label)) in
let max_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
if (Z.to_int n_value) >i max_index then
let? '_ :=
Error_monad.error_unless (Option.is_none payload)
(Build_extensible "Inbox_proof_error" string
"Payload provided but none expected") in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_merkelized_payload_hashes_repr.equal payload_cell
head_cell)
(Build_extensible "Inbox_proof_error" string
"Provided proof is about a unexpected payload") in
Error_monad.Result_syntax.return_none
else
let? payload :=
match payload with
| Some payload ⇒ return? payload
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"Expected a payload but none provided in the proof")
end in
let payload_hash :=
Sc_rollup_inbox_message_repr.hash_serialized_message payload in
let proven_payload_hash :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_payload_hash
payload_cell in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_message_repr.Hash.equal payload_hash
proven_payload_hash)
(Build_extensible "Inbox_proof_error" string
"the payload provided does not match the payload's hash found in the message proof")
in
let payload_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index
payload_cell in
let? '_ :=
Error_monad.error_unless
(Compare.Int.equal (Z.to_int n_value) payload_index)
(Build_extensible "Inbox_proof_error" string
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"found index in message_proof ("
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
") is incorrect"
CamlinternalFormatBasics.End_of_format)))
"found index in message_proof (%s) is incorrect") label)) in
Error_monad.Result_syntax.return_some payload.
: Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t → Z.t → string →
M? (option Sc_rollup_inbox_message_repr.serialized) :=
let '{|
level_tree_proof.proof := proof_value;
level_tree_proof.payload := payload
|} := function_parameter in
fun (head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t)
⇒
fun (n_value : Z.t) ⇒
fun (label : string) ⇒
let? '(payload_cell, head_cell) :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.verify_proof
proof_value in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal
head_cell_hash
(Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value
head_cell))
(Build_extensible "Inbox_proof_error" string
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "message_proof ("
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
") does not match history"
CamlinternalFormatBasics.End_of_format)))
"message_proof (%s) does not match history") label)) in
let max_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
if (Z.to_int n_value) >i max_index then
let? '_ :=
Error_monad.error_unless (Option.is_none payload)
(Build_extensible "Inbox_proof_error" string
"Payload provided but none expected") in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_merkelized_payload_hashes_repr.equal payload_cell
head_cell)
(Build_extensible "Inbox_proof_error" string
"Provided proof is about a unexpected payload") in
Error_monad.Result_syntax.return_none
else
let? payload :=
match payload with
| Some payload ⇒ return? payload
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"Expected a payload but none provided in the proof")
end in
let payload_hash :=
Sc_rollup_inbox_message_repr.hash_serialized_message payload in
let proven_payload_hash :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_payload_hash
payload_cell in
let? '_ :=
Error_monad.error_unless
(Sc_rollup_inbox_message_repr.Hash.equal payload_hash
proven_payload_hash)
(Build_extensible "Inbox_proof_error" string
"the payload provided does not match the payload's hash found in the message proof")
in
let payload_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index
payload_cell in
let? '_ :=
Error_monad.error_unless
(Compare.Int.equal (Z.to_int n_value) payload_index)
(Build_extensible "Inbox_proof_error" string
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"found index in message_proof ("
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
") is incorrect"
CamlinternalFormatBasics.End_of_format)))
"found index in message_proof (%s) is incorrect") label)) in
Error_monad.Result_syntax.return_some payload.
[produce_level_tree_proof get_level_tree_history head_cell_hash ~index]
[get_level_tree_history cell_hash] is a function that returns an
{!Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t}. The returned
history must contains the cell with hash [cell_hash], all its ancestor cell
and their associated payload.
[head_cell] the latest cell of the [level_tree] we want to produce a proof on
with hash [head_cell_hash].
This function produce either:
- if [index <= head_cell_max_index], a proof that [payload_cell] with
[index] is an ancestor to [head_cell] where [head_cell] is the cell with
hash [head_cell_hash]. It returns the proof and the payload associated to
[payload_cell];
- else a proof that [index] is out of bound for [head_cell]. It returns the
proof and no payload.
Definition produce_level_tree_proof
(get_level_tree_history :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key →
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key)
(index_value : int) : M? level_tree_proof :=
let level_tree_history := get_level_tree_history head_cell_hash in
let? head_cell :=
match
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.find head_cell_hash
level_tree_history with
|
Some {|
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
:= head_cell;
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
:= _
|} ⇒ return? head_cell
| None ⇒
Error_monad.error_value
(Build_extensible "Inbox_proof_error" string
"could not find head_cell in the level_tree_history")
end in
let head_cell_max_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
let target_index := Compare.Int.min index_value head_cell_max_index in
let proof_value :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.produce_proof
level_tree_history target_index head_cell in
match proof_value with
|
Some
({|
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
:= _;
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
:= payload
|}, proof_value) ⇒
if target_index =i index_value then
return?
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload := Some payload; |}
else
return?
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload := None; |}
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"could not produce a valid proof.")
end.
Axiom verify_inclusion_proof :
inclusion_proof → history_proof → M? history_proof.
Definition verify_proof (function_parameter : Raw_level_repr.t × Z.t)
: history_proof → proof → M? (option Sc_rollup_PVM_sig.inbox_message) :=
let '(l_value, n_value) := function_parameter in
fun (inbox_snapshot : history_proof) ⇒
fun (proof_value : proof) ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Z.geq n_value Z.zero) in
match proof_value with
|
Single_level {|
proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof
|} ⇒
let? history_proof := verify_inclusion_proof inc inbox_snapshot in
let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
let? payload_opt :=
verify_level_tree_proof message_proof
level_proof.(V1.level_proof.hash) n_value "single level" in
match payload_opt with
| None ⇒
if equal_history_proof inbox_snapshot history_proof then
Error_monad.Result_syntax.return_none
else
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"payload is None but proof.level not top level")
| Some payload ⇒
Error_monad.Result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
end
|
Next_level {|
proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc
|} ⇒
let? lower_history_proof := verify_inclusion_proof inc inbox_snapshot in
let lower_level_proof :=
Skip_list.(Skip_list_repr.S.content) lower_history_proof in
let? should_be_none :=
verify_level_tree_proof lower_message_proof
lower_level_proof.(V1.level_proof.hash) n_value "lower" in
match should_be_none with
| None ⇒
let? payload :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) in
let inbox_level := Raw_level_repr.succ l_value in
let message_counter := Z.zero in
Error_monad.Result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter :=
message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
| Some _ ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"more messages to read in current level")
end
end.
Definition produce_proof
(get_level_tree_history :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key →
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t))
(inbox_snapshot : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
(function_parameter : Raw_level_repr.raw_level × Z.t)
: M? (proof × option Sc_rollup_PVM_sig.inbox_message) :=
let '(l_value, n_value) := function_parameter in
let deref (ptr : Hash.H.(S.HASH.t)) : option V1.history_proof :=
History.(Bounded_history_repr.S.find) ptr history_value in
let compare (function_parameter : level_proof) : int :=
let '{| V1.level_proof.hash := _; V1.level_proof.level := level |} :=
function_parameter in
Raw_level_repr.compare level l_value in
let result_value :=
Skip_list.(Skip_list_repr.S.search) deref compare inbox_snapshot in
let? '(inc, history_proof) :=
match result_value with
| {|
Skip_list_repr.search_result.rev_path := rev_path;
Skip_list_repr.search_result.last_cell :=
Skip_list_repr.Found history_proof
|} ⇒ return? ((List.rev rev_path), history_proof)
|
({| Skip_list_repr.search_result.last_cell := Skip_list_repr.Nearest _ |}
| {|
Skip_list_repr.search_result.last_cell := Skip_list_repr.No_exact_or_lower_ptr
|} | {|
Skip_list_repr.search_result.last_cell := Skip_list_repr.Deref_returned_none
|}) ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Skip_list.search failed to find a valid path: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"Skip_list.search failed to find a valid path: %a")
(Skip_list.(Skip_list_repr.S.pp_search_result) pp_history_proof)
result_value))
end in
let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
let?
'{| level_tree_proof.proof := _; level_tree_proof.payload := payload |} as
message_proof :=
produce_level_tree_proof get_level_tree_history
level_proof.(V1.level_proof.hash) (Z.to_int n_value) in
match payload with
| Some payload ⇒
return?
((Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |}),
(Some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}))
| None ⇒
if equal_history_proof inbox_snapshot history_proof then
return?
((Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |}), None)
else
let lower_message_proof := message_proof in
let? input_given :=
let inbox_level := Raw_level_repr.succ l_value in
let message_counter := Z.zero in
let? payload :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) in
Error_monad.Lwt_result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |} in
return?
((Next_level
{| proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc; |}), input_given)
end.
Definition empty (level : Raw_level_repr.t) : t :=
let pre_genesis_level := Raw_level_repr.root_value in
let initial_level_proof :=
let hash_value := Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.zero
in
{| V1.level_proof.hash := hash_value;
V1.level_proof.level := pre_genesis_level; |} in
{| V1.t.level := level; V1.t.nb_messages_in_commitment_period := 0;
V1.t.current_level_proof :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
initial_level_proof;
V1.t.old_levels_messages :=
Skip_list.(Skip_list_repr.S.genesis) initial_level_proof; |}.
Definition inbox : Set := t.
(get_level_tree_history :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key →
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key)
(index_value : int) : M? level_tree_proof :=
let level_tree_history := get_level_tree_history head_cell_hash in
let? head_cell :=
match
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.find head_cell_hash
level_tree_history with
|
Some {|
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
:= head_cell;
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
:= _
|} ⇒ return? head_cell
| None ⇒
Error_monad.error_value
(Build_extensible "Inbox_proof_error" string
"could not find head_cell in the level_tree_history")
end in
let head_cell_max_index :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
let target_index := Compare.Int.min index_value head_cell_max_index in
let proof_value :=
Sc_rollup_inbox_merkelized_payload_hashes_repr.produce_proof
level_tree_history target_index head_cell in
match proof_value with
|
Some
({|
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
:= _;
Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
:= payload
|}, proof_value) ⇒
if target_index =i index_value then
return?
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload := Some payload; |}
else
return?
{| level_tree_proof.proof := proof_value;
level_tree_proof.payload := None; |}
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"could not produce a valid proof.")
end.
Axiom verify_inclusion_proof :
inclusion_proof → history_proof → M? history_proof.
Definition verify_proof (function_parameter : Raw_level_repr.t × Z.t)
: history_proof → proof → M? (option Sc_rollup_PVM_sig.inbox_message) :=
let '(l_value, n_value) := function_parameter in
fun (inbox_snapshot : history_proof) ⇒
fun (proof_value : proof) ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Z.geq n_value Z.zero) in
match proof_value with
|
Single_level {|
proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof
|} ⇒
let? history_proof := verify_inclusion_proof inc inbox_snapshot in
let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
let? payload_opt :=
verify_level_tree_proof message_proof
level_proof.(V1.level_proof.hash) n_value "single level" in
match payload_opt with
| None ⇒
if equal_history_proof inbox_snapshot history_proof then
Error_monad.Result_syntax.return_none
else
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"payload is None but proof.level not top level")
| Some payload ⇒
Error_monad.Result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
end
|
Next_level {|
proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc
|} ⇒
let? lower_history_proof := verify_inclusion_proof inc inbox_snapshot in
let lower_level_proof :=
Skip_list.(Skip_list_repr.S.content) lower_history_proof in
let? should_be_none :=
verify_level_tree_proof lower_message_proof
lower_level_proof.(V1.level_proof.hash) n_value "lower" in
match should_be_none with
| None ⇒
let? payload :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) in
let inbox_level := Raw_level_repr.succ l_value in
let message_counter := Z.zero in
Error_monad.Result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter :=
message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
| Some _ ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
"more messages to read in current level")
end
end.
Definition produce_proof
(get_level_tree_history :
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key →
Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
(history_value : V1.History.(Bounded_history_repr.S.t))
(inbox_snapshot : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
(function_parameter : Raw_level_repr.raw_level × Z.t)
: M? (proof × option Sc_rollup_PVM_sig.inbox_message) :=
let '(l_value, n_value) := function_parameter in
let deref (ptr : Hash.H.(S.HASH.t)) : option V1.history_proof :=
History.(Bounded_history_repr.S.find) ptr history_value in
let compare (function_parameter : level_proof) : int :=
let '{| V1.level_proof.hash := _; V1.level_proof.level := level |} :=
function_parameter in
Raw_level_repr.compare level l_value in
let result_value :=
Skip_list.(Skip_list_repr.S.search) deref compare inbox_snapshot in
let? '(inc, history_proof) :=
match result_value with
| {|
Skip_list_repr.search_result.rev_path := rev_path;
Skip_list_repr.search_result.last_cell :=
Skip_list_repr.Found history_proof
|} ⇒ return? ((List.rev rev_path), history_proof)
|
({| Skip_list_repr.search_result.last_cell := Skip_list_repr.Nearest _ |}
| {|
Skip_list_repr.search_result.last_cell := Skip_list_repr.No_exact_or_lower_ptr
|} | {|
Skip_list_repr.search_result.last_cell := Skip_list_repr.Deref_returned_none
|}) ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Inbox_proof_error" string
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Skip_list.search failed to find a valid path: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"Skip_list.search failed to find a valid path: %a")
(Skip_list.(Skip_list_repr.S.pp_search_result) pp_history_proof)
result_value))
end in
let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
let?
'{| level_tree_proof.proof := _; level_tree_proof.payload := payload |} as
message_proof :=
produce_level_tree_proof get_level_tree_history
level_proof.(V1.level_proof.hash) (Z.to_int n_value) in
match payload with
| Some payload ⇒
return?
((Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |}),
(Some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |}))
| None ⇒
if equal_history_proof inbox_snapshot history_proof then
return?
((Single_level
{| proof.Single_level.inc := inc;
proof.Single_level.message_proof := message_proof; |}), None)
else
let lower_message_proof := message_proof in
let? input_given :=
let inbox_level := Raw_level_repr.succ l_value in
let message_counter := Z.zero in
let? payload :=
Sc_rollup_inbox_message_repr.serialize
(Sc_rollup_inbox_message_repr.Internal
Sc_rollup_inbox_message_repr.Start_of_level) in
Error_monad.Lwt_result_syntax.return_some
{| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload; |} in
return?
((Next_level
{| proof.Next_level.lower_message_proof := lower_message_proof;
proof.Next_level.inc := inc; |}), input_given)
end.
Definition empty (level : Raw_level_repr.t) : t :=
let pre_genesis_level := Raw_level_repr.root_value in
let initial_level_proof :=
let hash_value := Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.zero
in
{| V1.level_proof.hash := hash_value;
V1.level_proof.level := pre_genesis_level; |} in
{| V1.t.level := level; V1.t.nb_messages_in_commitment_period := 0;
V1.t.current_level_proof :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
initial_level_proof;
V1.t.old_levels_messages :=
Skip_list.(Skip_list_repr.S.genesis) initial_level_proof; |}.
Definition inbox : Set := t.