Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ rust-version = "1.96"
license = "MIT"

[workspace.dependencies]
inkwell = { version = "0.9.0", default-features = false, features = ["llvm22-1-prefer-dynamic", "target-x86"] }
inkwell = { version = "0.9.0", default-features = false, features = ["llvm22-1-prefer-dynamic", "target-x86", "target-bpf"] }
serde = { version = "1.0.228", features = ["derive"] }
serde_json = "1.0.150"
sha2 = "0.11.0"
Expand Down
2 changes: 2 additions & 0 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,8 @@ Post-baseline library work has begun without widening the release foundation:
## Explicitly after 0.1.0

- expanding the experimental C backend beyond its accepted fail-closed subset;
- stabilizing or expanding the experimental eBPF backend beyond the initial
runtime-free XDP object experiment;
- a custom VM or stable serialized MIR/bytecode compatibility promise;
- the complete official extension and public-library catalog;
- finalizers, weak references, unrestricted runtime reflection, and Bubble
Expand Down
12 changes: 12 additions & 0 deletions architecture/03-compiler-pipeline.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ flowchart LR
M --> O[Optimized MIR]
O --> L[LLVM backend]
L --> N[Native object]
O -. experimental .-> B[LLVM BPF target]
B -. experimental .-> E[ELF eBPF object]
O -. experimental .-> C[C11 source backend]
O -. future .-> V[VM bytecode backend]
O -. tools .-> I[MIR interpreter / verifier]
Expand Down Expand Up @@ -166,6 +168,16 @@ optimization. It emits deterministic C11 for its declared runtime-free
capability subset and rejects unsupported MIR before publishing source; it never
reconstructs semantics from Pop source text.

The experimental eBPF backend follows the same handoff after portable MIR
optimization. It derives runtime-contract requirements from MIR, resolves them
against an explicit runtime profile, validates eBPF-specific target limits,
lowers through backend-private LLVM IR, selects LLVM's BPF target, and emits an
ELF eBPF object for an explicit program kind such as XDP. Missing runtime
contracts, unsupported backend representations, floating-point behavior,
dispatch, recursion, or unproven loop behavior are diagnosed before any object
is written; see
[ADR 0070](./decisions/0070-experimental-ebpf-backend.md).

## Tooling and incremental queries

The parser, resolver, type checker, and HIR APIs work without native code
Expand Down
1 change: 1 addition & 0 deletions architecture/04-intermediate-representations.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
| MIR | Portable execution semantics | CFGs, typed values, abstract runtime operations | source sugar, LLVM opcodes |
| C11 source | Experimental backend artifact | exact-width C types, checked helpers, private control-flow lowering | canonical language semantics, unchecked fallbacks |
| LLVM IR | Native backend implementation | LLVM types, intrinsics, target ABI | canonical language semantics |
| LLVM BPF IR | Experimental backend implementation | BPF triple, section metadata, backend-private scalar lowering | canonical language semantics, Pop managed runtime |

## Stable identities

Expand Down
6 changes: 3 additions & 3 deletions architecture/05-runtime-and-abi.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ a backend with verified relocating-root support. ABI 1.x, immutable root spills,
or a target capability alone cannot satisfy the production profile. Profile/
ABI mismatch fails before link or load; there is no silent bootstrap fallback.

Under ADR 0059, ABI 1 native execution no longer uses `BootstrapRuntime`.
Under ADR 0071, ABI 1 native execution no longer uses `BootstrapRuntime`.
Instead it composes the generational allocator and incremental SATB mature
collector in a `NativeStableGenerationalConformance` stage that places every
native allocation in a non-moving domain. This stage preserves ABI 1 stable
Expand Down Expand Up @@ -130,7 +130,7 @@ and capacity private, grows storage without changing the list handle, and
applies precise barriers for managed elements. MIR retains distinct typed list
operations; no backend may reinterpret them as array or table operations.

ADR 0060 advances native ABI 1 to version 1.11 with atomic initialized object
ADR 0072 advances native ABI 1 to version 1.11 with atomic initialized object
allocation. LLVM passes the exact pointer map and one physical initializer per
logical slot in a single native transition. The runtime validates every managed
initializer before publication and returns either a completely initialized
Expand Down Expand Up @@ -268,7 +268,7 @@ allocation assists, deterministic byte-limit OOM, empty-page return, and
domain/debt telemetry. It still reports the lower relocation contract because
cooperative work is not concurrent production marking, the native backend does
not yet provide writable relocating roots, and no profile may infer production
capability from implementation experiments. ADR 0059 permits a closed native
capability from implementation experiments. ADR 0071 permits a closed native
stable-token wrapper to use its mature allocator, SATB marking, and sweeping
without exposing nursery relocation; this does not select the production
profile.
Expand Down
25 changes: 25 additions & 0 deletions architecture/06-backend-architecture.md
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,31 @@ partial artifact. C text is disposable output and is not a stable ABI, cache,
or semantic contract. See
[ADR 0059](./decisions/0059-experimental-secure-c-transpilation-backend.md).

## Experimental eBPF backend

The experimental eBPF backend is an LLVM-backend mode for producing ELF eBPF
objects from verified MIR under an explicit runtime-contract profile. It
validates before emission, keeps BPF and Inkwell details inside the backend,
and uses LLVM's BPF target rather than a custom instruction emitter in the
first slice.

The initial triples are `bpfel-unknown-none` and `bpfeb-unknown-none`. They
represent ELF, no-OS LLVM BPF targets. Runtime support is selected separately
through profiles such as `linux-ebpf`. PLRI remains a set of abstract runtime
contracts; the `linux-ebpf` profile currently provides only the scalar
contracts needed by the MVP and therefore cannot satisfy requirements for
managed allocation, standard-library adapters, GC roots, closures, interfaces,
coroutines, or similar dynamic representations. Those failures are reported as
missing runtime contracts, not as HIR/MIR language bans.

The MVP supports an explicit XDP program mode, emits a wrapper in an `xdp`
section, and rejects checked arithmetic until trap-preserving lowering exists.
It also has eBPF-specific validation for invalid entry signatures, recursion,
floating point, unproven loop backedges, unsupported MIR operations, and
backend representations that have not been implemented yet. If LLVM BPF is
unavailable, object emission fails with a target diagnostic and no partial
artifact. See [ADR 0070](./decisions/0070-experimental-ebpf-backend.md).

## Future VM backend

The VM backend should lower canonical MIR to typed or register-based bytecode.
Expand Down
3 changes: 0 additions & 3 deletions architecture/22.2-system-network-security-catalog.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ the process filesystem through global registration.
| --- | --- | --- | --- |
| `Task` | standard/platform; planned; phase 3 | `Task<T>`, `CancelToken`, `Group`, deadline, spawn/join/race/select/yield/sleep; structured failure propagation | Time + PLRI scheduler; task creation may allocate; scope owns children; cancellation points explicit; no detached task by default or ambient context bag |
| `Channel` | standard; planned; phase 3 | bounded/unbounded typed channels, sender/receiver, select integration; `send`, `receive`, `trySend`, `close` | Task/Atomic; portable semantics; bounded is default for streams; allocation/copy/ownership documented; no untyped messages |
| `Actor` | standard/platform; planned; phase 4 | isolated local actors, exact typed mailboxes, actor references/replies, monitors, structured supervision, restart and shutdown policy | Task/Channel + scheduler and GC ownership contracts; messages are compiler-proven safe and copied into private actor ownership; mailboxes/restarts/cleanup are bounded; no shared mutable state, selective receive, marker-interface safety, or runtime type lookup |
| `Atomic` | standard/platform; planned; phase 3 | exact atomic integer/boolean/pointer-safe handles, memory order, fences, wait/notify | Intrinsics/PLRI; availability by target capability; operations allocate nothing; unsafe order combinations diagnosed; no managed raw pointers |
| `Actor` | standard/platform; planned; phase 4 | typed isolated `Ref<TMessage>`, `Inbox<TMessage>`, `Reply<T>`, supervisors, monitors, bounded mailboxes; `start`, `send`, `trySend`, `receive`, `reply` | Task/Channel/Codec + scheduler/GC isolation support; messages are statically proven copy-safe and copied into actor ownership; mailbox allocation, copying, suspension, stale incarnation, and failure are explicit; no symbolic registry, shared mutable actor state, or class hierarchy |
| `Cluster` | official/platform; planned; phase 8 | authenticated remote `Actor<TMessage>`, nodes, publish/spawn, delivery outcomes, remote supervision and test transports | Actor/Codec/Net/Crypto/Identity/Task; separately installed `Pop.Cluster`; bounded schema encoding and explicit partial failure; no location transparency, code shipping, string actor lookup, implicit retry, or exactly-once claim |
Expand All @@ -58,8 +57,6 @@ creating a general application service abstraction.
| `Socket` | standard/platform; planned; phase 4 | opaque socket handle, options, local/remote address, accept/send/receive/close, multicast | Io/Net/Task + PLRI; system calls explicit; caller buffers reusable; option availability typed; raw sockets require unsafe capability |
| `Http` | official; planned; phase 4 | `Request`, `Response`, `Header`, `Method`, `Status`, cookies, forms, multipart, cache/proxy/auth/redirect/retry records; `send`, `serve`; `Http.Route`, `Client`, `Server`, `Test` | Net/Uri/Mime/Codec/Task/Telemetry/Crypto; streaming bodies and pools explicit; safe redirect/TLS/header/body limits; HTTP/1.1, 2, 3 adapters typed; `Client` only an opaque connection-pool resource, never a service object |
| `WebSocket` | official; planned; phase 4 | handshake, typed frame/message stream, ping/pong/close, compression options | Http/Task/Bytes; bounded frames and backpressure; origin/auth checks; no string-dispatched message routing |
| `Cluster` | official; planned; phase 4 | optional `Pop.Cluster` Package for authenticated distributed actor endpoints, publication, remote spawn, monitoring, placement, and typed delivery outcomes | Actor/Codec/Net/Crypto/Identity/Task; exact public message schemas and explicit node/transport capabilities; bounded encoding, transport, and mailbox admission; partial failure remains typed; no location transparency, code shipping, runtime symbol lookup, automatic retry, or exactly-once claim |

Server-sent events are `Http.Event`; forms and multipart are `Http.Form` and
`Http.Multipart`. Retry/backoff policy is a typed `Http.Retry` value. Test and
in-memory transports implement the same explicit transport function record.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,8 @@ dependency requires a concrete component need, license/security review
proportional to its role, and tests proving the boundary it supports. Inkwell
0.9 is the first approved exception: the LLVM backend alone uses its Apache-2.0
safe wrapper with the exact installed LLVM-major feature, no default target
set, and only the native target enabled. Inkwell and `llvm-sys` types cannot
set, and only the reviewed native and BPF targets enabled. Inkwell and
`llvm-sys` types cannot
cross the backend crate boundary. Cargo
package/crate names are implementation details and do not replace Pop Lang's
`Item → Module → Bubble → Package → Workspace` terminology.
Expand Down
173 changes: 173 additions & 0 deletions architecture/decisions/0070-experimental-ebpf-backend.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,173 @@
# ADR 0070: Experimental eBPF Backend

- Status: accepted
- Date: 2026-07-14
- Supersedes: none

## Context

Pop Lang's canonical MIR is intentionally backend-neutral. A constrained eBPF
experiment can exercise that boundary for a kernel-oriented artifact, but it
must not turn Pop Lang into an implicit runtime inside the Linux kernel or leak
LLVM/BPF details into HIR, MIR, the driver, or target-independent crates.

PLRI is the abstract runtime-interface contract layer. It describes what a
program requires from a selected runtime profile; it is not itself the runtime
implementation and does not make every target provide allocation, GC,
standard-library adapters, or dynamic dispatch.

LLVM already provides a BPF target and ELF emission path. Reusing it for the
first slice gives Pop Lang a real object pipeline without committing to a custom
eBPF instruction emitter or a stable kernel ABI surface.

## Decision

Add an experimental `PopBpf` path inside the LLVM backend. It consumes verified
canonical MIR, derives runtime-contract requirements from MIR, resolves those
requirements against the selected runtime profile, runs dedicated eBPF target
validation, renders backend-private LLVM IR, initializes LLVM's BPF target, and
emits an ELF eBPF object. LLVM and Inkwell values remain private to the LLVM
backend.

The initial target triples are:

- `bpfel-unknown-none` for little-endian eBPF;
- `bpfeb-unknown-none` for big-endian eBPF.

Both are ELF targets with no conventional operating system. They record LLVM
BPF compatibility as a target capability. They do not themselves advertise
shared libraries, threads, unwind, stack maps, SIMD, coroutines, dynamic
loading, or GC relocation support. Runtime semantics are selected separately
through runtime profiles. If the linked LLVM was built without BPF support,
object emission fails before publishing an artifact and reports a backend
target diagnostic.

The initial runtime profile for this path is `linux-ebpf`. It provides only the
minimal contracts needed by scalar code: fixed stack storage, integer
operations, direct calls, and static data. It intentionally does not provide
managed allocation, GC, standard-library adapters, closure environments,
interface dispatch, coroutine scheduling, kernel helpers, maps, or ring
buffers. Programs that require those contracts fail contract resolution before
backend lowering. This is a profile limitation of the current implementation,
not a HIR/MIR rule that Pop strings, classes, collections, closures, or PLRI do
not exist.

The MVP supports an explicit XDP program mode selected by CLI:

```text
pop build <source.pop> \
--target bpfel-unknown-none \
--runtime-profile linux-ebpf \
--bpf-program xdp \
--emit-object <object.o>
```

The Pop entry point is the ordinary resolved binary entry in bootstrap source
mode. For XDP it must be a scalar function returning `Int` whose MIR runtime
requirements are satisfied by the selected profile; the backend generates an
`xdp` section wrapper named `pop_bpf_xdp` and maps the returned scalar to the
XDP action code. The first example returns numeric `2` (`XDP_PASS`). The MVP
does not expose an XDP context value to source code.

The initial supported subset is deliberately small:

- `Boolean`;
- fixed-width integers and `Int`;
- scalar enum constants;
- scalar constants;
- integer and Boolean operations that the backend can lower without changing
Pop Lang trap semantics;
- comparisons and Boolean/bitwise operations already represented in MIR;
- explicit branches without unproven loop backedges;
- non-recursive direct scalar calls;
- scalar returns;
- functions whose runtime-contract requirements are satisfied by the selected
profile.

Runtime-contract resolution rejects requirements that the selected profile does
not provide, including today's requirements for managed allocation, heap, GC,
roots, safe points, write barriers, string formatting, collections, classes,
closures, standard-library adapters, interface dispatch, coroutine/async
operations, arbitrary FFI, PLRI adapters, exceptions, and unwind.

The eBPF validator separately rejects floating point, recursion, invalid entry
signatures, unproven loops, indirect or dynamic calls, unsupported MIR
operations, incompatible layouts, and backend representations that this first
implementation cannot lower yet.

The memory model for the MVP is scalar SSA lowering backed by the `linux-ebpf`
profile. There is no selected profile implementation for a Pop managed heap,
object relocation, stack maps, standard runtime adapter, helper access, or map
access. Kernel memory, packet data, helpers, maps, ring buffers, and BTF are
future work that must be represented through explicit validated contracts
rather than raw pointer fallback.

Diagnostics use stable backend/target codes in the `POP7000` range and must
name the eBPF target, the rejected category, and the relevant MIR/source origin
when available. A failure emits no partial object.

## Consequences

- Pop Lang gains a real experimental path from source to ELF eBPF object while
preserving backend-neutral HIR and MIR.
- The feature is explicitly selected and is not a default build backend or a
`0.1.0` release requirement.
- The initial XDP example proves the pipeline, but not packet access, maps,
helpers, BTF, CO-RE, ring buffers, tracepoints, or attachment.
- LLVM BPF availability is an environment capability, so tests that require
object emission must detect and skip cleanly when unavailable; validation and
target tests remain unconditional.

## Alternatives considered

### Custom eBPF instruction emitter

Rejected for the first slice because it would expand the PR into instruction
selection, relocation, ELF writing, verifier-oriented optimization, and target
testing. A custom emitter remains possible after the MIR subset and artifact
contract mature.

### Treat eBPF as a normal native executable target

Rejected because eBPF has no process entry and no ordinary executable artifact.
Accepting it through the native path would hide target/profile contract failures
and risk host-target object emission.

### Add source-level BPF attributes immediately

Rejected for the MVP. CLI selection is sufficient for one explicit XDP entry
without adding parser, resolver, type-checker, and metadata surface area. Source
attributes can be revisited when maps, helpers, context types, or multiple
program entries require source ownership.

## Required conformance tests

- target tests recognize `bpfel-unknown-none` and `bpfeb-unknown-none` as ELF
LLVM BPF targets;
- runtime-contract tests prove `linux-ebpf` satisfies scalar contracts, rejects
missing managed/runtime contracts with profile/target/origin detail, and is
incompatible with non-BPF targets;
- validation accepts the minimal scalar XDP_PASS program;
- validation rejects floating point, missing runtime contracts, invalid
signatures, recursion, indirect calls, allocation/runtime effects, and
unproven loops;
- backend-private LLVM IR contains the BPF triple, an `xdp` section, the entry
wrapper, and no Pop runtime symbols;
- object-emission tests verify ELF BPF headers, section, symbol, and
deterministic output when LLVM BPF is available, and skip only that part with
an explicit reason otherwise;
- CLI tests require explicit target/profile/program/output selection and reject
unknown targets or runtime profiles without writing an object.

## Future work

Future ADRs or amendments must define typed contracts for checked integer trap
lowering, XDP context access, bounds-checked packet reads, helpers, maps, BTF,
CO-RE relocations, ring buffers, tracepoints, tail calls, verifier-oriented loop
bounds, and richer program types.

## Documents/components affected

Compiler pipeline, intermediate representations, backend architecture, CLI and
tooling contract, implementation roadmap, target inventory, diagnostic catalog,
LLVM backend tests, driver tests, and examples.
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ADR 0059: Native Stable-Token Generational Transition
# ADR 0071: Native Stable-Token Generational Transition

- Status: accepted
- Date: 2026-07-14
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
# ADR 0060: Atomic Initialized Object Allocation
# ADR 0072: Atomic Initialized Object Allocation

- Status: accepted
- Date: 2026-07-14
- Depends on: ADR 0022, ADR 0024, ADR 0038, ADR 0039, and ADR 0059
- Depends on: ADR 0022, ADR 0024, ADR 0038, ADR 0039, and ADR 0071
- Supersedes: none

## Context
Expand Down
Loading
Loading