🍬 Script_typed_ir_size.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.

Require TezosOfOCaml.Proto_alpha.Proofs.Cache_memory_helpers.

The function [value_size] is valid.

Lemma value_size_is_valid {A : Set} ty_value (x_value : A) :
  Cache_memory_helpers.nodes_and_size.Valid.t
    (Script_typed_ir_size.value_size ty_value x_value).
Proof.
Admitted.