From 27e2064858508fcc8459c840502d86ff66d5920d Mon Sep 17 00:00:00 2001 From: pravkr <121178833+splashevolution@users.noreply.github.com> Date: Wed, 7 Oct 2026 19:58:28 +0530 Subject: [PATCH] Close GREEN-1 with an independent device binding checker --- STATUS.md | 12 +- docs/research/GREEN1_DEVICE_BINDING_CHECK.md | 180 +++++++++++++++++++ lean/Audit.lean | 5 + lean/PSL/SemanticContinuityGreen1.lean | 148 +++++++++++++++ lean/lakefile.lean | 2 +- 5 files changed, 340 insertions(+), 7 deletions(-) create mode 100644 docs/research/GREEN1_DEVICE_BINDING_CHECK.md create mode 100644 lean/PSL/SemanticContinuityGreen1.lean diff --git a/STATUS.md b/STATUS.md index 0269510..ecd98fa 100644 --- a/STATUS.md +++ b/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: diff --git a/docs/research/GREEN1_DEVICE_BINDING_CHECK.md b/docs/research/GREEN1_DEVICE_BINDING_CHECK.md new file mode 100644 index 0000000..4b5e4ac --- /dev/null +++ b/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. diff --git a/lean/Audit.lean b/lean/Audit.lean index eb9efe3..326d5dd 100644 --- a/lean/Audit.lean +++ b/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 diff --git a/lean/PSL/SemanticContinuityGreen1.lean b/lean/PSL/SemanticContinuityGreen1.lean new file mode 100644 index 0000000..f03b3a3 --- /dev/null +++ b/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 diff --git a/lean/lakefile.lean b/lean/lakefile.lean index 7cd0281..a7a8b42 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] + roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1]