🗂️ Indexable.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Indexable.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Module Valid.
  Definition t {a : Set} (x : Indexable.t a) : Prop :=
    match x with
    | Indexable.Value _ | Indexable.Hidden_value _ ⇒ True
    | Indexable.Index index | Indexable.Hidden_index index ⇒
      Int32.Valid.non_negative index
    end.
End Valid.

Module Index.
  Module Valid.
    Definition t {a : Set} (x : Indexable.t a) : Prop :=
      match x with
      | Indexable.Index _ ⇒ Valid.t x
      | _ ⇒ False
      end.
  End Valid.
End Index.

Module Value.
  Module Valid.
    Definition t {a : Set} (x : Indexable.t a) : Prop :=
      match x with
      | Indexable.Value _ ⇒ Valid.t x
      | _ ⇒ False
      end.
  End Valid.
End Value.

Two elements are said equivalent if they are equal once we forget about their hidden status.

Definition eq_forgetting_hidden {a : Set} (i1 i2 : Indexable.t a) : Prop :=
  Indexable.forget i1 = Indexable.forget i2.

[destruct] does not depend on the hidden status.

Lemma destruct_forgets_hidden {a : Set} (i1 i2 : Indexable.t a) :
  eq_forgetting_hidden i1 i2 →
  Indexable.destruct i1 = Indexable.destruct i2.
Proof.
  sauto q: on.
Qed.

[forget] does not depend on the hidden status.

Lemma forget_forgets_hidden {a : Set} (i1 i2 : Indexable.t a) :
  eq_forgetting_hidden i1 i2 →
  Indexable.forget i1 = Indexable.forget i2.
Proof.
  sauto q: on.
Qed.

Lemma encoding_is_valid {a : Set} (val_encoding : Data_encoding.t a) :
  Data_encoding.Valid.t (fun _ ⇒ True) val_encoding →
  Data_encoding.Valid.t Valid.t (Indexable.encoding val_encoding).
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[in_memory_size] does not depend on the hidden status.

Lemma in_memory_size_forgets_hidden {a : Set} ims (i1 i2 : Indexable.t a) :
  eq_forgetting_hidden i1 i2 →
  Indexable.in_memory_size ims i1 = Indexable.in_memory_size ims i2.
Proof.
  sauto q: on.
Qed.

[size_value] does not depend on the hidden status.

Lemma size_value_forgets_hidden {a : Set} ims (i1 i2 : Indexable.t a) :
  eq_forgetting_hidden i1 i2 →
  Indexable.size_value ims i1 = Indexable.size_value ims i2.
Proof.
  sauto q: on.
Qed.

The [compare] function is valid and forgets about the hidden status.

Lemma compare_is_valid {a : Set} (c_value : a → a → int) :
  Compare.Valid.t (fun _ ⇒ True) id c_value →
  Compare.Valid.t (fun _ ⇒ True) Indexable.forget (Indexable.compare c_value).
Proof.
  intros H.
  apply (Compare.equality (
    let proj_value x :=
      match x with
      | Indexable.Hidden_value x | Indexable.Value x ⇒ Some x
      | _ ⇒ None
      end in
    let proj_index x :=
      match x with
      | Indexable.Hidden_index x | Indexable.Index x ⇒ Some x
      | _ ⇒ None
      end in
    let proj x :=
      (proj_value x, proj_index x) in
    Compare.projection proj (
      Compare.lexicographic
        (Compare.Option.compare c_value) (Compare.Option.compare Int32.compare)
    )
  )); [intros [] [] **; cbn; try (now destruct c_value); reflexivity |].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    eapply Compare.lexicographic_is_valid; eapply Compare.option_is_valid; [
      apply H |
      apply Compare.int32_is_valid
    ].
  }
  all: hauto drew: off.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma compare_values_is_valid {a : Set} (c_value : a → a → int) :
  Compare.Valid.t (fun _ ⇒ True) id c_value →
  Compare.Valid.t Value.Valid.t id (Indexable.compare_values c_value).
Proof.
  intros H.
  apply (Compare.equality (
    let proj x :=
      match x with
      | Indexable.Value x ⇒ Some x
      | _ ⇒ None
      end in
    Compare.projection proj (Compare.Option.compare c_value)
  )); [sauto lq: on rew: off|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    eapply Compare.option_is_valid.
    apply H.
  }
  all: intros [] []; unfold id; sfirstorder.
Qed.
#[global] Hint Resolve compare_values_is_valid : Compare_db.

Lemma compare_indexes_is_valid {a : Set} :
  Compare.Valid.t Index.Valid.t id (Indexable.compare_indexes (a := a)).
Proof.
  apply (Compare.equality (
    let proj x :=
      match x with
      | Indexable.Index x ⇒ Some x
      | _ ⇒ None
      end in
      Compare.projection proj (Compare.Option.compare (Compare.Int32.(Compare.S.compare)))
  )); [sauto lq: on rew: off|].
  eapply Compare.implies.
  {
    eapply Compare.projection_is_valid.
    eapply Compare.option_is_valid.
    apply Compare.int32_is_valid.
  }
  all: intros [] []; unfold id; hauto l: on.
Qed.
#[global] Hint Resolve compare_indexes_is_valid : Compare_db.

Module VALUE.
  Module Valid.
    Import TezosOfOCaml.Proto_alpha.Indexable.VALUE.

    Record t {t : Set} (V : Indexable.VALUE (t := t)) : Prop := {
      encoding : Data_encoding.Valid.t (fun _ ⇒ True) V.(encoding);
      compare : Compare.Valid.t (fun _ ⇒ True) id V.(compare);
    }.
  End Valid.
End VALUE.

Module INDEXABLE.
  Module Valid.
    Import TezosOfOCaml.Proto_alpha.Indexable.INDEXABLE.

    Record t {v_t : Set} (I : Indexable.INDEXABLE (v_t := v_t)) : Prop := {
      encoding : Data_encoding.Valid.t Valid.t I.(encoding);
      index_encoding : Data_encoding.Valid.t Index.Valid.t I.(index_encoding);
      value_encoding : Data_encoding.Valid.t Value.Valid.t I.(value_encoding);
      compare : Compare.Valid.t (fun _ ⇒ True) Indexable.forget I.(compare);
      compare_values : Compare.Valid.t Value.Valid.t id I.(compare_values);
    }.
  End Valid.
End INDEXABLE.

Lemma Make_is_valid {t : Set} (V : Indexable.VALUE (t := t)) :
  VALUE.Valid.t V → INDEXABLE.Valid.t (Indexable.Make V).
Proof.
  intro H.
  constructor.
  { apply encoding_is_valid.
    apply H.
  }
  { Data_encoding.Valid.data_encoding_auto.
    intros [] ?; simpl in *; try easy.
    split; lia.
  }
  { Data_encoding.Valid.data_encoding_auto; try apply H.
    hauto l: on.
  }
  { apply compare_is_valid.
    apply H.
  }
  {
    apply compare_values_is_valid.
    apply H.
  }
Qed.