Skip to main content

🍃 RPC_arg.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Int32.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.

Module Valid.
  Record t {a : Set} {domain : a Prop} {arg : RPC_arg.t a} : Prop := {
    destruct_construct v :
      domain v
      arg.(RPC_arg.t.destruct) (arg.(RPC_arg.t.construct) v) =
      Pervasives.Ok v;
    construct_destruct s :
      match arg.(RPC_arg.t.destruct) s with
      | Pervasives.Ok varg.(RPC_arg.t.construct) v = s
      | Pervasives.Error _True
      end;
  }.
  Arguments t {_}.

  Lemma implies {a : Set} {domain domain' : a Prop} {arg : RPC_arg.t a}
    : t domain arg
      ( x, domain' x domain x)
      t domain' arg.
    intros H H_implies; constructor; intros; apply H; now try apply H_implies.
  Qed.

  Axiom bool_value : t (fun _True) RPC_arg.bool_value.

  Axiom int_value : t Pervasives.Int.Valid.t RPC_arg.int_value.

  Axiom uint : t Pervasives.Int.Valid.non_negative RPC_arg.uint.

  Axiom int32_value : t Int32.Valid.t RPC_arg.int32_value.

  Axiom uint31 : t Int32.Valid.non_negative RPC_arg.uint31.

  Axiom int64_value : t Int64.Valid.t RPC_arg.int64_value.

  Axiom uint63 : t Int64.Valid.non_negative RPC_arg.uint63.

  Axiom string_value : t (fun _True) RPC_arg.string_value.

  Axiom option_value : {a : Set} (domain : a Prop) arg,
    t domain arg
    let option_domain x :=
      match x with
      | NoneTrue
      | Some xdomain x
      end in
    t option_domain (RPC_arg.option_value arg).

    Axiom list_value : {a : Set} (domain : a Prop) arg,
      t domain arg
      let list_domain x :=
        List.Forall domain x in
      t list_domain (RPC_arg.list_value arg).

  Axiom like : {a : Set} {domain} {arg : RPC_arg.t a} {description name},
    t domain arg t domain (RPC_arg.like arg description name).
End Valid.

Ltac valid_auto :=
  repeat first [
    apply Valid.bool_value |
    apply Valid.int_value |
    apply Valid.uint |
    apply Valid.int32_value |
    apply Valid.uint31 |
    apply Valid.int64_value |
    apply Valid.uint63 |
    apply Valid.string_value |
    apply Valid.option_value |
    apply Valid.list_value |
    apply Valid.like
  ].