Phase 1: Seq<T> ghost type

[coord-e]

Summary

Phase 1 of the Creusot-style ghost-sequence support tracked in
/root/.claude/plans/how-can-we-implement-buzzing-cascade.md. Eventual
goal: verify Creusot's iter::Map / iter::MapExt in Thrust.

Introduces thrust_models::model::Seq<T> as (Array<Int, T>, Int)
(mirroring the existing Vec model). Operations:

Op	Lowering
Seq::<T>::empty()	(seq_default_arr_int, 0)
Seq::singleton(e)	(store(seq_default_arr_int, 0, e), 1)
s.len()	tuple_proj(s, 1)
s.push(e)	(store(fst(s), snd(s), e), snd(s) + 1)
s[i]	select(fst(s), i)
s.concat(t)	(seq_concat_arr_int(fst(s), snd(s), fst(t), snd(t)), snd(s) + snd(t))
s.subsequence(l, r)	(seq_subseq_arr_int(fst(s), l, r), r - l)

seq_default_arr_int is ((as const (Array Int Int)) 0), always emitted
in the SMT preamble. Its concrete contents are irrelevant because callers
never access indices past the tracked length.

seq_concat_arr_int and seq_subseq_arr_int are emitted via SMT-LIB2
(define-fun-rec ...), gated by System::uses_seq_concat /
uses_seq_subseq so the recursive declarations are only in scope when
the analyzer has lowered at least one use. Unconditionally emitting the
two define-fun-rec definitions noticeably slows pcsat on unrelated
tests (a baseline ≈1 s test ran into the tens of seconds in
measurement), so gating is needed even for code paths that never touch
Seq.

Indexed reasoning

concat / subsequence length-only properties verify directly under
either solver because the length is computed inline by the analyzer.

For whole-Seq equality with a constant recursion bound (e.g.
Seq::singleton(x).concat(Seq::empty()) == Seq::singleton(x)), pcsat
unfolds the define-fun-rec definitions directly. The third commit
ships paired pass/fail tests (seq_concat_const, seq_subseq_const)
that exercise this without any peephole help — whole-Seq equality
reduces to tuple/array equality without ever constructing a
select(seq_concat_arr_int(...), _) term, so the follow-up commit's
peephole does not apply.

For unbounded indexed access (e.g. s.concat(t)[i] == s[i] when
i < s.len()), the fourth commit adds a chc::Term::select peephole
that rewrites one unfolding step of the recursive definitions:

select(seq_concat_arr_int(sa, sn, ta, tn), i)
  ↦ ite(i < sn, select(sa, i), select(ta, i - sn))

select(seq_subseq_arr_int(a, l, r), i)
  ↦ ite(0 <= i < r - l,
        select(a, l + i),
        select(seq_default_arr_int, 0))

The define-fun-rec definitions remain the ground truth — the rewrites
are exactly one unfolding step — but pcsat can prove unbounded indexed
properties against the inlined ITE form, where unfolding through
define-fun-rec over a universally quantified recursion bound requires
an inductive invariant pcsat doesn't find in a reasonable budget.

z3 / Spacer in HORN logic treats every define-fun-rec as
uninterpreted and returns unknown; per user direction, indexed
reasoning is not targeted at z3.

Tests gated on pcsat opt in with
//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper.

Term simplifiers added to chc::Term

• tuple_proj(tuple(ts...), i) ↦ ts[i] — Spacer doesn't reduce
  datatype projections of literal constructors, so this is needed for
  e.g. Seq::empty().len() to reduce syntactically to 0.
• select(store(a, i, v), j) ↦ v / select(a, j) for concrete i,
  j integer literals — needed for Seq::singleton(x)[0] == x.
• select(seq_concat_arr_int(...), i) / select(seq_subseq_arr_int(...), i)
  ↦ ite(...) — described above (commit 4 only).

chc::Function::ITE and chc::Term::ite are introduced; Term::select
gains a V: Clone bound (the rewrites duplicate index / sn) which
cascades into Resolver::Output: Clone plus matching bounds on the
three Resolver impls — all concrete usages already satisfy Clone,
so this is a non-breaking strengthening.

Also fixes chc::Term::App emission to print bare f (not (f)) for
nullary functions, matching SMT-LIB conventions for declare-const.

Commit layout

1. Add Seq<T> ghost type — the type and Model impl, no operations.
2. Add basic operations — empty, singleton, len, push,
   indexing. Each lowers to existing CHC primitives. Consolidated
   seq_basic pass/fail pair plus an end-to-end seq_specs_vec_build
   program test.
3. Add concat / subsequence via define-fun-rec — adds the two
   recursive SMT definitions and the analyzer arms that lower the
   methods. Paired length-only tests (seq_concat, seq_subsequence)
   plus paired whole-Seq equality tests with a constant recursion bound
   (seq_concat_const, seq_subseq_const) that exercise pcsat's
   unfolding of the define-fun-rec definitions directly, without
   passing through any select peephole.
4. Peephole-rewrite indexed access — chc::Function::ITE,
   Term::ite, and the two select rewrites described above. Paired
   pass/fail unbounded indexed tests for both ops (seq_concat_index,
   seq_concat_index_right, seq_subseq_index) plus an end-to-end
   seq_specs_concat_run test exercising the rewrites through a real
   runtime function.

Phases that follow (separate PRs)

• Phase 2: snapshot!{} / proof_assert!{} macros
• Phase 3: trait #[predicate] propagation
• Phase 4: end-to-end port of map.rs / map_ext.rs

Test plan

• cargo build
• cargo fmt --all -- --check
• cargo clippy -- -D warnings
• cargo test --test ui (272 / 272 passing, including 20 new
  paired seq_* tests: seq_basic, seq_specs_vec_build,
  seq_concat, seq_subsequence, seq_concat_const,
  seq_subseq_const, seq_concat_index, seq_concat_index_right,
  seq_subseq_index, seq_specs_concat_run)

Generated with Claude Code.

https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX