Repository: nexus-xyz/nexus-zkvm
File: vm/src/circuit/riscv.rs (Rust)

Code before:
    cs.w[f30a] = cs.get_var("f3=0") * &(ONE - cs.get_var("inst_30"));
    cs.w[f30b] = cs.get_var("f3=0") * cs.get_var("inst_30");
    cs.w[f35a] = cs.get_var("f3=5") * &(ONE - cs.get_var("inst_30"));
    cs.w[f35b] = cs.get_var("f3=5") * cs.get_var("inst_30");

    // constraints
    cs.constraint(|cs, a, b, c| {
        a[0] = ONE;
        a[cs.var("inst_30")] = MINUS;
        b[cs.var("f3=0")] = ONE;
        c[f30a] = ONE;
    });
    cs.mul("f3=0b", "f3=0", "inst_30");
    cs.constraint(|cs, a, b, c| {
        a[0] = ONE;
        a[cs.var("inst_30")] = MINUS;
        b[cs.var("f3=5")] = ONE;
        c[f35a] = ONE;
    });
    cs.mul("f3=5b", "f3=5", "inst_30");

    cs.set_eq("J=1", "opcode=55"); // lui
    cs.set_eq("J=2", "opcode=23"); // auipc
    cs.set_eq("J=3", "opcode=111"); // jal
    cs.set_eq("J=4", "opcode=103"); // jalr
    cs.nand("f3", "opcode=103");

    cs.mul("J=5", "opcode=99", "f3=0"); // beq
    cs.mul("J=6", "opcode=99", "f3=1"); // bne
    cs.mul("J=7", "opcode=99", "f3=4"); // blt
    cs.mul("J=8", "opcode=99", "f3=5"); // bge
    cs.mul("J=9", "opcode=99", "f3=6"); // bltu
    cs.mul("J=10", "opcode=99", "f3=7"); // bgeu

    cs.mul("J=11", "opcode=3", "f3=0"); // lb
    cs.mul("J=12", "opcode=3", "f3=1"); // lh
    cs.mul("J=13", "opcode=3", "f3=2"); // lw
    cs.mul("J=14", "opcode=3", "f3=4"); // lbu
    cs.mul("J=15", "opcode=3", "f3=5"); // lhu

    cs.mul("J=16", "opcode=35", "f3=0"); // sb
    cs.mul("J=17", "opcode=35", "f3=1"); // sh
    cs.mul("J=18", "opcode=35", "f3=2"); // sw

    cs.mul("J=19", "opcode=19", "f3=0"); // addi
    cs.set_var("J=20", 0); // subi does not exist
    cs.mul("J=21", "opcode=19", "f3=1"); // slli
    cs.nand("J=21", "f7"); // f7 == 0 if slli
    cs.mul("J=22", "opcode=19", "f3=2"); // slti
    cs.mul("J=23", "opcode=19", "f3=3"); // sltui
    cs.mul("J=24", "opcode=19", "f3=4"); // xori

Review comment (bug):
It's not clear to me that this check, while valid, is helpful. We should be explicitly checking that the `f3` chunk corresponds to one of the instructions. 

I feel like this would be a good `debug_assert!`, but not something that should be added to the constraints themselves.

Code after:
    cs.w[f30a] = cs.get_var("f3=0") * &(ONE - cs.get_var("inst_30"));
    cs.w[f30b] = cs.get_var("f3=0") * cs.get_var("inst_30");
    cs.w[f35a] = cs.get_var("f3=5") * &(ONE - cs.get_var("inst_30"));
    cs.w[f35b] = cs.get_var("f3=5") * cs.get_var("inst_30");

    // constraints
    cs.constraint(|cs, a, b, c| {
        a[0] = ONE;
        a[cs.var("inst_30")] = MINUS;
        b[cs.var("f3=0")] = ONE;
        c[f30a] = ONE;
    });
    cs.mul("f3=0b", "f3=0", "inst_30");
    cs.constraint(|cs, a, b, c| {
        a[0] = ONE;
        a[cs.var("inst_30")] = MINUS;
        b[cs.var("f3=5")] = ONE;
        c[f35a] = ONE;
    });
    cs.mul("f3=5b", "f3=5", "inst_30");

    cs.set_eq("J=1", "opcode=55"); // lui
    cs.set_eq("J=2", "opcode=23"); // auipc
    cs.set_eq("J=3", "opcode=111"); // jal
    cs.set_eq("J=4", "opcode=103"); // jalr
    cs.nand("f3", "opcode=103");

    cs.mul("J=5", "opcode=99", "f3=0"); // beq
    cs.mul("J=6", "opcode=99", "f3=1"); // bne
    cs.mul("J=7", "opcode=99", "f3=4"); // blt
    cs.mul("J=8", "opcode=99", "f3=5"); // bge
    cs.mul("J=9", "opcode=99", "f3=6"); // bltu
    cs.mul("J=10", "opcode=99", "f3=7"); // bgeu

    cs.mul("J=11", "opcode=3", "f3=0"); // lb
    cs.mul("J=12", "opcode=3", "f3=1"); // lh
    cs.mul("J=13", "opcode=3", "f3=2"); // lw
    cs.mul("J=14", "opcode=3", "f3=4"); // lbu
    cs.mul("J=15", "opcode=3", "f3=5"); // lhu

    cs.mul("J=16", "opcode=35", "f3=0"); // sb
    cs.mul("J=17", "opcode=35", "f3=1"); // sh
    cs.mul("J=18", "opcode=35", "f3=2"); // sw

    cs.mul("J=19", "opcode=19", "f3=0"); // addi
    cs.set_var("J=20", 0); // subi does not exist
    cs.mul("J=21", "opcode=19", "f3=1"); // slli
    cs.nand("J=21", "f7"); // f7 (technicallly imm[11:5]) == 0 if slli
    cs.mul("J=22", "opcode=19", "f3=2"); // slti
    cs.mul("J=23", "opcode=19", "f3=3"); // sltui
    cs.mul("J=24", "opcode=19", "f3=4"); // xori