Skip to content

QUICKSTART-DEV.adoc

Latest commit

 

History

History
139 lines (108 loc) · 3.89 KB

QUICKSTART-DEV.adoc

File metadata and controls

139 lines (108 loc) · 3.89 KB
Raw

proven-servers — Quick Start for Developers

Table of Contents

Tech Stack

  • ABI + proofs: Idris 2 (dependent types; %default total). Each component’s ABI lives in src/<Name>ABI/ — tag encodings with round-trip proofs, state-machine GADTs, and the FFI contract. Type-checking is proof checking.

  • FFI / engines: Zig 0.15+ in ffi/zig/, exporting a C ABI.

  • Bridge: generated C headers in generated/abi/.

  • Bindings: 20 languages in bindings/ — Ada, C++, C#, Dart, Elixir, Gleam, Go, Haskell, Java, JavaScript, Julia, Kotlin, Lua, OCaml, PHP, Python, ReScript, Ruby, Rust, Swift — thin wrappers over the same C ABI (Elixir/Gleam/ReScript are constants-only scaffolds pending FFI; see ADR 0003).

Set Up Development Environment

Option A: Guix (preferred)

guix shell

Option B: Nix (fallback)

nix develop

Option C: Manual

git clone https://github.com/hyperpolymath/proven-servers.git
cd proven-servers
just setup-dev

Build

# Idris2 core + proofs for one component (a clean build = proofs verified):
idris2 --build protocols/proven-<name>/proven-<name>.ipkg

# Zig FFI engine (shared + static libraries):
(cd protocols/proven-<name>/ffi/zig && zig build)

# Or, via the task runner:
just build

Test

# One engine's FFI tests:
(cd protocols/proven-<name>/ffi/zig && zig build test)

# Full end-to-end suite (FFI builds + safety aspects):
bash tests/e2e.sh        # or: just test

Project Structure

proven-servers/
├── src/                  # Source code
├── src/abi/              # Idris2 ABI definitions (if applicable)
├── ffi/zig/              # Zig FFI bridge (if applicable)
├── tests/                # Test suite
├── docs/                 # Documentation
├── .machine_readable/    # Checkpoint files (STATE, META, ECOSYSTEM)
├── Justfile              # Task runner recipes
├── guix.scm              # Guix environment
├── flake.nix             # Nix environment (fallback)
└── 0-AI-MANIFEST.a2ml    # AI agent entry point

Key Recipes

just build          # Build the project
just test           # Run tests
just doctor         # Self-diagnostic
just lint           # Lint and format
just panic-scan     # Security scan via panic-attacker
just tour           # Guided tour of the codebase

Before Submitting a PR

just lint           # Format and lint
just test           # All tests pass
just panic-scan     # No new security issues

Contractile Invariants

Read .machine_readable/MUST.contractile before making changes. Key invariants that must never be violated:

  • The ABI is defined in Idris 2; FFIs/APIs are implemented in Zig (the RSR standard — see ABI-FFI-README.md).

  • No proof-escape hatches in Idris code (believe_me, assert_total, assert_smaller, idris_crash, postulate); %default total in every module.

  • No @panic or unreachable in Zig FFI production code; every exported function is NULL-/invalid-handle-safe.

  • ABI tag values must match exactly between Idris (*ABI.Types) and Zig (@intFromEnum); the FFI tests enforce this.

  • Every component’s ABI modules are listed in its .ipkg, so the proofs are actually compiled (not orphaned).

LLM/AI Agent Development

If using an AI assistant, load the warmup context first:

just llm-context    # Outputs role-appropriate context

Or read 0-AI-MANIFEST.a2ml and .claude/CLAUDE.md directly.

Get Help