[Bug] Assertion failed `left == right` in ShrOperation

[pventuzelo]

Assertion failed left == right

We (@fuzzinglabs) found an assertion fail panics while fuzzing in Circuit::enforce().

This error can be triggered directly with the aleo build on the latest release version of the project

aleo build

⏳ Compiling 'foo.aleo'...

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `0`,
 right: `1`: Constant constraint failed: (0 * 1) =?= 1', /home/user/.cargo/registry/src/github.com-1ecc6299db9ec823/snarkvm-circuit-environment-0.9.14/src/circuit.rs:156:29
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Your Environment

• Aleo version: v0.3.6
• rustc 1.66.0-nightly (a37499ae6 2022-09-18)
• Ubuntu 20.04

Expected Behavior

The program should either gracefully exit or use the function halt() that is used in others cases when there's an error. The preferred behavior would be to gracefully exit.

Backtrace

⏳ Compiling 'foo.aleo'...

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `0`,
 right: `1`: Constant constraint failed: (0 * 1) =?= 1', /home/user/.cargo/registry/src/github.com-1ecc6299db9ec823/snarkvm-circuit-environment-0.9.14/src/circuit.rs:156:29
stack backtrace:
   0: rust_begin_unwind
             at /rustc/a37499ae66ec5fc52a93d71493b78fb141c32f6b/library/std/src/panicking.rs:584:5
   1: core::panicking::panic_fmt
             at /rustc/a37499ae66ec5fc52a93d71493b78fb141c32f6b/library/core/src/panicking.rs:142:14
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
   4: std::thread::local::LocalKey<T>::with
   5: <snarkvm_synthesizer::program::instruction::operation::ShrOperation<N> as snarkvm_synthesizer::program::instruction::operation::Operation<N,snarkvm_console_program::data::literal::Literal<N>,snarkvm_console_program::data_types::literal_type::LiteralType,2_usize>>::execute
   6: snarkvm_synthesizer::program::instruction::operation::literals::Literals<N,O,_>::execute
   7: snarkvm_synthesizer::process::stack::execute::<impl snarkvm_synthesizer::process::stack::Stack<N>>::execute_function
   8: snarkvm::package::build::<impl snarkvm::package::Package<N>>::build
   9: aleo::commands::build::Build::parse
  10: aleo::commands::Command::parse
  11: aleo::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Crash File (main.aleo)

program foo.aleo;

function fuzz:
  input r0 as i16.public;
	rem.w r0 r0 into r1;
	shr r1 32u8 into r2;

[ljedrz]

Cc https://github.com/AleoHQ/snarkVM/issues/986.

[howardwu]

@Pratyush @vicsn i think it might be time for us to debug this (along with AleoHQ/snarkVM#986) after multi-executions are feature complete. this issue seems to reappear from time to time (I ran into a similar issue with a community dev in Tokyo).

[vicsn]

Just FYI got a good lead on this - following up in two weeks from now due to some team member's holidays who I asked for input.

[vicsn]

TL;DR: the error is valid but we should decide how to handle build-time and runtime errors for all operators. In order to inform a refactor and update our developer docs, I could investigate for all Aleo/Leo operators what their behavior is at build and runtime on bad constant or dynamic inputs. Alternatively I can just replace the panicking assert(...) with a panicking halt(...).

– The assert which fails, checks whether the Magnitude we shift by is not too big. This is done by checking that enough trailing bits of the rhs we shift right by are zero.

As Alessandro noticed, the logic follows Rust's shr_checked specification, which we use directly when the operands are Constant. The only problem is that we panic instead of gracefully stopping. Noting that:

• These test descriptions imply that we should halt(), which is easy to implement.
• We do have infra in place to cleanly bail!() when the user tries to use the wrong operand types for a particular operator. However, our failure is caused by the value of the operand. Even the smallest type (U8) can hold a value (255) which we should never shift by. Pranav mentioned "I don’t think there is an easy way to modify the circuits APIs to better handle errors."

It looks like other operators are not consistent in dealing with bad input, which I think is worth streamlining so nothing panics:

• assert.eq 1i16 2i16 panics on build, if an operand is dynamic, we cleanly fail ⚠️at runtime
• add 30000i16 30000i16 panics on build, if an operand is dynamic we panic at runtime