🚪 Entrypoint_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.Entrypoint_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Proofs.Non_empty_string.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.

Module Valid.
  Definition t (s : string) : Prop :=
    s ≠ "" ∧ String.length s ≤ 31.
End Valid.

Module Pre_entrypoint.
  Lemma of_non_empty_string_eq s :
    Valid.t s →
    Pre_entrypoint.of_non_empty_string s = Some s.
    unfold Valid.t, Pre_entrypoint.of_non_empty_string.
    step; simpl in *; [lia | trivial].
  Qed.
End Pre_entrypoint.

[compare] function is valid

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Entrypoint_repr.compare.
Proof.
  apply Non_empty_string.compare_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma default_eq : Entrypoint_repr.default = "default".
  reflexivity.
Qed.

Lemma is_default_is_valid s :
  Entrypoint_repr.is_default s = true ↔
  s = "default".
  cbn; split; intro H.
  { apply Compare.string_is_valid; trivial; simpl.
    lia.
  }
  { rewrite H.
    erewrite Compare.Valid.refl;
      try apply Compare.string_is_valid;
      simpl; trivial.
  }
Qed.

[of_annot_lax_opt] returns [Some s] when [s] is valid

Lemma of_annot_lax_opt_eq s :
  Valid.t s →
  of_annot_lax_opt s = Some s.
Proof.
  unfold Valid.t, of_annot_lax_opt, of_string; intros.
  unfold of_non_empty_string.
  rewrite Pre_entrypoint.of_non_empty_string_eq by easy.
  destruct (is_default _) eqn:?; trivial.
  now rewrite (proj1 (is_default_is_valid s)).
Qed.

Lemma of_string_lax_opt_eq s :
  Valid.t s →
  of_string_lax_opt s = Some s.
Proof.
  unfold Valid.t, of_string_lax_opt, of_string; intros.
  rewrite Non_empty_string.of_string_eq by easy.
  unfold of_non_empty_string.
  rewrite Pre_entrypoint.of_non_empty_string_eq by easy.
  destruct (is_default _) eqn:?; trivial.
  now rewrite (proj1 (is_default_is_valid s)).
Qed.

Lemma of_string_lax_eq s :
  Valid.t s →
  of_string_lax s = return? s.
  unfold of_string_lax; intros.
  now rewrite of_string_lax_opt_eq.
Qed.

[of_annot_lax] returns [Pervasives.Ok s] when [s] is valid

Lemma of_annot_lax_eq s :
  Valid.t s →
  of_annot_lax s = return? s.
Proof.
  unfold Valid.t, of_annot_lax, of_string; intros.
  unfold of_non_empty_string.
  rewrite Pre_entrypoint.of_non_empty_string_eq by easy.
  destruct (is_default _) eqn:?; trivial.
  now rewrite (proj1 (is_default_is_valid s)).
Qed.

Lemma of_string_lax'_eq s :
  Valid.t s →
  of_string_lax' s = return? s.
  unfold of_string_lax'; intros.
  now rewrite of_string_lax_opt_eq.
Qed.

Lemma of_string_lax_exn_eq s :
  Valid.t s →
  of_string_lax_exn s = s.
  unfold of_string_lax_exn; intros.
  now rewrite of_string_lax'_eq.
Qed.

Lemma root_eq : Entrypoint_repr.root_value = "root".
Proof.
  reflexivity.
Qed.

Lemma do_eq : Entrypoint_repr.do_ = "do".
Proof.
  reflexivity.
Qed.

Lemma set_delegate_eq : Entrypoint_repr.set_delegate = "set_delegate".
Proof.
  reflexivity.
Qed.

Lemma remove_delegate_eq : Entrypoint_repr.remove_delegate = "remove_delegate".
Proof.
  reflexivity.
Qed.

Lemma simple_encoding_is_valid :
  Data_encoding.Valid.t Valid.t Entrypoint_repr.simple_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros; now rewrite of_string_lax'_eq.
Qed.
#[global] Hint Resolve simple_encoding_is_valid : Data_encoding_db.

Lemma value_encoding_is_valid :
  Data_encoding.Valid.t Valid.t Entrypoint_repr.value_encoding.
  Data_encoding.Valid.data_encoding_auto.
  unfold Valid.t; intros s ?.
  unfold of_string_strict', of_string.
  destruct (is_default _) eqn:H_default; simpl.
  { now rewrite (proj1 (is_default_is_valid s)). }
  { rewrite Non_empty_string.of_string_eq by tauto.
    unfold of_non_empty_string.
    rewrite Pre_entrypoint.of_non_empty_string_eq by trivial.
    now rewrite H_default.
  }
Qed.
#[global] Hint Resolve value_encoding_is_valid : Data_encoding_db.

Lemma smart_encoding_is_valid :
  Data_encoding.Valid.t Valid.t Entrypoint_repr.smart_encoding.
  Data_encoding.Valid.data_encoding_auto.
  unfold Valid.t; intros.
  cbn.
  repeat (
    destruct (_ =? 0) eqn:H_eq; [
      split; [easy|];
      apply Compare.string_is_valid; trivial;
        rewrite Compare.string_is_valid.(Compare.Valid.sym);
        simpl; lia
    |];
    clear H_eq
  ).
  split; [lia|].
  now rewrite of_string_lax_exn_eq.
Qed.
#[global] Hint Resolve smart_encoding_is_valid : Data_encoding_db.

The [rpc_arg] is valid

(* @TODO https://gitlab.com/formal-land/coq-tezos-of-ocaml/-/issues/377 *)
Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Entrypoint_repr.rpc_arg.
Proof.
Admitted.

Lemma default_condition_implies parameter entrypoint :
  Script_repr.is_unit_parameter parameter &&
    (String.compare entrypoint "default" =? 0) = true →
  parameter = Script_repr.unit_parameter ∧
  entrypoint = "default".
  intros H; rewrite Bool.andb_true_iff in H; split.
  { now apply Script_repr.is_unit_parameter_implies_eq. }
  { apply Compare.string_is_valid; trivial.
    hauto q: on solve: lia.
  }
Qed.

Module T.

[compare] function is valid

  Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Entrypoint_repr.compare.
  Proof. Compare.valid_auto. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End T.