Skip to main content

🍃 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
  ].