🦏 Sc_rollup_costs.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_costs.

Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

Module Constants.

The constant [cost_serialize_commitment] is valid

  Lemma cost_serialize_commitment_is_valid :
    Saturation_repr.Valid.t
      Sc_rollup_costs.Constants.cost_serialize_commitment.
  Proof.
    unfold Sc_rollup_costs.Constants.cost_serialize_commitment,
      Sc_rollup_costs.S_syntax.op_plus,
      Sc_rollup_costs.S.add.
    step; lia.
  Qed.

The function [cost_hash_bytes] is valid

  Lemma cost_hash_bytes_is_valid b :
    Saturation_repr.Valid.t
      (Sc_rollup_costs.cost_hash_bytes (V8.Bytes.length b)).
  Proof.
    unfold Sc_rollup_costs.cost_hash_bytes.
    unfold Sc_rollup_costs.S_syntax.op_plus.
    unfold Sc_rollup_costs.S.add.
    do 2 step; lia.
  Qed.
End Constants.