Contracts: Can't include non-Copy types in contract

[adpaco-aws]

When trying out the contracts feature (from Kani 0.46.0) in one of my projects, I got the following errors:

error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
  --> src/lib.rs:79:5
   |
79 |     #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
   |
   = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
  --> src/lib.rs:79:5
   |
79 |     #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
   |
   = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0507`.
error: could not compile `interpreter` (lib) due to 3 previous errors
error: Failed to execute cargo (exit status: 101). Found 3 compilation errors.

I've opened #3026 for improving the error message, but anyway it's clear to me that it's asking for Expr to implement Copy. In my case, Expr is an enum defined as follows:

pub enum Expr {
    Int(i32),
    Bool(bool),
    If {
        test_expr: Box<Expr>,
        then_expr: Box<Expr>,
        else_expr: Box<Expr>,
    },
    BinaryApp {
        op: BinaryOp,
        arg1: Box<Expr>,
        arg2: Box<Expr>,
    },
}

Here, the usage of Box<...> prevents me from directly deriving the Copy trait. As far as I know, the Copy trait cannot be implemented for Box<...> because we'd end up with multiple boxes referencing the same value.

Can you recommend a good workaround for this? I think it should be possible to have a custom impl for Copy that behaves like Clone, but then I'm not sure it'd work with the contracts implementation (and I'd expect performance issues even if it did).

If you'd like to reproduce the error or anything else, the complete program can be found in the kani-contracts branch of my project. Once it's cloned, simply run cargo kani.

[JustusAdam]

Yes, this makes sense. Why does typecheck_2 take e by value and not by reference? I think that would fix your problem.

The problem is not that contracts in general need Copy, but typecheck_2 which you're calling in the contract takes e by value and thus requires Copy.

[JustusAdam]

But also I think we could probably avoid actually renaming e to e_renamed and instead rely on macro hygiene to distinguish the two. That would improve the error message.

[adpaco-aws]

The problem is not that contracts in general need Copy, but typecheck_2 which you're calling in the contract takes e by value and thus requires Copy.

Oh, I see. Then let me check if I can pass a reference instead. Thank you!

[adpaco-aws]

If I pass the argument by reference then rustc crashes:

thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow
error: could not compile `interpreter` (lib); 2 warnings emitted

Caused by:
  process didn't exit successfully: `/Users/adrian/.kani/kani-0.46.0/bin/kani-compiler --crate-name interpreter --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=99 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 -C split-debuginfo=unpacked -Cllvm-args=--reachability=harnesses -C metadata=1a58319f898c6d22 -C extra-filename=-1a58319f898c6d22 --out-dir /Users/adrian/bolero-playground-clean/interpreter/target/kani/x86_64-apple-darwin/debug/deps --target x86_64-apple-darwin -C incremental=/Users/adrian/bolero-playground-clean/interpreter/target/kani/x86_64-apple-darwin/debug/incremental -L dependency=/Users/adrian/bolero-playground-clean/interpreter/target/kani/x86_64-apple-darwin/debug/deps -L dependency=/Users/adrian/bolero-playground-clean/interpreter/target/kani/debug/deps --extern bolero=/Users/adrian/bolero-playground-clean/interpreter/target/kani/x86_64-apple-darwin/debug/deps/libbolero-64e9f6a7f1410dbc.rmeta --extern bolero_generator=/Users/adrian/bolero-playground-clean/interpreter/target/kani/x86_64-apple-darwin/debug/deps/libbolero_generator-d989fabb5284594b.rmeta -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /Users/adrian/.kani/kani-0.46.0 -L /Users/adrian/.kani/kani-0.46.0/lib --extern kani --extern 'noprelude:std=/Users/adrian/.kani/kani-0.46.0/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes --kani-compiler '-Cllvm-args=--check-version=0.46.0 --log-level=warn --assertion-reach-checks --goto-c'` (signal: 6, SIGABRT: process abort signal)
error: Failed to execute cargo (exit status: 101). Found 0 compilation errors.

I've pushed the commit to the branch kani-contracts-crash.