test: property tests for staging stability and strictness

[iljakuklic]

Background

The staging literature specifies two testable correctness properties of the staging pass, neither of which the snapshot suite covers explicitly:

• Stability: staging is the identity on splice-free code — unstaging a program whose code defs contain no splices (and no meta references) must reproduce it verbatim.
• Strictness: staging performs no object-level computation — object redexes present in the input (lets, matches on literals, primitive applications in object code) must survive to the output unchanged.

The current implementation appears to satisfy both (eval_obj is structural), but nothing pins that down: a future "optimization" that constant-folds or inlines during eval_obj would silently violate strictness — and destroy user control over generated code size — without failing any test.

Proposal

• Unit/integration tests: stage splice-free programs and assert output ≡ input (alpha-equality); stage programs with deliberate object redexes (let x = 1; x, match 0 { ... }, 1 + 1 in object code) and assert the redexes are preserved.
• Optionally a bolero fuzz target: generate splice-free object programs, assert unstage(p) == p (stability is a cheap universally-quantified oracle).

Constant folding / simplification, if ever wanted, belongs in a separate explicit pass after staging, not in the staging evaluator.