🧠 Cache_memory_helpers.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
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].

  Module Valid.
    Definition t (x : Cache_memory_helpers.nodes_and_size) : Prop :=
      let '(nodes, size) := x in
      Pervasives.Int.Valid.t nodes ∧ Saturation_repr.Valid.t size.
  End Valid.
End nodes_and_size.

Lemma blake2b_hash_size_is_valid
  : Saturation_repr.Valid.t
      Cache_memory_helpers.blake2b_hash_size.
  now apply Saturation_repr.Valid.decide.
Qed.

Lemma public_key_hash_in_memory_size_is_valid
  : Saturation_repr.Valid.t
      Cache_memory_helpers.public_key_hash_in_memory_size.
  now apply Saturation_repr.Valid.decide.
Qed.

The function [node_size] is valid.

Lemma node_size_is_valid {A B : Set} node :
  let '(nb, size) := Cache_memory_helpers.node_size (A := A) (B := B) node in
  Pervasives.Int.Valid.t nb ∧ Saturation_repr.Valid.t size.
Proof.
Admitted.