Convert int to frontend.Variable or vice versa

[arater]

Description

I am trying to develop zk-regex with lookup table. But for now I am just trying to create one example circuit. I will make it more generic in the future. But I have problem with usage of currentState. I cannot use frontend variable in if condition so I need to use api.Select to adopt it. But in this case my currentState is only updated when charMatch satisfied but I cannot update it directly because it can be updated only with api.Select so I need to convert currentState from currentState := 0 to currentStateVar := api.Add(0, 0) but in this case I cannot use currentState for tranversing in my lookup because it is frontend variable right now such as c.LookupTable[currentStateVar][j][0]. How can I solve this issue your help will be very appreciated. And this my test circuit and its code.

package main

import (
	"github.com/consensys/gnark/frontend"
)

const (
	statesLength   = 4
	stringLength   = 11
	maxTransitions = 2
)

type Circuit struct {
	PrivateString [stringLength]frontend.Variable `gnark:",secret"`
	States        [statesLength]frontend.Variable `gnark:",secret"`

	// Transition information represented as frontend.Variable
	LookupTable [statesLength][maxTransitions][4]frontend.Variable `gnark:",public"`
}

func (c *Circuit) Commit(api frontend.API) {
	// Example transition data
	// Adjust the data and size according to your actual DFA
	transitions := [][]struct {
		char     rune
		currNode int
		nextNode int
		typ      int
	}{
		{{'a', 0, 1, 0}},
		{{'c', 1, 1, 0}, {'d', 1, 2, 0}},
		{{'b', 2, 3, 0}},
		{{0, 3, -1, 1}},
	}

	// Loop through the states
	for i, stateTransitions := range transitions {
		// Loop through the transitions for each state
		for j, t := range stateTransitions {
			c.LookupTable[i][j][0] = api.Add(0, int64(t.char))     // Transition character
			c.LookupTable[i][j][1] = api.Add(0, int64(t.currNode)) // Current node
			c.LookupTable[i][j][2] = api.Add(0, int64(t.nextNode)) // Next node
			c.LookupTable[i][j][3] = api.Add(0, int64(t.typ))      // Transition type
		}
	}

}

func (c *Circuit) Define(api frontend.API) error {
	c.Commit(api) // Populate the LookupTable

	matchFound := api.Add(0, 0)
	currentState := 0
	for i := 0; i < stringLength; i++ {
		charVar := c.PrivateString[i]

		for j := 0; j < maxTransitions; j++ {
			transitionChar := c.LookupTable[currentState][j][0]
			transitionNextState := c.LookupTable[currentState][j][2]

			charMatch := api.IsZero(api.Sub(charVar, transitionChar))

			// Use api.Select to conditionally update the state and matchFound
			currentState = api.Select(charMatch, transitionNextState, currentState)
			charMatchFound = api.Select(charMatch, api.Add(1, 0), charMatchFound) // Set to true (1) if charMatch

			/* 			if charMatch {
			   				currentState = int(transitionNextState)
			   				if api.IsZero(api.Sub(c.LookupTable[currentState][j][3], 1)) {
			   					matchFound = api.Add(1, 0)
			   				}
			   				break
			   			} else {
			   				currentState = 0
			   			} */
		}
	}

	// Assert that matchFound must equal 1 for the circuit to be satisfied
	api.AssertIsEqual(matchFound, api.Add(1, 0))

	return nil
}

func main() {
	// The rest of your main function
}

[ivokub]

To initialize a frontend.Variable, you have to explicitly define the type:

var currentState frontend.Variable = 0

That said, it is not possible to convert from frontend.Variable back to int. In essence you are defining a system of linear equations which need to be satisfied, e.g.

x := api.Mul(c.X, c.Y)
api.AssertIsEqual(x, c.N)

gets turned into

c.X*c.Y == c.N

for which there are many valid solutions (c.X, c.Y, c.N). When you define a witness or assignment, then you are fixing some of the solution and then gnark solves for the rest during Prove().

If you want to use lookups, then use Mux etc.

[ivokub]

I'm also converting this issue as discussion as it is general question about gnark usage. We use issues for tracking bugs and feature development.