simple_sum.pil

namespace std::convert(1024);
    let int = [];
namespace std::prover(1024);
    enum Query {
        Input(int),
        PrintChar(int),
        Hint(fe),
        DataIdentifier(int, int),
    }
    let eval: expr -> fe = [];
namespace main(1024);
    col witness XInv;
    col witness XIsZero;
    main.XIsZero = (1 - (main.X * main.XInv));
    (main.XIsZero * main.X) = 0;
    (main.XIsZero * (1 - main.XIsZero)) = 0;
    col witness _operation_id(i) query std::prover::Query::Hint(10);
    col fixed _block_enforcer_last_step = [0]* + [1];
    (((1 - main._block_enforcer_last_step) * (1 - main.instr_return)) * (main._operation_id' - main._operation_id)) = 0;
    col witness pc;
    col witness X;
    col witness reg_write_X_A;
    col witness A;
    col witness reg_write_X_CNT;
    col witness CNT;
    col witness instr_jmpz;
    col witness instr_jmpz_param_l;
    col instr_jmpz_pc_update = (main.XIsZero * main.instr_jmpz_param_l);
    col instr_jmpz_pc_update_1 = ((1 - main.XIsZero) * (main.pc + 1));
    col witness instr_jmp;
    col witness instr_jmp_param_l;
    col witness instr_dec_CNT;
    col witness instr_assert_zero;
    (main.instr_assert_zero * (main.XIsZero - 1)) = 0;
    col witness instr__jump_to_operation;
    col witness instr__reset;
    col witness instr__loop;
    col witness instr_return;
    col witness X_read_free;
    col witness read_X_A;
    col witness read_X_CNT;
    main.X = (((main.read_X_A * main.A) + (main.read_X_CNT * main.CNT)) + (main.X_read_free * main.X_free_value));
    col fixed first_step = [1] + [0]*;
    main.A' = ((main.reg_write_X_A * main.X) + ((1 - (main.reg_write_X_A + main.instr__reset)) * main.A));
    main.CNT' = (((main.reg_write_X_CNT * main.X) + (main.instr_dec_CNT * (main.CNT - 1))) + ((1 - ((main.reg_write_X_CNT + main.instr_dec_CNT) + main.instr__reset)) * main.CNT));
    col pc_update = (((((main.instr_jmpz * (main.instr_jmpz_pc_update + main.instr_jmpz_pc_update_1)) + (main.instr_jmp * main.instr_jmp_param_l)) + (main.instr__jump_to_operation * main._operation_id)) + (main.instr__loop * main.pc)) + ((1 - ((((main.instr_jmpz + main.instr_jmp) + main.instr__jump_to_operation) + main.instr__loop) + main.instr_return)) * (main.pc + 1)));
    main.pc' = ((1 - main.first_step') * main.pc_update);
    col fixed p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10] + [10]*;
    col witness X_free_value(__i) query match std::prover::eval(main.pc) {
        2 => std::prover::Query::Input(1),
        4 => std::prover::Query::Input(std::convert::int::<fe>((std::prover::eval(main.CNT) + 1))),
        7 => std::prover::Query::Input(0),
    };
    col fixed p_X_read_free = [0, 0, 1, 0, 1, 0, 0, 18446744069414584320, 0, 0, 0] + [0]*;
    col fixed p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*;
    col fixed p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_assert_zero = [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0] + [0]*;
    col fixed p_instr_dec_CNT = [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_jmp = [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_jmp_param_l = [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_jmpz = [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_jmpz_param_l = [0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_instr_return = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*;
    col fixed p_read_X_A = [0, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0] + [0]*;
    col fixed p_read_X_CNT = [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    col fixed p_reg_write_X_A = [0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0] + [0]*;
    col fixed p_reg_write_X_CNT = [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*;
    { main.pc, main.reg_write_X_A, main.reg_write_X_CNT, main.instr_jmpz, main.instr_jmpz_param_l, main.instr_jmp, main.instr_jmp_param_l, main.instr_dec_CNT, main.instr_assert_zero, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_read_free, main.read_X_A, main.read_X_CNT } in { main.p_line, main.p_reg_write_X_A, main.p_reg_write_X_CNT, main.p_instr_jmpz, main.p_instr_jmpz_param_l, main.p_instr_jmp, main.p_instr_jmp_param_l, main.p_instr_dec_CNT, main.p_instr_assert_zero, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_read_free, main.p_read_X_A, main.p_read_X_CNT };
    col fixed _linker_first_step = [1] + [0]*;
    (main._linker_first_step * (main._operation_id - 2)) = 0;