Add EliminateReturnStatements and ContractPass with functional $post

[keyboardDrummer-bot]

Summary

Copies two passes from PR #28 with modifications to the contract pass as requested:

EliminateReturnStatements (copied as-is)

Rewrites return statements to exit statements by wrapping procedure bodies in a labelled block. This ensures code placed after the body (e.g., postcondition assertions) is always reached.

ContractPass (modified)

Translates away pre and postconditions entirely by introducing assertions and assumptions at call sites and at procedure starts and ends.

Key differences from PR #28's contract pass:

1. $post procedures are marked as functional (isFunctional := true) — they are pure functions.

2. $post procedures take all inputs AND all outputs as parameters — so they don't need to call the original procedure in their body. For a procedure foo(a, b) returns (x, y) with postcondition P(a, b, x, y), generates:

   function foo$post(a, b, x, y) returns ($result : bool) {
     P(a, b, x, y)
   }
   

3. At call sites, input arguments are assigned to temporary variables first, then those temps are passed to both the call and the assumed $post:

   var $foo$arg0 := a;
   var $foo$arg1 := b;
   assert foo$pre($foo$arg0, $foo$arg1);
   var x, y := foo($foo$arg0, $foo$arg1);
   assume foo$post($foo$arg0, $foo$arg1, x, y);
   

   This ensures the postcondition assumption references the pre-call argument values even if the call modifies mutable variables.

[keyboardDrummer-bot]

The "Run internal benchmarks of Strata" CI failure is not caused by the code changes in this PR. I verified:

1. The project builds successfully locally (lake build — 579 jobs, all pass).
2. lake test passes (the only failure is an unrelated missing jar file for Java codegen tests).
3. lake lint passes (all 301 modules correctly imported).

The benchmark failure is a pre-existing infrastructure issue affecting all PRs in this fork. I confirmed that PRs #33, #34, and #36 (including completely unrelated changes) all have the same benchmark failure while all other checks pass. The CI workflow's strata-benchmarks job uses --source-location-override https://github.com/strata-org/Strata.git with the PR's head SHA, but since these commits only exist in keyboardDrummer/Strata, CodeBuild cannot find them.

No code fix is needed for this PR — the benchmark job configuration would need to be updated to reference the correct repository for fork PRs.