/zk-rollup-security

Primary LanguageAlloy

Alloy model for ZK rollups

The model is developed in Alloy 6.1. The properties and testing scenarios are checked with glucose 4.1 SAT solver.

Code accompanying "Towards a formal foundation of blockchain rollups" paper.

Contents

  • rollup_data_model.als definition of datatypes associated with basic entities of ZK rollups.
    • Input abstract inputs (transactions);
    • Block encapsulate sequence of inputs;
    • Proof and Commitment represent proofs and commitments submitted from L2 to L1 for block finalization;
    • ForcedEvent events forced upon L2 through L1;
    • UpgradeAnnouncement abstract datatype which represents an announcement of an upgrade;
    • Timeout after upgrade announcement users get a period of time to act on the "upgrade announcement". The end of this period is signalled by the timeout event.
    • L1 a singleton object with fields which represent the state of L2 rollup on L1;
  • rollup_dynamics.als implementation of queries associated with ZK-rollups.
    • receive_commitment receives a commitment for later process.
    • receive_proof receives a proof for later process.
    • receive_forced receives a forced event, appends it to the queue unless upgrade is in the processing mode.
    • rollup_process tries to finalize previously received commitment and the proof.
    • update_blacklist processes the blacklisting event from the head of the forced queue.
    • upgrade_init receives the UpgradeAnnouncement and sets the L1.ongoing_upgrade field.
    • upgrade_timeout receives a timeout indicating that the current queueing phase of the upgrade has finished.
    • upgrade_deploy deploys the upgrade once the processing phase has ended (i.e., forced queue is empty).
    • stutter ensures that traces are infinite
    • events set of possible events.
  • rollup_properties.als specification of properties.
    • simple_rollup_prop* - properties associated with the basic ("strawnan") rollups;
    • cold_rollup_prop* - properties associated with forced queues;
    • blacklist_prop* - properties associated with rollups with "eager" blacklists updated through the forced queue;
    • upgrade_prop* - properties associated with "soft" blacklists updated through the upgradeability mechanism;
  • rollup_scenarios.als various scenarios for testing.