Array Compilation

[mariari]

preamble

This is a followup issue to #5. Issue #5 demonstrates an array compilation technique for strings. Namely we can encode a string into a field element, by simply concatenating the binary representation padded to the nearest byte. The code for this is quite simple and can be seen below

(defconstant +byte-size+ 8)

(-> string-to-number (string) integer)
(defun string-to-number (string)
  "converts a string to a numerical encoding"
  (let ((cont 0))
    (sum (map 'list
              (lambda (c)
                (prog1
                    (ash (char-code c) (* cont +byte-size+))
                  (incf cont (char-byte-size c))))
              string))))

(-> char-byte-size (character) fixnum)
(defun char-byte-size (char)
  "Calculates how many bytes is needed to model the current char"
  (ceiling (integer-length (char-code char))
           +byte-size+))

We can thus view strings as a subset of a proper array compilation technique

Encoding Technique

The string code shows a good strategy for encoding utf8 style strings, for arrays we can actually simplify the technique quite a bit as instead of working on values with variable size dimensons (我 has a size of 15 bits, thus 2 bytes to encode. 🤕 takes 3 bytes to encode proper.), we can work on a fixed sized type to properly encode.

Thus if we have an array of size arr we can enocde it as the following

(defun sequence-to-number (size arr)
  "converts an array to a numerical encoding"
  (sum (map 'list
            (lambda (ele count) (ash ele (* count size)))
            arr
            (alexandria:iota (length arr)))))

Since the field element may overflow, we require arrays to be of a fixed size, as if we overflow, we have to split it into multiple field elements.

An amusing fact is that we can grow the array in O(1) given no overflow by simply noting the size and adding by the appropriate value.

(For I8's we can only fit 30 field elements before overflow as (ash 2 (* 8 31)) = 250 bits. Thus we can't even use the full size of the array due to byte alignment).

Indexing technique

So far we've only dealt with constructing an array, but how do we index into it? We can do this with a carry bit along with a condition that returns 1 when we hit the condition we want

carry = (condition * value_at_index_i) + (1 - condition) * carry

[TODO write more about the condition value and how we can compute it]

[mariari]

Arrays are mostly in, however one big missing feature is the lack of a range check, this is important, as it ensures we have an unique solution.

Here is an example of range gates we can use for this

def range[4] x {
  b0*b0 - b0
  b1*b1 - b1
  b2*b2 - b2
  b3*b3 - b3
  8*b3 + 4*b2 + 2*b1 + b0
}
def range[8] x {
  b0*b0 - b0
  b1*b1 - b1
  b2*b2 - b2
  b3*b3 - b3
  b4*b4 - b4
  b5*b5 - b5
  b6*b6 - b6
  b7*b7 - b7
  128*b7 + 64*b6 + 32*b5 + 16*b4 + 8*b3 + 4*b2 + 2*b1 + b0
}

we can compose range[4] from range[2], and range[2] from range[1] with these, we can split up any size n check with composition of powers of two.

Thus it's just a matter of generating out this code.