`NEG32` sign-extends its 32-bit result to 64 bits

[caomingpei]

Overview

Mithril sign-extends the result of NEG32 to 64 bits, while the sBPF
instruction definition requires the wrapped 32-bit result to be zero-extended.
A verifier-accepted program therefore returns 0xffffffffffffffff instead of
the specified 0x00000000ffffffff.

Minimal program:

mov32 r0, 1
neg32 r0
exit

b4 00 00 00 01 00 00 00
84 00 00 00 00 00 00 00
95 00 00 00 00 00 00 00

Configuration:

execution:          interpreter
sBPF versions:      V0, V1, and V3
instruction budget: 1,000
stack:              64 x 4,096-byte frames
heap:               empty
input:              one byte
syscalls/functions: none

Actual and specified results for each of V0, V1, and V3:

Specified NEG32 result: 0x00000000ffffffff
Mithril interpreter:    0xffffffffffffffff

V2 is excluded because opcode 0x84 is reserved in that version.

This is a deterministic interpreter semantic difference on ordinary,
verifier-approved bytecode. Later 64-bit comparisons, branches, arithmetic, or
program-status handling can observe the incorrect upper 32 bits. The
reproducer below directly establishes the VM-level register-value difference;
it does not claim that a matched transaction or committed-state divergence was
executed.

Tested Version

Mithril:    6f31241ba6c48a37316ea23cc947bde395e0722f (v0.3.0)
Anza sBPF:  db4f0681951171ee97988989695ceef67fe3dbb3 (specification/source oracle)
Go:         1.25.7

Root Cause

The sBPF bytecode definition specifies:

(dst as i32).wrapping_neg() as u32 as u64

See Anza's
NEG32 definition.
The intermediate u32 conversion is what clears the upper 32 bits.

Mithril instead evaluates:

r[ins.Dst()] = uint64(-int32(r[ins.Dst()]))

in
pkg/sbpf/interpreter.go.
When -int32(...) is negative, converting it directly to uint64 produces the
64-bit two's-complement representation. For an input of one, that is
0xffffffffffffffff.

Anza performs wrapping 32-bit negation and masks the value before storing it in
the 64-bit register in
src/interpreter.rs.
Firedancer independently negates an unsigned 32-bit value in
fd_vm_interp_core.c,
and Sig selects a u32 result for 32-bit opcodes in
shared/vm/interpreter.zig.

The program performs no memory access and uses no syscall, function registry,
ELF relocation, JIT, or FFI path. Both official verifiers accept the same raw
instructions. The result therefore does not depend on a loader quirk, memory
mapping, compute-budget mismatch, or caller-provided VM invariant.

Suggested Fix

Preserve the 32-bit wrapped value before widening it, for example:

r[ins.Dst()] = uint64(uint32(-int32(r[ins.Dst()])))

An equivalent unsigned form is:

r[ins.Dst()] = uint64(-uint32(r[ins.Dst()]))

Add table-driven interpreter tests for inputs 0, 1, 0x80000000, and
0xffffffff, plus values with nonzero upper 32 bits. Run the tests for V0, V1,
and V3, require every NEG32 result to have zero upper 32 bits, and retain a
separate test that V2 rejects opcode 0x84.

Reproduction

package main

import (
	"encoding/binary"
	"fmt"

	"github.com/Overclock-Validator/mithril/pkg/cu"
	"github.com/Overclock-Validator/mithril/pkg/sbpf"
	"github.com/Overclock-Validator/mithril/pkg/sbpf/sbpfver"
)

var sanity = []byte{
	0xb7, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00,
	0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
}

var candidate = []byte{
	0xb4, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00,
	0x84, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
	0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
}

func decode(raw []byte) []sbpf.Slot {
	text := make([]sbpf.Slot, len(raw)/sbpf.SlotSize)
	for i := range text {
		text[i] = sbpf.Slot(binary.LittleEndian.Uint64(raw[i*sbpf.SlotSize:]))
	}
	return text
}

func execute(version uint32, raw []byte) (uint64, uint64) {
	program := &sbpf.Program{
		RO:          raw,
		TextBytes:   raw,
		Text:        decode(raw),
		TextVA:      sbpf.VaddrProgram,
		Entrypoint:  0,
		SbpfVersion: sbpfver.SbpfVersion{Version: version},
	}
	if err := program.Verify(); err != nil {
		panic(fmt.Sprintf("Mithril verifier rejected the program: %v", err))
	}

	meter := cu.NewComputeMeter(1_000)
	vm := sbpf.NewInterpreter(program, &sbpf.VMOpts{
		HeapMax:        0,
		MaxCU:          1_000,
		ComputeMeter:   &meter,
		Input:          []byte{0},
		InputDataVaddr: sbpf.VaddrInput,
	})
	defer vm.Finish()

	value, count, err := vm.Run()
	if err != nil {
		panic(fmt.Sprintf("Mithril interpreter failed after %d instructions: %v", count, err))
	}
	return value, count
}

// NEG32 is defined as a wrapping 32-bit negation followed by zero-extension.
// Negating a uint32 performs the operation modulo 2^32; converting that result
// to uint64 therefore implements the specified oracle without using Mithril's
// NEG32 handler.
func specifiedNeg32(value uint64) uint64 {
	return uint64(-uint32(value))
}

func main() {
	value, count := execute(sbpfver.SbpfVersionV0, sanity)
	fmt.Printf(
		"implementation=mithril case=sanity version=V0 verify=accepted execute=ok r0=0x%016x instruction_count=%d\n",
		value,
		count,
	)
	if value != 1 || count != 2 {
		panic("sanity program did not return one in two instructions")
	}

	expected := specifiedNeg32(1)
	if expected != 0x00000000ffffffff {
		panic(fmt.Sprintf("oracle error: got 0x%016x", expected))
	}

	for _, item := range []struct {
		name    string
		version uint32
	}{
		{"V0", sbpfver.SbpfVersionV0},
		{"V1", sbpfver.SbpfVersionV1},
		{"V3", sbpfver.SbpfVersionV3},
	} {
		actual, count := execute(item.version, candidate)
		fmt.Printf(
			"implementation=mithril case=neg32 version=%s verify=accepted execute=ok actual=0x%016x expected=0x%016x mismatch=%t instruction_count=%d\n",
			item.name,
			actual,
			expected,
			actual != expected,
			count,
		)
		if actual == expected {
			panic("the tested revision no longer reproduces the NEG32 bug")
		}
		if actual != 0xffffffffffffffff || count != 3 {
			panic("unexpected result while reproducing the NEG32 bug")
		}
	}
}

Expected output:

implementation=mithril case=sanity version=V0 verify=accepted execute=ok r0=0x0000000000000001 instruction_count=2
implementation=mithril case=neg32 version=V0 verify=accepted execute=ok actual=0xffffffffffffffff expected=0x00000000ffffffff mismatch=true instruction_count=3
implementation=mithril case=neg32 version=V1 verify=accepted execute=ok actual=0xffffffffffffffff expected=0x00000000ffffffff mismatch=true instruction_count=3
implementation=mithril case=neg32 version=V3 verify=accepted execute=ok actual=0xffffffffffffffff expected=0x00000000ffffffff mismatch=true instruction_count=3