Resolve "Verify Zk_rollup_storage.v"
Closes #687 (closed) , #679 (closed) , #677 (closed)
We only write the specification and admit all the lemmas.
Edited by Guillaume Claret
Closes #687 (closed) , #679 (closed) , #677 (closed)
We only write the specification and admit all the lemmas.