🪜 Raw_level_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.Raw_level_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int32.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

#[global] Hint Unfold
  Raw_level_repr.to_int32
  : tezos_z.

Module Valid.
  Definition t (i : Raw_level_repr.t) : Prop :=
    0 ≤ i ≤ Int32.max_int.
  #[global] Hint Unfold t : tezos_z.
End Valid.

[compare] function is valid

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

Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Raw_level_repr.rpc_arg.
  constructor; intros; simpl.
  { now rewrite Int32.of_string_opt_to_string. }
  { assert (H := Int32.to_string_of_string_opt s).
    now destruct (Int32.of_string_opt _).
  }
Qed.

Lemma root_is_valid : Valid.t Raw_level_repr.root_value.
Proof.
  easy.
Qed.

Axiom succ_is_valid : ∀ {l : Raw_level_repr.t},
  Valid.t l → Valid.t (Raw_level_repr.succ l).

Axiom pred_is_valid : ∀ {l : Raw_level_repr.t},
  Valid.t l →
  match Raw_level_repr.pred l with
  | Some l' ⇒ Valid.t l'
  | None ⇒ True
  end.

Lemma of_int32_is_valid (i : int32) :
  Int32.Valid.t i →
  match Raw_level_repr.of_int32 i with
  | Pervasives.Ok l ⇒ Valid.t l
  | Pervasives.Error _ ⇒ True
  end.
  unfold Raw_level_repr.of_int32; simpl.
  destruct (_ >=? _) eqn:?; simpl; trivial.
  autounfold with tezos_z; lia.
Qed.

Lemma of_int32_to_int32 {l : Raw_level_repr.t}
  : Valid.t l →
    Raw_level_repr.of_int32 (Raw_level_repr.to_int32 l) = Pervasives.Ok l.
  unfold Raw_level_repr.of_int32, Raw_level_repr.to_int32.
  autounfold with tezos_z; simpl.
  destruct (_ >=? _) eqn:?; [reflexivity | lia].
Qed.

Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t Raw_level_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  rewrite of_int32_to_int32; autounfold with tezos_z in *; intuition lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module Index.

[compare] function is valid

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

Lemma Index_Path_is_valid
  : Path_encoding.S.Valid.t
      (Storage_description.INDEX.to_Path Raw_level_repr.Index).
  constructor; intros; try reflexivity; cbv;
    try apply Int32.of_string_opt_to_string.
  destruct path as [|s[]]; trivial.
  assert (H_eq := Int32.to_string_of_string_opt s).
  destruct (Int32.of_string_opt s); congruence.
Qed.

Lemma Index_is_valid
  : Storage_description.INDEX.Valid.t Valid.t Raw_level_repr.Index.
  constructor; [
    exact Index_Path_is_valid |
    exact rpc_arg_is_valid |
    exact encoding_is_valid |
    exact Compare.int32_is_valid
  ].
Qed.