param value

private value_bits[] = unpack(value)

digit = 1
linear_combo = []
for bit in value_bits:
    enforce (bit) * (1 - bit) == 0

    linear_combo.append((digit bit))

    digit = digit.double()

enforce (linear_combo) * (~one) == value