From ac3a06bf61aae067a4d80d520f7a891129274264 Mon Sep 17 00:00:00 2001 From: pravkr <121178833+splashevolution@users.noreply.github.com> Date: Wed, 7 Oct 2026 21:19:31 +0530 Subject: [PATCH] Establish RED-4 observation-blindness counterexample --- STATUS.md | 12 +- docs/research/RED4_OBSERVATION_BLINDNESS.md | 147 +++++++++++++++++++ lean/Audit.lean | 4 + lean/PSL/SemanticContinuityRed4.lean | 151 ++++++++++++++++++++ lean/lakefile.lean | 2 +- 5 files changed, 313 insertions(+), 3 deletions(-) create mode 100644 docs/research/RED4_OBSERVATION_BLINDNESS.md create mode 100644 lean/PSL/SemanticContinuityRed4.lean diff --git a/STATUS.md b/STATUS.md index 3f7eefa..77d70ce 100644 --- a/STATUS.md +++ b/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-3 +## Active formal milestone — RED-4 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate. @@ -87,7 +87,15 @@ GREEN-3 adds a generic target-specific \`ProtocolModel(State, Step)\` with an ex See \`docs/research/GREEN3_PROTOCOL_TRANSITION_CHECK.md\`. -This closes the RED-3 protocol-sequencing gap relative to the stated model. Concrete observations/effects, persistence, timing, and simulator/physical-device conformance remain open. +This closes the RED-3 protocol-sequencing gap relative to the stated model. + +RED-4 now freezes the GREEN-3-valid binding, representation, and protocol execution and mutates only the post-execution observation. A machine-checked witness shows that both outcomes pass GREEN-3 because observed semantic effect is outside its model. + +See \`docs/research/RED4_OBSERVATION_BLINDNESS.md\`. + +This establishes the next narrow gap: **a valid modeled realization is not the same thing as an observed semantic effect**. + +Observation provenance, payload-to-trace linkage, persistence, timing, and simulator/physical-device conformance remain open. The motivating case is: diff --git a/docs/research/RED4_OBSERVATION_BLINDNESS.md b/docs/research/RED4_OBSERVATION_BLINDNESS.md new file mode 100644 index 0000000..b34233a --- /dev/null +++ b/docs/research/RED4_OBSERVATION_BLINDNESS.md @@ -0,0 +1,147 @@ +# RED-4 — Observation-Blind Realization Check + +**Branch:** `research/semantic-continuity-red4` +**Baseline:** `fdba805e5d58113622851c52f68e96735d83c5d1` + +## Research question + +After GREEN-3, can PSL distinguish two outcomes that contain the **same valid +modeled execution** but differ in whether the intended effect was observed? + +At this baseline, the answer is **no**. + +## What RED-4 freezes + +RED-1 changed the resource. + +RED-2 changed the representation. + +RED-3 changed the protocol trace. + +RED-4 changes none of those. + +Both outcomes contain the exact same GREEN-3-valid execution: + +```text +resource = 0x20 +raw write = 250 +protocol trace = enter-config + issue-write + observe-ACK + exit-config +``` + +The only mutation is the post-execution observation: + +```text +reference observation = some 250 +mutated observation = none +``` + +## Machine-checked negative result + +`lean/PSL/SemanticContinuityRed4.lean` introduces: + +```text +CandidateOutcome(Resource, RawObservation) + execution + observation +``` + +and proves: + +```text +reference.execution = mutated.execution +reference.observation != mutated.observation + +GREEN3(reference) = true +GREEN3(mutated) = true +``` + +This establishes the next narrow gap: + +> **A valid modeled realization is not the same thing as an observed semantic effect.** + +## Important claim boundary + +RED-4 does **not** yet prove that raw observation `250` demonstrates the +intended semantic effect. + +At this stage `some 250` is only the reference fixture for the next +falsification step. + +The current theory has no independent relation connecting: + +```text +semantic intent + -> +executed realization + -> +observable target state +``` + +That missing relation is the RED-4 result. + +## Why GREEN-3 accepts both + +GREEN-3 checks: + +```text +semantic identity + -> target resource + +semantic value + -> target representation + +target trace + -> protocol transition model +``` + +The two RED-4 outcomes are identical on all three dimensions. + +GREEN-3 never inspects the post-execution observation, so absence of an +observation is invisible to it. + +## GREEN-4 obligation + +GREEN-4 should add the **minimum** observation/effect semantics required to +distinguish the outcomes. + +The acceptance target is: + +```text +same binding +same representation +same valid protocol trace + +reference observed effect -> ACCEPT +missing observed effect -> REJECT +``` + +without: + +- trusting a realization-generated success flag; +- treating ACK alone as proof of semantic effect; +- embedding PVM32 observation details into the target-neutral semantic intent; +- claiming simulator or physical-device conformance prematurely. + +A likely next object is an independent target-specific observation model that +relates concrete observable state back to the semantic value. + +## Still-open boundary + +GREEN-3's abstract `issueWrite` protocol marker is not yet parameterized by +the concrete payload. Resource/representation correctness and protocol +correctness are checked separately. + +RED-4 does not silently solve that issue. It remains an explicit future attack +surface alongside observation provenance, persistence, timing, and target +conformance. + +## Kill condition + +If proof of semantic effect requires target-specific observations to be copied +into the target-neutral contract, the continuity boundary has failed. + +The semantic contract should state the intended effect; target-specific +observation semantics should justify that effect independently. diff --git a/lean/Audit.lean b/lean/Audit.lean index 30be28c..32fb7d8 100644 --- a/lean/Audit.lean +++ b/lean/Audit.lean @@ -6,6 +6,7 @@ import PSL.SemanticContinuityRed2 import PSL.SemanticContinuityGreen2 import PSL.SemanticContinuityRed3 import PSL.SemanticContinuityGreen3 +import PSL.SemanticContinuityRed4 #print axioms validateIRClosed_sound #print axioms validateWords_execution @@ -34,3 +35,6 @@ import PSL.SemanticContinuityGreen3 #print axioms PSL.checkProtocol_true_iff #print axioms PSL.green3_separates_red3_witness #print axioms PSL.green3_checked_protocol_is_model_faithful + +#print axioms PSL.red4_executions_are_identical +#print axioms PSL.red4_green3_is_observation_blind diff --git a/lean/PSL/SemanticContinuityRed4.lean b/lean/PSL/SemanticContinuityRed4.lean new file mode 100644 index 0000000..6f38cb3 --- /dev/null +++ b/lean/PSL/SemanticContinuityRed4.lean @@ -0,0 +1,151 @@ +import PSL.SemanticContinuityGreen3 + +namespace PSL + +/- + Semantic Continuity RED-4 + ------------------------- + + GREEN-3 established: + * binding correctness relative to a DeviceModel, + * representation correctness relative to a RepresentationModel, and + * protocol-sequence correctness relative to a ProtocolModel. + + RED-4 asks whether that is enough to establish that the intended device + effect was actually observed. + + It is not. + + Two candidate outcomes may contain the exact same GREEN-3-valid execution + while differing only in externally reported observation. GREEN-3 has no + observation/effect relation, so both outcomes pass its strongest current + gate. + + This file deliberately does NOT introduce observation semantics. It records + the next missing relation. +-/ + +/-- +A minimal post-execution outcome. + +The execution is the object already checked by GREEN-3. The observation is kept +separate so RED-4 can show that GREEN-3 does not inspect it. + +RawObservation is generic because different targets may expose different +observable state. +-/ +structure CandidateOutcome (Resource RawObservation : Type) where + execution : CandidateExecution Resource + observation : Option RawObservation + deriving Repr, BEq, DecidableEq + +/-- +Lift the strongest GREEN-3 gate to an outcome. + +The observation is intentionally ignored because GREEN-3 has no observation or +effect model. That omission is the property RED-4 is testing. +-/ +def green3OutcomeGate + {Resource SemanticValue State Step RawObservation : Type} + (device : DeviceModel Resource) + (representation : RepresentationModel SemanticValue Nat) + (protocol : ProtocolModel State Step) + (semanticId : SemanticId) + (semanticValue : SemanticValue) + (traceOf : CandidateExecution Resource → List Step) + (outcome : CandidateOutcome Resource RawObservation) : Bool := + green3ExecutionGate + device + representation + protocol + semanticId + semanticValue + outcome.execution + traceOf + +/-- +Reference outcome for the RED-4 witness. + +The raw observation 250 is only an experiment fixture at RED-4. The current +theory does not yet state why this observation demonstrates the intended +semantic effect. +-/ +def referenceObservedOutcome : CandidateOutcome (Fin 256) Nat := + { execution := referenceSetpointExecution + , observation := some 250 } + +/-- +Mutation that keeps the exact same GREEN-3-valid execution but provides no +post-execution observation. +-/ +def missingObservationOutcome : CandidateOutcome (Fin 256) Nat := + { execution := referenceSetpointExecution + , observation := none } + +theorem red4_executions_are_identical : + referenceObservedOutcome.execution = + missingObservationOutcome.execution := by + native_decide + +theorem red4_observations_are_distinct : + referenceObservedOutcome.observation ≠ + missingObservationOutcome.observation := by + native_decide + +theorem red4_reference_outcome_passes_green3 : + green3OutcomeGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + red3ProtocolTrace + referenceObservedOutcome = true := by + native_decide + +theorem red4_missing_observation_also_passes_green3 : + green3OutcomeGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + red3ProtocolTrace + missingObservationOutcome = true := by + native_decide + +/-- +RED-4 result. + +The two outcomes contain the same GREEN-3-valid execution but differ in +post-execution observation. Since GREEN-3 has no observation/effect semantics, +both pass. + +The theorem deliberately does not assert that raw 250 proves the intended +semantic effect. That relation is exactly what is missing and what GREEN-4 must +add. +-/ +theorem red4_green3_is_observation_blind : + referenceObservedOutcome.execution = + missingObservationOutcome.execution ∧ + referenceObservedOutcome.observation ≠ + missingObservationOutcome.observation ∧ + green3OutcomeGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + red3ProtocolTrace + referenceObservedOutcome = true ∧ + green3OutcomeGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + red3ProtocolTrace + missingObservationOutcome = true := by + native_decide + +end PSL diff --git a/lean/lakefile.lean b/lean/lakefile.lean index 8f4b0e1..1566de3 100644 --- a/lean/lakefile.lean +++ b/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, `PSL.SemanticContinuityRed3, `PSL.SemanticContinuityGreen3] + roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2, `PSL.SemanticContinuityRed3, `PSL.SemanticContinuityGreen3, `PSL.SemanticContinuityRed4]