Skip to main content

🍃 Data_encoding.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Environment.V8.Proofs.Option.

Module Valid.
We should be more precise by also talking about the JSON encoding, but this is enough for now.
  Record t {a : Set} {domain : a Prop} {encoding : Data_encoding.t a}
    : Prop := {
    of_bytes_opt_to_bytes_opt value :
      domain value
      match Data_encoding.Binary.to_bytes_opt None encoding value with
      | Some bytes
        Data_encoding.Binary.of_bytes_opt encoding bytes = Some value
      | NoneFalse
      end;
    to_bytes_opt_of_bytes_opt bytes :
      match Data_encoding.Binary.of_bytes_opt encoding bytes with
      | Some value
        Data_encoding.Binary.to_bytes_opt None encoding value = Some bytes
        domain value
      | NoneTrue
      end;
  }.
  Arguments t {_}.

[of_bytes_opt enc (to_bytes_exn None domain enc)] is an inversion if the [enc] encoding is valid over the [domain]
  Lemma of_bytes_opt_to_bytes_exn_eq {a : Set} (domain : a Prop)
    (e : Data_encoding.t a) (x : a) :
    domain x
    t domain e
    Binary.of_bytes_opt e
      (Binary.to_bytes_exn None e x) = Some x.
  Proof.
    intros domain_x H_Valid.
    destruct H_Valid as [H_of_bytes H_to_bytes].
    specialize (H_of_bytes x).
    unfold Binary.to_bytes_exn.
    destruct (Binary.to_bytes_opt _ _ _) eqn:?.
    { specialize (H_to_bytes b).
      now apply H_of_bytes.
    }
    { now apply H_of_bytes in domain_x. }
  Qed.

  (* @TODO: add an hypothesis saying that the two domains are equivalent *)
  Lemma implies {a : Set} {domain domain' : a Prop}
    {encoding : Data_encoding.t a}
    : t domain encoding
      ( x, domain' x domain x)
      t domain' encoding.
  Proof.
  Admitted.

Since we do not specify the JSON encoding, we require both of the arguments of [splitted] to be valid. We believe this is a good enough approximation for now.
  Axiom splitted : {a : Set} {domain_json domain_binary}
    {json binary : Data_encoding.t a},
    t domain_json json t domain_binary binary
    let domain x :=
      domain_json x domain_binary x in
    t domain (Data_encoding.splitted json binary).

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

  Axiom string_enum : {a : Set} (enum : list (string × a)),
    List.all_distinct_strings (List.map fst enum) = true
    let domain x :=
      List.In x (List.map snd enum) in
    t domain (Data_encoding.string_enum enum).

  Lemma string_enum_dec {a : Set} (enum : list (string × a))
    {eq_dec : a a bool}
    (H_eq_dec : x y, eq_dec x y = true x = y)
    : List.all_distinct_strings (List.map fst enum) = true
      let domain x :=
        List.mem eq_dec x (List.map snd enum) = true in
      t domain (Data_encoding.string_enum enum).
    intro H.
    eapply implies.
    now apply string_enum.
    intros; simpl.
    now apply (List.mem_eq_dec H_eq_dec).
  Qed.

  Module Fixed.
    Axiom string_value : size,
      let domain s := String.length s = size in
      t domain (Data_encoding.Fixed.string_value size).

    Axiom bytes_value : size,
      let domain s := Bytes.length s = size in
      t domain (Data_encoding.Fixed.bytes_value size).

    Axiom add_padding : {a : Set} {domain} {encoding : Data_encoding.t a} {size : int},
      t domain encoding
      t domain (Data_encoding.Fixed.add_padding encoding size).
  End Fixed.

  Module _Variable.
    Axiom string_value :
      t (fun _True) (Data_encoding._Variable.string_value).

    Axiom bytes_value :
      t (fun _True) (Data_encoding._Variable.bytes_value).

    Axiom array_value : {a : Set} {domain} {encoding : Data_encoding.t a},
      t domain encoding
      t (List.Forall domain) (Data_encoding._Variable.array_value None encoding).

    Axiom list_value : {a : Set} {domain} {encoding : Data_encoding.t a},
      t domain encoding
      t (List.Forall domain) (Data_encoding._Variable.list_value None encoding).
  End _Variable.

  Module Bounded.
    Axiom string_value : size,
      let domain s := String.length s size in
      t domain (Data_encoding.Bounded.string_value size).

    Axiom bytes_value : size,
      let domain s := Bytes.length s size in
      t domain (Data_encoding.Bounded.bytes_value size).
  End Bounded.

  Axiom dynamic_size : {a : Set} {domain : a Prop} {encoding},
    t domain encoding
    t domain (Data_encoding.dynamic_size None encoding).

  Axiom json_value : t (fun _True) Data_encoding.json_value.

  Axiom json_schema_value : t (fun _True) Data_encoding.json_schema_value.

  Axiom merge_objs : {o1 o2 : Set}
    {domain1 domain2}
    {encoding1 : Data_encoding.t o1}
    {encoding2 : Data_encoding.t o2},
    t domain1 encoding1
    t domain2 encoding2
    let domain '(x1, x2) := domain1 x1 domain2 x2 in
    t domain (Data_encoding.merge_objs encoding1 encoding2).

  Module Field.
The validity of a [Data_encoding.field] on a certain domain.
    Inductive t (name : string) :
       {a : Set}, (a Prop) Data_encoding.field a Prop :=
    | Req :
       {a : Set} title description (domain_a : a Prop) encoding_a,
      Valid.t domain_a encoding_a
      t _ domain_a (Data_encoding.req title description name encoding_a)
    | Opt :
       {a : Set} title description (domain_a : a Prop) encoding_a,
      Valid.t domain_a encoding_a
      let domain x :=
        match x with
        | Some vdomain_a v
        | NoneTrue
        end in
      t _ domain (Data_encoding.opt title description name encoding_a)
    | Varopt :
       {a : Set} title description (domain_a : a Prop) encoding_a,
      Valid.t domain_a encoding_a
      let domain x :=
        match x with
        | Some vdomain_a v
        | NoneTrue
        end in
      t _ domain (Data_encoding.varopt title description name encoding_a)
    | Dft :
       {a : Set} title description (domain_a : a Prop) encoding_a
        default,
      Valid.t domain_a encoding_a
      t _ domain_a (Data_encoding.dft title description name encoding_a default).
  End Field.

  (* @TODO proper verify the domain for lazy_encoding. This can be done
   * once we verify data_encoding library. *)

  Axiom lazy_encoding : {a : Set} {domain : a Prop} {encoding : Data_encoding.t a},
    t domain encoding
    t (fun _True) (Data_encoding.lazy_encoding encoding).

  Axiom obj1 : {a1 : Set}
    {name1}
    {domain1}
    {field1 : Data_encoding.field a1},
    Field.t name1 domain1 field1
    t domain1 (Data_encoding.obj1 field1).

  Axiom obj2 : {a1 a2 : Set}
    {name1 name2}
    {domain1 domain2}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    List.all_distinct_strings
      [name1; name2] =
      true
    let domain '(x1, x2) :=
      domain1 x1 domain2 x2 in
    t domain (Data_encoding.obj2
      field1 field2).

  Axiom obj3 : {a1 a2 a3 : Set}
    {name1 name2 name3}
    {domain1 domain2 domain3}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    List.all_distinct_strings
      [name1; name2; name3] =
      true
    let domain '(x1, x2, x3) :=
      domain1 x1 domain2 x2 domain3 x3 in
    t domain (Data_encoding.obj3
      field1 field2 field3).

  Axiom obj4 : {a1 a2 a3 a4 : Set}
    {name1 name2 name3 name4}
    {domain1 domain2 domain3 domain4}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    List.all_distinct_strings
      [name1; name2; name3; name4] =
      true
    let domain '(x1, x2, x3, x4) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 in
    t domain (Data_encoding.obj4
      field1 field2 field3 field4).

  Axiom obj5 : {a1 a2 a3 a4 a5 : Set}
    {name1 name2 name3 name4 name5}
    {domain1 domain2 domain3 domain4 domain5}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    List.all_distinct_strings
      [name1; name2; name3; name4; name5] =
      true
    let domain '(x1, x2, x3, x4, x5) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5 in
    t domain (Data_encoding.obj5
      field1 field2 field3 field4 field5).

  Axiom obj6 : {a1 a2 a3 a4 a5 a6 : Set}
    {name1 name2 name3 name4 name5 name6}
    {domain1 domain2 domain3 domain4 domain5 domain6}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5}
    {field6 : Data_encoding.field a6},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    Field.t name6 domain6 field6
    List.all_distinct_strings
      [name1; name2; name3; name4; name5; name6] =
      true
    let domain '(x1, x2, x3, x4, x5, x6) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 in
    t domain (Data_encoding.obj6
      field1 field2 field3 field4 field5 field6).

  Axiom obj7 : {a1 a2 a3 a4 a5 a6 a7 : Set}
    {name1 name2 name3 name4 name5 name6 name7}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5}
    {field6 : Data_encoding.field a6}
    {field7 : Data_encoding.field a7},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    Field.t name6 domain6 field6
    Field.t name7 domain7 field7
    List.all_distinct_strings
      [name1; name2; name3; name4; name5; name6; name7] =
      true
    let domain '(x1, x2, x3, x4, x5, x6, x7) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 in
    t domain (Data_encoding.obj7
      field1 field2 field3 field4 field5 field6 field7).

  Axiom obj8 : {a1 a2 a3 a4 a5 a6 a7 a8 : Set}
    {name1 name2 name3 name4 name5 name6 name7 name8}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5}
    {field6 : Data_encoding.field a6}
    {field7 : Data_encoding.field a7}
    {field8 : Data_encoding.field a8},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    Field.t name6 domain6 field6
    Field.t name7 domain7 field7
    Field.t name8 domain8 field8
    List.all_distinct_strings
      [name1; name2; name3; name4; name5; name6; name7; name8] =
      true
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 in
    t domain (Data_encoding.obj8
      field1 field2 field3 field4 field5 field6 field7 field8).

  Axiom obj9 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 : Set}
    {name1 name2 name3 name4 name5 name6 name7 name8 name9}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5}
    {field6 : Data_encoding.field a6}
    {field7 : Data_encoding.field a7}
    {field8 : Data_encoding.field a8}
    {field9 : Data_encoding.field a9},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    Field.t name6 domain6 field6
    Field.t name7 domain7 field7
    Field.t name8 domain8 field8
    Field.t name9 domain9 field9
    List.all_distinct_strings
      [name1; name2; name3; name4; name5; name6; name7; name8; name9] =
      true
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 domain9 x9 in
    t domain (Data_encoding.obj9
      field1 field2 field3 field4 field5 field6 field7 field8 field9).

  Axiom obj10 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : Set}
    {name1 name2 name3 name4 name5 name6 name7 name8 name9 name10}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9
      domain10}
    {field1 : Data_encoding.field a1}
    {field2 : Data_encoding.field a2}
    {field3 : Data_encoding.field a3}
    {field4 : Data_encoding.field a4}
    {field5 : Data_encoding.field a5}
    {field6 : Data_encoding.field a6}
    {field7 : Data_encoding.field a7}
    {field8 : Data_encoding.field a8}
    {field9 : Data_encoding.field a9}
    {field10 : Data_encoding.field a10},
    Field.t name1 domain1 field1
    Field.t name2 domain2 field2
    Field.t name3 domain3 field3
    Field.t name4 domain4 field4
    Field.t name5 domain5 field5
    Field.t name6 domain6 field6
    Field.t name7 domain7 field7
    Field.t name8 domain8 field8
    Field.t name9 domain9 field9
    Field.t name10 domain10 field10
    List.all_distinct_strings
      [name1; name2; name3; name4; name5; name6; name7; name8; name9; name10] =
      true
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 domain9 x9 domain10 x10 in
    t domain (Data_encoding.obj10
      field1 field2 field3 field4 field5 field6 field7 field8 field9 field10).

  Axiom tup1 : {a : Set}
    {domain}
    {encoding : Data_encoding.t a},
    t domain encoding
    t domain (Data_encoding.tup1 encoding).

  Axiom tup2 : {a1 a2 : Set}
    {domain1 domain2}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2},
    t domain1 encoding1
    t domain2 encoding2
    let domain '(x1, x2) :=
      domain1 x1 domain2 x2 in
    t domain (Data_encoding.tup2
      encoding1 encoding2).

  Axiom tup3 : {a1 a2 a3 : Set}
    {domain1 domain2 domain3}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    let domain '(x1, x2, x3) :=
      domain1 x1 domain2 x2 domain3 x3 in
    t domain (Data_encoding.tup3
      encoding1 encoding2 encoding3).

  Axiom tup4 : {a1 a2 a3 a4 : Set}
    {domain1 domain2 domain3 domain4}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    let domain '(x1, x2, x3, x4) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 in
    t domain (Data_encoding.tup4
      encoding1 encoding2 encoding3 encoding4).

  Axiom tup5 : {a1 a2 a3 a4 a5 : Set}
    {domain1 domain2 domain3 domain4 domain5}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    let domain '(x1, x2, x3, x4, x5) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5 in
    t domain (Data_encoding.tup5
      encoding1 encoding2 encoding3 encoding4 encoding5).

  Axiom tup6 : {a1 a2 a3 a4 a5 a6 : Set}
    {domain1 domain2 domain3 domain4 domain5 domain6}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5}
    {encoding6 : Data_encoding.t a6},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    t domain6 encoding6
    let domain '(x1, x2, x3, x4, x5, x6) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 in
    t domain (Data_encoding.tup6
      encoding1 encoding2 encoding3 encoding4 encoding5 encoding6).

  Axiom tup7 : {a1 a2 a3 a4 a5 a6 a7 : Set}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5}
    {encoding6 : Data_encoding.t a6}
    {encoding7 : Data_encoding.t a7},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    t domain6 encoding6
    t domain7 encoding7
    let domain '(x1, x2, x3, x4, x5, x6, x7) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 in
    t domain (Data_encoding.tup7
      encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7).

  Axiom tup8 : {a1 a2 a3 a4 a5 a6 a7 a8 : Set}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5}
    {encoding6 : Data_encoding.t a6}
    {encoding7 : Data_encoding.t a7}
    {encoding8 : Data_encoding.t a8},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    t domain6 encoding6
    t domain7 encoding7
    t domain8 encoding8
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 in
    t domain (Data_encoding.tup8
      encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
      encoding8).

  Axiom tup9 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 : Set}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5}
    {encoding6 : Data_encoding.t a6}
    {encoding7 : Data_encoding.t a7}
    {encoding8 : Data_encoding.t a8}
    {encoding9 : Data_encoding.t a9},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    t domain6 encoding6
    t domain7 encoding7
    t domain8 encoding8
    t domain9 encoding9
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 domain9 x9 in
    t domain (Data_encoding.tup9
      encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
      encoding8 encoding9).

  Axiom tup10 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : Set}
    {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9
      domain10}
    {encoding1 : Data_encoding.t a1}
    {encoding2 : Data_encoding.t a2}
    {encoding3 : Data_encoding.t a3}
    {encoding4 : Data_encoding.t a4}
    {encoding5 : Data_encoding.t a5}
    {encoding6 : Data_encoding.t a6}
    {encoding7 : Data_encoding.t a7}
    {encoding8 : Data_encoding.t a8}
    {encoding9 : Data_encoding.t a9}
    {encoding10 : Data_encoding.t a10},
    t domain1 encoding1
    t domain2 encoding2
    t domain3 encoding3
    t domain4 encoding4
    t domain5 encoding5
    t domain6 encoding6
    t domain7 encoding7
    t domain8 encoding8
    t domain9 encoding9
    t domain10 encoding10
    let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :=
      domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
      domain6 x6 domain7 x7 domain8 x8 domain9 x9 domain10 x10 in
    t domain (Data_encoding.tup10
      encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
      encoding8 encoding9 encoding10).

  Axiom list_value : {a : Set} {domain_a}
    {encoding_a : Data_encoding.t a},
    t domain_a encoding_a
    t (List.Forall domain_a) (Data_encoding.list_value None encoding_a).

  Axiom assoc : {a : Set} {domain : a Prop} {encoding : Data_encoding.t a},
    t domain encoding
    t (List.Forall (fun pdomain (snd p))) (Data_encoding.assoc encoding).

We define the domain and validity on cases as an inductive rather than a function. This is because a case contains an existential set, and we cannot match on existential sets in [Prop] with impredicative sets.
  Module Case.
    Inductive t {u : Set} (title : string) (tag : int)
      : (u option Prop) Data_encoding.case u Prop :=
    | Intro :
       {a : Set} {domain_a : a Prop} {description : option string}
        {encoding : Data_encoding.t a} {proj : u option a} {inj : a u},
      Valid.t domain_a encoding
      let domain x :=
        match proj x with
        | NoneNone
        | Some ySome (domain_a y inj y = x)
        end in
      let case :=
        Data_encoding.case_value title description (Data_encoding.Tag tag)
          encoding proj inj in
      t _ _ domain case.

Experimental alternative axiom to [Intro] where we can force having a specific [domain].
    Axiom intro_with_implies : {u a : Set} {title description tag}
      {domain : u option Prop} {domain_a : a Prop}
      {encoding : Data_encoding.t a} {proj : u option a} {inj : a u},
      Valid.t domain_a encoding
      ( x,
        match domain x, proj x with
        | None, NoneTrue
        | Some P, Some yP (domain_a y inj y = x)
        | _, _False
        end
      )
      let case :=
        Data_encoding.case_value title description (Data_encoding.Tag tag)
          encoding proj inj in
      t title tag domain case.
  End Case.

  Module Cases.
    Inductive t {u : Set} :
      list string list int
      (u Prop) list (Data_encoding.case u) Prop :=
    | Nil : t [] [] (fun '_False) []
    | Cons :
       {title tag domain_case case},
       {excluding_titles excluding_tags domain cases},
      List.mem String.eqb title excluding_titles = false
      List.mem Compare.Int.(Compare.S.op_eq) tag excluding_tags = false
      Case.t (u := u) title tag domain_case case
      t (u := u) excluding_titles excluding_tags domain cases
      let excluding_titles := title :: excluding_titles in
      let excluding_tags := tag :: excluding_tags in
      let domain x :=
        match domain_case x with
        | Some PP
        | Nonedomain x
        end in
      let cases := case :: cases in
      t excluding_titles excluding_tags domain cases.
  End Cases.

  Module Eval_cases.
The tag, encoding and payload given by a list of cases for a certain value.
    Inductive t {u : Set} (value : u) :
      list (Data_encoding.case u)
      {a : Set & int × Data_encoding.t a × a}
      Prop :=
    | Current {a : Set} :
       title description tag encoding proj inj,
       (payload : a),
       cases,
      let case :=
        Data_encoding.case_value title description (Data_encoding.Tag tag)
          encoding proj inj in
      proj value = Some payload
      t value (case :: cases) (existT _ a (tag, encoding, payload))
    | Next {a : Set} :
       title description tag encoding proj inj,
       cases,
       tag_encoding_payload,
      let case :=
        Data_encoding.case_value title description (Data_encoding.Tag tag)
          encoding proj inj in
      proj value = (None : option a)
      t value cases tag_encoding_payload
      t value (case :: cases) tag_encoding_payload.
  End Eval_cases.

  Module Matching_function.
A matching function is valid when it returns the same result as the evaluation of the cases.
    Definition t {u : Set}
      (domain : u Prop)
      (f : Data_encoding.matching_function u)
      (cases : list (Data_encoding.case u)) :
      Prop :=
       (value : u),
      domain value
       (tag_encoding_payload : {a : Set & int × Data_encoding.t a × a}),
      let 'existT _ _ (tag, encoding, payload) := tag_encoding_payload in
      f value = Data_encoding.matched None tag encoding payload
      Eval_cases.t value cases tag_encoding_payload.
  End Matching_function.

  Axiom matching : {u : Set} {tag_size titles tags domain cases
    matching_function},
    Matching_function.t domain matching_function cases
    Cases.t (u := u) titles tags domain cases
    t domain (Data_encoding.matching tag_size matching_function cases).

  Axiom union : {u : Set} {tag_size titles tags domain cases},
    Cases.t (u := u) titles tags domain cases
    t domain (Data_encoding.union tag_size cases).

  Axiom def : {a : Set} {domain_a : a Prop}
    (id : string) (title description : option string)
    {encoding_a : Data_encoding.t a},
    t domain_a encoding_a
    t domain_a (Data_encoding.def id title description encoding_a).

  Axiom check_size : {a : Set} {domain} {encoding : Data_encoding.t a}
    {size : int},
    t domain encoding
    t domain (Data_encoding.check_size size encoding).

  Axiom conv : {a b : Set} {domain_b : b Prop}
    {a_to_b : a b} {b_to_a} {encoding_b : Data_encoding.t b},
    t domain_b encoding_b
    t
      (fun v_adomain_b (a_to_b v_a) b_to_a (a_to_b v_a) = v_a)
      (Data_encoding.conv a_to_b b_to_a None encoding_b).

  Axiom conv_with_guard : {a b : Set} {domain_b : b Prop}
    {a_to_b : a b} {b_to_a} {encoding_b : Data_encoding.t b},
    t domain_b encoding_b
    t
      (fun v_a
        domain_b (a_to_b v_a) b_to_a (a_to_b v_a) = Pervasives.Ok v_a)
      (Data_encoding.conv_with_guard a_to_b b_to_a None encoding_b).

  Axiom with_decoding_guard : {a : Set} {domain}
    {guard : a Pervasives.result unit string} {encoding : Data_encoding.t a},
    t domain encoding
    let domain v :=
      domain v
      match guard v with
      | Pervasives.Ok _True
      | Pervasives.Error _False
      end in
    t domain (Data_encoding.with_decoding_guard guard encoding).

  Axiom null : t (fun _True) Data_encoding.null.
  Axiom empty : t (fun _True) Data_encoding.empty.
  Axiom unit_value : t (fun _True) Data_encoding.unit_value.
  Axiom constant : s, t (fun _True) (Data_encoding.constant s).
  Axiom int8 : t Pervasives.Int8.Valid.t Data_encoding.int8.
  Axiom uint8 : t Pervasives.UInt8.Valid.t Data_encoding.uint8.
  Axiom int16 : t Pervasives.Int16.Valid.t Data_encoding.int16.
  Axiom uint16 : t Pervasives.UInt16.Valid.t Data_encoding.uint16.
  Axiom int31 : t Pervasives.Int31.Valid.t Data_encoding.int31.
  Axiom int32_value : t Int32.Valid.t Data_encoding.int32_value.
  Axiom int64_value : t Int64.Valid.t Data_encoding.int64_value.
  Axiom n_value : t (fun n ⇒ 0 n) Data_encoding.n_value.
  Axiom z_value : t (fun _True) Data_encoding.z_value.
  Axiom bool_value : t (fun _True) Data_encoding.bool_value.
  Axiom string' : length_kind string_json_repr,
    t (fun _True) (Data_encoding.string' length_kind string_json_repr).
  Axiom bytes' : length_kind string_json_repr,
    t (fun _True) (Data_encoding.bytes' length_kind string_json_repr).
  Axiom string_value : t (fun _True) Data_encoding.string_value.
  Axiom bytes_value : t (fun _True) Data_encoding.bytes_value.

  Create HintDb Data_encoding_db.

  (* Hints for primitives *)
  #[global] Hint Resolve
    null
    empty
    unit_value
    constant
    int8
    uint8
    int16
    uint16
    int31
    int32_value
    int64_value
    n_value
    z_value
    bool_value
    string'
    bytes'
    string_value
    bool_value
    bytes_value
    json_value
    json_schema_value
    _Variable.string_value
    _Variable.bytes_value
    : Data_encoding_db.

  Ltac data_encoding_auto :=
    (* We try to solve the goal using the hints first *)
    (try now eauto 1 with Data_encoding_db);

    (* If this doens't help we start by unfolding the 
     * definition of the encoding we verify *)

    match goal with
    | [|- t _ ?encoding] ⇒ try unfold encoding
    end;
    eapply implies;
    repeat (
      match goal with
      (* Encodings as combinators, with at least one function application *)
      | [|- t _ (_ _)] ⇒
        first [
          eapply splitted |
          eapply matching |
          eapply union |
          eapply option_value |
          eapply string_enum |
          eapply string_value |
          eapply bytes_value |
          eapply obj1 |
          eapply obj2 |
          eapply obj3 |
          eapply obj4 |
          eapply obj5 |
          eapply obj6 |
          eapply obj7 |
          eapply obj8 |
          eapply obj9 |
          eapply obj10 |
          eapply tup1 |
          eapply tup2 |
          eapply tup3 |
          eapply tup4 |
          eapply tup5 |
          eapply tup6 |
          eapply tup7 |
          eapply tup8 |
          eapply tup9 |
          eapply tup10 |
          eapply list_value |
          eapply def |
          eapply conv |
          eapply conv_with_guard |
          eapply with_decoding_guard |
          eapply check_size |
          eapply Fixed.string_value |
          eapply Fixed.bytes_value |
          eapply Fixed.add_padding |
          eapply _Variable.array_value |
          eapply _Variable.list_value |
          eapply Bounded.string_value |
          eapply Bounded.bytes_value |
          eapply dynamic_size |
          eapply merge_objs |
          eapply lazy_encoding |
          eapply assoc
        ]
      (* Special cases defined as inductive *)
      | [|- Field.t _ _ _] ⇒ constructor
      | [|- Cases.t _ _ _ _] ⇒ constructor
      | [|- Case.t _ _ _ _] ⇒ constructor
      (* Finally try the hints *)
      | _solve [eauto 1 with Data_encoding_db]
      end
    );
    (* We avoid [simpl] in the [List.mem] case as that would make the goal
       unreadable with just [true = false] in case of failure. *)

    lazymatch goal with
    | |- List.mem _ _ _ = falsereflexivity
    | |- _
      simpl; trivial; try tauto; try dtauto;
      try (intros []; tauto); try (intros []; dtauto)
    end.
End Valid.

Module Compact.
  Module Valid.
    Import Data_encoding.

    Parameter t : {a : Set}, (a Prop) Compact.t a Prop.

    Axiom implies : {a : Set} {domain domain' : a Prop}
      {encoding : Compact.t a},
      t domain encoding
      ( x, domain' x domain x)
      t domain' encoding.

    Axiom make : {a : Set} (tag_size : option Variant.t)
      (domain : a Prop) (encoding : Compact.t a),
      t domain encoding
      Data_encoding.Valid.t domain (Compact.make tag_size encoding).

    Axiom void_value : t (fun _True) Compact.void_value.
    Axiom unit_value : t (fun _True) Compact.unit_value.
    Axiom bool_value : t (fun _True) Compact.bool_value.

    Axiom payload : {a : Set}
      (domain : a Prop)
      (encoding : encoding a),
      Data_encoding.Valid.t domain encoding
      t domain (Compact.payload encoding).

    Axiom option_value : {a : Set}
      (domain : a Prop)
      (encoding : Compact.t a),
      t domain encoding
      let domain_opt opt :=
        match opt with
        | Some adomain a
        | NoneTrue
        end in
      t domain_opt (Compact.option_value encoding).

    Axiom conv_some : {a b : Set}
      {a_to_b : a b} {b_to_a : b a}
      {domain_a : a Prop}
      {domain_b : b Prop}
      (encoding_a : Data_encoding.t a)
      (encoding_b : Compact.t b),
      Data_encoding.Valid.t domain_a encoding_a
      t domain_b encoding_b
      let domain_aux (a_value : a) :=
        domain_a a_value
        domain_b (a_to_b a_value)
        b_to_a (a_to_b a_value) = a_value in
      t domain_aux
        (Compact.conv (Some encoding_a) a_to_b b_to_a encoding_b).

    Axiom conv_none : {a b : Set}
      {a_to_b : a b} {b_to_a : b a}
      {domain_b : b Prop}
      (encoding_b : Compact.t b),
      t domain_b encoding_b
      let domain_aux (a_value : a) :=
        domain_b (a_to_b a_value)
        b_to_a (a_to_b a_value) = a_value in
      t domain_aux
        (Compact.conv None a_to_b b_to_a encoding_b).

    Axiom tup1 : {a : Set}
      {domain}
      {encoding : Compact.t a},
      t domain encoding
      t domain (Compact.tup1 encoding).

    Axiom tup2 : {a1 a2 : Set}
      {domain1 domain2}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2},
      t domain1 encoding1
      t domain2 encoding2
      let domain '(x1, x2) :=
        domain1 x1 domain2 x2 in
      t domain (Compact.tup2
        encoding1 encoding2).

    Axiom tup3 : {a1 a2 a3 : Set}
      {domain1 domain2 domain3}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      let domain '(x1, x2, x3) :=
        domain1 x1 domain2 x2 domain3 x3 in
      t domain (Compact.tup3
        encoding1 encoding2 encoding3).

    Axiom tup4 : {a1 a2 a3 a4 : Set}
      {domain1 domain2 domain3 domain4}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      let domain '(x1, x2, x3, x4) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 in
      t domain (Compact.tup4
        encoding1 encoding2 encoding3 encoding4).

    Axiom tup5 : {a1 a2 a3 a4 a5 : Set}
      {domain1 domain2 domain3 domain4 domain5}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      let domain '(x1, x2, x3, x4, x5) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5 in
      t domain (Compact.tup5
        encoding1 encoding2 encoding3 encoding4 encoding5).

    Axiom tup6 : {a1 a2 a3 a4 a5 a6 : Set}
      {domain1 domain2 domain3 domain4 domain5 domain6}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5}
      {encoding6 : Compact.t a6},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      t domain6 encoding6
      let domain '(x1, x2, x3, x4, x5, x6) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 in
      t domain (Compact.tup6
        encoding1 encoding2 encoding3 encoding4 encoding5 encoding6).

    Axiom tup7 : {a1 a2 a3 a4 a5 a6 a7 : Set}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5}
      {encoding6 : Compact.t a6}
      {encoding7 : Compact.t a7},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      t domain6 encoding6
      t domain7 encoding7
      let domain '(x1, x2, x3, x4, x5, x6, x7) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 in
      t domain (Compact.tup7
        encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7).

    Axiom tup8 : {a1 a2 a3 a4 a5 a6 a7 a8 : Set}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5}
      {encoding6 : Compact.t a6}
      {encoding7 : Compact.t a7}
      {encoding8 : Compact.t a8},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      t domain6 encoding6
      t domain7 encoding7
      t domain8 encoding8
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 in
      t domain (Compact.tup8
        encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
        encoding8).

    Axiom tup9 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 : Set}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5}
      {encoding6 : Compact.t a6}
      {encoding7 : Compact.t a7}
      {encoding8 : Compact.t a8}
      {encoding9 : Compact.t a9},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      t domain6 encoding6
      t domain7 encoding7
      t domain8 encoding8
      t domain9 encoding9
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 domain9 x9 in
      t domain (Compact.tup9
        encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
        encoding8 encoding9).

    Axiom tup10 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : Set}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9
        domain10}
      {encoding1 : Compact.t a1}
      {encoding2 : Compact.t a2}
      {encoding3 : Compact.t a3}
      {encoding4 : Compact.t a4}
      {encoding5 : Compact.t a5}
      {encoding6 : Compact.t a6}
      {encoding7 : Compact.t a7}
      {encoding8 : Compact.t a8}
      {encoding9 : Compact.t a9}
      {encoding10 : Compact.t a10},
      t domain1 encoding1
      t domain2 encoding2
      t domain3 encoding3
      t domain4 encoding4
      t domain5 encoding5
      t domain6 encoding6
      t domain7 encoding7
      t domain8 encoding8
      t domain9 encoding9
      t domain10 encoding10
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 domain9 x9 domain10 x10 in
      t domain (Compact.tup10
        encoding1 encoding2 encoding3 encoding4 encoding5 encoding6 encoding7
        encoding8 encoding9 encoding10).

    Module Field.
The validity of a [Compact.field] on a certain domain.
      Inductive t (name : string) :
         {a : Set}, (a Prop) Compact.field a Prop :=
      | Req :
         {a : Set} (domain_a : a Prop) encoding_a,
        Valid.t domain_a encoding_a
        t _ domain_a (Compact.req name encoding_a)
      | Opt :
         {a : Set} (domain_a : a Prop) encoding_a,
        Valid.t domain_a encoding_a
        let domain x :=
          match x with
          | Some vdomain_a v
          | NoneTrue
          end in
        t _ domain (Compact.opt name encoding_a).
    End Field.

    Axiom obj1 : {a1 : Set}
      {name1}
      {domain1}
      {field1 : Compact.field a1},
      Field.t name1 domain1 field1
      t domain1 (Compact.obj1 field1).

    Axiom obj2 : {a1 a2 : Set}
      {name1 name2}
      {domain1 domain2}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      List.all_distinct_strings
        [name1; name2] =
        true
      let domain '(x1, x2) :=
        domain1 x1 domain2 x2 in
      t domain (Compact.obj2
        field1 field2).

    Axiom obj3 : {a1 a2 a3 : Set}
      {name1 name2 name3}
      {domain1 domain2 domain3}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      List.all_distinct_strings
        [name1; name2; name3] =
        true
      let domain '(x1, x2, x3) :=
        domain1 x1 domain2 x2 domain3 x3 in
      t domain (Compact.obj3
        field1 field2 field3).

    Axiom obj4 : {a1 a2 a3 a4 : Set}
      {name1 name2 name3 name4}
      {domain1 domain2 domain3 domain4}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      List.all_distinct_strings
        [name1; name2; name3; name4] =
        true
      let domain '(x1, x2, x3, x4) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 in
      t domain (Compact.obj4
        field1 field2 field3 field4).

    Axiom obj5 : {a1 a2 a3 a4 a5 : Set}
      {name1 name2 name3 name4 name5}
      {domain1 domain2 domain3 domain4 domain5}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      List.all_distinct_strings
        [name1; name2; name3; name4; name5] =
        true
      let domain '(x1, x2, x3, x4, x5) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5 in
      t domain (Compact.obj5
        field1 field2 field3 field4 field5).

    Axiom obj6 : {a1 a2 a3 a4 a5 a6 : Set}
      {name1 name2 name3 name4 name5 name6}
      {domain1 domain2 domain3 domain4 domain5 domain6}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5}
      {field6 : Compact.field a6},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      Field.t name6 domain6 field6
      List.all_distinct_strings
        [name1; name2; name3; name4; name5; name6] =
        true
      let domain '(x1, x2, x3, x4, x5, x6) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 in
      t domain (Compact.obj6
        field1 field2 field3 field4 field5 field6).

    Axiom obj7 : {a1 a2 a3 a4 a5 a6 a7 : Set}
      {name1 name2 name3 name4 name5 name6 name7}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5}
      {field6 : Compact.field a6}
      {field7 : Compact.field a7},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      Field.t name6 domain6 field6
      Field.t name7 domain7 field7
      List.all_distinct_strings
        [name1; name2; name3; name4; name5; name6; name7] =
        true
      let domain '(x1, x2, x3, x4, x5, x6, x7) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 in
      t domain (Compact.obj7
        field1 field2 field3 field4 field5 field6 field7).

    Axiom obj8 : {a1 a2 a3 a4 a5 a6 a7 a8 : Set}
      {name1 name2 name3 name4 name5 name6 name7 name8}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5}
      {field6 : Compact.field a6}
      {field7 : Compact.field a7}
      {field8 : Compact.field a8},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      Field.t name6 domain6 field6
      Field.t name7 domain7 field7
      Field.t name8 domain8 field8
      List.all_distinct_strings
        [name1; name2; name3; name4; name5; name6; name7; name8] =
        true
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 in
      t domain (Compact.obj8
        field1 field2 field3 field4 field5 field6 field7 field8).

    Axiom obj9 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 : Set}
      {name1 name2 name3 name4 name5 name6 name7 name8 name9}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5}
      {field6 : Compact.field a6}
      {field7 : Compact.field a7}
      {field8 : Compact.field a8}
      {field9 : Compact.field a9},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      Field.t name6 domain6 field6
      Field.t name7 domain7 field7
      Field.t name8 domain8 field8
      Field.t name9 domain9 field9
      List.all_distinct_strings
        [name1; name2; name3; name4; name5; name6; name7; name8; name9] =
        true
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 domain9 x9 in
      t domain (Compact.obj9
        field1 field2 field3 field4 field5 field6 field7 field8 field9).

    Axiom obj10 : {a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : Set}
      {name1 name2 name3 name4 name5 name6 name7 name8 name9 name10}
      {domain1 domain2 domain3 domain4 domain5 domain6 domain7 domain8 domain9
        domain10}
      {field1 : Compact.field a1}
      {field2 : Compact.field a2}
      {field3 : Compact.field a3}
      {field4 : Compact.field a4}
      {field5 : Compact.field a5}
      {field6 : Compact.field a6}
      {field7 : Compact.field a7}
      {field8 : Compact.field a8}
      {field9 : Compact.field a9}
      {field10 : Compact.field a10},
      Field.t name1 domain1 field1
      Field.t name2 domain2 field2
      Field.t name3 domain3 field3
      Field.t name4 domain4 field4
      Field.t name5 domain5 field5
      Field.t name6 domain6 field6
      Field.t name7 domain7 field7
      Field.t name8 domain8 field8
      Field.t name9 domain9 field9
      Field.t name10 domain10 field10
      List.all_distinct_strings
        [name1; name2; name3; name4; name5; name6; name7; name8; name9; name10] =
        true
      let domain '(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :=
        domain1 x1 domain2 x2 domain3 x3 domain4 x4 domain5 x5
        domain6 x6 domain7 x7 domain8 x8 domain9 x9 domain10 x10 in
      t domain (Compact.obj10
        field1 field2 field3 field4 field5 field6 field7 field8 field9 field10).

    Axiom int32_value : t Int32.Valid.t Compact.int32_value.
    Axiom int64_value : t Int64.Valid.t Compact.int64_value.

    Axiom list_value : {a : Set} {domain_a} {size : int}
      {encoding_a : Data_encoding.encoding a},
      Pervasives.Int.Valid.non_negative size
      Data_encoding.Valid.t domain_a encoding_a
      t (List.Forall domain_a) (Compact.list_value size encoding_a).

    Module Case.
      Inductive t {u : Set} (title : string)
        : (u option Prop) Compact.case u Prop :=
      | Intro :
         {a : Set} {domain_a : a Prop} {description : option string}
          {encoding : Compact.t a} {proj : u option a} {inj : a u},
        Valid.t domain_a encoding
        let domain x :=
          match proj x with
          | NoneNone
          | Some ySome (domain_a y inj y = x)
          end in
        let case :=
          Compact.case_value title description
            encoding proj inj in
        t _ domain case.
    End Case.

    Module Cases.
      Inductive t {u : Set} :
        list string
        (u Prop) list (Compact.case u) Prop :=
      | Nil : t [] (fun '_False) []
      | Cons :
         {title domain_case case},
         {excluding_titles domain cases},
        List.mem String.eqb title excluding_titles = false
        Case.t (u := u) title domain_case case
        t (u := u) excluding_titles domain cases
        let excluding_titles := title :: excluding_titles in
        let domain x :=
          match domain_case x with
          | Some PP
          | Nonedomain x
          end in
        let cases := case :: cases in
        t excluding_titles domain cases.
    End Cases.

    Axiom union : {u : Set} {tag_bits case_bits titles domain cases},
      Cases.t (u := u) titles domain cases
      t domain (Compact.union tag_bits case_bits cases).

    Axiom void_case : {a : Set} title,
      Case.t title (fun _None) (Compact.void_case (a := a) title).

    Axiom or_int32 : {u : Set} {int32_title alt_title descr}
      {domain} (encoding : Data_encoding.t u),
      Data_encoding.Valid.t domain encoding
      let domain_either (e : Either.t int u) : Prop :=
        match e with
        | Left iInt32.Valid.t i
        | Right udomain u
        end in
      t domain_either
        (Compact.or_int32 int32_title alt_title descr encoding).
  End Valid.
End Compact.