🇿 Zk_rollup_apply.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_transfer.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_parameters.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_transfer.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_parameters.
Init function; without side-effects in Coq
Definition init_module : unit :=
let description := "ZK rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.zk_rollup_disabled" "ZK rollups are disabled" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_feature_disabled" unit tt) in
let description := "The value of [nb_ops] should never be negative." in
Error_monad.register_error_kind Error_monad.Permanent
"operation.zk_rollup_negative_nb_ops"
"ZK rollups negative number of operations" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
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_nb_ops" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_negative_nb_ops" unit tt).
Definition assert_feature_enabled (ctxt : Alpha_context.context) : M? unit :=
Error_monad.error_unless (Alpha_context.Constants.zk_rollup_enable ctxt)
(Build_extensible "Zk_rollup_feature_disabled" unit tt).
Definition originate {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(public_parameters : Plonk.public_parameters)
(circuits_info :
Alpha_context.Zk_rollup.Account.SMap.(Map.S.t)
Alpha_context.Zk_rollup.Account.circuit_info)
(init_state : Array.t Bls.Primitive.Fr.(S.PRIME_FIELD.t)) (nb_ops : int)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let? '_ :=
Error_monad.error_when (nb_ops <i 0)
(Build_extensible "Zk_rollup_negative_nb_ops" unit tt) in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.originate ctxt
{|
Alpha_context.Zk_rollup.Account.static.public_parameters :=
public_parameters;
Alpha_context.Zk_rollup.Account.static.state_length :=
Array.length init_state;
Alpha_context.Zk_rollup.Account.static.circuits_info := circuits_info;
Alpha_context.Zk_rollup.Account.static.nb_ops := nb_ops; |} init_state)
(fun function_parameter ⇒
let '(ctxt, originated_zk_rollup, storage_size) := function_parameter in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_origination_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size; |} in
(ctxt, result_value, nil)).
let description := "ZK rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.zk_rollup_disabled" "ZK rollups are disabled" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_feature_disabled" unit tt) in
let description := "The value of [nb_ops] should never be negative." in
Error_monad.register_error_kind Error_monad.Permanent
"operation.zk_rollup_negative_nb_ops"
"ZK rollups negative number of operations" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
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_nb_ops" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_negative_nb_ops" unit tt).
Definition assert_feature_enabled (ctxt : Alpha_context.context) : M? unit :=
Error_monad.error_unless (Alpha_context.Constants.zk_rollup_enable ctxt)
(Build_extensible "Zk_rollup_feature_disabled" unit tt).
Definition originate {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(public_parameters : Plonk.public_parameters)
(circuits_info :
Alpha_context.Zk_rollup.Account.SMap.(Map.S.t)
Alpha_context.Zk_rollup.Account.circuit_info)
(init_state : Array.t Bls.Primitive.Fr.(S.PRIME_FIELD.t)) (nb_ops : int)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let? '_ :=
Error_monad.error_when (nb_ops <i 0)
(Build_extensible "Zk_rollup_negative_nb_ops" unit tt) in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.originate ctxt
{|
Alpha_context.Zk_rollup.Account.static.public_parameters :=
public_parameters;
Alpha_context.Zk_rollup.Account.static.state_length :=
Array.length init_state;
Alpha_context.Zk_rollup.Account.static.circuits_info := circuits_info;
Alpha_context.Zk_rollup.Account.static.nb_ops := nb_ops; |} init_state)
(fun function_parameter ⇒
let '(ctxt, originated_zk_rollup, storage_size) := function_parameter in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_origination_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size; |} in
(ctxt, result_value, nil)).
[parse_ticket ~ticketer ~contents ~ty ctxt] reconstructs a ticket from
individual parts submitted as part of a Zk_rollup_publish operation.
Definition parse_ticket
(ticketer : Alpha_context.Contract.t)
(contents : Micheline.canonical Alpha_context.Script.prim)
(ty_value : Micheline.canonical Alpha_context.Script.prim)
(ctxt : Alpha_context.context)
: M? (Alpha_context.context × Ticket_token.ex_token) :=
let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
Script_ir_translator.parse_comparable_ty ctxt
(Micheline.root_value ty_value) in
let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
cast_exists (Es := Set)
(fun __Ex_comparable_ty_'a ⇒
[Alpha_context.context ** Script_typed_ir.comparable_ty])
[ctxt, contents_type] in
let? '(contents, ctxt) :=
((Script_ir_translator.parse_comparable_data None ctxt contents_type
(Micheline.root_value contents)) :
M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
return?
(ctxt,
(Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |})).
Definition publish {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(zk_rollup : Alpha_context.Zk_rollup.t)
(l2_ops :
list
(Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t))
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let? '_ :=
Error_monad.error_unless
(List.for_all
(fun (function_parameter :
Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t) ⇒
let '(l2_op, _ticket_opt) := function_parameter in
l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
≤Z Z.zero) l2_ops) (Build_extensible "Deposit_as_external" unit tt)
in
let? '(ctxt, l2_ops_with_ticket_hashes) :=
List.fold_left_map_es
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter :
Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t) ⇒
let '(l2_op, ticket_opt) := function_parameter in
match ticket_opt with
| None ⇒
let? '_ :=
Error_monad.error_unless
(l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
=Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
in
return? (ctxt, (l2_op, None))
|
Some {|
Alpha_context.Zk_rollup.Ticket.t.contents := contents;
Alpha_context.Zk_rollup.Ticket.t.ty := ty_value;
Alpha_context.Zk_rollup.Ticket.t.ticketer := ticketer
|} ⇒
let? '_ :=
Error_monad.error_when
(l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
=Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
in
let? '(ctxt, ticket_token) :=
parse_ticket ticketer contents ty_value ctxt in
let? '(receiver_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Contract
(Contract_repr.Implicit
l2_op.(Alpha_context.Zk_rollup.Operation.t.l1_dst)))
ticket_token in
let? '(source_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Zk_rollup zk_rollup) ticket_token in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Ticket_hash.equal
l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
source_ticket_hash)
(Build_extensible "Invalid_deposit_ticket" unit tt) in
return? (ctxt, (l2_op, (Some receiver_ticket_hash)))
end) ctxt l2_ops in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.add_to_pending ctxt zk_rollup
l2_ops_with_ticket_hashes)
(fun function_parameter ⇒
let '(ctxt, paid_storage_size_diff) := function_parameter in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_publish_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff; |} in
(ctxt, result_value, nil)).
Definition transaction_to_zk_rollup {A B : Set}
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
(parameters : Script_typed_ir.pair (Script_typed_ir.ticket A) bytes)
(dst_rollup : Alpha_context.Zk_rollup.t) (since : Alpha_context.context)
: M?
(Alpha_context.context ×
Apply_internal_results.successful_internal_operation_result × list B) :=
let? '_ := assert_feature_enabled ctxt in
let? '{|
Zk_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
Zk_rollup_parameters.deposit_parameters.zkru_operation := zkru_operation
|} := Zk_rollup_parameters.get_deposit_parameters parameters_ty parameters
in
let? '(ticket_size, ctxt) := Ticket_scanner.ex_ticket_size ctxt ex_ticket in
let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt in
let? '_ :=
Error_monad.error_when (Saturation_repr.op_gtexclamation ticket_size limit)
(Build_extensible "Ticket_payload_size_limit_exceeded"
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded
{|
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.payload_size
:= ticket_size;
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.limit
:= limit; |}) in
let '(ex_token, ticket_amount) :=
Ticket_scanner.ex_token_and_amount_of_ex_ticket ex_ticket in
let? '(ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Zk_rollup dst_rollup) ex_token in
let ticket_amount := Script_int.to_zint ticket_amount in
let? '_ :=
Error_monad.error_unless
(ticket_amount =Z
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
(Build_extensible "Invalid_deposit_amount" unit tt) in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Ticket_hash.equal ticket_hash
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id))
(Build_extensible "Invalid_deposit_ticket" unit tt) in
let? '(receiver_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Contract
(Contract_repr.Implicit
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.l1_dst))) ex_token
in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.add_to_pending ctxt
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.rollup_id)
[ (zkru_operation, (Some receiver_ticket_hash)) ])
(fun function_parameter ⇒
let '(ctxt, paid_storage_size_diff) := function_parameter in
let result_value :=
Apply_internal_results.ITransaction_result
(Apply_internal_results.Transaction_to_zk_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.balance_updates
:= nil;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.consumed_gas
:= Alpha_context.Gas.consumed since ctxt;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |}) in
(ctxt, result_value, nil)).
Definition SMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Definition insert {A : Set} (s_value : String.t) (x_value : A)
: SMap.(Map.S.t) (list A) → SMap.(Map.S.t) (list A) :=
SMap.(Map.S.update) s_value
(fun (function_parameter : option (list A)) ⇒
match function_parameter with
| None ⇒ Some [ x_value ]
| Some l_value ⇒ Some (cons x_value l_value)
end).
Definition collect_pending_ops_inputs {A : Set}
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(pending_ops_and_pis :
list
((Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)))
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
list bool) :=
let? '(rev_pi_map, new_state, fees, rev_exit_validites) :=
List.fold_left_es
(fun (function_parameter :
SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
list bool) ⇒
let '(rev_pi_map, old_state, fees, rev_exit_validites) :=
function_parameter in
fun (function_parameter :
(Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)) ⇒
let '((l2_op, _ticket_hash_opt), (name, sent_pi)) :=
function_parameter in
let new_state :=
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.new_state) in
let? '_ :=
Error_monad.error_unless
((Array.length new_state) =i
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
(Build_extensible "Inconsistent_state_update" unit tt) in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Pending_op
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.fee
:= sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee);
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.exit_validity
:=
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity);
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.zk_rollup
:= zk_rollup;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.l2_op
:= l2_op; |} in
let rev_pi_map :=
insert name
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
return?
(rev_pi_map, new_state,
(Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee)),
(cons sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity)
rev_exit_validites)))
(rev_pi_map,
account.(Alpha_context.Zk_rollup.Account.t.dynamic).(Alpha_context.Zk_rollup.Account.dynamic.state),
Bls.Primitive.Fr.(S.PRIME_FIELD.zero), nil) pending_ops_and_pis in
return? (rev_pi_map, new_state, fees, (List.rev rev_exit_validites)).
Definition collect_pivate_batch_inputs
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(update : Alpha_context.Zk_rollup.Update.t)
(prev_state : Alpha_context.Zk_rollup.State.t)
(fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) :=
let is_private
(function_parameter : option Alpha_context.Zk_rollup.Account.circuit_info)
: bool :=
match function_parameter with
| Some Alpha_context.Zk_rollup.Account.Private ⇒ true
| _ ⇒ false
end in
List.fold_left_es
(fun (function_parameter :
SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒
let '(rev_pi_map, old_state, fees) := function_parameter in
fun (function_parameter :
string × Alpha_context.Zk_rollup.Update.private_inner_pi) ⇒
let '(name, sent_pi) := function_parameter in
let? '_ :=
Error_monad.error_unless
(is_private
(Alpha_context.Zk_rollup.Account.SMap.(Map.S.find) name
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.circuits_info)))
(Build_extensible "Invalid_circuit" unit tt) in
let new_state :=
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.new_state) in
let? '_ :=
Error_monad.error_unless
((Array.length new_state) =i
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
(Build_extensible "Inconsistent_state_update" unit tt) in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Private_batch
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.fees
:=
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees);
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.zk_rollup
:= zk_rollup; |} in
let rev_pi_map :=
insert name
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
return?
(rev_pi_map, new_state,
(Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees))))
(rev_pi_map, prev_state, fees)
update.(Alpha_context.Zk_rollup.Update.t.private_pis).
Definition collect_fee_inputs
(prev_state : Alpha_context.Zk_rollup.State.t)
(update : Alpha_context.Zk_rollup.Update.t)
(fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
: SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t :=
let old_state := prev_state in
let new_state :=
update.(Alpha_context.Zk_rollup.Update.t.fee_pi).(Alpha_context.Zk_rollup.Update.fee_pi.new_state)
in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Fee
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.fees :=
fees; |} in
let rev_pi_map :=
insert "fee"
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
(rev_pi_map, new_state).
Definition collect_inputs {A : Set}
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(pending_ops_and_pis :
list
((Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)))
(update : Alpha_context.Zk_rollup.Update.t)
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
list bool × Alpha_context.Zk_rollup.State.t) :=
let? '(rev_pi_map, new_state, fees, exit_validities) :=
collect_pending_ops_inputs zk_rollup account rev_pi_map pending_ops_and_pis
in
let? '(rev_pi_map, new_state, fees) :=
collect_pivate_batch_inputs zk_rollup account rev_pi_map update new_state
fees in
let '(rev_pi_map, new_state) :=
collect_fee_inputs new_state update fees rev_pi_map in
let pi_map := SMap.(Map.S.map) List.rev rev_pi_map in
return? (pi_map, exit_validities, new_state).
Definition perform_exits
(ctxt : Alpha_context.context)
(exits :
list
((Alpha_context.Zk_rollup.Operation.t × option Alpha_context.Ticket_hash.t)
× bool)) : M? (Alpha_context.context × Z.t) :=
List.fold_left_es
(fun (function_parameter : Alpha_context.context × Z.t) ⇒
let '(ctxt, storage_diff) := function_parameter in
fun (function_parameter :
(Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Ticket_hash.t) × bool) ⇒
let '((op, ticket_hash_opt), exit_validity) := function_parameter in
match ticket_hash_opt with
| None ⇒
let? '_ :=
Error_monad.error_unless
(Z.zero =Z
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
(Build_extensible "Invalid_deposit_amount" unit tt) in
return? (ctxt, storage_diff)
| Some receiver_ticket_hash ⇒
if exit_validity then
let? amount :=
Option.value_e
(Ticket_amount.of_zint
(Z.abs
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)))
(Error_monad.trace_of_error
(Build_extensible "Invalid_deposit_amount" unit tt)) in
let? '(ctxt, diff_value) :=
Ticket_transfer.transfer_ticket_with_hashes ctxt
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
receiver_ticket_hash amount in
return? (ctxt, (diff_value +Z storage_diff))
else
return? (ctxt, storage_diff)
end) (ctxt, Z.zero) exits.
Definition update {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(zk_rollup : Alpha_context.Zk_rollup.t)
(update : Alpha_context.Zk_rollup.Update.t)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let rev_pi_map {B : Set} : SMap.(Map.S.t) B :=
SMap.(Map.S.empty) in
let? '(ctxt, account) := Alpha_context.Zk_rollup.account ctxt zk_rollup in
let update_public_length :=
List.length update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
let? '(ctxt, pending_list_length) :=
Alpha_context.Zk_rollup.get_pending_length ctxt zk_rollup in
let min_pending_to_process :=
Alpha_context.Constants.zk_rollup_min_pending_to_process ctxt in
let? '_ :=
Error_monad.error_when
((update_public_length <i pending_list_length) &&
(update_public_length <i min_pending_to_process))
(Build_extensible "Pending_bound" unit tt) in
let? '(ctxt, pending_ops) :=
Alpha_context.Zk_rollup.get_prefix ctxt zk_rollup update_public_length in
let pending_ops_and_pis :=
List.combine_drop pending_ops
update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
let? '(pi_map, exit_validities, new_state) :=
collect_inputs zk_rollup account rev_pi_map pending_ops_and_pis update in
let verified :=
Plonk.verify_multi_circuits
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.public_parameters)
(SMap.(Map.S.bindings) pi_map)
update.(Alpha_context.Zk_rollup.Update.t.proof) in
let? '_ :=
Error_monad.error_unless verified
(Build_extensible "Invalid_verification" unit tt) in
let? ctxt :=
Alpha_context.Zk_rollup.update ctxt zk_rollup update_public_length
(Alpha_context.Zk_rollup.Account.t.with_dynamic
(Alpha_context.Zk_rollup.Account.dynamic.with_state new_state
account.(Alpha_context.Zk_rollup.Account.t.dynamic)) account) in
let exits := List.combine_drop pending_ops exit_validities in
let? '(ctxt, exits_paid_storage_size_diff) := perform_exits ctxt exits in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_update_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= exits_paid_storage_size_diff; |} in
return? (ctxt, result_value, nil).
(ticketer : Alpha_context.Contract.t)
(contents : Micheline.canonical Alpha_context.Script.prim)
(ty_value : Micheline.canonical Alpha_context.Script.prim)
(ctxt : Alpha_context.context)
: M? (Alpha_context.context × Ticket_token.ex_token) :=
let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
Script_ir_translator.parse_comparable_ty ctxt
(Micheline.root_value ty_value) in
let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
cast_exists (Es := Set)
(fun __Ex_comparable_ty_'a ⇒
[Alpha_context.context ** Script_typed_ir.comparable_ty])
[ctxt, contents_type] in
let? '(contents, ctxt) :=
((Script_ir_translator.parse_comparable_data None ctxt contents_type
(Micheline.root_value contents)) :
M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
return?
(ctxt,
(Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |})).
Definition publish {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(zk_rollup : Alpha_context.Zk_rollup.t)
(l2_ops :
list
(Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t))
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let? '_ :=
Error_monad.error_unless
(List.for_all
(fun (function_parameter :
Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t) ⇒
let '(l2_op, _ticket_opt) := function_parameter in
l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
≤Z Z.zero) l2_ops) (Build_extensible "Deposit_as_external" unit tt)
in
let? '(ctxt, l2_ops_with_ticket_hashes) :=
List.fold_left_map_es
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter :
Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Zk_rollup.Ticket.t) ⇒
let '(l2_op, ticket_opt) := function_parameter in
match ticket_opt with
| None ⇒
let? '_ :=
Error_monad.error_unless
(l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
=Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
in
return? (ctxt, (l2_op, None))
|
Some {|
Alpha_context.Zk_rollup.Ticket.t.contents := contents;
Alpha_context.Zk_rollup.Ticket.t.ty := ty_value;
Alpha_context.Zk_rollup.Ticket.t.ticketer := ticketer
|} ⇒
let? '_ :=
Error_monad.error_when
(l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
=Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
in
let? '(ctxt, ticket_token) :=
parse_ticket ticketer contents ty_value ctxt in
let? '(receiver_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Contract
(Contract_repr.Implicit
l2_op.(Alpha_context.Zk_rollup.Operation.t.l1_dst)))
ticket_token in
let? '(source_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Zk_rollup zk_rollup) ticket_token in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Ticket_hash.equal
l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
source_ticket_hash)
(Build_extensible "Invalid_deposit_ticket" unit tt) in
return? (ctxt, (l2_op, (Some receiver_ticket_hash)))
end) ctxt l2_ops in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.add_to_pending ctxt zk_rollup
l2_ops_with_ticket_hashes)
(fun function_parameter ⇒
let '(ctxt, paid_storage_size_diff) := function_parameter in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_publish_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff; |} in
(ctxt, result_value, nil)).
Definition transaction_to_zk_rollup {A B : Set}
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
(parameters : Script_typed_ir.pair (Script_typed_ir.ticket A) bytes)
(dst_rollup : Alpha_context.Zk_rollup.t) (since : Alpha_context.context)
: M?
(Alpha_context.context ×
Apply_internal_results.successful_internal_operation_result × list B) :=
let? '_ := assert_feature_enabled ctxt in
let? '{|
Zk_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
Zk_rollup_parameters.deposit_parameters.zkru_operation := zkru_operation
|} := Zk_rollup_parameters.get_deposit_parameters parameters_ty parameters
in
let? '(ticket_size, ctxt) := Ticket_scanner.ex_ticket_size ctxt ex_ticket in
let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt in
let? '_ :=
Error_monad.error_when (Saturation_repr.op_gtexclamation ticket_size limit)
(Build_extensible "Ticket_payload_size_limit_exceeded"
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded
{|
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.payload_size
:= ticket_size;
Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.limit
:= limit; |}) in
let '(ex_token, ticket_amount) :=
Ticket_scanner.ex_token_and_amount_of_ex_ticket ex_ticket in
let? '(ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Zk_rollup dst_rollup) ex_token in
let ticket_amount := Script_int.to_zint ticket_amount in
let? '_ :=
Error_monad.error_unless
(ticket_amount =Z
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
(Build_extensible "Invalid_deposit_amount" unit tt) in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Ticket_hash.equal ticket_hash
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id))
(Build_extensible "Invalid_deposit_ticket" unit tt) in
let? '(receiver_ticket_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt
(Alpha_context.Destination.Contract
(Contract_repr.Implicit
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.l1_dst))) ex_token
in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Zk_rollup.add_to_pending ctxt
zkru_operation.(Alpha_context.Zk_rollup.Operation.t.rollup_id)
[ (zkru_operation, (Some receiver_ticket_hash)) ])
(fun function_parameter ⇒
let '(ctxt, paid_storage_size_diff) := function_parameter in
let result_value :=
Apply_internal_results.ITransaction_result
(Apply_internal_results.Transaction_to_zk_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.balance_updates
:= nil;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.consumed_gas
:= Alpha_context.Gas.consumed since ctxt;
Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |}) in
(ctxt, result_value, nil)).
Definition SMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Definition insert {A : Set} (s_value : String.t) (x_value : A)
: SMap.(Map.S.t) (list A) → SMap.(Map.S.t) (list A) :=
SMap.(Map.S.update) s_value
(fun (function_parameter : option (list A)) ⇒
match function_parameter with
| None ⇒ Some [ x_value ]
| Some l_value ⇒ Some (cons x_value l_value)
end).
Definition collect_pending_ops_inputs {A : Set}
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(pending_ops_and_pis :
list
((Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)))
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
list bool) :=
let? '(rev_pi_map, new_state, fees, rev_exit_validites) :=
List.fold_left_es
(fun (function_parameter :
SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
list bool) ⇒
let '(rev_pi_map, old_state, fees, rev_exit_validites) :=
function_parameter in
fun (function_parameter :
(Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)) ⇒
let '((l2_op, _ticket_hash_opt), (name, sent_pi)) :=
function_parameter in
let new_state :=
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.new_state) in
let? '_ :=
Error_monad.error_unless
((Array.length new_state) =i
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
(Build_extensible "Inconsistent_state_update" unit tt) in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Pending_op
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.fee
:= sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee);
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.exit_validity
:=
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity);
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.zk_rollup
:= zk_rollup;
Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.l2_op
:= l2_op; |} in
let rev_pi_map :=
insert name
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
return?
(rev_pi_map, new_state,
(Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee)),
(cons sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity)
rev_exit_validites)))
(rev_pi_map,
account.(Alpha_context.Zk_rollup.Account.t.dynamic).(Alpha_context.Zk_rollup.Account.dynamic.state),
Bls.Primitive.Fr.(S.PRIME_FIELD.zero), nil) pending_ops_and_pis in
return? (rev_pi_map, new_state, fees, (List.rev rev_exit_validites)).
Definition collect_pivate_batch_inputs
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(update : Alpha_context.Zk_rollup.Update.t)
(prev_state : Alpha_context.Zk_rollup.State.t)
(fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) :=
let is_private
(function_parameter : option Alpha_context.Zk_rollup.Account.circuit_info)
: bool :=
match function_parameter with
| Some Alpha_context.Zk_rollup.Account.Private ⇒ true
| _ ⇒ false
end in
List.fold_left_es
(fun (function_parameter :
SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒
let '(rev_pi_map, old_state, fees) := function_parameter in
fun (function_parameter :
string × Alpha_context.Zk_rollup.Update.private_inner_pi) ⇒
let '(name, sent_pi) := function_parameter in
let? '_ :=
Error_monad.error_unless
(is_private
(Alpha_context.Zk_rollup.Account.SMap.(Map.S.find) name
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.circuits_info)))
(Build_extensible "Invalid_circuit" unit tt) in
let new_state :=
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.new_state) in
let? '_ :=
Error_monad.error_unless
((Array.length new_state) =i
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
(Build_extensible "Inconsistent_state_update" unit tt) in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Private_batch
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.fees
:=
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees);
Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.zk_rollup
:= zk_rollup; |} in
let rev_pi_map :=
insert name
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
return?
(rev_pi_map, new_state,
(Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees))))
(rev_pi_map, prev_state, fees)
update.(Alpha_context.Zk_rollup.Update.t.private_pis).
Definition collect_fee_inputs
(prev_state : Alpha_context.Zk_rollup.State.t)
(update : Alpha_context.Zk_rollup.Update.t)
(fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
: SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
Alpha_context.Zk_rollup.State.t :=
let old_state := prev_state in
let new_state :=
update.(Alpha_context.Zk_rollup.Update.t.fee_pi).(Alpha_context.Zk_rollup.Update.fee_pi.new_state)
in
let pi :=
Alpha_context.Zk_rollup.Circuit_public_inputs.Fee
{|
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.old_state
:= old_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.new_state
:= new_state;
Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.fees :=
fees; |} in
let rev_pi_map :=
insert "fee"
(Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
rev_pi_map in
(rev_pi_map, new_state).
Definition collect_inputs {A : Set}
(zk_rollup : Alpha_context.Zk_rollup.t)
(account : Alpha_context.Zk_rollup.Account.t)
(rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
(pending_ops_and_pis :
list
((Alpha_context.Zk_rollup.Operation.t × A) ×
(String.t × Alpha_context.Zk_rollup.Update.op_pi)))
(update : Alpha_context.Zk_rollup.Update.t)
: M?
(SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
list bool × Alpha_context.Zk_rollup.State.t) :=
let? '(rev_pi_map, new_state, fees, exit_validities) :=
collect_pending_ops_inputs zk_rollup account rev_pi_map pending_ops_and_pis
in
let? '(rev_pi_map, new_state, fees) :=
collect_pivate_batch_inputs zk_rollup account rev_pi_map update new_state
fees in
let '(rev_pi_map, new_state) :=
collect_fee_inputs new_state update fees rev_pi_map in
let pi_map := SMap.(Map.S.map) List.rev rev_pi_map in
return? (pi_map, exit_validities, new_state).
Definition perform_exits
(ctxt : Alpha_context.context)
(exits :
list
((Alpha_context.Zk_rollup.Operation.t × option Alpha_context.Ticket_hash.t)
× bool)) : M? (Alpha_context.context × Z.t) :=
List.fold_left_es
(fun (function_parameter : Alpha_context.context × Z.t) ⇒
let '(ctxt, storage_diff) := function_parameter in
fun (function_parameter :
(Alpha_context.Zk_rollup.Operation.t ×
option Alpha_context.Ticket_hash.t) × bool) ⇒
let '((op, ticket_hash_opt), exit_validity) := function_parameter in
match ticket_hash_opt with
| None ⇒
let? '_ :=
Error_monad.error_unless
(Z.zero =Z
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
(Build_extensible "Invalid_deposit_amount" unit tt) in
return? (ctxt, storage_diff)
| Some receiver_ticket_hash ⇒
if exit_validity then
let? amount :=
Option.value_e
(Ticket_amount.of_zint
(Z.abs
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)))
(Error_monad.trace_of_error
(Build_extensible "Invalid_deposit_amount" unit tt)) in
let? '(ctxt, diff_value) :=
Ticket_transfer.transfer_ticket_with_hashes ctxt
op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
receiver_ticket_hash amount in
return? (ctxt, (diff_value +Z storage_diff))
else
return? (ctxt, storage_diff)
end) (ctxt, Z.zero) exits.
Definition update {A : Set}
(ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
(zk_rollup : Alpha_context.Zk_rollup.t)
(update : Alpha_context.Zk_rollup.Update.t)
: M?
(Alpha_context.context × Apply_results.successful_manager_operation_result ×
list A) :=
let? '_ := assert_feature_enabled ctxt in
let rev_pi_map {B : Set} : SMap.(Map.S.t) B :=
SMap.(Map.S.empty) in
let? '(ctxt, account) := Alpha_context.Zk_rollup.account ctxt zk_rollup in
let update_public_length :=
List.length update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
let? '(ctxt, pending_list_length) :=
Alpha_context.Zk_rollup.get_pending_length ctxt zk_rollup in
let min_pending_to_process :=
Alpha_context.Constants.zk_rollup_min_pending_to_process ctxt in
let? '_ :=
Error_monad.error_when
((update_public_length <i pending_list_length) &&
(update_public_length <i min_pending_to_process))
(Build_extensible "Pending_bound" unit tt) in
let? '(ctxt, pending_ops) :=
Alpha_context.Zk_rollup.get_prefix ctxt zk_rollup update_public_length in
let pending_ops_and_pis :=
List.combine_drop pending_ops
update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
let? '(pi_map, exit_validities, new_state) :=
collect_inputs zk_rollup account rev_pi_map pending_ops_and_pis update in
let verified :=
Plonk.verify_multi_circuits
account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.public_parameters)
(SMap.(Map.S.bindings) pi_map)
update.(Alpha_context.Zk_rollup.Update.t.proof) in
let? '_ :=
Error_monad.error_unless verified
(Build_extensible "Invalid_verification" unit tt) in
let? ctxt :=
Alpha_context.Zk_rollup.update ctxt zk_rollup update_public_length
(Alpha_context.Zk_rollup.Account.t.with_dynamic
(Alpha_context.Zk_rollup.Account.dynamic.with_state new_state
account.(Alpha_context.Zk_rollup.Account.t.dynamic)) account) in
let exits := List.combine_drop pending_ops exit_validities in
let? '(ctxt, exits_paid_storage_size_diff) := perform_exits ctxt exits in
let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
let result_value :=
Apply_results.Zk_rollup_update_result
{|
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.balance_updates
:= nil;
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
Apply_results.successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= exits_paid_storage_size_diff; |} in
return? (ctxt, result_value, nil).