A cargo-generate template for formally-verified data processing pipelines using the Rhodium Standard Repositories (RSR) methodology.
This repository is a code generator template, not a library or framework.
Template engine |
|
Output |
A complete, buildable Rust project with proofs, configuration, and automation |
Determinism |
Same inputs → byte-identical output (suitable for reproducible builds) |
When you run cargo generate, this template produces a complete project with:
| Component | Purpose |
|---|---|
Rust CLI |
Comprehensive command-line interface with full flag taxonomy |
Isabelle/HOL |
Formal proofs of structural invariants (partitions, bijections, checksums) |
Nickel |
Type-safe build-time configuration with contracts |
Guile Scheme |
Runtime configuration validation and scripting |
just |
Task automation with layered recipe organisation |
Julia (optional) |
Numerical/ML integration via FFI |
Prove the scaffolding, test the logic.
-
Formal proofs for structure — Isabelle verifies data doesn’t disappear, splits are disjoint, mappings are bijective
-
Empirical tests for domain — Property-based and unit tests for business logic
-
Configuration as code — Nickel (build-time) + Guile (runtime) + env vars (deploy-time)
-
Automation over documentation — Procedures are recipes; docs explain why
-
No Python — Rust + Julia + Guile + shell
cargo install cargo-generate # if needed
cargo generate --git https://github.com/hyperpolymath/rhodium-pipeline
cd my-pipeline && just check-deps && just fullcargo generate --git https://github.com/hyperpolymath/rhodium-pipeline \
--name my-pipeline \
--define project_name=my_pipeline \
--define ProjectName=MyPipeline \
--define PROJECT_NAME=MY_PIPELINE \
--define description="My data processing pipeline" \
--define author="Your Name" \
--define email="you@example.com" \
--define license=MIT \
--define include_julia=false \
--define checksum_algo=blake3 \
--define isabelle_version=Isabelle2024 \
--define min_rust_version=1.75.0 \
--define default_threads=4 \
--define enable_telemetry=false \
--define target_platforms="linux-x86_64,macos-arm64"See QUICKSTART.adoc for the full variable reference.
| Variable | Type | Description | Example |
|---|---|---|---|
|
string |
Kebab-case project name |
|
|
string |
Snake_case for Rust modules |
|
|
string |
PascalCase for Isabelle theories |
|
|
string |
SCREAMING_SNAKE_CASE for env vars |
|
|
string |
One-line project description |
|
|
string |
Author name |
|
|
string |
Contact email |
|
|
choice |
Base license (MIT or PMPL-1.0) |
|
|
bool |
Include Julia FFI integration |
|
|
choice |
blake3, shake256, sha3-256, xxhash |
|
|
string |
Isabelle release version |
|
|
string |
Minimum supported Rust |
|
|
string |
Default parallelism |
|
|
bool |
Optional telemetry hooks |
|
|
string |
Comma-separated targets |
|
{{project-name}}/
├── Cargo.toml # Rust manifest
├── src/
│ ├── main.rs # CLI entry (500+ flag combinations)
│ ├── cli.rs # Argument definitions
│ ├── config.rs # Configuration loading
│ ├── pipeline.rs # Core pipeline logic
│ ├── validation.rs # Input/output validation
│ ├── checksum.rs # Integrity verification
│ └── {{module}}.rs # Domain-specific logic
├── proofs/
│ ├── {{ProjectName}}_Invariants.thy # Core invariants
│ ├── {{ProjectName}}_Partition.thy # Partition proofs
│ ├── {{ProjectName}}_Bijection.thy # Bijection proofs
│ ├── {{ProjectName}}_Checksum.thy # Checksum proofs
│ └── ROOT # Isabelle session
├── config/
│ ├── default.ncl # Nickel configuration
│ ├── presets/
│ │ ├── dev.ncl
│ │ ├── prod.ncl
│ │ ├── ci.ncl
│ │ └── paranoid.ncl
│ └── contracts/
│ ├── paths.ncl
│ ├── ratios.ncl
│ └── checksums.ncl
├── schemes/
│ ├── config.scm # Guile runtime validation
│ ├── validators.scm # Custom validators
│ └── transforms.scm # Data transforms
├── justfile # 200+ recipes
├── scripts/
│ └── (integrated into just)
├── tests/
│ ├── integration/
│ └── property/
├── fixtures/
│ └── sample_data/
├── docs/
│ ├── README.adoc
│ ├── QUICKSTART.adoc
│ ├── CLI.adoc
│ ├── ARCHITECTURE.adoc
│ ├── PROOFS.adoc
│ └── man/
│ └── {{project-name}}.1
└── LICENSEThis template is released under the Palimpsest License v0.8.
Generated projects inherit Palimpsest v0.8 layered on your choice of:
-
Palimpsest-MPL-1.0 License
-
Palimpsest-MPL-1.0 License
See LICENSE.txt and LICENSING.adoc for details.
zerostep — VAE dataset normalizer built using this methodology.
See CONTRIBUTING.adoc for guidelines.
-
HANDOVER.adoc — Complete methodology documentation
-
QUICKSTART.adoc — 5-minute getting started
-
ARCHITECTURE.adoc — Design decisions and rationale
-
CLI.adoc — Complete CLI reference
-
PROOFS.adoc — Isabelle proof patterns