contract bits_decomposition param x {% for n in range(255) %} private b_{{n}} {% endfor %} unpack_bits x b_0 b_254 {% for n in range(255) %} # (1 - b) * b == 0 lc0_add_one lc0_sub b_{{n}} lc1_add b_{{n}} enforce {% endfor %} lc0_add_bits b_0 lc0_sub x enforce end