Keelung Basics

This article is a brief introduction to the fundamental features and capabilities of Keelung.

We've linked the headers of each feature to dedicated articles with more in-depth information for those who want to learn more.

Input / Output

In the previous section, we looked at the echo example, which had 1 private input and 1 output.

However, Keelung programs can have any number of inputs and outputs.

Private & Public Inputs

In zero-knowledge proofs, it's vital to differentiate between two input types: public and private. Here's how they differ:

A private input's value is exclusively known to the prover, whereas a public input's value is shared with both the prover and the verifier.

Additionally, output values are always public, regardless of their input source.

Keelung uses modifiers like Public or Private to indicate this distinction.

The next example combines values from both public and private inputs and adds them together:

src/Tutorial.hs

-- | A program that requests for 2 inputs and add them together
add :: Comp Field
add = do
  x <- input Public -- request for a public input and bind it to 'x'
  y <- input Private -- request for a private input and bind it to 'y'
  return (x + y)

Arithmetics & Literals

Now that you've learned how to add two numbers together, why not take it a step further? Here's how you can perform various arithmetic operations and represent literal numbers in Keelung:

src/Tutorial.hs

-- | Crunch some numbers
arithmetics :: Comp Field
arithmetics = do
  x <- input Public
  y <- input Private
  let temp = x * (3 - y)
  return (temp * temp + 42)

Here, we've introduced a temporary variable named temp to avoid writing x * (3 - y) twice.

Keep in mind that this variable exists solely within the language itself (both Keelung and Haskell); whether or not it exists in the resulting constraint system depends on optimization considerations.

Due to the limitation of constraint systems, an expression in Keelung may also be compiled into multiple small constraints, with intermediate variables in between.

Types

Let's now explore types in Keelung.

arithmetics :: Comp Field -- type
arithmetics = ...         -- value

The first line is the type signature. It declares us that arithmetics should have a type of Comp Field, while the following lines define what the arithmetics actually is.

You can ask the REPL about the type of a definition like this:

ghci

ghci> :t arithmetics
arithmetics :: Comp Field

Field is the type of the number we've been dealing with, while Comp represents the context needed for constructing a Keelung program. Comp Field means that arithmetics is a Keelung program that computes a value of Field.

Booleans

Field isn’t the only type in Keelung. There’s also Boolean, a datatype that has just two inhabitants: true and false.

Logical operaters

There is a whole range of logical operators for manipulating Boolean values.

For example, here’s a program that returns the conjunction of a private and a public input:

src/Tutorial.hs

-- | A program that requests for 2 Boolean inputs and returns the conjunction of them
conjunct :: Comp Boolean
conjunct = do
  x <- input Public
  y <- input Private
  return (x .&. y)

Type of .&.

.&. is an infix operator. If you want to inquire about its type in the REPL, enclose the operator within parentheses like this to appease the REPL (or otherwise you’ll get parsing errors):

ghci

ghci> :t (.&.)
(.&.) :: Bits a => a -> a -> a

This type signature may come as a surprise. Instead of the expected type Boolean -> Boolean -> Boolean, we get something a bit more general.

This is because there are other datatypes in Keelung that can also undergo conjunction.

Rather than having separate conjunction operators for each datatype, we have consolidated them all under .&..

Interpreting Boolean values

Keelung’s interpreter only accepts and returns lists of integers as inputs and outputs.

The Boolean value true is translated as 1 while false is translated as 0.

ghci

ghci> interpret gf181 conjunct [1] [0] 
[0]

Field equality

We can see if two Field values are equal or not with functions like eq:

src/Tutorial.hs

-- | A program that requests for 2 Field inputs and see if they are equal
equalField :: Comp Boolean
equalField = do
  x <- inputField Private
  y <- inputField Private
  return (x `eq` y)

As eq is not an infix operator like .&., we enclose it in backquotes, allowing us to use it in a similar manner. inputField is input specialized on Field so that we don’t have to annotate the type ourselves.

When we interpret equalField with these inputs, it should give us the expected outputs:

ghci

ghci> interpret gf181 equalField [] [3, 3] 
[1]
ghci> interpret gf181 equalField [] [3, 4] 
[0]

Assertions

With Booleans at our disposal, we can now formulate assertions.

Assertions are arguably the most important construct in Keelung, because they allow us to articulate the relationship (and thus the constraint) between variables, which is what ZKPs are all about.

Assertions are made using the following function:

assert :: Boolean -> Comp ()

It takes something of the Boolean type and "remembers" it in the Comp context, so that the compiler can generate constraints for the Boolean expression later on.

Here’s a modified version of equalField, which asserts that 2 inputs to be equal instead of returning the result of comparison.

src/Tutorial.hs

-- | A program that asserts 2 Field inputs to be equal
assertEqualField :: Comp ()
assertEqualField = do
  x <- inputField Private
  y <- inputField Private
  assert (x `eq` y)

Assertion v.s. Computation

If we compile both equalField and assertEqualField and compare the resulting constraints side by side, we’ll notice that assertEqualField generates fewer constraints, because it doesn’t need to compute the value of the comparison, it just assert it as-is.

ghci

ghci> compile gf181 equalField
Right R1CS {
  Constriant (3): 
    Ordinary constraints (2):

      ($1 - $2) * $0 = 0
      ($1 - $2) * $3 = 1 - $0

    Boolean constraints (1):

      $0 = $0 * $0

  Variables (4):

    Output variable:         $0
    Private input variables: $1 ... $2
    Other variable:          $3

}

ghci

ghci> compile gf181 assertEqualField
Right R1CS {
  Constriant (1): 
    Ordinary constraints (1):

      $0 - $1 = 0

  Variables (2):

    Private input variables: $0 ... $1

}

You should use assertions rather than computations whenever possible, unless you need the result for subsequent calculations.

Conditionals

Another thing we can achieve with Booleans is the ability to modify the flow of control within a Keelung program.

Let's explore an example that dynamically returns either of the two Field inputs based on another Boolean input:

src/Tutorial.hs

-- | Returns either the first Field or the second Field base on the Boolean
choose :: Comp Field
choose = do
  xOrY <- input Public
  x <- input Public
  y <- input Public
  return $
    cond
      xOrY -- predicate
      x    -- then branch
      y    -- else branch

The cond function takes a Boolean predicate, and if that predicate evaluates to true, it returns the first branch of type t; otherwise, it returns the second branch of type t.

cond :: Proper t => Boolean -> t -> t -> t

It's important to note that cond is an expression, not a statement that causes side effects as seen in some languages like C. In Keelung, you must provide both "then" and "else" branches for the conditional; partial branching is not allowed.

Loops

Unlike conditionals, Keelung does not have constructs like cond for expressing loops, because they are simply not allowed in zero-knowledge proofs.

However, this doesn't mean we cannot use loops to generate Keelung code in Haskell. We'll explore this concept further in the following examples.

List of Inputs

Suppose we need a list of 4 inputs. This can be done as shown below:

src/Tutorial.hs

-- | Request for 4 public inputs
get4Field :: Comp [Field]
get4Field = do 
  x0 <- input Public
  x1 <- input Public
  x2 <- input Public
  x3 <- input Public
  return [x0, x1, x2, x3]

However, this code doesn’t scale well as the required number of inputs increases.

Fortunately, Haskell provides combinators like replicateM :: Int -> Comp a -> Comp [a], which allows you to execute a statement repeatedly a certain number of times and collect the results as a list:

src/Tutorial.hs

-- | Request for 8 public inputs
get8Field :: Comp [Field]
get8Field = replicateM 8 (input Public)

Int is a Haskell datatype for representing signed integers, since there are no way of converting a Keelung number to Int, the number of repetitions cannot be dynamically determined from inputs.

Keelung also comes a similar helper function called inputList:

src/Tutorial.hs

-- | Request for 10 public inputs
get10Field :: Comp [Field]
get10Field = inputList Public 10

But there’s really nothing special about replicateM or inputList; you can always roll your own in Haskell.

Iterating a list

Now that we have a list of Field values [Field], let's iterate through the list and make assertions about each of its elements:

src/Tutorial.hs

-- | Assert all 4 inputs to be 42
allBe42 :: Comp ()
allBe42 = do 
  xs <- inputList Public 4 :: Comp [Field]
  -- access elements of `xs` with indices from 0 to 3
  forM_ [0 .. 3] $ \\i -> do
    assert (xs !! i `eq` 42)

The function forM_ :: [a] -> (a -> Comp b) -> Comp () accepts a list and a function that operates on each element of the list, discarding the result of that operation. On the other hand, (!!) :: [a] -> Int -> a allows for list indexing.

Instead of iterating over a list of indices and then accessing list elements using indices, we can also iterate directly over the list elements themselves:

src/Tutorial.hs

-- | Assert all 4 inputs to be 42
allBe42 :: Comp ()
allBe42 = do 
  xs <- inputList Public 4 :: Comp [Field]
  -- access elements of `xs` directly
  forM_ xs $ \\x -> do
    assert (x `eq` 42)

Programmers coming from imperative languages like C might find the former style more familiar, whereas the latter style is more common in functional languages like Haskell. Feel free to use any programming style you prefer in Keelung, as they should all generate the same zero-knowledge proof.

Aggregating a list

Here we calculate the sum of them with built-in Haskell function sum :: [Field] -> Field:

src/Tutorial.hs

-- | Request for 4 public inputs and sum them up
sumOf4Fields :: Comp Field
sumOf4Fields = do 
  xs <- inputList Public 4
  return (sum xs)

Functions

Let’s generalize sumOf4Fields by abstracting it as some function so that we don’t need to come up with something like sumOf5Fields.

Like loops, functions are not first-class citizens in Keelung, but that’s okay, because Haskell as the metalanguage has it all!

Function Definition

Here’s how functions are defined in Haskell:

src/Tutorial.hs

-- | Request for a certain number of public inputs and sum them up
sumOfFields :: Int -> Comp Field
sumOfFields n = do
  xs <- inputList Public n
  return (sum xs)

Arguments of a function are placed on the left-hand side of the definition. In the case of sumOfFields, it has an argument called n which has the type of Int. Note that the types of arguments are also reflected in the function’s type signature.

Function Instantiation

On call sites, apply functions with arguments by juxtapositioning them like this:

src/Tutorial.hs

-- | `caller` intantiates `sumOfFields` with different numbers
caller :: Comp Field
caller = do 
  sum1 <- sumOfFields 2
  sum2 <- sumOfFields 3
  return (sum1 + sum2)

You can think of Haskell functions as Keelung macros. Functions are inlined and expanded at the call sites, with arguments substituted as if you had manually written the code:

-- | `caller` intantiates `sumOfFields` with different numbers
caller :: Comp Field
caller = do 
  sum1 <- do
    xs <- inputList Public 2
    return (sum xs)
  sum2 <- do
    xs <- inputList Public 3
    return (sum xs)
  return (sum1 + sum2)

Conclusion

Congratulations on completing this tutorial! We've touched on key concepts of Keelung, including input/output, datatypes, assertions, control flows, and techniques of abstraction.

Check out other guides and examples if you want to venture further into the world of Keelung and zero-knowledge proofs. Our comprehensive language reference also provides detailed information into Keelung's syntax and semantics.

Happy coding!