user3347: I am trying to spend from a branched Simplicity program, but I don't wanna supply the signatures in the untaken branch, so I am trying to prune the program by hand. I have verified that I can take the commitmentRoot of a checkSig with the signature set to undefined.
To make a valid spend, I think I need to construct a pruned program that has the same CommitmentRoot that the full program has. So I boiled by program down to a single case expression:
u :: CommitmentRoot () ()
u = unit

full :: CommitmentRoot (Bit, ()) ()
full = cond u unit

pruned :: CommitmentRoot (Bit, ()) ()
pruned = assertr (commitmentRoot u) unit

But the CommitmentRoots do not have the same hash:
*Main> (encode.fromShort.hash256.commitmentRoot) pruned
"7b4082aaae5e289f29855ede047b2b6598805b153324aa3a5fd4fec5b1a86053"
*Main> (encode.fromShort.hash256.commitmentRoot) full
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"

What gives? Is my understanding that I need a matching CommitmentRoot incorrect? If it is not correct, how do I prune a case expression correctly?
Furthermore, section "4.3.2.1 Pruning Unused case Branches" of the Simplicity Technical Report claims that "We can effectively replace any unused branch in a case expression with its commitment Merkle root." But if I do that, I cannot run the Simplicity program with runKleisli. So how is this supposed to work?

user49364: The definition of cond is
cond thn els = match (drop els) (drop thn)

Expanding this in your definition of full yields
full = match (drop unit) (drop u)

The correct pruned version should be
pruned = assertl (drop unit) (commitmentRoot (drop u))

which has commitment root that matches:
let full = cond unit unit in (flip Numeric.showHex "".integerHash256.commitmentRoot) (full :: CommitmentRoot (Bit, ()) ())
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"

let pruned = assertl (Simplicity.Term.Core.drop unit) (commitmentRoot (Simplicity.Term.Core.drop unit :: CommitmentRoot ((),()) ())) in (flip Numeric.showHex "".integerHash256.commitmentRoot) (pruned :: CommitmentRoot (Bit, ()) ())
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"

Better library support for pruning expressions is something that will be developed.

3347: <p>I am trying to spend from a branched Simplicity program, but I don't wanna supply the signatures in the untaken branch, so I am trying to prune the program by hand. I have verified that I can take the <code>commitmentRoot</code> of a checkSig with the signature set to <code>undefined</code>.</p>

<p>To make a valid spend, I think I need to construct a pruned program that has the same <code>CommitmentRoot</code> that the full program has. So I boiled by program down to a single case expression:</p>

<pre><code>u :: CommitmentRoot () ()
u = unit

full :: CommitmentRoot (Bit, ()) ()
full = cond u unit

pruned :: CommitmentRoot (Bit, ()) ()
pruned = assertr (commitmentRoot u) unit
</code></pre>

<p>But the <code>CommitmentRoot</code>s do not have the same hash:</p>

<pre><code>*Main&gt; (encode.fromShort.hash256.commitmentRoot) pruned
"7b4082aaae5e289f29855ede047b2b6598805b153324aa3a5fd4fec5b1a86053"
*Main&gt; (encode.fromShort.hash256.commitmentRoot) full
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"
</code></pre>

<p>What gives? Is my understanding that I need a matching <code>CommitmentRoot</code> incorrect? If it is not correct, how do I prune a case expression correctly?</p>

<p>Furthermore, section "4.3.2.1 Pruning Unused case Branches" of the Simplicity Technical Report claims that "We can effectively replace any unused branch in a case expression with its commitment Merkle root." But if I do that, I cannot run the Simplicity program with <code>runKleisli</code>. So how is this supposed to work?</p>
 49364: <p>The definition of <code>cond</code> is</p>

<pre><code>cond thn els = match (drop els) (drop thn)
</code></pre>

<p>Expanding this in your definition of <code>full</code> yields</p>

<pre><code>full = match (drop unit) (drop u)
</code></pre>

<p>The correct pruned version should be</p>

<pre><code>pruned = assertl (drop unit) (commitmentRoot (drop u))
</code></pre>

<p>which has commitment root that matches:</p>

<pre><code>let full = cond unit unit in (flip Numeric.showHex "".integerHash256.commitmentRoot) (full :: CommitmentRoot (Bit, ()) ())
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"

let pruned = assertl (Simplicity.Term.Core.drop unit) (commitmentRoot (Simplicity.Term.Core.drop unit :: CommitmentRoot ((),()) ())) in (flip Numeric.showHex "".integerHash256.commitmentRoot) (pruned :: CommitmentRoot (Bit, ()) ())
"dded2b0938bb9f58f20324ab1f699e7006ffd8e9251b3ddd0f551de1d66fe119"
</code></pre>

<p>Better library support for pruning expressions is something that will be developed.</p>
