Contract
What must remain true.
Inputs, observations, preconditions, postconditions, authority, persistence, atomicity, and allowed failure behavior.
meaning ≠ target encoding
Open formal-systems research
Software intent should
outlive hardware.
PSL investigates whether a stable semantic contract can survive materially different hardware generations while target realizations are independently checked and incompatible targets fail closed.
Research prototype
Lean 4
CI-backed baseline
Virtual-hardware first
semantic contract
C
observable intent
MEANING≠
PROTOCOL≠
HARDWARE
ADDRESS
ADDRESS
Hypothesis: one contract can survive
different faithful realizations.
01 / Research problem
A checked boundary between meaning and realization.
A target does not become correct because a driver says it supports an operation. Its observable behavior must satisfy the semantic contract.
PSL / CONTINUITY PATH
small trusted boundary · fail closed
01
Semantic Contractobservable requirements · target neutral
02
Target Realizationbinding · representation · sequencing · state
03
Realization Evidenceproof / certificate material connecting behavior to contract
research boundary
04
Lean-checked Relationaccept only what the evidence establishes
05
Device Modelformal state · transitions · observations
Legacy Aaccept if faithful
Modern Baccept independently
Incapable Crefuse
Protocol validity is not semantic correctness.Refuse incompatible realizations.
First falsification target
A dishonest binding should fail.
The current capability gate can say that a target supports a write. It cannot yet prove that the write reaches the right resource with the right representation and state transition.
Read the threat modelcontract
SetSetpoint(25.0 °C)legacy encoding
25.0 °C → 250 → register 0x20accept
config → write 250 @ 0x20 → ACKreject
write 25 · 0x21 · wrong unit · wrong state02 / Three boundaries
Contract. Evidence. Device behavior.
Evidence
Why a realization is legal.
A realization must justify its mapping and behavior. A boolean capability declaration is only an early gate.
claim ≠ proof
Device
How a generation performs it.
Different targets may use different words, registers, protocols, state machines, or persistence mechanisms.
different realization · same contract
Hardware may change. Realizations may change. The accepted semantic obligation must not silently change.
03 / Adversarial model
Syntactically valid can still be semantically wrong.
The realization generator is treated as untrusted. The checker must detect errors that an ordinary protocol parser would happily accept.
Wrong bindingcorrect command · wrong resource
Wrong scale25 vs 250
Wrong unit°C vs °F
Wrong endianvalid bytes · wrong value
Wrong statemissing configuration mode
Wrong orderinglegal steps · illegal sequence
Wrong persistencevolatile vs required durable state
False capabilityclaim without behavioral evidence
Silent degradationincompatible target hidden by emulation
Ignored failureNACK / error discarded
The new work begins where the current boolean capability model stops: capability declaration is not realization correctness.
04 / Evidence, not hype
Different evidence supports different claims.
A theorem about a device model is not automatically a theorem about physical silicon. A virtual execution is evidence about that virtual implementation, not a proof of every real device.
Evidence typeWhat it can supportBoundary
λLean theoremProperties of the stated semantic/device modelsformal
✓Regression / adversarial testsCovered cases and expected rejection behaviorfinite
▶QEMU / Renode executionObserved behavior of selected virtual targetssimulation
↔Model conformance evidenceEvidence connecting executable model and formal modelseparate obligation
○Physical-device conformanceNot established merely by proving the modelfuture / empirical
contract→realization evidence→checked relation→device model→virtual / physical implementation
05 / Current baseline
Verified foundations, narrower claims.
01
Repaired canonical abstract/control semantics
02
Lean forward-simulation results for the verified model
03
Finite Python → Lean compiler-output conformance bridge
04
Semantic identity separated from PVM32 target binding
05
Capability refusal witness — not yet realization proof
finite compiler-output cross-check
65 accepted
streams
streams
22 distinct
ABI words
ABI words
The current surface-language witness is historical prototype evidence, not the new research claim.
06 / Virtual hardware first
No specialized equipment required.
The primary laboratory is deterministic virtual hardware. QEMU, Renode, and small frozen emulators may instantiate device generations while Lean defines the formal boundary.
reproducibleadversarialCI-friendly
same Semantic Contract
Legacy Aold-style protocol · fixed-point · stateful↓ACCEPT if proved
Modern B / Incapable Cdifferent realization / insufficient semantics↓ACCEPT / REFUSE
07 / Kill criteria
Make the hypothesis falsifiable.
PSL should become smaller if standard refinement techniques provide the same result more directly or if the continuity boundary cannot localize change.
01
Wrong bindings cannot be rejected without trusting the driver.
02
A second target contaminates the semantic contract with hardware details.
03
Hardware substitution forces unrelated semantic proofs to be redone.
04
The checker becomes as complex or trusted as the realization itself.
05
Simulation-specific assumptions leak into the formal semantic layer.
06
No measurable advantage appears over a conventional refinement baseline.
08 / Research position
The hypothesis, not a novelty claim.
Verified compilation, proof-carrying systems, platform-independent models, verified drivers, legacy emulation, and multilingual syntax already have substantial prior art.
Not novel individually
- verified compilation
- proof-carrying code / hardware
- platform-independent models
- portable/extensible IRs
- verified device drivers
- legacy emulation
“Can a stable semantic contract survive materially different hardware generations while independent realizations are checked for behavioral compatibility, incompatible targets fail closed, and upstream semantic evidence remains reusable?
current PSL research hypothesis
09 / Research documents
Claims, boundaries, and evaluation are explicit.
01Research charterscope and kill criteria↗
02Prior artwhat is already known↗
03Novelty contractwhat PSL may and may not claim↗
04Semantic continuityformal research model↗
05Threat modeldishonest and defective realizations↗
06Evaluation protocolvirtual generations and proof reuse↗
07Project originPāṇinian exploration · historical↗
10 / North star
Preserve meaning across implementation change.
Require evidence for realization.
Refuse incompatible targets.
Keep every proof boundary visible.
Measure what survives evolution.