smite-ir: Introduce affine state variables for strict state enforcement by Chand-ra · Pull Request #97 · morehouse/smite

Chand-ra · 2026-05-25T11:02:37Z

This PR introduces affine (single-use) types to the IR to strictly enforce the Lightning Network state machine during fuzzing, in order to prevent timeout hangs caused by semantically invalid mutation sequences.

Solves issue #75, see it for more details.

Adds `PendingAccept` and `ChannelState` to the `Variable` and `VariableType` enums. Unlike standard data variables which can be referenced infinitely, these new types are designed to be "affine" (single-use). They represent strict topological locks in the Lightning Network state machine (e.g., `PendingAccept` ensures a channel is actively pending before allowing subsequent channel actions).

Introduce the strict topological link for channel initialization. - Add `SendOpenChannel` operation: Consumes a composed `Message` and outputs a `PendingAccept` affine variable. The executor verifies the outgoing message is type `open_channel`. - Modify `RecvAcceptChannel`: Now requires `PendingAccept` as an input, enforcing that the fuzzer cannot wait for an `accept_channel` unless it actually opened a channel first. - Modify `AcceptChannelField`: Allow the compound variable produced by `RecvAcceptChannel` to yield a `ChannelState` affine variable. - Update unit tests to accommodate the new input requirements for `RecvAcceptChannel`.

Update `pick_variable` with a dedicated branch for affine types. Unlike data variables which use a probabilistic 75/15/10 strategy, affine types use deterministic tip-tracking. When a generator requests an affine variable, the builder iterates backwards to find the most recent unspent candidate. If all are spent, it defaults to the tip of the chain, allowing the Validator to catch and reject the duplicate consumption. This prevents fuzzer crashes while eliminating generator starvation.

Update `Program::validate()` to enforce the single-use nature of affine state variables, preventing mutators from generating impossible state-machine sequences. Add two validation rules: 1. Affine Over-Use: An affine variable cannot be consumed as an input more than once. This prevents mutators from reusing old state locks to bypass protocol ordering. 2. Affine Over-Extract: An affine token cannot be extracted more than once from the same compound variable. This prevents `InputSwapMutator` from cloning state locks and forking the timeline into parallel, conflicting execution paths.

Update `OpenChannelGenerator` to utilize the newly introduced strict topological operations: 1. Replace `SendMessage` with `SendOpenChannel`, which consumes the `Message` payload and outputs a `PendingAccept`. 2. Update `RecvAcceptChannel` to consume the `PendingAccept`. 3. Update tests to accommodate the non-void output of `SendOpenChannel`.

Introduce a `LoadStateFromContext` operation to allow the IR to integrate with advanced fuzzing setups (like a future `PostOpenChannelSetup`). When the fuzzer starts execution from a snapshot where a channel is already open, the IR needs a way to acquire the `ChannelState` lock without having to execute the entire channel opening process. This operation allows the Executor to pull pre-existing state variables directly out of the `ProgramContext`.

Modify the mutator loop to clone the program and validate it after each applied mutation. Because the IR now contains affine state variables, mutators will frequently generate invalid graphs. By calling `cloned.validate()`, we drop mutations that violate the protocol's state machine, keeping the target node from hanging.

Add tests to verify the data-flow rules introduced for state tracking.

Chand-ra · 2026-05-28T06:18:27Z

+            let candidate_to_resolve = chosen_candidate
+                .unwrap_or_else(|| candidates.last().unwrap())
+                .clone();
+            return self.resolve_candidate(candidate_to_resolve);
+        }


As discussed here, this is an anti-pattern and we should modify the function's signature to return an Option<usize> instead of intentionally generating an invalid instruction.

morehouse · 2026-05-28T17:01:41Z

+    /// Affine lock: Channel opened, waiting for `accept_channel`.
+    PendingAccept,


The term "affine lock" is unnecessarily confusing -- I don't think anything is actually being "locked". Let's just create a section titled "affine variables".

Also I think it would be slightly easier to understand the variable if we called it SentOpenChannel instead. Then SendOpenChannel returns a SentOpenChannel and RecvAcceptChannel requires SentOpenChannel. Both read more naturally.

Suggested change

/// Affine lock: Channel opened, waiting for `accept_channel`.

PendingAccept,

// Affine (single-use) variables

/// `open_channel` has been sent, so `accept_channel` may now be received.

SentOpenChannel,

morehouse · 2026-05-28T17:02:03Z

+    /// Affine lock: Channel established. Consumed by all active channel actions.
+    ChannelState,


I don't think we need this variable.

morehouse · 2026-05-28T17:27:04Z

+    /// Send an `open_channel` message over the connection.
+    /// Produces a `PendingAccept` variable.
+    /// Input: `Message`.
+    SendOpenChannel,


I think we might actually want a specific OpenChannelMessage type that is input for SendOpenChannel. That way we can be sure that some other message type is never used as input to SendOpenChannel.

Relying on the executor to reject these cases is slow and unnecessary if we add the new variable type.

I'm worried about the IR bloat if we do that, we'd eventually need 40+ variants for every LN message. Maybe making the executor reject these is wrong and we should allow InputSwapMutator to freely swap different message types?

morehouse · 2026-05-28T18:50:02Z

+        for input in inputs {
+            self.refs_count[*input] += 1;
+        }
+


append also needs to verify that any affine variables referenced haven't already been consumed.

morehouse · 2026-05-28T18:55:16Z

    /// Candidate variables indexed by output type.
    candidates: HashMap<VariableType, Vec<Candidate>>,
+    /// Reference count for each variable.
+    refs_count: Vec<usize>,


We don't need a reference count -- really all we need is to know whether affine variables have been consumed yet or not. So a Vec<bool> would suffice, or even better -- just remove affine variables from candidates as they're consumed (no new vector necessary).

morehouse · 2026-05-28T19:06:52Z

+
+    /// Returns true if this operation is Extract*.
+    #[must_use]
+    pub fn is_extract(&self) -> bool {


We already have extractable_fields, so maybe we don't need this function.

morehouse · 2026-05-28T19:23:51Z

+    #[error(
+        "Instruction {instr}: affine {var_type:?} extracted {extract_count} times from {index} (max 1)"
+    )]
+    AffineOverExtract {


I think we should just make InputSwapMutator skip affine variables. In general these variables carry no data and are just there for sequencing, so swapping one affine variable with another has no practical effect.

And if extracting affine variables is an issue for other mutators, then perhaps we can outright ban affine variables inside compound variables, so we don't have to deal with it. At least for now we don't have any need since Send*Message only ever has a single return value (the affine variable).

morehouse · 2026-05-28T20:13:28Z

    /// Load the chain hash from the program context.
    LoadChainHashFromContext,
+    /// Load a state variable from the program context.
+    LoadStateFromContext(VariableType),


We don't currently need this operation, so let's defer implementing it until there's a need.

morehouse · 2026-05-28T20:16:45Z

+                Some(Variable::PendingAccept)
+            }
+
            Operation::RecvAcceptChannel => {


The executor needs to enforce the affine input type, and should also ensure the affine type hasn't already been consumed.

morehouse · 2026-05-28T20:18:21Z

+                InputSwapMutator.mutate(&mut cloned, &mut self.rng);
                "input-swap"
            };
+            if cloned.validate().is_err() {


I don't think we need to do this. I'd prefer to have the requirement that mutators always produce valid programs.

Chand-ra force-pushed the implicit_dependence branch from 80932e9 to 531ca61 Compare May 25, 2026 11:16

Chandra Pratap added 8 commits May 25, 2026 11:16

smite-ir/tests: Add tests for affine type constraints

798752a

Add tests to verify the data-flow rules introduced for state tracking.

Chand-ra force-pushed the implicit_dependence branch from 531ca61 to 798752a Compare May 25, 2026 11:16

Chand-ra mentioned this pull request May 27, 2026

IR Design and Implementation Plan #5

Open

9 tasks

morehouse mentioned this pull request May 27, 2026

Panic on invalid programs and bad seed inputs #94

Draft

Chand-ra commented May 28, 2026

View reviewed changes

morehouse requested changes May 28, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

smite-ir: Introduce affine state variables for strict state enforcement#97

smite-ir: Introduce affine state variables for strict state enforcement#97
Chand-ra wants to merge 8 commits into
morehouse:masterfrom
Chand-ra:implicit_dependence

Chand-ra commented May 25, 2026

Uh oh!

Uh oh!

Chand-ra May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

Chand-ra May 30, 2026 •

edited

Loading

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

morehouse May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		/// Affine lock: Channel opened, waiting for `accept_channel`.
		PendingAccept,

-    /// Affine lock: Channel opened, waiting for `accept_channel`.
-    PendingAccept,
+    // Affine (single-use) variables
+    /// `open_channel` has been sent, so `accept_channel` may now be received.
+    SentOpenChannel,

		/// Affine lock: Channel established. Consumed by all active channel actions.
		ChannelState,

Conversation

Chand-ra commented May 25, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Chand-ra May 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Chand-ra May 30, 2026 •

edited

Loading