fix: handle panics for Structural

[nuczyc]

Replace reachable panics in source/rust_verify/src/rust_to_vir_impl.rs with user-facing errors when verus_builtin::Structural is implemented for non-ADT types.

PoCs:

use vstd::prelude::*;

verus! {

struct Local {
}

unsafe impl verus_builtin::Structural for &mut Local {
}

}

fn main() {}

and

use vstd::prelude::*;

verus! {

struct Local {
}

type Alias = &'static mut Local;

unsafe impl verus_builtin::Structural for Alias {
}

}

fn main() {}

Logs

thread 'rustc' (2754427) panicked at rust_verify/src/rust_to_vir_impl.rs:281:26:
self type of impl is not resolved: Ref(Lifetime { hir_id: HirId(DefId(0:6 ~ 17[bab3]::{impl#0}).5), ident: '_#0, kind: Param(DefId(0:7 ~ 17[bab3]::{impl#0}::'_)), source: Reference, syntax: Implicit }, MutTy { ty: Ty { hir_id: HirId(DefId(0:6 ~ 17[bab3]::{impl#0}).6), span: /home/yuchen/verus-rag/issue/17.rs:8:48: 8:53 (#0), kind: Path(Resolved(None, Path { span: /home/yuchen/verus-rag/issue/17.rs:8:48: 8:53 (#0), res: Def(Struct, DefId(0:5 ~ 17[bab3]::Local)), segments: [PathSegment { ident: Local#0, hir_id: HirId(DefId(0:6 ~ 17[bab3]::{impl#0}).7), res: Def(Struct, DefId(0:5 ~ 17[bab3]::Local)), args: None, infer_args: false }] })) }, mutbl: Mut })
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

and

thread 'rustc' (2735939) panicked at rust_verify/src/rust_to_vir_impl.rs:298:17:
Structural impl for non-adt type
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Now Verus reports: Structural can only be implemented for struct or enum types

[nuczyc]

Treat UnaryOp::StrLen, BinaryOp::StrGetChar, and UnaryOp::CastToInteger as non-trigger/internal wrapper expressions instead of hitting unreachable!/panic!.

PoCs:

use vstd::prelude::*;

verus! {

spec fn f(i: int) -> bool { i == i }

proof fn test<A: Integer>(a: A) {
    assert(forall|b: bool| f(spec_cast_integer::<A, int>(a)));
}

}

fn main() {}

and

use vstd::prelude::*;

verus! {
proof fn test() {
    use verus_builtin::*;
    assert(forall|i: u64| strslice_len::<u64>(i) >= 0int);
}
}

fn main() {}

Logs

thread '<unnamed>' (2646684) panicked at vir/src/triggers_auto.rs:391:13:
internal error: CastToInteger should have been removed before here
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (2646684) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

and

thread '<unnamed>' (202344) panicked at vir/src/triggers_auto.rs:305:9:
internal error: entered unreachable code: internal error: doesn't make sense to reach `gather_terms` for string operations defined for verus_builtin, these are only used to tie verus_builtin and vstd together and do not make sense in user programs
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (202344) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

Now Verus reports: Could not automatically infer triggers for this quantifier. Use #[trigger] annotations to manually mark trigger terms instead.

[nuczyc]

The new commit fixes:
https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=c2ba3347880fc2c32d2c8e6d3fd99845

[nuczyc]

Fix https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=56c50a023852d55ab91a7248ee56dfdf
Now Verus reports: unexpected FnProof argument.