🍃 RPC_query.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.

Module Field.
  Module Valid.
    Import RPC_query.field.

    Record t {a b : Set} (domain : b → Prop) (f : RPC_query.field a b) :
      Prop := {
      ty : RPC_arg.Valid.t domain f.(ty);
    }.
  End Valid.
End Field.

We axiomatize the validity predicate, and state how to verify it by use cases. We will essentially verify that we provide a bijection to build the query.

Module Valid.
  Parameter t : ∀ {a : Set}, (a → Prop) → RPC_query.t a → Prop.
End Valid.

Axiom implies : ∀ {a : Set} (domain1 domain2 : a → Prop)
  (query : RPC_query.t a),
  Valid.t domain1 query →
  (∀ x, domain2 x → domain1 x) →
  Valid.t domain2 query.

Axiom empty : Valid.t (fun _ ⇒ True) RPC_query.empty.

Axiom seal1 : ∀ {a1 b : Set} (make : a1 → b)
  domain1 (f1 : RPC_query.field b a1),
  Field.Valid.t domain1 f1 →
  (∀ y,
    make
      (f1.(RPC_query.field.get) y) = y) →
  (∀ x1, f1.(RPC_query.field.get) (make x1) = x1) →
  let domain x :=
    domain1 (f1.(RPC_query.field.get) x) in
  Valid.t domain (
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.query_value make)
        f1)).

Axiom seal2 : ∀ {a1 a2 b : Set} (make : a1 → a2 → b)
  domain1 (f1 : RPC_query.field b a1)
  domain2 (f2 : RPC_query.field b a2),
  Field.Valid.t domain1 f1 →
  Field.Valid.t domain2 f2 →
  (∀ y,
    make
      (f1.(RPC_query.field.get) y)
      (f2.(RPC_query.field.get) y) = y) →
  (∀ x1 x2, f1.(RPC_query.field.get) (make x1 x2) = x1) →
  (∀ x1 x2, f2.(RPC_query.field.get) (make x1 x2) = x2) →
  let domain x :=
    domain1 (f1.(RPC_query.field.get) x) ∧
    domain2 (f2.(RPC_query.field.get) x) in
  Valid.t domain (
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.op_pipeplus
          (RPC_query.query_value make)
          f1)
        f2)).

Axiom seal3 : ∀ {a1 a2 a3 b : Set} (make : a1 → a2 → a3 → b)
  domain1 (f1 : RPC_query.field b a1)
  domain2 (f2 : RPC_query.field b a2)
  domain3 (f3 : RPC_query.field b a3),
  Field.Valid.t domain1 f1 →
  Field.Valid.t domain2 f2 →
  Field.Valid.t domain3 f3 →
  (∀ y,
    make
      (f1.(RPC_query.field.get) y)
      (f2.(RPC_query.field.get) y)
      (f3.(RPC_query.field.get) y) = y) →
  (∀ x1 x2 x3, f1.(RPC_query.field.get) (make x1 x2 x3) = x1) →
  (∀ x1 x2 x3, f2.(RPC_query.field.get) (make x1 x2 x3) = x2) →
  (∀ x1 x2 x3, f3.(RPC_query.field.get) (make x1 x2 x3) = x3) →
  let domain x :=
    domain1 (f1.(RPC_query.field.get) x) ∧
    domain2 (f2.(RPC_query.field.get) x) ∧
    domain3 (f3.(RPC_query.field.get) x) in
  Valid.t domain (
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.op_pipeplus
          (RPC_query.op_pipeplus
            (RPC_query.query_value make)
            f1)
          f2)
        f3)).

Axiom seal4 : ∀ {a1 a2 a3 a4 b : Set} (make : a1 → a2 → a3 → a4 → b)
  domain1 (f1 : RPC_query.field b a1)
  domain2 (f2 : RPC_query.field b a2)
  domain3 (f3 : RPC_query.field b a3)
  domain4 (f4 : RPC_query.field b a4),
  Field.Valid.t domain1 f1 →
  Field.Valid.t domain2 f2 →
  Field.Valid.t domain3 f3 →
  Field.Valid.t domain4 f4 →
  (∀ y,
    make
      (f1.(RPC_query.field.get) y)
      (f2.(RPC_query.field.get) y)
      (f3.(RPC_query.field.get) y)
      (f4.(RPC_query.field.get) y) = y) →
  (∀ x1 x2 x3 x4, f1.(RPC_query.field.get) (make x1 x2 x3 x4) = x1) →
  (∀ x1 x2 x3 x4, f2.(RPC_query.field.get) (make x1 x2 x3 x4) = x2) →
  (∀ x1 x2 x3 x4, f3.(RPC_query.field.get) (make x1 x2 x3 x4) = x3) →
  (∀ x1 x2 x3 x4, f4.(RPC_query.field.get) (make x1 x2 x3 x4) = x4) →
  let domain x :=
    domain1 (f1.(RPC_query.field.get) x) ∧
    domain2 (f2.(RPC_query.field.get) x) ∧
    domain3 (f3.(RPC_query.field.get) x) ∧
    domain4 (f4.(RPC_query.field.get) x) in
  Valid.t domain (
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.op_pipeplus
          (RPC_query.op_pipeplus
            (RPC_query.op_pipeplus
              (RPC_query.query_value make)
              f1)
            f2)
          f3)
        f4)).

Ltac valid_auto :=
  eapply implies; [
    first [
      apply empty |
      apply seal1 |
      apply seal2 |
      apply seal3 |
      apply seal4
    ]; try (constructor; simpl; RPC_arg.valid_auto); trivial |
    trivial; simpl; try dtauto
  ].