A Quick Tour of Keelung
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.
-- | A program that outputs whatever number is given.
echo :: Comp Field
echo = do
x <- input Private -- request for a private input and bind it to 'x'
return x -- return 'x'
We can modify this program to request two inputs instead of one, and produce no output as a result:
src/Tutorial.hs
-- | A program that requests for 2 inputs and does nothing with them
useless :: Comp ()
useless = do
_x <- inputField Public -- request for a public input and bind it to '_x'
_y <- inputField Private -- request for a private input and bind it to '_y'
return () -- return nothing
input would try its best to infer the type of input you want when possible.
However, in the case of useless, since there is no way to infer the type of _x or _y, we need to specify the type of inputs using functions like inputField.
See Input / Output for more information.It will generate no constraints if we attempt to compile it.
stack repl
> compile gf181 useless
Right R1CS {
Constriant (0):
Variables (2):
Public Input variable : $0
Private Input variable : $1
}
There's really no use for a Keelung program if it can't generate any constraints unless we can make assertions and associate one input with another. The
assert statement allows us to do just that!Here's another program that takes two inputs and asserts that the second input is the square of the first input:
src/Tutorial.hs
-- | A program that expects the second input to be the square of the first input
square :: Comp ()
square = do
x <- inputField Public -- request for a public input and bind it to 'x'
y <- inputField Private -- request for a private input and bind it to 'y'
assert ((x * x) `eq` y) -- assert that 'y' equals to 'x' squared
Compiling this function would result in the following:
ghci
> compile gf181 square
Right R1CS {
Constriant (1):
Ordinary constriants (1):
$0 * $0 = $1
Variables (2):
Public Input variable : $0
Private Input variable : $1
}
The resulting constraint system has two input variables,
$0 and $1, and an additional constraint stating that $1 should be the square of $0, which is exactly what we want.Sometimes we may want to change the computation conditionally according to some input.
Here's a simple calculator has only 2 operations: addition and multiplication. It takes a Boolean operation flag and 2 inputs, and returns the result.
calculator :: Comp Field
calculator = do
addOrMultiply <- input Public -- Boolean
x <- input Public -- Field
y <- input Public -- Field
return $
cond
addOrMultiply
(x + y)
(x * y)
Unlike in most imperative languages, conditionals are expressions rather than just statements. Both branches have to be present and must be of the same type. That means you cannot omit the
else ... branch like in C.Instead of repeatedly calling
input, we can use inputList to ask for multiple input variables at once:src/Tutorial.hs
fourthInput :: Comp Field
fourthInput = do
xs <- inputList Public 10 -- ask for 10 inputs
return (xs !! 3)
Arrays only make sense if we have a way of iterating over it.
There are two ways of doing this in Keelung:
If you are coming from a C/Python/Java background, this should look familiar to you:
src/Tutorial.hs
allBe42 :: Comp ()
allBe42 = do
xs <- inputList Public 10 :: Comp [Field]
-- access elements of `xs` with indices from 0 to 9
forM_ [0 .. 9] $ \i -> do
assert (xs !! i `eq` 42)
We annotate the type of
inputList Public 10 as Comp [Field] because it cannot be inferred from the context. Without the annotation, Keelung would not know what type of input to expect for inputList and would result in a type error.But why stop at iterating over a list of indices when we can iterate over a list of values in
xs instead?allBe42 :: Comp ()
allBe42 = do
xs <- inputList Public 10 :: Comp [Field]
-- access elements of `xs` directly
forM_ xs $ \x -> do
assert (x `eq` 42)
Here's an example of how to compute the sum of an array:
src/Tutorial.hs
-- | A program that sums all the 10 inputs
summation :: Comp Field
summation = do
xs <- inputList Public 10
return $ sum xs
A Keelung program is a Haskell program with a type of the form
Comp X, where X is one of the Values in Keelung.It is also common to write functions of the form
prog : Y -> Comp X, in this case when Y is given we can get different Keelung programs based on different Y.blake2b :: Int -> Int -> Comp [[Boolean]]
blake2b msglen hashlen = do
msg <- inputsList2 Public msglen 8 >>= thaw2
BLAKE2b.hash msg msglen hashlen
Technically from a Keelung's perspective,
blake2b is a metaprogram - a Haskell program that generates Keelung programs given two Ints. For convenience, these not yet instantiated functions are still referred to as Keelung programs.You can put your Keelung programs in
src/Tutorial.hs or in a separate file, and likewise load it in the REPL with :l.Last modified 24d ago