Skip to main content

🦏 Sc_rollup_management_protocol.v

Proofs

See code, Gitlab , OCaml

The [make_internal_transfer] is valid
The [transactions_batch_of_internal] is valid
@TODO define and prove fold_left_map_es_is_valid in Environment/V8/List.v
Admitted.

The [outbox_message_of_outbox_message_repr] is valid