Establish RED-3: protocol-blind realization checking

STATUS.md

@@ -55,7 +55,7 @@ They should not be copied into new semantic-continuity modules.
 
 See `docs/TERMINOLOGY_AUDIT.md`.
 
-## Active formal milestone — GREEN-2
+## Active formal milestone — RED-3
 
 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate.
 
@@ -77,7 +77,13 @@ The composed GREEN-2 gate accepts the reference candidate and rejects the RED-2
 
 See \`docs/research/GREEN2_REPRESENTATION_CHECK.md\`.
 
-Protocol state, ordering, acknowledgements, persistence, and physical-device conformance remain open.
+RED-3 now freezes the GREEN-2-correct resource and raw payload and mutates only the surrounding protocol trace. A machine-checked witness shows that both executions pass GREEN-2 because protocol/state behavior is outside its model.
+
+See \`docs/research/RED3_PROTOCOL_BLINDNESS.md\`.
+
+This establishes the next narrow gap: **binding correctness plus representation correctness is not protocol/state correctness**.
+
+Persistence, timing, and physical-device conformance remain open.
 
 The motivating case is:
 

docs/research/RED3_PROTOCOL_BLINDNESS.md

@@ -0,0 +1,143 @@
+# RED-3 — Protocol-Blind Realization Check
+
+**Branch:** `research/semantic-continuity-red3`  
+**Baseline:** `3b36d61b0d5637ae52f2cd0c646e98f9d28c7054`
+
+## Research question
+
+After GREEN-2, can PSL distinguish two executions that use:
+
+- the same correct semantic binding;
+- the same correct raw representation;
+- but different protocol/state sequences?
+
+At this baseline, the answer is **no**.
+
+## What RED-3 freezes
+
+RED-1 changed the resource.
+
+RED-2 changed the payload.
+
+RED-3 changes neither.
+
+Both executions use the exact same GREEN-2-correct write:
+
+```text
+resource = 0x20
+raw      = 250
+```
+
+The only mutation is the surrounding protocol trace.
+
+Reference trace:
+
+```text
+enter-config
+issue-write
+observe-ACK
+exit-config
+```
+
+Mutated trace:
+
+```text
+issue-write
+observe-ACK
+```
+
+## Machine-checked negative result
+
+`lean/PSL/SemanticContinuityRed3.lean` introduces:
+
+```text
+CandidateExecution(Resource)
+  write
+  trace
+```
+
+and proves:
+
+```text
+reference.write = mutated.write
+reference.trace != mutated.trace
+
+GREEN2(reference) = true
+GREEN2(mutated)   = true
+```
+
+This establishes the next narrow gap:
+
+> **Binding correctness plus representation correctness is not protocol/state correctness.**
+
+## Important claim boundary
+
+RED-3 does **not** yet prove that the reference trace is valid or required, nor
+that the mutated trace is invalid.
+
+The current theory cannot express that relationship.
+
+Those names describe the experiment setup relative to the planned stateful
+device witness. GREEN-3 must introduce enough protocol semantics to make trace
+validity a formal statement rather than a convention.
+
+## Why GREEN-2 accepts both
+
+GREEN-2 checks only:
+
+```text
+semantic identity
+  -> target resource
+
+semantic value
+  -> raw representation
+```
+
+Both executions are identical along those dimensions.
+
+GREEN-2 has no object for:
+
+```text
+initial state
+  -> command
+  -> next state
+  -> observation
+  -> ...
+```
+
+so the trace difference is invisible.
+
+## GREEN-3 obligation
+
+GREEN-3 should add the **minimum** state/transition semantics required to
+distinguish the two traces.
+
+The acceptance target is:
+
+```text
+same resource 0x20
+same raw value 250
+
+reference trace -> ACCEPT
+mutated trace   -> REJECT
+```
+
+without:
+
+- hard-coding one whole trace as a magic accepted list;
+- trusting the realization generator;
+- moving target protocol mechanics into the target-neutral semantic contract;
+- adding persistence or timing before they are required;
+- introducing QEMU/Renode yet.
+
+A likely next object is a small target-specific protocol transition model, but
+RED-3 intentionally does not prescribe the final architecture.
+
+## Kill condition
+
+If protocol correctness can only be established by embedding the entire target
+command sequence into the target-neutral semantic contract, the continuity
+boundary has failed.
+
+The target-neutral intent must remain stable while target protocol machinery
+remains replaceable.

lean/Audit.lean

@@ -4,6 +4,7 @@ import PSL.SemanticContinuityRed1
 import PSL.SemanticContinuityGreen1
 import PSL.SemanticContinuityRed2
 import PSL.SemanticContinuityGreen2
+import PSL.SemanticContinuityRed3
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
@@ -25,3 +26,6 @@ import PSL.SemanticContinuityGreen2
 #print axioms PSL.checkRepresentation_true_iff
 #print axioms PSL.green2_separates_red2_witness
 #print axioms PSL.green2_checked_representation_is_model_faithful
+
+#print axioms PSL.red3_writes_are_identical
+#print axioms PSL.red3_green2_is_protocol_blind

lean/PSL/SemanticContinuityRed3.lean

@@ -0,0 +1,135 @@
+import PSL.SemanticContinuityGreen2
+
+namespace PSL
+
+/-
+  Semantic Continuity RED-3
+  -------------------------
+
+  GREEN-2 established binding correctness and representation correctness.
+  RED-3 asks whether that boundary also establishes protocol/state correctness.
+
+  It does not.
+
+  Two candidate executions may use the same semantically correct resource and
+  the same semantically correct raw representation while presenting different
+  command/state traces. GREEN-2 has no protocol semantics, so both executions
+  pass its strongest current gate.
+
+  This file deliberately does NOT introduce a protocol automaton or execution
+  semantics. It records the next missing relation.
+-/
+
+inductive ProtocolStep where
+  | enterConfig
+  | issueWrite
+  | observeAck
+  | exitConfig
+  deriving Repr, BEq, DecidableEq
+
+structure CandidateExecution (Resource : Type) where
+  write : CandidateWrite Resource
+  trace : List ProtocolStep
+  deriving Repr, BEq, DecidableEq
+
+/--
+Lift the strongest GREEN-2 checker to an execution.
+
+The trace is intentionally ignored because GREEN-2 has no protocol/state model.
+That omission is the property RED-3 is testing.
+-/
+def green2ExecutionGate
+    {Resource SemanticValue : Type}
+    (device : DeviceModel Resource)
+    (representation : RepresentationModel SemanticValue Nat)
+    (semanticId : SemanticId)
+    (semanticValue : SemanticValue)
+    (execution : CandidateExecution Resource) : Bool :=
+  green2CandidateGate
+    device
+    representation
+    semanticId
+    semanticValue
+    execution.write
+
+/--
+Reference execution for the next falsification experiment.
+
+The sequence is only a reference witness at RED-3. The current theory does not
+yet prove that this trace is required or valid.
+-/
+def referenceSetpointExecution : CandidateExecution (Fin 256) :=
+  { write := referenceSetpointWrite
+  , trace :=
+      [ .enterConfig
+      , .issueWrite
+      , .observeAck
+      , .exitConfig ] }
+
+/--
+Mutation that keeps the exact same GREEN-2-correct write but omits the
+configuration-state transitions.
+-/
+def missingConfigExecution : CandidateExecution (Fin 256) :=
+  { write := referenceSetpointWrite
+  , trace :=
+      [ .issueWrite
+      , .observeAck ] }
+
+theorem red3_writes_are_identical :
+    referenceSetpointExecution.write =
+      missingConfigExecution.write := by
+  native_decide
+
+theorem red3_traces_are_distinct :
+    referenceSetpointExecution.trace ≠
+      missingConfigExecution.trace := by
+  native_decide
+
+theorem red3_reference_passes_green2 :
+    green2ExecutionGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      referenceSetpointExecution = true := by
+  native_decide
+
+theorem red3_missing_config_also_passes_green2 :
+    green2ExecutionGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      missingConfigExecution = true := by
+  native_decide
+
+/--
+RED-3 result.
+
+The two executions carry the same GREEN-2-correct write, but their protocol
+traces differ. Since GREEN-2 has no protocol/state semantics, both pass.
+
+The theorem deliberately does not assert which trace is valid. That relation is
+exactly what is missing and what GREEN-3 must add.
+-/
+theorem red3_green2_is_protocol_blind :
+    referenceSetpointExecution.write =
+      missingConfigExecution.write ∧
+    referenceSetpointExecution.trace ≠
+      missingConfigExecution.trace ∧
+    green2ExecutionGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      referenceSetpointExecution = true ∧
+    green2ExecutionGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      missingConfigExecution = true := by
+  native_decide
+
+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, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2, `PSL.SemanticContinuityRed3]