Milestone 3: HTLC and Commitment Operations Implementation Plan

[NishantBansal2003]

Objective

After the funding flow, we need a scenario for fuzzing normal channel operations. So the main objective of this plan is that we can complete the commitment dance fully, and the design should be extensible enough to support future extensions. That way, once we have more advanced mutators, cases like multiple HTLC adds or many commitment dance operations can happen correctly, helping test deeper code paths and edge cases.

Smite APIs

BOLT messages

• update_fulfill_htlc
• update_fail_htlc
• update_fail_malformed_htlc
• update_add_htlc
• commitment_signed
• revoke_and_ack
• update_fee

Commitment sign/verify APIs

Currently, smite only supports the initial funding flow, so we need to extend it with HTLC support. The main changes are:

• Add Htlc struct and in-flight HTLC tracking to CommitmentState.
• Extend channel/holder config with HTLC basepoints and signing keys.
• Extend commitment signing/verification to include HTLC second-stage signatures.
• Introduce a PendingUpdate enum covering the commitment-affecting updates (AddHtlc(Htlc), FulfillHtlc(id), FailHtlc(id), UpdateFee(feerate_per_kw)).
• Update commitment advancement (CommitmentState::advance(updates)) and fee accounting to handle HTLC outputs.

Variables and VariableType

VariableType	Payload
HtlcId	u64
PaymentHash	[u8; 32]
OnionRoutingPacket	[u8; 1366]
Htlc	smite::channel_tx::Htlc
RevokeAndAck	smite::bolt::RevokeAndAck

Operations

• CreateHtlc: We need this operation so that we can tie the same HTLC to BuildUpdateAddHtlc and AdvanceCommitmentStateAddHtlc. Otherwise, there is a chance that we send one HTLC but use a different HTLC in the commitment state, which would only result in invalid signatures. So, if we want to test that mismatch case, we can omit this operation, otherwise, it makes sense to keep it.

  • Input types: HtlcId, Amount,PaymentHash, BlockHeight
  • Output type: Htlc

• BuildUpdateAddHtlc:

  • Input types: ChannelId, Htlc, OnionRoutingPacket
  • Output type: Message

• AdvanceCommitmentState{Kind}: One op per update kind, each producing the next CommitmentState from the previous one plus the kind-specific payload. This can be implemented in two ways. One approach is the commitment chaining approach (currently used), where each new commitment state is derived from the previous one. This ensures the commitment number and balances on both sides remain correct, and also allows exercising cases with multiple commitments once more interesting mutators are added. The tradeoff is that both SpliceMutator and GeneratorInsertionMutator must update the commitment state indices if instructions are inserted in between, otherwise, these mutators become ineffective for this flow. Another approach is to build the next commitment state directly from raw inputs. However, this has a major caveat around balance handling: if the balances are not correct, the commitment dance will not complete successfully.

  • AdvanceCommitmentStateAddHtlc
    • Input types: CommitmentState, Htlc, Point, Point (local and remote per-commitment points)
    • Output type: CommitmentState
  • AdvanceCommitmentStateFailHtlc
    • Input types: CommitmentState, HtlcId, Point, Point
    • Output type: CommitmentState
  • AdvanceCommitmentStateFulfillHtlc
    • Input types: CommitmentState, HtlcId, Point, Point
    • Output type: CommitmentState
  • AdvanceCommitmentStateUpdateFee
    • Input types: CommitmentState, FeeratePerKw, Point, Point
    • Output type: CommitmentState

• BuildCommitmentSigned:

  • Input types: ChannelId, ChannelConfig, CommitmentState, HolderIdentity
  • Output type: Message

• RecvRevokeAndAck: We can also verify here that the received PerCommitmentSecret actually derives the peer's per_commitment_point stored in the old CommitmentState. For that, we would either need to carry old CommitmentState as an input or simply pass the expected Point directly for verification.

  • Input types: None
  • Output type: RevokeAndAck

• ExtractRevokeAndAck:

  • Input types: RevokeAndAck
  • Output type: RevokeAndAckField { PerCommitmentSecret: PrivateKey, NextPerCommitmentPoint: Point}

• RecvCommitmentSigned: Here, we can simply verify the signature and avoid extracting any fields. In the future, if we add cases like force-close fuzzing, we can instead output CommitmentSigned and introduce a separate operation to extract its fields.

  • Input types: ChannelConfig, CommitmentState, HolderIdentity
  • Output type: None

• BuildRevokeAndAck:

  • Input types: ChannelId, PrivateKey, Point
  • Output type: Message

• RecvUpdateFailMalformedHtlc: Until we send a valid OnionRoutingPacket or HtlcId, we are mostly going to get this. Here, we do not care about any other received message fields anyway, because we already know we sent something invalid. So we simply accept the failure and extract the HtlcId in order to remove it from the commitment state.

  • Input types: None
  • Output type: HtlcId

• RecvUpdateFailHtlc: Mostly same as RecvUpdateFailMalformedHtlc

  • Input types: None
  • Output type: HtlcId

• RecvUpdateFulfillHtlc: Though we are not going to get this right now, maybe we could defer it until we add support for valid OnionRoutingPackets? Also, right now we ignore the received payment_preimage, but we could add support for it later. We can retrieve the HTLC from the commitment state and verify the preimage against its payment hash, or perhaps simply query the output of CreateHtlc.

  • Input types: None
  • Output type: HtlcId

• BuildUpdateFee:

  • Input types: ChannelId, FeeratePerKw
  • Output type: Message

Builder

generate_fresh arms for HtlcId, PaymentHash, and OnionRoutingPacket, the other variable types should be generated from composed inputs.

Note that for the MVP we send arbitrary OnionRoutingPackets, but later we will need to add support for constructing valid onions as well, and only mutate them through mutators for invalid cases.

Generators

Currently, until we have SpliceMutator or GeneratorInsertionMutator, we cannot realistically have many standalone generators for things like UpdateAddHtlcGenerator, CommitmentSignedGenerator, or UpdateFeeGenerator. So until then, we likely need a single generator such as CommitmentDanceGenerator that exercises the full commitment dance end-to-end, either with update_add_htlc or perhaps with update_fee as well.

Mutators

• OperationParamMutator: Most of the operations defined above are built from composed inputs, so they will not be op-param mutable.

• SpliceMutator and GeneratorInsertionMutator: Now, the current design of CommitmentState is such that we need a previous commitment state in order to create a valid commitment signature. For mutators like these, if another set of valid instructions is inserted at some point, then the commitment state references in the instructions need to be updated accordingly so that the current commitment state always references the closest previous commitment state. Otherwise, these mutators will become ineffective for normal channel operations. The same applies to BuildCommitmentSigned as well. In short, whichever operations take CommitmentState as an input need to be updated to reference the latest commitment state known to them.

Note: We also need to think about how to ensure that the commitment number is updated only once during an entire commitment dance, especially if a generator is inserted before the commitment dance. The same concern applies within a single dance when multiple updates are batched together, since each AdvanceCommitmentState{Kind} currently bumps the number.

• InstructionDeleteMutator: Currently, I have not wired the commitment dance for this yet, but this also needs to be handled, otherwise, deleting certain operations may cause timeouts. I think this can be updated accordingly once we standardize the approach and properly integrate these mutators.

SnapshotSetup

Add PostChannelOpenSetup alongside PostInitSetup. It drives the full funding flow procedurally and snapshots with a channel already open, so CommitmentDanceGenerator can exercise the HTLC adds, commitment dance, update fees. State is written into ProgramContext. For this I have 2 ideas on which we can discuss which one to proceed forward with:

• One approach is to add the channel open state through ProgramContext, where we store discrete values and load them via Load*FromContext operations. In that case, the ProgramContext would look like:

struct ProgramContext {
	...

  channel_id: Option<ChannelId>,
  feerate_per_kw: Option<u32>,
  channel_type: Option<Vec<u8>>,
  funding_satoshis: Option<u64>,
  local_config: Option<ChannelPartyConfig>,
  remote_config: Option<ChannelPartyConfig>,
  initial_per_commitment_privkey: Option<PrivateKey>, // open_channel <-> accept_channel
  next_per_commitment_privkey: Option<PrivateKey>, // channel_ready <-> channel_ready
  local_funding_privkey: Option<Secret>,
  local_htlc_basepoint_privkey: Option<Secret>,
  // from open_channel <-> accept_channel
  local_initial_per_commitment_point: Option<PublicKey>, // #0
  remote_initial_per_commitment_point: Option<PublicKey>, // #0
  // from channel_ready <-> channel_ready
  local_next_per_commitment_point: Option<PublicKey>, // #1
  remote_next_per_commitment_point: Option<PublicKey>, // #1
  funding_outpoint: Option<OutPoint>,
}

Then, ChannelConfig, CommitmentState, HolderIdentity can be constructed from those loaded inputs. The main benefit of this approach is that, since the program loads discrete values directly, mutators can modify individual fields before constructing ChannelConfig, CommitmentState, HolderIdentity. However, I think mutating most of these fields would mainly just result in invalid signatures being sent to the peer, so I am not sure this approach provides much additional value beyond exercising incorrect-signature cases. Because of that, I am thinking about another approach instead.

• Another approach is to directly export ChannelConfig, CommitmentState and HolderIdentity through ProgramContext, and load them in the executor using LoadChannelConfigFromContext and LoadCommitmentStateFromContext operations. In that case, the ProgramContext would look like:

struct ProgramContext {
	...

  channel_id: Option<ChannelId>,
  channel_config: Option<ChannelConfig>,
  commitment_state: Option<CommitmentState>,
  initial_per_commitment_privkey: Option<PrivateKey>, // #0
  next_per_commitment_privkey: Option<PrivateKey>, // #1
  local_per_commitment_point: Option<PublicKey>, // #1
  remote_per_commitment_point: Option<PublicKey>, // #1
  holder_identity: Option<HolderIdentity>,
}

The tradeoff of this approach is that we lose the ability to mutate individual fields inside ChannelConfig, CommitmentState, HolderIdentity. However, as mentioned above, mutating those fields would mostly just result in invalid signatures being sent, without providing much additional coverage. I think mutations are more valuable when applied to HTLC-related messages and flows, which this approach would still allow.

NOTE: One point to discuss here is that, with the current design, CommitmentDanceGenerator can also run in the PostInitSetup state. We need to ensure that it only runs in the PostChannelOpenSetup state, since only that setup contains valid inputs in ProgramContext for the Load*FromContext operations. Otherwise, those operations may fail in the PostInitSetup state.

Example generated program

# Channel state from ProgramContext
v0 = LoadChannelIdFromContext()
v1 = LoadChannelConfigFromContext()
v2 = LoadCommitmentStateFromContext()
v3 = LoadInitialPerCommitmentPrivkeyFromContext()
v4 = LoadNextPerCommitmentPrivkeyFromContext()
v5 = LoadLocalPerCommitmentPointFromContext()
v6 = LoadRemotePerCommitmentPointFromContext()
v7 = LoadHolderIdentityFromContext()

# HTLC primitives
v8 = LoadHtlcId(0)
v9 = LoadAmount(50_000_000)
v10 = LoadPaymentHash(0xAA..AA)
v11 = LoadBlockHeight(1_000)
v12 = CreateHtlc(v8, v9, v10, v11)
v13 = LoadOnionRoutingPacket(0x00..00)

# Send update_add_htlc (ignoring TLV fields for now)
v14 = BuildUpdateAddHtlc(v0, v12, v13)
SendMessage(v14)

# Advance state with the AddHtlc update
v15 = AdvanceCommitmentStateAddHtlc(v2, v12, v5, v6)

# Sign and send commitment_signed
v16 = BuildCommitmentSigned(v0, v1, v15, v7)
SendMessage(v16)

# Receive peer's revoke_and_ack and their commitment_signed
v17 = RecvRevokeAndAck()
v18 = ExtractNextPerCommitmentPoint(v17)
RecvCommitmentSigned(v1, v15, v7)

# Our next per-commitment point
v19 = LoadPrivateKey(0x02)
v20 = DerivePoint(v19)

# Send our revoke_and_ack
v21 = BuildRevokeAndAck(v0, v3, v20)
SendMessage(v21)

# Receive the failure and extract the failed HtlcId
v22 = RecvUpdateFailMalformedHtlc()

# Advance state to remove the failed HTLC
v23 = AdvanceCommitmentStateFailHtlc(v15, v22, v20, v18)

# Receive target's commitment_signed
RecvCommitmentSigned(v1, v23, v7)

# Our next per-commitment point
v24 = LoadPrivateKey(0x03)
v25 = DerivePoint(v24)

# Send our revoke_and_ack
v26 = BuildRevokeAndAck(v0, v4, v25)
SendMessage(v26)

# Sign and send commitment_signed
v27 = BuildCommitmentSigned(v0, v1, v23, v7)
SendMessage(v27)

# Receive target's final revoke_and_ack
v28 = RecvRevokeAndAck()

Note

Please note that this design is currently more of an MVP, since there are many aspects of normal channel operations still left to cover.

Some assumptions in the current design:

• In PostChannelOpenSetup, we assume that we are always the channel opener. If we later support the target as the channel opener, we will need to carry a local_side field in ProgramContext. Similarly, Htlc will also need a Side field since the struct should work for both sides. For now, we can keep an offerer field in Htlc and always set it to Side::Opener.

• Since we currently only exercise the case where we send HTLCs, there is no need for operations like BuildUpdateFulfillHtlc, BuildUpdateFailHtlc etc yet. However, if we later support receiving HTLCs from the target, we can add these operations as well.

Discussion

Multiple pending updates within one commitment dance: Currently, we only support a single pending update between CommitmentSigned messages, which makes it easier to construct and exchange the commitment dance. However, supporting N pending updates may expose additional bugs and edge cases. We need to consider how to evolve the design to support this. In such a case, AdvanceCommitmentStateAddHtlc would need to accept multiple commitment updates between BuildCommitmentSigned calls. Another extension is supporting different pending updates on local and remote sides (which may come later when we receive add Htlc). This would require handling asymmetric pending updates on both sides.

[morehouse]

I think this approach may be encoding too many things in the IR, which is why there's complications with the mutators.

I think we could simplify quite a bit if we treat CommitmentState like we treat the noise connection and have the executor manage it implicitly. Then we don't have to pass around commitment numbers, per-commitment points, channel balances, etc in the IR, and mutators can blindly rearrange the program in any structurally valid way without invalidating commitment sigs.

It would look something like this:

• The executor maintains a ProgramContext.channel_states field that maps ChannelId -> ChannelState.
• Operations no longer input or output CommitmentState, since it is implicitly loaded/saved by the executor in channel_states.
• QueuePending[Add|Fail|Fulfill]Htlc: the executor saves the pending update in channel_states.
• BuildCommitmentSigned(channel_id): the executor builds and signs the commitment from the current channel state, automatically bumping commitment numbers and clearing pending updates.
• BuildRevokeAndAck(channel_id, secret): the executor advances per-commitment points using secret.

I think this would also make it much easier to mutate/generate programs that batch multiple updates into a single commitment.

[NishantBansal2003]

Yeah, I thought about this too, and it’s definitely the simpler approach.

My main hesitation is around:

• ProgramContext is documented as "state captured during snapshot setup", and the intent seems to be that it's immutable once handed to the executor. Operations only read from it through the Load*FromContext ops. If we add commitment state there, that changes the meaning a bit -- some fields remain read-only while CommitmentState gets mutated in place, so ProgramContext is no longer a clean immutable snapshot.

• If we want the executor to own commitment state, I think it would be more consistent to pass it alongside conn and bitcoin_cli as a separate mutable parameter. The only thing that gives me pause is that conn and bitcoin_cli both have external side effects every time they're used -- conn to the target and bitcoin_cli to the bitcoind. CommitmentState, on the other hand, is purely internal bookkeeping used to generate signatures and has no external effect. so it doesn’t fit quite as naturally into the same category from a design perspective.

So, if we're okay with that distinction, then I’m fully convinced with the implicit approach. Otherwise, encoding all of this in the IR is going to make the design space quite a bit more complicated.

[Chand-ra]

CommitmentState, on the other hand, is purely internal bookkeeping used to generate signatures and has no external effect. so it doesn’t fit quite as naturally into the same category from a design perspective.

From this description, It sounds like it does fit into the same category as ProgramContext's existing fields (to me, at least 😅).

ProgramContext::chain_hash, ProgramContext::block_height are only used to craft messages like ChannelAnnouncement and OpenChannel, and ProgramContext::target_pubkey, ProgramContext::target_features aren't currently used for anything.

[morehouse]

If we want ProgramContext to stay immutable (which seems reasonable, though I don't have a strong opinion), perhaps we should finally turn the executor into an actual type that we instantiate with Executor{conn, bitcoin_cli, context, channels}. Each field would then get a doc comment explaining it's purpose, whether it's constant or mutable, etc., and the execute signature becomes Executor::execute(program, start_time) instead of having 6 params.

[NishantBansal2003]

If we want ProgramContext to stay immutable (which seems reasonable, though I don't have a strong opinion), perhaps we should finally turn the executor into an actual type that we instantiate with Executor{conn, bitcoin_cli, context, channels}. Each field would then get a doc comment explaining it's purpose, whether it's constant or mutable, etc., and the execute signature becomes Executor::execute(program, start_time) instead of having 6 params.

I think this makes sense to me. Let me update the design based on that

[NishantBansal2003]

I was working on updating the design and exploring how affine and implicit dependencies could be extended to normal channel operations.

This is the design I have so far (still incomplete), but I have a question about the following part:

sequenceDiagram
    participant smite
    participant target

    rect rgb(238, 232, 245)
        Note over smite: BuildUpdateAddHtlc -> Message
        smite->>target: SendMessage

        Note over smite: BuildCommitmentSigned -> CommitmentSignedMessage
        smite->>target: SendCommitmentSigned

        Note over target: Consumes SentCommitmentSigned from SendCommitmentSigned
        target->>smite: RecvRevokeAndAck

        Note over target: **1 What is the dependency here?
        target->>smite: RecvCommitmentSigned

        Note over smite: BuildRevokeAndAck -> Message
        smite->>target: SendMessage
        
    end

    rect rgb(228, 238, 248)
        Note over target: **2 What is the dependency here?
        target->>smite: RecvUpdateFailMalformedHtlc

        Note over target: **3 What is the dependency here?
        target->>smite: RecvCommitmentSigned

        Note over smite: BuildRevokeAndAck -> Message
        smite->>target: SendMessage
        
        Note over smite: BuildCommitmentSigned -> CommitmentSignedMessage
        smite->>target: SendCommitmentSigned

        Note over target: Consumes SentCommitmentSigned from SendCommitmentSigned
        target->>smite: RecvRevokeAndAck

    end

Loading

I have marked the dependency and affine issues above as “What is the dependency here?”.

For **1: We can’t use RecvRevokeAndAck as the dependency, because it would also be emitted during the second commitment dance, where it would not be consumed. This could cause issues once additional mutators are added.
I was thinking of introducing a separate SendCommitmentSignedAsInitiator + RecvRevokeAndAckAsInitiator operation here. Then we could directly consume a PendingCommitmentSigned value from RecvRevokeAndAckAsInitiator instead. We would also need to update the second commitment dance to use SendCommitmentSignedAsResponder + RecvRevokeAndAckAsResponder. WDYT?

For **2: I can’t really see any plausible dependency that could be used here.
Also, if we make the dependency the last BuildRevokeAndAck required to fully commit the HTLC, we would still get only one affine value. However, we may need multiple affine values if multiple HTLCs are fully committed.

For **3: We can't use RecvUpdate* here either. If we have multiple pending updates, the target will most likely send a single CommitmentSigned covering all of them. In that case, the other affine variables would remain unconsumed, which could cause issues with impossible receive operations.

We also need to ensure that no update_add_htlc or commitment_signed message is sent in between sending and receiving a commitment_signed; otherwise, we won’t be able to correctly verify the received signature. I checked LDK, and it does not send a second commitment_signed until the first one has been fully committed. Though this restricts us quite heavily to valid cases, if we want to support more general scenarios, we’ll need a way to determine which commitment state the commitment_signed received from the target corresponds to.

[Chand-ra]

For **1: We can’t use RecvRevokeAndAck as the dependency, because it would also be emitted during the second commitment dance, where it would not be consumed. This could cause issues once additional mutators are added. I was thinking of introducing a separate SendCommitmentSignedAsInitiator + RecvRevokeAndAckAsInitiator operation here. Then we could directly consume a PendingCommitmentSigned value from RecvRevokeAndAckAsInitiator instead. We would also need to update the second commitment dance to use SendCommitmentSignedAsResponder + RecvRevokeAndAckAsResponder. WDYT?

If I'm not wrong, what we're trying to prevent is a RecvCommitmentSigned happening before a RecvRevokeAndAck as that will cause timeouts, right? It is fine for an affine type to go unconsumed, and I cannot think of any scenario where it would cause an issue with the mutators. Do you have any specific examples in mind?

For **2: I can’t really see any plausible dependency that could be used here. Also, if we make the dependency the last BuildRevokeAndAck required to fully commit the HTLC, we would still get only one affine value. However, we may need multiple affine values if multiple HTLCs are fully committed.

For **3: We can't use RecvUpdate* here either. If we have multiple pending updates, the target will most likely send a single CommitmentSigned covering all of them. In that case, the other affine variables would remain unconsumed, which could cause issues with impossible receive operations.

How about creating a single RecvCommitmentDance operation instead? Something that modifies ProgramContext::CommitmentState according to each received message's type? This will most probably be a variadic node (e.g. Phi node in SSA) and we'll have to face the downside of not being able to send messages while receiving commitment ones.

We also need to ensure that no update_add_htlc or commitment_signed message is sent in between sending and receiving a commitment_signed; otherwise, we won’t be able to correctly verify the received signature.

I don't get this, isn't sending a second commitment_signed immediately after sending a first one a protocol violation? That is, won't the target drop the connection immediately?

[NishantBansal2003]

If I'm not wrong, what we're trying to prevent is a RecvCommitmentSigned happening before a RecvRevokeAndAck as that will cause timeouts, right?

Yes, if we are the initiator, then RecvCommitmentSigned should happen after RecvRevokeAndAck. If their ordering is swapped, we currently do not time out, instead, we receive an UnexpectedMessage, which we ignore. However, if we do not define a dependency between them, an unnecessary swap could result in an impossible receive operation and consequently cause a timeout

It is fine for an affine type to go unconsumed, and I cannot think of any scenario where it would cause an issue with the mutators. Do you have any specific examples in mind?

Let's say a generator produces an unconsumed affine type. Then, after applying GeneratorInsertionMutator and InstructionDeleteMutator, I can imagine cases where an entire commitment dance is removed, leaving only the RecvCommitmentSigned. This leftover operation could then consume the previously unconsumed affine type, resulting in an impossible receive operation. i.e: CommitmentDanceGenerator produces an unconsumed affine -> InstructionDeleteMutator removes most of the commitment dance from another CommitmentDanceGenerator after GeneratorInsertionMutator, leaving only RecvCommitmentSigned -> consuming affine causing impossible recv

How about creating a single RecvCommitmentDance operation instead? Something that modifies ProgramContext::CommitmentState according to each received message's type? This will most probably be a variadic node (e.g. Phi node in SSA) and we'll have to face the downside of not being able to send messages while receiving commitment ones.

IIUC, you mean that we will lock the commitment dance from SendCommitmentSigned through RecvCommitmentSigned as a single operation that emits an affine type. That affine type (along with the one from the separate SendRevokeAndAck operation) is then consumed by a single aggregated receive-update operation containing N receive operations, where N is determined by the number of fully committed HTLCs in the commitment state. This is then aggregated with the RecvCommitmentSigned through RecvRevokeAndAck phase, which does not produce any output type.

It does have the drawback you mentioned, and also with that we won’t be able to extract (because of the affine output type) the recv revokes which can be used for new secret/point and recv commit sign fields which will be used for force close fuzzing. so we need a solution for that as well. I’m thinking that if we do not take this approach, we run into the issue mentioned above and would need an out-of-the-box way to handle commitment signature verification and determine which commitment state a received signature belongs to. WDYT?

I don't get this, isn't sending a second commitment_signed immediately after sending a first one a protocol violation? That is, won't the target drop the connection immediately?

There is no mention in the BOLTs of how to handle such cases, so I think that, in the first place, implementations do not send a second commitment_signed until the first one has been fully committed.

Although the 2nd commitment_signed we send will almost certainly be rejected, resulting in an error or a force-close, consider the following scenario: before we send the 2nd commitment_signed, the target has already queued a revoke_and_ack and a commitment_signed for the first commitment_signed. We then send the 2nd commitment_signed and attempt to receive the queued commitment_signed from the 1st dance. In that case, we would receive a signature that commits only htlc1 and not htlc2. However, we would have already added htlc2 to our commitment_state. As a result, instead of recognizing that the received message belongs to an earlier commitment state and skipping it, we would incorrectly report the received signature as invalid.

[Chand-ra]

Let's say a generator produces an unconsumed affine type. Then, after applying GeneratorInsertionMutator and InstructionDeleteMutator, I can imagine cases where an entire commitment dance is removed, leaving only the RecvCommitmentSigned.

This cannot happen unless RecvCommitmentSigned consumes no affine variables. The swap mutator is forbidden from touching affines, so the only thing that can re-wire affine dependencies is the delete mutator (which does so during healing), and it is disallowed from removing a producer (of affine variable) until a consumer (of the said affine variable) exists.

IIUC, you mean that we will lock the commitment dance from SendCommitmentSigned through RecvCommitmentSigned as a single operation that emits an affine type. That affine type (along with the one from the separate SendRevokeAndAck operation) is then consumed by a single aggregated receive-update operation containing N receive operations, where N is determined by the number of fully committed HTLCs in the commitment state. This is then aggregated with the RecvCommitmentSigned through RecvRevokeAndAck phase, which does not produce any output type.

We can do this, but it is not what I meant. I'm proposing replacing all Recv* operations in the commitment dance with a single operation (leaving Send* operations as is). This new operation can consume a variable number of affine types, so we can handle batched updates using it. (Phi nodes in LLVM's SSA are an example of such variable-inputs-consuming operations).

I cannot fully map out the details because I'm not really familiar with the commitment scheme 😓.

It does have the drawback you mentioned, and also with that we won’t be able to extract (because of the affine output type) the recv revokes which can be used for new secret/point and recv commit sign fields which will be used for force close fuzzing. so we need a solution for that as well. I’m thinking that if we do not take this approach, we run into the issue mentioned above and would need an out-of-the-box way to handle commitment signature verification and determine which commitment state a received signature belongs to. WDYT?

We can always use the ProgramContext::CommitmentState to store the values that we need to craft later messages. If not, we already had a way to include an affine type in a compound variable (that we got rid of in the final affine implementation because it wasn't currently used). It allowed multiple extractions of non-affine types, but only a single extraction of affine types to prevent multiple-uses.

Let me know if this is useful, I can always re-implement it.

Although the 2nd commitment_signed we send will almost certainly be rejected, resulting in an error or a force-close, consider the following scenario: before we send the 2nd commitment_signed, the target has already queued a revoke_and_ack and a commitment_signed for the first commitment_signed. We then send the 2nd commitment_signed and attempt to receive the queued commitment_signed from the 1st dance. In that case, we would receive a signature that commits only htlc1 and not htlc2. However, we would have already added htlc2 to our commitment_state. As a result, instead of recognizing that the received message belongs to an earlier commitment state and skipping it, we would incorrectly report the received signature as invalid.

Oh okay, I think I get it now. And this is why you proposed the solution earlier to "never send a second commitment_signed until we've received confirmation for the first one". Shouldn't be too difficult to do using affine types.

The other option is to encode state tracking for each HTLC in ProgramContext::CommitmentState similar to an existing solution from a client implementations. Don't know how difficult this would be though.

[morehouse]

The channel state machine is complicated enough that I think we really want to have the executor handle the receive logic implicitly rather than encoding it in the IR.

Affine types aren't a great fit here because there isn't a static 1:1 correspondence between sent messages and received messages (e.g., one SendCommitmentSigned can result in us being owed a variable number of messages, and one RecvUpdateFailMalformedHtlc is dependent on multiple previously sent messages). I think affine types are more suitable for handshake-type interactions where we send one message and get one message in response (e.g., open_channel/accept_channel, funding_created/funding_signed).

Additionally, the current static Recv* operations aren't a great fit because we can't reliably predict what level of commitment batching the target will use when sending its own update messages (e.g., will we receive 1 update then commitment_signed or 10 updates then commitment_signed), and the target will likely vary its behavior based on timing artifacts (typical implementations batch across a fixed time window).

I propose that we reduce the IR for commitment fuzzing to just a few send operations. Initially just:

• SendUpdateAddHtlc(channel_id, htlc_id, amount, hash, cltv, onion)
• SendCommitmentSigned(channel_id)
• SendRevokeAndAck(channel_id)

Build* operations would no longer be needed as they would be absorbed into the Send* operations. Commitment-related Recv* operations would also go away and receives would be handled implicitly by the executor when a data dependency requires it and the target owes us messages.

When the executor determines that it needs a key protocol message from the target to properly handle the current send operation, it would drain all incoming messages until the needed message is received, applying any received updates to the channel state as it goes. I think there's only 2 situations where this needs to be done:

• Before executing SendCommitmentSigned if the latest commitment point for the target is unknown. This situation means the target owes us a revoke_and_ack. The executor would block and drain incoming messages until the revoke_and_ack with the needed commitment point is received.
• Before executing SendRevokeAndAck if the target owes us a commitment_signed. The executor would block and drain incoming messages until the owed commitment_signed is received. (Note: this is not a strict data dependency because we don't actually need any data from the commitment_signed to construct our revoke_and_ack message, but there is an event-ordering dependency if we want to exercise deeper protocol states). commitment_signed is owed to us in two cases:
  • Mirror case: We previously sent updates and a commitment_signed. The target needs to mirror those updates onto our commitment by sending revoke_and_ack followed by commitment_signed.
  • Resolve HTLC case: one or more HTLCs are irrevocably committed and we know the target is currently able to resolve at least one HTLC (either fail or success). The target needs to send us update_[fulfill|fail]_htlc followed by commitment_signed.

Besides these two cases, all commitment messages get constructed and sent immediately using the executor's current channel state, without checking for incoming messages.

Using this approach, @NishantBansal2003's protocol flow listed above would be exercised as follows:

 sequenceDiagram                                                                                          
     participant IR as IR program                                                     
     participant Exec as Executor                                           
     participant Tgt as Target                                                                            
                                                                                                          
     IR->>Exec: SendUpdateAddHtlc
     Exec->>Tgt: update_add_htlc                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is known, do not drain
     Exec->>Tgt: commitment_signed
                                                                                                          
     IR->>Exec: SendRevokeAndAck
     Note over Exec: committed HTLCs not mirrored by target -> drain messages until commitment_signed
     Tgt-->>Exec: revoke_and_ack (apply to channel state)
     Tgt-->>Exec: commitment_signed (verify sigs, apply to channel state)
     Exec->>Tgt: revoke_and_ack
                                                     
     IR->>Exec: SendRevokeAndAck
     Note over Exec: target-resolvable HTLC is irrevocably committed -> drain messages until commitment_signed     
     Tgt-->>Exec: update_fail_malformed_htlc (apply to channel state)           
     Tgt-->>Exec: commitment_signed (verify sigs, apply to channel state)
     Exec->>Tgt: revoke_and_ack                                                                           
                                                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is known, do not drain
     Exec->>Tgt: commitment_signed
     Note over Exec: optional (non-blocking) drain at end of program to check signatures and run state oracles
     Tgt-->>Exec: revoke_and_ack

Loading

The biggest win from this approach is that all the commitment-related IR operations can be reordered however mutators want without causing timeouts. We shouldn't have to worry about unusual protocol flows since the executor will automatically figure out when the target owes us messages.

Here's another example program that exercises a highly unusual (though technically legal until the last operation) flow:

 sequenceDiagram                                                                                          
     participant IR as IR program                                                     
     participant Exec as Executor                                           
     participant Tgt as Target                                                                            
                                                                                                          
     IR->>Exec: SendUpdateAddHtlc
     Exec->>Tgt: update_add_htlc                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is known, do not drain
     Exec->>Tgt: commitment_signed

     IR->>Exec: SendUpdateAddHtlc
     Exec->>Tgt: update_add_htlc                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is unknown -> drain messages until revoke_and_ack
     Tgt-->>Exec: revoke_and_ack (apply to channel state)
     Exec->>Tgt: commitment_signed

     IR->>Exec: SendRevokeAndAck
     Note over Exec: committed HTLCs not mirrored by target -> drain messages until commitment_signed
     Tgt-->>Exec: commitment_signed (verify sigs, apply to channel state)
     Exec->>Tgt: revoke_and_ack

     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is unknown -> drain messages until revoke_and_ack
     Tgt-->>Exec: revoke_and_ack
     Exec->>Tgt: commitment_signed

     Note over Exec: optional (non-blocking) drain at end of program to check signatures and run state oracles
     Tgt-->>Exec: update_fail_malformed_htlc
     Tgt-->>Exec: commitment_signed
     Tgt-->>Exec: error (commitment_signed with no updates)

Loading

[Chand-ra]

The channel state machine is complicated enough that I think we really want to have the executor handle the receive logic implicitly rather than encoding it in the IR.

So basically making the executor act as a sink for commitment messages received from the target. Looks very similar in spirit to the RecvCommitmentDance operation that I proposed. The downsides should be the same then, we won't be able to insert flows between receiving a revoke_and_ack and sending a commitment_signed. Personally, I think the upsides (no changes to the IR, only minimal additions) are strong enough to see this plan through.

[morehouse]

So basically making the executor act as a sink for commitment messages received from the target. Looks very similar in spirit to the RecvCommitmentDance operation that I proposed.

It's similar. The main differences:

• Commitment-related receives stay out of the IR. Instruction sequencing and timeouts should become a non-issue.
• Receives are lazy and finer-grained. The executor only receives up to the message it needs -- the whole commitment dance doesn't need to finish at once.

The downsides should be the same then, we won't be able to insert flows between receiving a revoke_and_ack and sending a commitment_signed.

Actually I think we can. We only need to drain the revoke_and_ack if we're attempting to send a commitment_signed and we don't know the next commitment point. But we would opportunistically apply the revoke_and_ack when receiving other messages. For example:

 sequenceDiagram                                                                                          
     participant IR as IR program                                                     
     participant Exec as Executor                                           
     participant Tgt as Target                                                                            
                                                                                                          
     IR->>Exec: SendUpdateAddHtlc
     Exec->>Tgt: update_add_htlc                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is known, do not drain
     Exec->>Tgt: commitment_signed

     IR->>Exec: SendOpenChannel
     Exec->>Tgt: open_channel
     IR->>Exec: RecvAcceptChannel
     Note over Exec: drain messages until accept_channel or error
     Tgt-->>Exec: revoke_and_ack (apply to channel state)
     Tgt-->>Exec: commitment_signed (verify sigs, apply to channel state)
     Tgt-->>Exec: accept_channel

     Note over IR: other arbitrary operations can happen here

     IR->>Exec: SendUpdateAddHtlc
     Exec->>Tgt: update_add_htlc                                                                          
     IR->>Exec: SendCommitmentSigned
     Note over Exec: latest_commitment_point is known, do not drain
     Exec->>Tgt: commitment_signed

Loading

We read and apply the target's revoke_and_ack and commitment_signed messages while waiting for accept_channel. We then can insert whatever operations we want between that received revoke_and_ack and the send of commitment_signed below.