From 70dbbe3806d001f12ef8b3bb5e1f09f6d7fe8c8b Mon Sep 17 00:00:00 2001 From: pravkr <121178833+splashevolution@users.noreply.github.com> Date: Wed, 7 Oct 2026 19:25:43 +0530 Subject: [PATCH] Establish RED-1 binding-blind realization counterexample --- STATUS.md | 14 ++- docs/research/RED1_DISHONEST_BINDING.md | 161 ++++++++++++++++++++++++ lean/Audit.lean | 4 + lean/PSL/SemanticContinuityRed1.lean | 79 ++++++++++++ lean/lakefile.lean | 2 +- 5 files changed, 255 insertions(+), 5 deletions(-) create mode 100644 docs/research/RED1_DISHONEST_BINDING.md create mode 100644 lean/PSL/SemanticContinuityRed1.lean diff --git a/STATUS.md b/STATUS.md index 2e76c89..0269510 100644 --- a/STATUS.md +++ b/STATUS.md @@ -55,11 +55,17 @@ They should not be copied into new semantic-continuity modules. See `docs/TERMINOLOGY_AUDIT.md`. -## Next formal milestone +## Active formal milestone — RED-1 -The next research milestone should establish a RED case where the current -system cannot distinguish a declared capability from a semantically correct -realization. +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. + +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. + +See \`docs/research/RED1_DISHONEST_BINDING.md\`. + +The next GREEN step must distinguish correct from adversarial realization without hard-coding a physical address into the target-neutral semantic contract. + +The motivating case remains: Example: diff --git a/docs/research/RED1_DISHONEST_BINDING.md b/docs/research/RED1_DISHONEST_BINDING.md new file mode 100644 index 0000000..03fcfd2 --- /dev/null +++ b/docs/research/RED1_DISHONEST_BINDING.md @@ -0,0 +1,161 @@ +# RED-1 — Binding-Blind Realization Gate + +**Branch:** `research/semantic-continuity-red1` +**Baseline:** `7317e0a6a1bb8c888dd52f1feed2c23074b4938e` + +## Research question + +Can the current PSL realization boundary distinguish a target that merely +provides a usable binding from a target binding that is semantically justified? + +The answer at this baseline is **no**. + +This is the first controlled RED result for the semantic-continuity research +line. + +## Existing mechanism + +The current PVM32 path has two independent pieces: + +```text +DriverContract.supports + │ + ▼ +required capability gate + +PVM32Bindings.targetOf + │ + ▼ +target-specific lowering +``` + +For `statusScript`, the reference mapping is: + +```text +SemanticId(1001) -> 0x20 +``` + +Nothing in the current formal model states why `0x20` is the semantically +correct resource. + +## Adversarial witness + +RED-1 introduces a second binding: + +```text +SemanticId(1001) -> 0x21 +``` + +The two mappings are different. + +Yet both: + +1. satisfy the same capability declaration; +2. provide a target for lowering; +3. produce a valid PVM32 word stream. + +The resulting words differ: + +```text +reference: 0x200520F0 +adversarial: 0x200521F0 +``` + +The current architecture has no formal object that can say which target +behavior actually realizes the semantic identity. + +## Machine-checked negative result + +`lean/PSL/SemanticContinuityRed1.lean` proves: + +```text +reference binding ≠ adversarial binding + +currentRealizationGate(reference, statusScript) = true +currentRealizationGate(adversarial, statusScript) = true + +lower(reference, statusScript) ≠ +lower(adversarial, statusScript) +``` + +This keeps ordinary CI green while proving a negative fact about the current +design. + +RED here means **the desired research property is false of the current +architecture**, not that the repository intentionally fails to build. + +## Claim boundary + +This experiment deliberately does **not** prove that physical address +`0x20` is correct and `0x21` is wrong. + +That distinction cannot yet be represented. + +Calling `0x21` adversarial is relative to the repository's existing +reference binding. GREEN-1 must introduce enough target semantics to make +correctness a formal statement rather than a convention. + +## Why this matters + +A boolean declaration such as: + +```text +supports(write) = true +``` + +can establish only that an operation class is declared available. + +It cannot establish: + +```text +semantic identity + ↓ +correct target resource + ↓ +correct target behavior +``` + +Therefore: + +> **Capability declaration is not realization correctness.** + +That statement is now backed by a checked counterexample in the repository. + +## GREEN-1 obligation + +GREEN-1 should introduce the **minimum** theory needed to make the reference +and adversarial cases distinguishable. + +Candidate objects are: + +```text +DeviceModel +Realization +RealizationEvidence +RealizationChecker +Observation +``` + +But GREEN-1 should not add all of them merely because they appear in the +research charter. We should add only what the proof requires. + +The acceptance target is: + +```text +reference realization -> ACCEPT +adversarial realization -> REJECT +``` + +without: + +- placing target address `0x20` inside the target-neutral semantic contract; +- trusting the realization generator; +- modifying the historical PVM32 semantics to make the test pass; +- introducing QEMU/Renode yet; +- making a claim about physical hardware. + +## Kill condition + +If rejecting the adversarial binding requires hard-coding the expected +physical address into the semantic contract, then the proposed continuity +boundary has failed its first abstraction test. diff --git a/lean/Audit.lean b/lean/Audit.lean index 5cce91c..eb9efe3 100644 --- a/lean/Audit.lean +++ b/lean/Audit.lean @@ -1,5 +1,6 @@ import PSL.Semantics import PSL.PVM32Driver +import PSL.SemanticContinuityRed1 #print axioms validateIRClosed_sound #print axioms validateWords_execution @@ -7,3 +8,6 @@ import PSL.PVM32Driver #print axioms valid_program_executes #print axioms certified_ir_executes #print axioms PSL.status_script_realizes_on_pvm32 + +#print axioms PSL.red1_bindings_are_distinct +#print axioms PSL.red1_capability_gate_is_binding_blind diff --git a/lean/PSL/SemanticContinuityRed1.lean b/lean/PSL/SemanticContinuityRed1.lean new file mode 100644 index 0000000..01a68dd --- /dev/null +++ b/lean/PSL/SemanticContinuityRed1.lean @@ -0,0 +1,79 @@ +import PSL.PVM32Driver + +namespace PSL + +/- + Semantic Continuity RED-1 + ------------------------- + + Purpose: + exhibit a machine-checked counterexample to the idea that the current + capability gate establishes realization correctness. + + The existing model can check whether a script requires WRITE and whether the + PVM32 driver declares WRITE support. It can also lower any supplied + SemanticId -> target-byte binding. + + What it cannot express is why one supplied binding is semantically faithful + and another is not. + + This file deliberately does NOT introduce the missing device model or + realization-proof machinery. It records the gap we want GREEN-1 to close. +-/ + +/-- An adversarial alternative to the existing reference binding. + +Both bindings are total enough for statusScript to lower. The current core has +no semantic relation capable of preferring 0x20 over 0x21. +-/ +def adversarialPVM32Bindings : PVM32Bindings := + { targetOf := fun id => + if id == statusIdentity then some (fin256 0x21) else none } + +/-- +Characterize the acceptance boundary that exists today: + 1. the driver declares the script's required capabilities, and + 2. lowering succeeds for the supplied target binding. + +This is an observation of the current architecture, not the desired future +definition of realization correctness. +-/ +def currentRealizationGate + (bindings : PVM32Bindings) (script : SemanticScript) : Bool := + pvm32Driver.acceptsScript script && + (pvm32LowerScript? bindings script).isSome + +theorem red1_bindings_are_distinct : + referencePVM32Bindings.targetOf statusIdentity ≠ + adversarialPVM32Bindings.targetOf statusIdentity := by + native_decide + +theorem red1_reference_binding_lowers : + pvm32Words? referencePVM32Bindings statusScript = + some [0x200520F0] := by + native_decide + +theorem red1_adversarial_binding_also_lowers : + pvm32Words? adversarialPVM32Bindings statusScript = + some [0x200521F0] := by + native_decide + +/-- +RED-1 result. + +Two distinct target bindings for the same semantic script both pass the entire +acceptance boundary available today, even though they produce different target +programs. + +The theorem does NOT assert which target byte is physically correct. That fact +cannot be stated in the current model. The inability to state and check that +relationship is exactly the research gap. +-/ +theorem red1_capability_gate_is_binding_blind : + currentRealizationGate referencePVM32Bindings statusScript = true ∧ + currentRealizationGate adversarialPVM32Bindings statusScript = true ∧ + pvm32Words? referencePVM32Bindings statusScript ≠ + pvm32Words? adversarialPVM32Bindings statusScript := by + native_decide + +end PSL diff --git a/lean/lakefile.lean b/lean/lakefile.lean index 3c6eff5..7cd0281 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] + roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1]