Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Initial Syntax for DefCompute #398

Open
DavePearce opened this issue Nov 27, 2024 · 2 comments
Open

Initial Syntax for DefCompute #398

DavePearce opened this issue Nov 27, 2024 · 2 comments
Assignees
Labels
enhancement New feature or request

Comments

@DavePearce
Copy link
Collaborator

DavePearce commented Nov 27, 2024

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 DavePearce self-assigned this Nov 27, 2024
@DavePearce DavePearce added the enhancement New feature or request label Nov 27, 2024
@DavePearce
Copy link
Collaborator Author

DavePearce commented Nov 27, 2024

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.

@DavePearce DavePearce changed the title Draft Initial Syntax for DefCompute Initial Syntax for DefCompute Nov 28, 2024
@DavePearce
Copy link
Collaborator Author

For minDeploymentNo and maxDeploymentNo we have this loop:

// this function will construct e.g. account/MIN_DEPLOYMENT_NUMBER_IN_BLOCK
func firstValue(source, first, persp []fr.Element) firstValue []fr.Element {
	firstValue = make([]fr.Element, len(source))
	var current = fr.Element{0}
	for (i := 0; i < len(source); i++) {
		
		if persp[i] == 0 {
			firstValue[i] = 0;
			continue
		}
		
		if first[i] == 1 {
			current = source[i]
		}
		
		firstValue[i] = current
	}
}

And this function.

// this function will construct e.g. account/MAX_DEPLOYMENT_NUMBER_IN_BLOCK
func finalValue(source, final, persp []fr.Element) finalValue []fr.Element {
	finalValue = make([]fr.Element, len(source))
	var current = fr.Element{0}
	for (i := len(source); i > 0 ; --i) {
		
		if persp[i] == 0 {
			finalValue[i] = 0;
			continue
		}
		
		if final[i] == 1 {
			current = source[i]
		}
		
		finalValue[i] = current
	}
}

And example trace would be:

|-------------+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| persp.      | 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 | 0 | 1 | 1  | 1  | 1  | 1  | 0  | 0  | 0  | 1  |   |   |   |   |
| AGAIN       |   |   | 0 | 1 | 0 | 0  | 0  | 0  | 0  | 1  | 1  | 1  | 0  |   |   |   |   |
| FINAL       |   |   | 0 | 1 | 1 | 1  | 1  | 1  | 0  | 0  | 0  | 1  | 1  |   |   |   |   |
|-------------+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
|-------------+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| MIN_DEP_NUM |   |   | 0 | 0 | 0 | 11 | 3  | 6  | 6  | 6  | 6  | 6  | 1  |   |   |   |   |
|             |   |   | ↓ |   | ↓ | ↓  | ↓  | ↓  | ↓  |    |    |    | ↓  |   |   |   |   |
|-------------+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
| DEP_NUM_NEW |   |   | 0 | 0 | 0 | 11 | 3  | 6  | 6  | 7  | 8  | 8  | 1  |   |   |   |   |
|-------------+---+---+---+---+---+----+----+----+----+----+----+----+----+---+---+---+---|
|             |   |   |   | ↑ | ↑ | ↑  | ↑  | ↑  |    |    |    | ↑  | ↑  |   |   |   |   |
| MAX_DEP_NUM |   |   | 0 | 0 | 0 | 11 | 3  | 6  | 8  | 8  | 8  | 8  | 1  |   |   |   |   |

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant