【session 2】 Exercise Integer Division - why does the if-else statement throw "signal already assigned" error?

[abbylow]

S2的最后一题IntegerDivide，我稍微修改了Example Solution里的答案，以下是我的代码

代码

pragma circom 2.1.4;

include "circomlib/compconstant.circom";

template IsNegative(){
    signal input in;
    signal output out;

    component n2b = Num2Bits(254);
    component comp = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808);

    n2b.in <== in;
    comp.in <== n2b.out;
    out <== comp.out;
}

template IntegerDivide(divisor_bits) {
    signal input dividend; // -8
    signal input divisor; // 5
    signal output remainder; // 2
    signal output quotient; // -2

    component is_neg = IsNegative();
    is_neg.in <== dividend;

    signal output is_dividend_negative;
    is_dividend_negative <== is_neg.out;

    signal output dividend_adjustment;
    dividend_adjustment <== 1 + is_dividend_negative * -2; // 1 or -1

    signal output abs_dividend;
    abs_dividend <== dividend * dividend_adjustment; // 8

    signal output raw_remainder;
    raw_remainder <-- abs_dividend % divisor;
    
    signal output neg_remainder;
    neg_remainder <-- divisor - raw_remainder;

    if (is_dividend_negative == 1 && raw_remainder != 0) {
        remainder <-- neg_remainder;
    // 问题在这里：报错error[T3001]: Exception caused by invalid assignment: signal already assigned
    } else {
        remainder <-- raw_remainder;
    }

    quotient <-- (dividend - remainder) / divisor; // (-8 - 2) / 5 = -2

    dividend === divisor * quotient + remainder; // -8 = 5 * -2 + 2

    // check that 0 <= remainder < divisor
    component remainderUpper = LessThan(divisor_bits);
    remainderUpper.in[0] <== remainder;
    remainderUpper.in[1] <== divisor;
    remainderUpper.out === 1;
}

component main = IntegerDivide(8);

/* INPUT = {
    "dividend": "19",
    "divisor": "5"
} */

疑问

为何else statement会报错呢？报错原因是指remainder已经被assigned了，不能被重复assign。但按理来说，remainder应该只会被assign一次，要嘛在if statement里被assign，要嘛在else statement里被assign。

这几行if-else statement是从example solution模版里抄出来的，为何我跑不了呢？

我的workaround

pragma circom 2.1.4;

include "circomlib/compconstant.circom";

template IsNegative(){
    signal input in;
    signal output out;

    component n2b = Num2Bits(254);
    component comp = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808);

    n2b.in <== in;
    comp.in <== n2b.out;
    out <== comp.out;
}

template IntegerDivide(divisor_bits) {
    signal input dividend; // -8
    signal input divisor; // 5
    signal output remainder; // 2
    signal output quotient; // -2

    component is_neg = IsNegative();
    is_neg.in <== dividend;

    signal output is_dividend_negative;
    is_dividend_negative <== is_neg.out;

    signal output dividend_adjustment;
    dividend_adjustment <== 1 + is_dividend_negative * -2; // 1 or -1

    signal output abs_dividend;
    abs_dividend <== dividend * dividend_adjustment; // 8

    signal output raw_remainder;
    raw_remainder <-- abs_dividend % divisor;
    
    signal output neg_remainder;
    neg_remainder <-- divisor - raw_remainder;

    // 换成Optional chaining (?.)就跑得通了
    remainder <-- (is_dividend_negative == 1 && raw_remainder != 0) ? neg_remainder : raw_remainder;

    quotient <-- (dividend - remainder) / divisor; // (-8 - 2) / 5 = -2

    dividend === divisor * quotient + remainder; // -8 = 5 * -2 + 2

    // check that 0 <= remainder < divisor
    component remainderUpper = LessThan(divisor_bits);
    remainderUpper.in[0] <== remainder;
    remainderUpper.in[1] <== divisor;
    remainderUpper.out === 1;
}

component main = IntegerDivide(8);

/* INPUT = {
    "dividend": "19",
    "divisor": "5"
} */

我的猜测（未经验证）

会不会是remainder <-- 只能出现一次呢？但这样也太不合理了，既然有了if-else statement的语法，就应该支持上述的if-else statement才对。

注：上述solution在zkrepl里依旧跑不了negative input，要放p-1才能表示-1，以此类推。

[lkiversonlk]

反正都是瞎猜。。。我也来猜。

考虑下写电路编译器的难度，这种写法：

remainder <-- (is_dividend_negative == 1 && raw_remainder != 0) ? neg_remainder : raw_remainder;

你的条件语句和结果是在一个地方集中给编译器的，所以他容易判断和生成电路。
用一个冗长的if else，可能会导致编译器很难去跟随和收集后续所有的计算。

所以逻辑上确实支持?就应该支持if else，但是实现上可能不一样。
瞎猜的。

[abbylow]

还是没找到答案，用circom（之前用的是zkrepl）跑了也是一样的报错

这里补充2点：

1. 根据Circom文档 Control Flow的例子
   这个例子里用的是var不是signal，所以我们知道用的是var的话不会throw signal already assigned

var x = 0;
var y = 1;
if (x >= 0) {
   x = y + 1;
   y += 1;
} else {
   y = x;
}

但这个点好像没什么帮助，因为remainder必须是output signal 😂

2. 根据Circom文档 Unknowns，我们如果用signal作为if condition，在compile的时候由于in是未知的，所以不能生成constraint

pragma circom 2.0.0;

template A(){
   signal input in;
   signal output out;

   if (in < 0){
   // Error: There are constraints depending on the value of the condition and it can be unknown during the constraint generation phase
       out <== 0;
   }
}

component main = A();

但若if condition之后不是生成constraint而是单纯地assign是ok的

pragma circom 2.0.0;

template A(){
   signal input in;
   signal output out;

   if (in < 0){
       out <-- 0;
   }
}

component main = A();

这个点好像也没什么帮助，因为我们代码里用的就是<--

默默在这里等哪位大大解惑