Implement slice construction from array literals and Vec::as_slice

[coord-e]

Builds on the codex/slices-basic work (merged into this branch) to add support for constructing &[T] slices from array literals ([T; N]) and from Vec<T> via as_slice, then indexing through them with full refinement-type tracking.

Changes

src/analyze/basic_block.rs

• AggregateKind::Array: Build a Seq<T> model ((Box<Array<Int,T>>, Box<Int>)) from array literal elements by folding store calls to pin each element at its index, then construct the length as Box<N>.
• Rvalue::CopyForDeref: Delegate to env.place_type (same as Use).
• Rvalue::Len: Extract length by projecting field 1 of the Seq tuple and dereffing the box.
• PointerCoercion::Unsize: Identity pass-through for &[T; N] → &[T] (both share the same Seq model).
• mir::Const::Ty: Handle type-level constants (const generics) by extracting their scalar value.

src/refine/env.rs

• Path::Index variant: Projects an element out of a Seq-modeled slice. Gets the inner Array<Int, T>, introduces an existential for the element value, and constrains it with arr.select(idx).

src/analyze/reconstruct_slice_indexing.rs

• Bug fix: remove_bounds_check_setup was incorrectly adding the slice receiver local to lowered_locals when PtrMetadata was applied directly to the slice reference (rather than an intermediate raw-pointer temporary). This caused the receiver's assignment to be NOP'd in-block, making it appear live-in to the entry block. The resulting synthetic unit parameter carried a refinement referencing RefinedTypeVar::Value, which panicked when value_var was None (empty tuple → singleton sort). Fix: skip raw_place.local when it equals the receiver local.

std.rs

• [T; N] model: impl<T: Model, const N: usize> Model for [T; N] mapping to Seq<T::Ty>.
• Vec::as_slice extern spec: #[ensures(*result == *vec)] — copies the Seq refinement from the Vec to the returned slice.

Tests

10 new UI tests (5 pass / 5 fail):

Test	What it checks
pass/array_literal_1.rs	Build [1i32,2,3], coerce to &[i32], assert s[0]==1
pass/array_literal_2.rs	4-element array, access last element
pass/array_literal_3.rs	&mut [i32], write through slice, verify updated value
pass/array_literal_4.rs	[&mut i32; 2], dereference through slice
pass/vec_as_slice.rs	Push 10, 20 to Vec, as_slice, assert len and element values
fail/array_literal_1.rs	Wrong expected value → Unsat
fail/array_literal_2.rs	Out-of-bounds index → Unsat
fail/array_literal_3.rs	Read stale value after write → Unsat
fail/array_literal_4.rs	Wrong expected value through &mut → Unsat
fail/vec_as_slice.rs	Wrong expected element value → Unsat

---

Generated by Claude Code