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 Signatureval conv :
('u1 -> 'u0 ) ->
('u0 -> 'u1 ) ->
('o1 -> 'o0 ) ->
('o0 -> 'o1 ) ->
('o0 , 'u0 , 'p ) encoding ->
('o1 , 'u1 , 'p ) encoding
The function conv
defines conversions for encoding
s, by changing the higher-level 'u
and and 'oh
types.
val list_encoding :
('a , 'b , 'c ) encoding ->
('a list , 'b list , 'c list ) 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