[splashevolution]

Purpose

Establish the next machine-checked negative result after GREEN-2.

GREEN-2 checks:

• semantic identity -> target resource;
• semantic value -> raw representation.

RED-3 asks whether that is enough to establish protocol/state correctness.

It is not.

Witness

Both executions use the exact same GREEN-2-correct write:

resource = 0x20
raw      = 250

Only the surrounding trace changes.

Reference:

enter-config
issue-write
observe-ACK
exit-config

Mutation:

issue-write
observe-ACK

Machine-checked result

reference.write = mutated.write
reference.trace != mutated.trace

GREEN2(reference) = true
GREEN2(mutated)   = true

This establishes:

binding correctness plus representation correctness is not protocol/state correctness.

Claim boundary

This PR does not yet claim that the reference trace is valid or that the mutated trace is invalid. The current theory cannot state that relation. That missing relation is precisely RED-3.

GREEN-3 constraint

The next step must distinguish the traces without:

• hard-coding one whole accepted sequence;
• trusting the realization generator;
• moving target protocol mechanics into the target-neutral semantic contract;
• adding persistence/timing before required;
• introducing QEMU/Renode yet.