Verify Tx_rollup_l2_context.v
Verify the validity, and hence the absence of internal errors, for the file https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/tx_rollup_l2_context/ . You can first make a merge request to axiomatize all the expected properties. If you need validity properties in other files, you can axiomatize them. An example of validity proofs is in https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/proofs/apply/