[Detail Bug] Verification: Porcupine model rejects valid appends with empty fencing token on fresh streams

[detail-app]

Detail Bug Report

https://app.detail.dev/org_89d327b3-b883-4365-b6a3-46b6701342a9/bugs/bug_e3c3571e-2970-459a-85dd-e1843d70941b

Introduced in #1 by @sgbalogh on Aug 11, 2025

Summary

• Context: The Go Porcupine linearizability model validates S2 stream operations including fencing token semantics.
• Bug: The model incorrectly initializes the stream's fencing token as nil instead of empty string "", causing it to reject valid S2 behavior where an append with BatchFencingToken: "" succeeds on a fresh stream.
• Actual vs. expected: Model rejects append with empty fencing token on fresh stream, but S2 allows it because streams default to fencing token "".
• Impact: The model incorrectly flags legitimate S2 behavior as a linearizability violation, producing false negatives during verification.

Code with Bug

var s2Model = porcupine.NondeterministicModel{
    Init: func() []interface{} {
        states := []interface{}{
            StreamState{
                Tail:         0,
                StreamHash:   0,
                FencingToken: nil, // <-- BUG 🔴 should be Ptr("") to match S2's default
            },
        }
        return states
    },

if inp.BatchFencingToken != nil {
    // Illegal
    if startingState.FencingToken == nil || *startingState.FencingToken != *inp.BatchFencingToken {
        return []interface{}{} // <-- BUG 🔴 treats nil as mismatch, rejecting valid provided token "" on fresh stream
    }
}

Explanation

S2 streams default their fencing token to the empty string "". The model instead represents a fresh stream as FencingToken: nil. When an append explicitly provides BatchFencingToken: "" (protobuf field present but empty), the model checks startingState.FencingToken == nil and immediately rejects the operation as illegal.

In S2, None (field omitted) and Some("") (field present and empty) are distinct at the API boundary: omitting the token bypasses the check, while providing "" performs an equality check that succeeds because the stream’s default token is also "".

Codebase Inconsistency

S2 server initializes the fencing token to its default (empty string) and compares provided tokens via exact equality:

fencing_token: CommandState {
    state: FencingToken::default(), // defaults to ""
    applied_point: ..SeqNum::MIN,
},

if let Some(provided_token) = fencing_token
    && provided_token != self.fencing_token.state
{
    Err(AppendConditionFailedError::FencingTokenMismatch { ... })?;
}

This allows Some("") to match a fresh stream’s "", whereas the Go model’s nil cannot.

Failing Test

TestAppendWithEmptyFencingTokenOnFreshStream (main_test.go:446-465) demonstrates the issue.

Test output:

main_test.go:458: Model result for append with BatchFencingToken='' on fresh stream: Illegal
main_test.go:462: Model incorrectly rejects append with empty fencing token on fresh stream

Recommended Fix

Initialize the stream fencing token as an empty string instead of nil:

StreamState{
    Tail:         0,
    StreamHash:   0,
    FencingToken: Ptr(""),
},

History

This bug was introduced in commit 12a649b. The commit added fencing token support to the Porcupine model but incorrectly initialized the stream's FencingToken to nil, assuming this represented "no fencing token" on a fresh stream.