🦏 Sc_rollup_inbox_merkelized_payload_hashes_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require Import TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require Import TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
[remember] is valid.
Lemma remember_is_valid
history_value merkelized payload :
letP? res := remember history_value merkelized payload in True.
Proof.
Admitted.
history_value merkelized payload :
letP? res := remember history_value merkelized payload in True.
Proof.
Admitted.
[add_payload] is valid.
Lemma add_payload_is_valid
history_value prev_merkelized payload :
letP? res := add_payload history_value prev_merkelized payload in True.
Proof.
unfold add_payload.
eapply Error.split_letP.
apply remember_is_valid.
scongruence.
Qed.
history_value prev_merkelized payload :
letP? res := add_payload history_value prev_merkelized payload in True.
Proof.
unfold add_payload.
eapply Error.split_letP.
apply remember_is_valid.
scongruence.
Qed.
[genesis] is valid.
Lemma genesis_is_valid history_value payload :
letP? res := genesis history_value payload in True.
Proof.
Admitted.
letP? res := genesis history_value payload in True.
Proof.
Admitted.