🇿 Zk_rollup_storage.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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Zk_rollup_does_not_exist" "ZK Rollup does not exist"
"Attempted to use a ZK rollup that has not been originated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : Zk_rollup_repr.Address.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Rollup "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " does not exist"
CamlinternalFormatBasics.End_of_format)))
"Rollup %a does not exist") Zk_rollup_repr.Address.pp x_value))
(Data_encoding.obj1
(Data_encoding.req None None "rollup" Zk_rollup_repr.Address.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_does_not_exist" then
let x_value := cast Zk_rollup_repr.t payload in
Some x_value
else None
end)
(fun (x_value : Zk_rollup_repr.Address.t) ⇒
Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
x_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Zk_rollup_invalid_op code" "Invalid op code in append"
"Invalid op code in append"
(Some
(fun (ppf : Format.formatter) ⇒
fun (oc : int) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Op code "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" is not valid for this ZK Rollup"
CamlinternalFormatBasics.End_of_format)))
"Op code %d is not valid for this ZK Rollup") oc))
(Data_encoding.obj1
(Data_encoding.req None None "op_code" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_invalid_op_code" then
let oc := cast int payload in
Some oc
else None
end)
(fun (oc : int) ⇒ Build_extensible "Zk_rollup_invalid_op_code" int oc) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Zk_rollup_pending_list_too_short" "Pending list is too short"
"Pending list is too short" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_pending_list_too_short" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"Zk_rollup_negative_length" "Negative length for pending list prefix"
"Negative length for pending list prefix" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_negative_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_negative_length" unit tt).
Definition account
: Raw_context.t → Zk_rollup_repr.Address.t →
M? (Raw_context.t × Zk_rollup_account_repr.t) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get).
Definition pending_list_value
: Raw_context.t → Zk_rollup_repr.Address.t →
M? (Raw_context.t × Zk_rollup_repr.pending_list) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get).
Definition pending_op (ctxt : Raw_context.t) (id : Zk_rollup_repr.t)
: int64 →
M?
(Raw_context.t ×
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
(ctxt, id).
Definition originate
(ctxt : Raw_context.t) (static : Zk_rollup_account_repr.static)
(init_state : Zk_rollup_state_repr.t)
: M? (Raw_context.t × Zk_rollup_repr.Address.t × Z.t) :=
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
let? address := Zk_rollup_repr.Address.from_nonce nonce_value in
let origination_size := Constants_storage.zk_rollup_origination_size ctxt in
let initial_account :=
{| Zk_rollup_account_repr.t.static := static;
Zk_rollup_account_repr.t.dynamic :=
{| Zk_rollup_account_repr.dynamic.state := init_state;
Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space :=
Z.of_int origination_size;
Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space :=
Z.zero; |}; |} in
let? '(ctxt, account_size) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address initial_account in
let init_pl :=
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := 0; |} in
let? '(ctxt, pl_size) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address init_pl in
let address_size := Zk_rollup_repr.Address.size_value in
let size_value :=
Z.of_int (((origination_size +i address_size) +i account_size) +i pl_size)
in
return? (ctxt, address, size_value).
Definition add_to_pending
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
(ops :
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
: M? (Raw_context.t × Z.t) :=
let? '(ctxt, acc_value) := account ctxt rollup in
let? '_ :=
List.iter_e
(fun (function_parameter :
Zk_rollup_operation_repr.t × option Ticket_hash_repr.t) ⇒
let '(op, _ticket_hash_opt) := function_parameter in
if
(op.(Zk_rollup_operation_repr.t.op_code) ≥i
acc_value.(Zk_rollup_account_repr.t.static).(Zk_rollup_account_repr.static.nb_ops))
|| (op.(Zk_rollup_operation_repr.t.op_code) <i 0)
then
Error_monad.error_value
(Build_extensible "Zk_rollup_invalid_op_code" int
op.(Zk_rollup_operation_repr.t.op_code))
else
return? tt) ops in
let? '(ctxt, pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
ctxt rollup in
let '(next_index, length) :=
match pl with
|
Zk_rollup_repr.Empty {|
Zk_rollup_repr.pending_list.Empty.next_index := next_index |} ⇒
(next_index, 0)
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length
|} ⇒ (next_index, length)
end in
let? '(ctxt, next_index, length, storage_diff) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × int64 × int × int) ⇒
let '(ctxt, next_index, length, storage_diff) := function_parameter in
fun (op :
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
⇒
let? '(ctxt, new_storage_diff, _was_bound) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, rollup) next_index op in
return?
(ctxt, (Int64.succ next_index), (length +i 1),
(new_storage_diff +i storage_diff))) (ctxt, next_index, length, 0)
ops in
let used_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space)
+Z (Z.of_int storage_diff) in
let l2_operations_storage_space_to_pay :=
Z.max Z.zero
(used_l2_operations_storage_space -Z
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space))
in
let paid_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space)
+Z l2_operations_storage_space_to_pay in
let acc_value :=
Zk_rollup_account_repr.t.with_dynamic
(Zk_rollup_account_repr.dynamic.with_used_l2_operations_storage_space
used_l2_operations_storage_space
(Zk_rollup_account_repr.dynamic.with_paid_l2_operations_storage_space
paid_l2_operations_storage_space
acc_value.(Zk_rollup_account_repr.t.dynamic))) acc_value in
let pl :=
if length =i 0 then
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := next_index; |}
else
Zk_rollup_repr.Pending
{| Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length; |} in
let? '(ctxt, _diff_acc) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup acc_value in
let? '(ctxt, _diff_pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup pl in
return? (ctxt, l2_operations_storage_space_to_pay).
Definition pending_length (function_parameter : Zk_rollup_repr.pending_list)
: int :=
match function_parameter with
| Zk_rollup_repr.Empty _ ⇒ 0
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.length := length |} ⇒ length
end.
Definition head (function_parameter : Zk_rollup_repr.pending_list) : M? int64 :=
match function_parameter with
| Zk_rollup_repr.Empty _ ⇒
Error_monad.error_value
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt)
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length
|} ⇒ return? (next_index -i64 (Int64.of_int length))
end.
Definition next_index (function_parameter : Zk_rollup_repr.pending_list)
: int64 :=
match function_parameter with
|
Zk_rollup_repr.Empty {|
Zk_rollup_repr.pending_list.Empty.next_index := next_index |} ⇒
next_index
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index |} ⇒
next_index
end.
Definition get_pending_length
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? (Raw_context.t × int) :=
let? '(ctxt, pl) := pending_list_value ctxt rollup in
return? (ctxt, (pending_length pl)).
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Zk_rollup_does_not_exist" "ZK Rollup does not exist"
"Attempted to use a ZK rollup that has not been originated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : Zk_rollup_repr.Address.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Rollup "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " does not exist"
CamlinternalFormatBasics.End_of_format)))
"Rollup %a does not exist") Zk_rollup_repr.Address.pp x_value))
(Data_encoding.obj1
(Data_encoding.req None None "rollup" Zk_rollup_repr.Address.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_does_not_exist" then
let x_value := cast Zk_rollup_repr.t payload in
Some x_value
else None
end)
(fun (x_value : Zk_rollup_repr.Address.t) ⇒
Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
x_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Zk_rollup_invalid_op code" "Invalid op code in append"
"Invalid op code in append"
(Some
(fun (ppf : Format.formatter) ⇒
fun (oc : int) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Op code "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" is not valid for this ZK Rollup"
CamlinternalFormatBasics.End_of_format)))
"Op code %d is not valid for this ZK Rollup") oc))
(Data_encoding.obj1
(Data_encoding.req None None "op_code" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_invalid_op_code" then
let oc := cast int payload in
Some oc
else None
end)
(fun (oc : int) ⇒ Build_extensible "Zk_rollup_invalid_op_code" int oc) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"Zk_rollup_pending_list_too_short" "Pending list is too short"
"Pending list is too short" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_pending_list_too_short" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"Zk_rollup_negative_length" "Negative length for pending list prefix"
"Negative length for pending list prefix" None Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_negative_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_negative_length" unit tt).
Definition account
: Raw_context.t → Zk_rollup_repr.Address.t →
M? (Raw_context.t × Zk_rollup_account_repr.t) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get).
Definition pending_list_value
: Raw_context.t → Zk_rollup_repr.Address.t →
M? (Raw_context.t × Zk_rollup_repr.pending_list) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get).
Definition pending_op (ctxt : Raw_context.t) (id : Zk_rollup_repr.t)
: int64 →
M?
(Raw_context.t ×
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
(ctxt, id).
Definition originate
(ctxt : Raw_context.t) (static : Zk_rollup_account_repr.static)
(init_state : Zk_rollup_state_repr.t)
: M? (Raw_context.t × Zk_rollup_repr.Address.t × Z.t) :=
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
let? address := Zk_rollup_repr.Address.from_nonce nonce_value in
let origination_size := Constants_storage.zk_rollup_origination_size ctxt in
let initial_account :=
{| Zk_rollup_account_repr.t.static := static;
Zk_rollup_account_repr.t.dynamic :=
{| Zk_rollup_account_repr.dynamic.state := init_state;
Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space :=
Z.of_int origination_size;
Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space :=
Z.zero; |}; |} in
let? '(ctxt, account_size) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address initial_account in
let init_pl :=
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := 0; |} in
let? '(ctxt, pl_size) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt address init_pl in
let address_size := Zk_rollup_repr.Address.size_value in
let size_value :=
Z.of_int (((origination_size +i address_size) +i account_size) +i pl_size)
in
return? (ctxt, address, size_value).
Definition add_to_pending
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
(ops :
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
: M? (Raw_context.t × Z.t) :=
let? '(ctxt, acc_value) := account ctxt rollup in
let? '_ :=
List.iter_e
(fun (function_parameter :
Zk_rollup_operation_repr.t × option Ticket_hash_repr.t) ⇒
let '(op, _ticket_hash_opt) := function_parameter in
if
(op.(Zk_rollup_operation_repr.t.op_code) ≥i
acc_value.(Zk_rollup_account_repr.t.static).(Zk_rollup_account_repr.static.nb_ops))
|| (op.(Zk_rollup_operation_repr.t.op_code) <i 0)
then
Error_monad.error_value
(Build_extensible "Zk_rollup_invalid_op_code" int
op.(Zk_rollup_operation_repr.t.op_code))
else
return? tt) ops in
let? '(ctxt, pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
ctxt rollup in
let '(next_index, length) :=
match pl with
|
Zk_rollup_repr.Empty {|
Zk_rollup_repr.pending_list.Empty.next_index := next_index |} ⇒
(next_index, 0)
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length
|} ⇒ (next_index, length)
end in
let? '(ctxt, next_index, length, storage_diff) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × int64 × int × int) ⇒
let '(ctxt, next_index, length, storage_diff) := function_parameter in
fun (op :
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
⇒
let? '(ctxt, new_storage_diff, _was_bound) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctxt, rollup) next_index op in
return?
(ctxt, (Int64.succ next_index), (length +i 1),
(new_storage_diff +i storage_diff))) (ctxt, next_index, length, 0)
ops in
let used_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space)
+Z (Z.of_int storage_diff) in
let l2_operations_storage_space_to_pay :=
Z.max Z.zero
(used_l2_operations_storage_space -Z
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space))
in
let paid_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space)
+Z l2_operations_storage_space_to_pay in
let acc_value :=
Zk_rollup_account_repr.t.with_dynamic
(Zk_rollup_account_repr.dynamic.with_used_l2_operations_storage_space
used_l2_operations_storage_space
(Zk_rollup_account_repr.dynamic.with_paid_l2_operations_storage_space
paid_l2_operations_storage_space
acc_value.(Zk_rollup_account_repr.t.dynamic))) acc_value in
let pl :=
if length =i 0 then
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := next_index; |}
else
Zk_rollup_repr.Pending
{| Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length; |} in
let? '(ctxt, _diff_acc) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup acc_value in
let? '(ctxt, _diff_pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup pl in
return? (ctxt, l2_operations_storage_space_to_pay).
Definition pending_length (function_parameter : Zk_rollup_repr.pending_list)
: int :=
match function_parameter with
| Zk_rollup_repr.Empty _ ⇒ 0
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.length := length |} ⇒ length
end.
Definition head (function_parameter : Zk_rollup_repr.pending_list) : M? int64 :=
match function_parameter with
| Zk_rollup_repr.Empty _ ⇒
Error_monad.error_value
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt)
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := length
|} ⇒ return? (next_index -i64 (Int64.of_int length))
end.
Definition next_index (function_parameter : Zk_rollup_repr.pending_list)
: int64 :=
match function_parameter with
|
Zk_rollup_repr.Empty {|
Zk_rollup_repr.pending_list.Empty.next_index := next_index |} ⇒
next_index
|
Zk_rollup_repr.Pending {|
Zk_rollup_repr.pending_list.Pending.next_index := next_index |} ⇒
next_index
end.
Definition get_pending_length
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? (Raw_context.t × int) :=
let? '(ctxt, pl) := pending_list_value ctxt rollup in
return? (ctxt, (pending_length pl)).
Same as [Tezos_stdlib.Utils.fold_n_times] but with Lwt and Error monad
#[bypass_check(guard)]
Definition fold_n_times_es {A : Set}
(when_negative : Error_monad._error) (n_value : int) (f_value : A → M? A)
(e_value : A) : M? A :=
if n_value <i 0 then
Error_monad.Lwt_result_syntax.tzfail when_negative
else
let fix go (acc_value : A) (function_parameter : int)
{struct function_parameter} : M? A :=
match function_parameter with
| 0 ⇒ return? acc_value
| n_value ⇒
let? acc_value := f_value acc_value in
go acc_value (n_value -i 1)
end in
go e_value n_value.
Definition get_prefix
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t) (n_value : int)
: M?
(Raw_context.t ×
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)) :=
if n_value =i 0 then
return? (ctxt, nil)
else
let? '(ctxt, pl) := pending_list_value ctxt rollup in
let pl_length := pending_length pl in
let? '_ :=
Error_monad.error_when (n_value >i pl_length)
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
let? hd := head pl in
let? '(ctxt, ops, _i) :=
fold_n_times_es (Build_extensible "Zk_rollup_negative_length" unit tt)
n_value
(fun (function_parameter :
Raw_context.t ×
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)
× int64) ⇒
let '(ctxt, ops, i_value) := function_parameter in
let? '(ctxt, op) := pending_op ctxt rollup i_value in
return? (ctxt, (cons op ops), (Int64.pred i_value)))
(ctxt, nil, ((hd +i64 (Int64.of_int n_value)) -i64 1)) in
return? (ctxt, ops).
Definition update
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
(pending_to_drop : int) (new_account : Zk_rollup_account_repr.t)
: M? Raw_context.t :=
let? '(ctxt, pl) := pending_list_value ctxt rollup in
let? '(ctxt, acc_value) := account ctxt rollup in
let pl_length := pending_length pl in
let? '_ :=
Error_monad.error_when (pending_to_drop >i pl_length)
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
let next_index := next_index pl in
let? '(ctxt, freed) :=
match head pl with
| Pervasives.Error _e ⇒ return? (ctxt, 0)
| Pervasives.Ok head ⇒
let? '(ctxt, freed, _i) :=
fold_n_times_es (Build_extensible "Zk_rollup_negative_length" unit tt)
pending_to_drop
(fun (function_parameter : Raw_context.t × int × int64) ⇒
let '(ctxt, freed, i_value) := function_parameter in
let? '(ctxt, new_freed, _bound) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
(ctxt, rollup) i_value in
return? (ctxt, (freed +i new_freed), (Int64.succ i_value)))
(ctxt, 0, head) in
return? (ctxt, freed)
end in
let used_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space)
-Z (Z.of_int freed) in
let new_account :=
Zk_rollup_account_repr.t.with_dynamic
{|
Zk_rollup_account_repr.dynamic.state :=
new_account.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.state);
Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space :=
new_account.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space);
Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space; |} new_account in
let? '(ctxt, _diff_acc) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup new_account in
let pl_length := pl_length -i pending_to_drop in
let pl :=
if pl_length =i 0 then
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := next_index; |}
else
Zk_rollup_repr.Pending
{| Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := pl_length; |} in
let? '(ctxt, _diff_pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup pl in
return? ctxt.
Definition assert_exist
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? Raw_context.t :=
let? '(ctxt, _exists) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt rollup in
let? '_ :=
Error_monad.error_unless _exists
(Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
rollup) in
return? ctxt.
Definition _exists (ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? (Raw_context.t × bool) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt rollup.
Definition fold_n_times_es {A : Set}
(when_negative : Error_monad._error) (n_value : int) (f_value : A → M? A)
(e_value : A) : M? A :=
if n_value <i 0 then
Error_monad.Lwt_result_syntax.tzfail when_negative
else
let fix go (acc_value : A) (function_parameter : int)
{struct function_parameter} : M? A :=
match function_parameter with
| 0 ⇒ return? acc_value
| n_value ⇒
let? acc_value := f_value acc_value in
go acc_value (n_value -i 1)
end in
go e_value n_value.
Definition get_prefix
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t) (n_value : int)
: M?
(Raw_context.t ×
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)) :=
if n_value =i 0 then
return? (ctxt, nil)
else
let? '(ctxt, pl) := pending_list_value ctxt rollup in
let pl_length := pending_length pl in
let? '_ :=
Error_monad.error_when (n_value >i pl_length)
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
let? hd := head pl in
let? '(ctxt, ops, _i) :=
fold_n_times_es (Build_extensible "Zk_rollup_negative_length" unit tt)
n_value
(fun (function_parameter :
Raw_context.t ×
list
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value)
× int64) ⇒
let '(ctxt, ops, i_value) := function_parameter in
let? '(ctxt, op) := pending_op ctxt rollup i_value in
return? (ctxt, (cons op ops), (Int64.pred i_value)))
(ctxt, nil, ((hd +i64 (Int64.of_int n_value)) -i64 1)) in
return? (ctxt, ops).
Definition update
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
(pending_to_drop : int) (new_account : Zk_rollup_account_repr.t)
: M? Raw_context.t :=
let? '(ctxt, pl) := pending_list_value ctxt rollup in
let? '(ctxt, acc_value) := account ctxt rollup in
let pl_length := pending_length pl in
let? '_ :=
Error_monad.error_when (pending_to_drop >i pl_length)
(Build_extensible "Zk_rollup_pending_list_too_short" unit tt) in
let next_index := next_index pl in
let? '(ctxt, freed) :=
match head pl with
| Pervasives.Error _e ⇒ return? (ctxt, 0)
| Pervasives.Ok head ⇒
let? '(ctxt, freed, _i) :=
fold_n_times_es (Build_extensible "Zk_rollup_negative_length" unit tt)
pending_to_drop
(fun (function_parameter : Raw_context.t × int × int64) ⇒
let '(ctxt, freed, i_value) := function_parameter in
let? '(ctxt, new_freed, _bound) :=
Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
(ctxt, rollup) i_value in
return? (ctxt, (freed +i new_freed), (Int64.succ i_value)))
(ctxt, 0, head) in
return? (ctxt, freed)
end in
let used_l2_operations_storage_space :=
acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space)
-Z (Z.of_int freed) in
let new_account :=
Zk_rollup_account_repr.t.with_dynamic
{|
Zk_rollup_account_repr.dynamic.state :=
new_account.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.state);
Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space :=
new_account.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space);
Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space; |} new_account in
let? '(ctxt, _diff_acc) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup new_account in
let pl_length := pl_length -i pending_to_drop in
let pl :=
if pl_length =i 0 then
Zk_rollup_repr.Empty
{| Zk_rollup_repr.pending_list.Empty.next_index := next_index; |}
else
Zk_rollup_repr.Pending
{| Zk_rollup_repr.pending_list.Pending.next_index := next_index;
Zk_rollup_repr.pending_list.Pending.length := pl_length; |} in
let? '(ctxt, _diff_pl) :=
Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt rollup pl in
return? ctxt.
Definition assert_exist
(ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? Raw_context.t :=
let? '(ctxt, _exists) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt rollup in
let? '_ :=
Error_monad.error_unless _exists
(Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
rollup) in
return? ctxt.
Definition _exists (ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
: M? (Raw_context.t × bool) :=
Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt rollup.