Initial Syntax for `DefCompute`

[DavePearce]

Overview

There is a need for a new set of computed columns. Its not clear at this stage the full set of requirements, but an initial idea was to introduce a generic defcompute syntax. This would be an Assignment taking on a form roughly as follows:

(defcolumns X Y)
(defcompute A (+ X Y))

This then creates a computed column A whose contents are calculated by evaluating the expression + X Y. Already, in essence, this construct exists within go-corset (e.g. for handling inverse columns), but it is not accessible at the source level.

Requirements

// There is an implicit assumption that all rows on which orderedPerspectiveColumn is = 1 are contiguous
// so  orderedPerspectiveColumn = [ 0, 0, 1, 1, 1, 1, 1, 0] is allowed
// but orderedPerspectiveColumn = [ 0, 0, 1, 1, 1, 0, 1, 0] isn't
// 
// It is also assumed that columns is lexicographically sorted
// along those rows where orderedPerspectiveColumn[i] ≡ 1
func compute_FIRST(orderedPerspectiveColumn []fr.Element, columns [][]fr.Element) []fr.Element {
    first := make([]fr.Element, len(orderedPerspectiveColumn))
    nCols := len(columns)
    var [nCols]fr.Element currentValue = null;
    hasStarted = false
    for i := 0; i < len(column); i++ {

        if orderedPerspectiveColumn[i] == 0 {
            first[i] = 0
            continue
        }

        row := extractRow(i, columns)

        if !hasStarted {
            hasStarted = true
            currentValue = row
            first[i] = 1
            continue
        }

        if currentValue.equals(row) {
            first[i] = 0
            continue
        }

        currentValue = row
        first[i] = 1
        }
    }
}

func extractRow(int i, columns [][]fr.Element) row []fr.Element {
    nCols := len(columns)
    row := make([]fr.Element, nCols)
    for c := 0; c < nCols; c ++ {
        row[c] = columns[c][i]
    }
}

In addition, we want similar computations for again and last. The latter is roughly the same as first, but done backwards. Likewise, again can be computed as perspective && !first.

Traces

perspective | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0
            +---+---+---+---+---+---+---+---
value       | 1 | 2 | 3 | 4 | 5 | 4 | 3 | 2
            +---+---+---+---+---+---+---+---
first       | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0

perspective | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 0
            +---+---+---+---+---+---+---+---
value       | 1 | 2 | 3 | 4 | 4 | 6 | 7 | 8
            +---+---+---+---+---+---+---+---
first       | 0 | 0 | 0 | 1 | 1 | 1 | 0 | 0

|--------+---+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| persp. | 0 | 0 | 0 | 1 | 1 | 1 | 1  | 1  | 1  | 1  | 1  | 1  | 1  | 1  | 0 | 0 | 0 | 0 |
|--------+---+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| col. 1 |   |   |   | 4 | 4 | 4 | 12 | 19 | 20 | 20 | 20 | 20 | 20 | 23 |   |   |   |   |
|--------+---+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| col. 2 |   |   |   | 1 | 1 | 2 | 1  | 9  | 0  | 4  | 4  | 4  | 4  | 7  |   |   |   |   |
|--------+---+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| FIRST  |   |   |   | 1 |   | 1 | 1  | 1  | 1  | 1  |    |    |    | 1  |   |   |   |   |
| AGAIN  |   |   |   |   | 1 |   |    |    |    |    | 1  | 1  | 1  |    |   |   |   |   |
| FINAL  |   |   |   |   | 1 | 1 | 1  | 1  | 1  |    |    |    | 1  | 1  |   |   |   |   |
|--------+---+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|

[DavePearce]

Thoughts

The initial syntax is not enough for these computations. Perhaps a slightly more ambitious syntax, which allows loops with state variables? I suppose we could restrict to forward loops / backward loops. For example:

(defcolumns (P :binary@prove) (VAL :i128))

(defcompute (FIRST :binary@prove) (:forward (TMP :i128 0) (MATCHED :binary@prove 0)) 
    (if-not-zero P 
      (if-zero MATCHED (begin (set TMP VAL) (set MATCHED 1) 1)
        (if-eq TMP VAL 0 1))))  

Another possibility would be a functional style which use recursion instead of imperative loops, and passes state variables as parameters.