🎰 Slot_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Slot_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.

Module Valid.
  Definition t (s : Slot_repr.t) : Prop :=
    0 ≤ s ≤ Pervasives.UInt16.max.
  #[global] Hint Unfold t : tezos_z.
End Valid.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Slot_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma zero_is_valid : Valid.t Slot_repr.zero.
  easy.
Qed.

Lemma max_value_is_valid : Valid.t Slot_repr.max_value.
  easy.
Qed.

Lemma max_value_eq : Slot_repr.max_value = Pervasives.UInt16.max.
  reflexivity.
Qed.

Lemma of_int_eq : ∀ i,
  Valid.t i →
  Slot_repr.of_int i = return? i.
  unfold Slot_repr.of_int.
  rewrite max_value_eq.
  autounfold with tezos_z.
  intros.
  destruct (_ || _) eqn:?; [| reflexivity ].
  rewrite Bool.orb_true_iff in ×.
  hauto q: on solve: lia.
Qed.

Lemma succ_is_valid : ∀ s,
  Valid.t s →
  s ≠ Pervasives.UInt16.max →
  match Slot_repr.succ s with
  | Pervasives.Ok s ⇒ Valid.t s
  | Pervasives.Error _ ⇒ True
  end.
  intros; unfold Slot_repr.succ.
  assert (Valid.t (s +i 1)) by
    (repeat (autounfold with tezos_z in *; unfold normalize_int);
    lia).
  now rewrite of_int_eq.
Qed.

Module Range.
  Module Interval.
    Import Slot_repr.Range.t.Interval.

    Record t (v : Slot_repr.Range.t.Interval) : Prop := {
      lo : Slot_repr.Valid.t v.(lo);
      hi : Slot_repr.Valid.t v.(hi);
    }.
  End Interval.

  Module Valid.
    Definition t (v : Slot_repr.Range.t) : Prop :=
      match v with
      | Slot_repr.Range.Interval i ⇒ Interval.t i
      end.
  End Valid.
End Range.