Cardano Updates

See plutus-private#2257.

The uplc-evaluator is a non-critical on-demand tool, so its integration
tests need not gate every PR. The test executable is still built on every
PR; the suite is run nightly instead. See plutus-private#2257.

Test teardown ran terminateProcess followed by an unbounded
waitForProcess, so a spawned service that missed SIGTERM hung the run
until the 2h CI cap (plutus-private#2257). Bound the wait and escalate to
SIGKILL, add a per-test tasty timeout as a safety net, and a regression
test that drives a SIGTERM-ignoring process.

Compose the force/delay chain with (.) instead of mixing ($) and parens,
and lay the mkInlinePurityTest argument out across lines. Same term.

In an Agda certificate, all work for type-checking the translation relation proofs is done in the top-level agda module. This PR instead constructs a module per pass which has the corresponding translation relation proof. This is useful for performance debugging when type-checking an agda certificate, as we can see a break-down of the decision procedure's performance.

So in addition to Pass_xyz/AST.agda, there is now also Passxyz/Proof.agda. The top-level module simply imports the proofs and constructs the certificate proof (a big tuple).

Replace raw UPLC constructors and the per-arity fresh-name plumbing in the Simplify, Inline, CaseOfCase and EvaluateBuiltins specs with the shared Transform.Lib helpers. Golden outputs are unchanged.

Shared UPLC term builders for the Transform.*.Spec modules: var "x" / lam "x" for occurrences and binders, name "x" for the bare Name, the ite helper, and the sopTrue/sopFalse vs builtinTrue/builtinFalse boolean constants. Variable identity is derived deterministically from the hint text; see Note [Names from textual hints].

Replace raw UPLC constructors and the per-arity fresh-name plumbing in the Simplify, Inline, CaseOfCase and EvaluateBuiltins specs with the shared Transform.Lib helpers and the var.x / lam.x / name.x dot syntax. Golden outputs are unchanged.

Shared UPLC term builders for the Transform.*.Spec modules: var.x and lam.x occurrence/binder handles via OverloadedRecordDot, name.x for bare names, the ite helper, and the sopTrue/sopFalse vs builtinTrue/builtinFalse boolean constants. Variable identity is derived deterministically from the hint text, so one hint denotes one variable.