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.
git clone https://github.com/btq-ag/keelung-examples.git
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!
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
Here's a Keelung program that takes a private input and then immediately returns it as output.
src/Tutorial.hs
echo :: Comp Field
echo = do
x <- input Private -- request for a private input and bind it to 'x'
return x -- return 'x'
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]
[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.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.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]
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
There should be no problem if you have successfully interpreted and compiled the example above.