📜 Bounded_history_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.

Module Make.
  Import Bounded_history_repr.

Assume validity of the key encoding

  Axiom key_encoding_id_valid : ∀ {key value : Set}
    `{Make.FArgs (Key_t := key) (Value_t := value)},
    Data_encoding.Valid.t (fun _ ⇒ True) Make.Key.(KEY.encoding).
  #[global] Hint Resolve key_encoding_id_valid : Data_encoding_db.

Assume validity of the value encoding

  Axiom value_encoding_id_valid : ∀ {key value : Set}
    `{Make.FArgs (Key_t := key) (Value_t := value)},
    Data_encoding.Valid.t (fun _ ⇒True) Make.Value.(VALUE.encoding).
  #[global] Hint Resolve value_encoding_id_valid : Data_encoding_db.

The validity predicate for [Make.t]

  Module Valid.
    Record t {key value : Set}
      `{Make.FArgs (Key_t := key) (Value_t := value)}
      (x : Make.t) : Prop := {
        events : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
          Make.compare_keys k2 k1 = Datatypes.Gt) x.(Make.t.events);
        keys : Forall (fun '(k, _) ⇒ Int64.Valid.t k)
          (Make.Int64_map.(S.bindings) x.(Make.t.sequence));
        capacity : Int64.Valid.t x.(Make.t.capacity);
        index : Int64.Valid.t x.(Make.t.next_index);
        oldest_index : Int64.Valid.t x.(Make.t.oldest_index);
        size : Int64.Valid.t x.(Make.t.size);
        sequence : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
          Int64.compare k1 k2 = -1) x.(Make.t.sequence);
      }.
  End Valid.

[encoding_is_valid]

  Lemma encoding_is_valid {key value : Set}
    `{Make.FArgs (Key_t := key) (Value_t := value)} :
    Data_encoding.Valid.t Valid.t
      Bounded_history_repr.Make.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros [x] H_Valid.
    repeat match goal with
    | |- _ ∧ _ ⇒ split
    end; try apply H_Valid; try f_equal.
    { unfold Make.Int64_map, Make.Map in *;
      with_strategy transparent [Map.Make] unfold Map.Make in *;
      cbn in *; unfold Make.bindings in *;
      unfold Map.Make.empty;
      destruct H_Valid; cbn in ×.
      induction x; [constructor|].
      constructor.
      { step; easy. }
      { apply IHx. now inversion events. }
    }
    { unfold Make.Int64_map, Make.Map in *;
        with_strategy transparent [Map.Make] unfold Map.Make in *;
        cbn in *; unfold Make.bindings, Map.Make.empty in *; cbn in ×.
      apply Map.add_seq_node_to_seq_node_eq.
      apply H_Valid.
    }
    { unfold Make.Int64_map, Make.Map in *;
      with_strategy transparent [Map.Make] unfold Map.Make in *;
      cbn in *; unfold Make.bindings in *;
      unfold Map.Make.empty;
      destruct H_Valid; cbn in ×.
      induction sequence; constructor; fcrush. }
    { epose proof (Map.bindings_of_bindings)
        as H_bindings_of_bindings.
      unfold Make.Int64_map, Make.Map in *; cbn.
        with_strategy transparent [Map.Make] unfold Map.Make in *;
        cbn in ×.
      rewrite Map.make_bindings_rev_eq.
      unfold Make.bindings, Map.of_bindings in ×.
      with_strategy transparent [Map.Make] unfold Map.Make in *;
        cbn in *; unfold Map.Make.empty in ×.
      rewrite <- fold_left_rev_right, <- List.fold_right_eq.
      rewrite List.rev_eq, rev_involutive.
      match goal with
      | |- context [fold_right ?f _ _] ⇒
          let t := type of H_bindings_of_bindings in
          match t with
          | context [fold_right ?f' _ _] ⇒
              assert (H_f_ext : f = f')
          end
      end.
      { do 2 (apply FunctionalExtensionality.functional_extensionality;
          intro).
        now step.
      }
      rewrite H_f_ext in ×.
      apply Map.bindings_of_bindings.
      apply H_Valid.
    }
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[Bounded_history_repr.Make.remember] is valid.

  Lemma remember_is_valid `{Make.FArgs}
    key_value value_value t_value :
    letP? res :=
      Bounded_history_repr.Make.remember key_value value_value t_value in True.
  Proof.
  Admitted.

End Make.