Add slice construction from array literals by coord-e · Pull Request #158 · coord-e/thrust

coord-e · 2026-06-29T05:19:24Z

Adds support for constructing &[T] slices from array literals ([T; N]) and indexing through them with full refinement-type tracking.

Changes

`src/analyze/basic_block.rs`

AggregateKind::Array: Build the Seq<T> model from array literal elements by folding store calls to pin each element at its index and recording the static length. This is intentionally model-aware — following the precedent of Verus, Prusti, and Creusot, array literal construction is a primitive whose semantics the verifier encodes directly (analogous to integer arithmetic), rather than routing through user-visible extern specs.
Rvalue::CopyForDeref: Delegate to env.place_type (same as Use).
Rvalue::Cast(PointerCoercion::Unsize): Identity pass-through for &[T; N] → &[T] (both share the same Seq<T> model).
mir::Const::Ty: Handle type-level constants (const generics, e.g. array length N) by extracting their scalar value.

`src/analyze/reconstruct_slice_indexing.rs`

Bug fix: remove_bounds_check_setup was incorrectly NOP'ing the slice receiver local when PtrMetadata was applied directly to it (rather than to a raw-pointer temporary). This caused the receiver's assignment to be erased in-block, making it appear live-in to the entry block, and ultimately panicking in Instantiator::instantiate when a synthetic unit parameter carried a RefinedTypeVar::Value refinement with value_var = None. 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 model::Seq<T::Ty>, consistent with [T].

Tests

6 new UI tests (3 pass / 3 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
`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

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: adb2eab745

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-07-01T14:47:20Z

+                        let base_idx = builder.push_existential(chc::Sort::array(
+                            chc::Sort::int(),
+                            elem_ty.to_sort(),
+                        ));
+                        let mut arr_term: chc::Term<PlaceTypeVar> = chc::Term::var(base_idx.into());


Start array literals from a canonical empty array

When two array literals with the same visible elements are compared, this existential base makes their Seq array components arbitrary outside 0..N. Since the [T; N] model is model::Seq and equality/PartialEq compares the underlying tuple/array extensionally, a case like comparing two independently constructed [1i32, 2] values cannot be proved equal even though Rust array equality only depends on the initialized elements. Build the literal from a canonical array_empty term instead of a fresh unconstrained array so equal literals don't differ outside their length.

Useful? React with 👍 / 👎.

Copilot

Pull request overview

Adds verifier support for constructing &[T]/&mut [T] slices from array literals ([T; N]) while preserving refinement-type tracking through indexing, and fixes a MIR slice-indexing reconstruction edge case involving PtrMetadata.

Changes:

Teach the MIR analyzer to model array literals as Seq<T> by folding element stores and recording a static length; add handling for type-level consts and CopyForDeref.
Treat &[T; N] → &[T] unsize coercions as model-preserving, and fix remove_bounds_check_setup to avoid NOP’ing the slice receiver local in a specific PtrMetadata shape.
Add 6 UI tests covering correct slice reads/writes through array-literal-backed slices and expected failures (unsat/out-of-bounds/stale read).

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/analyze/basic_block.rs	Models array literal construction as a `Seq<T>` and extends rvalue/const handling to support the new slice-from-array behavior.
src/analyze/reconstruct_slice_indexing.rs	Fixes bounds-check temporary cleanup to avoid erasing the slice receiver assignment in certain MIR patterns.
std.rs	Adds a `[T; N]` `Model` impl mapping arrays to the same `Seq<T>` model as slices.
tests/ui/pass/array_literal_1.rs	Pass case: read `s[0]` after coercing `&[T; N]` to `&[T]`.
tests/ui/pass/array_literal_2.rs	Pass case: access last element via slice indexing.
tests/ui/pass/array_literal_3.rs	Pass case: write through `&mut [T]` and observe updated value.
tests/ui/fail/array_literal_1.rs	Fail case: wrong expected value yields `Unsat`.
tests/ui/fail/array_literal_2.rs	Fail case: out-of-bounds slice index yields `Unsat`.
tests/ui/fail/array_literal_3.rs	Fail case: reading stale value after write yields `Unsat`.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Handle `Rvalue::Aggregate(Array, ...)` by building a Seq<T> model (Box<Array<Int,T>>, Box<Int>) whose array component is the store-fold of all literal elements and whose length is the static count N. Also handle `mir::Const::Ty` (type-level constants, e.g. array length N) by extracting the scalar integer and delegating to `const_value_ty`. Map `[T; N]` to `model::Seq<T::Ty>` in `std.rs`, matching `[T]` and `Vec<T>`. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP

Support the MIR operations needed to turn `[T; N]` into `&[T]` and index it: - `Rvalue::CopyForDeref`: pass-through to the place type (coerce-for-deref). - `Rvalue::Cast(PointerCoercion::Unsize)`: identity coercion since `[T; N]` and `[T]` share the same `Seq<T>` model. Fix a bug in `remove_bounds_check_setup` where the slice receiver local was incorrectly NOP'd when `PtrMetadata` was applied directly to it. The receiver must remain live for the reconstructed `Index::index` call. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP

coord-e force-pushed the claude/slice-construction-tstquo branch 6 times, most recently from d1cab50 to eb0c396 Compare July 1, 2026 14:39

coord-e changed the title ~~Implement slice construction from array literals and Vec::as_slice~~ Add slice construction from array literals Jul 1, 2026

coord-e force-pushed the claude/slice-construction-tstquo branch from eb0c396 to adb2eab Compare July 1, 2026 14:42

coord-e marked this pull request as ready for review July 1, 2026 14:42

coord-e requested a review from Copilot July 1, 2026 14:42

Copilot started reviewing on behalf of coord-e July 1, 2026 14:43 View session

chatgpt-codex-connector Bot reviewed Jul 1, 2026

View reviewed changes

Copilot AI reviewed Jul 1, 2026

View reviewed changes

Comment thread src/analyze/basic_block.rs

Comment thread src/analyze/basic_block.rs Outdated

Comment thread src/analyze/basic_block.rs

claude added 2 commits July 2, 2026 00:32

coord-e force-pushed the claude/slice-construction-tstquo branch from ab15156 to 878aa3c Compare July 1, 2026 15:32

coord-e merged commit c22ad90 into main Jul 1, 2026
6 checks passed

coord-e deleted the claude/slice-construction-tstquo branch July 1, 2026 15:34

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add slice construction from array literals#158

Add slice construction from array literals#158
coord-e merged 2 commits into
mainfrom
claude/slice-construction-tstquo

coord-e commented Jun 29, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Jul 1, 2026

Uh oh!

coord-e Jul 1, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

coord-e commented Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

src/analyze/basic_block.rs

src/analyze/reconstruct_slice_indexing.rs

std.rs

Tests

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jul 1, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jul 1, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

coord-e commented Jun 29, 2026 •

edited

Loading

`src/analyze/basic_block.rs`

`src/analyze/reconstruct_slice_indexing.rs`

`std.rs`