Hello World

The tutorial for writing Keelung from an example
After Setting up the environment or launching The Keelung Playground,let's start writing some Keelung programs. We will carry out examples in this guide using the Codespace we launched in the Keelung Playground. Since the playground is essentially a Linux environment with a VS Code editor, you may follow the same steps if you have your own Unix-like environment and have installed Keelung in it.


We use Git for distributing the files for this tutorial.


The simplest way to start coding in Keelung is by cloning this repository.
git clone
After cloning the repository, enter the directory and then run stack build to compile the project. If you are using the Haskell Language Server, it is also necessary to build the project once for the extension to work.
cd keelung-examples
stack build
This should take a while for the first time, but it will be faster afterwards!

Load keelung-examples

Once the tutorial is built, we can load it into the REPL by invoking:
stack repl
This allows us to fiddle with the examples in the tutorial.
Let's load the module in src/Tutorial.hs, type the following instruction in the REPL and hit enter:
stack repl
> :l Tutorial

Example: Echo

Here's a Keelung program that takes a private input and then immediately returns it as output.
echo :: Comp Field
echo = do
x <- input Private -- request for a private input and bind it to 'x'
return x -- return 'x'

Interpret echo

If you want to check if your program is working correctly, you can simulate its execution using an interpreter.
Execute the following command in the REPL (stack repl) to interpret the program:
stack repl
> interpret gf181 echo [] [3]
interpret takes a field type, a Keelung program, a list of public inputs, and a list of private inputs, and returns the result of interpreting the function with those inputs.

Compile echo

Use the compile command to compile echo. This command takes a field type and a Keelung program as inputs, and outputs a set of constraints that can be used for verification.
stack repl
> compile GF181 echo
Right R1CS {
Constriant (1):
Ordinary constriants (1):
- $0 + $1 = 0
Variables (2):
Output variable : $0
Private Input variable : $1
The resulting R1CS has two variables, labeled as $0 and $1 respectively. $0 is marked as an output, and $1 is marked as a private input. The system has only one constraint, which requires that the value of $0 should be equal to the value of $1.

Generate a proof of echo

The generateDefault command generates a proof of echo. This command takes a field type, a Keelung program, a list of public inputs and a list of private inputs, and generates a file called proof in the directory. generateDefault is a more ad-hoc version of generate, which allows you to specify the paths of input and output files.
stack repl
> generateDefault gf181 echo [] [2]

Verify the proof of echo

The verify command is used to verify a proof file by taking the paths to the file and inputs as its argument, verifyDefault takes a file named proof and a public inputs file named input.jsonl by default in the working directory. These files are generated by the generate command when creating a proof.
stack repl
> verifyDefault

All set, ready to go!

There should be no problem if you have successfully interpreted and compiled the example above.
Copyright © 2023 BTQ