47 lines
No EOL
1.6 KiB
Text
47 lines
No EOL
1.6 KiB
Text
from "utils/pack/bool/unpack.zok" import main as unpack
|
|
from "utils/casts/u32_to_bits" import main as u32_to_bits
|
|
|
|
// this comparison works for any N smaller than the field size, which is the case in practice
|
|
def lt<N>(bool[N] a_bits, bool[N] c_bits) -> bool:
|
|
|
|
bool[N] is_not_smaller_run = [false; N]
|
|
bool[N] size_unknown = [false; N]
|
|
|
|
u32 verified_conditions = 0 // `and(conditions) == (sum(conditions) == len(conditions))`, here we initialize `sum(conditions)`
|
|
|
|
size_unknown[0] = true
|
|
|
|
for u32 i in 0..N - 1 do
|
|
is_not_smaller_run[i] = if c_bits[i] then a_bits[i] else is_not_smaller_run[i] fi
|
|
size_unknown[i + 1] = if c_bits[i] then size_unknown[i] && is_not_smaller_run[i] else size_unknown[i] fi
|
|
verified_conditions = verified_conditions + if c_bits[i] then 1 else if (!size_unknown[i] || !a_bits[i]) then 1 else 0 fi fi
|
|
endfor
|
|
|
|
u32 i = N - 1
|
|
is_not_smaller_run[i] = if c_bits[i] then a_bits[i] else is_not_smaller_run[i] fi
|
|
verified_conditions = verified_conditions + if c_bits[i] then 1 else if (!size_unknown[i] || !a_bits[i]) then 1 else 0 fi fi
|
|
|
|
return verified_conditions == N // this checks that all conditions were verified
|
|
|
|
// this instanciates comparison starting from field elements
|
|
def lt<N>(field a, field c) -> bool:
|
|
bool[N] a_bits = unpack(a)
|
|
bool[N] c_bits = unpack(c)
|
|
|
|
return lt(a_bits, c_bits)
|
|
|
|
// this instanciates comparison starting from u32
|
|
def lt(u32 a, u32 c) -> bool:
|
|
bool[32] a_bits = u32_to_bits(a)
|
|
bool[32] c_bits = u32_to_bits(c)
|
|
|
|
return lt(a_bits, c_bits)
|
|
|
|
def main(field a) -> bool:
|
|
|
|
u32 N = 254
|
|
field c = 42
|
|
|
|
//u32 d = 42
|
|
|
|
return lt::<N>(a, c) |