Markdown Converter
Agent skill for markdown-converter
Guidelines for AI agents working on the lading codebase. For detailed rationale
Sign in to like and favorite skills
Guidelines for AI agents working on the lading codebase. For detailed rationale behind these rules, see the Architecture Decision Records.
| Need | Answer |
|---|---|
| Validate changes | (mandatory, never skip) |
| Run tests | |
| Run Kani proofs | |
| Shape rule | 3+ repetitions = create abstraction |
| Dependencies | When in doubt, implement rather than import |
| HashMap allowed? | No - use / for determinism |
| Task | Key Rules | ADRs |
|---|---|---|
| Adding a generator | Pre-compute payloads, deterministic RNG, no panics, property tests for determinism | 001, 002, 003, 006 |
| Modifying payload generation | Property tests for invariants, deterministic output, no wall-clock time | 002, 003, 006 |
| Adding a blackhole | Must never backpressure target, property tests for throughput guarantees | 001, 005, 006 |
| Modifying throttle | Kani proofs required, formal invariants | 003, 005, 006 |
| Core algorithm changes | Proofs where feasible, property tests otherwise | 006 |
| Writing tests | Property tests default, document invariants | 006 |
| Adding a dependency | Evaluate: performance, determinism, control | 008 |
| Code style questions | Shape rule, no mod.rs, imports at top | 007 |
Generator --> Target --> Blackhole
Key principle: Pre-compute everything possible. See ADR-001, ADR-002.
Lading must be:
See ADR-005.
When writing generators or payload code:
thread_rng())IndexMap/IndexSet over HashMap/HashSetSee ADR-003.
Result<T, E> always.unwrap() or .expect()thiserror#[derive(Debug, thiserror::Error)] pub enum Error { #[error("failed to connect to {addr}: {source}")] Connect { addr: SocketAddr, source: io::Error }, }
See ADR-004.
mod.rs - use foo.rs not foo/mod.rs"{index}" not "{}"See ADR-007.
Hierarchy: Proofs > property tests > unit tests
Invariant documentation required - use formal mathematical language:
/// For all request > max_capacity: request(ticks, request) returns Err /// /// Capacity requests exceeding maximum always fail. #[kani::proof] fn request_too_large_always_errors() { ... }
See ADR-006 for patterns and examples.
Evaluate before adding: performance, determinism, control, criticality. When in doubt, implement rather than import.
See ADR-008.
Document why, not what. The code shows what; comments explain why.
//! for crate/module level/// for types and functions# Errors, # Panics sections/// Send payload bytes to the target. /// /// # Errors /// /// Returns error if connection is closed or write times out. pub async fn send(&mut self, payload: &[u8]) -> Result<(), Error> { ... }
MUST run
after any code changes.ci/validate
| Task | Command |
|---|---|
| Full validation | |
| Format | |
| Check | |
| Lint | |
| Test | |
| Kani proofs | |
| Outdated deps | |
| Benchmarks | |
| Environment | PROPTEST_CASES | PROPTEST_MAX_SHRINK_ITERS |
|---|---|---|
Local () | 64 | 2048 |
| CI | 512 | 10000 |
Override locally:
PROPTEST_CASES=512 ci/test
ci/validate after changes - never skip