Round last three digits of a frontend.variable number

[2pir2]

I am trying to round a frontend.variable number based on the last three digits. For example, 1234 would be rounded to 1000 since 234 is less than 500 and 1501 would be 2000. However, since there is no modular operation, I am wondering if there is any alternative method to do so?

[ivokub]

I think there is no direct way. You would have to resort to using hints (non-deterministic computation) to obtain this.

Essentially, lets say you have a variable a = a_high + 1000 * a_low. Using a hint you provide the results a_high and a_low non-deterministically and then in-circuit you assert that the equation holds. However, keep in mind that you also have to assert that a_low < 1000 and a_high < native_modulus/1000.

See as an example std/math/bitslice.Partition implementation how this can be done.

[ivokub]

See also the example in #1362 (comment). In your case it should be a bit different as you have fixed the modulus, so you can hardcode it in the hint etc. But on a high level should be very similar.