Commands
Commands in Keelung allow you to interact with the compiler and proving systems.
How to execute a command
There are two ways to a execute command:
Through GHCi REPL
In the GHCi REPL, you can execute Keelung commands as Haskell functions for interactive development and testing:
Through the CLI
You can also use the CLI (Command Line Interface) to run Keelung commands directly from your terminal or scripts for streamlined integration into your applications:
Entry point
When using the CLI, your Keelung program requires a designated entry point, similar to the concept of "main" in languages like C. In Haskell, entry points are also called "main" functions.
You will need to bridge your Keelung program to the main
function like this:
Here, keelung
is a function that links your Keelung program to the main
function for CLI execution:
Compiled executable
To use the CLI, your Keelung program must first be compiled into executables. You can do this with the following command (suppose that your executable is named compiled-executable
in package.yaml
):
Alternatively, during development, you can compile and execute it on-the-fly using:
Command line options
You can add --help
or -h
everywhere in the CLI to get more information on how to use a command. For instance:
Commands
Here's the table of all commands:
Interpret
interpret
interpret
simulate the behaviour of a program with inputs
Compile
compile
compile
compile a program into R1CS circuits
Generate Witness
witness
witness'
witness
generate the witness of a program with inputs
Generate Proof
prove
prove'
prove
generate the proof of a program with inputs and the witness
Verify Proof
verify
verify'
verify
verify the proof generated from a program
We will be using this someFunction
function for the command usage examples in the following sections:
Interpret a program
You can feed a Keelung program into the interpreter to test and see if it is working as expected.
REPL
For example:
CLI
Enclose arguments like input lists in colons to avoid parsing error
Compile a program
Generate R1CS constraints by specifying the type of field to use and a Keelung program.
REPL
For example:
CLI
Generate witness
This command generates the witness file of a program with inputs at aurora/witness.jsonl
. This command also returns the simulated output like interpret
.
REPL
Use witness'
if you need finer control over filepaths etc.
For example:
CLI
See stack run witness --help
for more options.
Generate proof
This command generates the proof of a program with the witness file and inputs at aurora/proof
.
REPL
Use prove'
if you need finer control over filepaths etc.
For example:
CLI
See stack run prove --help
for more options.
Verify proof
This command verifies the proof of a program with the witness file at aurora/proof
at aurora/witness
.
REPL
Use verify'
if you need finer control over filepaths etc.
For example:
CLI
See stack run
verify --help
for more options.
Last updated