Skip to content

Strengthen fired-proof oracle in the #214/#225 unpacking properties (countFreeRef on a bound name is vacuous) #322

Description

@Unisay

Problem

The through-a-let unpacking suites for constructors (#214) and literal arrays (#225) each carry a property titled "eliminates the binding without growing the reference multiset", whose first assertion is meant to prove the rewrite fired:

optimized = optimizedExpression original
countFreeRef (Local (Name "v")) optimized === 0

But countFreeRef counts free references, and a reference to a name its enclosing Let still binds is not free — the traversal tracks bound names and skips them (see the Let case of countFreeRefs in Language.PureScript.Backend.IR.Types). So when the rule declines and leaves the binding in place, the count is 0 all the same: the assertion passes whether the rule fired or not. The property still checks the reference-multiset submap condition, but its "proof the rule fired" half is vacuous, so a regression that silently disables propagateKnownCtorThroughLet or propagateKnownArrayThroughLet on these shapes would not be caught here (it would surface only indirectly, via golden churn).

Approach

Replace the vacuous assertion with a shape oracle that distinguishes fired from declined. The record twin added for #240 does this with an allocation count — a recursive count of aggregate nodes (LiteralObject/ObjectUpdate there; Ctor and LiteralArray respectively here) asserted to be 0 after optimization:

countObjectAllocations optimized === 0

(countObjectAllocations in test/Language/PureScript/Backend/IR/Optimizer/Spec.hs, next to let1.) Generalize that helper over the node kinds it counts, or add per-kind siblings, and use it in both older properties. The multiset-submap half of each property stays as is.

Prerequisites / Relations

None — an independent test-quality fix. The shape-oracle pattern to copy (countObjectAllocations) landed with #240 (closed); the affected suites belong to #214 and #225 (both closed).

Verification

Temporarily disabling each propagate rule must turn its strengthened property red; with the rules active, both properties stay green across seeds.

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: irIR / optimizer / DCE / inlinerchoreMaintenance / infrastructure

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions