diff --git a/STATUS.md b/STATUS.md index ae3a1f7..3f7eefa 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 — RED-3 +## Active formal milestone — GREEN-3 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate. @@ -83,7 +83,11 @@ 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. +GREEN-3 adds a generic target-specific \`ProtocolModel(State, Step)\` with an executable state-transition checker. The PVM32 witness is a fail-closed state machine rather than a comparison against one magic trace. It accepts the reference configuration/write/ACK/exit sequence and rejects the RED-3 missing-configuration sequence. + +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. The motivating case is: diff --git a/docs/research/GREEN3_PROTOCOL_TRANSITION_CHECK.md b/docs/research/GREEN3_PROTOCOL_TRANSITION_CHECK.md new file mode 100644 index 0000000..d2af8ab --- /dev/null +++ b/docs/research/GREEN3_PROTOCOL_TRANSITION_CHECK.md @@ -0,0 +1,159 @@ +# GREEN-3 — Target-Specific Protocol Transition Check + +**Branch:** `research/semantic-continuity-green3` +**Baseline:** `beef97449d50f10aea97d7556450501f5d377d3e` + +## Result + +GREEN-3 closes the exact protocol/state gap demonstrated by RED-3. + +RED-3 established that two executions can share: + +```text +resource = 0x20 +raw = 250 +``` + +while differing only in protocol trace, and GREEN-2 still accepts both. + +GREEN-3 adds one missing formal object: + +```text +ProtocolModel(State, Step) + initial + transition + accepting +``` + +plus an executable checker: + +```text +checkProtocol(model, trace) +``` + +## Why this is not a magic accepted list + +The PVM32 witness does not compare a trace to one hard-coded sequence. + +It defines target-specific transitions: + +```text +operational --enter-config--> config +config --issue-write--> awaiting-ACK +awaiting-ACK --observe-ACK--> config +config --exit-config--> operational +``` + +All other transitions fail closed. + +Acceptance is determined by executing the trace through that state machine and +ending in an accepting state. + +## Machine-checked result + +`lean/PSL/SemanticContinuityGreen3.lean` proves: + +```text +GREEN2(reference) = true +GREEN2(mutated) = true + +Protocol(reference) = true +Protocol(mutated) = false + +GREEN3(reference) = true +GREEN3(mutated) = false +``` + +The generic theorem is: + +```text +checkProtocol(model, trace) = true + <-> +protocolAccepts(model, trace) +``` + +So the executable checker is sound and complete for the transition relation +GREEN-3 actually states. + +## Separation of concerns + +The current target boundary now has three independent obligations: + +```text +semantic identity + -> DeviceModel + -> target resource + +semantic value + -> RepresentationModel + -> raw payload + +target execution + -> ProtocolModel + -> valid state transitions +``` + +The target-neutral semantic quantity still contains no PVM32 address, fixed +point scale, or protocol state. + +## Claim boundary + +GREEN-3 proves protocol-sequence correctness **relative to the stated protocol +model**. + +It does not yet prove that: + +- an ACK was emitted by a real or simulated device; +- the written value persisted; +- timing constraints were met; +- an external observation confirms the semantic effect; +- the protocol model matches firmware or physical hardware. + +Also, the RED-3 `ProtocolStep.issueWrite` marker is still abstract. GREEN-3 +checks the candidate write separately through GREEN-2 and checks the protocol +trace separately; it does not yet prove that a concrete trace event carries +that exact payload. + +That is a real remaining boundary, not hidden by this milestone. + +## Why this remains minimal + +RED-3 required only state-transition semantics. + +GREEN-3 therefore does not yet introduce: + +- physical or simulator I/O; +- wall-clock timing; +- persistence models; +- trace certificates; +- QEMU or Renode; +- hardware conformance claims. + +Those should be justified by later counterexamples, not added pre-emptively. + +## Next falsification direction + +The next useful RED should attack the boundary between a valid modeled trace +and an actual observable effect. + +One candidate is: + +```text +valid protocol trace +correct resource +correct representation +ACK marker present + +but no modeled observation that the intended device state changed +``` + +That would test whether PSL now needs an explicit observation/effect relation +rather than another static checker. + +## Kill condition retained + +If protocol correctness requires the target-specific transition sequence to be +embedded in the target-neutral semantic contract, the continuity boundary has +failed. + +GREEN-3 avoids that: protocol machinery remains target-specific. diff --git a/lean/Audit.lean b/lean/Audit.lean index a95d919..30be28c 100644 --- a/lean/Audit.lean +++ b/lean/Audit.lean @@ -5,6 +5,7 @@ import PSL.SemanticContinuityGreen1 import PSL.SemanticContinuityRed2 import PSL.SemanticContinuityGreen2 import PSL.SemanticContinuityRed3 +import PSL.SemanticContinuityGreen3 #print axioms validateIRClosed_sound #print axioms validateWords_execution @@ -29,3 +30,7 @@ import PSL.SemanticContinuityRed3 #print axioms PSL.red3_writes_are_identical #print axioms PSL.red3_green2_is_protocol_blind + +#print axioms PSL.checkProtocol_true_iff +#print axioms PSL.green3_separates_red3_witness +#print axioms PSL.green3_checked_protocol_is_model_faithful diff --git a/lean/PSL/SemanticContinuityGreen3.lean b/lean/PSL/SemanticContinuityGreen3.lean new file mode 100644 index 0000000..044acd4 --- /dev/null +++ b/lean/PSL/SemanticContinuityGreen3.lean @@ -0,0 +1,217 @@ +import PSL.SemanticContinuityRed3 + +namespace PSL + +/- + Semantic Continuity GREEN-3 + --------------------------- + + RED-3 showed that GREEN-2 is blind to protocol/state behavior: two candidate + executions can carry the same correct resource and representation while + differing only in their surrounding command trace. + + GREEN-3 adds the minimum missing relation: a target-specific transition model + plus an executable trace checker. + + This closes only the RED-3 protocol-sequencing gap relative to the stated + model. It does NOT yet establish persistence, timing, concrete I/O + observations, simulator conformance, or physical-device conformance. +-/ + +/-- +A target-specific protocol transition model. + +The semantic contract does not contain these target states or transitions. +Different hardware generations may supply different State and Step types while +the target-neutral intent remains unchanged. +-/ +structure ProtocolModel (State Step : Type) where + initial : State + transition : State → Step → Option State + accepting : State → Bool + +/-- Execute a protocol trace from an explicit state. -/ +def runProtocol + {State Step : Type} + (model : ProtocolModel State Step) : + State → List Step → Option State + | state, [] => some state + | state, event :: rest => + match model.transition state event with + | none => none + | some next => runProtocol model next rest + +/-- +Formal acceptance relation for the target protocol model. + +A trace is accepted when all transitions are defined and the resulting state +is marked accepting. +-/ +def protocolAccepts + {State Step : Type} + (model : ProtocolModel State Step) + (trace : List Step) : Prop := + match runProtocol model model.initial trace with + | none => False + | some finalState => model.accepting finalState = true + +/-- Executable protocol checker. -/ +def checkProtocol + {State Step : Type} + (model : ProtocolModel State Step) + (trace : List Step) : Bool := + match runProtocol model model.initial trace with + | none => false + | some finalState => model.accepting finalState + +/-- +The executable checker is sound and complete for the protocol relation that +GREEN-3 actually states. +-/ +theorem checkProtocol_true_iff + {State Step : Type} + (model : ProtocolModel State Step) + (trace : List Step) : + checkProtocol model trace = true ↔ + protocolAccepts model trace := by + unfold checkProtocol protocolAccepts + cases hrun : runProtocol model model.initial trace with + | none => simp [hrun] + | some finalState => simp [hrun] + +-- PVM32 witness --------------------------------------------------------------- + +/-- +Minimal target-specific states needed to close the RED-3 witness. + +These states belong to the target protocol model, not to the target-neutral +semantic quantity or semantic identity. +-/ +inductive PVM32ProtocolState where + | operational + | config + | awaitingAck + deriving Repr, BEq, DecidableEq + +/-- +State-machine semantics for the RED-3 witness. + +This is intentionally a transition relation, not a hard-coded comparison +against one accepted trace: + + operational --enterConfig--> config + config --issueWrite--> awaitingAck + awaitingAck --observeAck--> config + config --exitConfig--> operational + +Every other transition fails closed. +-/ +def pvm32SetpointProtocol : + ProtocolModel PVM32ProtocolState ProtocolStep := + { initial := .operational + , transition := fun state event => + match state, event with + | .operational, .enterConfig => some .config + | .config, .issueWrite => some .awaitingAck + | .awaitingAck, .observeAck => some .config + | .config, .exitConfig => some .operational + | _, _ => none + , accepting := fun state => + match state with + | .operational => true + | _ => false } + +/-- +Compose GREEN-2 resource/representation checking with GREEN-3 protocol +checking. The obligations remain separate. +-/ +def green3ExecutionGate + {Resource SemanticValue State Step : Type} + (device : DeviceModel Resource) + (representation : RepresentationModel SemanticValue Nat) + (protocol : ProtocolModel State Step) + (semanticId : SemanticId) + (semanticValue : SemanticValue) + (execution : CandidateExecution Resource) + (traceOf : CandidateExecution Resource → List Step) : Bool := + green2ExecutionGate + device + representation + semanticId + semanticValue + execution && + checkProtocol protocol (traceOf execution) + +/-- +Specialized trace projection for the RED-3 witness. +-/ +def red3ProtocolTrace + (execution : CandidateExecution (Fin 256)) : List ProtocolStep := + execution.trace + +theorem green3_reference_protocol_accepts : + checkProtocol + pvm32SetpointProtocol + referenceSetpointExecution.trace = true := by + native_decide + +theorem green3_missing_config_protocol_rejects : + checkProtocol + pvm32SetpointProtocol + missingConfigExecution.trace = false := by + native_decide + +/-- +GREEN-3 closes exactly the RED-3 counterexample: + +* both executions still carry the same GREEN-2-correct write; +* GREEN-2 therefore accepts both; +* the target transition model accepts the reference trace; +* the same model rejects the missing-configuration trace. +-/ +theorem green3_separates_red3_witness : + referenceSetpointExecution.write = + missingConfigExecution.write ∧ + green2ExecutionGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + statusIdentity + setpoint25C + referenceSetpointExecution = true ∧ + green2ExecutionGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + statusIdentity + setpoint25C + missingConfigExecution = true ∧ + green3ExecutionGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + referenceSetpointExecution + red3ProtocolTrace = true ∧ + green3ExecutionGate + pvm32Green1DeviceModel + pvm32SetpointRepresentation + pvm32SetpointProtocol + statusIdentity + setpoint25C + missingConfigExecution + red3ProtocolTrace = false := by + native_decide + +/-- +Any trace accepted by checkProtocol satisfies the stated target transition +relation. The realization generator itself is not trusted for that claim. +-/ +theorem green3_checked_protocol_is_model_faithful + {State Step : Type} + (model : ProtocolModel State Step) + (trace : List Step) + (hcheck : checkProtocol model trace = true) : + protocolAccepts model trace := + (checkProtocol_true_iff model trace).mp hcheck + +end PSL diff --git a/lean/lakefile.lean b/lean/lakefile.lean index 83f78b9..8f4b0e1 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] + roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2, `PSL.SemanticContinuityRed3, `PSL.SemanticContinuityGreen3]