Skip to content

fix(prune): preserve case target when pruning case -> assert#352

Open
tvolk131 wants to merge 1 commit intoBlockstreamResearch:masterfrom
tvolk131:codex/preserve-case-target-pruning
Open

fix(prune): preserve case target when pruning case -> assert#352
tvolk131 wants to merge 1 commit intoBlockstreamResearch:masterfrom
tvolk131:codex/preserve-case-target-pruning

Conversation

@tvolk131
Copy link

@tvolk131 tvolk131 commented Mar 7, 2026

This fixes a pruning bug in RedeemNode::prune_with_tracker() that can corrupt nested sum-shaped witnesses when a case is pruned into assertl/assertr.

The issue was that after pruning a case into an assert, the temporary Construct DAG was retyped from the pruned structure alone. That drops the original case target constraint, which can let free target vars on the surviving branch collapse to 1. When final witness pruning runs, a live nested sum payload can then be incorrectly shrunk to unit.

The fix preserves the original case target when a pruned case is rebuilt as assertl/assertr, so witness shrinking continues to use the correct surviving type.

Tests

Adds a focused regression test that builds the failing shape directly with ConstructNode:

  • unpruned execution succeeds
  • pruning rewrites the case to assertl
  • the pruned witness keeps the nested sum payload instead of collapsing to unit
  • pruned execution matches unpruned execution

The regression reproduces the old witness-shrinking failure if this fix is reverted.

Copilot AI review requested due to automatic review settings March 7, 2026 02:19
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Fixes a pruning/type-inference edge case in RedeemNode::prune_with_tracker() where pruning a case into assertl/assertr could drop the original case target constraint, leading to incorrect witness shrinking for nested sum-shaped values.

Changes:

  • Preserve the original case target type constraint when a pruned case is rebuilt as assertl/assertr during the temporary ConstructData rebuild.
  • Add a focused regression test that constructs the failing shape directly with ConstructNode and verifies pruning rewrites + witness preservation + execution equivalence.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants