Agent boundary: support real multi-turn conversations without collapsing prompts

[AminChirazi]

Readiness gap

Flowproof currently supports one user turn, not a conversation. Every prompt: step is joined into one task delivered up front, as documented in README.md and docs/agent-testing.md.

That is sufficient for single-task agents, but it cannot represent the production flows most likely to exercise approval and safety controls:

• the agent asks a clarifying question and the user answers;
• the agent proposes a destructive action and waits for approval;
• a user changes intent after seeing an intermediate result;
• a denial or tool error is followed by recovery;
• a later turn attempts to exploit context accumulated earlier.

CHARTER.md already authorises this as Milestone 3. This issue gives that milestone an implementation target.

Constraint

Multi-turn must preserve the existing invariants:

• replay makes zero LLM calls and needs no provider key;
• a cassette remains ground truth;
• recorded turn boundaries are replayed, not re-decided;
• healing proposes a diff and never silently changes the recording;
• secrets do not enter the trace.

This is a driver-contract change, not only a new grammar form.

Acceptance criteria

• Approve and document an explicit spec shape for alternating user turns.
• Deliver each user turn only after the preceding agent trajectory reaches its recorded boundary; do not concatenate prompts.
• Preserve user, assistant, tool-call and tool-result turn boundaries in the cassette and trace schema.
• Define whether assertions are conversation-wide, turn-local, or both, with unambiguous syntax.
• Record and replay multi-turn flows for OpenAI-compatible and Anthropic dialects.
• Cover buffered and streaming responses, and both agent.command and agent.url.
• Prove replay makes zero upstream model calls across the entire conversation.
• Keep every existing single-turn flow byte-compatible or provide an explicit trace migration.
• Update docs/agent-testing.md, docs/trace-format.md, the JSON Schema and runnable examples in the same change.
• Add red-path tests for a changed later user turn, a missing turn, an extra turn and a tool-call divergence after turn one.