Skip to main content

🧠 Cache_memory_helpers.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

Module nodes_and_size.
The validity of the type [nodes_and_size].
The function [node_size] is valid.
Lemma node_size_is_valid node :
  let '(nb, size) := Cache_memory_helpers.node_size node in
  Pervasives.Int.Valid.t nb Saturation_repr.Valid.t size.
Proof.
Admitted.