Closed
Description
While exploring Aiur (in Lean), I created following program that does bitwise left-shifting:
-- Left-shifting by k is the same as multiplying an unsigned integer by 2^k, e.g.:
-- x << 1 = x + x // 2x
-- x << 2 = (x + x) + (x + x) // 4x
-- x << 3 = (x + x) + (x + x) + (x + x) + (x + x) // 8x
-- ...
-- x << k = x ⋆ 2^k
fn shl(a: u64, b: u64) -> u64 {
if b {
shl(add(a, a), sub(b, 1u64))
} else {
a
}
}
Trying to run the aiurTest with it on the following cases gives me following:
⟨`shl, #[0xffffffffffffffff, 1], #[0xfffffffffffffffe] ⟩, Expected '"ok _"' but got '"error constraint error: zerocheck naive witness validation failed: func-shared-constraint-0, vertex index 1"'
⟨`shl, #[0xffffffffffffffff, 2], #[0xfffffffffffffffc] ⟩, StackOverflow
⟨`shl, #[0xffffffffffffffff, 10], #[0xfffffffffffffc00] ⟩, StackOverflow