🐆 Tx_rollup_gas.v

Proofs

See code, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.

Require TezosOfOCaml.Proto_alpha.Simulations.Tx_rollup_gas.

Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

The function [hash_cost] is valid.

Lemma hash_cost_is_valid input_size :
  letP? cost := Tx_rollup_gas.hash_cost input_size in
  Saturation_repr.Valid.t cost.
Proof.
  unfold Tx_rollup_gas.hash_cost.
  destruct (_ ≤i _); simpl; [|easy].
  apply Saturation_repr.add_is_valid.
Qed.

[Simulations.Tx_rollup_gas.check_path_cost] is equal to [check_path_cost].

#[bypass_check(guard)]
Lemma check_path_cost_eq element_size path_depth :
  Pervasives.Int.Valid.t path_depth →
  0 ≤ path_depth →
  Proto_alpha.Tx_rollup_gas.check_path_cost element_size path_depth =
  Simulations.Tx_rollup_gas.check_path_cost element_size (Z.to_nat path_depth).
Proof.
  intros Hv Hnn.
  rewrite <- (Z2Nat.id _ Hnn) in Hv.
  rewrite <- (Z2Nat.id _ Hnn) at 1.
  unfold Proto_alpha.Tx_rollup_gas.check_path_cost.
  unfold Simulations.Tx_rollup_gas.check_path_cost.
  apply Error.let_ext; [reflexivity| intros _].
  apply Error.let_ext; [reflexivity| intro gas1].
  apply Error.let_ext; [reflexivity| intro gas2].
  repeat f_equal.
  generalize Tx_rollup_gas.compare_blake2b_hash.
  induction (Z.to_nat path_depth); [reflexivity|intro; simpl].
  rewrite <- IHn; [|lia].
  f_equal.
  unfold "-i".
  rewrite Pervasives.normalize_identity; lia.
Qed.

The function [check_path_cost] is valid.

#[bypass_check(guard)]
Lemma check_path_cost_is_valid element_size path_depth :
  letP? cost := Proto_alpha.Tx_rollup_gas.check_path_cost element_size path_depth in
  Saturation_repr.Valid.t cost.
Proof.
  destruct (0 ≤i path_depth) eqn:Hpd;
  unfold Tx_rollup_gas.check_path_cost.
  { apply Error.split_letP_triv; [now rewrite Hpd |].
    intros _.
    do 2 Error.split_error_with hash_cost_is_valid.
    apply Saturation_repr.add_is_valid.
  }
  { apply Error.split_letP with (P := fun _ ⇒ False).
    now rewrite Hpd.
    intros _ [].
  }
Qed.

The function [consume_check_path_inbox_cost] is valid.

Lemma consume_check_path_inbox_cost_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Tx_rollup_gas.consume_check_path_inbox_cost ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  unfold Tx_rollup_gas.consume_check_path_inbox_cost.
  Error.split_error_with check_path_cost_is_valid.
  now apply Raw_context.consume_gas_is_valid.
Qed.

The function [consume_check_path_commitment_cost] is valid.

Lemma consume_check_path_commitment_cost_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Tx_rollup_gas.consume_check_path_commitment_cost ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  unfold Tx_rollup_gas.consume_check_path_commitment_cost.
  Error.split_error_with check_path_cost_is_valid.
  now apply Raw_context.consume_gas_is_valid.
Qed.

The function [model_inbox_add_message_codegen] is valid.

Lemma model_inbox_add_message_codegen_is_valid inbox_length :
  Saturation_repr.Valid.t (Tx_rollup_gas.model_inbox_add_message_codegen inbox_length).
Proof.
  unfold Tx_rollup_gas.model_inbox_add_message_codegen.
  apply Saturation_repr.mul_is_valid; [easy|].
  apply Saturation_repr.safe_int_is_valid.
Qed.

The function [consume_add_message_cost] is valid.

Lemma consume_add_message_cost_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Tx_rollup_gas.consume_add_message_cost ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  unfold Tx_rollup_gas.consume_add_message_cost.
  apply Raw_context.consume_gas_is_valid; [assumption|].
  apply model_inbox_add_message_codegen_is_valid.
Qed.

The function [model_commitment_full_compact] is valid.

Lemma model_commitment_full_compact_is_valid inbox_length :
  Saturation_repr.Valid.t (Tx_rollup_gas.model_commitment_full_compact inbox_length).
Proof.
  apply Saturation_repr.mul_is_valid; [easy|].
  apply Saturation_repr.safe_int_is_valid.
Qed.

The function [consume_compact_commitment] is valid.

Lemma consume_compact_commitment_cost_is_valid ctxt inbox_length :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Tx_rollup_gas.consume_compact_commitment_cost ctxt inbox_length in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  apply Raw_context.consume_gas_is_valid; [auto|].
  apply model_commitment_full_compact_is_valid.
Qed.

The function [hash_value] is valid.

Lemma hash_value_is_valid {A B : Set} domain hash_f ctxt encoding input :
  Raw_context.Valid.t ctxt →
  Data_encoding.Valid.t domain encoding →
  domain input →
  letP? '(ctxt, _) :=
    Tx_rollup_gas.hash_value (A := A) (B := B) hash_f ctxt encoding input in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt H_encoding H_input.
  unfold Tx_rollup_gas.hash_value.
  destruct H_encoding.
  pose proof (of_bytes_opt_to_bytes_opt input H_input).
  destruct Binary.to_bytes_opt; simpl; [|contradiction].
  eapply Error.split_letP. {
    apply hash_cost_is_valid.
  }
  intros cost H_cost.
  eapply Error.split_letP. {
    now apply Raw_context.consume_gas_is_valid.
  }
  trivial.
Qed.