Input / Output

Keelung programs are like circuits, they feature ports for communicating with other circuits or the external world. Although Keelung employs statements like input to request inputs and return to deliver outputs, these inputs and outputs effectively function as ports of a circuit. Keelung programs establish relationships between inputs and outputs, rather than just calculating outputs from inputs like traditional programs.

The most basic function for requesting a input is:

input :: InputAccess -> Comp a

The input function takes an access modifier as an argument and tries to infer the datatype of the input if possible. See the section below to learn how to specify the access modifier and how to explicitly annotate the desired datatype of the input request.

Modifiers

Because these ports in Keelung can have different properties, we will need to specify them in the program.

Public vs. Private

Because we are building ZK programs, it's important to differentiate between public and private values:

  • Private values are only known to the prover.

  • Public values, on the other hand, are known by both the prover and the verifier.

In Keelung, inputs can be either public or private, whereas the outputs of the entry program (i.e., the "main" function) are always public.

This modifier is controlled by the InputAccess type, which has two constructors:

Public :: InputAccess
Private :: InputAccess

To request a public input, you can use Public as an argument to input. For example:

x <- input Public

Similarly, to request a private input, use Private as an argument to input:

y <- input Private

Once requested, the values of both x and y can be used in the program to perform computations.

Datatype

Values passing through these ports in Keelung can be one of three types:

Field element is the most fundamental datatype in Keelung. To request a field element input, use the following function:

inputField :: InputAccess -> Comp Field

Booleans can either be true or false. Here's how to request a Boolean input:

inputBool :: InputAccess -> Comp Boolean

Unsigned integers are similar to field elements but have a fixed bit-width. To request an unsigned integer input, use the following function:

inputUInt :: KnownNat w => InputAccess -> Comp (UInt w)

If the bit-width w cannot be inferred from the context, you will need to annotate it explicitly. For example, to request a public byte, you can use the following code:

x <- inputUInt @8 Public

Helper functions

List of inputs

We can also ask for a bunch of inputs by specifying the dimensions.

inputList  :: InputAccess -> Int -> Comp [t]
inputList2 :: InputAccess -> Int -> Int -> Comp [[t]]
inputList3 :: InputAccess -> Int -> Int -> Int -> Comp [[[t]]]

Examples usage:

  • inputList Public 4: a list with 4 public inputs

  • inputList2 Private 3 4: a list of 3 lists with 4 private inputs

  • inputList3 Public 7 3 4: a list of 7 lists of 3 lists with 4 public inputs

Vector of inputs

You can use the Data.Vector library to work with a group of input values in Keelung. Here are the equivalent functions to the inputList family:

inputVec  :: InputAccess -> Int -> Comp (Vector t)
inputVec2 :: InputAccess -> Int -> Int -> Comp (Vector (Vector))
inputVec3 :: InputAccess -> Int -> Int -> Int -> Comp (Vector (Vector (Vector)))

These functions are useful if you want to speed up the elaboration of your program. For example, if you are requesting a very large array of inputs, Vectors can provide O(1) random access.

Last updated

Logo

Copyright © 2023 BTQ