From bfaaa5877beb75a272a885ac3d38dd572939678b Mon Sep 17 00:00:00 2001 From: pravkr <121178833+splashevolution@users.noreply.github.com> Date: Wed, 7 Oct 2026 20:06:22 +0530 Subject: [PATCH] Establish RED-2 representation-blindness counterexample --- STATUS.md | 17 +- .../research/RED2_REPRESENTATION_BLINDNESS.md | 149 ++++++++++++++++++ lean/Audit.lean | 4 + lean/PSL/SemanticContinuityRed2.lean | 128 +++++++++++++++ lean/lakefile.lean | 2 +- 5 files changed, 293 insertions(+), 7 deletions(-) create mode 100644 docs/research/RED2_REPRESENTATION_BLINDNESS.md create mode 100644 lean/PSL/SemanticContinuityRed2.lean diff --git a/STATUS.md b/STATUS.md index ecd98fa..5ce5421 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-1 +## Active formal milestone — RED-2 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate. @@ -65,7 +65,13 @@ See \`docs/research/RED1_DISHONEST_BINDING.md\` and \`docs/research/GREEN1_DEVIC 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 next falsification target is the same physical resource with a wrong representation: +RED-2 now freezes the GREEN-1-correct resource binding and mutates only the target payload. A machine-checked witness shows that both raw values pass the GREEN-1 binding checker because representation is outside its model. + +See \`docs/research/RED2_REPRESENTATION_BLINDNESS.md\`. + +This establishes the next narrow gap: **binding correctness is not representation correctness**. + +The motivating case is: Example: @@ -79,10 +85,9 @@ correct: ACK observed incorrect: - write 25 - wrong resource - wrong unit - missing state transition + encode 25.0 as 25 + correct resource + representation mismatch ``` The new theory should reject incorrect realizations because of behavior, not diff --git a/docs/research/RED2_REPRESENTATION_BLINDNESS.md b/docs/research/RED2_REPRESENTATION_BLINDNESS.md new file mode 100644 index 0000000..8f0fae1 --- /dev/null +++ b/docs/research/RED2_REPRESENTATION_BLINDNESS.md @@ -0,0 +1,149 @@ +# RED-2 — Representation-Blind Binding Check + +**Branch:** `research/semantic-continuity-red2` +**Baseline:** `ebb21af2489e3a05a2fb17f6bb67657f7bba813e` + +## Research question + +After GREEN-1, can PSL distinguish two realizations that use the **same correct +resource binding** but carry **different raw representations**? + +At this baseline, the answer is **no**. + +## Why RED-2 is different from RED-1 + +RED-1 changed the physical resource: + +```text +reference: SemanticId(1001) -> 0x20 +adversarial: SemanticId(1001) -> 0x21 +``` + +GREEN-1 fixed that gap by independently modeling what each target resource +denotes. + +RED-2 holds the resource fixed: + +```text +resource: 0x20 +``` + +and mutates only the target payload: + +```text +reference raw value: 250 +mutated raw value: 25 +``` + +The intended motivating interpretation is a 25.0 °C setpoint on a legacy +fixed-point target, but RED-2 does not yet formalize that interpretation. + +## Machine-checked negative result + +`lean/PSL/SemanticContinuityRed2.lean` introduces a minimal: + +```text +CandidateWrite(Resource) + resource + rawValue +``` + +and proves: + +```text +reference.resource = mutated.resource +reference.rawValue != mutated.rawValue + +GREEN1(reference) = true +GREEN1(mutated) = true +``` + +This is enough to establish the next gap: + +> **Binding correctness is not representation correctness.** + +## Important claim boundary + +RED-2 does **not** prove that raw value `250` is semantically correct or that +`25` is semantically wrong. + +The current theory cannot express that relationship. + +The words "reference" and "wrong-scale" describe the experiment setup relative +to the planned 25.0 °C witness. GREEN-2 must introduce enough representation +semantics to turn that convention into a formal statement. + +## What GREEN-1 can see + +GREEN-1 checks: + +```text +semantic identity + | + v +target resource + | + v +device-model denotation +``` + +For both RED-2 candidates: + +```text +SemanticId(1001) + | + v +0x20 + | + v +SemanticId(1001) +``` + +So both correctly pass. + +## What GREEN-1 cannot see + +It has no relation for: + +```text +semantic value + | + v +target representation + | + v +raw payload +``` + +Therefore changing only the payload is invisible to the checker. + +## GREEN-2 obligation + +GREEN-2 should add the **minimum** semantics required to state and check a +representation relation. + +The acceptance target is: + +```text +same resource 0x20 + +reference representation -> ACCEPT +mutated representation -> REJECT +``` + +without: + +- hard-coding raw value `250` into a supposedly target-neutral contract; +- trusting the realization generator; +- conflating resource binding with representation; +- adding protocol-state machinery before it is required; +- introducing QEMU/Renode yet. + +A likely next object is a target-specific representation model or encoder +relation, but RED-2 intentionally does not prescribe its final shape. + +## Kill condition + +If representation correctness can only be obtained by embedding the target's +raw encoding directly in the semantic contract, then the abstraction boundary +has failed and should be redesigned. diff --git a/lean/Audit.lean b/lean/Audit.lean index 326d5dd..e7011b6 100644 --- a/lean/Audit.lean +++ b/lean/Audit.lean @@ -2,6 +2,7 @@ import PSL.Semantics import PSL.PVM32Driver import PSL.SemanticContinuityRed1 import PSL.SemanticContinuityGreen1 +import PSL.SemanticContinuityRed2 #print axioms validateIRClosed_sound #print axioms validateWords_execution @@ -16,3 +17,6 @@ import PSL.SemanticContinuityGreen1 #print axioms PSL.checkBinding_true_iff #print axioms PSL.green1_separates_red1_witness #print axioms PSL.green1_checked_binding_is_model_faithful + +#print axioms PSL.red2_same_resource +#print axioms PSL.red2_green1_is_representation_blind diff --git a/lean/PSL/SemanticContinuityRed2.lean b/lean/PSL/SemanticContinuityRed2.lean new file mode 100644 index 0000000..1f7edb6 --- /dev/null +++ b/lean/PSL/SemanticContinuityRed2.lean @@ -0,0 +1,128 @@ +import PSL.SemanticContinuityGreen1 + +namespace PSL + +/- + Semantic Continuity RED-2 + ------------------------- + + GREEN-1 established binding correctness relative to an independently stated + DeviceModel. + + RED-2 asks whether that boundary also establishes representation correctness. + + It does not. + + Two candidate writes may select the same semantically correct resource while + carrying different raw payloads. The GREEN-1 checker inspects only the + resource binding, so both candidates pass. + + This file deliberately does NOT introduce representation semantics. It + records the next missing relation. +-/ + +/-- +A minimal target-side write candidate used only for RED-2. + +The resource and raw payload are separated explicitly so the theorem can show +which field GREEN-1 observes and which field it ignores. +-/ +structure CandidateWrite (Resource : Type) where + resource : Resource + rawValue : Nat + deriving Repr, BEq, DecidableEq + +/-- +Turn one concrete candidate into the single semantic binding needed by the +GREEN-1 checker. + +The raw payload is intentionally absent because GREEN-1 has no representation +semantics. +-/ +def CandidateWrite.resourceOf + {Resource : Type} + (semanticId : SemanticId) + (candidate : CandidateWrite Resource) : + SemanticId → Option Resource := + fun id => if id == semanticId then some candidate.resource else none + +/-- +The strongest GREEN-1 gate available for one explicit write candidate: +binding agreement with the independently stated device model. +-/ +def green1CandidateGate + {Resource : Type} + (device : DeviceModel Resource) + (semanticId : SemanticId) + (candidate : CandidateWrite Resource) : Bool := + checkBinding + device + (candidate.resourceOf semanticId) + semanticId + +/-- +Reference encoding for the next falsification experiment. + +At RED-2 this is only an experimental reference payload. The current theory +does not yet state why 250 represents the desired semantic value. +-/ +def referenceSetpointWrite : CandidateWrite (Fin 256) := + { resource := fin256 0x20 + , rawValue := 250 } + +/-- +Wrong-scale mutation of the same target resource. + +Again, RED-2 does not yet prove that 25 is semantically wrong. It proves that +GREEN-1 cannot distinguish it from the reference payload. +-/ +def wrongScaleSetpointWrite : CandidateWrite (Fin 256) := + { resource := fin256 0x20 + , rawValue := 25 } + +theorem red2_same_resource : + referenceSetpointWrite.resource = + wrongScaleSetpointWrite.resource := by + native_decide + +theorem red2_payloads_are_distinct : + referenceSetpointWrite.rawValue ≠ + wrongScaleSetpointWrite.rawValue := by + native_decide + +theorem red2_reference_passes_green1 : + green1CandidateGate + pvm32Green1DeviceModel + statusIdentity + referenceSetpointWrite = true := by + native_decide + +theorem red2_wrong_scale_also_passes_green1 : + green1CandidateGate + pvm32Green1DeviceModel + statusIdentity + wrongScaleSetpointWrite = true := by + native_decide + +/-- +RED-2 result. + +The two candidates select the same resource and therefore both satisfy the +GREEN-1 binding relation, even though their raw payloads differ. + +The theorem deliberately does not claim which payload realizes the intended +semantic value. That relation is exactly what is missing. +-/ +theorem red2_green1_is_representation_blind : + referenceSetpointWrite.rawValue ≠ wrongScaleSetpointWrite.rawValue ∧ + green1CandidateGate + pvm32Green1DeviceModel + statusIdentity + referenceSetpointWrite = true ∧ + green1CandidateGate + pvm32Green1DeviceModel + statusIdentity + wrongScaleSetpointWrite = true := by + native_decide + +end PSL diff --git a/lean/lakefile.lean b/lean/lakefile.lean index a7a8b42..7566b91 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] + roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2]