🍃 TzEndian.v
Proofs
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).
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).