handshake.rs `wrap_post_forall` should plumb the producer's actual return sort instead of hard-coding `Int`

[TSavo]

Surfaced by CodeRabbit Major on PR #1565 (review comment).

`provekit-verifier::handshake::wrap_post_forall` currently binds the carrier `result` as canonical `Int` regardless of the producer's actual return type. This is right for integer-returning functions (the demo) but ill-typed for `Bool`/`String`/etc. returns — the synthesized `forall result: Int. <post_body>` over a non-integer `result` is a type-mistake, and it changes Tier 1/Tier 2 implication-cache hashes.

Why it landed

• The previous code used `formalSorts[0]` (parameter sort, paired with `formals`) for the `result` binder — also wrong, just wrong in a different way (PARAMETER's sort, not RETURN's). PR Catalog starts empty, promotion torn out, the missing edge caught — on canonical Int #1565 replaced it with `Int` to address CodeRabbit's earlier Major and to match `build_implication_obligation`'s LIA default.
• Pre-existing limitation: the contract memento exposes `formals`/`formalSorts` but not a separate `returnSort` field. There's no clean way today to read the producer's actual return sort from the memento.

Fix shape

Per CodeRabbit's recommendation: plumb the producer's actual return sort from the memento (or fail closed when unavailable), instead of defaulting to `Int`. Two paths:

1. Extend the contract memento with `returnSort` — minted from `MintContractArgs.return_sort` (which already exists at mint time; see `provekit-cli/src/cmd_mint.rs` and `provekit-ir-types::WitnessMemento`-adjacent structs). Lifters that don't supply it would have `returnSort` absent; `wrap_post_forall` fails closed when absent. Heavy lift (touches the memento shape + every kit + the canonicalization).

2. Infer from the post body — if the post is `= (result, )`, the `result`'s sort can be inferred from ``'s top-level constructor / known-term-sort. Lighter; works for the common shape; fails closed otherwise.

Today's demo (rust-missing-edge / cmd_materialize_integration::materialize_write_emits_contract_bridge_that_verify_refuses_on_violation) all-integer, so `Int` is correct end-to-end. The bug only bites contracts whose producer's return type is non-integer.

Acceptance

• `wrap_post_forall` either binds `result` with the producer's actual return sort, or fails closed when the return sort is unavailable.
• A regression test: a Bool-returning producer's witness handshake synthesizes a well-typed `forall result: Bool. ...` (or refuses).

cc PR #1565, CodeRabbit comment thread on `handshake.rs:162-169`.