🦏 Sc_rollup_commitment_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

Import Error.Tactics_letP.

#[local] Ltac destruct_match :=
  match goal with
  | H : match ?a with _ ⇒ _ end |-
      context [match ?b with _ ⇒ _ end] ⇒
      change b with a; destruct a eqn:?
  end.

The function [get_commitment_opt_unsafe] is valid.

Lemma get_commitment_opt_unsafe_is_valid ctxt rollup commitment
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(commitment, ctxt) :=
    Sc_rollup_commitment_storage.get_commitment_opt_unsafe
      ctxt rollup commitment in
  Option.Forall Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.get_commitment_opt_unsafe.
  Raw_context.Valid.destruct_rewrite H_ctxt.
  rewrite_db storage_db.
  destruct H_sim_ctxt. red in Sc_rollup_Commitments.
  specialize (Sc_rollup_Commitments rollup commitment).
  simpl in ×.
  unfold Option.bind.
  do 2 (destruct_match; [|split; easy]).
  now split.
Qed.

The function [get_commitment_unsafe] is valid

Lemma get_commitment_unsafe_is_valid ctxt rollup commitment :
  Raw_context.Valid.t ctxt →
  letP? '(commitment, ctxt) :=
    Sc_rollup_commitment_storage.get_commitment_unsafe
      ctxt rollup commitment in
  Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
  Raw_context.Valid.t ctxt .
Proof.
  intros.
  unfold Sc_rollup_commitment_storage.get_commitment_unsafe.
  esplit_letP. {
    now apply get_commitment_opt_unsafe_is_valid.
  }
  i_des_pairs.
  step; simpl in *; [|reflexivity]. now split.
Qed.

The function [last_cemented_commitment] is valid.

Lemma last_cemented_commitment_is_valid ctxt rollup
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(_, ctxt) :=
    Sc_rollup_commitment_storage.last_cemented_commitment
      ctxt rollup in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.last_cemented_commitment.
  Raw_context.Valid.destruct_rewrite H_ctxt.
  rewrite_db storage_db; simpl.
  now step.
Qed.

The function [get_commitment] is valid.

Lemma get_commitment_is_valid ctxt rollup commitment
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(commitment, ctxt) :=
    Sc_rollup_commitment_storage.get_commitment
      ctxt rollup commitment in
  Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.get_commitment.
  esplit_letP. {
    now apply last_cemented_commitment_is_valid.
  }
  i_des_pairs.
  now apply get_commitment_unsafe_is_valid.
Qed.

The function [last_cemented_commitment_hash_with_level] is valid.

Lemma last_cemented_commitment_hash_with_level_is_valid ctxt rollup
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(_, level, ctxt) :=
    Sc_rollup_commitment_storage
      .last_cemented_commitment_hash_with_level
      ctxt rollup in
  Raw_level_repr.Valid.t level ∧
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage
    .last_cemented_commitment_hash_with_level.
  esplit_letP. {
    now apply last_cemented_commitment_is_valid.
  }
  i_des_pairs.
  unfold Lwt_result_syntax.op_letplus.
  esplit_letP. {
    now apply get_commitment_unsafe_is_valid.
  }
  intros [? ?] [? ?].
  simpl.
  split; [|easy].
  apply_by_type (Sc_rollup_commitment_repr.V1.Valid.t _).
Qed.

The function [set_commitment_added] is valid.

Lemma set_commitment_added_is_valid ctxt rollup node_value new_value
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_new_value : Raw_level_repr.Valid.t new_value) :
  letP? '(size_diff, new_value, ctxt) :=
    Sc_rollup_commitment_storage.set_commitment_added
      ctxt rollup node_value new_value in
  Pervasives.Int.Valid.t size_diff ∧
  Raw_level_repr.Valid.t new_value ∧
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.set_commitment_added.
  esplit_letP. {
    Raw_context.Valid.destruct_rewrite H_ctxt.
    simpl. destruct H_sim_ctxt.
    rewrite Storage_generated.Sc_rollup.Commitment_added.find.
    simpl.
    unshelve instantiate (1 := fun '(ctxt, opt_raw_level) ⇒
      Raw_context.Valid.t ctxt ∧
      Option.Forall Raw_level_repr.Valid.t opt_raw_level
      ). simpl.
    split; [easy|].
    unfold Option.bind.
    specialize (Sc_rollup_Commitment_added rollup node_value).
    simpl in ×.
    now do 2 (destruct_match; [|easy]).
  }
  i_des_pairs.
  step; simpl; [now split_conj|].
  esplit_letP. {
    select (Raw_context.Valid.t _) Raw_context.Valid.destruct_rewrite.
    rewrite Storage_generated.Sc_rollup.Commitment_added.add
      with (size := 0); simpl.
    destruct H_sim_ctxt.
    specialize (Sc_rollup_Commitment_added ltac:(assumption)
      ltac:(assumption)).
    unshelve instantiate (1 := fun '(ctxt, i, b) ⇒
      Raw_context.Valid.t ctxt ∧ Pervasives.Int.Valid.t i); simpl.
    simpl in ×.
    destruct_match; simpl; split; [|easy| |easy];
    apply (Raw_context.f_preserves_context_trivial_validity
                   _ Raw_context.Sc_rollup_Commitment_added
                   ltac:(eauto) H).
  }
  i_des_pairs.
  simpl. split_conj; easy.
Qed.

The function [get_predecessor_opt_unsafe] is valid.

Lemma get_predecessor_opt_unsafe_is_valid ctxt rollup node_value
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(_, ctxt) :=
    Sc_rollup_commitment_storage.get_predecessor_opt_unsafe
      ctxt rollup node_value in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.get_predecessor_opt_unsafe.
  esplit_letP. {
    now apply get_commitment_opt_unsafe_is_valid.
  }
  now intros [? ?] [? ?].
Qed.

The function [get_predecessor_unsafe] is valid.

Lemma get_predecessor_unsafe_is_valid ctxt rollup node_value
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(_, ctxt) :=
    Sc_rollup_commitment_storage.get_predecessor_unsafe
      ctxt rollup node_value in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.get_predecessor_unsafe.
  esplit_letP. {
    now apply get_commitment_unsafe_is_valid.
  }
  now intros [? ?] [? ?].
Qed.

The function [hash_value] is valid.

Lemma hash_value_is_valid ctxt commitment
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_commitment : Sc_rollup_commitment_repr.V1.Valid.t commitment) :
  letP? '(ctxt, _) :=
    Sc_rollup_commitment_storage.hash_value ctxt commitment in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_commitment_storage.hash_value.
  esplit_letP. {
    apply Raw_context.consume_gas_is_valid; [easy|].
    Raw_context.Valid.destruct_rewrite H_ctxt.
    apply Sc_rollup_costs.Constants.cost_serialize_commitment_is_valid.
  }
  intros.
  unfold to_result.
  step; simpl; [|reflexivity].
  esplit_letP. {
    apply Raw_context.consume_gas_is_valid; [easy|].
    apply Sc_rollup_costs.Constants.cost_hash_bytes_is_valid.
  }
  now intros.
Qed.