PVerifier: handle choose in expression contexts to avoid internal codegen crash

[Copilot]

p compile --mode pverifier could throw an internal error when choose(...) appeared inside a larger expression (notably tuple construction in the Two-Phase Commit tutorial client). The backend only handled ChooseExpr in a narrow assignment shape, so nested usage reached the unsupported-expression fallback.

• PVerifier expression coverage

  • Added explicit ChooseExpr handling in ExprToString(...):
    • choose() lowers to nondet *
    • choose(x) lowers to generated chooser call via ChooseExprHelper(...)
  • This closes the unsupported nested-expression path (e.g., tuple field initializers).

• Chooser declaration model update

  • Replaced chooser emission from procedure ... returns ... ensures ... to function ... + axiom forall ... constraints for int, set, and map domains.
  • Aligns chooser usage with expression-level codegen (chooser now composes naturally inside expressions).

• Assignment path alignment

  • Updated AssignStmt { Value: ChooseExpr } emission to expression assignment form, with explicit handling for choose().

• Regression coverage

  • Added a focused unit test (PVerifierChooseExprTests) that exercises a named tuple containing nested choose(...) and asserts correct rendering behavior.

// Before: could hit Not supported expr (ChooseExpr) when nested in tuple expressions
ChooseExpr { SubExpr: null } => "*",
ChooseExpr cexpr => ChooseExprHelper(cexpr),