[splashevolution]

Purpose

Close the exact RED-1 binding gap with the smallest useful formal addition.

RED-1 showed that capability declaration plus successful lowering accepts two different bindings for the same semantic identity.

GREEN-1 introduces a target-specific DeviceModel(Resource) and an executable checkBinding relation.

Machine-checked result

For the existing RED-1 witness:

old gate(reference)   = true
old gate(adversarial) = true

new binding check(reference)   = true
new binding check(adversarial) = false

The target-neutral statusScript remains free of physical addresses.

The PVM32 device model independently states:

0x20 -> SemanticId(1001)
0x21 -> SemanticId(1002)

and the checker verifies that the realization binding agrees with that device model.

General theorem

The PR proves:

checkBinding(device, resourceOf, id) = true
    <->
bindingMatchesDevice(device, resourceOf, id)

and audits the theorem dependencies in CI.

Deliberate limitation

GREEN-1 closes binding correctness only.

It does not yet establish:

• scale/representation correctness;
• units;
• byte order;
• protocol state;
• ACK/NACK semantics;
• persistence;
• atomicity;
• simulator or physical-device conformance.

The DeviceModel itself is currently an explicit model assumption; physical conformance is a later obligation.

Why this is intentionally small

We do not yet introduce RealizationEvidence, Observation, traces, evolution proofs, QEMU, or Renode because RED-1 does not require them.

The next falsification target should keep the correct resource and use the wrong representation, e.g. 25 instead of 250 for a 25.0 °C fixed-point target.