LRW

Work / Research · active

Song

An operating system, language and compiler, with proof responsibility down to native instructions and bytes.

Iota · x86-64 · Lean 4

Song is my attempt to build an operating system whose foundation can explain why its operations do what they say. I want to be able to change it without rebuilding that argument by hand.

Gen2 had a self-hosting compiler above a handwritten assembly seed. Repeated compilation reached byte-identical binaries, a compiler fixpoint. That was useful evidence of reproducibility. The assembly seed itself was unverified.

Gen3 brings native instruction generation into the proof boundary. For the first multiplication, the proof follows the operation through its instructions and the encoded bytes, against the stated x86-64 model. Ten instructions, 32 bytes. The results page explains what that establishes and provides the source records.

The rings

Ring 0 is the mathematical and computational foundation. Ring 1 contains reusable libraries, including storage and I/O. Ring 2 contains applications and services. Ring 3 contains the interfaces and clients people use. Dependencies run inward: the foundation doesn't need a dashboard in order to work.

Ring 3Interfaces · clients · dashboards
Ring 2Applications · services
Ring 1Storage · I/O · reusable libraries
Ring 0Mathematical and computational foundation
Gen2

Checked foundation

↓ trusted handwritten assembly
Gen3

Checked foundation

↓ generated instructions + bytes
inside the proof boundary
Applications depend on the foundation. The foundation doesn't depend on an application. Gen3 extends its proof responsibility through the native code; the first multiplication is proved against the stated x86-64 model. The rest of the stack is ahead.

The change from gen2 to gen3 is at that innermost layer. The assembly core is generated and covered by Ring 0's proof responsibility too. The first native operation demonstrates the path; the full compiler and kernel are ahead.

Iota

I renamed Slang to Iota after learning that Slang was already a shader language. The language design is still changing. I want a function's meaning, what it may touch and the evidence for it to be readable together.

Song and Apeiron are independent implementations of the same underlying algebra. Apeiron uses Rust with Lean refinements. Song generates its own native code. Their relationship is correspondence between operations, without a Rust runtime inside Song.

Results and evidence · Discuss collaboration, funding or a contract.