🐆 Tx_rollup_state_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.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Records for the constructor parameters
Module ConstructorRecords_range.
Module range.
Module Interval.
Record record {oldest newest : Set} : Set := Build {
oldest : oldest;
newest : newest;
}.
Arguments record : clear implicits.
Definition with_oldest {t_oldest t_newest} oldest
(r : record t_oldest t_newest) :=
Build t_oldest t_newest oldest r.(newest).
Definition with_newest {t_oldest t_newest} newest
(r : record t_oldest t_newest) :=
Build t_oldest t_newest r.(oldest) newest.
End Interval.
Definition Interval_skeleton := Interval.record.
Module Empty.
Record record {next : Set} : Set := Build {
next : next;
}.
Arguments record : clear implicits.
Definition with_next {t_next} next (r : record t_next) :=
Build t_next next.
End Empty.
Definition Empty_skeleton := Empty.record.
End range.
End ConstructorRecords_range.
Import ConstructorRecords_range.
Reserved Notation "'range.Interval".
Reserved Notation "'range.Empty".
Inductive range : Set :=
| Interval : 'range.Interval → range
| Empty : 'range.Empty → range
where "'range.Interval" :=
(range.Interval_skeleton Tx_rollup_level_repr.t Tx_rollup_level_repr.t)
and "'range.Empty" := (range.Empty_skeleton Tx_rollup_level_repr.t).
Module range.
Include ConstructorRecords_range.range.
Definition Interval := 'range.Interval.
Definition Empty := 'range.Empty.
End range.
Definition range_newest (function_parameter : range)
: option Tx_rollup_level_repr.t :=
match function_parameter with
| Interval {| range.Interval.newest := newest |} ⇒ Some newest
| _ ⇒ None
end.
Definition range_oldest (function_parameter : range)
: option Tx_rollup_level_repr.t :=
match function_parameter with
| Interval {| range.Interval.oldest := oldest |} ⇒ Some oldest
| _ ⇒ None
end.
Definition extend (function_parameter : range)
: range × Tx_rollup_level_repr.t :=
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒
((Interval
{| range.Interval.oldest := next; range.Interval.newest := next; |}), next)
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
let newest := Tx_rollup_level_repr.succ newest in
((Interval
{| range.Interval.oldest := oldest; range.Interval.newest := newest; |}),
newest)
end.
Definition shrink (function_parameter : range) : M? range :=
match
(function_parameter,
match function_parameter with
|
Interval {|
range.Interval.oldest := oldest;
range.Interval.newest := newest
|} ⇒ Tx_rollup_level_repr.op_lt oldest newest
| _ ⇒ false
end) with
| (Empty _, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "cannot shrink range")
|
(Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |},
true) ⇒
return?
(Interval
{| range.Interval.oldest := Tx_rollup_level_repr.succ oldest;
range.Interval.newest := newest; |})
|
(Interval {| range.Interval.oldest := _; range.Interval.newest := newest |},
_) ⇒
return? (Empty {| range.Empty.next := Tx_rollup_level_repr.succ newest; |})
end.
Definition belongs_to (range_value : range) (level : Tx_rollup_level_repr.level)
: bool :=
match range_value with
| Empty _ ⇒ false
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
(Tx_rollup_level_repr.op_lteq oldest level) &&
(Tx_rollup_level_repr.op_lteq level newest)
end.
Definition right_cut (range_value : range) (level : Tx_rollup_level_repr.level)
: M? range :=
match Tx_rollup_level_repr.pred level with
| None ⇒
return? (Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |})
| Some predecessor ⇒
match
(range_value,
match range_value with
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := _ |}
⇒ belongs_to range_value level
| _ ⇒ false
end) with
|
(Interval {|
range.Interval.oldest := oldest; range.Interval.newest := _ |}, true)
⇒
if Tx_rollup_level_repr.op_lteq oldest predecessor then
return?
(Interval
{| range.Interval.oldest := oldest;
range.Interval.newest := predecessor; |})
else
return? (Empty {| range.Empty.next := level; |})
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "cannot cut range")
end
end.
Definition left_extend {A : Set}
(range_value : range) (level : Tx_rollup_level_repr.t)
: Pervasives.result range A :=
match range_value with
| Interval {| range.Interval.oldest := _; range.Interval.newest := newest |}
⇒
return?
(Interval
{| range.Interval.oldest := level; range.Interval.newest := newest; |})
| Empty {| range.Empty.next := next |} ⇒
let newest := Option.value_value (Tx_rollup_level_repr.pred next) level in
return?
(Interval
{| range.Interval.oldest := level; range.Interval.newest := newest; |})
end.
Definition range_count (function_parameter : range) : int :=
match function_parameter with
| Empty _ ⇒ 0
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
Int32.to_int (Int32.succ (Tx_rollup_level_repr.diff_value newest oldest))
end.
Definition range_encoding : Data_encoding.t range :=
Data_encoding.union None
[
Data_encoding.case_value "empty" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "next" Tx_rollup_level_repr.encoding))
(fun (function_parameter : range) ⇒
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒ Some next
| _ ⇒ None
end)
(fun (next : Tx_rollup_level_repr.level) ⇒
Empty {| range.Empty.next := next; |});
Data_encoding.case_value "interval" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "newest"
Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "oldest"
Tx_rollup_level_repr.encoding))
(fun (function_parameter : range) ⇒
match function_parameter with
|
Interval {|
range.Interval.oldest := oldest;
range.Interval.newest := newest
|} ⇒ Some (newest, oldest)
| _ ⇒ None
end)
(fun (function_parameter :
Tx_rollup_level_repr.level × Tx_rollup_level_repr.level) ⇒
let '(newest, oldest) := function_parameter in
Interval
{| range.Interval.oldest := oldest;
range.Interval.newest := newest; |})
].
Definition pp_range (fmt : Format.formatter) (function_parameter : range)
: unit :=
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "next: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"next: %a") Tx_rollup_level_repr.pp next
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "oldest: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " newest: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"oldest: %a newest: %a") Tx_rollup_level_repr.pp oldest
Tx_rollup_level_repr.pp newest
end.
Definition watermark : Set := option Tx_rollup_level_repr.t.
Definition is_above_watermark
(watermark : option Tx_rollup_level_repr.level)
(level : Tx_rollup_level_repr.level) : bool :=
match watermark with
| Some watermark ⇒ Tx_rollup_level_repr.op_lt watermark level
| None ⇒ true
end.
Definition make_watermark {A : Set} (level : A) : option A := Some level.
Module range.
Module Interval.
Record record {oldest newest : Set} : Set := Build {
oldest : oldest;
newest : newest;
}.
Arguments record : clear implicits.
Definition with_oldest {t_oldest t_newest} oldest
(r : record t_oldest t_newest) :=
Build t_oldest t_newest oldest r.(newest).
Definition with_newest {t_oldest t_newest} newest
(r : record t_oldest t_newest) :=
Build t_oldest t_newest r.(oldest) newest.
End Interval.
Definition Interval_skeleton := Interval.record.
Module Empty.
Record record {next : Set} : Set := Build {
next : next;
}.
Arguments record : clear implicits.
Definition with_next {t_next} next (r : record t_next) :=
Build t_next next.
End Empty.
Definition Empty_skeleton := Empty.record.
End range.
End ConstructorRecords_range.
Import ConstructorRecords_range.
Reserved Notation "'range.Interval".
Reserved Notation "'range.Empty".
Inductive range : Set :=
| Interval : 'range.Interval → range
| Empty : 'range.Empty → range
where "'range.Interval" :=
(range.Interval_skeleton Tx_rollup_level_repr.t Tx_rollup_level_repr.t)
and "'range.Empty" := (range.Empty_skeleton Tx_rollup_level_repr.t).
Module range.
Include ConstructorRecords_range.range.
Definition Interval := 'range.Interval.
Definition Empty := 'range.Empty.
End range.
Definition range_newest (function_parameter : range)
: option Tx_rollup_level_repr.t :=
match function_parameter with
| Interval {| range.Interval.newest := newest |} ⇒ Some newest
| _ ⇒ None
end.
Definition range_oldest (function_parameter : range)
: option Tx_rollup_level_repr.t :=
match function_parameter with
| Interval {| range.Interval.oldest := oldest |} ⇒ Some oldest
| _ ⇒ None
end.
Definition extend (function_parameter : range)
: range × Tx_rollup_level_repr.t :=
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒
((Interval
{| range.Interval.oldest := next; range.Interval.newest := next; |}), next)
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
let newest := Tx_rollup_level_repr.succ newest in
((Interval
{| range.Interval.oldest := oldest; range.Interval.newest := newest; |}),
newest)
end.
Definition shrink (function_parameter : range) : M? range :=
match
(function_parameter,
match function_parameter with
|
Interval {|
range.Interval.oldest := oldest;
range.Interval.newest := newest
|} ⇒ Tx_rollup_level_repr.op_lt oldest newest
| _ ⇒ false
end) with
| (Empty _, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "cannot shrink range")
|
(Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |},
true) ⇒
return?
(Interval
{| range.Interval.oldest := Tx_rollup_level_repr.succ oldest;
range.Interval.newest := newest; |})
|
(Interval {| range.Interval.oldest := _; range.Interval.newest := newest |},
_) ⇒
return? (Empty {| range.Empty.next := Tx_rollup_level_repr.succ newest; |})
end.
Definition belongs_to (range_value : range) (level : Tx_rollup_level_repr.level)
: bool :=
match range_value with
| Empty _ ⇒ false
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
(Tx_rollup_level_repr.op_lteq oldest level) &&
(Tx_rollup_level_repr.op_lteq level newest)
end.
Definition right_cut (range_value : range) (level : Tx_rollup_level_repr.level)
: M? range :=
match Tx_rollup_level_repr.pred level with
| None ⇒
return? (Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |})
| Some predecessor ⇒
match
(range_value,
match range_value with
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := _ |}
⇒ belongs_to range_value level
| _ ⇒ false
end) with
|
(Interval {|
range.Interval.oldest := oldest; range.Interval.newest := _ |}, true)
⇒
if Tx_rollup_level_repr.op_lteq oldest predecessor then
return?
(Interval
{| range.Interval.oldest := oldest;
range.Interval.newest := predecessor; |})
else
return? (Empty {| range.Empty.next := level; |})
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "cannot cut range")
end
end.
Definition left_extend {A : Set}
(range_value : range) (level : Tx_rollup_level_repr.t)
: Pervasives.result range A :=
match range_value with
| Interval {| range.Interval.oldest := _; range.Interval.newest := newest |}
⇒
return?
(Interval
{| range.Interval.oldest := level; range.Interval.newest := newest; |})
| Empty {| range.Empty.next := next |} ⇒
let newest := Option.value_value (Tx_rollup_level_repr.pred next) level in
return?
(Interval
{| range.Interval.oldest := level; range.Interval.newest := newest; |})
end.
Definition range_count (function_parameter : range) : int :=
match function_parameter with
| Empty _ ⇒ 0
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
Int32.to_int (Int32.succ (Tx_rollup_level_repr.diff_value newest oldest))
end.
Definition range_encoding : Data_encoding.t range :=
Data_encoding.union None
[
Data_encoding.case_value "empty" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "next" Tx_rollup_level_repr.encoding))
(fun (function_parameter : range) ⇒
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒ Some next
| _ ⇒ None
end)
(fun (next : Tx_rollup_level_repr.level) ⇒
Empty {| range.Empty.next := next; |});
Data_encoding.case_value "interval" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "newest"
Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "oldest"
Tx_rollup_level_repr.encoding))
(fun (function_parameter : range) ⇒
match function_parameter with
|
Interval {|
range.Interval.oldest := oldest;
range.Interval.newest := newest
|} ⇒ Some (newest, oldest)
| _ ⇒ None
end)
(fun (function_parameter :
Tx_rollup_level_repr.level × Tx_rollup_level_repr.level) ⇒
let '(newest, oldest) := function_parameter in
Interval
{| range.Interval.oldest := oldest;
range.Interval.newest := newest; |})
].
Definition pp_range (fmt : Format.formatter) (function_parameter : range)
: unit :=
match function_parameter with
| Empty {| range.Empty.next := next |} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "next: "
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
"next: %a") Tx_rollup_level_repr.pp next
|
Interval {|
range.Interval.oldest := oldest; range.Interval.newest := newest |} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "oldest: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " newest: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"oldest: %a newest: %a") Tx_rollup_level_repr.pp oldest
Tx_rollup_level_repr.pp newest
end.
Definition watermark : Set := option Tx_rollup_level_repr.t.
Definition is_above_watermark
(watermark : option Tx_rollup_level_repr.level)
(level : Tx_rollup_level_repr.level) : bool :=
match watermark with
| Some watermark ⇒ Tx_rollup_level_repr.op_lt watermark level
| None ⇒ true
end.
Definition make_watermark {A : Set} (level : A) : option A := Some level.
The state of a transaction rollup is composed of [burn_per_byte]
and [inbox_ema] fields. [initial_state] introduces their initial
values. Both values are updated by [update_burn_per_byte] as the
rollup progresses.
[burn_per_byte] state the cost of burn per byte to be paid for
each byte submitted to a transaction rollup inbox. [inbox_ema]
is a key factor to impact the update of [burn_per_byte].
[inbox_ema] is the N-block EMA to react to recent N-inbox size
changes. N-block EMA is an exponential moving average (EMA), that
is a type of moving average that places a greater weight and
significance on the most N data points. The purpose of [inbox_ema]
is to get lessened volatility of burn, that is more resistant to
spurious spikes of [burn_per_byte].
The state of the transaction rollup also keeps track of four pointers
to four different rollup levels.
- The [commitment_oldest_level] is the level of the oldest
finalized commitment still stored in the layer-1 storage.
- The [commitment_newest_level] is the level of the most recent
unfinalized commitment in the layer-1 storage.
- The [oldest_inbox_level] is the level of the oldest inbox still stored
in the layer-1 storage.
- The [newest_level] is the level of the most recent inbox in the
layer-1 storage.
Module t.
Record record : Set := Build {
last_removed_commitment_hashes :
option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t);
finalized_commitments : range;
unfinalized_commitments : range;
uncommitted_inboxes : range;
commitment_newest_hash : option Tx_rollup_commitment_repr.Hash.t;
tezos_head_level : option Raw_level_repr.t;
burn_per_byte : Tez_repr.t;
inbox_ema : int;
allocated_storage : Z.t;
occupied_storage : Z.t;
commitments_watermark : watermark;
}.
Definition with_last_removed_commitment_hashes last_removed_commitment_hashes
(r : record) :=
Build last_removed_commitment_hashes r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_finalized_commitments finalized_commitments (r : record) :=
Build r.(last_removed_commitment_hashes) finalized_commitments
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_unfinalized_commitments unfinalized_commitments
(r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
unfinalized_commitments r.(uncommitted_inboxes) r.(commitment_newest_hash)
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_uncommitted_inboxes uncommitted_inboxes (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) uncommitted_inboxes r.(commitment_newest_hash)
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_commitment_newest_hash commitment_newest_hash (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes) commitment_newest_hash
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_tezos_head_level tezos_head_level (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) tezos_head_level r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_burn_per_byte burn_per_byte (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) burn_per_byte
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_inbox_ema inbox_ema (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
inbox_ema r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_allocated_storage allocated_storage (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) allocated_storage r.(occupied_storage)
r.(commitments_watermark).
Definition with_occupied_storage occupied_storage (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) occupied_storage
r.(commitments_watermark).
Definition with_commitments_watermark commitments_watermark (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
commitments_watermark.
End t.
Definition t := t.record.
Definition initial_state (pre_allocated_storage : Z.t) : t :=
{| t.last_removed_commitment_hashes := None;
t.finalized_commitments :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.unfinalized_commitments :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.uncommitted_inboxes :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.commitment_newest_hash := None; t.tezos_head_level := None;
t.burn_per_byte := Tez_repr.zero; t.inbox_ema := 0;
t.allocated_storage := pre_allocated_storage; t.occupied_storage := Z.zero;
t.commitments_watermark := None; |}.
Definition encoding : Data_encoding.t t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte;
t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark
|} := function_parameter in
((last_removed_commitment_hashes, finalized_commitments,
unfinalized_commitments, uncommitted_inboxes, commitment_newest_hash,
tezos_head_level, burn_per_byte, allocated_storage, occupied_storage,
inbox_ema), commitments_watermark))
(fun (function_parameter :
(option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t)
× range × range × range × option Tx_rollup_commitment_repr.Hash.t ×
option Raw_level_repr.t × Tez_repr.t × Z.t × Z.t × int) × watermark) ⇒
let
'((last_removed_commitment_hashes, finalized_commitments,
unfinalized_commitments, uncommitted_inboxes, commitment_newest_hash,
tezos_head_level, burn_per_byte, allocated_storage, occupied_storage,
inbox_ema), commitments_watermark) := function_parameter in
{| t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte; t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark; |}) None
(Data_encoding.merge_objs
(Data_encoding.obj10
(Data_encoding.req None None "last_removed_commitment_hashes"
(Data_encoding.option_value
(Data_encoding.obj2
(Data_encoding.req None None "last_message_hash"
Tx_rollup_message_result_hash_repr.encoding)
(Data_encoding.req None None "commitment_hash"
Tx_rollup_commitment_repr.Hash.encoding))))
(Data_encoding.req None None "finalized_commitments" range_encoding)
(Data_encoding.req None None "unfinalized_commitments" range_encoding)
(Data_encoding.req None None "uncommitted_inboxes" range_encoding)
(Data_encoding.req None None "commitment_newest_hash"
(Data_encoding.option_value Tx_rollup_commitment_repr.Hash.encoding))
(Data_encoding.req None None "tezos_head_level"
(Data_encoding.option_value Raw_level_repr.encoding))
(Data_encoding.req None None "burn_per_byte" Tez_repr.encoding)
(Data_encoding.req None None "allocated_storage" Data_encoding.n_value)
(Data_encoding.req None None "occupied_storage" Data_encoding.n_value)
(Data_encoding.req None None "inbox_ema" Data_encoding.int31))
(Data_encoding.obj1
(Data_encoding.req None None "commitments_watermark"
(Data_encoding.option_value Tx_rollup_level_repr.encoding)))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte;
t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "cost_per_byte: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " inbox_ema: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" finalized_commitments: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" unfinalized_commitments: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" uncommitted_inboxes: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" commitment_newest_hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" tezos_head_level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" last_removed_commitment_hashes: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" allocated_storage: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" occupied_storage: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" commitments_watermark: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))))))))))))))))))
"cost_per_byte: %a inbox_ema: %d finalized_commitments: %a unfinalized_commitments: %a uncommitted_inboxes: %a commitment_newest_hash: %a tezos_head_level: %a last_removed_commitment_hashes: %a allocated_storage: %a occupied_storage: %a commitments_watermark: %a")
Tez_repr.pp burn_per_byte inbox_ema pp_range finalized_commitments pp_range
unfinalized_commitments pp_range uncommitted_inboxes
(Format.pp_print_option None Tx_rollup_commitment_repr.Hash.pp)
commitment_newest_hash (Format.pp_print_option None Raw_level_repr.pp)
tezos_head_level
(Format.pp_print_option None
(fun (fmt : Format.formatter) ⇒
fun (function_parameter :
Tx_rollup_message_result_hash_repr.t ×
Tx_rollup_commitment_repr.Hash.t) ⇒
let '(m_value, c_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "(message result: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", commitment: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"(message result: %a, commitment: %a)")
Tx_rollup_message_result_hash_repr.pp m_value
Tx_rollup_commitment_repr.Hash.pp c_value))
last_removed_commitment_hashes Z.pp_print allocated_storage Z.pp_print
occupied_storage (Format.pp_print_option None Tx_rollup_level_repr.pp)
commitments_watermark.
Definition adjust_storage_allocation (state_value : t) (delta : Z.t)
: M? (t × Z.t) :=
if Z.equal Z.zero delta then
return? (state_value, Z.zero)
else
let occupied_storage' := state_value.(t.occupied_storage) +Z delta in
if occupied_storage' <Z Z.zero then
Error_monad.error_value
(Build_extensible "Internal_error" string
"Storage size should be positive after occupied space is freed.")
else
let diff_value := occupied_storage' -Z state_value.(t.allocated_storage)
in
if diff_value >Z Z.zero then
let state_value :=
t.with_occupied_storage occupied_storage'
(t.with_allocated_storage occupied_storage' state_value) in
return? (state_value, diff_value)
else
let state_value := t.with_occupied_storage occupied_storage' state_value
in
return? (state_value, Z.zero).
Definition update_burn_per_byte_helper (function_parameter : t)
: int → int → int → t :=
let
'{| t.burn_per_byte := burn_per_byte; t.inbox_ema := inbox_ema |} as
state_value := function_parameter in
fun (factor : int) ⇒
fun (final_size : int) ⇒
fun (hard_limit : int) ⇒
let threshold_increase := 90 in
let threshold_decrease := 80 in
let variation_factor := 5 in
let smoothing := 2 in
let inbox_ema :=
inbox_ema +i
(((final_size -i inbox_ema) ×i smoothing) /i (1 +i factor)) in
let percentage := (inbox_ema ×i 100) /i hard_limit in
let computation :=
if
(threshold_decrease <i percentage) &&
(percentage ≤i threshold_increase)
then
return? burn_per_byte
else
let? variation :=
let? x_value :=
Tez_repr.op_starquestion burn_per_byte variation_factor in
Tez_repr.op_divquestion x_value 100 in
let variation :=
if Tez_repr.op_eq variation Tez_repr.zero then
Tez_repr.one_mutez
else
variation in
if threshold_increase <i percentage then
Tez_repr.op_plusquestion burn_per_byte variation
else
if
(percentage <i threshold_decrease) &&
(Tez_repr.op_lt Tez_repr.zero burn_per_byte)
then
Tez_repr.op_minusquestion burn_per_byte variation
else
return? burn_per_byte in
match computation with
| Pervasives.Ok burn_per_byte ⇒
t.with_inbox_ema inbox_ema
(t.with_burn_per_byte burn_per_byte state_value)
| Pervasives.Error _ ⇒
t.with_inbox_ema inbox_ema
(t.with_burn_per_byte Tez_repr.max_mutez state_value)
end.
#[bypass_check(guard)]
Fixpoint update_burn_per_byte
(state_value : t) (elapsed : int) (factor : int) (final_size : int)
(hard_limit : int) {struct elapsed} : t :=
if elapsed >i factor then
t.with_inbox_ema 0 (t.with_burn_per_byte Tez_repr.zero state_value)
else
if elapsed ≤i 0 then
update_burn_per_byte_helper state_value factor final_size hard_limit
else
let state' := update_burn_per_byte_helper state_value factor 0 hard_limit
in
let elapsed := elapsed -i 1 in
update_burn_per_byte state' elapsed factor final_size hard_limit.
Definition has_valid_commitment_at (function_parameter : t)
: Tx_rollup_level_repr.level → bool :=
let '{|
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments
|} := function_parameter in
fun (level : Tx_rollup_level_repr.level) ⇒
(belongs_to finalized_commitments level) ||
(belongs_to unfinalized_commitments level).
Definition inboxes_count (function_parameter : t) : int :=
let '{|
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes
|} := function_parameter in
(range_count unfinalized_commitments) +i (range_count uncommitted_inboxes).
Definition uncommitted_inboxes_count (function_parameter : t) : int :=
let '{| t.uncommitted_inboxes := uncommitted_inboxes |} := function_parameter
in
range_count uncommitted_inboxes.
Definition commitments_count (function_parameter : t) : int :=
let '{|
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments
|} := function_parameter in
(range_count unfinalized_commitments) +i (range_count finalized_commitments).
Definition record_inbox_creation
(t_value : t) (level : Raw_level_repr.raw_level)
: M? (t × Tx_rollup_level_repr.t × Z.t) :=
let? '_ :=
match t_value.(t.tezos_head_level) with
| Some tezos_lvl ⇒
Error_monad.error_when (Raw_level_repr.op_lteq level tezos_lvl)
(Build_extensible "Internal_error" string
"Trying to create an inbox in the past")
| None ⇒ return? tt
end in
let '(uncommitted_inboxes, new_level) :=
extend t_value.(t.uncommitted_inboxes) in
let? '(t_value, diff_value) :=
adjust_storage_allocation t_value Tx_rollup_inbox_repr.size_value in
return?
((t.with_tezos_head_level (Some level)
(t.with_uncommitted_inboxes uncommitted_inboxes t_value)), new_level,
diff_value).
Definition next_commitment_predecessor (state_value : t)
: option Tx_rollup_commitment_repr.Hash.t :=
state_value.(t.commitment_newest_hash).
Definition finalized_commitment_oldest_level (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.finalized_commitments).
Definition next_commitment_level
(state_value : t) (current_level : Raw_level_repr.raw_level)
: M? Tx_rollup_level_repr.t :=
match
((range_oldest state_value.(t.uncommitted_inboxes)),
(range_newest state_value.(t.uncommitted_inboxes))) with
| (Some oldest_level, Some newest_level) ⇒
if Tx_rollup_level_repr.op_lt oldest_level newest_level then
return? oldest_level
else
match state_value.(t.tezos_head_level) with
| Some newest_inbox_creation ⇒
let? '_ :=
Error_monad.error_when
(Raw_level_repr.op_lteq current_level newest_inbox_creation)
(Build_extensible "No_uncommitted_inbox" unit tt) in
return? oldest_level
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"tezos_head_level was not properly set")
end
| (None, None) ⇒
Error_monad.error_value (Build_extensible "No_uncommitted_inbox" unit tt)
| ((Some _, None) | (None, Some _)) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "rollup state is inconsistent")
end.
Definition next_commitment_to_finalize (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.unfinalized_commitments).
Definition next_commitment_to_remove (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.finalized_commitments).
Definition record_inbox_deletion
(state_value : t) (candidate : Tx_rollup_level_repr.level) : M? t :=
match
((range_oldest state_value.(t.unfinalized_commitments)),
match range_oldest state_value.(t.unfinalized_commitments) with
| Some level ⇒ Tx_rollup_level_repr.op_eq candidate level
| _ ⇒ false
end) with
| (Some level, true) ⇒
let? unfinalized_commitments :=
shrink state_value.(t.unfinalized_commitments) in
let '(finalized_commitments, _) :=
extend state_value.(t.finalized_commitments) in
return?
(t.with_unfinalized_commitments unfinalized_commitments
(t.with_finalized_commitments finalized_commitments state_value))
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Trying to delete the wrong inbox")
end.
Definition record_commitment_creation
(state_value : t) (level : Tx_rollup_level_repr.level)
(hash_value : Tx_rollup_commitment_repr.Hash.t) : M? t :=
match range_oldest state_value.(t.uncommitted_inboxes) with
| Some oldest ⇒
let? '_ :=
Error_monad.error_unless (Tx_rollup_level_repr.op_eq level oldest)
(Build_extensible "Internal_error" string
"Trying to create the wrong commitment") in
let? uncommitted_inboxes := shrink state_value.(t.uncommitted_inboxes) in
let '(unfinalized_commitments, _) :=
extend state_value.(t.unfinalized_commitments) in
let state_value :=
t.with_commitment_newest_hash (Some hash_value)
(t.with_uncommitted_inboxes uncommitted_inboxes
(t.with_unfinalized_commitments unfinalized_commitments state_value))
in
if is_above_watermark state_value.(t.commitments_watermark) level then
let? '(state_value, _) :=
adjust_storage_allocation state_value
(Z.neg Tx_rollup_inbox_repr.size_value) in
return? (t.with_commitments_watermark (make_watermark level) state_value)
else
return? state_value
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Cannot create a commitment due to lack of inbox")
end.
Definition record_commitment_rejection
(state_value : t) (level : Tx_rollup_level_repr.t)
(predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) : M? t :=
let unwrap_option {A : Set} (msg : string) (function_parameter : option A)
: M? A :=
match function_parameter with
| Some x_value ⇒ return? x_value
| _ ⇒
Error_monad.error_value (Build_extensible "Internal_error" string msg)
end in
let check_none {A : Set} (msg : string) (function_parameter : option A)
: M? unit :=
match function_parameter with
| None ⇒ return? tt
| Some _ ⇒
Error_monad.error_value (Build_extensible "Internal_error" string msg)
end in
let? uncommitted_inboxes :=
left_extend state_value.(t.uncommitted_inboxes) level in
let state_value := t.with_uncommitted_inboxes uncommitted_inboxes state_value
in
let? unfinalized_commitments :=
right_cut state_value.(t.unfinalized_commitments) level in
match
((Tx_rollup_level_repr.pred level),
match Tx_rollup_level_repr.pred level with
| Some pred_level ⇒
(belongs_to state_value.(t.unfinalized_commitments) pred_level) ||
(belongs_to state_value.(t.finalized_commitments) pred_level)
| _ ⇒ false
end) with
| (Some pred_level, true) ⇒
let? predecessor_hash :=
unwrap_option "Missing predecessor commitment" predecessor_hash in
return?
(t.with_commitment_newest_hash (Some predecessor_hash)
(t.with_unfinalized_commitments unfinalized_commitments state_value))
| (Some _, _) ⇒
let? '_ := check_none "Unexpected predecessor hash" predecessor_hash in
let? '(_, pred_hash) :=
unwrap_option "Missing commitment hash"
state_value.(t.last_removed_commitment_hashes) in
return?
(t.with_commitment_newest_hash (Some pred_hash)
(t.with_unfinalized_commitments unfinalized_commitments state_value))
| (None, _) ⇒
return?
(t.with_commitment_newest_hash None
(t.with_unfinalized_commitments unfinalized_commitments state_value))
end.
Definition record_commitment_deletion
(state_value : t) (level : Tx_rollup_level_repr.level)
(hash_value : Tx_rollup_commitment_repr.Hash.t)
(message_hash : Tx_rollup_message_result_hash_repr.t) : M? t :=
match
((range_oldest state_value.(t.finalized_commitments)),
match range_oldest state_value.(t.finalized_commitments) with
| Some oldest ⇒ Tx_rollup_level_repr.op_eq level oldest
| _ ⇒ false
end) with
| (Some oldest, true) ⇒
let? finalized_commitments := shrink state_value.(t.finalized_commitments)
in
return?
(t.with_finalized_commitments finalized_commitments
(t.with_last_removed_commitment_hashes (Some (message_hash, hash_value))
state_value))
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Trying to remove an incorrect commitment")
end.
Definition burn_cost
(limit : option Tez_repr.t) (state_value : t) (size_value : int)
: M? Tez_repr.t :=
let? burn :=
Tez_repr.op_starquestion state_value.(t.burn_per_byte)
(Int64.of_int size_value) in
match
(limit,
match limit with
| Some limit ⇒ Tez_repr.op_gteq limit burn
| _ ⇒ false
end) with
| (Some limit, true) ⇒
Error_monad.error_value
(Build_extensible "Submit_batch_burn_exceeded"
Tx_rollup_errors_repr.Submit_batch_burn_exceeded
{| Tx_rollup_errors_repr.Submit_batch_burn_exceeded.burn := burn;
Tx_rollup_errors_repr.Submit_batch_burn_exceeded.limit := limit; |})
| (_, _) ⇒ return? burn
end.
Definition finalized_commitments_range (state_value : t)
: option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t) :=
match
((range_oldest state_value.(t.finalized_commitments)),
(range_newest state_value.(t.finalized_commitments))) with
| (Some oldest, Some newest) ⇒ Some (oldest, newest)
| _ ⇒ None
end.
Definition check_level_can_be_rejected
(state_value : t) (level : Tx_rollup_level_repr.level) : M? unit :=
match
((range_oldest state_value.(t.unfinalized_commitments)),
(range_newest state_value.(t.unfinalized_commitments))) with
| (Some oldest, Some newest) ⇒
Error_monad.error_unless
((Tx_rollup_level_repr.op_lteq oldest level) &&
(Tx_rollup_level_repr.op_lteq level newest))
(Build_extensible "Cannot_reject_level"
Tx_rollup_errors_repr.Cannot_reject_level
{| Tx_rollup_errors_repr.Cannot_reject_level.provided := level;
Tx_rollup_errors_repr.Cannot_reject_level.accepted_range :=
Some (oldest, newest); |})
| _ ⇒
Error_monad.error_value
(Build_extensible "Cannot_reject_level"
Tx_rollup_errors_repr.Cannot_reject_level
{| Tx_rollup_errors_repr.Cannot_reject_level.provided := level;
Tx_rollup_errors_repr.Cannot_reject_level.accepted_range := None; |})
end.
Definition last_removed_commitment_hashes (state_value : t)
: option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t) :=
state_value.(t.last_removed_commitment_hashes).
Definition head_levels (state_value : t)
: option (Tx_rollup_level_repr.level × Raw_level_repr.t) :=
match (state_value.(t.uncommitted_inboxes), state_value.(t.tezos_head_level))
with
| (Empty {| range.Empty.next := l_value |}, Some tz_level) ⇒
Option.map
(fun (l_value : Tx_rollup_level_repr.level) ⇒ (l_value, tz_level))
(Tx_rollup_level_repr.pred l_value)
| (Interval {| range.Interval.newest := newest |}, Some tz_level) ⇒
Some (newest, tz_level)
| _ ⇒ None
end.
Record record : Set := Build {
last_removed_commitment_hashes :
option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t);
finalized_commitments : range;
unfinalized_commitments : range;
uncommitted_inboxes : range;
commitment_newest_hash : option Tx_rollup_commitment_repr.Hash.t;
tezos_head_level : option Raw_level_repr.t;
burn_per_byte : Tez_repr.t;
inbox_ema : int;
allocated_storage : Z.t;
occupied_storage : Z.t;
commitments_watermark : watermark;
}.
Definition with_last_removed_commitment_hashes last_removed_commitment_hashes
(r : record) :=
Build last_removed_commitment_hashes r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_finalized_commitments finalized_commitments (r : record) :=
Build r.(last_removed_commitment_hashes) finalized_commitments
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_unfinalized_commitments unfinalized_commitments
(r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
unfinalized_commitments r.(uncommitted_inboxes) r.(commitment_newest_hash)
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_uncommitted_inboxes uncommitted_inboxes (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) uncommitted_inboxes r.(commitment_newest_hash)
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_commitment_newest_hash commitment_newest_hash (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes) commitment_newest_hash
r.(tezos_head_level) r.(burn_per_byte) r.(inbox_ema) r.(allocated_storage)
r.(occupied_storage) r.(commitments_watermark).
Definition with_tezos_head_level tezos_head_level (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) tezos_head_level r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_burn_per_byte burn_per_byte (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) burn_per_byte
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_inbox_ema inbox_ema (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
inbox_ema r.(allocated_storage) r.(occupied_storage)
r.(commitments_watermark).
Definition with_allocated_storage allocated_storage (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) allocated_storage r.(occupied_storage)
r.(commitments_watermark).
Definition with_occupied_storage occupied_storage (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) occupied_storage
r.(commitments_watermark).
Definition with_commitments_watermark commitments_watermark (r : record) :=
Build r.(last_removed_commitment_hashes) r.(finalized_commitments)
r.(unfinalized_commitments) r.(uncommitted_inboxes)
r.(commitment_newest_hash) r.(tezos_head_level) r.(burn_per_byte)
r.(inbox_ema) r.(allocated_storage) r.(occupied_storage)
commitments_watermark.
End t.
Definition t := t.record.
Definition initial_state (pre_allocated_storage : Z.t) : t :=
{| t.last_removed_commitment_hashes := None;
t.finalized_commitments :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.unfinalized_commitments :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.uncommitted_inboxes :=
Empty {| range.Empty.next := Tx_rollup_level_repr.root_value; |};
t.commitment_newest_hash := None; t.tezos_head_level := None;
t.burn_per_byte := Tez_repr.zero; t.inbox_ema := 0;
t.allocated_storage := pre_allocated_storage; t.occupied_storage := Z.zero;
t.commitments_watermark := None; |}.
Definition encoding : Data_encoding.t t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte;
t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark
|} := function_parameter in
((last_removed_commitment_hashes, finalized_commitments,
unfinalized_commitments, uncommitted_inboxes, commitment_newest_hash,
tezos_head_level, burn_per_byte, allocated_storage, occupied_storage,
inbox_ema), commitments_watermark))
(fun (function_parameter :
(option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t)
× range × range × range × option Tx_rollup_commitment_repr.Hash.t ×
option Raw_level_repr.t × Tez_repr.t × Z.t × Z.t × int) × watermark) ⇒
let
'((last_removed_commitment_hashes, finalized_commitments,
unfinalized_commitments, uncommitted_inboxes, commitment_newest_hash,
tezos_head_level, burn_per_byte, allocated_storage, occupied_storage,
inbox_ema), commitments_watermark) := function_parameter in
{| t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte; t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark; |}) None
(Data_encoding.merge_objs
(Data_encoding.obj10
(Data_encoding.req None None "last_removed_commitment_hashes"
(Data_encoding.option_value
(Data_encoding.obj2
(Data_encoding.req None None "last_message_hash"
Tx_rollup_message_result_hash_repr.encoding)
(Data_encoding.req None None "commitment_hash"
Tx_rollup_commitment_repr.Hash.encoding))))
(Data_encoding.req None None "finalized_commitments" range_encoding)
(Data_encoding.req None None "unfinalized_commitments" range_encoding)
(Data_encoding.req None None "uncommitted_inboxes" range_encoding)
(Data_encoding.req None None "commitment_newest_hash"
(Data_encoding.option_value Tx_rollup_commitment_repr.Hash.encoding))
(Data_encoding.req None None "tezos_head_level"
(Data_encoding.option_value Raw_level_repr.encoding))
(Data_encoding.req None None "burn_per_byte" Tez_repr.encoding)
(Data_encoding.req None None "allocated_storage" Data_encoding.n_value)
(Data_encoding.req None None "occupied_storage" Data_encoding.n_value)
(Data_encoding.req None None "inbox_ema" Data_encoding.int31))
(Data_encoding.obj1
(Data_encoding.req None None "commitments_watermark"
(Data_encoding.option_value Tx_rollup_level_repr.encoding)))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.last_removed_commitment_hashes := last_removed_commitment_hashes;
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes;
t.commitment_newest_hash := commitment_newest_hash;
t.tezos_head_level := tezos_head_level;
t.burn_per_byte := burn_per_byte;
t.inbox_ema := inbox_ema;
t.allocated_storage := allocated_storage;
t.occupied_storage := occupied_storage;
t.commitments_watermark := commitments_watermark
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "cost_per_byte: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " inbox_ema: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" finalized_commitments: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" unfinalized_commitments: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" uncommitted_inboxes: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" commitment_newest_hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" tezos_head_level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" last_removed_commitment_hashes: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" allocated_storage: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" occupied_storage: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" commitments_watermark: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))))))))))))))))))
"cost_per_byte: %a inbox_ema: %d finalized_commitments: %a unfinalized_commitments: %a uncommitted_inboxes: %a commitment_newest_hash: %a tezos_head_level: %a last_removed_commitment_hashes: %a allocated_storage: %a occupied_storage: %a commitments_watermark: %a")
Tez_repr.pp burn_per_byte inbox_ema pp_range finalized_commitments pp_range
unfinalized_commitments pp_range uncommitted_inboxes
(Format.pp_print_option None Tx_rollup_commitment_repr.Hash.pp)
commitment_newest_hash (Format.pp_print_option None Raw_level_repr.pp)
tezos_head_level
(Format.pp_print_option None
(fun (fmt : Format.formatter) ⇒
fun (function_parameter :
Tx_rollup_message_result_hash_repr.t ×
Tx_rollup_commitment_repr.Hash.t) ⇒
let '(m_value, c_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "(message result: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", commitment: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"(message result: %a, commitment: %a)")
Tx_rollup_message_result_hash_repr.pp m_value
Tx_rollup_commitment_repr.Hash.pp c_value))
last_removed_commitment_hashes Z.pp_print allocated_storage Z.pp_print
occupied_storage (Format.pp_print_option None Tx_rollup_level_repr.pp)
commitments_watermark.
Definition adjust_storage_allocation (state_value : t) (delta : Z.t)
: M? (t × Z.t) :=
if Z.equal Z.zero delta then
return? (state_value, Z.zero)
else
let occupied_storage' := state_value.(t.occupied_storage) +Z delta in
if occupied_storage' <Z Z.zero then
Error_monad.error_value
(Build_extensible "Internal_error" string
"Storage size should be positive after occupied space is freed.")
else
let diff_value := occupied_storage' -Z state_value.(t.allocated_storage)
in
if diff_value >Z Z.zero then
let state_value :=
t.with_occupied_storage occupied_storage'
(t.with_allocated_storage occupied_storage' state_value) in
return? (state_value, diff_value)
else
let state_value := t.with_occupied_storage occupied_storage' state_value
in
return? (state_value, Z.zero).
Definition update_burn_per_byte_helper (function_parameter : t)
: int → int → int → t :=
let
'{| t.burn_per_byte := burn_per_byte; t.inbox_ema := inbox_ema |} as
state_value := function_parameter in
fun (factor : int) ⇒
fun (final_size : int) ⇒
fun (hard_limit : int) ⇒
let threshold_increase := 90 in
let threshold_decrease := 80 in
let variation_factor := 5 in
let smoothing := 2 in
let inbox_ema :=
inbox_ema +i
(((final_size -i inbox_ema) ×i smoothing) /i (1 +i factor)) in
let percentage := (inbox_ema ×i 100) /i hard_limit in
let computation :=
if
(threshold_decrease <i percentage) &&
(percentage ≤i threshold_increase)
then
return? burn_per_byte
else
let? variation :=
let? x_value :=
Tez_repr.op_starquestion burn_per_byte variation_factor in
Tez_repr.op_divquestion x_value 100 in
let variation :=
if Tez_repr.op_eq variation Tez_repr.zero then
Tez_repr.one_mutez
else
variation in
if threshold_increase <i percentage then
Tez_repr.op_plusquestion burn_per_byte variation
else
if
(percentage <i threshold_decrease) &&
(Tez_repr.op_lt Tez_repr.zero burn_per_byte)
then
Tez_repr.op_minusquestion burn_per_byte variation
else
return? burn_per_byte in
match computation with
| Pervasives.Ok burn_per_byte ⇒
t.with_inbox_ema inbox_ema
(t.with_burn_per_byte burn_per_byte state_value)
| Pervasives.Error _ ⇒
t.with_inbox_ema inbox_ema
(t.with_burn_per_byte Tez_repr.max_mutez state_value)
end.
#[bypass_check(guard)]
Fixpoint update_burn_per_byte
(state_value : t) (elapsed : int) (factor : int) (final_size : int)
(hard_limit : int) {struct elapsed} : t :=
if elapsed >i factor then
t.with_inbox_ema 0 (t.with_burn_per_byte Tez_repr.zero state_value)
else
if elapsed ≤i 0 then
update_burn_per_byte_helper state_value factor final_size hard_limit
else
let state' := update_burn_per_byte_helper state_value factor 0 hard_limit
in
let elapsed := elapsed -i 1 in
update_burn_per_byte state' elapsed factor final_size hard_limit.
Definition has_valid_commitment_at (function_parameter : t)
: Tx_rollup_level_repr.level → bool :=
let '{|
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments
|} := function_parameter in
fun (level : Tx_rollup_level_repr.level) ⇒
(belongs_to finalized_commitments level) ||
(belongs_to unfinalized_commitments level).
Definition inboxes_count (function_parameter : t) : int :=
let '{|
t.unfinalized_commitments := unfinalized_commitments;
t.uncommitted_inboxes := uncommitted_inboxes
|} := function_parameter in
(range_count unfinalized_commitments) +i (range_count uncommitted_inboxes).
Definition uncommitted_inboxes_count (function_parameter : t) : int :=
let '{| t.uncommitted_inboxes := uncommitted_inboxes |} := function_parameter
in
range_count uncommitted_inboxes.
Definition commitments_count (function_parameter : t) : int :=
let '{|
t.finalized_commitments := finalized_commitments;
t.unfinalized_commitments := unfinalized_commitments
|} := function_parameter in
(range_count unfinalized_commitments) +i (range_count finalized_commitments).
Definition record_inbox_creation
(t_value : t) (level : Raw_level_repr.raw_level)
: M? (t × Tx_rollup_level_repr.t × Z.t) :=
let? '_ :=
match t_value.(t.tezos_head_level) with
| Some tezos_lvl ⇒
Error_monad.error_when (Raw_level_repr.op_lteq level tezos_lvl)
(Build_extensible "Internal_error" string
"Trying to create an inbox in the past")
| None ⇒ return? tt
end in
let '(uncommitted_inboxes, new_level) :=
extend t_value.(t.uncommitted_inboxes) in
let? '(t_value, diff_value) :=
adjust_storage_allocation t_value Tx_rollup_inbox_repr.size_value in
return?
((t.with_tezos_head_level (Some level)
(t.with_uncommitted_inboxes uncommitted_inboxes t_value)), new_level,
diff_value).
Definition next_commitment_predecessor (state_value : t)
: option Tx_rollup_commitment_repr.Hash.t :=
state_value.(t.commitment_newest_hash).
Definition finalized_commitment_oldest_level (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.finalized_commitments).
Definition next_commitment_level
(state_value : t) (current_level : Raw_level_repr.raw_level)
: M? Tx_rollup_level_repr.t :=
match
((range_oldest state_value.(t.uncommitted_inboxes)),
(range_newest state_value.(t.uncommitted_inboxes))) with
| (Some oldest_level, Some newest_level) ⇒
if Tx_rollup_level_repr.op_lt oldest_level newest_level then
return? oldest_level
else
match state_value.(t.tezos_head_level) with
| Some newest_inbox_creation ⇒
let? '_ :=
Error_monad.error_when
(Raw_level_repr.op_lteq current_level newest_inbox_creation)
(Build_extensible "No_uncommitted_inbox" unit tt) in
return? oldest_level
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"tezos_head_level was not properly set")
end
| (None, None) ⇒
Error_monad.error_value (Build_extensible "No_uncommitted_inbox" unit tt)
| ((Some _, None) | (None, Some _)) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string "rollup state is inconsistent")
end.
Definition next_commitment_to_finalize (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.unfinalized_commitments).
Definition next_commitment_to_remove (state_value : t)
: option Tx_rollup_level_repr.t :=
range_oldest state_value.(t.finalized_commitments).
Definition record_inbox_deletion
(state_value : t) (candidate : Tx_rollup_level_repr.level) : M? t :=
match
((range_oldest state_value.(t.unfinalized_commitments)),
match range_oldest state_value.(t.unfinalized_commitments) with
| Some level ⇒ Tx_rollup_level_repr.op_eq candidate level
| _ ⇒ false
end) with
| (Some level, true) ⇒
let? unfinalized_commitments :=
shrink state_value.(t.unfinalized_commitments) in
let '(finalized_commitments, _) :=
extend state_value.(t.finalized_commitments) in
return?
(t.with_unfinalized_commitments unfinalized_commitments
(t.with_finalized_commitments finalized_commitments state_value))
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Trying to delete the wrong inbox")
end.
Definition record_commitment_creation
(state_value : t) (level : Tx_rollup_level_repr.level)
(hash_value : Tx_rollup_commitment_repr.Hash.t) : M? t :=
match range_oldest state_value.(t.uncommitted_inboxes) with
| Some oldest ⇒
let? '_ :=
Error_monad.error_unless (Tx_rollup_level_repr.op_eq level oldest)
(Build_extensible "Internal_error" string
"Trying to create the wrong commitment") in
let? uncommitted_inboxes := shrink state_value.(t.uncommitted_inboxes) in
let '(unfinalized_commitments, _) :=
extend state_value.(t.unfinalized_commitments) in
let state_value :=
t.with_commitment_newest_hash (Some hash_value)
(t.with_uncommitted_inboxes uncommitted_inboxes
(t.with_unfinalized_commitments unfinalized_commitments state_value))
in
if is_above_watermark state_value.(t.commitments_watermark) level then
let? '(state_value, _) :=
adjust_storage_allocation state_value
(Z.neg Tx_rollup_inbox_repr.size_value) in
return? (t.with_commitments_watermark (make_watermark level) state_value)
else
return? state_value
| None ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Cannot create a commitment due to lack of inbox")
end.
Definition record_commitment_rejection
(state_value : t) (level : Tx_rollup_level_repr.t)
(predecessor_hash : option Tx_rollup_commitment_repr.Hash.t) : M? t :=
let unwrap_option {A : Set} (msg : string) (function_parameter : option A)
: M? A :=
match function_parameter with
| Some x_value ⇒ return? x_value
| _ ⇒
Error_monad.error_value (Build_extensible "Internal_error" string msg)
end in
let check_none {A : Set} (msg : string) (function_parameter : option A)
: M? unit :=
match function_parameter with
| None ⇒ return? tt
| Some _ ⇒
Error_monad.error_value (Build_extensible "Internal_error" string msg)
end in
let? uncommitted_inboxes :=
left_extend state_value.(t.uncommitted_inboxes) level in
let state_value := t.with_uncommitted_inboxes uncommitted_inboxes state_value
in
let? unfinalized_commitments :=
right_cut state_value.(t.unfinalized_commitments) level in
match
((Tx_rollup_level_repr.pred level),
match Tx_rollup_level_repr.pred level with
| Some pred_level ⇒
(belongs_to state_value.(t.unfinalized_commitments) pred_level) ||
(belongs_to state_value.(t.finalized_commitments) pred_level)
| _ ⇒ false
end) with
| (Some pred_level, true) ⇒
let? predecessor_hash :=
unwrap_option "Missing predecessor commitment" predecessor_hash in
return?
(t.with_commitment_newest_hash (Some predecessor_hash)
(t.with_unfinalized_commitments unfinalized_commitments state_value))
| (Some _, _) ⇒
let? '_ := check_none "Unexpected predecessor hash" predecessor_hash in
let? '(_, pred_hash) :=
unwrap_option "Missing commitment hash"
state_value.(t.last_removed_commitment_hashes) in
return?
(t.with_commitment_newest_hash (Some pred_hash)
(t.with_unfinalized_commitments unfinalized_commitments state_value))
| (None, _) ⇒
return?
(t.with_commitment_newest_hash None
(t.with_unfinalized_commitments unfinalized_commitments state_value))
end.
Definition record_commitment_deletion
(state_value : t) (level : Tx_rollup_level_repr.level)
(hash_value : Tx_rollup_commitment_repr.Hash.t)
(message_hash : Tx_rollup_message_result_hash_repr.t) : M? t :=
match
((range_oldest state_value.(t.finalized_commitments)),
match range_oldest state_value.(t.finalized_commitments) with
| Some oldest ⇒ Tx_rollup_level_repr.op_eq level oldest
| _ ⇒ false
end) with
| (Some oldest, true) ⇒
let? finalized_commitments := shrink state_value.(t.finalized_commitments)
in
return?
(t.with_finalized_commitments finalized_commitments
(t.with_last_removed_commitment_hashes (Some (message_hash, hash_value))
state_value))
| (_, _) ⇒
Error_monad.error_value
(Build_extensible "Internal_error" string
"Trying to remove an incorrect commitment")
end.
Definition burn_cost
(limit : option Tez_repr.t) (state_value : t) (size_value : int)
: M? Tez_repr.t :=
let? burn :=
Tez_repr.op_starquestion state_value.(t.burn_per_byte)
(Int64.of_int size_value) in
match
(limit,
match limit with
| Some limit ⇒ Tez_repr.op_gteq limit burn
| _ ⇒ false
end) with
| (Some limit, true) ⇒
Error_monad.error_value
(Build_extensible "Submit_batch_burn_exceeded"
Tx_rollup_errors_repr.Submit_batch_burn_exceeded
{| Tx_rollup_errors_repr.Submit_batch_burn_exceeded.burn := burn;
Tx_rollup_errors_repr.Submit_batch_burn_exceeded.limit := limit; |})
| (_, _) ⇒ return? burn
end.
Definition finalized_commitments_range (state_value : t)
: option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t) :=
match
((range_oldest state_value.(t.finalized_commitments)),
(range_newest state_value.(t.finalized_commitments))) with
| (Some oldest, Some newest) ⇒ Some (oldest, newest)
| _ ⇒ None
end.
Definition check_level_can_be_rejected
(state_value : t) (level : Tx_rollup_level_repr.level) : M? unit :=
match
((range_oldest state_value.(t.unfinalized_commitments)),
(range_newest state_value.(t.unfinalized_commitments))) with
| (Some oldest, Some newest) ⇒
Error_monad.error_unless
((Tx_rollup_level_repr.op_lteq oldest level) &&
(Tx_rollup_level_repr.op_lteq level newest))
(Build_extensible "Cannot_reject_level"
Tx_rollup_errors_repr.Cannot_reject_level
{| Tx_rollup_errors_repr.Cannot_reject_level.provided := level;
Tx_rollup_errors_repr.Cannot_reject_level.accepted_range :=
Some (oldest, newest); |})
| _ ⇒
Error_monad.error_value
(Build_extensible "Cannot_reject_level"
Tx_rollup_errors_repr.Cannot_reject_level
{| Tx_rollup_errors_repr.Cannot_reject_level.provided := level;
Tx_rollup_errors_repr.Cannot_reject_level.accepted_range := None; |})
end.
Definition last_removed_commitment_hashes (state_value : t)
: option
(Tx_rollup_message_result_hash_repr.t × Tx_rollup_commitment_repr.Hash.t) :=
state_value.(t.last_removed_commitment_hashes).
Definition head_levels (state_value : t)
: option (Tx_rollup_level_repr.level × Raw_level_repr.t) :=
match (state_value.(t.uncommitted_inboxes), state_value.(t.tezos_head_level))
with
| (Empty {| range.Empty.next := l_value |}, Some tz_level) ⇒
Option.map
(fun (l_value : Tx_rollup_level_repr.level) ⇒ (l_value, tz_level))
(Tx_rollup_level_repr.pred l_value)
| (Interval {| range.Interval.newest := newest |}, Some tz_level) ⇒
Some (newest, tz_level)
| _ ⇒ None
end.