Verify Zk_rollup_parameters.v
Verify https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/zk_rollup_parameters/
-
add a validity predicate for deposit_parameters
-
verify the validity of get_deposit_parameters
(this depends on making progress on the task to remove the simulations)
Edited by Evan Marzion