Skip to main content

➰ Cycle_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.Cycle_repr.

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

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

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

Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Cycle_repr.rpc_arg.
  apply RPC_arg.Valid.like.
  eapply RPC_arg.Valid.implies; [apply RPC_arg.Valid.uint31|].
  autounfold with tezos_z; simpl.
  lia.
Qed.

Lemma compare_is_valid : Compare.Valid.t (fun _True) id Cycle_repr.compare.
Proof.
  apply Compare.int32_is_valid.
Qed.

Lemma Index_is_valid
  : Storage_description.INDEX.Valid.t Valid.t Cycle_repr.Index.
Proof.
  constructor.
  { constructor; try reflexivity.
    { cbv.
      apply Int32.of_string_opt_to_string.
    }
    { cbv - [length].
      intro path.
      destruct path as [|s[]]; trivial.
      assert (H_s := Int32.to_string_of_string_opt s).
      destruct (Int32.of_string_opt s); congruence.
    }
  }
  { apply rpc_arg_is_valid. }
  { Data_encoding.Valid.data_encoding_auto.
    autounfold with tezos_z; lia.
  }
  { apply compare_is_valid. }
Qed.

Module Index.
[compare] function is valid
  Lemma compare_is_valid : Compare.Valid.t (fun _True) id Cycle_repr.compare.
  Proof.
    apply Index_is_valid.
  Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Index.