Answer ports from the transcript and carry per-exchange guarantees #231

A key-exchange challenger answers Test and finalize from the visible transcript and forwards
every other query. Its state is the transcript, so it should be one generic converter with two
functions, not a hand-written converter. Proofs about the experiment then need contracts on single
exchanges (every reply of a session satisfies an invariant) that pass through attachment,
parallel composition, routers and sampling.

Add:

• TypedConverter.answerFromTranscript f : TypedConverter (B ⊗ L) B (answer the ports of L
  by f applied to the transcript so far, forward the rest), with AnswersFrom,
  answerFromTranscript_smul_ofProbAutomaton, the transcript law
  answerFromTranscript_smul_mass, answerFromTranscript_smul_congr and its off-condition form
  answerFromTranscript_smul_mass_eq_of_agree, and answerFromTranscript_smul_routingAt;
• TypedSystem.Guarantees X P (every possible exchange satisfies P) with mono, and,
  ofFunction, sample, sample_smul, parallel_left/right, parallel, parallel_inl/inr,
  parallelAll, ofProgram, ofDDC_ofProgramOn (an invariant kept by every completed
  invocation, any domain certificate), routingAt, routingAt_exchange, routingAt_reply,
  answerFromTranscript, rename, answerFromTranscript_smul_congr_of_guarantees, and
  parallel_parallelAll_ofDDC_ofProgramOn;
• the parallel transcript laws exists_left_of_parallel_ne_zero,
  exists_right_of_parallel_ne_zero, exists_component_of_parallelAll_ne_zero;
• the invariant lift TypedConverter.exists_invariant_of_ofProgram_smul_ne_zero (a state
  invariant of a bounded program holds along every positive transcript of ofProgram s P • R,
  any R).

A local version of every item exists (Typed/AnswerFromTranscript.lean, Typed/Guarantees.lean,
Typed/ParallelTranscripts.lean, Typed/ProbProgramAttachment.lean).

Not built: a transcript function that ignores the exchanges of one port is invariant under a
query or reply map at that port. A second game with an oracle translation would use it.

Acceptance:

• answerFromTranscript is stated for any outside and listed interfaces, with no game names.
• Guarantees through programs need no rely on the inside system.
• Test a first-reply answer against one that stops after a flag, and a guarantee through a
  family beside forwarded ports.
• Pass focused/full builds, standard linters and the axiom audit.

Depends on: #227, #228, #229.
Related: #222 (automaton invariants), #197 (selected-port histories), #110.