Epic: Proven Core — formal verification and crate restructuring #262

Summary

Restructure logfwd into a proven core architecture with formal verification (Kani), portable SIMD (wide crate), and streaming structural character detection.

Current status (2026-04-04)

Done

• Phase 0: Kani prototype — 31 proofs across core modules
• Phase 1a: logfwd-arrow crate (PR feat: create logfwd-arrow crate, move builders + scanner structs (Step 1) #307)
• Phase 1b: logfwd-input/io crate (Create logfwd-input crate, move file tailer + IO #265)
• Phase 1c: Move impure modules (Move remaining impure modules (enrichment, compress, diagnostics) #266)
• Phase 1d: Tighten core to #![no_std] + #![forbid(unsafe_code)] (Tighten logfwd-core to no_std + forbid(unsafe_code) #267, PR feat: logfwd-core is now #![no_std] + #![forbid(unsafe_code)] #375)
• Phase 1.5: Framer + CriAggregator + byte_search with Kani proofs (PR feat: Framer + CriAggregator — zero-copy, Kani-proven line splitting (Steps 4-5) #311)
• Phase 2: Unified StructuralIndex — portable SIMD via wide (Unified SIMD StructuralIndex: extend ChunkIndex to detect all structural characters #313, PR feat: StructuralIndex — portable SIMD via wide, replace ChunkIndex #360)
• Phase 3: Zero-copy Bytes pipeline (Refactor: zero-copy pipeline — Bytes as universal currency, Framer/Aggregator model #303)
• Phase 4: Scanner restructure + FieldSink (Phase 3: Scanner restructure + FieldSink trait #269)
• Phase 5a: Typestate BatchTicket (PR feat: pipeline state machine — typestate BatchTicket + PipelineMachine #425)
• Phase 5b: PipelineMachine lifecycle (PR feat: pipeline state machine — typestate BatchTicket + PipelineMachine #425)
• Phase 5c: Wire PipelineMachine into pipeline.rs (Pipeline state machine extraction + BatchToken #270, PRs feat: Phase 5c — checkpoint wiring (#584, #585, #586, #587, #589) #637, feat: wire FileCheckpointStore into pipeline — persist and restore file offsets (#588) #784)
• Phase 5d: proptest random event sequences
• Phase 5e: Offset semantics research
• Phase 6: proptest state machines + CI hardening (proptest state machines + CI hardening #271)
• Phase 7a: TLA+ PipelineMachine specification (TLA+ specification for pipeline protocol #272)

Remaining

• Phase 7b/7c: TLA+ FileCheckpoint + additional specs (Remove extern crate alloc from logfwd-core (allocation-free kernel) #358)
• Phase 9: Allocation-free kernel (Remove extern crate alloc from logfwd-core (allocation-free kernel) #358)

Note: Phase 8 (no_std) completed ahead of schedule (done as Phase 1d).

Architecture

logfwd-core         #![no_std], #![forbid(unsafe_code)], proven
  structural.rs     StructuralIndex + wide SIMD + Kani proofs
  scanner.rs        Sequential bitmask consumer (trailing_zeros)
  framer.rs         Newline bitmask → line ranges
  aggregator.rs     CRI P/F merging
  pipeline/         BatchTicket + PipelineMachine typestates

logfwd-arrow        Arrow builders (StreamingBuilder, StorageBuilder)
logfwd-io           File tailer, diagnostics, checkpoint, enrichment, compression
logfwd-transform    DataFusion SQL transforms
logfwd-output       OTLP, Elasticsearch, Loki, Parquet, JSON lines
logfwd-config       YAML parsing and validation

Key decisions

See dev-docs/DECISIONS.md:

• Two-stage architecture: SIMD detects (parallel), scanner consumes (sequential)
• Streaming per-block: no stored bitmask vectors (simdjson pattern)
• Portable SIMD via wide crate: no hand-rolled platform backends
• Three-layer verification: Kani (scalar) → proptest (SIMD ≡ scalar) → Kani (consumers)
• Opaque checkpoints: generic over type C (u64 for file, i64 for Kafka, String for journald)