Close GREEN-1 with an independent device binding checker

STATUS.md

@@ -55,17 +55,17 @@ They should not be copied into new semantic-continuity modules.
 
 See `docs/TERMINOLOGY_AUDIT.md`.
 
-## Active formal milestone — RED-1
+## Active formal milestone — GREEN-1
 
-RED-1 now targets the precise gap between declared capability and realization correctness. The branch \`research/semantic-continuity-red1\` adds a machine-checked counterexample showing that two distinct target bindings for the same semantic script both pass the current capability-plus-lowering gate.
+RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate.
 
-The experiment is intentionally narrower than a device-correctness theorem: the current model cannot yet state why one binding is semantically faithful. That inability is the RED result.
+GREEN-1 adds the minimum missing formal boundary: a generic \`DeviceModel(Resource)\` that independently states what each target resource denotes, plus an executable \`checkBinding\` relation. The PVM32 witness accepts the reference binding and rejects the RED-1 adversarial binding without putting a physical address into the target-neutral semantic script.
 
-See \`docs/research/RED1_DISHONEST_BINDING.md\`.
+See \`docs/research/RED1_DISHONEST_BINDING.md\` and \`docs/research/GREEN1_DEVICE_BINDING_CHECK.md\`.
 
-The next GREEN step must distinguish correct from adversarial realization without hard-coding a physical address into the target-neutral semantic contract.
+This closes only binding correctness relative to a stated device model. Representation, units, protocol state, persistence, failure handling, and physical-device conformance remain open.
 
-The motivating case remains:
+The next falsification target is the same physical resource with a wrong representation:
 
 Example:
 

docs/research/GREEN1_DEVICE_BINDING_CHECK.md

@@ -0,0 +1,180 @@
+# GREEN-1 — Device-Model Binding Check
+
+**Branch:** `research/semantic-continuity-green1`  
+**Baseline:** `334363d4befdae9a3c31675c8feab0fe0214aa57`
+
+## Result
+
+GREEN-1 closes the exact binding gap demonstrated by RED-1.
+
+RED-1 established:
+
+```text
+capability declaration + successful lowering
+                 ≠
+binding correctness
+```
+
+because both of these mappings were accepted:
+
+```text
+SemanticId(1001) -> 0x20
+SemanticId(1001) -> 0x21
+```
+
+GREEN-1 adds one missing formal object:
+
+```text
+DeviceModel(Resource)
+    denotes : Resource -> Option SemanticId
+```
+
+and one executable relation:
+
+```text
+checkBinding(device, resourceOf, semanticId)
+```
+
+The realization supplies `resourceOf`.  
+The independently stated device model supplies `denotes`.
+
+A binding is accepted only when both agree on semantic identity.
+
+## Why the physical address is allowed in DeviceModel
+
+The target-neutral contract still contains only:
+
+```text
+statusIdentity = SemanticId(1001)
+statusScript   = WRITE(destination = statusIdentity)
+```
+
+It does **not** contain `0x20`.
+
+For the PVM32 target, the device model states target-specific facts:
+
+```text
+0x20 denotes SemanticId(1001)
+0x21 denotes SemanticId(1002)
+```
+
+That is the intended abstraction boundary:
+
+```text
+target-neutral meaning
+        |
+        v
+target-specific device model
+        |
+        v
+physical resource representation
+```
+
+Moving the physical fact into the device model is not hiding it. The address is
+a target fact and therefore belongs at the target boundary.
+
+## Machine-checked result
+
+`lean/PSL/SemanticContinuityGreen1.lean` proves:
+
+```text
+old gate(reference)   = true
+old gate(adversarial) = true
+
+new binding check(reference)   = true
+new binding check(adversarial) = false
+```
+
+It also proves generically:
+
+```text
+checkBinding(device, resourceOf, id) = true
+    <->
+bindingMatchesDevice(device, resourceOf, id)
+```
+
+So the executable checker is sound and complete for the relation GREEN-1
+actually claims.
+
+## What GREEN-1 does not prove
+
+This is **not** yet full realization soundness.
+
+The device model currently says only what a resource denotes. It does not yet
+model:
+
+- numeric representation or scale;
+- engineering units;
+- byte order or signedness;
+- configuration/authority state;
+- command ordering;
+- ACK/NACK behavior;
+- persistence;
+- atomicity;
+- timing;
+- simulator or physical-device conformance.
+
+A realization that uses the correct resource but writes the wrong value can
+still pass GREEN-1.
+
+That limitation is intentional.
+
+## Trust boundary
+
+GREEN-1 removes trust in the realization's binding declaration itself.
+
+It does **not** remove trust in the stated `DeviceModel`.
+
+The theorem is therefore:
+
+> accepted binding is faithful **with respect to the stated device model**.
+
+Whether that model matches QEMU, Renode, firmware, or physical hardware remains
+a separate conformance obligation.
+
+## Why this is the minimum useful GREEN
+
+We considered introducing all of:
+
+```text
+Realization
+RealizationEvidence
+Observation
+Trace
+Checker
+Evolution
+```
+
+GREEN-1 does not need them.
+
+For the RED-1 counterexample, the smallest missing distinction is an
+independent target model of resource meaning.
+
+Adding more theory before a failing case requires it would make the research
+architecture larger without increasing the result.
+
+## Next falsification target
+
+The natural RED-2 is:
+
+> use the **correct resource** but the **wrong representation**.
+
+For example:
+
+```text
+semantic intent: 25.0 °C
+correct target encoding: 250
+adversarial encoding:    25
+resource:                0x20 in both cases
+```
+
+Both bindings would pass GREEN-1.
+
+If we can machine-check that failure without changing the semantic contract,
+then RED-2 will justify the next layer of device behavior/observation theory.
+
+## Kill condition retained
+
+If future work requires target addresses, encodings, or protocol mechanics to
+be inserted into the target-neutral semantic contract, the continuity
+abstraction has failed and should be redesigned rather than patched.

lean/Audit.lean

@@ -1,6 +1,7 @@
 import PSL.Semantics
 import PSL.PVM32Driver
 import PSL.SemanticContinuityRed1
+import PSL.SemanticContinuityGreen1
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
@@ -11,3 +12,7 @@ import PSL.SemanticContinuityRed1
 
 #print axioms PSL.red1_bindings_are_distinct
 #print axioms PSL.red1_capability_gate_is_binding_blind
+
+#print axioms PSL.checkBinding_true_iff
+#print axioms PSL.green1_separates_red1_witness
+#print axioms PSL.green1_checked_binding_is_model_faithful

lean/PSL/SemanticContinuityGreen1.lean

@@ -0,0 +1,148 @@
+import PSL.SemanticContinuityRed1
+
+namespace PSL
+
+/-
+  Semantic Continuity GREEN-1
+  ---------------------------
+
+  RED-1 showed that capability declaration plus successful lowering is blind to
+  whether a supplied target binding is semantically justified.
+
+  GREEN-1 adds the minimum missing object: a target-specific DeviceModel whose
+  resource denotation is independent of the realization binding.
+
+  This closes only the binding-correctness gap. It does NOT yet model value
+  representation, units, protocol state, acknowledgements, persistence,
+  atomicity, timing, or physical-device conformance.
+-/
+
+/--
+A target-specific model of what each concrete resource denotes semantically.
+
+Resource is intentionally abstract here. A PVM32 instance may use Fin 256;
+another hardware generation may use a different resource type.
+
+The target-neutral SemanticScript does not contain a physical resource.
+-/
+structure DeviceModel (Resource : Type) where
+  denotes : Resource → Option SemanticId
+
+/--
+A binding matches a device model when the resource selected for a semantic
+identity is independently modeled as denoting that same identity.
+-/
+def bindingMatchesDevice
+    {Resource : Type}
+    (device : DeviceModel Resource)
+    (resourceOf : SemanticId → Option Resource)
+    (id : SemanticId) : Prop :=
+  match resourceOf id with
+  | none => False
+  | some resource => device.denotes resource = some id
+
+/--
+Executable binding checker.
+
+The realization supplies resourceOf; the device model supplies denotes.
+Acceptance therefore does not trust the realization's mapping by itself.
+-/
+def checkBinding
+    {Resource : Type}
+    (device : DeviceModel Resource)
+    (resourceOf : SemanticId → Option Resource)
+    (id : SemanticId) : Bool :=
+  match resourceOf id with
+  | none => false
+  | some resource => decide (device.denotes resource = some id)
+
+/--
+The executable checker is sound and complete for the binding relation stated
+above. This theorem is generic over the target resource type.
+-/
+theorem checkBinding_true_iff
+    {Resource : Type}
+    (device : DeviceModel Resource)
+    (resourceOf : SemanticId → Option Resource)
+    (id : SemanticId) :
+    checkBinding device resourceOf id = true ↔
+      bindingMatchesDevice device resourceOf id := by
+  unfold checkBinding bindingMatchesDevice
+  cases hresource : resourceOf id <;> simp [hresource]
+
+-- PVM32 witness ---------------------------------------------------------------
+
+/--
+A second semantic identity used to make 0x21 a modeled resource rather than
+merely an unmapped byte. GREEN-1 therefore rejects the adversarial RED-1
+binding because 0x21 denotes a different meaning, not just because it is
+absent from the model.
+-/
+def diagnosticIdentity : SemanticId := ⟨1002⟩
+
+/--
+Minimal target-specific PVM32 device model for the RED-1 witness.
+
+Physical addresses belong here, at the target model boundary, not in
+statusScript or statusIdentity.
+-/
+def pvm32Green1DeviceModel : DeviceModel (Fin 256) :=
+  { denotes := fun resource =>
+      if resource = fin256 0x20 then
+        some statusIdentity
+      else if resource = fin256 0x21 then
+        some diagnosticIdentity
+      else
+        none }
+
+theorem green1_reference_binding_accepts :
+    checkBinding
+      pvm32Green1DeviceModel
+      referencePVM32Bindings.targetOf
+      statusIdentity = true := by
+  native_decide
+
+theorem green1_adversarial_binding_rejects :
+    checkBinding
+      pvm32Green1DeviceModel
+      adversarialPVM32Bindings.targetOf
+      statusIdentity = false := by
+  native_decide
+
+/--
+GREEN-1 closes exactly the counterexample established by RED-1:
+
+* both bindings still pass the old capability-plus-lowering boundary;
+* the independently modeled resource semantics accepts the reference binding;
+* the same checker rejects the adversarial binding.
+
+No physical address was added to the target-neutral semantic script.
+-/
+theorem green1_separates_red1_witness :
+    currentRealizationGate referencePVM32Bindings statusScript = true ∧
+    currentRealizationGate adversarialPVM32Bindings statusScript = true ∧
+    checkBinding
+      pvm32Green1DeviceModel
+      referencePVM32Bindings.targetOf
+      statusIdentity = true ∧
+    checkBinding
+      pvm32Green1DeviceModel
+      adversarialPVM32Bindings.targetOf
+      statusIdentity = false := by
+  native_decide
+
+/--
+Any binding accepted by checkBinding satisfies the stated device-model
+denotation relation. The realization generator itself is not trusted for that
+claim.
+-/
+theorem green1_checked_binding_is_model_faithful
+    {Resource : Type}
+    (device : DeviceModel Resource)
+    (resourceOf : SemanticId → Option Resource)
+    (id : SemanticId)
+    (hcheck : checkBinding device resourceOf id = true) :
+    bindingMatchesDevice device resourceOf id :=
+  (checkBinding_true_iff device resourceOf id).mp hcheck
+
+end PSL

lean/lakefile.lean

@@ -5,4 +5,4 @@ package «PSL»
 
 @[default_target]
 lean_lib «PSL» where
-  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1]