Verify 2-case select

[lredlin]

This PR adds specifications and proofs for BlockingSelect2 and NonBlockingSelect2, which handle selection over two channels.

Changes

• Added wp_BlockingSelect2: Specification for blocking select over two channels
• Added wp_NonBlockingSelect2: Specification for non-blocking select over two channels

Both specs support mixed send/receive operations on each channel, determined by the direction parameters.
Notes on proof size
The proofs are quite large (~500 lines each) because the primary goal was to validate the specification structure rather than optimize the proof strategy. As a result:

1. Much of the proof is brute-forced through all possible cases
2. There's significant repetition across similar branches
3. Little abstraction or tactical refinement was applied

I think for anything larger we can either replace the Select functions with a gooselang wrapper that uses a list fold or use a proof strategy that isn't brute forced so it doesn't blow up by the number of permutations

[tchajed]

This looks good to me. Simplifying the proofs might be easier done by also tweaking the code, and we can do that separately.

CI seems to only be failing because you linked goose-lang/goose#144 but this PR doesn't have translations for those examples. Can you remove that from the description if it isn't part of this?