✒️ Contract_services.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_services.

Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Environment.V8.Proofs.Micheline.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

Module Info.
  Module Valid.
    Import Contract_services.info.

    Record t (x : Contract_services.info) : Prop := {
      balance : Tez_repr.Valid.t x.(balance);
      counter : Option.Forall (fun n ⇒ 0 ≤ n) x.(counter);
    }.
  End Valid.
End Info.

Lemma info_encoding_is_valid
  : Data_encoding.Valid.t Info.Valid.t Contract_services.info_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros ? []; hauto l: on.
Qed.

Module S.
  Lemma balance_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
      Contract_services.S.balance.
    RPC_service.rpc_auto.
  Qed.

  Lemma manager_key_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.manager_key.
    RPC_service.rpc_auto.
  Qed.

  Lemma delegate_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.delegate.
    RPC_service.rpc_auto.
  Qed.

  Lemma counter_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True)
      (fun (x : Alpha_context.Manager_counter.t) ⇒ x ≥ 0)
      Contract_services.S.counter.
    RPC_service.rpc_auto.
    intros.
    lia.
  Qed.

  Lemma script_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.script.
    RPC_service.rpc_auto.
  Qed.

  Lemma storage_value_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.storage_value.
    RPC_service.rpc_auto.
  Qed.

  Lemma entrypoint_type_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.entrypoint_type.
    RPC_service.rpc_auto.
  Qed.

  Lemma list_entrypoints_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.list_entrypoints.
    RPC_service.rpc_auto.
    intros x H. simpl. destruct x. split.
    { apply List.Forall_True. intro x.
      apply List.Forall_True. constructor. }
    { apply List.Forall_True. constructor. }
  Qed.

  Lemma contract_big_map_get_opt_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.contract_big_map_get_opt.
    RPC_service.rpc_auto.
  Qed.

  Lemma big_map_get_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.big_map_get.
    RPC_service.rpc_auto.
  Qed.

  Module Big_map_get_all_query.
    Module Valid.
      Import Contract_services.S.big_map_get_all_query.

      Record t (x : Contract_services.S.big_map_get_all_query) : Prop := {
        offset : Option.Forall Pervasives.Int.Valid.non_negative x.(offset);
        length : Option.Forall Pervasives.Int.Valid.non_negative x.(length);
      }.
    End Valid.
  End Big_map_get_all_query.

  Lemma rpc_arg_uint_is_valid :
    RPC_arg.Valid.t Pervasives.Int.Valid.non_negative
      Contract_services.S.rpc_arg_uint.
  Proof.
    constructor; intros; simpl.
    { rewrite Pervasives.int_of_string_opt_string_of_int by lia; simpl.
      destruct (_ <i 0) eqn:?; lia.
    }
    { hfcrush use: Pervasives.string_of_int_int_of_string_opt. }
  Qed.

The query [big_map_get_all_query_value] is valid.

  Lemma big_map_get_all_query_value_is_valid :
    RPC_query.Valid.t Big_map_get_all_query.Valid.t
      Contract_services.S.big_map_get_all_query_value.
  Proof.
    RPC_query.valid_auto; try apply rpc_arg_uint_is_valid; dtauto.
  Qed.

  Lemma big_map_get_all_is_valid :
    RPC_service.Valid.t
      Big_map_get_all_query.Valid.t (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.big_map_get_all.
    RPC_service.rpc_auto; try apply rpc_arg_uint_is_valid; try dtauto.
    intros; now apply List.Forall_True.
  Qed.

  Lemma info_value_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Info.Valid.t
      Contract_services.S.info_value.
    RPC_service.rpc_auto.
    sauto lq: on.
  Qed.

  Lemma list_value_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Contract_services.S.list_value.
    RPC_service.rpc_auto.
    intros; now apply List.Forall_True.
  Qed.
End S.