Some variables shown as unresolved

[infinite-pursuits]

I have the following code:

type verifyactivationcode struct {
	Callweights        [3][24][24]frontend.Variable `gnark:"allweights"`
	Callbiases         [3][24]frontend.Variable     `gnark:"allbiases"`
	Cx                 [24]frontend.Variable        `gnark:"Cx"`
	Chidden_layer_size [3]frontend.Variable         `gnark:"chidden_layer_size"`
	Actcodearray       [3][24]frontend.Variable     `gnark:",public"`
}

func (circuit *verifyactivationcode) Define(api frontend.API) error {
	var x [24]frontend.Variable
	var allweights [3][24][24]frontend.Variable
	var allbiases [3][24]frontend.Variable
	var activation_code_array [3][24]frontend.Variable
	var tempinp [24]frontend.Variable

	allweights = circuit.Callweights
	allbiases = circuit.Callbiases
	x = circuit.Cx
	tempinp = x

	for hidden_layer := 0; hidden_layer < 3; hidden_layer++ {

		var temp_act_code [24]frontend.Variable
		var dotpdtvec [24]frontend.Variable
		var biassum [24]frontend.Variable
		var postrelu [24]frontend.Variable

		dotpdtvec = MulVecf(api, allweights[hidden_layer], tempinp)
		biassum = AddVecf(api, dotpdtvec, allbiases[hidden_layer])

		for i := 0; i < 24; i++ {

			postrelu[i] = api.Select(biassum[i], biassum[i], frontend.Variable(0))
			temp_act_code[i] = api.Select(biassum[i], frontend.Variable(1), frontend.Variable(0))

		}
		tempinp = postrelu
                activation_code_array[hidden_layer] = temp_act_code
	}
	
	for i := 0; i < 3; i++ {
		for j := 0; j < 24; j++ {
			api.AssertIsEqual(circuit.Actcodearray[i][j], activation_code_array[i][j])
		}
	}
	api.Mul(circuit.Chidden_layer_size[0], circuit.Chidden_layer_size[1], circuit.Chidden_layer_size[2])
	return nil
}


func dotpdtf(api frontend.API, v1 [24]frontend.Variable, v2 [24]frontend.Variable) frontend.Variable {
	var tempsum frontend.Variable
	tempsum = 0
	l := len(v1)
	for i := 0; i < l; i++ {
		tempsum = api.Add(api.Mul(v1[i], v2[i]), tempsum)
	}
	return tempsum
}

func MulVecf(api frontend.API, matrix [24][24]frontend.Variable, v [24]frontend.Variable) [24]frontend.Variable {
	var dpdtvec [24]frontend.Variable
	for i, vec := range matrix {
		dpdtvec[i] = dotpdtf(api, vec, v)
	}
	return dpdtvec
}

func AddVecf(api frontend.API, v1 [24]frontend.Variable, v2 [24]frontend.Variable) [24]frontend.Variable {
	var sumvec [24]frontend.Variable
	for i := 0; i < len(v1); i++ {
		sumvec[i] = api.Add(v1[i], v2[i])
	}
	return sumvec
}

After adding api.Println statements, I see the following

Printing biassum:  {_0: -29, _1: 10, _2: 6, _3: -3, _4: 0, _5: 0, _6: 0, _7: 0, _8: 0, _9: 0, _10: 0, _11: 0, _12: 0, _13: 0, _14: 0, _15: 0, _16: 0, _17: 0, _18: 0, _19: 0, _20: 0, _21: 0, _22: 0, _23: 0}

Printing postrelu:  {_0: <unsolved>, _1: <unsolved>, _2: <unsolved>, _3: <unsolved>, _4: <unsolved>, _5: <unsolved>, _6: <unsolved>, _7: <unsolved>, _8: <unsolved>, _9: <unsolved>, _10: <unsolved>, _11: 0, _12: 0, _13: 0, _14: 0, _15: 0, _16: 0, _17: 0, _18: 0, _19: 0, _20: 0, _21: 0, _22: 0, _23: 0}

and type of biassum is expr.LinearExpression.

I am running a for loop three times. For the first 2, I see unsolved for all 0-23. but for the last one I see some unsolved and some zeros. Cannot figure out what is going wrong.

[gbotrel]

hi!
2 possibilities;

1. there may be a bug in the api.Println, particularly for nested arrays or data structures, what is exactly your call?
2. what may be happening is the following; api.Println logs are printed once the constraint system is solved. But the solving of the constraint system is done in parallel, so if you have some failing constraints in your circuit, the output of the log may not be deterministic.

[ivokub]

Can you first try running using the test engine? For example:

func TestCircuitt(t *testing.T) {
	witness := verifyactivationcode{}
        // define witness
	err := test.IsSolved(&verifyactivationcode{}, &witness, ecc.BN254.ScalarField())
	if err != nil {
		t.Log(err)
	}
}

Please also provide valid witness for testing.

I also see that line api.AssertIsEqual(circuit.Actcodearray[i][j], activation_code_array[i][j]) checks against activation_code_array whose elements are not initialised.

[infinite-pursuits]

Thanks a lot for helping.
After using the test engine, I see the following error :
[assertIsBoolean] 2
main.(*verifyactivationcode).Define
main.go:433
fatal error: no goroutines (main called runtime.Goexit) - deadlock!

a) This is for the statement --> postrelu[i] = api.Select(biassum[i], biassum[i], frontend.Variable(0)) in my code. The biassum[i] is not 0 or 1. I wish to check if biassum[i]>=0 and based on that put different values in post_relu[i] and temp_act_code[i]. what should be the correct way of doing this?

b) Biassum values in the clear are as follows.
[2 4 -204353 -1 -2.01875722e+08 -1.3809983e+07 -3.877177e+06 -199992 8 2 -205550 -1.1403683e+07 -1.2458499e+07 -208064 -209793 -2.555409e+06 0 0 0 0 0 0 0 0]

When I check the biassum values in the calculated in the circuit through a debugger, I see the exact values for the 0th and 1st indices (i.e. 2, 4 from the above array) but when it comes to negative integers I see weird stuff. For eg. the 2nd index value should be -204353 but what I see in the debugger for biassum[2] is the follows :

Suddenly for i=2, biassum[2] has four rows, while for biassum[0] and biassum[1] I could see a single value. This is correct right based on how gnark treats negative numbers? In that case, how do I do the biassum[i]>=0 check?

c) I do the println calls as -> api.Println(biassum).. Is this the wrong way of calling? @gbotrel

d) I had missed a line for activation_code_array initialization in the circuit above, added that (It existed in my copy of the code). @ivokub

[infinite-pursuits]

I think the main issue is that in the clear the allweights and allbiases variables can have negative values. So when the dotpdtf, MulVecf and AddVecf functions operate on negative values and call api.Mul/Add functions, the variables get converted from type frontend.Variable | int to frontend.Variable|*big.Int. Therefore the api.Cmp or api.Select function will not work here, since the negative values are saved as unsigned integers which are huge positive numbers and therefore the checks basically get bypassed. How do I get over this? I need the check biassum[i]>=0 (in clear) to be translated to gnark.

[ivokub]

The underlying type is *big.Int only when you run within the test engine. Using test engine gnark does not actually compile the circuit nor compute the execution trace but instead computes all the values in-line in the circuit definition. It is only meant for debugging and development.

When actually compiling, then the underlying int type doesn't represent the actual value, but instead is an identifier to an element in the witness. It is not meaningful to the user, and only used for the compiler for tracking the computations.

In finite field arithmetic you always have biassum[i]>=0 as canonical representation of finite field element is a positive integer in range [0, r-1]. I recommend using #530. It is not merged yet, but should be able to merge into your vendored copy of gnark.

[infinite-pursuits]

Also how come you use if statements in the circuits here - https://github.com/ConsenSys/gnark/blob/master/std/math/emulated/field_test.go

[ivokub]

We can use if statement if it depends on a constant. A constant is some integer value which does not depend on the witness assignment.

[infinite-pursuits]

thanks that makes sense!