🦏 Sc_rollup_inbox_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
A Merkelized inbox represents a list of available messages. This
list is decomposed into sublist of messages, one for each Tezos
level greater than the level of the Last Cemented Commitment
(LCC).
This module is designed to:
1. give a constant-time access to the number of available messages
;
2. provide a space-efficient representation for proofs of inbox
inclusions (only for inboxes obtained at the end of block
validation) ;
3. offer an efficient function to add a new batch of messages in
the inbox at the current level.
To solve (1), we simply maintain the number of available messages
in a field.
To solve (2), 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 (3), we maintain a separate proof tree C witnessing the
contents of messages of the current level.
The protocol maintains the number of available messages, the
hashes of the head of H, and the root hash of 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 an 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
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.consume_n_messages"
"Internal error: Trying to consume a negative number of messages"
"Sc_rollup_inbox.consume_n_messages must be called with a non negative integer."
None
(Data_encoding.obj1
(Data_encoding.req None None "n" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_number_of_messages_to_consume" then
let n_value := cast int64 payload in
Some n_value
else None
end)
(fun (n_value : int64) ⇒
Build_extensible "Invalid_number_of_messages_to_consume" int64 n_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 proof_hash : Set := Context.Proof.hash.
Definition history_proof_hash : Set := Context.Proof.hash.
Definition history_proof : Set :=
Skip_list.(Skip_list_repr.S.cell) proof_hash history_proof_hash.
Definition equal_history_proof
: Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t →
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t → bool :=
Skip_list.(Skip_list_repr.S.equal) Context_hash.equal Context_hash.equal.
Definition history_proof_encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Context_hash.encoding
Context_hash.encoding.
Definition pp_history_proof
(fmt : Format.formatter)
(cell_value : Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "\n content = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n index = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"\n back_pointers = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n "
CamlinternalFormatBasics.End_of_format)))))))
"\n content = %a\n index = %d\n back_pointers = %a\n ")
Context_hash.pp (Skip_list.(Skip_list_repr.S.content) cell_value)
(Skip_list.(Skip_list_repr.S.index_value) cell_value)
(Format.pp_print_list None Context_hash.pp)
(Skip_list.(Skip_list_repr.S.back_pointers) cell_value).
Module t.
Record record : Set := Build {
rollup : Sc_rollup_repr.t;
level : Raw_level_repr.t;
nb_available_messages : int64;
message_counter : Z.t;
current_messages_hash : unit → Context.Proof.hash;
old_levels_messages : history_proof;
}.
Definition with_rollup rollup (r : record) :=
Build rollup r.(level) r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_level level (r : record) :=
Build r.(rollup) level r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_nb_available_messages nb_available_messages (r : record) :=
Build r.(rollup) r.(level) nb_available_messages r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_message_counter message_counter (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) message_counter
r.(current_messages_hash) r.(old_levels_messages).
Definition with_current_messages_hash current_messages_hash (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
current_messages_hash r.(old_levels_messages).
Definition with_old_levels_messages old_levels_messages (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) old_levels_messages.
End t.
Definition t := t.record.
Definition equal (inbox1 : t) (inbox2 : t) : bool :=
let '{|
t.rollup := rollup;
t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages
|} := inbox1 in
(Sc_rollup_repr.Address.equal rollup inbox2.(t.rollup)) &&
((Raw_level_repr.equal level inbox2.(t.level)) &&
((Compare.Int64.(Compare.S.equal) nb_available_messages
inbox2.(t.nb_available_messages)) &&
((Z.equal message_counter inbox2.(t.message_counter)) &&
((Context_hash.equal (current_messages_hash tt)
(inbox2.(t.current_messages_hash) tt)) &&
(equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))))).
Definition pp (fmt : Format.formatter) (inbox : t) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "\n rollup = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n current messages hash = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n nb_available_messages = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
"\n message_counter = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n old_levels_messages = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n "
CamlinternalFormatBasics.End_of_format)))))))))))))
"\n rollup = %a\n level = %a\n current messages hash = %a\n nb_available_messages = %s\n message_counter = %a\n old_levels_messages = %a\n ")
Sc_rollup_repr.Address.pp inbox.(t.rollup) Raw_level_repr.pp inbox.(t.level)
Context_hash.pp (inbox.(t.current_messages_hash) tt)
(Int64.to_string inbox.(t.nb_available_messages)) Z.pp_print
inbox.(t.message_counter) pp_history_proof inbox.(t.old_levels_messages).
Definition inbox_level (inbox : t) : Raw_level_repr.t := inbox.(t.level).
Definition old_levels_messages_encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Context_hash.encoding
Context_hash.encoding.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.rollup := rollup;
t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
(rollup, message_counter, nb_available_messages, level,
(current_messages_hash tt), old_levels_messages))
(fun (function_parameter :
Sc_rollup_repr.t × Z.t × int64 × Raw_level_repr.t × Context.Proof.hash ×
history_proof) ⇒
let
'(rollup, message_counter, nb_available_messages, level,
current_messages_hash, old_levels_messages) := function_parameter in
{| t.rollup := rollup; t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
current_messages_hash; t.old_levels_messages := old_levels_messages;
|}) None
(Data_encoding.obj6
(Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
(Data_encoding.req None None "message_counter" Data_encoding.n_value)
(Data_encoding.req None None "nb_available_messages"
Data_encoding.int64_value)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "current_messages_hash" Context_hash.encoding)
(Data_encoding.req None None "old_levels_messages"
old_levels_messages_encoding)).
Definition number_of_available_messages (inbox : t) : Z.t :=
Z.of_int64 inbox.(t.nb_available_messages).
Definition no_messages_hash : Context_hash.t :=
Context_hash.hash_bytes None [ Bytes.empty ].
Definition empty (rollup : Sc_rollup_repr.t) (level : Raw_level_repr.t) : t :=
{| t.rollup := rollup; t.level := level; t.nb_available_messages := 0;
t.message_counter := Z.zero;
t.current_messages_hash :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
no_messages_hash;
t.old_levels_messages :=
Skip_list.(Skip_list_repr.S.genesis) no_messages_hash; |}.
Definition consume_n_messages (n_value : int) (function_parameter : t)
: M? (option t) :=
let '{| t.nb_available_messages := nb_available_messages |} as inbox :=
function_parameter in
if n_value <i 0 then
Error_monad.error_value
(Build_extensible "Invalid_number_of_messages_to_consume" int64
(Int64.of_int n_value))
else
if (Int64.of_int n_value) >i64 nb_available_messages then
return? None
else
let nb_available_messages :=
nb_available_messages -i64 (Int64.of_int n_value) in
return? (Some (t.with_nb_available_messages nb_available_messages inbox)).
Definition key_of_message : Z.t → string :=
Data_encoding.Binary.to_string_exn None Data_encoding.z_value.
Module MerkelizedOperations.
Record signature {tree history inclusion_proof : Set} : Set := {
tree := tree;
messages := tree;
message := tree;
history := history;
history_encoding : Data_encoding.t history;
pp_history : Format.formatter → history → unit;
history_at_genesis : int64 → history;
add_messages :
history → t → Raw_level_repr.t → list string → messages →
M? (messages × history × t);
add_messages_no_history :
t → Raw_level_repr.t → list string → messages → M? (messages × t);
get_message : messages → Z.t → option message;
get_message_payload : messages → Z.t → option string;
inclusion_proof := inclusion_proof;
pp_inclusion_proof : Format.formatter → inclusion_proof → unit;
number_of_proof_steps : inclusion_proof → int;
produce_inclusion_proof : history → t → t → option inclusion_proof;
verify_inclusion_proof : inclusion_proof → t → t → bool;
}.
End MerkelizedOperations.
Definition MerkelizedOperations := @MerkelizedOperations.signature.
Arguments MerkelizedOperations {_ _ _}.
Module TREE.
Record signature {t tree : Set} : Set := {
t := t;
tree := tree;
key := list string;
value := bytes;
find : tree → key → option value;
find_tree : tree → key → option tree;
add : tree → key → value → tree;
is_empty : tree → bool;
hash_value : tree → Context_hash.t;
__infer_t : t → unit;
}.
End TREE.
Definition TREE := @TREE.signature.
Arguments TREE {_ _}.
Module MakeHashingScheme.
Class FArgs {P_t P_tree : Set} := {
P : TREE (t := P_t) (tree := P_tree);
}.
Arguments Build_FArgs {_ _}.
Definition Tree `{FArgs} := P.
Definition tree `{FArgs} : Set := P.(TREE.tree).
Definition messages `{FArgs} : Set := tree.
Definition message `{FArgs} : Set := tree.
Definition add_message `{FArgs}
(inbox : t) (payload : string) (messages : P.(TREE.tree))
: P.(TREE.tree) × t :=
let message_index := inbox.(t.message_counter) in
let message_counter := Z.succ inbox.(t.message_counter) in
let key_value := key_of_message message_index in
let nb_available_messages := Int64.succ inbox.(t.nb_available_messages) in
let messages :=
Tree.(TREE.add) messages [ key_value; "payload" ]
(Bytes.of_string payload) in
let inbox :=
t.with_message_counter message_counter
(t.with_nb_available_messages nb_available_messages inbox) in
(messages, inbox).
Definition get_message `{FArgs}
(messages : P.(TREE.tree)) (message_index : Z.t) : option P.(TREE.tree) :=
let key_value := key_of_message message_index in
Tree.(TREE.find_tree) messages [ key_value ].
Definition get_message_payload `{FArgs}
(messages : P.(TREE.tree)) (message_index : Z.t) : option string :=
let key_value := key_of_message message_index in
Error_monad.op_gtpipeeq (Tree.(TREE.find) messages [ key_value; "payload" ])
(Option.map Bytes.to_string).
Definition hash_old_levels_messages `{FArgs}
(cell_value :
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: Context_hash.t :=
let current_messages_hash := 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
(let arg := Context_hash.hash_bytes in
fun (eta : list bytes) ⇒ arg None eta)
(List.map Context_hash.to_bytes
(cons current_messages_hash back_pointers_hashes)).
Definition Int64_map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Module history.
Record record `{FArgs} : Set := Build {
events : Context_hash.Map.(S.INDEXES_MAP.t) history_proof;
sequence : Int64_map.(Map.S.t) Context_hash.t;
bound : int64;
counter : int64;
}.
Definition with_events `{FArgs} events (r : record) :=
Build _ _ _ events r.(sequence) r.(bound) r.(counter).
Definition with_sequence `{FArgs} sequence (r : record) :=
Build _ _ _ r.(events) sequence r.(bound) r.(counter).
Definition with_bound `{FArgs} bound (r : record) :=
Build _ _ _ r.(events) r.(sequence) bound r.(counter).
Definition with_counter `{FArgs} counter (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(bound) counter.
End history.
Definition history `{FArgs} := history.record.
Definition history_encoding `{FArgs} : Data_encoding.encoding history :=
let events_encoding :=
Context_hash.Map.(S.INDEXES_MAP.encoding) history_proof_encoding in
let sequence_encoding :=
Data_encoding.conv
(fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
Int64_map.(Map.S.bindings) m_value)
(List.fold_left
(fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
fun (function_parameter : Int64.t × Context_hash.t) ⇒
let '(k_value, v_value) := function_parameter in
Int64_map.(Map.S.add) k_value v_value m_value)
Int64_map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.int64_value Context_hash.encoding))
in
Data_encoding.conv
(fun (function_parameter : history) ⇒
let '{|
history.events := events;
history.sequence := sequence_value;
history.bound := bound;
history.counter := counter
|} := function_parameter in
(events, sequence_value, bound, counter))
(fun (function_parameter :
Context_hash.Map.(S.INDEXES_MAP.t) history_proof ×
Int64_map.(Map.S.t) Context_hash.t × int64 × int64) ⇒
let '(events, sequence_value, bound, counter) := function_parameter in
{| history.events := events; history.sequence := sequence_value;
history.bound := bound; history.counter := counter; |}) None
(Data_encoding.obj4 (Data_encoding.req None None "events" events_encoding)
(Data_encoding.req None None "sequence" sequence_encoding)
(Data_encoding.req None None "bound" Data_encoding.int64_value)
(Data_encoding.req None None "counter" Data_encoding.int64_value)).
Definition pp_history `{FArgs}
(fmt : Format.formatter) (history_value : history) : unit :=
(fun (bindings :
list
(Context_hash.t ×
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)) ⇒
let pp_binding
(fmt : Format.formatter)
(function_parameter :
Context_hash.t ×
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: unit :=
let '(hash_value, history_proof) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))) "@[%a -> %a@]")
Context_hash.pp hash_value pp_history_proof history_proof in
Format.pp_print_list None pp_binding fmt bindings)
(Context_hash.Map.(S.INDEXES_MAP.bindings) history_value.(history.events)).
Definition history_at_genesis `{FArgs} (bound : int64) : history :=
{| history.events := Context_hash.Map.(S.INDEXES_MAP.empty);
history.sequence := Int64_map.(Map.S.empty); history.bound := bound;
history.counter := 0; |}.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.invalid_level_add_messages"
"Internal error: Trying to add an 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
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_inbox.consume_n_messages"
"Internal error: Trying to consume a negative number of messages"
"Sc_rollup_inbox.consume_n_messages must be called with a non negative integer."
None
(Data_encoding.obj1
(Data_encoding.req None None "n" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_number_of_messages_to_consume" then
let n_value := cast int64 payload in
Some n_value
else None
end)
(fun (n_value : int64) ⇒
Build_extensible "Invalid_number_of_messages_to_consume" int64 n_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 proof_hash : Set := Context.Proof.hash.
Definition history_proof_hash : Set := Context.Proof.hash.
Definition history_proof : Set :=
Skip_list.(Skip_list_repr.S.cell) proof_hash history_proof_hash.
Definition equal_history_proof
: Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t →
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t → bool :=
Skip_list.(Skip_list_repr.S.equal) Context_hash.equal Context_hash.equal.
Definition history_proof_encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Context_hash.encoding
Context_hash.encoding.
Definition pp_history_proof
(fmt : Format.formatter)
(cell_value : Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "\n content = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n index = "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"\n back_pointers = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n "
CamlinternalFormatBasics.End_of_format)))))))
"\n content = %a\n index = %d\n back_pointers = %a\n ")
Context_hash.pp (Skip_list.(Skip_list_repr.S.content) cell_value)
(Skip_list.(Skip_list_repr.S.index_value) cell_value)
(Format.pp_print_list None Context_hash.pp)
(Skip_list.(Skip_list_repr.S.back_pointers) cell_value).
Module t.
Record record : Set := Build {
rollup : Sc_rollup_repr.t;
level : Raw_level_repr.t;
nb_available_messages : int64;
message_counter : Z.t;
current_messages_hash : unit → Context.Proof.hash;
old_levels_messages : history_proof;
}.
Definition with_rollup rollup (r : record) :=
Build rollup r.(level) r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_level level (r : record) :=
Build r.(rollup) level r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_nb_available_messages nb_available_messages (r : record) :=
Build r.(rollup) r.(level) nb_available_messages r.(message_counter)
r.(current_messages_hash) r.(old_levels_messages).
Definition with_message_counter message_counter (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) message_counter
r.(current_messages_hash) r.(old_levels_messages).
Definition with_current_messages_hash current_messages_hash (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
current_messages_hash r.(old_levels_messages).
Definition with_old_levels_messages old_levels_messages (r : record) :=
Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
r.(current_messages_hash) old_levels_messages.
End t.
Definition t := t.record.
Definition equal (inbox1 : t) (inbox2 : t) : bool :=
let '{|
t.rollup := rollup;
t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages
|} := inbox1 in
(Sc_rollup_repr.Address.equal rollup inbox2.(t.rollup)) &&
((Raw_level_repr.equal level inbox2.(t.level)) &&
((Compare.Int64.(Compare.S.equal) nb_available_messages
inbox2.(t.nb_available_messages)) &&
((Z.equal message_counter inbox2.(t.message_counter)) &&
((Context_hash.equal (current_messages_hash tt)
(inbox2.(t.current_messages_hash) tt)) &&
(equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))))).
Definition pp (fmt : Format.formatter) (inbox : t) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "\n rollup = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n level = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n current messages hash = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n nb_available_messages = "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
"\n message_counter = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"\n old_levels_messages = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "\n "
CamlinternalFormatBasics.End_of_format)))))))))))))
"\n rollup = %a\n level = %a\n current messages hash = %a\n nb_available_messages = %s\n message_counter = %a\n old_levels_messages = %a\n ")
Sc_rollup_repr.Address.pp inbox.(t.rollup) Raw_level_repr.pp inbox.(t.level)
Context_hash.pp (inbox.(t.current_messages_hash) tt)
(Int64.to_string inbox.(t.nb_available_messages)) Z.pp_print
inbox.(t.message_counter) pp_history_proof inbox.(t.old_levels_messages).
Definition inbox_level (inbox : t) : Raw_level_repr.t := inbox.(t.level).
Definition old_levels_messages_encoding
: Data_encoding.t
(Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) :=
Skip_list.(Skip_list_repr.S.encoding) Context_hash.encoding
Context_hash.encoding.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.rollup := rollup;
t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages
|} := function_parameter in
(rollup, message_counter, nb_available_messages, level,
(current_messages_hash tt), old_levels_messages))
(fun (function_parameter :
Sc_rollup_repr.t × Z.t × int64 × Raw_level_repr.t × Context.Proof.hash ×
history_proof) ⇒
let
'(rollup, message_counter, nb_available_messages, level,
current_messages_hash, old_levels_messages) := function_parameter in
{| t.rollup := rollup; t.level := level;
t.nb_available_messages := nb_available_messages;
t.message_counter := message_counter;
t.current_messages_hash :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
current_messages_hash; t.old_levels_messages := old_levels_messages;
|}) None
(Data_encoding.obj6
(Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
(Data_encoding.req None None "message_counter" Data_encoding.n_value)
(Data_encoding.req None None "nb_available_messages"
Data_encoding.int64_value)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "current_messages_hash" Context_hash.encoding)
(Data_encoding.req None None "old_levels_messages"
old_levels_messages_encoding)).
Definition number_of_available_messages (inbox : t) : Z.t :=
Z.of_int64 inbox.(t.nb_available_messages).
Definition no_messages_hash : Context_hash.t :=
Context_hash.hash_bytes None [ Bytes.empty ].
Definition empty (rollup : Sc_rollup_repr.t) (level : Raw_level_repr.t) : t :=
{| t.rollup := rollup; t.level := level; t.nb_available_messages := 0;
t.message_counter := Z.zero;
t.current_messages_hash :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
no_messages_hash;
t.old_levels_messages :=
Skip_list.(Skip_list_repr.S.genesis) no_messages_hash; |}.
Definition consume_n_messages (n_value : int) (function_parameter : t)
: M? (option t) :=
let '{| t.nb_available_messages := nb_available_messages |} as inbox :=
function_parameter in
if n_value <i 0 then
Error_monad.error_value
(Build_extensible "Invalid_number_of_messages_to_consume" int64
(Int64.of_int n_value))
else
if (Int64.of_int n_value) >i64 nb_available_messages then
return? None
else
let nb_available_messages :=
nb_available_messages -i64 (Int64.of_int n_value) in
return? (Some (t.with_nb_available_messages nb_available_messages inbox)).
Definition key_of_message : Z.t → string :=
Data_encoding.Binary.to_string_exn None Data_encoding.z_value.
Module MerkelizedOperations.
Record signature {tree history inclusion_proof : Set} : Set := {
tree := tree;
messages := tree;
message := tree;
history := history;
history_encoding : Data_encoding.t history;
pp_history : Format.formatter → history → unit;
history_at_genesis : int64 → history;
add_messages :
history → t → Raw_level_repr.t → list string → messages →
M? (messages × history × t);
add_messages_no_history :
t → Raw_level_repr.t → list string → messages → M? (messages × t);
get_message : messages → Z.t → option message;
get_message_payload : messages → Z.t → option string;
inclusion_proof := inclusion_proof;
pp_inclusion_proof : Format.formatter → inclusion_proof → unit;
number_of_proof_steps : inclusion_proof → int;
produce_inclusion_proof : history → t → t → option inclusion_proof;
verify_inclusion_proof : inclusion_proof → t → t → bool;
}.
End MerkelizedOperations.
Definition MerkelizedOperations := @MerkelizedOperations.signature.
Arguments MerkelizedOperations {_ _ _}.
Module TREE.
Record signature {t tree : Set} : Set := {
t := t;
tree := tree;
key := list string;
value := bytes;
find : tree → key → option value;
find_tree : tree → key → option tree;
add : tree → key → value → tree;
is_empty : tree → bool;
hash_value : tree → Context_hash.t;
__infer_t : t → unit;
}.
End TREE.
Definition TREE := @TREE.signature.
Arguments TREE {_ _}.
Module MakeHashingScheme.
Class FArgs {P_t P_tree : Set} := {
P : TREE (t := P_t) (tree := P_tree);
}.
Arguments Build_FArgs {_ _}.
Definition Tree `{FArgs} := P.
Definition tree `{FArgs} : Set := P.(TREE.tree).
Definition messages `{FArgs} : Set := tree.
Definition message `{FArgs} : Set := tree.
Definition add_message `{FArgs}
(inbox : t) (payload : string) (messages : P.(TREE.tree))
: P.(TREE.tree) × t :=
let message_index := inbox.(t.message_counter) in
let message_counter := Z.succ inbox.(t.message_counter) in
let key_value := key_of_message message_index in
let nb_available_messages := Int64.succ inbox.(t.nb_available_messages) in
let messages :=
Tree.(TREE.add) messages [ key_value; "payload" ]
(Bytes.of_string payload) in
let inbox :=
t.with_message_counter message_counter
(t.with_nb_available_messages nb_available_messages inbox) in
(messages, inbox).
Definition get_message `{FArgs}
(messages : P.(TREE.tree)) (message_index : Z.t) : option P.(TREE.tree) :=
let key_value := key_of_message message_index in
Tree.(TREE.find_tree) messages [ key_value ].
Definition get_message_payload `{FArgs}
(messages : P.(TREE.tree)) (message_index : Z.t) : option string :=
let key_value := key_of_message message_index in
Error_monad.op_gtpipeeq (Tree.(TREE.find) messages [ key_value; "payload" ])
(Option.map Bytes.to_string).
Definition hash_old_levels_messages `{FArgs}
(cell_value :
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: Context_hash.t :=
let current_messages_hash := 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
(let arg := Context_hash.hash_bytes in
fun (eta : list bytes) ⇒ arg None eta)
(List.map Context_hash.to_bytes
(cons current_messages_hash back_pointers_hashes)).
Definition Int64_map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Module history.
Record record `{FArgs} : Set := Build {
events : Context_hash.Map.(S.INDEXES_MAP.t) history_proof;
sequence : Int64_map.(Map.S.t) Context_hash.t;
bound : int64;
counter : int64;
}.
Definition with_events `{FArgs} events (r : record) :=
Build _ _ _ events r.(sequence) r.(bound) r.(counter).
Definition with_sequence `{FArgs} sequence (r : record) :=
Build _ _ _ r.(events) sequence r.(bound) r.(counter).
Definition with_bound `{FArgs} bound (r : record) :=
Build _ _ _ r.(events) r.(sequence) bound r.(counter).
Definition with_counter `{FArgs} counter (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(bound) counter.
End history.
Definition history `{FArgs} := history.record.
Definition history_encoding `{FArgs} : Data_encoding.encoding history :=
let events_encoding :=
Context_hash.Map.(S.INDEXES_MAP.encoding) history_proof_encoding in
let sequence_encoding :=
Data_encoding.conv
(fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
Int64_map.(Map.S.bindings) m_value)
(List.fold_left
(fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
fun (function_parameter : Int64.t × Context_hash.t) ⇒
let '(k_value, v_value) := function_parameter in
Int64_map.(Map.S.add) k_value v_value m_value)
Int64_map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.int64_value Context_hash.encoding))
in
Data_encoding.conv
(fun (function_parameter : history) ⇒
let '{|
history.events := events;
history.sequence := sequence_value;
history.bound := bound;
history.counter := counter
|} := function_parameter in
(events, sequence_value, bound, counter))
(fun (function_parameter :
Context_hash.Map.(S.INDEXES_MAP.t) history_proof ×
Int64_map.(Map.S.t) Context_hash.t × int64 × int64) ⇒
let '(events, sequence_value, bound, counter) := function_parameter in
{| history.events := events; history.sequence := sequence_value;
history.bound := bound; history.counter := counter; |}) None
(Data_encoding.obj4 (Data_encoding.req None None "events" events_encoding)
(Data_encoding.req None None "sequence" sequence_encoding)
(Data_encoding.req None None "bound" Data_encoding.int64_value)
(Data_encoding.req None None "counter" Data_encoding.int64_value)).
Definition pp_history `{FArgs}
(fmt : Format.formatter) (history_value : history) : unit :=
(fun (bindings :
list
(Context_hash.t ×
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)) ⇒
let pp_binding
(fmt : Format.formatter)
(function_parameter :
Context_hash.t ×
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
: unit :=
let '(hash_value, history_proof) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))) "@[%a -> %a@]")
Context_hash.pp hash_value pp_history_proof history_proof in
Format.pp_print_list None pp_binding fmt bindings)
(Context_hash.Map.(S.INDEXES_MAP.bindings) history_value.(history.events)).
Definition history_at_genesis `{FArgs} (bound : int64) : history :=
{| history.events := Context_hash.Map.(S.INDEXES_MAP.empty);
history.sequence := Int64_map.(Map.S.empty); history.bound := bound;
history.counter := 0; |}.
[remember ptr cell history] extends [history] with a new
mapping from [ptr] to [cell]. If [history] is full, the
oldest mapping is removed. If the history bound is less
or equal to zero, then this function returns [history]
untouched.
Definition remember `{FArgs}
(ptr : Context_hash.t) (cell_value : history_proof)
(history_value : history) : history :=
if history_value.(history.bound) ≤i64 0 then
history_value
else
let events :=
Context_hash.Map.(S.INDEXES_MAP.add) ptr cell_value
history_value.(history.events) in
let counter := Int64.succ history_value.(history.counter) in
let history_value :=
{| history.events := events;
history.sequence :=
Int64_map.(Map.S.add) history_value.(history.counter) ptr
history_value.(history.sequence);
history.bound := history_value.(history.bound);
history.counter := counter; |} in
if
Int64.equal history_value.(history.counter)
history_value.(history.bound)
then
match Int64_map.(Map.S.min_binding) history_value.(history.sequence)
with
| None ⇒ history_value
| Some (l_value, h_value) ⇒
let sequence_value :=
Int64_map.(Map.S.remove) l_value history_value.(history.sequence) in
let events := Context_hash.Map.(S.INDEXES_MAP.remove) h_value events
in
{| history.events := events; history.sequence := sequence_value;
history.bound := history_value.(history.bound);
history.counter := Int64.pred history_value.(history.counter); |}
end
else
history_value.
#[bypass_check(guard)]
Definition archive_if_needed `{FArgs}
(history_value : history) (inbox : t)
(target_level : Raw_level_repr.raw_level) : history × t :=
let archive_level (history_value : history) (inbox : t) : history × t :=
let prev_cell := inbox.(t.old_levels_messages) in
let prev_cell_ptr := hash_old_levels_messages prev_cell in
let history_value := remember prev_cell_ptr prev_cell history_value in
let old_levels_messages :=
Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr
(inbox.(t.current_messages_hash) tt) in
let level := Raw_level_repr.succ inbox.(t.level) in
let current_messages_hash (function_parameter : unit) : Context_hash.t :=
let '_ := function_parameter in
no_messages_hash in
let inbox :=
{| t.rollup := inbox.(t.rollup); t.level := level;
t.nb_available_messages := inbox.(t.nb_available_messages);
t.message_counter := Z.zero;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages; |} in
(history_value, inbox) in
let fix aux (function_parameter : history × t) {struct function_parameter}
: history × t :=
let '(history_value, inbox) := function_parameter in
if Raw_level_repr.op_eq inbox.(t.level) target_level then
(history_value, inbox)
else
aux (archive_level history_value inbox) in
aux (history_value, inbox).
Definition add_messages `{FArgs}
(history_value : history) (inbox : t) (level : Raw_level_repr.raw_level)
(payloads : list string) (messages : P.(TREE.tree))
: M? (P.(TREE.tree) × history × t) :=
if Raw_level_repr.op_lt level inbox.(t.level) then
Error_monad.fail
(Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level)
else
let '(history_value, inbox) := archive_if_needed history_value inbox level
in
let? '(messages, inbox) :=
List.fold_left_es
(fun (function_parameter : P.(TREE.tree) × t) ⇒
let '(messages, inbox) := function_parameter in
fun (payload : string) ⇒
Error_monad.op_gtgteq (add_message inbox payload messages)
Error_monad._return) (messages, inbox) payloads in
let current_messages_hash (function_parameter : unit) : Context_hash.t :=
let '_ := function_parameter in
if Tree.(TREE.is_empty) messages then
no_messages_hash
else
Tree.(TREE.hash_value) messages in
return?
(messages, history_value,
(t.with_current_messages_hash current_messages_hash inbox)).
Definition add_messages_no_history `{FArgs}
(inbox : t) (level : Raw_level_repr.raw_level) (payloads : list string)
(messages : P.(TREE.tree)) : M? (P.(TREE.tree) × t) :=
let history_value := history_at_genesis 0 in
let? '(messages, _, inbox) :=
add_messages history_value inbox level payloads messages in
return? (messages, inbox).
Definition inclusion_proof `{FArgs} : Set := list history_proof.
Definition pp_inclusion_proof `{FArgs}
(fmt : Format.formatter)
(proof :
list (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t))
: unit := Format.pp_print_list None pp_history_proof fmt proof.
Definition number_of_proof_steps `{FArgs} {A : Set} (proof : list A) : int :=
List.length proof.
Definition lift_ptr_path `{FArgs} {A B : Set}
(history_value : 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 (history_value x_value)
(fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
end in
aux nil ptr_path.
Definition produce_inclusion_proof `{FArgs}
(history_value : history) (inbox1 : t) (inbox2 : t)
: option (list history_proof) :=
let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
let target_index :=
Skip_list.(Skip_list_repr.S.index_value) inbox1.(t.old_levels_messages) in
let history_value :=
remember cell_ptr inbox2.(t.old_levels_messages) history_value in
let deref (ptr : Context_hash.t) : option history_proof :=
Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr
history_value.(history.events) in
Option.join
(Option.map (lift_ptr_path deref)
(Skip_list.(Skip_list_repr.S.back_path) deref cell_ptr target_index)).
Definition verify_inclusion_proof `{FArgs}
(proof :
list (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t))
(inbox1 : t) (inbox2 : t) : bool :=
let assoc :=
List.map
(fun (c_value :
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) ⇒
((hash_old_levels_messages c_value), c_value)) proof in
let path := Pervasives.fst (List.split assoc) in
let deref :=
let map := Context_hash.Map.(S.INDEXES_MAP.of_seq) (List.to_seq assoc) in
fun (ptr : Context_hash.t) ⇒
Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr map in
let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
let target_ptr := hash_old_levels_messages inbox1.(t.old_levels_messages) in
Skip_list.(Skip_list_repr.S.valid_back_path) Context_hash.equal deref
cell_ptr target_ptr path.
(* MakeHashingScheme *)
Definition functor `{FArgs} :=
{|
MerkelizedOperations.history_encoding := history_encoding;
MerkelizedOperations.pp_history := pp_history;
MerkelizedOperations.history_at_genesis := history_at_genesis;
MerkelizedOperations.add_messages := add_messages;
MerkelizedOperations.add_messages_no_history := add_messages_no_history;
MerkelizedOperations.get_message := get_message;
MerkelizedOperations.get_message_payload := get_message_payload;
MerkelizedOperations.pp_inclusion_proof := pp_inclusion_proof;
MerkelizedOperations.number_of_proof_steps := number_of_proof_steps;
MerkelizedOperations.produce_inclusion_proof := produce_inclusion_proof;
MerkelizedOperations.verify_inclusion_proof := verify_inclusion_proof
|}.
End MakeHashingScheme.
Definition MakeHashingScheme {P_t P_tree : Set}
(P : TREE (t := P_t) (tree := P_tree))
: MerkelizedOperations (tree := P.(TREE.tree)) (history := _)
(inclusion_proof := _) :=
let '_ := MakeHashingScheme.Build_FArgs P in
MakeHashingScheme.functor.
Definition MakeHashingScheme_include :
MerkelizedOperations (tree := Context.tree) (history := _)
(inclusion_proof := _) :=
MakeHashingScheme
(let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let add := Context.Tree.(Context.TREE.add) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let t : Set := Context.t in
let tree : Set := Context.tree in
let value : Set := bytes in
let key : Set := list string in
let __infer_t (function_parameter : t) : unit :=
let '_ := function_parameter in
tt in
{|
TREE.find := find;
TREE.find_tree := find_tree;
TREE.add := add;
TREE.is_empty := is_empty;
TREE.hash_value := hash_value;
TREE.__infer_t := __infer_t
|}).
(ptr : Context_hash.t) (cell_value : history_proof)
(history_value : history) : history :=
if history_value.(history.bound) ≤i64 0 then
history_value
else
let events :=
Context_hash.Map.(S.INDEXES_MAP.add) ptr cell_value
history_value.(history.events) in
let counter := Int64.succ history_value.(history.counter) in
let history_value :=
{| history.events := events;
history.sequence :=
Int64_map.(Map.S.add) history_value.(history.counter) ptr
history_value.(history.sequence);
history.bound := history_value.(history.bound);
history.counter := counter; |} in
if
Int64.equal history_value.(history.counter)
history_value.(history.bound)
then
match Int64_map.(Map.S.min_binding) history_value.(history.sequence)
with
| None ⇒ history_value
| Some (l_value, h_value) ⇒
let sequence_value :=
Int64_map.(Map.S.remove) l_value history_value.(history.sequence) in
let events := Context_hash.Map.(S.INDEXES_MAP.remove) h_value events
in
{| history.events := events; history.sequence := sequence_value;
history.bound := history_value.(history.bound);
history.counter := Int64.pred history_value.(history.counter); |}
end
else
history_value.
#[bypass_check(guard)]
Definition archive_if_needed `{FArgs}
(history_value : history) (inbox : t)
(target_level : Raw_level_repr.raw_level) : history × t :=
let archive_level (history_value : history) (inbox : t) : history × t :=
let prev_cell := inbox.(t.old_levels_messages) in
let prev_cell_ptr := hash_old_levels_messages prev_cell in
let history_value := remember prev_cell_ptr prev_cell history_value in
let old_levels_messages :=
Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr
(inbox.(t.current_messages_hash) tt) in
let level := Raw_level_repr.succ inbox.(t.level) in
let current_messages_hash (function_parameter : unit) : Context_hash.t :=
let '_ := function_parameter in
no_messages_hash in
let inbox :=
{| t.rollup := inbox.(t.rollup); t.level := level;
t.nb_available_messages := inbox.(t.nb_available_messages);
t.message_counter := Z.zero;
t.current_messages_hash := current_messages_hash;
t.old_levels_messages := old_levels_messages; |} in
(history_value, inbox) in
let fix aux (function_parameter : history × t) {struct function_parameter}
: history × t :=
let '(history_value, inbox) := function_parameter in
if Raw_level_repr.op_eq inbox.(t.level) target_level then
(history_value, inbox)
else
aux (archive_level history_value inbox) in
aux (history_value, inbox).
Definition add_messages `{FArgs}
(history_value : history) (inbox : t) (level : Raw_level_repr.raw_level)
(payloads : list string) (messages : P.(TREE.tree))
: M? (P.(TREE.tree) × history × t) :=
if Raw_level_repr.op_lt level inbox.(t.level) then
Error_monad.fail
(Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
level)
else
let '(history_value, inbox) := archive_if_needed history_value inbox level
in
let? '(messages, inbox) :=
List.fold_left_es
(fun (function_parameter : P.(TREE.tree) × t) ⇒
let '(messages, inbox) := function_parameter in
fun (payload : string) ⇒
Error_monad.op_gtgteq (add_message inbox payload messages)
Error_monad._return) (messages, inbox) payloads in
let current_messages_hash (function_parameter : unit) : Context_hash.t :=
let '_ := function_parameter in
if Tree.(TREE.is_empty) messages then
no_messages_hash
else
Tree.(TREE.hash_value) messages in
return?
(messages, history_value,
(t.with_current_messages_hash current_messages_hash inbox)).
Definition add_messages_no_history `{FArgs}
(inbox : t) (level : Raw_level_repr.raw_level) (payloads : list string)
(messages : P.(TREE.tree)) : M? (P.(TREE.tree) × t) :=
let history_value := history_at_genesis 0 in
let? '(messages, _, inbox) :=
add_messages history_value inbox level payloads messages in
return? (messages, inbox).
Definition inclusion_proof `{FArgs} : Set := list history_proof.
Definition pp_inclusion_proof `{FArgs}
(fmt : Format.formatter)
(proof :
list (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t))
: unit := Format.pp_print_list None pp_history_proof fmt proof.
Definition number_of_proof_steps `{FArgs} {A : Set} (proof : list A) : int :=
List.length proof.
Definition lift_ptr_path `{FArgs} {A B : Set}
(history_value : 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 (history_value x_value)
(fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
end in
aux nil ptr_path.
Definition produce_inclusion_proof `{FArgs}
(history_value : history) (inbox1 : t) (inbox2 : t)
: option (list history_proof) :=
let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
let target_index :=
Skip_list.(Skip_list_repr.S.index_value) inbox1.(t.old_levels_messages) in
let history_value :=
remember cell_ptr inbox2.(t.old_levels_messages) history_value in
let deref (ptr : Context_hash.t) : option history_proof :=
Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr
history_value.(history.events) in
Option.join
(Option.map (lift_ptr_path deref)
(Skip_list.(Skip_list_repr.S.back_path) deref cell_ptr target_index)).
Definition verify_inclusion_proof `{FArgs}
(proof :
list (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t))
(inbox1 : t) (inbox2 : t) : bool :=
let assoc :=
List.map
(fun (c_value :
Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) ⇒
((hash_old_levels_messages c_value), c_value)) proof in
let path := Pervasives.fst (List.split assoc) in
let deref :=
let map := Context_hash.Map.(S.INDEXES_MAP.of_seq) (List.to_seq assoc) in
fun (ptr : Context_hash.t) ⇒
Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr map in
let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
let target_ptr := hash_old_levels_messages inbox1.(t.old_levels_messages) in
Skip_list.(Skip_list_repr.S.valid_back_path) Context_hash.equal deref
cell_ptr target_ptr path.
(* MakeHashingScheme *)
Definition functor `{FArgs} :=
{|
MerkelizedOperations.history_encoding := history_encoding;
MerkelizedOperations.pp_history := pp_history;
MerkelizedOperations.history_at_genesis := history_at_genesis;
MerkelizedOperations.add_messages := add_messages;
MerkelizedOperations.add_messages_no_history := add_messages_no_history;
MerkelizedOperations.get_message := get_message;
MerkelizedOperations.get_message_payload := get_message_payload;
MerkelizedOperations.pp_inclusion_proof := pp_inclusion_proof;
MerkelizedOperations.number_of_proof_steps := number_of_proof_steps;
MerkelizedOperations.produce_inclusion_proof := produce_inclusion_proof;
MerkelizedOperations.verify_inclusion_proof := verify_inclusion_proof
|}.
End MakeHashingScheme.
Definition MakeHashingScheme {P_t P_tree : Set}
(P : TREE (t := P_t) (tree := P_tree))
: MerkelizedOperations (tree := P.(TREE.tree)) (history := _)
(inclusion_proof := _) :=
let '_ := MakeHashingScheme.Build_FArgs P in
MakeHashingScheme.functor.
Definition MakeHashingScheme_include :
MerkelizedOperations (tree := Context.tree) (history := _)
(inclusion_proof := _) :=
MakeHashingScheme
(let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let add := Context.Tree.(Context.TREE.add) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let t : Set := Context.t in
let tree : Set := Context.tree in
let value : Set := bytes in
let key : Set := list string in
let __infer_t (function_parameter : t) : unit :=
let '_ := function_parameter in
tt in
{|
TREE.find := find;
TREE.find_tree := find_tree;
TREE.add := add;
TREE.is_empty := is_empty;
TREE.hash_value := hash_value;
TREE.__infer_t := __infer_t
|}).
Inclusion of the module [MakeHashingScheme_include]
Definition tree := MakeHashingScheme_include.(MerkelizedOperations.tree).
Definition messages :=
MakeHashingScheme_include.(MerkelizedOperations.messages).
Definition message := MakeHashingScheme_include.(MerkelizedOperations.message).
Definition history := MakeHashingScheme_include.(MerkelizedOperations.history).
Definition history_encoding :=
MakeHashingScheme_include.(MerkelizedOperations.history_encoding).
Definition pp_history :=
MakeHashingScheme_include.(MerkelizedOperations.pp_history).
Definition history_at_genesis :=
MakeHashingScheme_include.(MerkelizedOperations.history_at_genesis).
Definition add_messages :=
MakeHashingScheme_include.(MerkelizedOperations.add_messages).
Definition add_messages_no_history :=
MakeHashingScheme_include.(MerkelizedOperations.add_messages_no_history).
Definition get_message :=
MakeHashingScheme_include.(MerkelizedOperations.get_message).
Definition get_message_payload :=
MakeHashingScheme_include.(MerkelizedOperations.get_message_payload).
Definition inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.inclusion_proof).
Definition pp_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.pp_inclusion_proof).
Definition number_of_proof_steps :=
MakeHashingScheme_include.(MerkelizedOperations.number_of_proof_steps).
Definition produce_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.produce_inclusion_proof).
Definition verify_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.verify_inclusion_proof).
Definition messages :=
MakeHashingScheme_include.(MerkelizedOperations.messages).
Definition message := MakeHashingScheme_include.(MerkelizedOperations.message).
Definition history := MakeHashingScheme_include.(MerkelizedOperations.history).
Definition history_encoding :=
MakeHashingScheme_include.(MerkelizedOperations.history_encoding).
Definition pp_history :=
MakeHashingScheme_include.(MerkelizedOperations.pp_history).
Definition history_at_genesis :=
MakeHashingScheme_include.(MerkelizedOperations.history_at_genesis).
Definition add_messages :=
MakeHashingScheme_include.(MerkelizedOperations.add_messages).
Definition add_messages_no_history :=
MakeHashingScheme_include.(MerkelizedOperations.add_messages_no_history).
Definition get_message :=
MakeHashingScheme_include.(MerkelizedOperations.get_message).
Definition get_message_payload :=
MakeHashingScheme_include.(MerkelizedOperations.get_message_payload).
Definition inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.inclusion_proof).
Definition pp_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.pp_inclusion_proof).
Definition number_of_proof_steps :=
MakeHashingScheme_include.(MerkelizedOperations.number_of_proof_steps).
Definition produce_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.produce_inclusion_proof).
Definition verify_inclusion_proof :=
MakeHashingScheme_include.(MerkelizedOperations.verify_inclusion_proof).