z3 proof that mulv works up to 64bit

minimal_bitvec.cpp

// code proven:
// mulv - multiplication oVerflow
//   var res: ST = a *% b;
//   if (a != 0 and @divTrunc(res, a) != b) {
//       return -5; // overflow case
//   }
//   return res;

void minimal_bitvec() {
    z3::context ctx;
    z3::expr a = ctx.bv_const("a", 64);
    z3::expr b = ctx.bv_const("b", 64);
    z3::expr res = ctx.bv_const("res", 64);
    z3::expr i64max = ctx.bv_const("i64max", 64);
    z3::expr i64min = ctx.bv_const("i64max", 64);
    z3::expr mulres = ctx.bv_const("mulres", 64);
    int64_t maxi64 = 2147483647;
    int64_t mini64 = -2147483648;
    i64min = ctx.bv_val(mini64, 64);
    i64max = ctx.bv_val(maxi64, 64);

    //z3::expr tmp =
    //(
    //  1 <= a && a <= 2147483647 && 1 <= b && b <= 2147483647
    //  && mulres == a*b
    //  && res == z3::smod(mulres,i64max)
    //  && res / a == b
    //);
    //z3::expr cond = (i64min <= mulres && mulres <= i64max);
    //z3::expr implies = z3::implies(tmp, cond);

    z3::expr tmp =
    (
      i64min <= a && a <= -1 && i64min <= b && b <= -1
      && mulres == a*b
      && res == z3::smod(mulres,i64min)
      && res / a == b
    );
    z3::expr cond = (i64min <= mulres && mulres <= i64max);
    z3::expr implies = z3::implies(tmp, cond);

    z3::expr_vector forallvec(ctx);
    forallvec.push_back(a);
    forallvec.push_back(b);
    forallvec.push_back(res);
    z3::expr forallexpr = z3::forall(forallvec, implies);
    //z3::expr forallexpr = z3::exists(forallvec, tmp);
    z3::solver solver(ctx);
    solver.add(forallexpr);
    z3::check_result proofres = solver.check();
    assert(proofres == z3::check_result::sat);
    std::cout << "sat\n";
    z3::model m = solver.get_model();
    std::cout << "model satisfiable:\n" << m << "\n";
}
int main() {
    minimal_bitvec();
    Z3_finalize_memory();
    return 0;
}
// usage: insert into z3/examples/c++/ and adjust its CMakeLists.txt:
//set(Z3_DIR "PATHTO/z3/build")
//set(Z3_LIBRARIES "PATHTO/z3/build/libz3.so")
//add_executable(minimal_bitvec minimal_bitvec.cpp.)
//target_include_directories(minimal_bitvec PRIVATE ${Z3_CXX_INCLUDE_DIRS})
//target_link_libraries(minimal_bitvec PRIVATE ${Z3_LIBRARIES})