Skip to main content

🦏 Sc_rollup_inbox_repr.v

Proofs

See code, Gitlab , OCaml

[hash_encoding] is valid
  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _True)
      Sc_rollup_inbox_repr.Hash.encoding.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
End Hash.
#[global] Hint Resolve Hash.encoding_is_valid : Data_encoding_db.

Validity of [old_level_messages]
Module old_levels_messages.
  Module Valid.
    Record t `{Skip_list_repr.Make.FArgs}
      (r : Skip_list_repr.Make.cell.record
         Sc_rollup_inbox_repr.Hash.t Sc_rollup_inbox_repr.Hash.t)
      : Prop := {
      back_pointers :
       let bp := r.(Skip_list_repr.Make.cell.back_pointers) in
         bp.(FallbackArray.t.default) = None
         Forall (fun xx None) bp.(FallbackArray.t.items);
      index : Pervasives.Int31.Valid.t r.(Skip_list_repr.Make.cell.index);
    }.
  End Valid.
End old_levels_messages.

Module V1.
Validity of [Sc_rollup_inbox_repr.V1.t]
  Module Valid.
    Import Sc_rollup_inbox_repr.V1.t.

    Record t (x : Sc_rollup_inbox_repr.V1.t) : Prop := {
        level : Raw_level_repr.Valid.t x.(level);
        nb_messages_in_commitment_period :
          Int64.Valid.t x.(nb_messages_in_commitment_period);
      }.
  End Valid.

  Lemma level_proof_encoding_is_valid :
    Data_encoding.Valid.t (fun _True) V1.level_proof_encoding.
  Proof.
  Admitted.
  #[global] Hint Resolve level_proof_encoding_is_valid : Data_encoding_db.

  Lemma history_proof_encoding_is_valid :
    Data_encoding.Valid.t (fun _True) V1.history_proof_encoding.
  Proof.
  Admitted.
  #[global] Hint Resolve history_proof_encoding_is_valid : Data_encoding_db.

[encoding] is valid
  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.V1.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x H_valid.
    repeat (split; try dtauto);
      destruct_all Sc_rollup_inbox_repr.t;
      destruct H_valid; simpl in *;
      unfold Pervasives.Int.Valid.t in *;
      f_equal.
    now apply FunctionalExtensionality.functional_extensionality; intros [].
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End V1.

[inclusion_proof_encoding] is valid
Lemma inclusion_proof_encoding_is_valid :
  Data_encoding.Valid.t (fun _True)
    Sc_rollup_inbox_repr.inclusion_proof_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  sfirstorder.
Qed.
#[global] Hint Resolve inclusion_proof_encoding_is_valid : Data_encoding_db.

[add_message] is valid.
[form_history_proof] is valid.
Lemma form_history_proof_is_valid history_value
  inbox_value :
  letP? res := form_history_proof history_value inbox_value in True.
Proof.
  unfold form_history_proof. simpl.
  apply Error.split_letP with (P:=(fun _True)).
  apply Bounded_history_repr.Make.remember_is_valid.
  intros. reflexivity.
Qed.

[initialize_level_tree_when_needed] is valid.
Lemma initialize_level_tree_when_needed_is_valid level_tree_history
  inbox_value level_tree payloads :
  letP? res := initialize_level_tree_when_needed level_tree_history
    inbox_value level_tree payloads in True.
Proof.
  unfold initialize_level_tree_when_needed.
  step; [hauto l: on |].
  step.
  { apply Error.split_letP with (P:=(fun _True)); [hauto lq: on |].
    intros.
    step.
    eapply Error.split_letP;
      [apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
    intros.
    hauto l: on.
  }
  { simpl.
    eapply Error.split_letP;
      [apply Sc_rollup_inbox_merkelized_payload_hashes_repr.genesis_is_valid |].
    intros.
    hauto l: on.
  }
Qed.

[archive_if_needed] is valid.
Lemma archive_if_needed_is_valid level_tree_history history_value
  inbox_value new_level level_tree payloads :
  letP? res := archive_if_needed level_tree_history history_value
    inbox_value new_level level_tree payloads in True.
Proof.
  unfold archive_if_needed.
  step. {
    step; [hauto l: on |].
    eapply Error.split_letP;
      [apply initialize_level_tree_when_needed_is_valid | hauto l: on].
  }
  { apply Error.split_letP with (P:=(fun _True));
      [apply form_history_proof_is_valid |].
    intros.
    step.
    eapply Error.split_letP;
      [apply initialize_level_tree_when_needed_is_valid | hauto l: on].
  }
Qed.

[add_messages] is valid.
Lemma add_messages_is_valid level_tree_history history_value inbox_value
  level payloads level_tree :
  letP? res := add_messages level_tree_history history_value inbox_value
  level payloads level_tree in True.
Proof.
  unfold add_messages.
  apply Error.split_letP with (P:=(fun _True)); [hauto l: on |].
  intros.
  apply Error.split_letP with (P:=(fun _True)).
  { cbn.
    unfold error_when.
    step; reflexivity.
  }
  { intros.
    eapply Error.split_letP; [apply archive_if_needed_is_valid |].
    intros.
    do 4 step.
    apply Error.split_letP with (P:=(fun _True)).
    { admit.
@TODO induction by payloads with generalization
    }
    { intros.
      hauto l: on.
    }
Admitted.

[add_messages_no_history] is valid.
Lemma add_messages_no_history_is_valid
  inbox_value level payloads level_tree :
  letP? res := add_messages_no_history inbox_value level
                 payloads level_tree in True.
Proof.
  unfold add_messages_no_history.
  unfold Result_syntax.op_letplus.
  apply Error.split_letP with (P:=(fun _True)).
  apply add_messages_is_valid.
  intros.
  reflexivity.
Qed.

[verify_proof] is valid.