RAM Boolean v0 Plugin

The ram_bool_v0 plugin provides private indexed array access when using bit-vectors in Boolean ZK.

Types

The ram type is a plugin type for a privately indexable array. It uses the following plugin parameters.

  1. Plugin Name: ram_bool_v0

  2. Type name: ram

  3. Number: type index for the index and element type

  4. Number: number of bits in a RAM index

  5. Number: number of bits in a RAM element

  6. Number: number of allocations

  7. Number: total size of all allocations (in elements)

  8. Number: maximum size concurrently allocated buffers

The first three parameters, type and bit-counts, should be self explanatory. The latter three are there to aid in allocation schemes which a backend may utilize. For example, if a program had two allocations, both with 64 elements but one is free’d before the other allocated, the type could be declared as such. For the sake of the example, we’ll use type 0, 8-bits of index precision, and 16-bits of element precision.

@type @plugin(ram_bool_v0, ram, 0, 8, 16, 2, 128, 64);

If, instead, both were allocated before one was free’d, the concurrent allocation size would be the same as the total.

@type @plugin(ram_bool_v0, ram, 0, 8, 16, 2, 128, 128);

Operations

The following operations are used with RAM.

init

Create a new RAM buffer with specified size.

read

Retrieve and return the element at a specified index.

write

overwrite the value at the specified index.

Here is an example declaration of each.

// index/element is type 0, buffer is type 1, again 8-bit index and 16-bit element.

// initialize a RAM buffer. Each element is given the input value as a start value.
// The size is a constant given in the plugin binding.
//                           buffer    fill
@function(ram_init_64, @out: 1:1, @in: 0:16)
//                           size
  @plugin(ram_bool_v0, init, 64);

// Read an element from the RAM buffer.
//                        out        buffer index
@function(ram_read, @out: 0:16, @in: 1:1,   0:8)
  @plugin(ram_bool_v0, read);

// Write an element into the RAM buffer.
//                        buffer index element
#function(ram_write, @in: 1:1,   0:8,  0:16)
  @plugin(ram_bool_v0, read);

init

Initialize a new RAM buffer. For a given buffer type b, index type i, index bit-width iw, size s, and element bit-width ew, the following parameters are used. Note that i must represent a field with prime 2.

Function Signature

  • Output b:1: The newly created buffer

  • Input i:ew: A value copied into each buffer element

Plugin Binding

  • Plugin Name: ram_bool_v0

  • Operation: init

  • Number: the size of the buffer.

read

Read an element from the buffer. For a given buffer type b, index type i, index bit-width iw, size s, and element bit-width ew, the following parameters are used. Note that i must represent a field with prime 2. Although the read operation does not have a parameter for the size, if the index exceeds the size declared when the buffer was initialized, an @assert_zero failure occurs. If this failure occurs, the backend may assign to the output value an unspecified value.

Function Signature

  • Output i:ew: output value

  • Input b:1: the buffer

  • Input i:iw: the index

Plugin Binding

  • Plugin Name: ram_bool_v0

  • Operation: read

write

write an element into the buffer. For a given buffer type b, index type i, index bit-width iw, size s, and element bit-width ew, the following parameters are used. Note that i must represent a field with prime 2. Although the write operation does not have a parameter for the size, if the index exceeds the size declared when the buffer was initialized, an @assert_zero failure occurs. If this failure occurs, the backend may assign an unspecified value to the indexed element.

Function Signature

  • Input b:1: the buffer

  • Input i:iw: the index

  • Input i:ew: the input value

Plugin Binding

  • Plugin Name: ram_bool_v0

  • Operation: write

Implementing the ram_bool_v0 Plugin

The RAM plugin is likely the trickiest plugin to implement, because it utilizes "IR Plugin Types". That means that an IR type will describe wires which aren’t arithmeic or boolean values. Instead, wires in the RAM buffer type carry RAM buffers.

This means that in addition to implementing operations for init, read, and write, you need a Buffer_T template to take the place of Wire_T, and you need a wtk::TypeBackend<Number, Buffer_T> to allow NAILS to interact with your Buffer_T. Fortunately, whether you choose to implement your own RAM, or use the fallback implementation, WizToolKit has you covered.

Both the arithmetic RAM interface and fallback implementation reside in the #include <wtk/plugins/BooleanRAM.h> header.

Implementing your own RAM Plugin

To implement your RAM plugin, you’ll need to start with your Buffer_T type. This type must follow the same rules as any other wire template used with NAILS: it must be default and move constructible. Of course, you will also need a Wire_T for the buffer’s private indices and elements.

Next you’ll need to implement a wtk::TypeBackend<Number_T, Buffer_T>. Ordinarily, this has callbacks for @add and @mul gates, however, such operations are nonsensical with RAM. Instead, subclass the wtk::plugins::BoolRAMBackend<Number_T, Buffer_T, Wire_T>, which indicates to NAILS that such gates are unsupported (and implements no-ops in the unused callbacks). You must provide a constructor with the wire’s type and backend, along with the bit-widths, and implement the check() method to indicate if proof errors occurred.

struct MyBoolRAMBackend
  : public wtk::plugins::BoolRAMBackend <Number, MyBuffer, MyWire>
{
  MyRAMBackend(wtk::type_idx type, wtk::TypeBackend<Number, MyWire>* backend,
      wtk::wire_idx idx_bits, wtk::wire_idx elt_bits)
    : wtk::plugins::BoolRAMBackend<Number, MyBuffer, MyWire>(
        type, backend, idx_bits, elt_bits);

  bool failure = false;

  // Returns false if any errors are encountered, true otherwise
  bool check() override
  {
    return !this->failure;
    // alternatively, report failures through this->wireBackend->assertZero()
    // and always return true;
  }
};

You’ll need to implement the three RAM operations: init, read, and write. These have convenient superclasses which handle signature and argument checking and provide easy-to-implement callbacks. Within each operation, the Wire_T* parameters are list pointers with index or element bit-width. The bit-widths, and the backend, may be accessed as attributes of the operation→ramBackend() helper.

struct MyRAMInit
  : public wtk::plugins::RAMInitOperation<Number, MyBuffer, MyWire>
{
  void init(wtk::wire_idx const size,
      MyBuffer* const buffer, MyWire const* const fill) override
  {
    /**
     * Instantiate the buffer with the stated size. Then assign each
     * element the fill value
     */

    // fill has length
    this->ramBackend()->elementBits;
  }
};

struct MyRAMRead
  : public wtk::plugins::RAMReadOperation<Number, MyBuffer, MyWire>
{
  void read(MyWire* const out,
      MyBuffer* const buffer, MyWire const* const idx) override
  {
    /* implement: out = buffer[idx]; */

    // out has bit-length
    this->ramBackend()->elementBits;

    // idx has bit-length
    this->ramBackend()->indexBits;
  }
};

struct MyRAMWrite
  : public wtk::plugins::RAMReadOperation<Number, MyBuffer, MyWire>
{
  void write(MyBuffer* const buffer,
      MyWire const* const idx, MyWire const* const in) override
  {
    /* implement: obuffer[idx] = in; */

    // idx has bit-length
    this->ramBackend()->indexBits;

    // in has bit-length
    this->ramBackend()->elementBits;
  }
};

Lastly, you’ll want to implement the wtk::plugins::BoolRAMPlugin<Number_T, Buffer_T, Wire_T> superclass, which is essentially a factory for your operations.

Fallback RAM Plugin

WizToolKit provides a buffer, wtk::plugins::FallbackBoolRAMBuffer<Wire_T>, backend, wtk::plugins::FallbackBoolRAMBackend<Number_T, Wire_T>, and plugin, wtk::plugins::FallbackBoolRAMPlugin<Number_T, Wire_T>, the latter two using the afformentioned buffer to fill the middle Buffer_T template.

Instantiating the RAM Plugin

To instantiate an instance of the RAM plugin, allocate both a plugin object and a RAM backend object. Pass the plugin object to your plugins manager and the backend to both the plugins manager and NAILS interpreter.

Although there is no Boolean RAM demo at this time, you can check out the Arithmetic RAM sample instead.