🦏 Sc_rollup_inbox_merkelized_payload_hashes_repr.v

Proofs

See code, Gitlab , OCaml

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.

[remember] is valid.

Lemma remember_is_valid
  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.

[genesis] is valid.

Lemma genesis_is_valid history_value payload :
  letP? res := genesis history_value payload in True.
Proof.
Admitted.