contract bits_decomposition
    param x
    {% for i in range(256) %}
        private b_{{i}}
    {% endfor %}

    # x is unpacked into little endian order
    unpack_bits x b_0 b_255

    {% for i in range(256) %}
        # (1 - b) * b == 0
        lc0_add_one
        lc0_sub b_{{i}}

        lc1_add b_{{i}}

        enforce
    {% endfor %}

    {% for i in range(256) %}
        lc0_add b_{{i}}
        lc_coeff_double
    {% endfor %}
    lc_coeff_reset
    lc0_sub x
    lc1_add_one
    enforce
end