GETTINGSTARTED.md

Getting started with the Pepper project

This document gives a brief, high-level overview of the Pepper system. It assumes you've already installed the prerequisites; if you haven't, see README.txt for a roadmap.

Directory organization

This repository has three main subdirectories:

• compiler - This directory contains the front-end code; it turns source files in C or SFDL into sets of constraints suitable for execution by the back-end.

• pepper - This directory contains the back-end code, the driver scripts, and the source code that gets compiled by the front-end.

• libsnark - This directory contains the libsnark submodule. For more information, see https://github.com/scipr-lab/libsnark

• tinyram - This directory contains the tinyram submodule, which has the code necessary to run tinyram programs inside the Pepper system. See tinyram/doc for more information.

Anatomy of a Pepper execution

(In this section, unless otherwise specified, directories are relative to pepper.)

The short-short-short version:

• Our example is matrix multiplication. The source code is in apps_sfdl/mm_pure_arith.c. Open this file in your favorite text editor and change value ofSIZE on line 8 from 30 to 10 to make the execution faster. Then...

• To run this program, cd pepper ; ./run/run_pepper.sh mm_pure_arith

IMPORTANT: on Fedora, you need to take a few more steps before running. You will need to set up your environment this way every time you want to run a Pepper computation!

source /etc/profile.d/modules.sh
module load mpi/openmpi-x86_64

Simple enough! If you haven't yet, go ahead and run this now; we'll be taking a look at a bunch of files, some of which are automatically generated by this script.

Now, let's dive into some details. The apps_sfdl_hw subdirectory has a few source files related to mm_pure_arith, namely

mm_pure_arith_p_exo.cpp
mm_pure_arith_p_exo.h
mm_pure_arith_v_inp_gen_hw.cpp
mm_pure_arith_v_inp_gen_hw.h

What are these files? They are fragments of the prover (_p_) and verifier (_v_) that are used to set up the computation.

Similarly, apps_sfdl_gen contains a bunch more prover and verifier fragments:

mm_pure_arith_cons.cpp
mm_pure_arith_cons.h
mm_pure_arith_p.cpp
mm_pure_arith_p.h
mm_pure_arith_v.cpp
mm_pure_arith_v.h
mm_pure_arith_v_inp_gen.cpp
mm_pure_arith_v_inp_gen.h
mm_pure_arith.ZAATAR.spec

We'll take a closer look at some of these files in the next few sections.

mm_pure_arith.c

This is the source code for the verified computation we wish to run. This code is compiled into a set of constraints, whose satisfying assignment is dettermined by the prover.

A few things to note here:

1. The function compute() is the entry point for the computation. It takes two structs, struct In and struct Out, for arguments.

2. The input and output struct definitions must be provided---they have no default definition.

3. Preprocessor directives are allowed here. The search path for the preprocessor is ../compiler/cstdinc.

apps_sfdl_hw/

Exogenous check (_p_exo.cpp)

_p_exo.cpp is an exogenous check---given the computation's input and output, it checks that the computation was run correctly. This is just a sanity check on the proof system. You will notice that mm_pure_arith_p_exo.cpp has the following line:

using mm_pure_arith_cons::SIZE;

See Constant definitions, below, for more information on this.

Input generator (_v_inp_gen_hw.cpp)

_v_inp_gen_hw.cpp is the input generator---it assigns values to the inputs of the computations. Notice that this already has a boilerplate implementation that calls compiler_implementation.create_input(). As we'll see later, this other create_input() function is automatically generated when mm_pure_arith.c is compiled, and by default is assigns a random value to each input.

However, if you have more complicated input generation needs, you should define them in this file rather than relying on the automatically generated file. For an example of this, see apps_sfdl_hw/sparse_matvec_v_inp_gen_hw.cpp.

You will notice that the inputs are represented by an array, input_q[], while in mm_pure_arith.c they are represented by an arbitrary struct. The array corresponds to a "flattened" view of the struct in the order dictated by the struct's memory layout per the C standard.

apps_sfdl_gen

Constant definitions (_cons)

Remember the constant we saw in _p_exo.cpp, above (Exogenous check)? This is the file that instantiates this definition.

Where does this come from? During compilation, the compiler automatically generates a class, that contains the values of any constants #defined in apps_sfdl/mm_pure_arith.c, in this case, SIZE. This is handy for constructing the exogenous check and the input generator.

Verifier and prover top-level files (_v.cpp, _p.cpp)

The verifier and prover top-level classes live in _v.cpp and _p.cpp. These are autogenerated classes that simply tie together a few pieces of functionality. You should probably never need to change these.

Default input generator (_v_inp_gen.cpp)

_v_inp_gen.cpp instantiates the default input generator, including the create_input() function that's called from the default input generator in _v_inp_gen_hw.cpp. By default, inputs are initialized to a random value with a number of bits dependent on the declared type of the input.

Creating a new computation

So, what is the process when we wish to create a new program? Really, it's pretty simple:

1. Write the program, storing it in apps_sfdl.

2. ./run/run_pepper.sh program

3. Now that the compiler has automatically generated the relevant files in apps_sfdl_hw, modify them as appropriate.

Caution: make clean deletes the contents of apps_sfdl_gen. Your modifications should be to the apps_sfdl_hw files only!

4. Now, make clean; ./run/run_pepper.sh program.

If you are using the Pantry PutBlock and GetBlock primitives, there are a couple extra requirements for your program:

• You need to #include <db.h> in program.c.

• You need to tell the verifier to initialize the blockstore. For an example of how to do this, see apps_sfdl_hw/ramput_micro_v_inp_gen_hw.cpp.