[Dijkstra] Replace `postulate trustMe-*` in Foreign with checked conversions

[williamdemeo]

Background

The Foreign layer (added for Dijkstra in #1134) uses postulate-based shortcuts at three sites where Haskell-side values must be promoted to Agda-side values that carry proof obligations.

1. ppWF in src/Ledger/Dijkstra/Foreign/ExternalStructures.lagda.md (already marked FIXME) — postulates well-formedness of applyPParamsUpdate.
2. trustMe-flowConservation, trustMe-nonneg, trustMe-nonpos in src/Ledger/Dijkstra/Foreign/Rewards.lagda.md — postulate the three invariants of RewardUpdate when reconstructing it from a HsRewardUpdate.

The latter two are jointly inconsistent if ever instantiated on the same ℤ value, though current call sites avoid this.

Goal

Replace each postulate with one of the following:

• a decision procedure that runs at the Haskell-Agda boundary and produces failure if the invariant is violated (preferred for fields the Haskell side can construct freely);
• a genuine proof, where the structure of the construction makes one available.

The pattern in Foreign/Chain.lagda.md (decidable check on bBodySize ≡ hBbsize, returning error on mismatch) is a good template.

Acceptance

• No postulate blocks in Ledger/Dijkstra/Foreign/*.lagda.md outside of clearly-scoped TODOs with a tracking issue link.
• trustMe-nonneg and trustMe-nonpos deleted (replaced by decidable bounds checks in Conv-RewardUpdate.from).

[williamdemeo]

This is not an issue that needs to be fixed. Closing.