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:

stack repl

ghci> compile gf181 someFunction

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:

bash

> ./compiled-executable compile gf181

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:

haskell

main :: IO ()
main = keelung someFunction

Here, keelung is a function that links your Keelung program to the main function for CLI execution:

haskell

keelung :: Comp t -> IO ()

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):

bash

> stack install
...
Installing executable compiled-executable in ...
> ./compiled-executable compile gf181

Alternatively, during development, you can compile and execute it on-the-fly using:

bash

> stack run compile gf181

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:

bash

> stack run compile --help
Usage: <interactive> compile (FIELD-TYPE | (-p|--prime Integer) |
                               (-b|--binary Integer))

  Compile Keelung program

Available options:
  -p,--prime Integer       Order of the prime field
  -b,--binary Integer      Order of the binary field
  -h,--help                Show this help text

Named field types:
  gf181                    Prime
                           1552511030102430251236801561344621993261920897571225601
  b64                      Binary 18446744073709551643
  bn128                    Prime
                           21888242871839275222246405745257275088548364400416034343698204186575808495617
*** Exception: ExitSuccess

Commands

Here's the table of all commands:

Command	REPL	CLI	what for?
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:

someFunction :: Comp Field
someFunction = do
    x <- input Public
    y <- input Private
    return (x * y)

Interpret a program

You can feed a Keelung program into the interpreter to test and see if it is working as expected.

REPL

haskell

interpret :: FieldType -> Comp t -> [Integer] -> [Integer] -> IO [Integer]

For example:

stack repl

> interpret gf181 someFunction [2] [3]
[6]

CLI

bash

> stack run interpret gf181 '[2]' '[3]'
[6]

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.

Here's the definition of R1CS in case you want to do something with it.

REPL

haskell

compile :: FieldType -> Comp t -> IO (Either Error (R1CS Integer))

For example:

stack repl

> compile gf181 someFunction
Right R1CS {
  Constriant (1): 
    Ordinary constriants (1):

      $1 * $2 = $0

  Variables (2):

    Output variable : $0
    Public Input variable : $1
    Private Input variable : $2

}

CLI

bash

> stack run compile gf181
...

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

haskell

witness :: FieldType -> Comp t -> [Integer] -> [Integer] -> IO [Integer]

Use witness' if you need finer control over filepaths etc.

For example:

stack repl

> witness gf181 someFunction [2] [3]
[6]

CLI

bash

> stack run witness gf181 '[2]' '[3]'
[6]

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

haskell

prove :: FieldType -> Comp t -> [Integer] -> [Integer] -> IO ()

Use prove' if you need finer control over filepaths etc.

For example:

stack repl

> prove gf181 someFunction [2] [3]
Generated circuit file at: aurora/circuit.jsonl
Generated witness file at: aurora/witness.jsonl
....

CLI

bash

> stack run prove gf181 '[2]' '[3]'
[6]

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

haskell

verify :: IO ()

Use verify' if you need finer control over filepaths etc.

For example:

stack repl

> verify

CLI

bash

> stack run verify

See stack run verify --help for more options.

generateDefault :: FieldType -> Comp t -> [Integer] -> [Integer] -> IO ()