LLBC backend: constructs that still abort translation

[feliperodri]

These constructs abort the compiler with the LLBC backend (kani -Zlean --print-llbc), all at the backend's own todo!()s rather than anything in Charon. Checked on the old Charon pin and again after the bump (#4883); the list is the same.

Construct	Minimal example	Stops at
Casts	a as u32	translate_cast is a bare todo!()
Arrays / const generics	[1u8, 2, 3], fn len<const N: usize>(_: [u8; N])	ConstantKind::Ty(_) in translate_constant_value
Slices	fn first(s: &[u8]) -> u8 { s[0] }	UnOp::PtrMetadata
str literals	fn name() -> &'static str { "kani" }	translate_allocation has no case for &str
Box	Box::new(3)	RigidTy::Pat (the pattern type inside NonNull)
Supertraits	trait Named: Shape { fn id(&self) -> u32 { self.sides() + 1 } }	Instance::resolve(..).unwrap() of the default method, in translate_terminator
Associated consts	fn limit<T: HasLimit>() -> u32 { T::LIMIT }	"Expect free type var id" in translate_generic_args

Each is a separate piece of work. The first three are probably the most useful, since almost any real code hits them. tests/llbc has no coverage for any of these yet — a test should come with each fix.