🍬 Script_typed_ir_size_costs.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
The function [nodes_cost] is valid.
Lemma nodes_cost_is_valid nodes :
Pervasives.Int.Valid.t nodes →
Saturation_repr.Valid.t
(Script_typed_ir_size_costs.nodes_cost nodes).
Proof.
Admitted.
Pervasives.Int.Valid.t nodes →
Saturation_repr.Valid.t
(Script_typed_ir_size_costs.nodes_cost nodes).
Proof.
Admitted.