Skip to main content

πŸƒΒ Data_encoding.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.List.
Require TezosOfOCaml.Environment.V7.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
      | None β‡’ False
      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
      | None β‡’ True
      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
      | None β‡’ True
      | Some x β‡’ domain 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 v β‡’ domain_a v
        | None β‡’ True
        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 v β‡’ domain_a v
        | None β‡’ True
        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 p β‡’ domain (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
        | None β‡’ None
        | Some y β‡’ Some (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, None β‡’ True
        | Some P, Some y β‡’ P β†’ (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 P β‡’ P
        | None β‡’ domain 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_a β‡’ domain_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_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
    null
    empty
    unit_value
    constant
    int8
    uint8
    int16
    uint16
    int31
    int32_value
    int64_value
    n_value
    z_value
    bool_value
    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 _ _ _ = false β‡’ reflexivity
    | |- _ β‡’
      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 a β‡’ domain a
        | None β‡’ True
        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 v β‡’ domain_a v
          | None β‡’ True
          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
          | None β‡’ None
          | Some y β‡’ Some (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 P β‡’ P
          | None β‡’ domain 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 i β‡’ Int32.Valid.t i
        | Right u β‡’ domain u
        end in
      t domain_either
        (Compact.or_int32 int32_title alt_title descr encoding).
  End Valid.
End Compact.