M2.2: KRaft reference implementation in Rust #26

New issue

Closed

opened 2026-05-10 04:42:20 +00:00 by agent-engineering · 1 comment

agent-engineering commented

2026-05-10 04:42:20 +00:00

What

Compile KafkaKRaft.speck to Rust, run the generated code, and demonstrate it enforces all invariants from the spec at runtime.

Tasks

speckl compile examples/KafkaKRaft.speck --target=rust produces a runnable Rust module
Runtime guard checks fire and prevent invariant violations
Provenance trace: each Rust function has a doc comment pointing to source .speck line
Benchmark: state transition throughput for generated Rust vs handwritten equivalent

Exit Criteria

Generated KRaft Rust module compiles, runs, and enforces all invariants
Benchmark shows generated code within 2x of hand-optimized Rust for state transitions
Every generated function has provenance doc comments

Dependencies

#22 (M1.1: KRaft spec) and #25 (M2.1: Rust backend) must be complete.

Context

Part of M2.2 in docs/PROVE-KAFKA-PLAN.md.

## What Compile `KafkaKRaft.speck` to Rust, run the generated code, and demonstrate it enforces all invariants from the spec at runtime. ## Tasks - `speckl compile examples/KafkaKRaft.speck --target=rust` produces a runnable Rust module - Runtime guard checks fire and prevent invariant violations - Provenance trace: each Rust function has a doc comment pointing to source `.speck` line - Benchmark: state transition throughput for generated Rust vs handwritten equivalent ## Exit Criteria - Generated KRaft Rust module compiles, runs, and enforces all invariants - Benchmark shows generated code within 2x of hand-optimized Rust for state transitions - Every generated function has provenance doc comments ## Dependencies #22 (M1.1: KRaft spec) and #25 (M2.1: Rust backend) must be complete. ## Context Part of M2.2 in `docs/PROVE-KAFKA-PLAN.md`.

agent-cos referenced this issue

2026-05-10 04:43:02 +00:00

Prove Kafka — Project Plan #17

sscoble commented

2026-05-25 22:32:10 +00:00

Owner

M2.2 is gated on M2.1 (Rust code generation). The goal is:

speckl compile KafkaKRaft.speck --target=rust produces a Rust module
The generated code enforces all 6 KRaft invariants at runtime
Tests demonstrate invariant violation detection

Cannot execute until the Rust generator (M2.1/#25) is implemented.
The design is documented there. Re-assess when M2.1 implementation is complete.

Skipping this cycle — gated on M2.1 code generator implementation.

M2.2 is gated on M2.1 (Rust code generation). The goal is: 1. `speckl compile KafkaKRaft.speck --target=rust` produces a Rust module 2. The generated code enforces all 6 KRaft invariants at runtime 3. Tests demonstrate invariant violation detection Cannot execute until the Rust generator (M2.1/#25) is implemented. The design is documented there. Re-assess when M2.1 implementation is complete. Skipping this cycle — gated on M2.1 code generator implementation.