refactor: add stack comments to claim_batch_pipe_double_words

[partylikeits1983]

This PR adds stack comments to claim_batch_pipe_double_words, and was an opportunity to research if the call to mem::pipe_double_words_preimage_to_memory for PROOF_DATA_KEY is necessary in the claim_batch_pipe_double_words procedure.

The purpose of this PR is to close #2237 specifically point 5:

5. Refactor & clean up batch_pipe_double_words context: Add Agglayer CLAIM note & bridging in functionality #2188 (comment). Refactor & clean up batch_pipe_double_words context: Add Agglayer CLAIM note & bridging in functionality #2188 (comment)

@bobbinth left a comment here regarding the old state of the claim_batch_pipe_double_words procedure. In the comment, it is pointed out that it is not necessary to call exec.mem::pipe_double_words_preimage_to_memory for the PROOF_DATA_KEY, which is technically true.

This is the current state of the claim_batch_pipe_double_words procedure:

# Inputs: [PROOF_DATA_KEY, LEAF_DATA_KEY]
# Outputs: []
proc claim_batch_pipe_double_words
    # 1) Verify PROOF_DATA_KEY
    mem_storew_be.CLAIM_PROOF_DATA_KEY_MEM_ADDR
    adv.push_mapval
    # => [PROOF_DATA_KEY]

    push.CLAIM_PROOF_DATA_START_PTR push.CLAIM_PROOF_DATA_WORD_LEN
    exec.mem::pipe_double_words_preimage_to_memory drop
    # => []

    # 2) Verify LEAF_DATA_KEY
    mem_storew_be.CLAIM_LEAF_DATA_KEY_MEM_ADDR
    adv.push_mapval
    # => [LEAF_DATA_KEY]

    push.CLAIM_LEAF_DATA_START_PTR push.CLAIM_LEAF_DATA_WORD_LEN
    exec.mem::pipe_double_words_preimage_to_memory drop
    # => []
end

It is possible to remove the call to mem::pipe_double_words_preimage_to_memory for the PROOF_DATA_KEY, however, I think we should keep this call.

Why? Because the bridge should not have to trust that the CLAIM note (or the note calling the claim procedure), correctly inserted PROOF_DATA under PROOF_DATA_KEY in the AdviceMap. This call to mem::pipe_double_words_preimage_to_memory is in effect a sanity check. If we removed it, it's unlikely to open a possible vulnerability, however, I think we should keep it, unless there is a strong reason to remove it. Removing it would save around ~257 cycles.

Essentially this call to mem::pipe_double_words_preimage_to_memory makes it so that the bridge_in component does not have to trust that the note which called the claim procedure correctly inserted PROOF_DATA under PROOF_DATA_KEY in the AdviceMap.

---

Closes #2237

[mmagician]

We should not remove the current invocation of claim_batch_pipe_double_words, but leaf data is piped to memory twice now:

1. claim -> claim_batch_pipe_double_words (piped via pipe_double_words_preimage_to_memory)
2. claim -> verify_leaf_bridge -> get_leaf_value -> (piped via pipe_preimage_to_memory)

Since both happen within the AggLayerBridge account context, the latter is not necessary

[bobbinth]

Seems like changes from this PR are already in the agglayer branch?

[partylikeits1983]

We should not remove the current invocation of claim_batch_pipe_double_words, but leaf data is piped to memory twice now:
claim -> claim_batch_pipe_double_words (piped via pipe_double_words_preimage_to_memory)
claim -> verify_leaf_bridge -> get_leaf_value -> (piped via pipe_preimage_to_memory)
Since both happen within the AggLayerBridge account context, the latter is not necessary

Good catch. I did a really deep dive into this and here's what's going on:

Why leaf data is piped twice

The leaf data pipe in get_leaf_value (to addr 0) exists because pack_leaf_data in leaf_utils::compute_leaf_value is destructive: it shifts all elements left by 3 bytes in-place to match Solidity's abi.encodePacked. After packing, the original field layout at that address is destroyed.

The data at addr 536 (from claim_batch_pipe_double_words) is the "golden copy" that load_origin_token_address, load_destination_address, and load_raw_claim_amount all read from after verification. If pack_leaf_data ran on addr 536, those subsequent reads would return garbage.

So the second pipe to addr 0 is effectively a memcpy, it creates a sacrificial copy that pack_leaf_data can safely destroy. MASM has no native memcpy, so the advice map pipe serves as the copy mechanism.

Proof data is also piped twice

Note that it's not just leaf data, proof data is also piped to memory twice:

1. claim_batch_pipe_double_words pipes proof data to addr 0 via pipe_double_words_preimage_to_memory
2. verify_leaf pipes the same proof data to addr 0 via pipe_preimage_to_memory

The first pipe serves as the integrity/sanity check. The second pipe in verify_leaf overwrites the same address with the same data.

Can we remove the double pipe?

Yes, the double pipe of leaf data can be removed. I prototyped the change and all tests pass, however, there are some trade offs. The approach:

1. Add a new internal procedure copy_leaf_data_and_compute_value that manually copies 32 felts from addr 536 → addr 0 using 8 mem_loadw_le/mem_storew_le pairs, then calls compute_leaf_value:

proc copy_leaf_data_and_compute_value
    padw mem_loadw_le.536 mem_storew_le.0 dropw
    padw mem_loadw_le.540 mem_storew_le.4 dropw
    padw mem_loadw_le.544 mem_storew_le.8 dropw
    padw mem_loadw_le.548 mem_storew_le.12 dropw
    padw mem_loadw_le.552 mem_storew_le.16 dropw
    padw mem_loadw_le.556 mem_storew_le.20 dropw
    padw mem_loadw_le.560 mem_storew_le.24 dropw
    padw mem_loadw_le.564 mem_storew_le.28 dropw

    push.LEAF_DATA_START_PTR
    exec.leaf_utils::compute_leaf_value
end

2. Modify verify_leaf_bridge to drop LEAF_DATA_KEY and call the new proc instead of get_leaf_value.

Alternatively, we could refactor leaf_utils::pack_leaf_data to take separate source and destination pointers (read from src, write to dest) so it doesn't destroy the source data. That would eliminate the need for the copy entirely — compute_leaf_value could read directly from addr 536 and write packed output to addr 0. However, pack_leaf_data is also used by bridge_out.masm, so changing its signature is a deeper refactor that touches multiple callers.

Why I think we should keep the code as is

The double pipe costs extra cycles, but it keeps the code clearer. The current verify_leaf_bridge has a clean API, it takes [LEAF_DATA_KEY, PROOF_DATA_KEY] on the stack and uses the advice map to load both datasets independently. This matches the original bridge-in flow design where each procedure is self-contained.

Removing the double pipe would require changing the expected API of verify_leaf_bridge, it would rely on the fact that leaf data is already in memory at addr 536. This makes the procedure less self-documenting and couples it more tightly to the caller's memory layout.

This is a valid optimization but the tradeoff is reduced clarity for ~cycle savings.

What do you think @mmagician @bobbinth ?

[mmagician]

Thanks for the investigation.

---

Alternatively, we could refactor leaf_utils::pack_leaf_data to take separate source and destination pointers

I agree this would be the cleanest approach to not overwrite memory but instead write to a different pointer location.

---

[proof data] The first pipe serves as the integrity/sanity check. The second pipe in verify_leaf overwrites the same address with the same data.

So we can remove one of the writes of proof data - it sounds like that one is clear?
If so, then for now I would:

• remove the redundant write of proof data
• add clear comments describing the overwriting of leaf data in memory
• create an issue to address the separation of read&write pointers as a follow-up (though I'd still like to tackle it this week before handing off the code)

[bobbinth]

I agree this would be the cleanest approach to not overwrite memory but instead write to a different pointer location.

I think we may even be able to use the local memory of compute_leaf_value for this.

Also (and not for this PR), I think we may be able to simplify the pack_leaf_data procedure by using field multiplications. For example, if we have a felt of the form [0, 0, 0, 0, byte0, byte1, byte2, byte3] and we want to get [0, 0, 0, 0, byte0, byte1, byte2] out of it, we could do this like:

mul.2^24 u32split drop

This is because multiplying this value by $2^{24}$ would result in [0, byte0, byte1, byte2, byte3, 0, 0, 0] and then u32split would give us the upper and lower limbs of this felt.