#Aletheia - Property-Based Testing Code Generation for MoonBit

#Overview

• Pattern Detection: Automatically detects Round-Trip, Idempotent, Producer-Consumer, Invariant, and Oracle patterns
• Test Generation: Generates PBT code based on detected patterns
• PBT Synchronization: Syncs code blocks from <module>.pbt.mbt.md to per-package tests
• Dogfooding: Self-validates tool quality using its own test generation

#Current Status

#✅ Implemented Modules

#Test Coverage

• Total Tests: 50+
• Pass Rate: 100%

#Usage

# Run all tests
moon test

# Type check
moon check

# CLI help
moon run src/aletheia

# Generate PBT targets
moon run src/aletheia -- generate ./src

# Generate with JSON summary (dry-run)
moon run src/aletheia -- generate ./src --dry-run --format json

# Analyze with detailed explanations
moon run src/aletheia -- analyze ./src --explain

# Sync PBT markdown (default: src/aletheia.pbt.mbt.md)
moon run src/aletheia -- sync

# Self-apply PBT generation (template output)
./scripts/self_pbt.sh
# self_pbt.sh runs generate/sync + moon info + moon fmt

# Development batch check
./scripts/dev-check.sh

#PBT Development Workflow

1. Edit .pbt.mbt.md markdown file
2. Run ./scripts/self_pbt.sh to regenerate test files
3. Verify with moon test
4. Commit both markdown and generated test files

# Recommended PBT development workflow
# 1. Edit markdown
vim src/aletheia.pbt.mbt.md

# 2. Regenerate test files
./scripts/self_pbt.sh

# 3. Run tests
moon test

# 4. Review changes
git status
git diff

# 5. Commit (both markdown and generated test files)
git add src/aletheia.pbt.mbt.md src/*/pbt_generated_test.mbt
git commit -m "feat: add PBT tests for XYZ"

#Claude Code Plugins

# Try plugin locally (general use)
claude --plugin-dir ./plugins/aletheia-pbt

# Try plugin locally (self-apply)
claude --plugin-dir ./plugins/aletheia-self-pbt

# Add marketplace and install (within Claude Code)
/plugin marketplace add .
/plugin install aletheia-pbt@f4ah6o-plugins
/plugin install aletheia-self-pbt@f4ah6o-plugins

#Module Structure

src/
├── aletheia.pbt.mbt.md  # PBT targets/properties aggregation
├── aletheia/       # CLI entry point
├── analyzer/       # Function extractor and arbitrary detector
├── ast/            # AST definitions
├── cli/            # CLI command processing
├── dogfooding/     # Self-testing (Dogfooding)
├── generator/      # PBT code generation
├── parser/         # Markdown parser
├── patterns/       # Pattern detection
├── pbt/            # PBT runtime
├── pbt_sync/       # PBT synchronization
└── state_machine/  # State machine testing

#Architecture

#Core Components

1. aletheia - CLI entry point for moon-pbt-gen tool
   • Commands: analyze, generate, sync, help

2. analyzer - Code analysis engine
   • Detects Arbitrary trait implementations for testable types
   • Extracts function metadata using moonbitlang/parser
   • Builds call graphs for dependency analysis

3. generator - PBT test code generation
   • Edge case input generation
   • Expression generators for various types
   • Oracle-based testing templates
   • Frequency-based property test generation

4. patterns - Pattern detection engine
   • Round-Trip (encode/decode, serialize/deserialize)
   • Idempotent (sort, normalize, trim)
   • Producer-Consumer chains
   • Collection invariants (Map, Filter, Sort)
   • Oracle patterns (implementation vs reference)

5. pbt - Property-Based Testing runtime
   • Test execution with configuration
   • Value generators
   • Test case shrinking for counterexamples
   • Advanced shrinking strategies

6. state_machine - Stateful system testing
   • Shim interface for side effects
   • Command generation and execution

#Recent Enhancements (v0.4.0)

• Statistics integration for better test insights
• Enhanced invariant detection for collections
• Advanced shrinking systems
• State machine testing support
• Improved template generation
• Size parameter control for recursive types

#Limitations

• AST Parsing Precision: Currently uses simple line scanning, complex signatures and type inference are not supported
• Generated Test Adjustment: Treat generated .pbt.mbt.md as templates; adjust types and properties as needed
• Generation Markers: Inserts <!-- aletheia:begin --> and <!-- aletheia:end --> in .pbt.mbt.md. Manual edits outside markers are preserved
• Warnings: Build warnings about unused variables/functions exist (no functional impact)

#Editing Generated Files

#Marker-Protected Sections

• Inside markers: Auto-generated content, overwritten by generate command
• Outside markers: Manually added content is preserved

#Regeneration Rules

# Running generate multiple times produces identical results
moon run src/aletheia -- generate ./src
moon run src/aletheia -- generate ./src  # No diff

# Manual edits outside markers are preserved
echo "## Manual Notes" >> src/aletheia.pbt.mbt.md
moon run src/aletheia -- generate ./src
grep "Manual Notes" src/aletheia.pbt.mbt.md  # Manual Notes still present

#Verifying Determinism

# Generate first time
moon run src/aletheia -- generate ./src
cp src/aletheia.pbt.mbt.md /tmp/original.md

# Generate second time
moon run src/aletheia -- generate ./src

# Compare - should have no differences
diff /tmp/original.md src/aletheia.pbt.mbt.md

#Marker Specification

• Start marker: <!-- aletheia:begin -->
• End marker: <!-- aletheia:end -->

1. Content between markers is replaced on each generation
2. Content outside markers is preserved unchanged
3. If markers don't exist, they are created with all generated content inside
4. Manual edits should be placed outside markers to persist across regenerations

#Dependencies

• moonbitlang/parser - AST parsing
• moonbitlang/x - Standard extensions
• moonbitlang/quickcheck - PBT runtime

#License