ICmp does not work with signed values

[0xThemis]

During the ICMP handling, the parser behaves incorrectly if one of the operands is negative (additionally, it does not constrain anything at the moment). The problem arises because the comparison simply compares the underlying field elements by "<", ">" etc. For negative values, which are greater than modulus / 2, this yields a wrong result.

The code responsible can be seen here:

            template<typename map_type>
            void handle_scalar_cmp(const llvm::ICmpInst *inst, map_type &variables) {
                // omitted
                if (p == llvm::CmpInst::ICMP_EQ || p ==llvm::CmpInst::ICMP_NE) {
                // omitted
                } else {
                    bool res;
                    switch (p) {
                    case llvm::CmpInst::ICMP_SGE:
                    case llvm::CmpInst::ICMP_UGE:{
                        res = (var_value(assignmnt, lhs) >= var_value(assignmnt, rhs));
                        break;
                    }

// rest omitted....

For a fast fix, we check whether one of the operands (or both) is negative, then change the final result depending on that, as seen here:

            template<typename map_type>
            void handle_scalar_cmp(const llvm::ICmpInst *inst, map_type &variables) {
                // omitted

                if (p == llvm::CmpInst::ICMP_EQ || p ==llvm::CmpInst::ICMP_NE) {
                // omitted
                } else {
                    auto P_HALF = BlueprintFieldType::modulus / 2;
                    bool leftNegative = var_value(assignmnt, lhs) > P_HALF;
                    bool rightNegative = var_value(assignmnt, rhs) > P_HALF;
                    bool res;
                    switch (p) {
                    case llvm::CmpInst::ICMP_SGE:
                    case llvm::CmpInst::ICMP_UGE:{
                        res = (var_value(assignmnt, lhs) >= var_value(assignmnt, rhs));
                        res ^= leftNegative;
                        res ^= rightNegative;
                        break;
                    }
// rest omitted....

Of course, more is needed to solve the soundness, and it requires better handling.

Here is a small example where you can reproduce the problem. The input should be 5. We compare if $(5 * -1) &lt; 10000$, which should be clearly true. Compiled with clang++, the compiled binary writes 1 to the console. When running with the assigner binary and circuit output enabled, we can see that it, in fact, outputs 0.

#include <stdlib.h>
#include <stdint.h>

#ifndef __ZKLLVM__
#include <iostream>
#endif


[[circuit]] int check_negative_number(signed a) {
  #ifdef __ZKLLVM__
  __builtin_assigner_exit_check(a==5);
  #endif
  bool b = (a * -1) < 10000;
  #ifndef __ZKLLVM__
  std::cout << b << std::endl;
  #endif
  return b;
}

#ifndef __ZKLLVM__

int main (int argc, char *argv[]){

    check_negative_number(5);
    return 0;
}
#endif