From ba08fb688aa88971db46b8d9950c792147502341 Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Fri, 7 Apr 2023 17:16:50 +0300 Subject: [PATCH] feat: add range checker bus constraints --- constraints/miden-vm/range_checker_bus.air | 24 ++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 constraints/miden-vm/range_checker_bus.air diff --git a/constraints/miden-vm/range_checker_bus.air b/constraints/miden-vm/range_checker_bus.air new file mode 100644 index 00000000..0bfda99c --- /dev/null +++ b/constraints/miden-vm/range_checker_bus.air @@ -0,0 +1,24 @@ +mod RangeCheckerBusAir + +### Helper functions ############################################################################## + +# Returns array of mutually exclusive multiplicity flags. +# p[0] set to 1 when we don't include the value into the running product. +# p[1] set to 1 when we include the value into the running product. +# p[2] set to 1 when we include two copies of the value into the running product. +# p[3] set to 1 when we include four copies of the value into the running product. +fn get_multiplicity_flags(s0: scalar, s1: scalar) -> vector[4]: + return [!s0 & !s1, s0 & !s1, !s0 & s1, s0 & s1] + + +### Range Checker Bus Air Constraints ################################################################ + +ev range_checker_bus(main: [t, s0, s1, v], aux: [b_range]): + let val = $alpha[0] + v + let f = get_multiplicity_flags(s0, s1) + + # z represents how a row in the execution trace is reduced to a single value. + let z = val^4 * f[3] + val^2 * f[2] + val * f[1] + f[0] + enf b_range' = b_range * (z * t - t + 1) + + # TODO: add boundary constraints b_range.first = 1 and b_range.last = 1 \ No newline at end of file