🍃 TzEndian.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.

Axiom get_int32_is_valid : ∀ b index,
  index + 4 ≤ Bytes.length b →
  Int32.Valid.t (TzEndian.get_int32 b index).