octez-plompiler 17.3 · OCaml Package

Encoding type for encapsulating encoding/decoding/input functions. This type enables us to use more structured types for data in circuits. For that, encoding is parameterized by 3 types:

'oh is the type of the high-level OCaml representation
'u is the unpacked type, i.e. a collection of atomic reprs.
`p is the packed type, i.e the inner type of Plompiler's repr.

For example, for the representation of a point (pair of scalars), one might have: ( x:int; y:int, scalar repr * scalar repr, scalar * scalar ) encoding

The first type, the record {x:int; y:int}, represents an OCaml point, which becomes the argument taken by the input function.

The second type, scalar repr * scalar repr, is an unpacking of the encoding. This is used for the result of decode. We can use any type isomorphic to scalar repr * scalar repr here.

The last type must be scalar * scalar, as an encoding of a point will be of the type (scalar * scalar) repr.

Parameters

module L : sig ... end

Signature

type ('oh, 'u, 'p) encoding = {

encode : 'u -> 'p L.repr;
decode : 'p L.repr -> 'u;
input : 'oh -> 'p L.Input.t;
of_input : 'p L.Input.t -> 'oh;

}

val conv : 
  ('u1 -> 'u0) ->
  ('u0 -> 'u1) ->
  ('o1 -> 'o0) ->
  ('o0 -> 'o1) ->
  ('o0, 'u0, 'p) encoding ->
  ('o1, 'u1, 'p) encoding

The function conv defines conversions for encodings, by changing the higher-level 'u and and 'oh types.

val with_implicit_bool_check : 
  ('p L.repr -> bool L.repr L.t) ->
  ('o, 'u, 'p) encoding ->
  ('o, 'u, 'p) encoding

val with_assertion : 
  ('p L.repr -> unit L.repr L.t) ->
  ('o, 'u, 'p) encoding ->
  ('o, 'u, 'p) encoding

val scalar_encoding : (Csir.Scalar.t, L.scalar L.repr, L.scalar) encoding

Encoding combinators

val bool_encoding : (bool, bool L.repr, bool) encoding

val list_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d list, 'e list, 'f list) encoding

val atomic_list_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('a list, 'b list L.repr, 'c list) encoding

val obj2_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g * 'h, 'i * 'j, 'k * 'l) encoding

val atomic_obj2_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('a * 'd, ('b * 'e) L.repr, 'c * 'f) encoding

val obj3_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('a * ('d * 'g), 'b * ('e * 'h), 'c * ('f * 'i)) encoding

val atomic_obj3_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('a * ('d * 'g), ('b * ('e * 'h)) L.repr, 'c * ('f * 'i)) encoding

val obj4_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('a * ('d * ('g * 'j)), 'b * ('e * ('h * 'k)), 'c * ('f * ('i * 'l)))
    encoding

val atomic_obj4_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('a * ('d * ('g * 'j)),
    ('b * ('e * ('h * 'k))) L.repr,
    'c * ('f * ('i * 'l)))
    encoding

val obj5_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('a * ('d * ('g * ('j * 'm))),
    'b * ('e * ('h * ('k * 'n))),
    'c * ('f * ('i * ('l * 'o))))
    encoding

val atomic_obj5_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('a * ('d * ('g * ('j * 'm))),
    ('b * ('e * ('h * ('k * 'n)))) L.repr,
    'c * ('f * ('i * ('l * 'o))))
    encoding

val obj6_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('p, 'q, 'r) encoding ->
  ('a * ('d * ('g * ('j * ('m * 'p)))),
    'b * ('e * ('h * ('k * ('n * 'q)))),
    'c * ('f * ('i * ('l * ('o * 'r)))))
    encoding

val atomic_obj6_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('p, 'q L.repr, 'r) encoding ->
  ('a * ('d * ('g * ('j * ('m * 'p)))),
    ('b * ('e * ('h * ('k * ('n * 'q))))) L.repr,
    'c * ('f * ('i * ('l * ('o * 'r)))))
    encoding

val obj7_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('p, 'q, 'r) encoding ->
  ('s, 't, 'u) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * 's))))),
    'b * ('e * ('h * ('k * ('n * ('q * 't))))),
    'c * ('f * ('i * ('l * ('o * ('r * 'u))))))
    encoding

val atomic_obj7_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('p, 'q L.repr, 'r) encoding ->
  ('s, 't L.repr, 'u) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * 's))))),
    ('b * ('e * ('h * ('k * ('n * ('q * 't)))))) L.repr,
    'c * ('f * ('i * ('l * ('o * ('r * 'u))))))
    encoding

val obj8_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('p, 'q, 'r) encoding ->
  ('s, 't, 'u) encoding ->
  ('v, 'w, 'x) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * 'v)))))),
    'b * ('e * ('h * ('k * ('n * ('q * ('t * 'w)))))),
    'c * ('f * ('i * ('l * ('o * ('r * ('u * 'x)))))))
    encoding

val atomic_obj8_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('p, 'q L.repr, 'r) encoding ->
  ('s, 't L.repr, 'u) encoding ->
  ('v, 'w L.repr, 'x) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * 'v)))))),
    ('b * ('e * ('h * ('k * ('n * ('q * ('t * 'w))))))) L.repr,
    'c * ('f * ('i * ('l * ('o * ('r * ('u * 'x)))))))
    encoding

val obj9_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('p, 'q, 'r) encoding ->
  ('s, 't, 'u) encoding ->
  ('v, 'w, 'x) encoding ->
  ('y, 'z, 'a1) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * ('v * 'y))))))),
    'b * ('e * ('h * ('k * ('n * ('q * ('t * ('w * 'z))))))),
    'c * ('f * ('i * ('l * ('o * ('r * ('u * ('x * 'a1))))))))
    encoding

val atomic_obj9_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('p, 'q L.repr, 'r) encoding ->
  ('s, 't L.repr, 'u) encoding ->
  ('v, 'w L.repr, 'x) encoding ->
  ('y, 'z L.repr, 'a1) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * ('v * 'y))))))),
    ('b * ('e * ('h * ('k * ('n * ('q * ('t * ('w * 'z)))))))) L.repr,
    'c * ('f * ('i * ('l * ('o * ('r * ('u * ('x * 'a1))))))))
    encoding

val obj10_encoding : 
  ('a, 'b, 'c) encoding ->
  ('d, 'e, 'f) encoding ->
  ('g, 'h, 'i) encoding ->
  ('j, 'k, 'l) encoding ->
  ('m, 'n, 'o) encoding ->
  ('p, 'q, 'r) encoding ->
  ('s, 't, 'u) encoding ->
  ('v, 'w, 'x) encoding ->
  ('y, 'z, 'a1) encoding ->
  ('b1, 'c1, 'd1) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * ('v * ('y * 'b1)))))))),
    'b * ('e * ('h * ('k * ('n * ('q * ('t * ('w * ('z * 'c1)))))))),
    'c * ('f * ('i * ('l * ('o * ('r * ('u * ('x * ('a1 * 'd1)))))))))
    encoding

val atomic_obj10_encoding : 
  ('a, 'b L.repr, 'c) encoding ->
  ('d, 'e L.repr, 'f) encoding ->
  ('g, 'h L.repr, 'i) encoding ->
  ('j, 'k L.repr, 'l) encoding ->
  ('m, 'n L.repr, 'o) encoding ->
  ('p, 'q L.repr, 'r) encoding ->
  ('s, 't L.repr, 'u) encoding ->
  ('v, 'w L.repr, 'x) encoding ->
  ('y, 'z L.repr, 'a1) encoding ->
  ('b1, 'c1 L.repr, 'd1) encoding ->
  ('a * ('d * ('g * ('j * ('m * ('p * ('s * ('v * ('y * 'b1)))))))),
    ('b * ('e * ('h * ('k * ('n * ('q * ('t * ('w * ('z * 'c1))))))))) L.repr,
    'c * ('f * ('i * ('l * ('o * ('r * ('u * ('x * ('a1 * 'd1)))))))))
    encoding

package octez-plompiler

Parameters

Signature