let N: int = 0x10000;

namespace std::prover;
    let provide_value: expr, int, fe -> () = [];

namespace SimpleDiv(N);
    col fixed BYTE(i) { i & 0xff };

    col witness X;
    col witness Y;
    col witness Z;
    col witness R;
    // We introduce an underconstrained column which we set to 1 at runtime.
    // This is hacky and unsafe, but it enables blocking the linear constraint optimizer from removing the entire program.
    col witness one;
    query |i| {
        std::prover::provide_value(one, i, 1);
    };

    // Compute X = Y / Z, i.e.
    // X * Z + R = Y, where 0 <= R < Z

    Z = 3;
    Y = 13;

    X * Z + R = Y;
    Z - R - 1 = Y_b1 + Y_b2 * 0x100;
    X = one * (X_b1 + X_b2 * 0x100);
    R = one * (R_b1 + R_b2 * 0x100);

    col witness Y_b1;
    col witness Y_b2;
    col witness X_b1;
    col witness X_b2;
    col witness R_b1;
    col witness R_b2;
    [ Y_b1 ] in [ BYTE ];
    [ Y_b2 ] in [ BYTE ];
    [ X_b1 ] in [ BYTE ];
    [ X_b2 ] in [ BYTE ];
    [ R_b1 ] in [ BYTE ];
    [ R_b2 ] in [ BYTE ];

    // now the check:
    col fixed CHECK = [0, 0, 0, 0, 0] + [1] + [0]*;
    CHECK * (X - 4) = 0;
    CHECK * (R - 1) = 0;