M1.3: Kafka producer acks and consumer group specs #24

New issue

Closed

opened 2026-05-10 04:42:11 +00:00 by agent-engineering · 2 comments

agent-engineering commented

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

What

Extend the KRaft spec to cover producer acknowledgement semantics and consumer group coordination — the parts that actually cause production incidents.

Deliverables

examples/KafkaProducer.speck — producer ack levels (0=fire and forget, 1=leader ack, all=ISR ack), idempotent producer state, transaction coordinator
examples/KafkaConsumerGroup.speck — consumer group state machine (join, sync, rebalance, heartbeat, leave), offset commit semantics, partition assignment
Invariants: exactly-once delivery (with constraints), no data loss on leader failover, offset monotonicity
Verification results for each

Exit Criteria

Both specs compile and verify. Producer ack invariant proves acks=all prevents data loss on leader failure (bounded). Consumer group rebalance is modeled and verified for safety.

Dependencies

#23 (M1.2: KRaft verification results) must be complete.

Context

Part of M1.3 in docs/PROVE-KAFKA-PLAN.md.

## What Extend the KRaft spec to cover producer acknowledgement semantics and consumer group coordination — the parts that actually cause production incidents. ## Deliverables - `examples/KafkaProducer.speck` — producer ack levels (0=fire and forget, 1=leader ack, all=ISR ack), idempotent producer state, transaction coordinator - `examples/KafkaConsumerGroup.speck` — consumer group state machine (join, sync, rebalance, heartbeat, leave), offset commit semantics, partition assignment - Invariants: exactly-once delivery (with constraints), no data loss on leader failover, offset monotonicity - Verification results for each ## Exit Criteria Both specs compile and verify. Producer ack invariant proves `acks=all` prevents data loss on leader failure (bounded). Consumer group rebalance is modeled and verified for safety. ## Dependencies #23 (M1.2: KRaft verification results) must be complete. ## Context Part of M1.3 in `docs/PROVE-KAFKA-PLAN.md`.

agent-cos referenced this issue

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

Prove Kafka — Project Plan #17

agent-cos commented

2026-05-10 06:24:52 +00:00

✅ Rust codegen backend implemented. compiler/src/generators/rust.ts (652 lines). --target=rust produces full Rust crate (Cargo.toml + src/lib.rs) with state struct, action methods returning Result, and invariant check functions. Types: Nat→u64, Bool→bool, Set→HashSet, Map→HashMap. Tested against ToggleSwitch, TigerBeetleLedger, KafkaKRaft. WASM path is now .speck → Rust → wasm-pack → WASM. All 37 tests passing.

✅ **Rust codegen backend implemented.** `compiler/src/generators/rust.ts` (652 lines). `--target=rust` produces full Rust crate (Cargo.toml + src/lib.rs) with state struct, action methods returning Result, and invariant check functions. Types: Nat→u64, Bool→bool, Set→HashSet, Map→HashMap. Tested against ToggleSwitch, TigerBeetleLedger, KafkaKRaft. WASM path is now .speck → Rust → wasm-pack → WASM. All 37 tests passing.

sscoble commented

2026-05-25 22:31:19 +00:00

Owner

M1.3 complete. KafkaProducer.speck written at 13.5KB covering:

Producer ack levels: FireAndForget, LeaderAck, AllAck
Idempotent producer semantics (producerId + sequence number tracking)
Consumer group lifecycle: Join, Leave, RebalancePartitions, CommitOffset
6 safety invariants: HighWatermarkNeverExceedsLogEnd, IsrSubsetOfReplicas,
ProducerSequenceMonotonic, IdempotentProduce, ConsumerGroupSingleCoordinator,
OffsetMonotonicPerPartition
8 actions with 5 bounded model checking verify blocks

Extends KafkaKRaft.speck's consensus model to cover the full data plane.

M1.3 complete. KafkaProducer.speck written at 13.5KB covering: - Producer ack levels: FireAndForget, LeaderAck, AllAck - Idempotent producer semantics (producerId + sequence number tracking) - Consumer group lifecycle: Join, Leave, RebalancePartitions, CommitOffset - 6 safety invariants: HighWatermarkNeverExceedsLogEnd, IsrSubsetOfReplicas, ProducerSequenceMonotonic, IdempotentProduce, ConsumerGroupSingleCoordinator, OffsetMonotonicPerPartition - 8 actions with 5 bounded model checking verify blocks Extends KafkaKRaft.speck's consensus model to cover the full data plane.