diff --git a/src/app/zeko/circuits/count_commits.ml b/src/app/zeko/circuits/count_commits.ml new file mode 100644 index 0000000000..3ded454306 --- /dev/null +++ b/src/app/zeko/circuits/count_commits.ml @@ -0,0 +1,69 @@ +open Snark_params.Tick +open Zeko_util + +module Definition = struct + module Stmt = struct + type t = + { source_action_state : Rollup_state.Outer_action_state.t + ; target_action_state : Rollup_state.Outer_action_state.t + ; n_commits : Checked32.t + } + [@@deriving snarky] + end + + module Elem = Rollup_state.Outer_action + + let dummy_elem = + Rollup_state.Outer_action.Witness + { aux = Field.zero + ; children_digest = Rollup_state.Zkapp_call_forest.Digest.empty + ; slot_range = Slot_range.infinite + } + + module Init = struct + type t = { original_action_state : Rollup_state.Outer_action_state.t } + [@@deriving snarky] + end + + let init ~check:_ ({ original_action_state } : Init.var) : Stmt.var Checked.t + = + Checked.return + ( { source_action_state = original_action_state + ; target_action_state = original_action_state + ; n_commits = Checked32.Checked.zero + } + : Stmt.var ) + + let step (action : Rollup_state.Outer_action.var) + ({ source_action_state; target_action_state; n_commits } : Stmt.var) = + let* target_action_state = + Rollup_state.Outer_action.push_var action target_action_state + in + let*| n_commits = + let* increment = + if_ ~typ:Checked32.typ action.is_commit + ~then_:Checked32.(Checked.constant one) + ~else_:Checked32.Checked.zero + in + Checked32.Checked.add n_commits increment + in + Stmt.{ source_action_state; target_action_state; n_commits } + + let name = "count_commits" + + let leaf_iterations = + Zeko_constants.Folder_iterations.Count_commits.leaf_iterations + + let leaf_option_iterations = + Zeko_constants.Folder_iterations.Count_commits.leaf_option_iterations + + let extend_iterations = + Zeko_constants.Folder_iterations.Count_commits.extend_iterations + + let extend_option_iterations = + Zeko_constants.Folder_iterations.Count_commits.extend_option_iterations + + let wrap_domain = Some `N14 +end + +include Folder.Make (Definition) () diff --git a/src/app/zeko/circuits/design/rollup-centralized-explanation.md b/src/app/zeko/circuits/design/rollup-centralized-explanation.md index f9cd870b9d..6d988c42c5 100644 --- a/src/app/zeko/circuits/design/rollup-centralized-explanation.md +++ b/src/app/zeko/circuits/design/rollup-centralized-explanation.md @@ -10,6 +10,7 @@ It should be possible to have a stake in the rollup. And above all, it should be secure. To that end, here is a summary of what we want from the core protocol: + - The core rollup protocol does not handle transfer of value/MINA. - There is an associated token called ZEKO, using the fungible token standard, minted on the L1. @@ -25,8 +26,8 @@ To that end, here is a summary of what we want from the core protocol: to ensure that sequencer does not waste work synchronizing something that might be rolled back immediately. - Actions on the outside: - + Witness (witness arbitrary account update) - + Commit (sequencer committed) + - Witness (witness arbitrary account update) + - Commit (sequencer committed) - There is a backup special committee that can pause the rollup. Being paused is indicated by a field on the outer account. @@ -42,6 +43,7 @@ of actions. Withdrawals happen correspondingly, the other way around. We also wish to support timeouts on deposits. We do this by regarding a deposit as having three states: + - Unknown - Accepted - Rejected @@ -117,6 +119,30 @@ can profit from those deposits being processed. To prevent this from happening, we also specify a maximum size for the slot range. +## Emergency commit + +When the sequencer goes offline, we need a way to unblock the system +without decentralization of sequencing already in place. + +An emergency commit may be issued by anyone once enough time has +passed since the upper bound of the last commit slot range. +That upper bound witnesses the latest possible time a commit could +have occurred; if the current slot is past it by a fixed margin, +then no commit has happened since. + +Malicious sequencer can not pick a very large upper bound, since the slot range is capped by max_valid_size. + +However, we can only certify “no commit happened” relative to one of +the last five outer action states. To make this check viable, +the sequencer must maintain rolling commits over at least five slots +within the max_sequencer_inactivity window. With a sufficiently +large window (e.g., on the order of a month), this obligation is +trivial for a healthy sequencer. + +In effect, the emergency commit seals the gap with a bounded slot +range, restores liveness, and lets subsequent sequencers resume +committing under the usual rules. + ## ZEKO token The ZEKO token will use the diff --git a/src/app/zeko/circuits/design/rollup-centralized-spec.md b/src/app/zeko/circuits/design/rollup-centralized-spec.md index fe568389ec..9807478651 100644 --- a/src/app/zeko/circuits/design/rollup-centralized-spec.md +++ b/src/app/zeko/circuits/design/rollup-centralized-spec.md @@ -141,6 +141,65 @@ let do_commit } ] +let count_commits original_action_state actions = + let f (acc_action_state, n) = function + | (Commit _) as action -> + List.append action acc_action_state, n + 1 + | (Witness _) as action -> + List.append action acc_action_state, n + in + List.fold_left ~init:(original_action_state, 0) ~f actions + +val max_sequencer_inactivity : nat + +(* Emergency commit in case of sequencer's inactivity *) +let do_emergency_commit + ~txn_snark + ~valid_while + ~new_actions + ~new_inner_actions + ~old_inner_action_state_length + ~unsynchronized_actions + ~pause_key + ~da_key + ~outer_action_state_before_last_commit + ~last_commit + ~actions_since_last_commit + = + let [ commit ] = + do_commit + ~txn_snark + ~valid_while + ~new_actions + ~new_inner_actions + ~old_inner_action_state_length + ~unsynchronized_actions + ~pause_key + ~da_key + in + + (* Count commits since last commit *) + let (target_action_state, n_commits) = count_commits + (List.append last_commit outer_action_state_before_last_commit) + actions_since_last_commit + in + + (* Check that there has not been any commit after last commit *) + assert n_commits = 0 ; + + (* Check that count_commits is matching the precondition *) + assert target_action_state = commit.preconditions.action_state ; + + (* Check that enought time elapsed since last commit *) + assert commit.preconditions.valid_while.lower - last_commit.valid_while.upper >= max_sequencer_inactivity; + + (* Remove sequencer preconditions *) + [ { commit with + children = [] + ; preconditions.app_state.sequencer = Ignore + } + ] + let do_witness_outer ~aux ~children ~valid_while = [ { public_key = zeko_pk ; actions = [ Witness { aux ; children ; valid_while } ] diff --git a/src/app/zeko/circuits/dune b/src/app/zeko/circuits/dune index 9c52d1e38a..d6d3c3e56f 100644 --- a/src/app/zeko/circuits/dune +++ b/src/app/zeko/circuits/dune @@ -37,6 +37,7 @@ rule_bridge_outer_token_owner rule_change_permissions check_accepted_make + count_commits bridge_state outer_rules inner_rules diff --git a/src/app/zeko/circuits/outer_rules.ml b/src/app/zeko/circuits/outer_rules.ml index 5c29649887..4f7ab2a44c 100644 --- a/src/app/zeko/circuits/outer_rules.ml +++ b/src/app/zeko/circuits/outer_rules.ml @@ -4,6 +4,8 @@ module Make (Inputs : sig val inner_public_key : Signature_lib.Public_key.Compressed.t val chain_l1 : Mina_signature_kind.t + + val max_sequencer_inactivity : int end) () = struct @@ -17,6 +19,7 @@ struct Snark_params.Tick.Typ.(Mina_base.Zkapp_statement.typ * V.typ) ~branches: [ Rule_commit_inst.rule + ; Rule_commit_inst.Emergency_commit.rule ; Rule_action_witness_inst.rule ; Rule_pause_inst.rule ] diff --git a/src/app/zeko/circuits/rule_commit.ml b/src/app/zeko/circuits/rule_commit.ml index af6d6f35ad..1c01b7eedf 100644 --- a/src/app/zeko/circuits/rule_commit.ml +++ b/src/app/zeko/circuits/rule_commit.ml @@ -43,6 +43,43 @@ module Verify_both_ases = struct () ) end +(** Used to prove the number of commits in the emergency case. *) +module Count_commits_inst = Count_commits.Make (struct + let get_iterations = Zeko_constants.Max_excess_actions.Commit.count_commits +end) + +(** Proves Ase_outer_inst, Ase_inner_inst, and Count_commits to circumvent limitation of two recursive proof verifications per proof. *) +module Verify_emergency_folders = struct + let main (w : (Verify_both_ases.t * Count_commits_inst.t) V.t) = + let* verify_both_ases, count_commits = + exists ~compute:(V.get w) + Typ.(Verify_both_ases.typ * Count_commits_inst.typ) + in + let* both_ases, verify_both_ases = Verify_both_ases.get verify_both_ases in + let*| count_commits, verify_count_commits = + Count_commits_inst.get count_commits + in + Compile_simple. + { prevs = Two_prevs (verify_both_ases, verify_count_commits) + ; out = (both_ases, count_commits) + } + + let rule : _ Compile_simple.branch = + { branch_name = "Verify_emergency_folders" + ; tags = Two_tags (Verify_both_ases.tag, Count_commits.tag) + ; main + } + + include + ( val Compile_simple.compile ~name:"Verify_emergency_folders" + ~branches:[ rule ] + ~out_typ: + Typ.( + Ase_outer_inst.Stmt.typ * Ase_inner_inst.Stmt.typ + * Count_commits.Definition.Stmt.typ) + () ) +end + module Make (Inputs : sig (** max_valid_while_size signifies how big the valid_while can be for commits. *) val max_valid_while_size : int @@ -51,6 +88,8 @@ module Make (Inputs : sig val inner_public_key : PC.t val chain_l1 : Mina_signature_kind.t + + val max_sequencer_inactivity : int end) = struct open Inputs @@ -67,12 +106,11 @@ struct let length = Account_set.height end) - module Witness = struct + module Base_witness = struct type t = { txn_snark : Txn_rules.t (** The ledger transition we are performing. *) ; public_key : PC.t (** Our public key on the L2 *) ; vk_hash : F.t (** Our vk hash *) - ; verify_both_ases : Verify_both_ases.t ; old_inner_acc : Account.t ; old_inner_acc_path : Path.t ; new_inner_acc : Account.t @@ -84,6 +122,12 @@ struct [@@deriving snarky] end + module Witness = struct + type t = + { base_witness : Base_witness.t; verify_both_ases : Verify_both_ases.t } + [@@deriving snarky] + end + let implied_root (account : Account.var) (path : Path.var) : F.var Checked.t = let* init = Account.Checked.digest account in Checked.List.foldi path ~init ~f:(fun height acc PathElt.{ right_side } -> @@ -105,23 +149,24 @@ struct in content - let main (w : Witness.t V.t) = + let main ?(check_sequencer_precondition = true) (w : Base_witness.var) + ((ase_outer, ase_inner) : + Ase_outer_inst.Stmt.var * Ase_inner_inst.Stmt.var ) = with_label __LOC__ @@ fun () -> - let* ({ txn_snark - ; public_key - ; vk_hash - ; verify_both_ases - ; old_inner_acc - ; old_inner_acc_path - ; new_inner_acc - ; new_inner_acc_path - ; da_signature - ; da_key - ; slot_range - } : - Witness.var ) = - with_label __LOC__ @@ fun () -> exists ~compute:(V.get w) Witness.typ + let ({ txn_snark + ; public_key + ; vk_hash + ; old_inner_acc + ; old_inner_acc_path + ; new_inner_acc + ; new_inner_acc_path + ; da_signature + ; da_key + ; slot_range + } + : Base_witness.var ) = + w in with_label __LOC__ @@ fun () -> @@ -245,11 +290,6 @@ struct .outer_action_state in - (* Extract information from Verify_both_ases wrapper proof. *) - let* (ase_outer, ase_inner), verify_ases = - Verify_both_ases.get verify_both_ases - in - let Ase_outer_inst.Stmt. { source = synchronized_outer_action_state' ; target = outer_action_state @@ -361,7 +401,10 @@ struct The state we already know from the ledger hash, but the length is information we didn't have before. *) - ; sequencer = Some sequencer (* We must be the sequencer. *) + ; sequencer = + (* We must be the sequencer. *) + ( if check_sequencer_precondition then Some sequencer + else None ) ; paused = Some Boolean.false_ (* We must not be paused. *) ; pause_key = None (* We don't care about who can pause the rollup. *) @@ -416,11 +459,103 @@ struct make_outputs ~chain:chain_l1 account_update [ (sequencer_account_update, []) ] in - Compile_simple.{ prevs = Two_prevs (verify_txn_snark, verify_ases); out } + (out, verify_txn_snark) let rule : _ Compile_simple.branch = { branch_name = "Rollup step" ; tags = Two_tags (Txn_rules.tag, Verify_both_ases.tag) - ; main + ; main = + (fun (w : Witness.t V.t) -> + let* Witness.{ base_witness; verify_both_ases } = + exists ~compute:(V.get w) Witness.typ + in + let* (ase_outer, ase_inner), verify_both_ases = + Verify_both_ases.get verify_both_ases + in + let*| out, verify_txn_snark = + main base_witness (ase_outer, ase_inner) + in + Compile_simple. + { prevs = Two_prevs (verify_txn_snark, verify_both_ases); out } ) } + + (** Specialized version of the main function, used for emergency commits. + Only usable after [max_sequencer_inactivity] slots of the sequencer not committing. *) + module Emergency_commit = struct + module Witness = struct + type t = + { base_witness : Base_witness.t + ; before_last_commit : Rollup_state.Outer_action_state.t + ; last_commit : Rollup_state.Outer_action.Commit.t + ; verify_emergency_folders : Verify_emergency_folders.t + } + [@@deriving snarky] + end + + let rule : _ Compile_simple.branch = + { branch_name = "Emergency step" + ; tags = Two_tags (Txn_rules.tag, Verify_emergency_folders.tag) + ; main = + (fun (w : Witness.t V.t) -> + let* Witness. + { base_witness + ; before_last_commit + ; last_commit + ; verify_emergency_folders + } = + exists ~compute:(V.get w) Witness.typ + in + let* ( ((ase_outer, ase_inner), count_commits) + , verify_emergency_folders ) = + Verify_emergency_folders.get verify_emergency_folders + in + + (* Check that at least [max_sequencer_inactivity] slots have passed between last_commit and and this new commit *) + let* () = + assert_var __LOC__ (fun () -> + let* diff = + Slot.Checked.diff base_witness.slot_range.lower + last_commit.slot_range.upper + in + Mina_numbers.Global_slot_span.Checked.( + diff + >= constant + (Global_slot_span + (Unsigned.UInt32.of_int max_sequencer_inactivity) )) ) + in + + let Count_commits.Definition.Stmt. + { source_action_state; target_action_state; n_commits } = + count_commits + in + (* Apply last_commit to before_last_commit *) + let* after_last_commit = + Outer_action.push_commit_var last_commit before_last_commit + in + (* Check that counting started immediately after last_commit *) + let* () = + assert_equal ~label:__LOC__ Outer_action_state.typ + after_last_commit source_action_state + in + (* Check that target_action_state is the target of ase_outer, i.e. the outer action state precondition *) + let* () = + assert_equal ~label:__LOC__ Outer_action_state.typ + target_action_state ase_outer.target + in + (* Check that there has been no commits since last_commit *) + let* () = + assert_equal ~label:__LOC__ Checked32.typ n_commits + Checked32.Checked.zero + in + + let*| out, verify_txn_snark = + main ~check_sequencer_precondition:false base_witness + (ase_outer, ase_inner) + in + Compile_simple. + { prevs = Two_prevs (verify_txn_snark, verify_emergency_folders) + ; out + } ) + } + end end diff --git a/src/app/zeko/sequencer/prover/lib/prover.ml b/src/app/zeko/sequencer/prover/lib/prover.ml index 21d5e98a39..643d3761cf 100644 --- a/src/app/zeko/sequencer/prover/lib/prover.ml +++ b/src/app/zeko/sequencer/prover/lib/prover.ml @@ -299,7 +299,7 @@ let prove ?fake_proving_time ~logger ~proof_cache_db : in Output.Verify_both_ases (stmt, proof) | Outer_commit input -> - let Compile_simple.[ prove; _; _ ] = Outer_rules_inst.provers in + let Compile_simple.[ prove; _; _; _ ] = Outer_rules_inst.provers in let%bind vk_hash = Compile_simple.Verification_key.of_tag Outer_rules_inst.tag |> Promise.to_deferred @@ -318,7 +318,7 @@ let prove ?fake_proving_time ~logger ~proof_cache_db : ~f:Account_update.read_all_proofs_from_disk ) , proof ) | Bridge (Outer_action_witness input) -> - let Compile_simple.[ _; prove; _ ] = Outer_rules_inst.provers in + let Compile_simple.[ _; _; prove; _ ] = Outer_rules_inst.provers in let%bind vk_hash = Compile_simple.Verification_key.of_tag Outer_rules_inst.tag |> Promise.to_deferred diff --git a/src/app/zeko/zeko_circuits_config/zeko_circuits_config.ml b/src/app/zeko/zeko_circuits_config/zeko_circuits_config.ml index 724ceb54ba..72aac961ac 100644 --- a/src/app/zeko/zeko_circuits_config/zeko_circuits_config.ml +++ b/src/app/zeko/zeko_circuits_config/zeko_circuits_config.ml @@ -92,6 +92,8 @@ module Inputs = struct let max_valid_while_size = Zeko_circuits.Zeko_util.Slot.to_int t.max_valid_while_size + let max_sequencer_inactivity = (24 * 60 * 30 / 3) + 5 (* A month in slots *) + let holder_accounts_l1 = t.holder_accounts_l1 let holder_account_l2 = Zeko_constants.inner_holder_key diff --git a/src/app/zeko/zeko_constants.ml b/src/app/zeko/zeko_constants.ml index c2c015b390..f13640c2b9 100644 --- a/src/app/zeko/zeko_constants.ml +++ b/src/app/zeko/zeko_constants.ml @@ -54,6 +54,8 @@ module Max_excess_actions = struct let inner = Int.pow 2 9 let outer = Int.pow 2 9 + + let count_commits = Int.pow 2 9 end module Finalize_cancelled_deposit = struct @@ -119,4 +121,6 @@ module Folder_iterations = struct let extend_option_iterations = Int.pow 2 3 end + + module Count_commits : FOLDER_ITERATIONS = Check_accepted end diff --git a/src/app/zeko/zeko_types/zeko_types.ml b/src/app/zeko/zeko_types/zeko_types.ml index 7f44359a73..52a7789b36 100644 --- a/src/app/zeko/zeko_types/zeko_types.ml +++ b/src/app/zeko/zeko_types/zeko_types.ml @@ -697,7 +697,6 @@ module Outer_commit = struct type serializable = { txn_snark : Txn_snark.serializable ; public_key : Public_key.Compressed.t - ; verify_both_ases : Verify_both_ases.serializable ; old_inner_acc : Account.t ; old_inner_acc_path : Path.t ; new_inner_acc : Account.t @@ -705,6 +704,7 @@ module Outer_commit = struct ; da_signature : Signature.t ; da_key : Even_PC.t ; slot_range : Slot_range.t + ; verify_both_ases : Verify_both_ases.serializable } [@@deriving yojson] @@ -721,17 +721,19 @@ module Outer_commit = struct ; slot_range } : serializable ) ~vk_hash : t = - { txn_snark = Txn_snark.of_serializable txn_snark - ; public_key - ; vk_hash + { base_witness = + { txn_snark = Txn_snark.of_serializable txn_snark + ; public_key + ; vk_hash + ; old_inner_acc + ; old_inner_acc_path + ; new_inner_acc + ; new_inner_acc_path + ; da_signature + ; da_key + ; slot_range + } ; verify_both_ases = Verify_both_ases.of_serializable verify_both_ases - ; old_inner_acc - ; old_inner_acc_path - ; new_inner_acc - ; new_inner_acc_path - ; da_signature - ; da_key - ; slot_range } end end