🦏 Sc_rollup_management_protocol.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_management_protocol.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_management_protocol.
The [make_internal_transfer] is valid
Lemma make_internal_transfer_is_valid {A : Set} ctxt ty_value payload sender
source destination:
letP? '(_, ctxt) := @Sc_rollup_management_protocol.make_internal_transfer A
ctxt ty_value payload sender source destination in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.make_internal_transfer.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP.
pose proof Script_ir_translator.unparse_data_is_valid.
Admitted.
source destination:
letP? '(_, ctxt) := @Sc_rollup_management_protocol.make_internal_transfer A
ctxt ty_value payload sender source destination in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.make_internal_transfer.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP.
pose proof Script_ir_translator.unparse_data_is_valid.
Admitted.
The [transactions_batch_of_internal] is valid
Lemma transactions_batch_of_internal_is_valid ctxt transactions :
letP? '(_, ctxt) := Sc_rollup_management_protocol
.transactions_batch_of_internal
ctxt transactions in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.transactions_batch_of_internal.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP.
letP? '(_, ctxt) := Sc_rollup_management_protocol
.transactions_batch_of_internal
ctxt transactions in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.transactions_batch_of_internal.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP.
@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
Lemma outbox_message_of_outbox_message_repr_is_valid ctxt function_parameter :
letP? '(_, ctxt) := Sc_rollup_management_protocol
.outbox_message_of_outbox_message_repr ctxt function_parameter in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.outbox_message_of_outbox_message_repr.
step.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP. {
apply transactions_batch_of_internal_is_valid.
}
intros x H.
hauto lq: on.
Qed.
letP? '(_, ctxt) := Sc_rollup_management_protocol
.outbox_message_of_outbox_message_repr ctxt function_parameter in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_management_protocol.outbox_message_of_outbox_message_repr.
step.
unfold Lwt_result_syntax.op_letplus.
eapply Error.split_letP. {
apply transactions_batch_of_internal_is_valid.
}
intros x H.
hauto lq: on.
Qed.