Cleanup prusti-contracts, add/implement all Viper builtins

[JonasAlaif]

Native Viper collections, executable ghost types, and reworked ghost! blocks

This PR completes the prusti_contracts ghost types (Seq, Set, Multiset, Map,
Ghost, alongside the existing Int/Real): the collections are now encoded as the
corresponding native Viper collection types, ghost types can be used in executable
(impure) code, and ghost! blocks are redesigned to be value-producing, codegen-free, and
verified inline — in both impure and pure code.

prusti-contracts: one API surface, safe to execute

The ghost types are rewritten as zero-sized types in a private_shared module compiled under
both the prusti and non-prusti features. The split is by executability: everything in
the shared module has real (non-panicking) bodies and is safe to run, while operations only
available under the prusti flag are the ones whose use in executable code is rejected with
a verification error (rather than ever reaching their panicking bodies at runtime).

• Seq<T>/Set<T>/Multiset<T>/Map<K, V> with a uniform API (new, single,
  append/union, update, insert, intersection, difference, is_subset,
  contains, len, keys, values, setminus) and the seq!/set!/multiset!/map!
  literal macros. A Value<T> helper trait lets elements be passed as T or &T.
• Indexing: seq[i] and map[k] return Ghost<T> (deref for the value); seq[a..b],
  seq[a..], seq[..b] return subsequences.
• PartialEq on all ghost types is snapshot equality; a === b now desugars to
  Ghost::new_ref(&a) == Ghost::new_ref(&b), replacing the removed snapshot_equality and
  snap functions. The float classification helpers get real bodies.

VIR: native collection support

TypeKind gains Seq/Multiset/Map alongside Set, with new expression nodes:
CollectionBinOp (contains/union/intersection/difference/subset/concat/index/take/drop —
separate from BinOpKind because the operands are heterogeneously typed and the operation is
selected by the collection operand's type), CollectionLiteral, CollectionUpdate
(x[k := v]), CollectionLen, MapDomain, and MapRange; plus statically-typed,
type-checked mk_* constructors and expr! macro syntax for the new operations
((x) in (c), (a) setminus (b), (base)[index], |c|, domain(m), !(b)).

Encoder: operand-based builtin encoding

PrustiBuiltin classifies calls into prusti_contracts (attributing trait-method calls via
the resolved impl, so e.g. PartialOrd::le on Int is recognized even though the default
body lives in core). All operand-based builtins are encoded once per (op, generics) by
PrustiBuiltinEnc as a cached snapshot expression with one hole per operand, shared by the
pure and impure encoders. The collections are encoded at their most generic instantiation
(s_Param elements) with casters applied at use sites.

Partial operations (s[i], s[i := v], m[k], slicing) are encoded by context:

• Impure code uses the checked native form: the well-definedness obligation becomes a
  verification condition with a dedicated message ("the sequence index may be out of
  bounds", "the map may not contain this key", …), matching Rust's panicking semantics.
• Pure code uses total uninterpreted wrappers (CollectionOpsEnc), axiomatized to
  agree with the native operation on their domain — precondition-free f_ functions could
  never discharge the obligation.

Ghost types are now allowed in executable code: construction, arithmetic, collection
updates etc. encode as snapshot assignments. Spec-only operations (comparisons yielding
bool, Ghost deref, contains, is_subset, …) remain rejected in executable code —
except inside ghost blocks (below).

ghost! blocks, redesigned

ghost! { body } now expands to:

if false {
    ghost_call(&(|| { body }), { body })   // dead arm: verified, never codegened
} else {
    ghost_erased()                          // live path: constructs the Ghost ZST
}

• The body appears inline as real MIR (what gets verified) and duplicated into a
  never-called Fn closure, so the compiler enforces ghost discipline: no mutation,
  mutable borrowing, or consumption of outer variables (rebind instead:
  let x = ghost! { .. }). ghost_call's signature unifies the two copies' types, and the
  if/else gives ghost_erased() the body's type — so let x = ghost! { .. } binds a
  Ghost<T> inferable from either side.
• The whole ghost arm sits in if false, so it is pruned before codegen — the runtime
  effect of a ghost block is exactly Ghost(PhantomData).
• Both encoders detect ghost blocks the same way (GhostBlocks, keyed off the single-block
  ghost_erased stand-in arm) and encode the switch as an unconditional jump into the ghost
  arm; within the ghost region (blocks dominated by the arm entry) spec-only builtins are
  allowed.
• Ghost bodies run in the enclosing frame: they capture runtime values, read through
  references in scope, call pure and impure (contract-checked) functions, branch, loop
  (with body_invariant!), contain prusti_assert!s, and nest. ghost! also works in
  pure functions.
• The macro rejects all early exits (return, break, continue, and now ?) with
  "Can't leave the ghost block early", while correctly allowing them inside closures/items
  nested in the body. The old ghost_begin/ghost_end marker machinery is removed
  throughout.

Other encoder changes

• ImpureEncVisitor::visit_body walks blocks in reverse-postorder instead of BFS, so
  both branches are always encoded before their join; a new wandless_calls set correctly
  exempts all non-method-call terminators (pure calls, intrinsics, builtins) from wand
  application on borrow expiry.
• Method-body encoding errors now surface as early errors instead of silently degrading the
  method to a contract-only stub.
• Fixed an ICE when naming nested closure types (e.g. a quantifier's closure inside an
  assertion's closure); regression test: quick/forall-in-assert.rs.
• Cleanups: deduplicated quantifier/spec-block closure encoding, impure closure aggregates
  (needed for the checker closures).

Tests

• New verify/pass/ghost-types/ suites: int, sequences, sets, multisets, maps,
  unsized, ordering, extended ghost/impure, and blocks (29 items covering value
  binding, spec-only ops in ghost code, capture/flow, calls, loops with invariants,
  nesting, generics, inference through the binding, pure-code ghost blocks).
• New verify/fail/ghost-types/ suites: bounds (checked collection ops), blocks
  (failing asserts in ghost code, ghost values are constrained, contract violations,
  panicking bodies), captures (the Fn capture discipline).
• Existing core_proof ghost tests and counterexample UI tests migrated to the new API.

Breaking changes

• Seq::empty/concat/lookup → Seq::new/append/indexing (via Ghost);
  Map::empty/lookup → Map::new/indexing; snapshot_equality/snap removed (===
  still works); DerefMut for Ghost removed.
• Assigning to variables captured by a ghost! block no longer compiles; rebind the result
  instead (let x = ghost! { .. };).