No description
| examples | ||
| src | ||
| .gitignore | ||
| Cargo.lock | ||
| Cargo.toml | ||
| formal_verification_demo.html | ||
| formal_verification_demo.md | ||
| protocol_demo.html | ||
| protocol_demo.md | ||
| README.md | ||
| spec.md | ||
synplexum
End to end framework for compiling tensor programs. Splits the program into abstraction layers, relies on automated tools for verification and optimization. Allows the programmer full control of the execution, down to ASM and GPU instruction graphs, without weighing them down with implementation details.
quickstart
Read the spec.md and other *_demo.md files in the root to understand the scope of the project.
We have a L1 DSL specifying actors and leafs over a data pipeline. These are primitives meant for dealing with moving data over a CPU or network. To interact, run the repl:
cargo run -- repl
Then type :help for usage guidelines, and :examples to see some prebuilt usage.
demo output
L1 REPL — type declarations or :help for commands.
l1> :help
L1 REPL Commands
────────────────
:load <file> Load a .l1 file, replacing current state
:reset Clear all declarations
:run [N] Compile and execute (N overrides step count)
:ir Show current L1 IR with pipeline diagram
:l0 Show emitted L0 IR (syntax-highlighted)
:verify Run formal verification pipeline
:run-verified Run with all invariant checks and produce verified report
:help Show this help and DSL reference
:examples List built-in examples
:examples <name> Load example with annotated walkthrough
:quit Exit the REPL
Declaration Forms
─────────────────
actor <name> {
state { <field>: <type> = <init>, ... }
Mutable fields owned by this actor. Updated in handlers.
window <name> : (<field>, ...) readers(<leaf>, ...)
Read-only snapshot of selected fields. Leaves listed in
readers() may read this window. Provides safe concurrent access.
on <MessageType>(<arg>: <type>, ...) { <body> }
Message handler. Body is a sequence of field assignments.
Expressions: field refs, args, literals, arithmetic (+, -, *).
}
leaf <name> {
reads <actor>.<window>
(optional) Declares which actor window this leaf may read.
process {
forward(<actor>, <MsgType>(<arg>, ...))
Send a message to an actor's handler.
read(<actor>.<window>.<field>)
Read a field from a window snapshot.
emit(<expr>)
Emit a value to the output region (observable output).
}
}
pipeline <name> { <stage> -> <stage> -> ... }
Defines execution order. Stages are actor or leaf names.
Each core step walks the pipeline left to right.
core <name> {
actors: [<name>, ...] Actors in this core
leaves: [<name>, ...] Leaves in this core
pipelines: [<name>, ...] Pipelines to execute
steps: <N> Number of execution steps (bounded)
}
Types & Expressions
───────────────────
Field types: u64, i64, f64
Operators: + - * (binary arithmetic)
Literals: 0, 1, 42, ... (unsigned integers)
Expressions: field, arg, literal, (expr op expr)
Execution Semantics
───────────────────
Each core step:
1. Walk pipeline stages left to right
2. Leaves execute: forward messages, read windows, emit outputs
3. Messages dispatched to actor handlers, updating state
4. Window snapshots updated for next step
Execution is bounded (finite steps) — no unbounded loops.
Multi-line input: open braces auto-continue to the next line.
built in example:
l1> :examples counter
Example: counter
─────────────────
┌─ The simplest L1 program. One actor receives Increment messages
│ and counts up. A leaf sends the message each step.
actor counter {
state {
count: u64 = 0
}
▲ One mutable field: count, starts at 0.
window count_view : (count) readers(display)
▲ Exposes 'count' as a read-only window. The 'display' leaf
can read it safely without blocking the actor.
on Increment(amount: u64) {
count = count + amount
}
▲ Handler: when an Increment(amount) message arrives,
add amount to count. This is the only way state changes.
}
leaf ticker {
process {
forward(counter, Increment(1))
}
}
▲ Each step, ticker sends Increment(1) to counter.
Leaves are the edges of the system — they produce and consume.
leaf display {
reads counter.count_view
process {
read(counter.count_view.count)
}
}
▲ display reads the count window. 'reads' declares the dependency;
read() in process actually fetches the value.
pipeline main { ticker -> counter -> display }
▲ Execution order: ticker sends, counter processes, display reads.
core main {
actors: [counter] leaves: [ticker, display]
pipelines: [main] steps: 5
}
▲ Runs the pipeline for 5 steps. After: count = 5.
Execution is bounded — no infinite loops possible.
Try: :run to execute, :ir for IR, :verify for formal verification
l1> :ir
L1 IR
─────
actor counter {
state {
count: u64 = 0
}
window count_view : (count) readers(display)
on Increment(amount: u64) { count = (count + amount) }
}
leaf ticker { forward(counter, Increment(1)); }
leaf display { reads counter.count_view; read(counter.count_view.count); }
pipeline main { ticker -> counter -> display }
core main {
actors: [counter]
leaves: [ticker, display]
pipelines: [main]
steps: 5
}
Pipeline Topology
─────────────────
pipeline: main
[ leaf: ticker ]
forward -> counter.Increment
│ Increment
▼
┌─ actor: counter ─┐
│ state: {count: u64} │
│ window: count_view (count) │
│ on Increment(amount: u64) │
└──────────────┘
│
▼
[ leaf: display ]
read counter.count_view.count
core: main
actors: [counter] leaves: [ticker, display] steps: 5