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) and wires the following operations,
each with paired pass/fail UI tests:

Op	Lowering
s.len()	tuple_proj(s, 1)
s.push(e)	tuple([store(s.0, s.1, e), s.1 + 1])
s[i]	select(s.0, i) — detected via #[thrust::def::seq_model] marker
Seq::<T>::empty()	tuple([seq_default_arr_int, 0])
Seq::singleton(x)	tuple([store(seq_default_arr_int, 0, x), 1])
s.concat(t)	tuple([seq_concat_arr_int(s.0, s.1, t.0), s.1 + t.1])
s.subsequence(l, r)	tuple([seq_subseq_arr_int(s.0, l), r - l])

Solver-side details

seq_default_arr_int is declared once in the SMT preamble; the array
contents are irrelevant because indices ≥ length are never accessed.

seq_concat_arr_int(a, la, b) / seq_subseq_arr_int(a, l) are
peephole markers: the select simplifier rewrites
select(seq_concat_arr_int(a, la, b), i) → element-getter
seq_concat_get_int(a, la, b, i) (and similarly for subseq) before
the term reaches the SMT solver. The getters are emitted via SMT-LIB2
(define-fun-rec ...) whenever used, on demand (gated by
System::uses_seq_concat / uses_seq_subseq).

• Length reasoning on concat / subsequence works under either
  solver, because the length is computed inline by the analyzer
  (a.len + b.len, r - l).
• Indexed reasoning (e.g. s.concat(t)[i] == s[i] when
  i < s.len()) works under pcsat — opt in with
  //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper. z3 / Spacer
  in HORN logic returns unknown for define-fun-rec over arrays,
  which is a known solver limitation.

The marker symbols themselves are never declared and should not reach
the SMT output; if they do (e.g. through a whole-array equality), the
SMT solver reports an undeclared symbol. The reference iterator
examples never compare array slots directly, so this is not expected to
block the eventual port.

Term simplifiers added to chc::Term

Two small peephole rules keep the encoding inside what HORN solvers
reliably reduce:

• 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.

Plus the marker-consuming select(seq_*_arr_int(...), i) rewrites
described above.

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

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 (270 / 270 passing, including 12 new paired
  seq_* tests: seq_len_push, seq_index, seq_empty,
  seq_singleton, seq_concat, seq_subsequence,
  seq_concat_index, seq_concat_index_right, seq_subseq_index)

🤖 Generated with Claude Code

https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX