feat(symbolic): Seq, powerset, choose, keys/values, strings, compound dicts

[danwt]

Summary

• Seq[T] encoding: ExplodedSeq VarKind with [len, elem_0..elem_n] Z3 layout, --seq-bound CLI flag, head/tail/concat/slice/index operations, init and effect encoding
• Dict[Range, Seq[T]]: stride-based compound encoding with symbolic key support via ITE chains, compound locals for function inlining, If-then-else in dict merge updates
• Powerset quantification: bitmask enumeration over all 2^n subsets with set-local tracking
• Choose expression: ITE chain over domain with predicate
• Keys/Values: membership and length encoding for dict variables
• String gaps: Value::String in constants, Type::String action parameters and trace extraction
• Clear error messages: specific messages for Tuple, Record, Option, Powerset-as-value, BigUnion, Fix, temporal operators, action calls

Specs now passing symbolic checking

Counter, SeqTest, Transfer, DieHard, DiningPhilosophers, ProcessStates, DistributedCounter, TrafficLight, Bunny1, Bunny2, BankingRecords, SimpleQueue, RaftMongo, TCommit_Simple, EWD840, ChainReplication, ChandyLamport, MESI

Known remaining limitations (clear error messages)

• Nested dicts (Dict[Int, Dict[Int, Bool]]) — Paxos, Comet, PBFT
• Set as container value — Redlock
• Set-typed action parameters

Test plan

• cargo test --workspace --exclude specl-tla — all 125 tests pass
• cargo fmt --check clean, zero warnings on specl-symbolic
• Regression: Counter, SeqTest, SimpleQueue, RaftMongo, ChainReplication, EWD840, TCommit_Simple
• New: ChandyLamport (Dict[Int, Seq[Int]] with if-then-else), Bunny1/2, BankingRecords, MESI, DiningPhilosophers
• Powerset: custom voting specs with majority quorum patterns

🤖 Generated with Claude Code