Skip to main content

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