diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 031e9cb..80311cf 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -32,9 +32,8 @@ RSR layout — see https://github.com/hyperpolymath/standards): | **Gleam** | Backend services | Runs on BEAM or compiles to JS | | **Bash/POSIX Shell** | Scripts, automation | Keep minimal | | **JavaScript** | Only where AffineScript cannot | MCP protocol glue, Deno APIs | -| **Python** | SaltStack only | No other Python permitted | | **Nickel** | Configuration language | For complex configs | -| **Guile Scheme** | State/meta files | STATE.scm, META.scm, ECOSYSTEM.scm | +| **A2ML** | State/meta files | STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml (TOML-like) | | **Julia** | Batch scripts, data processing | Per RSR | | **OCaml** | AffineScript compiler | Language-specific | | **Ada** | Safety-critical systems | Where required | @@ -71,7 +70,7 @@ Both are FOSS with independent governance (no Big Tech). 2. **No package.json - use deno.json deps** - Use deno.json imports 3. **No node_modules in production** - Deno caches deps automatically 4. **No Go code** - Use Rust instead -5. **Python only for SaltStack** - All other Python must be rewritten +5. **No Python** - Python is fully banned (no exceptions); rewrite in AffineScript/Rust 6. **No Kotlin/Swift for mobile** - Use Tauri 2.0+ or Dioxus ### Package Management diff --git a/copilot-instructions.md b/.github/copilot-instructions.md similarity index 94% rename from copilot-instructions.md rename to .github/copilot-instructions.md index afee095..0e9129a 100644 --- a/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -13,15 +13,15 @@ When reviewing code in this repository, apply these standards strictly. 3. Ada/SPARK — safety-critical, formal verification 4. Haskell — pure functional, type-heavy domains 5. Elixir — concurrent, distributed, fault-tolerant systems -6. ReScript — frontend when JS interop needed +6. AffineScript — application code where a typed web/Deno target is needed 7. Chapel — parallel computing, HPC workloads 8. Julia — numerical computing, scientific applications **Avoid:** - C — use Zig instead - C++ — use Zig or Rust instead -- Python — reject unless interfacing with Python-only libraries -- JavaScript — use ReScript or TypeScript instead +- Python — reject (banned across the estate) +- JavaScript — use AffineScript instead - Shell scripts over 50 lines — rewrite in a proper language **Flag for justification:** @@ -80,8 +80,7 @@ When reviewing code in this repository, apply these standards strictly. |-----------|-----------| | Docker | Podman | | Makefile | Justfile | -| GitHub Actions self-reference | GitLab CI preferred for personal projects | -| npm/yarn | pnpm (if JS unavoidable) | +| npm/yarn/pnpm | Deno | | pip/poetry | Reject (avoid Python) | **Build files:** diff --git a/.gitignore b/.gitignore index 0854481..1c65f1b 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,6 @@ Thumbs.db # Temporary *.tmp *.log + +# Built escript binary (mix escript.build) +/phronesis diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index cbf251b..e8e73bb 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,9 +5,9 @@ [metadata] project = "phronesis" version = "0.9.0" -last-updated = "2026-06-18" +last-updated = "2026-06-20" status = "active" -session = "reflexion design layer + docs/metadata/licence sync — 2026-06-18" +session = "docs refresh + RSR/bot-doc compliance + root cleanup — 2026-06-20" [project-context] name = "Phronesis" @@ -32,18 +32,16 @@ milestones = [ [blockers-and-issues] issues = [ - { id = "pre-existing-test-failures", note = "DebuggerTest (Trace.merge/2 undefined; State.variables), DocGeneratorTest, IncrementalLexerTest, ConformanceTest 04_boolean_logic — predate the reflexion work" }, { id = "compiler-backend", note = "Rust to WASM codegen is still AST scaffolding only" }, ] [critical-next-actions] actions = [ - "Repair pre-existing test failures (Trace.merge/2 in debugger; State.variables field)", "Wire reflexion claim ingest for the compiler, formal/proof, and benchmark sources", "Advance the Rust to WASM production compiler beyond AST scaffolding", "Add Idris2 ABI definitions and the Zig FFI layer", ] [maintenance-status] -last-run-utc = "2026-06-18T00:00:00Z" -last-result = "warn" # unknown | pass | warn | fail (reflexion suite green; pre-existing failures remain) +last-run-utc = "2026-06-20T00:00:00Z" +last-result = "pass" # unknown | pass | warn | fail (full ExUnit suite green; consensus/Raft cases skipped pending :ra) diff --git a/.machine_readable/6a2/anchors/ANCHOR.a2ml b/.machine_readable/6a2/anchors/ANCHOR.a2ml new file mode 100644 index 0000000..566c696 --- /dev/null +++ b/.machine_readable/6a2/anchors/ANCHOR.a2ml @@ -0,0 +1,63 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# ANCHOR.a2ml - authoritative anchor for the phronesis repository. + +[metadata] +version = "1.0.0" +last-updated = "2026-06-20" + +[anchor] +schema = "hyperpolymath.anchor/1" +repo = "hyperpolymath/phronesis" +authority = "upstream-canonical" + +purpose = [ + "Define canonical semantics and policy boundaries for Phronesis.", + "Declare what downstream/satellite repos can extend but not redefine.", + "Provide a stable golden path and invariant contract for release readiness.", +] + +[identity] +project = "phronesis" +kind = "language" +one-sentence = "A neuro-symbolic, provably-safe language for agentic ethical reasoning on the BEAM." +domain = "ethical AI / policy languages / formal verification" + +[semantic-authority] +policy = "canonical" +owns = [ + "Phronesis language semantics and specification (spec/, formal/)", + "Invariant definitions and contractiles (.machine_readable/contractiles/)", + "Reference implementation behaviour (lib/phronesis/)", +] + +[implementation-policy] +# Languages actually used in this repo, plus estate-allowed neighbours. +allowed = ["Elixir", "Rust", "Idris2", "Agda", "Zig", "TLA+", "AsciiDoc", "Just", "Guix Scheme"] +forbidden = ["Python", "Go", "TypeScript", "ReScript", "V-lang", "Node.js", "npm"] + +[golden-path] +smoke-test-command = [ + "just deps", + "just build", + "just test", +] +success-criteria = [ + "Full ExUnit suite passes (consensus/Raft cases skipped — see docs/TESTING-REPORT.adoc)", + "just build is clean under --warnings-as-errors", + "No unresolved critical security findings", +] + +[satellite-policy] +must-pin-upstream = true +must-declare-authority = true +must-have-anchor = true +must-have-golden-path = true + +[semantic-authority-files] +language-spec = "spec/grammar.ebnf" +operational-semantics = ".machine_readable/SPEC.core.a2ml" +formal-consensus-spec = "formal/PhronesisConsensus.tla" +proof-corpus = "academic/proofs/" +claims-vs-reality = "AUDIT.adoc" diff --git a/.machine_readable/ai/.clinerules b/.machine_readable/ai/.clinerules new file mode 100644 index 0000000..662b944 --- /dev/null +++ b/.machine_readable/ai/.clinerules @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Phronesis — Cline AI rules. Kept in sync with .cursorrules / .windsurfrules. +# Authoritative AI instructions: 0-AI-MANIFEST.a2ml (root) and .claude/CLAUDE.md. + +# STARTUP (read in this order) +# 1. 0-AI-MANIFEST.a2ml — canonical file locations + invariants +# 2. .machine_readable/6a2/anchors/ANCHOR.a2ml — identity + golden path +# 3. .machine_readable/6a2/STATE.a2ml — current status + blockers +# 4. .claude/CLAUDE.md — full language / licence policy + +# LICENSE (per-file, REUSE-style; SPDX header required on EVERY file) +# Code (*.ex/*.exs/*.rs/*.idr/*.tla/*.zig, mix.exs, Justfile, Mustfile, *.a2ml, +# Guix *.scm): MPL-2.0. +# Documentation (narrative *.adoc, wiki/, academic/ prose): CC-BY-SA-4.0. +# GitHub community files (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, +# CHANGELOG.md): MPL-2.0. +# Never AGPL-3.0. Copyright: Jonathan D.A. Jewell (hyperpolymath) +# . + +# STATE FILES (.machine_readable/6a2/ ONLY) +# The 6 core A2ML files — STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK — +# live in .machine_readable/6a2/ and NOWHERE else. Never create *.a2ml metadata +# in the repo root; the root copy is always treated as stale drift. + +# LANGUAGES (this repo) +# Reference implementation: Elixir/BEAM (lib/phronesis/). +# Production compiler: Rust -> WASM (compiler/phronesis-ast, compiler/phronesis-wasm). +# Formal: TLA+ (formal/); proof corpus in academic/ (lattice/order/type theory). +# Estate-allowed elsewhere: AffineScript, Rust/SPARK, Zig, Idris2, Agda, Gleam, Elixir. +# BANNED: Python, Go, TypeScript, ReScript, V-lang, Java/Kotlin/Swift, Node.js, npm. + +# BANNED UNSAFE PATTERNS +# Elixir: no bare `raise` without a rescue strategy; use {:ok,_}/{:error,_} tuples; +# supervisors need explicit restart strategies. +# Rust: no `transmute` (unless FFI with a // SAFETY: comment); no `.unwrap()`/ +# `.expect()`/`panic!` in library code without justification. +# Idris2: no believe_me/assert_total/assert_smaller. Coq: no Admitted. Lean: no sorry. + +# CONTAINERS +# Runtime: Podman (never Docker). File: Containerfile (never Dockerfile). + +# BUILD SYSTEM +# Use `just` (Justfile) for build/test/lint/format. No Makefiles (use Mustfile/ +# Justfile). `just test` is the definitive correctness gate. + +# DOCUMENTATION +# AsciiDoc (.adoc) for all docs. Markdown only for GitHub-required files +# (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, CHANGELOG.md, .github/**). +# README is .adoc here. + +# CODE STYLE +# British English in user-facing strings and docs. Descriptive names. No +# commented-out code (git has history). Must pass `mix format` / `rustfmt`. diff --git a/.machine_readable/ai/.cursorrules b/.machine_readable/ai/.cursorrules new file mode 100644 index 0000000..cdadbc7 --- /dev/null +++ b/.machine_readable/ai/.cursorrules @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Phronesis — Cursor AI rules. Kept in sync with .clinerules / .windsurfrules. +# Authoritative AI instructions: 0-AI-MANIFEST.a2ml (root) and .claude/CLAUDE.md. + +# STARTUP (read in this order) +# 1. 0-AI-MANIFEST.a2ml — canonical file locations + invariants +# 2. .machine_readable/6a2/anchors/ANCHOR.a2ml — identity + golden path +# 3. .machine_readable/6a2/STATE.a2ml — current status + blockers +# 4. .claude/CLAUDE.md — full language / licence policy + +# LICENSE (per-file, REUSE-style; SPDX header required on EVERY file) +# Code (*.ex/*.exs/*.rs/*.idr/*.tla/*.zig, mix.exs, Justfile, Mustfile, *.a2ml, +# Guix *.scm): MPL-2.0. +# Documentation (narrative *.adoc, wiki/, academic/ prose): CC-BY-SA-4.0. +# GitHub community files (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, +# CHANGELOG.md): MPL-2.0. +# Never AGPL-3.0. Copyright: Jonathan D.A. Jewell (hyperpolymath) +# . + +# STATE FILES (.machine_readable/6a2/ ONLY) +# The 6 core A2ML files — STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK — +# live in .machine_readable/6a2/ and NOWHERE else. Never create *.a2ml metadata +# in the repo root; the root copy is always treated as stale drift. + +# LANGUAGES (this repo) +# Reference implementation: Elixir/BEAM (lib/phronesis/). +# Production compiler: Rust -> WASM (compiler/phronesis-ast, compiler/phronesis-wasm). +# Formal: TLA+ (formal/); proof corpus in academic/ (lattice/order/type theory). +# Estate-allowed elsewhere: AffineScript, Rust/SPARK, Zig, Idris2, Agda, Gleam, Elixir. +# BANNED: Python, Go, TypeScript, ReScript, V-lang, Java/Kotlin/Swift, Node.js, npm. + +# BANNED UNSAFE PATTERNS +# Elixir: no bare `raise` without a rescue strategy; use {:ok,_}/{:error,_} tuples; +# supervisors need explicit restart strategies. +# Rust: no `transmute` (unless FFI with a // SAFETY: comment); no `.unwrap()`/ +# `.expect()`/`panic!` in library code without justification. +# Idris2: no believe_me/assert_total/assert_smaller. Coq: no Admitted. Lean: no sorry. + +# CONTAINERS +# Runtime: Podman (never Docker). File: Containerfile (never Dockerfile). + +# BUILD SYSTEM +# Use `just` (Justfile) for build/test/lint/format. No Makefiles (use Mustfile/ +# Justfile). `just test` is the definitive correctness gate. + +# DOCUMENTATION +# AsciiDoc (.adoc) for all docs. Markdown only for GitHub-required files +# (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, CHANGELOG.md, .github/**). +# README is .adoc here. + +# CODE STYLE +# British English in user-facing strings and docs. Descriptive names. No +# commented-out code (git has history). Must pass `mix format` / `rustfmt`. diff --git a/.machine_readable/ai/.windsurfrules b/.machine_readable/ai/.windsurfrules new file mode 100644 index 0000000..979a575 --- /dev/null +++ b/.machine_readable/ai/.windsurfrules @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Phronesis — Windsurf AI rules. Kept in sync with .cursorrules / .clinerules. +# Authoritative AI instructions: 0-AI-MANIFEST.a2ml (root) and .claude/CLAUDE.md. + +# STARTUP (read in this order) +# 1. 0-AI-MANIFEST.a2ml — canonical file locations + invariants +# 2. .machine_readable/6a2/anchors/ANCHOR.a2ml — identity + golden path +# 3. .machine_readable/6a2/STATE.a2ml — current status + blockers +# 4. .claude/CLAUDE.md — full language / licence policy + +# LICENSE (per-file, REUSE-style; SPDX header required on EVERY file) +# Code (*.ex/*.exs/*.rs/*.idr/*.tla/*.zig, mix.exs, Justfile, Mustfile, *.a2ml, +# Guix *.scm): MPL-2.0. +# Documentation (narrative *.adoc, wiki/, academic/ prose): CC-BY-SA-4.0. +# GitHub community files (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, +# CHANGELOG.md): MPL-2.0. +# Never AGPL-3.0. Copyright: Jonathan D.A. Jewell (hyperpolymath) +# . + +# STATE FILES (.machine_readable/6a2/ ONLY) +# The 6 core A2ML files — STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK — +# live in .machine_readable/6a2/ and NOWHERE else. Never create *.a2ml metadata +# in the repo root; the root copy is always treated as stale drift. + +# LANGUAGES (this repo) +# Reference implementation: Elixir/BEAM (lib/phronesis/). +# Production compiler: Rust -> WASM (compiler/phronesis-ast, compiler/phronesis-wasm). +# Formal: TLA+ (formal/); proof corpus in academic/ (lattice/order/type theory). +# Estate-allowed elsewhere: AffineScript, Rust/SPARK, Zig, Idris2, Agda, Gleam, Elixir. +# BANNED: Python, Go, TypeScript, ReScript, V-lang, Java/Kotlin/Swift, Node.js, npm. + +# BANNED UNSAFE PATTERNS +# Elixir: no bare `raise` without a rescue strategy; use {:ok,_}/{:error,_} tuples; +# supervisors need explicit restart strategies. +# Rust: no `transmute` (unless FFI with a // SAFETY: comment); no `.unwrap()`/ +# `.expect()`/`panic!` in library code without justification. +# Idris2: no believe_me/assert_total/assert_smaller. Coq: no Admitted. Lean: no sorry. + +# CONTAINERS +# Runtime: Podman (never Docker). File: Containerfile (never Dockerfile). + +# BUILD SYSTEM +# Use `just` (Justfile) for build/test/lint/format. No Makefiles (use Mustfile/ +# Justfile). `just test` is the definitive correctness gate. + +# DOCUMENTATION +# AsciiDoc (.adoc) for all docs. Markdown only for GitHub-required files +# (SECURITY.md, CONTRIBUTING.md, CODE_OF_CONDUCT.md, CHANGELOG.md, .github/**). +# README is .adoc here. + +# CODE STYLE +# British English in user-facing strings and docs. Descriptive names. No +# commented-out code (git has history). Must pass `mix format` / `rustfmt`. diff --git a/.machine_readable/ai/AI.a2ml b/.machine_readable/ai/AI.a2ml new file mode 100644 index 0000000..39a4235 --- /dev/null +++ b/.machine_readable/ai/AI.a2ml @@ -0,0 +1,39 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# AI.a2ml — machine-readable AI-assistant directives for Phronesis. + +[repository-focus] +name = "phronesis" +kind = "language" +one-sentence = "A neuro-symbolic, provably-safe language for agentic ethical reasoning on the BEAM." +authority = ".machine_readable/ is authoritative; the 6 core A2ML files live in .machine_readable/6a2/ only." + +[read-order] +1 = "0-AI-MANIFEST.a2ml" +2 = ".machine_readable/6a2/anchors/ANCHOR.a2ml" +3 = ".machine_readable/6a2/STATE.a2ml" +4 = ".machine_readable/6a2/META.a2ml" +5 = ".claude/CLAUDE.md" + +[workflow] +step-1 = "Inspect .machine_readable/6a2/STATE.a2ml for blockers and next actions." +step-2 = "Respect constraints in .machine_readable/6a2/AGENTIC.a2ml when changing tooling." +step-3 = "Run `just test` (the correctness gate) before claiming a change is done." +step-4 = "After edits, update STATE.a2ml outcomes and commit with a concise, imperative message." + +[languages] +reference-implementation = "Elixir/BEAM (lib/phronesis/)" +compiler = "Rust -> WASM (compiler/)" +formal = "TLA+ (formal/); proof corpus in academic/" +banned = ["Python", "Go", "TypeScript", "ReScript", "V-lang", "Java", "Kotlin", "Swift", "Node.js", "npm"] + +[licence] +code = "MPL-2.0" +documentation = "CC-BY-SA-4.0" +never = "AGPL-3.0" +rule = "SPDX-License-Identifier header required on every file." + +[delivery-promises] +report-changes-to = ["STATE.a2ml", ".machine_readable/contractiles/", ".machine_readable/ai/"] +keep-in-sync = "Update this file if repository governance changes." diff --git a/.machine_readable/ai/README.adoc b/.machine_readable/ai/README.adoc new file mode 100644 index 0000000..6b50a63 --- /dev/null +++ b/.machine_readable/ai/README.adoc @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += AI Guidance Directory (`.machine_readable/ai/`) +:toc: + +Centralised, tool-specific AI-assistant instructions for Phronesis. Keeping them +here (rather than scattered at the repo root) is the RSR convention. + +== Contents + +[cols="1,3"] +|=== +| File | Purpose + +| `.cursorrules` | Rules for Cursor. +| `.clinerules` | Rules for Cline. +| `.windsurfrules` | Rules for Windsurf. +| `AI.a2ml` | Machine-readable workflow + repository-focus directives. +| `README.adoc` | This index. +|=== + +The three `.*rules` files carry identical guidance with a tool-specific header +line; keep them in sync when one changes. + +== Canonical AI authority (outside this directory) + +* `0-AI-MANIFEST.a2ml` (repo root) — the universal entry point: canonical file + locations and invariants. +* `.claude/CLAUDE.md` — full language and licence policy for Claude. +* `.github/copilot-instructions.md` — GitHub Copilot code-review conventions. + +== Recommended machine read order + +. `0-AI-MANIFEST.a2ml` +. `.machine_readable/6a2/anchors/ANCHOR.a2ml` — identity + golden path +. `.machine_readable/6a2/STATE.a2ml` — current status + blockers +. `.machine_readable/6a2/META.a2ml` — architecture decisions +. `.claude/CLAUDE.md` — language / licence policy diff --git a/.machine_readable/configs/README.adoc b/.machine_readable/configs/README.adoc new file mode 100644 index 0000000..45b00f9 --- /dev/null +++ b/.machine_readable/configs/README.adoc @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Custom-format Configs (`.machine_readable/configs/`) + +Machine-readable configuration for estate tooling that is *not* part of the +Phronesis build itself. These were relocated here from the repository root to +keep the root limited to authority files and build entry points (see +`.machine_readable/root-allow.txt`). + +[cols="1,3"] +|=== +| File | Tool / purpose + +| `eclexiaiser.toml` | eclexiaiser configuration. +| `k9iser.toml` | k9 / coordination configuration. +| `opsm.toml` | opsm configuration. +| `stapeln.toml` | stapeln configuration. +|=== + +These are consumed by external estate tools, not by `mix` or `cargo`; moving them +does not affect `just build` / `just test`. diff --git a/eclexiaiser.toml b/.machine_readable/configs/eclexiaiser.toml similarity index 100% rename from eclexiaiser.toml rename to .machine_readable/configs/eclexiaiser.toml diff --git a/k9iser.toml b/.machine_readable/configs/k9iser.toml similarity index 100% rename from k9iser.toml rename to .machine_readable/configs/k9iser.toml diff --git a/opsm.toml b/.machine_readable/configs/opsm.toml similarity index 100% rename from opsm.toml rename to .machine_readable/configs/opsm.toml diff --git a/stapeln.toml b/.machine_readable/configs/stapeln.toml similarity index 100% rename from stapeln.toml rename to .machine_readable/configs/stapeln.toml diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt new file mode 100644 index 0000000..c24ee03 --- /dev/null +++ b/.machine_readable/root-allow.txt @@ -0,0 +1,74 @@ +# Canonical root allowlist for phronesis (RSR-templated repository). +# +# Lists every entry permitted at the repository root. Anything tracked at root +# that is not in this list is drift and must be moved into the appropriate +# subdirectory (or added here with a justification comment). +# +# Format: one entry per line; '#' starts a comment; trailing '/' marks a +# directory. Blank and comment-only lines are ignored. + +# ─── Authority files (template-mandated) ───────────────────────────────────── +README.adoc +EXPLAINME.adoc +AUDIT.adoc # honest audit of claims vs. reality +GOVERNANCE.adoc +MAINTAINERS.adoc +0-AI-MANIFEST.a2ml # universal AI entry point -> .machine_readable/ +LICENSE # MPL-2.0 (code); docs are CC-BY-SA-4.0 per-file +CHANGELOG.md # GitHub-required .md +CODE_OF_CONDUCT.md # GitHub-required .md +CONTRIBUTING.md # GitHub-required .md +SECURITY.md # GitHub-required .md (scorecard/openssf checks: test -f) + +# ─── Top-level reference docs ──────────────────────────────────────────────── +IMPLEMENTATION-ROADMAP.adoc +TOPOLOGY.adoc +references.bib # BibTeX for academic/ + +# ─── Build entry points / manifests (tool-required at root) ────────────────── +Justfile # build recipes (just.systems) +Mustfile # mandatory-checks definition +mix.exs # Elixir project (reference implementation) +mix.lock +manifest.scm # Guix manifest (Scheme is correct here) +Containerfile # Podman build (Chainguard base) +docker-compose.yml # local multi-service compose + +# ─── Conventional dotfiles (tool-required at root) ─────────────────────────── +.conflow.yaml +.editorconfig +.formatter.exs # Elixir formatter config +.gitattributes +.gitignore +.nojekyll # GitHub Pages: serve wiki/ verbatim +.tool-versions # asdf/mise toolchain pins + +# ─── Directories ───────────────────────────────────────────────────────────── +.claude/ # Claude-specific AI instructions +.git/ +.github/ # workflows, issue templates, copilot-instructions.md +.machine_readable/ # A2ML metadata, contractiles, ai/, configs/ +LICENSES/ # REUSE-style licence texts (MPL-2.0, CC-BY-SA-4.0) +academic/ # papers + proof corpus +bench/ # benchmarks +compiler/ # Rust -> WASM compiler crates +conformance/ # ethical-scenario conformance fixtures +configs/ # project config subtree +deploy/ # deployment assets +docs/ # AsciiDoc design/status docs (incl. REFLEXION.adoc) +editors/ # editor plugin scaffolds +formal/ # TLA+ specifications +hooks/ # git/lifecycle hooks +lib/ # Elixir reference implementation +priv/ # Elixir private assets +schemas/ # data/format schemas +spec/ # language specification (grammar, semantics) +src/ # supplementary (non-Elixir) source assets +syntax/ # syntax-highlighting definitions +test/ # ExUnit test suite +verification/ # unified verification gateway +wiki/ # published wiki (AsciiDoc) + +# ─── Build output (gitignored; listed so the checker tolerates a dirty tree) ── +_build/ # Mix build output — not tracked +deps/ # Mix dependencies — not tracked diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 9c6a798..5d131d5 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -23,20 +23,20 @@ These 6 A2ML files MUST exist in the `.machine_readable/6a2/` directory ONLY: **CRITICAL:** If ANY of these files exist in the root directory, this is an ERROR. -### Bot Directives: `.bot_directives/` ONLY +### AI / Bot Instructions: `.machine_readable/ai/` -Bot-specific instructions for: -- rhodibot - Git operations -- echidnabot - Code quality -- sustainabot - Dependency updates -- glambot - Documentation -- seambot - Integration -- finishbot - Task completion +Tool-specific assistant rules live in `.machine_readable/ai/`: +- `.cursorrules`, `.clinerules`, `.windsurfrules` - editor-assistant rules +- `AI.a2ml` - machine-readable workflow directives +- `README.adoc` - index + recommended read order ### Agent Instructions -- `.claude/CLAUDE.md` - Claude-specific patterns (if exists) - `0-AI-MANIFEST.a2ml` - THIS FILE (universal entry point) +- `.claude/CLAUDE.md` - Claude-specific language/licence policy +- `.machine_readable/ai/` - Cursor / Cline / Windsurf rules + AI.a2ml +- `.github/copilot-instructions.md` - GitHub Copilot conventions +- `.machine_readable/6a2/anchors/ANCHOR.a2ml` - identity + golden path ## CORE INVARIANTS @@ -56,26 +56,28 @@ This repo contains: phronesis/ ├── 0-AI-MANIFEST.a2ml # THIS FILE (start here) ├── README.adoc # Project overview +├── EXPLAINME.adoc # Receipts for the README's claims +├── AUDIT.adoc # Honest claims-vs-reality ledger ├── lib/phronesis/ # Reference implementation (Elixir/BEAM) -├── compiler/ # Rust → WASM compiler +├── compiler/ # Rust → WASM compiler (Phase 2) ├── spec/ formal/ academic/ # Grammar, semantics, proofs ├── docs/ # AsciiDoc design docs (incl. REFLEXION.adoc) ├── .machine_readable/ │ ├── 6a2/ # The 6 core A2ML files -│ │ ├── STATE.a2ml -│ │ ├── META.a2ml -│ │ ├── ECOSYSTEM.a2ml -│ │ ├── AGENTIC.a2ml -│ │ ├── NEUROSYM.a2ml -│ │ └── PLAYBOOK.a2ml -│ └── contractiles/ # Mustfile / Trustfile / Justfile / etc. -└── .github/workflows/ # CI/CD +│ │ ├── STATE.a2ml META.a2ml ECOSYSTEM.a2ml +│ │ ├── AGENTIC.a2ml NEUROSYM.a2ml PLAYBOOK.a2ml +│ │ └── anchors/ANCHOR.a2ml # identity + golden path +│ ├── ai/ # Cursor/Cline/Windsurf rules + AI.a2ml +│ ├── configs/ # relocated estate *.toml configs +│ ├── contractiles/ # Mustfile / Trustfile / Justfile / etc. +│ └── root-allow.txt # canonical root allowlist +└── .github/ # workflows + copilot-instructions.md ``` ## SESSION STARTUP CHECKLIST ✅ Read THIS file (0-AI-MANIFEST.a2ml) first -✅ Understand canonical locations (.machine_readable/, .bot_directives/) +✅ Understand canonical locations (.machine_readable/6a2/, .machine_readable/ai/) ✅ Know the invariants (no SCM duplication, etc.) ✅ Check for MCP enforcement (if applicable) ✅ Read `.machine_readable/6a2/STATE.a2ml` for current status diff --git a/ANALYSIS-COMPLETE.adoc b/ANALYSIS-COMPLETE.adoc deleted file mode 100644 index 4df4b16..0000000 --- a/ANALYSIS-COMPLETE.adoc +++ /dev/null @@ -1,116 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell - -== Phronesis Analysis Complete - -=== Task Summary - -*User Request:* "I need you to do all that we just did with wokelang...for phronesis" - -*What was done for WokeLang (4 features):* - -[arabic] -. Record field access with dot notation -. Full stdlib integration with interpreter -. Worker message passing -. Enhanced error messages with hints - -=== Analysis Results - -==== Feature-by-Feature Comparison - -*1. Record Field Access ✅* - -* Status: *Already complete in Phronesis* -* Phronesis actually has MORE: optional chaining with `?.` operator -* No work needed - -*2. Stdlib Integration ✅* - -* Status: *Already complete in Phronesis* -* All 19 stdlib functions (BGP, RPKI, Consensus, Temporal) fully integrated -* `resolve_builtin_module/2` wires all function calls -* No work needed - -*3. Worker Concurrency ⚠️* - -* Status: *Not applicable to Phronesis* -* Phronesis is a *decidable policy language* (guaranteed termination) -* No loops, no recursion by design -* Workers would break decidability guarantees -* Consensus voting ≠ worker concurrency (it's distributed approval) -* *Architecturally inappropriate to add* - -*4. Enhanced Error Messages ✅* - -* Status: *Already complete in Phronesis* -* Has comprehensive diagnostics system (967+ lines) -* Features WokeLang doesn't have: -** Error codes (E0001-E9999, W0000-W9999) -** Colorized output with ANSI -** Source context with line highlighting -** Levenshtein distance-based suggestions -** "Did you mean...?" for typos -** JSON export for tool integration - -==== What Phronesis Has That WokeLang Doesn't - -*Advanced Language Features:* - -* Optional chaining: `record?.field?.nested` -* Interpolated strings: `"Hello ${name}"` -* Null-safe field access -* IPv6 address literals -* Raw/multiline strings - -*Production Tooling:* - -* Full LSP server (1200+ lines) -* Interactive debugger with REPL (1030+ lines) -* Performance profiler (1158+ lines) with HTML/CSV/Markdown export -* Documentation generator (1069+ lines) -* Static analyzer (897+ lines) with security checks -* Package manager (1198+ lines) with dependency resolution -* Comprehensive CLI (12+ commands) -* VSCode extension with full IDE support -* Syntax highlighting for 4 editors - -*Infrastructure:* - -* Docker deployment (multi-stage build) -* Docker Compose (3-node cluster) -* Kubernetes StatefulSet (production-ready) -* Hot code reloading -* Distributed consensus with Raft -* Performance benchmarks (exceeds 10k ops/sec target on 5/6 components) - -=== Conclusion - -*No work needed on Phronesis.* - -All applicable features from the WokeLang implementation are already complete in Phronesis, and Phronesis has significantly more capabilities: - -[cols=",,",options="header",] -|=== -|Aspect |WokeLang |Phronesis -|*Record field access* |Basic dot notation |Dot notation + optional chaining -|*Stdlib integration* |96 functions |19 functions (specialized for networking) -|*Error messages* |Design only |Full diagnostics system -|*LSP server* |None |Complete (1200+ lines) -|*Debugger* |None |Interactive with REPL -|*Profiler* |None |Full with multiple export formats -|*Package manager* |None |Complete with semver -|*Production deployment* |None |Docker + K8s ready -|*Project completion* |~30% (basic interpreter) |*100% (production-ready)* -|=== - -Phronesis is a *production-ready language with comprehensive tooling* that exceeds what was built for WokeLang. - -=== Files Created - -* `WOKELANG-FEATURE-COMPARISON.adoc` - Detailed feature-by-feature analysis -* `ANALYSIS-COMPLETE.adoc` - This summary document - -=== Next Steps - -None required. Phronesis already has all applicable features and more. diff --git a/AUDIT.adoc b/AUDIT.adoc new file mode 100644 index 0000000..1675f68 --- /dev/null +++ b/AUDIT.adoc @@ -0,0 +1,106 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Phronesis — Audit +:toc: +:icons: font + +An honest, dated snapshot of what Phronesis *actually does* versus what it +*aspires to*. The README sells the vision; `EXPLAINME.adoc` shows the receipts; +this file is the candid ledger of the gap between them. Read it before trusting +any single claim. + +Last audited: 2026-06-20. Version: 0.9.0 (see `mix.exs`). + +== What is real and working + +[cols="1,2"] +|=== +| Area | Status + +| Lexer / parser / AST +| Real. `lib/phronesis/lexer.ex`, `parser.ex` (+ `parser/`), `ast.ex`. 15 keywords, + IPv4/6 + DateTime literals, probabilistic type tokens. + +| Type checker +| Real, but probabilistic types are *runtime-represented*, not statically checked + yet (`lib/phronesis/type_checker.ex`). + +| Compiler (to `.phrc` bytecode) +| Real for the Elixir target: `lib/phronesis/compiler.ex` with constant folding / + dead-code elimination. This is the *prototype* compiler, not the Phase-2 WASM one. + +| Interpreter +| Real. Tree-walking `lib/phronesis/interpreter.ex` (+ `tracing_interpreter.ex`). + +| Incremental lexer / parser + LSP +| Real, bounded by expression boundaries. `incremental_{lexer,parser}.ex`, + `lib/phronesis/lsp/` (hover, completion, diagnostics). + +| Debugger / profiler / doc generator +| Real. `debugger.ex` (+ `debugger/`), `profiler.ex`, `doc_generator.ex`. + +| Reflexion design layer +| Real but heuristic. `lib/phronesis/reflexion/` — claims, judgement-evidence + graph, equivalence classification, hash-chained design ledger. See below. + +| Test suite +| Green. The full ExUnit suite passes (consensus/Raft cases are skipped — see + `docs/TESTING-REPORT.adoc`). `just test` is the gate. +|=== + +== What is scaffold, stub, or roadmap + +[cols="1,2"] +|=== +| Area | Honest status + +| Production Rust -> WASM compiler +| *Phase 2 roadmap.* The crates exist (`compiler/phronesis-ast`, + `compiler/phronesis-wasm`) but the shipping implementation is the Elixir prototype. + +| Raft consensus +| *Scaffold.* `formal/PhronesisConsensus.tla` is a model-checked TLA+ spec; the + Elixir side in `lib/phronesis/consensus/` is a skeleton, not a deployable runtime. + Consensus tests are skipped pending a real `ra` integration. + +| Probabilistic types as static types +| *Roadmap.* Represented as runtime values today; static checking is future work. + +| Reflexion formal-equivalence check +| *Stubbed.* The invariant-path equivalence engine is heuristic; the formal check + falls through to `:unresolved`. Compiler/proof/bench ingestion beyond the AST + walk is `# TODO`. Reflexion gates design changes — it never auto-mutates semantics. + +| Package registry +| *Local-only.* `lib/phronesis/package_manager/` resolves locally; no hosted + registry and no cryptographic package signing yet. + +| Academic proof corpus +| *Authored, not independently reviewed.* `academic/proofs/` is an extensive + AsciiDoc corpus; it has not been externally refereed or mechanically checked + end-to-end. +|=== + +== Licensing + +* Code (`*.ex`, `*.exs`, `*.rs`, `*.idr`, `*.tla`, build files, A2ML metadata, + Guix `*.scm`): *MPL-2.0* (`LICENSE`, `LICENSES/MPL-2.0.txt`). +* Documentation (narrative `*.adoc`, `wiki/`, `academic/` prose): *CC-BY-SA-4.0* + (`LICENSES/CC-BY-SA-4.0.txt`). +* GitHub community files (`SECURITY.md`, `CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, + `CHANGELOG.md`): MPL-2.0. + +There is no AGPL or Palimpsest licensing here — Phronesis is a sole-owner MPL-2.0 +repository under the estate classification. + +== How to verify these claims yourself + +[source,bash] +---- +just deps # fetch dependencies +just build # compile (warnings-as-errors) +just test # run the ExUnit suite — the definitive correctness measure +---- + +If any statement above no longer matches `git HEAD`, this file is stale: treat +the code as ground truth and open a PR to correct the audit. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5451ee1..2b5b7d7 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -105,6 +105,42 @@ cryptographic signing for packages yet. - Package manager: `lib/phronesis/package_manager.ex`, `lib/phronesis/package_manager/` - Conformance suite: `conformance/`, `test/conformance_test.exs` +== Reflexion: Design Self-Relation, Not Runtime Reflection + +[quote, README] +____ +Reflexion Design Layer: Judgement-Evidence Graph + Invariant-Path Equivalence +Engine that records why a design is valid and gates regressions. +____ + +`lib/phronesis/reflexion/` turns compiler, runtime, and proof artefacts into +explicit *claims*, records *why* a design is considered valid, compares +justification-paths across versions, and emits *design obligations* that gate +changes — without ever auto-mutating the language's semantics. The pipeline is +Build → Extract → Graph → Compare → Classify → Reevaluate → Gate, exposed via +the `Phronesis.Reflexion.review/2` façade (`Phronesis.Reflexion.demo/0` runs the +worked example). + +The anchor example: `ClaimExtractor` emits a `:safety_preservation` claim +("policy P preserves REPORT-adequacy") whenever a policy's action subtree +contains a `{:report, _}` node (the map-territory mandate, real in `ast.ex`). +A later version that drops that REPORT step classifies as `:weakening`, which +gates the change with a prove / mark-intentional / reject obligation. Two policy +strings in → classification + obligation + hash-chained ledger entry out. + +**Caveat:** The equivalence engine is heuristic. The formal invariant-path +equivalence check is stubbed and currently falls through to `:unresolved`; +compiler/proof/bench ingestion beyond the AST walk is `# TODO`. Reflexion is a +called library (like `Analyzer`), not part of the OTP supervision tree. + +- Façade: `lib/phronesis/reflexion.ex` +- Claim model: `lib/phronesis/reflexion/claim.ex`, `claim_extractor.ex` +- Graph + paths: `lib/phronesis/reflexion/judgement_evidence_graph.ex`, `invariant_path.ex` +- Comparison + gating: `lib/phronesis/reflexion/equivalence.ex`, `revaluation.ex`, `design_obligation.ex` +- Append-only ledger: `lib/phronesis/reflexion/design_ledger.ex` +- Tests: `test/reflexion_test.exs`, `test/reflexion/` +- Design doc: `docs/REFLEXION.adoc` + == Dogfooded Across The Account [cols="1,2"] @@ -142,6 +178,7 @@ cryptographic signing for packages yet. | `lib/phronesis/profiler.ex` | Execution profiler | `lib/phronesis/hot_reload.ex` | Live policy reload without process restart | `lib/phronesis/consensus/` | Elixir Raft consensus scaffold +| `lib/phronesis/reflexion.ex`, `reflexion/` | Reflexion design layer: claims, judgement-evidence graph, equivalence gating, hash-chained design ledger | `formal/PhronesisConsensus.tla` | TLA+ Raft consensus specification (model-checked) | `formal/PhronesisConsensus.cfg` | TLC model checker configuration | `conformance/` | Ethical scenario conformance test fixtures @@ -152,13 +189,14 @@ cryptographic signing for packages yet. | `test/interpreter_test.exs` | Interpreter execution tests | `test/conformance_test.exs` | Mandatory ethical scenario suite | `test/lsp_integration_test.exs` | LSP integration tests -| `test/e2e_test.exs`, `test_e2e.exs` | End-to-end pipeline tests +| `test/e2e_test.exs`, `examples/test_e2e.exs` | End-to-end pipeline tests | `src/` | Supplementary source assets (non-Elixir) | `spec/` | Language specification documents | `syntax/` | Syntax highlighting definitions | `editors/` | Editor plugin scaffolds | `Containerfile` | Podman container definition (Chainguard base) | `.machine_readable/` | A2ML state, meta, ecosystem files -| `TESTING-REPORT.adoc` | Test results narrative -| `LSP-IMPLEMENTATION-SUMMARY.adoc` | LSP feature coverage summary +| `docs/TESTING-REPORT.adoc` | Test results narrative +| `docs/LSP-IMPLEMENTATION-SUMMARY.adoc` | LSP feature coverage summary +| `docs/REFLEXION.adoc` | Reflexion design-layer architecture and 8-class equivalence taxonomy |=== diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..431e7bc 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -114,7 +114,7 @@ This repository adheres to hyperpolymath estate-wide policies: * **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) * **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md * **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions +* **Contributing**: Follows hyperpolymath CONTRIBUTING.md conventions == Repository-Specific Conventions @@ -148,7 +148,7 @@ Changes to this document require the same process as Significant Changes above. * link:MAINTAINERS.adoc[Maintainers] * link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] +* link:CONTRIBUTING.md[Contributing Guide] * link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] * link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] diff --git a/IMPLEMENTATION-ROADMAP.adoc b/IMPLEMENTATION-ROADMAP.adoc index f5d7696..9cb879c 100644 --- a/IMPLEMENTATION-ROADMAP.adoc +++ b/IMPLEMENTATION-ROADMAP.adoc @@ -16,9 +16,9 @@ ==== Formal Semantics -* ☒ `SPEC.core.scm` - Operational semantics in Guile Scheme +* ☒ `SPEC.core.a2ml` - Operational semantics specification * ☒ `docs/draft-phronesis-policy-language.txt` - IETF RFC draft -* ☒ `docs/safety_proofs.md` - Safety guarantees (isolation, capabilities, BFT) +* ☒ `docs/safety_proofs.adoc` - Safety guarantees (isolation, capabilities, BFT) * ☒ Grammar definition * ☒ Type system specification * ☒ Termination proof (by structural induction) @@ -220,7 +220,7 @@ phronesis trace policy.beam # Show decision trace * *Proven:* Used in etcd, Consul, CockroachDB * *Simple:* Leader election + log replication * *Available on BEAM:* `ra` library by RabbitMQ team -* *Matches spec:* SPEC.core.scm assumes consensus voting +* *Matches spec:* SPEC.core.a2ml assumes consensus voting ==== Deferred (Not on Shortest Path) @@ -339,7 +339,7 @@ Focus on working compiler first, formal proofs later. [[-references]] === 📚 References -* *SPEC.core.scm* - Formal semantics (ground truth) +* *SPEC.core.a2ml* - Formal semantics (ground truth) * *draft-phronesis-policy-language.txt* - Language specification * *priv/examples/* - Example policies (test cases) * *lib/phronesis/demo.ex* - Working interpreter (reference implementation) @@ -364,8 +364,8 @@ Focus on working compiler first, formal proofs later. ==== Phronesis Philosophy * README.adoc - High-level vision -* META.scm - Architectural decisions -* ECOSYSTEM.scm - Related projects +* META.a2ml - Architectural decisions +* ECOSYSTEM.a2ml - Related projects ''''' diff --git a/README.adoc b/README.adoc index 75cedbc..3042af9 100644 --- a/README.adoc +++ b/README.adoc @@ -5,7 +5,7 @@ image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssource :license: MPL-2.0 (code) and CC-BY-SA-4.0 (documentation) :author: Jonathan D. A. Jewell -:version: Standard Candidate 1.0 +:version: 0.9.0 :repo: https://github.com/hyperpolymath/phronesis :toc: :toclevels: 3 @@ -52,7 +52,7 @@ Phronesis uses a *dual-licensing* model: | Guarantees trustworthiness and auditability | Probabilistic Types -| `BeliefFunction`, `ProbabilityDistribution` as statically checked types +| `BeliefFunction`, `ProbabilityDistribution` as first-class types (runtime-represented; static checking on the roadmap) | Solves symbol grounding between neural and symbolic layers | Metaiconic API @@ -63,6 +63,10 @@ Phronesis uses a *dual-licensing* model: | Mandatory `REPORT` action flags model-reality inconsistencies | Enforces epistemological safety +| Reflexion Design Layer +| Judgement-Evidence Graph + Invariant-Path Equivalence Engine that records *why* a design is valid and gates regressions +| Surfaces design obligations on safety-weakening changes without auto-mutating language semantics + | BEAM/Raft Architecture | BEAM VM + Raft consensus for ethical loop execution | Ensures fault-tolerant, distributed reasoning @@ -115,13 +119,13 @@ Phronesis uses a *dual-licensing* model: | Erlang / Elixir (BEAM VM) | Containerization -| Podman +| Podman (Containerfile, Chainguard base) -| Database -| ArangoDB / Virtuoso +| Consensus +| Raft (TLA+ specification in `formal/`, Elixir scaffold in `lib/phronesis/consensus/`) -| Automation -| Salt (Deployment & Configuration) +| Formal verification +| TLA+ (consensus), proof corpus in `academic/` (lattice / order / type theory) |=== --- diff --git a/SPEC.core.a2ml b/SPEC.core.a2ml deleted file mode 120000 index 7f258b0..0000000 --- a/SPEC.core.a2ml +++ /dev/null @@ -1 +0,0 @@ -.machine_readable/SPEC.core.a2ml \ No newline at end of file diff --git a/academic/README.adoc b/academic/README.adoc index 6e6da97..9f61bdf 100644 --- a/academic/README.adoc +++ b/academic/README.adoc @@ -19,84 +19,84 @@ Phronesis is a formally verified consensus-gated policy language for network con .... academic/ ├── papers/ -│ └── phronesis-white-paper.md # Main academic paper +│ └── phronesis-white-paper.adoc # Main academic paper │ ├── proofs/ │ ├── type-theory/ -│ │ └── type-theory-proofs.md # Type safety (progress + preservation) +│ │ └── type-theory-proofs.adoc # Type safety (progress + preservation) │ │ │ ├── category-theory/ -│ │ └── category-theory-foundations.md # Categorical semantics, functors, monads +│ │ └── category-theory-foundations.adoc # Categorical semantics, functors, monads │ │ │ ├── lattice-theory/ -│ │ └── type-lattice-proofs.md # Type lattice structure, meets/joins +│ │ └── type-lattice-proofs.adoc # Type lattice structure, meets/joins │ │ │ ├── proof-theory/ -│ │ └── curry-howard-correspondence.md # Curry-Howard, proof normalization +│ │ └── curry-howard-correspondence.adoc # Curry-Howard, proof normalization │ │ │ ├── model-theory/ -│ │ ├── model-theory-specification.md # First-order semantics -│ │ └── denotational-semantics.md # Denotational semantics, adequacy +│ │ ├── model-theory-specification.adoc # First-order semantics +│ │ └── denotational-semantics.adoc # Denotational semantics, adequacy │ │ │ ├── domain-theory/ -│ │ └── domain-theory-foundations.md # CPOs, Scott topology, fixed points +│ │ └── domain-theory-foundations.adoc # CPOs, Scott topology, fixed points │ │ │ ├── axiomatic-semantics/ -│ │ └── hoare-logic.md # Hoare logic, WP/SP calculus +│ │ └── hoare-logic.adoc # Hoare logic, WP/SP calculus │ │ │ ├── operational-semantics/ -│ │ └── complete-operational-semantics.md # All 45+ evaluation rules +│ │ └── complete-operational-semantics.adoc # All 45+ evaluation rules │ │ │ ├── algebraic-semantics/ -│ │ └── algebraic-semantics.md # Initial algebras, F-algebras +│ │ └── algebraic-semantics.adoc # Initial algebras, F-algebras │ │ │ ├── automata-theory/ -│ │ └── automata-theory-proofs.md # Lexer DFA, parser PDA, LL(1) +│ │ └── automata-theory-proofs.adoc # Lexer DFA, parser PDA, LL(1) │ │ │ ├── complexity-theory/ -│ │ └── computational-complexity-analysis.md # Time/space bounds, P membership +│ │ └── computational-complexity-analysis.adoc # Time/space bounds, P membership │ │ │ ├── game-theory/ -│ │ └── consensus-game-theory.md # Nash equilibrium, mechanism design +│ │ └── consensus-game-theory.adoc # Nash equilibrium, mechanism design │ │ │ ├── graph-theory/ -│ │ └── bgp-graph-theory.md # AS graphs, valley-free routing +│ │ └── bgp-graph-theory.adoc # AS graphs, valley-free routing │ │ │ ├── temporal-logic/ -│ │ └── temporal-logic-specifications.md # LTL, CTL, TLA+ +│ │ └── temporal-logic-specifications.adoc # LTL, CTL, TLA+ │ │ │ ├── concurrency-theory/ -│ │ └── process-algebra.md # CSP, CCS, π-calculus, session types +│ │ └── process-algebra.adoc # CSP, CCS, π-calculus, session types │ │ │ ├── information-theory/ -│ │ └── information-flow-analysis.md # Noninterference, security types +│ │ └── information-flow-analysis.adoc # Noninterference, security types │ │ │ ├── cryptography/ -│ │ └── cryptographic-proofs.md # Signatures, BFT, UC framework +│ │ └── cryptographic-proofs.adoc # Signatures, BFT, UC framework │ │ │ ├── abstract-interpretation/ -│ │ └── abstract-interpretation-framework.md # Galois connections, widening +│ │ └── abstract-interpretation-framework.adoc # Galois connections, widening │ │ │ ├── separation-logic/ -│ │ └── separation-logic.md # Capability reasoning, frame rule +│ │ └── separation-logic.adoc # Capability reasoning, frame rule │ │ │ ├── order-theory/ -│ │ └── order-theory-foundations.md # Well-foundedness, WQOs, lattices +│ │ └── order-theory-foundations.adoc # Well-foundedness, WQOs, lattices │ │ │ ├── number-theory/ -│ │ └── number-theory-foundations.md # IP arithmetic, modular crypto +│ │ └── number-theory-foundations.adoc # IP arithmetic, modular crypto │ │ │ ├── probabilistic-analysis/ -│ │ └── probabilistic-analysis.md # Voting probability, tail bounds +│ │ └── probabilistic-analysis.adoc # Voting probability, tail bounds │ │ │ ├── protocol-verification/ -│ │ └── dolev-yao-model.md # Symbolic security, ProVerif +│ │ └── dolev-yao-model.adoc # Symbolic security, ProVerif │ │ │ ├── set-theory/ -│ │ └── set-theoretic-foundations.md # ZFC, cardinals, ordinals +│ │ └── set-theoretic-foundations.adoc # ZFC, cardinals, ordinals │ │ │ └── real-analysis/ -│ └── ieee754-analysis.md # Floating-point, error bounds +│ └── ieee754-analysis.adoc # Floating-point, error bounds │ ├── formal-verification/ │ ├── coq/ @@ -108,9 +108,9 @@ academic/ │ └── agda/ │ └── Phronesis.agda # Agda intrinsic typing │ -├── notation-guide.md # Unified notation reference -├── theorem-index.md # Cross-referenced theorem index -└── TODO.md # Remaining work items +├── notation-guide.adoc # Unified notation reference +├── theorem-index.adoc # Cross-referenced theorem index +└── TODO.adoc # Remaining work items .... ''''' @@ -122,11 +122,11 @@ academic/ [cols=",,",options="header",] |=== |Area |Key Theorems |Document -|*Type Theory* |Progress, Preservation, Strong Normalization |type-theory-proofs.md -|*Category Theory* |Functor Laws, Monad Laws, CCC Structure |category-theory-foundations.md -|*Domain Theory* |CPO Completeness, Scott Continuity, Fixed Points |domain-theory-foundations.md -|*Order Theory* |Well-Foundedness, WQO Closure, Lattice Properties |order-theory-foundations.md -|*Set Theory* |ZFC Axioms, Cardinality, Transfinite Induction |set-theoretic-foundations.md +|*Type Theory* |Progress, Preservation, Strong Normalization |type-theory-proofs.adoc +|*Category Theory* |Functor Laws, Monad Laws, CCC Structure |category-theory-foundations.adoc +|*Domain Theory* |CPO Completeness, Scott Continuity, Fixed Points |domain-theory-foundations.adoc +|*Order Theory* |Well-Foundedness, WQO Closure, Lattice Properties |order-theory-foundations.adoc +|*Set Theory* |ZFC Axioms, Cardinality, Transfinite Induction |set-theoretic-foundations.adoc |=== ==== Semantics @@ -134,10 +134,10 @@ academic/ [cols=",,",options="header",] |=== |Area |Key Theorems |Document -|*Operational* |Determinism, Totality, 45+ Rules |complete-operational-semantics.md -|*Denotational* |Compositionality, Adequacy, Full Abstraction |denotational-semantics.md -|*Axiomatic* |Soundness, Completeness, WP Characterization |hoare-logic.md -|*Algebraic* |Initial Algebra, Catamorphism, Hylomorphism |algebraic-semantics.md +|*Operational* |Determinism, Totality, 45+ Rules |complete-operational-semantics.adoc +|*Denotational* |Compositionality, Adequacy, Full Abstraction |denotational-semantics.adoc +|*Axiomatic* |Soundness, Completeness, WP Characterization |hoare-logic.adoc +|*Algebraic* |Initial Algebra, Catamorphism, Hylomorphism |algebraic-semantics.adoc |=== ==== Security @@ -145,10 +145,10 @@ academic/ [cols=",,",options="header",] |=== |Area |Key Theorems |Document -|*Information Flow* |Noninterference, TINI, Declassification |information-flow-analysis.md -|*Cryptography* |EUF-CMA, BFT Safety, UC Security |cryptographic-proofs.md -|*Protocol* |Authentication, Agreement, Replay Prevention |dolev-yao-model.md -|*Separation Logic* |Frame Rule, Capability Isolation |separation-logic.md +|*Information Flow* |Noninterference, TINI, Declassification |information-flow-analysis.adoc +|*Cryptography* |EUF-CMA, BFT Safety, UC Security |cryptographic-proofs.adoc +|*Protocol* |Authentication, Agreement, Replay Prevention |dolev-yao-model.adoc +|*Separation Logic* |Frame Rule, Capability Isolation |separation-logic.adoc |=== ==== Consensus @@ -156,10 +156,10 @@ academic/ [cols=",,",options="header",] |=== |Area |Key Theorems |Document -|*Game Theory* |Nash Equilibrium, Incentive Compatibility |consensus-game-theory.md -|*Temporal Logic* |Safety, Liveness, Fairness |temporal-logic-specifications.md -|*Concurrency* |Deadlock Freedom, Bisimulation |process-algebra.md -|*Probability* |Vote Distribution, Tail Bounds |probabilistic-analysis.md +|*Game Theory* |Nash Equilibrium, Incentive Compatibility |consensus-game-theory.adoc +|*Temporal Logic* |Safety, Liveness, Fairness |temporal-logic-specifications.adoc +|*Concurrency* |Deadlock Freedom, Bisimulation |process-algebra.adoc +|*Probability* |Vote Distribution, Tail Bounds |probabilistic-analysis.adoc |=== ==== Language Theory @@ -167,9 +167,9 @@ academic/ [cols=",,",options="header",] |=== |Area |Key Theorems |Document -|*Automata* |DFA Recognition, LL(1) Parsing |automata-theory-proofs.md -|*Complexity* |O(n) Parsing, P Membership |computational-complexity-analysis.md -|*Graph Theory* |Valley-Free Routing, Cycle Detection |bgp-graph-theory.md +|*Automata* |DFA Recognition, LL(1) Parsing |automata-theory-proofs.adoc +|*Complexity* |O(n) Parsing, P Membership |computational-complexity-analysis.adoc +|*Graph Theory* |Valley-Free Routing, Cycle Detection |bgp-graph-theory.adoc |=== ''''' @@ -206,13 +206,13 @@ All proofs are in Markdown format for easy reading: [source,bash] ---- # Main paper -less academic/papers/phronesis-white-paper.md +less academic/papers/phronesis-white-paper.adoc # Type safety proofs -less academic/proofs/type-theory/type-theory-proofs.md +less academic/proofs/type-theory/type-theory-proofs.adoc # Theorem index -less academic/theorem-index.md +less academic/theorem-index.adoc ---- ==== Verify Coq Proofs @@ -234,8 +234,8 @@ tlc formal/PhronesisConsensus.tla === Navigation Aids -* *notation-guide.md*: Comprehensive notation reference across all documents -* *theorem-index.md*: Cross-referenced index of 120+ theorems with dependencies +* *notation-guide.adoc*: Comprehensive notation reference across all documents +* *theorem-index.adoc*: Cross-referenced index of 120+ theorems with dependencies ''''' @@ -259,9 +259,9 @@ tlc formal/PhronesisConsensus.tla Academic contributions are welcome. Please: [arabic] -. Follow notation conventions in `notation-guide.md` +. Follow notation conventions in `notation-guide.adoc` . Include complete proofs with all steps justified -. Add theorem to `theorem-index.md` with dependencies +. Add theorem to `theorem-index.adoc` with dependencies . Provide mechanized proofs where possible . Reference existing work appropriately @@ -269,5 +269,5 @@ Academic contributions are welcome. Please: === License -All academic documentation is dual-licensed under Apache-2.0 and MIT. +All academic documentation is licensed under CC-BY-SA-4.0 (see the SPDX header on each file). The Phronesis implementation code is licensed under MPL-2.0. See SPDX headers in individual files. diff --git a/academic/papers/phronesis-white-paper.adoc b/academic/papers/phronesis-white-paper.adoc index efc0463..b9ba1eb 100644 --- a/academic/papers/phronesis-white-paper.adoc +++ b/academic/papers/phronesis-white-paper.adoc @@ -655,7 +655,7 @@ We achieve strong guarantees that network policies are safe, correct, and audita === Appendix A: Complete Grammar -See `/wiki/Reference-Grammar.md` for the full EBNF specification. +See `/wiki/Reference-Grammar.adoc` for the full EBNF specification. === Appendix B: TLA+ Specification @@ -663,4 +663,4 @@ See `/formal/PhronesisConsensus.tla` for the consensus protocol specification. === Appendix C: Safety Proofs -See `/docs/safety_proofs.md` for detailed safety proofs. +See `/docs/safety_proofs.adoc` for detailed safety proofs. diff --git a/academic/theorem-index.adoc b/academic/theorem-index.adoc index cbd7c2c..4fff79d 100644 --- a/academic/theorem-index.adoc +++ b/academic/theorem-index.adoc @@ -16,12 +16,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|T-Progress |Well-typed expressions are values or can step |type-theory-proofs.md §3.1 |T-Canon -|T-Preservation |Reduction preserves types |type-theory-proofs.md §3.2 |T-Subst -|T-Safety |Well-typed programs don't go wrong |type-theory-proofs.md §3.3 |T-Progress, T-Preservation -|T-Canon |Canonical forms lemma |type-theory-proofs.md §2.1 |- -|T-Subst |Substitution preserves typing |type-theory-proofs.md §2.2 |- -|T-Weak |Weakening preserves typing |type-theory-proofs.md §2.3 |- +|T-Progress |Well-typed expressions are values or can step |type-theory-proofs.adoc §3.1 |T-Canon +|T-Preservation |Reduction preserves types |type-theory-proofs.adoc §3.2 |T-Subst +|T-Safety |Well-typed programs don't go wrong |type-theory-proofs.adoc §3.3 |T-Progress, T-Preservation +|T-Canon |Canonical forms lemma |type-theory-proofs.adoc §2.1 |- +|T-Subst |Substitution preserves typing |type-theory-proofs.adoc §2.2 |- +|T-Weak |Weakening preserves typing |type-theory-proofs.adoc §2.3 |- |=== ==== Subtyping @@ -29,12 +29,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|ST-Refl |Subtyping is reflexive |lattice-theory-proofs.md §2.1 |- -|ST-Trans |Subtyping is transitive |lattice-theory-proofs.md §2.2 |- -|ST-Antisym |Subtyping with mutual implies equivalence |lattice-theory-proofs.md §2.3 |- -|ST-Lattice |Types form a bounded lattice |lattice-theory-proofs.md §3 |ST-Refl, ST-Trans, ST-Antisym -|ST-Join |Join exists for all type pairs |lattice-theory-proofs.md §3.2 |- -|ST-Meet |Meet exists for all type pairs |lattice-theory-proofs.md §3.3 |- +|ST-Refl |Subtyping is reflexive |proofs/lattice-theory/type-lattice-proofs.adoc §2.1 |- +|ST-Trans |Subtyping is transitive |proofs/lattice-theory/type-lattice-proofs.adoc §2.2 |- +|ST-Antisym |Subtyping with mutual implies equivalence |proofs/lattice-theory/type-lattice-proofs.adoc §2.3 |- +|ST-Lattice |Types form a bounded lattice |proofs/lattice-theory/type-lattice-proofs.adoc §3 |ST-Refl, ST-Trans, ST-Antisym +|ST-Join |Join exists for all type pairs |proofs/lattice-theory/type-lattice-proofs.adoc §3.2 |- +|ST-Meet |Meet exists for all type pairs |proofs/lattice-theory/type-lattice-proofs.adoc §3.3 |- |=== ==== Termination @@ -42,11 +42,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|TERM-Expr |Expression evaluation terminates |type-theory-proofs.md §4 |TERM-Measure -|TERM-Policy |Policy evaluation terminates |type-theory-proofs.md §4.2 |TERM-Expr -|TERM-Total |All programs terminate |type-theory-proofs.md §4.3 |TERM-Expr, TERM-Policy -|TERM-Measure |Well-founded measure exists |order-theory-foundations.md §2 |- -|SN-Strong |Strong normalization |type-theory-proofs.md §5 |TERM-Total +|TERM-Expr |Expression evaluation terminates |type-theory-proofs.adoc §4 |TERM-Measure +|TERM-Policy |Policy evaluation terminates |type-theory-proofs.adoc §4.2 |TERM-Expr +|TERM-Total |All programs terminate |type-theory-proofs.adoc §4.3 |TERM-Expr, TERM-Policy +|TERM-Measure |Well-founded measure exists |order-theory-foundations.adoc §2 |- +|SN-Strong |Strong normalization |type-theory-proofs.adoc §5 |TERM-Total |=== ''''' @@ -59,10 +59,10 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|OP-Det |Evaluation is deterministic |complete-operational-semantics.md §9 |- -|OP-Total |Evaluation is total |complete-operational-semantics.md §11 |TERM-Total -|OP-Progress |Well-typed terms make progress |complete-operational-semantics.md §10.1 |T-Progress -|OP-Preserve |Types preserved under reduction |complete-operational-semantics.md §10.2 |T-Preservation +|OP-Det |Evaluation is deterministic |complete-operational-semantics.adoc §9 |- +|OP-Total |Evaluation is total |complete-operational-semantics.adoc §11 |TERM-Total +|OP-Progress |Well-typed terms make progress |complete-operational-semantics.adoc §10.1 |T-Progress +|OP-Preserve |Types preserved under reduction |complete-operational-semantics.adoc §10.2 |T-Preservation |=== ==== Denotational Semantics @@ -70,10 +70,10 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|DEN-Compose |Semantic compositionality |denotational-semantics.md §3 |- -|DEN-Adequate |Adequacy theorem |denotational-semantics.md §6 |OP-Det -|DEN-Full |Full abstraction |denotational-semantics.md §6.3 |DEN-Adequate -|DEN-Cont |Semantic functions are continuous |denotational-semantics.md §4 |- +|DEN-Compose |Semantic compositionality |denotational-semantics.adoc §3 |- +|DEN-Adequate |Adequacy theorem |denotational-semantics.adoc §6 |OP-Det +|DEN-Full |Full abstraction |denotational-semantics.adoc §6.3 |DEN-Adequate +|DEN-Cont |Semantic functions are continuous |denotational-semantics.adoc §4 |- |=== ==== Domain Theory @@ -81,10 +81,10 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|DOM-CPO |Semantic domains are CPOs |domain-theory-foundations.md §2 |- -|DOM-Cont |Scott continuity of operations |domain-theory-foundations.md §4 |- -|DOM-Fix |Fixed point theorem |domain-theory-foundations.md §5 |DOM-Cont -|DOM-Compact |Compactness properties |domain-theory-foundations.md §6 |- +|DOM-CPO |Semantic domains are CPOs |domain-theory-foundations.adoc §2 |- +|DOM-Cont |Scott continuity of operations |domain-theory-foundations.adoc §4 |- +|DOM-Fix |Fixed point theorem |domain-theory-foundations.adoc §5 |DOM-Cont +|DOM-Compact |Compactness properties |domain-theory-foundations.adoc §6 |- |=== ==== Axiomatic Semantics @@ -92,11 +92,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|AX-Sound |Hoare logic is sound |hoare-logic.md §7.3 |OP-Det -|AX-Complete |Relative completeness |hoare-logic.md §7.4 |- -|AX-WP |wp characterization |hoare-logic.md §5 |- -|AX-SP |sp characterization |hoare-logic.md §6 |- -|AX-Health |Healthiness conditions |hoare-logic.md §5.3 |AX-WP +|AX-Sound |Hoare logic is sound |hoare-logic.adoc §7.3 |OP-Det +|AX-Complete |Relative completeness |hoare-logic.adoc §7.4 |- +|AX-WP |wp characterization |hoare-logic.adoc §5 |- +|AX-SP |sp characterization |hoare-logic.adoc §6 |- +|AX-Health |Healthiness conditions |hoare-logic.adoc §5.3 |AX-WP |=== ''''' @@ -109,12 +109,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|CON-Agree |Agreement property |cryptographic-proofs.md §3.1 |CON-Quorum -|CON-Valid |Validity property |cryptographic-proofs.md §3.2 |- -|CON-Term |Termination under partial synchrony |cryptographic-proofs.md §3.3 |- -|CON-Quorum |Quorum intersection |game-theory.md §4.2 |- -|CON-Safe |Safety under Byzantine faults |cryptographic-proofs.md §6.1 |CON-Agree -|CON-Live |Liveness under partial synchrony |cryptographic-proofs.md §6.2 |CON-Term +|CON-Agree |Agreement property |cryptographic-proofs.adoc §3.1 |CON-Quorum +|CON-Valid |Validity property |cryptographic-proofs.adoc §3.2 |- +|CON-Term |Termination under partial synchrony |cryptographic-proofs.adoc §3.3 |- +|CON-Quorum |Quorum intersection |proofs/game-theory/consensus-game-theory.adoc §4.2 |- +|CON-Safe |Safety under Byzantine faults |cryptographic-proofs.adoc §6.1 |CON-Agree +|CON-Live |Liveness under partial synchrony |cryptographic-proofs.adoc §6.2 |CON-Term |=== ==== Game Theory @@ -122,10 +122,10 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|GT-Nash |Nash equilibrium existence |consensus-game-theory.md §3 |- -|GT-IC |Incentive compatibility |consensus-game-theory.md §4 |GT-Nash -|GT-Dominant |Honest voting is dominant strategy |consensus-game-theory.md §5 |GT-IC -|GT-Mechanism |Mechanism design optimality |consensus-game-theory.md §6 |- +|GT-Nash |Nash equilibrium existence |consensus-game-theory.adoc §3 |- +|GT-IC |Incentive compatibility |consensus-game-theory.adoc §4 |GT-Nash +|GT-Dominant |Honest voting is dominant strategy |consensus-game-theory.adoc §5 |GT-IC +|GT-Mechanism |Mechanism design optimality |consensus-game-theory.adoc §6 |- |=== ==== Cryptographic @@ -133,10 +133,10 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|CRYPTO-Auth |Signature authentication |cryptographic-proofs.md §5.1 |- -|CRYPTO-NonRep |Non-repudiation |cryptographic-proofs.md §5 |CRYPTO-Auth -|CRYPTO-BFT |Byzantine fault tolerance |cryptographic-proofs.md §6 |CON-Safe -|CRYPTO-UC |UC security |cryptographic-proofs.md §12 |CRYPTO-BFT +|CRYPTO-Auth |Signature authentication |cryptographic-proofs.adoc §5.1 |- +|CRYPTO-NonRep |Non-repudiation |cryptographic-proofs.adoc §5 |CRYPTO-Auth +|CRYPTO-BFT |Byzantine fault tolerance |cryptographic-proofs.adoc §6 |CON-Safe +|CRYPTO-UC |UC security |cryptographic-proofs.adoc §12 |CRYPTO-BFT |=== ''''' @@ -147,12 +147,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|IF-Nonint |Noninterference theorem |information-flow-analysis.md §3.2 |- -|IF-TINI |Termination-insensitive NI |information-flow-analysis.md §3.3 |TERM-Total -|IF-Implicit |Implicit flow prevention |information-flow-analysis.md §4 |IF-Nonint -|IF-Declassify |Robust declassification |information-flow-analysis.md §5 |IF-Nonint -|IF-Integrity |Integrity preservation |information-flow-analysis.md §6 |- -|IF-Quant |Quantitative leakage bound |information-flow-analysis.md §9 |- +|IF-Nonint |Noninterference theorem |information-flow-analysis.adoc §3.2 |- +|IF-TINI |Termination-insensitive NI |information-flow-analysis.adoc §3.3 |TERM-Total +|IF-Implicit |Implicit flow prevention |information-flow-analysis.adoc §4 |IF-Nonint +|IF-Declassify |Robust declassification |information-flow-analysis.adoc §5 |IF-Nonint +|IF-Integrity |Integrity preservation |information-flow-analysis.adoc §6 |- +|IF-Quant |Quantitative leakage bound |information-flow-analysis.adoc §9 |- |=== ''''' @@ -163,12 +163,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|CAT-Functor |Type constructor functoriality |category-theory-foundations.md §2 |- -|CAT-Monad |Action monad laws |category-theory-foundations.md §4 |CAT-Functor -|CAT-CCC |Types form CCC |category-theory-foundations.md §6 |- -|CAT-Curry |Curry-Howard-Lambek |curry-howard-correspondence.md §1 |CAT-CCC -|CAT-Initial |Initial algebra for types |algebraic-semantics.md §3 |CAT-Functor -|CAT-Terminal |Terminal coalgebra |algebraic-semantics.md §5 |- +|CAT-Functor |Type constructor functoriality |category-theory-foundations.adoc §2 |- +|CAT-Monad |Action monad laws |category-theory-foundations.adoc §4 |CAT-Functor +|CAT-CCC |Types form CCC |category-theory-foundations.adoc §6 |- +|CAT-Curry |Curry-Howard-Lambek |curry-howard-correspondence.adoc §1 |CAT-CCC +|CAT-Initial |Initial algebra for types |algebraic-semantics.adoc §3 |CAT-Functor +|CAT-Terminal |Terminal coalgebra |algebraic-semantics.adoc §5 |- |=== ''''' @@ -179,12 +179,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|AUT-DFA |Lexer is DFA |automata-theory-proofs.md §2 |- -|AUT-Regular |Token language is regular |automata-theory-proofs.md §2.3 |AUT-DFA -|AUT-CFG |Grammar is context-free |automata-theory-proofs.md §3 |- -|AUT-LL1 |Grammar is LL(1) |automata-theory-proofs.md §3.2 |AUT-CFG -|AUT-Parse |Parsing is O(n) |automata-theory-proofs.md §3.4 |AUT-LL1 -|AUT-Decide |Type checking is decidable |automata-theory-proofs.md §4 |- +|AUT-DFA |Lexer is DFA |automata-theory-proofs.adoc §2 |- +|AUT-Regular |Token language is regular |automata-theory-proofs.adoc §2.3 |AUT-DFA +|AUT-CFG |Grammar is context-free |automata-theory-proofs.adoc §3 |- +|AUT-LL1 |Grammar is LL(1) |automata-theory-proofs.adoc §3.2 |AUT-CFG +|AUT-Parse |Parsing is O(n) |automata-theory-proofs.adoc §3.4 |AUT-LL1 +|AUT-Decide |Type checking is decidable |automata-theory-proofs.adoc §4 |- |=== ''''' @@ -195,13 +195,13 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|COMP-Lex |Lexing is O(n) |computational-complexity-analysis.md §2 |AUT-DFA -|COMP-Parse |Parsing is O(n) |computational-complexity-analysis.md §3 |AUT-LL1 -|COMP-Type |Type checking is O(n) |computational-complexity-analysis.md §4 |- -|COMP-Eval |Evaluation is O(size) |computational-complexity-analysis.md §5 |TERM-Measure -|COMP-Con |Consensus is O(n²) messages |computational-complexity-analysis.md §6 |- -|COMP-Space |Space is O(n) |computational-complexity-analysis.md §7 |- -|COMP-P |All operations in P |computational-complexity-analysis.md §8 |COMP-* +|COMP-Lex |Lexing is O(n) |computational-complexity-analysis.adoc §2 |AUT-DFA +|COMP-Parse |Parsing is O(n) |computational-complexity-analysis.adoc §3 |AUT-LL1 +|COMP-Type |Type checking is O(n) |computational-complexity-analysis.adoc §4 |- +|COMP-Eval |Evaluation is O(size) |computational-complexity-analysis.adoc §5 |TERM-Measure +|COMP-Con |Consensus is O(n²) messages |computational-complexity-analysis.adoc §6 |- +|COMP-Space |Space is O(n) |computational-complexity-analysis.adoc §7 |- +|COMP-P |All operations in P |computational-complexity-analysis.adoc §8 |COMP-* |=== ''''' @@ -212,11 +212,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|TL-Safety |Safety properties hold |temporal-logic-specifications.md §3 |CON-Safe -|TL-Liveness |Liveness under fairness |temporal-logic-specifications.md §4 |CON-Live -|TL-Fair |Fairness assumptions |temporal-logic-specifications.md §5 |- -|TL-CTL |CTL model checking |temporal-logic-specifications.md §6 |- -|TL-TLA |TLA+ specification valid |temporal-logic-specifications.md §7 |TL-Safety, TL-Liveness +|TL-Safety |Safety properties hold |temporal-logic-specifications.adoc §3 |CON-Safe +|TL-Liveness |Liveness under fairness |temporal-logic-specifications.adoc §4 |CON-Live +|TL-Fair |Fairness assumptions |temporal-logic-specifications.adoc §5 |- +|TL-CTL |CTL model checking |temporal-logic-specifications.adoc §6 |- +|TL-TLA |TLA+ specification valid |temporal-logic-specifications.adoc §7 |TL-Safety, TL-Liveness |=== ''''' @@ -227,11 +227,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|PA-Deadlock |Deadlock freedom |process-algebra.md §5.4 |- -|PA-Diverge |Divergence freedom |process-algebra.md §6.2 |TERM-Total -|PA-Bisim |Bisimulation congruence |process-algebra.md §7.3 |- -|PA-Session |Session type duality |process-algebra.md §13 |- -|PA-Compose |Compositional refinement |process-algebra.md §14 |PA-Bisim +|PA-Deadlock |Deadlock freedom |process-algebra.adoc §5.4 |- +|PA-Diverge |Divergence freedom |process-algebra.adoc §6.2 |TERM-Total +|PA-Bisim |Bisimulation congruence |process-algebra.adoc §7.3 |- +|PA-Session |Session type duality |process-algebra.adoc §13 |- +|PA-Compose |Compositional refinement |process-algebra.adoc §14 |PA-Bisim |=== ''''' @@ -242,12 +242,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|PROTO-Auth |Authentication |dolev-yao-model.md §5.3 |CRYPTO-Auth -|PROTO-Agree |Protocol agreement |dolev-yao-model.md §5.1 |CON-Agree -|PROTO-Replay |Replay prevention |dolev-yao-model.md §6.1 |- -|PROTO-MitM |MitM prevention |dolev-yao-model.md §6.3 |CRYPTO-Auth -|PROTO-Sound |Computational soundness |dolev-yao-model.md §12 |- -|PROTO-Verify |ProVerif/Tamarin verified |dolev-yao-model.md §13 |PROTO-* +|PROTO-Auth |Authentication |dolev-yao-model.adoc §5.3 |CRYPTO-Auth +|PROTO-Agree |Protocol agreement |dolev-yao-model.adoc §5.1 |CON-Agree +|PROTO-Replay |Replay prevention |dolev-yao-model.adoc §6.1 |- +|PROTO-MitM |MitM prevention |dolev-yao-model.adoc §6.3 |CRYPTO-Auth +|PROTO-Sound |Computational soundness |dolev-yao-model.adoc §12 |- +|PROTO-Verify |ProVerif/Tamarin verified |dolev-yao-model.adoc §13 |PROTO-* |=== ''''' @@ -258,11 +258,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|AI-Galois |Galois connection |abstract-interpretation-framework.md §2 |- -|AI-Sound |Abstract interpretation soundness |abstract-interpretation-framework.md §4 |AI-Galois -|AI-Complete |Best abstract transformer |abstract-interpretation-framework.md §5 |AI-Galois -|AI-Wide |Widening convergence |abstract-interpretation-framework.md §6 |- -|AI-Narrow |Narrowing improvement |abstract-interpretation-framework.md §7 |AI-Wide +|AI-Galois |Galois connection |abstract-interpretation-framework.adoc §2 |- +|AI-Sound |Abstract interpretation soundness |abstract-interpretation-framework.adoc §4 |AI-Galois +|AI-Complete |Best abstract transformer |abstract-interpretation-framework.adoc §5 |AI-Galois +|AI-Wide |Widening convergence |abstract-interpretation-framework.adoc §6 |- +|AI-Narrow |Narrowing improvement |abstract-interpretation-framework.adoc §7 |AI-Wide |=== ''''' @@ -273,12 +273,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|ORD-WF |Well-foundedness of measures |order-theory-foundations.md §2 |- -|ORD-Lex |Lexicographic order WF |order-theory-foundations.md §3 |ORD-WF -|ORD-WQO |WQO closure properties |order-theory-foundations.md §4 |- -|ORD-Lattice |Complete lattice properties |order-theory-foundations.md §5 |- -|ORD-KT |Knaster-Tarski fixed point |order-theory-foundations.md §6 |ORD-Lattice -|ORD-Galois |Galois connection properties |order-theory-foundations.md §7 |- +|ORD-WF |Well-foundedness of measures |order-theory-foundations.adoc §2 |- +|ORD-Lex |Lexicographic order WF |order-theory-foundations.adoc §3 |ORD-WF +|ORD-WQO |WQO closure properties |order-theory-foundations.adoc §4 |- +|ORD-Lattice |Complete lattice properties |order-theory-foundations.adoc §5 |- +|ORD-KT |Knaster-Tarski fixed point |order-theory-foundations.adoc §6 |ORD-Lattice +|ORD-Galois |Galois connection properties |order-theory-foundations.adoc §7 |- |=== ''''' @@ -289,12 +289,12 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|PROB-Vote |Vote distribution |probabilistic-analysis.md §3 |- -|PROB-Thresh |Threshold probability |probabilistic-analysis.md §3.3 |PROB-Vote -|PROB-BFT |Byzantine reliability |probabilistic-analysis.md §4 |- -|PROB-Leader |Leader election fairness |probabilistic-analysis.md §5 |- -|PROB-Chernoff |Concentration bounds |probabilistic-analysis.md §8 |- -|PROB-Markov |Markov chain analysis |probabilistic-analysis.md §9 |- +|PROB-Vote |Vote distribution |probabilistic-analysis.adoc §3 |- +|PROB-Thresh |Threshold probability |probabilistic-analysis.adoc §3.3 |PROB-Vote +|PROB-BFT |Byzantine reliability |probabilistic-analysis.adoc §4 |- +|PROB-Leader |Leader election fairness |probabilistic-analysis.adoc §5 |- +|PROB-Chernoff |Concentration bounds |probabilistic-analysis.adoc §8 |- +|PROB-Markov |Markov chain analysis |probabilistic-analysis.adoc §9 |- |=== ''''' @@ -305,11 +305,11 @@ This document provides a comprehensive index of all theorems, lemmas, and key de [cols=",,,",options="header",] |=== |ID |Theorem |Location |Dependencies -|NUM-Prefix |Prefix containment is partial order |number-theory-foundations.md §1.3 |- -|NUM-LPM |Longest prefix match |number-theory-foundations.md §1.4 |NUM-Prefix -|NUM-Aggregate |Prefix aggregation |number-theory-foundations.md §2.5 |- -|NUM-Curve |Elliptic curve properties |number-theory-foundations.md §4 |- -|NUM-Birthday |Birthday bound |number-theory-foundations.md §5 |- +|NUM-Prefix |Prefix containment is partial order |number-theory-foundations.adoc §1.3 |- +|NUM-LPM |Longest prefix match |number-theory-foundations.adoc §1.4 |NUM-Prefix +|NUM-Aggregate |Prefix aggregation |number-theory-foundations.adoc §2.5 |- +|NUM-Curve |Elliptic curve properties |number-theory-foundations.adoc §4 |- +|NUM-Birthday |Birthday bound |number-theory-foundations.adoc §5 |- |=== ''''' @@ -364,12 +364,12 @@ Protocol Security [cols=",,",options="header",] |=== |Term |Definition |Location -|Type |τ ::= Int \| Bool \| ... |type-theory-proofs.md §1.1 -|Expression |e ::= x \| l \| e op e \| ... |complete-operational-semantics.md §1.1 -|Value |v ::= n \| b \| s \| ... |complete-operational-semantics.md §1.2 -|Environment |ρ : Var ⇀ Val |complete-operational-semantics.md §1.2 -|Policy |POLICY name: cond THEN action |complete-operational-semantics.md §1.1 -|Consensus |(PROPOSE, VOTE, COMMIT) |cryptographic-proofs.md §2 +|Type |τ ::= Int \| Bool \| ... |type-theory-proofs.adoc §1.1 +|Expression |e ::= x \| l \| e op e \| ... |complete-operational-semantics.adoc §1.1 +|Value |v ::= n \| b \| s \| ... |complete-operational-semantics.adoc §1.2 +|Environment |ρ : Var ⇀ Val |complete-operational-semantics.adoc §1.2 +|Policy |POLICY name: cond THEN action |complete-operational-semantics.adoc §1.1 +|Consensus |(PROPOSE, VOTE, COMMIT) |cryptographic-proofs.adoc §2 |=== ==== Semantic Domains @@ -377,9 +377,9 @@ Protocol Security [cols=",,",options="header",] |=== |Term |Definition |Location -|CPO |Complete partial order |domain-theory-foundations.md §2 -|Scott Topology |Open = Scott-open sets |domain-theory-foundations.md §3 -|Continuous |Preserves directed sups |domain-theory-foundations.md §4 +|CPO |Complete partial order |domain-theory-foundations.adoc §2 +|Scott Topology |Open = Scott-open sets |domain-theory-foundations.adoc §3 +|Continuous |Preserves directed sups |domain-theory-foundations.adoc §4 |=== ==== Security @@ -387,9 +387,9 @@ Protocol Security [cols=",,",options="header",] |=== |Term |Definition |Location -|Security Level |L = \{Public, Private, System} |information-flow-analysis.md §1 -|Noninterference |ρ₁ ≈ₗ ρ₂ → ⟦e⟧ρ₁ = ⟦e⟧ρ₂ |information-flow-analysis.md §3 -|Byzantine |Agent deviating from protocol |cryptographic-proofs.md §2 +|Security Level |L = \{Public, Private, System} |information-flow-analysis.adoc §1 +|Noninterference |ρ₁ ≈ₗ ρ₂ → ⟦e⟧ρ₁ = ⟦e⟧ρ₂ |information-flow-analysis.adoc §3 +|Byzantine |Agent deviating from protocol |cryptographic-proofs.adoc §2 |=== ''''' diff --git a/deploy/DEPLOYMENT.adoc b/deploy/DEPLOYMENT.adoc new file mode 100644 index 0000000..ad7193c --- /dev/null +++ b/deploy/DEPLOYMENT.adoc @@ -0,0 +1,511 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +== Phronesis Production Deployment Guide + +=== Overview + +This guide covers deploying Phronesis in production with high +availability, distributed consensus, and performance optimization. + +=== Performance Baseline + +*Current Performance (as of 2026-01-30):* + +[cols=",,,",options="header",] +|=== +|Component |Throughput |Latency |Status +|Lexer |17.3k ops/sec |57.7 μs/op |✓ 173% of target +|Parser |1.43M ops/sec |0.7 μs/op |✓ 14,257% of target +|Compiler |14.1k ops/sec |70.9 μs/op |✓ 141% of target +|Interpreter |3.18M ops/sec |0.3 μs/op |✓ 31,786% of target +|Consensus |1.05M ops/sec |0.95 μs/op |✓ 10,482% of target +|*End-to-End* |*7.04k ops/sec* |*142 μs/op* |*✓ 70% of target* +|=== + +*Target:* 10,000 policies/sec *Status:* 5/6 components exceed target, +end-to-end at 70% of target + +=== Docker Deployment + +==== Single Node (Development) + +[source,bash] +---- +# Build image +docker build -t phronesis:latest . + +# Run single node +docker run -d \ + --name phronesis \ + -p 4369:4369 \ + -p 9100:9100 \ + -v phronesis_data:/app/priv/consensus_data \ + -e PHRONESIS_CONSENSUS_ENABLED=false \ + phronesis:latest +---- + +==== Multi-Node Cluster (Production) + +[source,bash] +---- +# Set cluster cookie (use secure random value in production) +export PHRONESIS_CLUSTER_COOKIE=$(openssl rand -base64 32) + +# Start 3-node cluster +docker-compose up -d + +# Check cluster health +docker-compose ps + +# View logs +docker-compose logs -f node1 + +# Connect to node 1 +docker exec -it phronesis-node1 /app/bin/phronesis remote_console + +# Stop cluster +docker-compose down + +# Stop and remove volumes +docker-compose down -v +---- + +*Environment Variables:* + +* `RELEASE_DISTRIBUTION` - Distribution type (`name` or `sname`) +* `RELEASE_NODE` - Node name (e.g., `node1@phronesis-node1`) +* `RELEASE_COOKIE` - Erlang cluster cookie (MUST match across nodes) +* `PHRONESIS_CONSENSUS_ENABLED` - Enable distributed consensus +(`true`/`false`) +* `PHRONESIS_NODE_ID` - Unique node identifier (`node1`, `node2`, etc.) +* `ERL_DIST_PORT` - Erlang distribution port (default: 9100) + +=== Kubernetes Deployment + +==== Prerequisites + +* Kubernetes cluster (1.24+) +* kubectl configured +* Storage class for PersistentVolumes + +==== Deploy StatefulSet + +[source,bash] +---- +# Create namespace and deploy +kubectl apply -f deploy/kubernetes/statefulset.yaml + +# Check status +kubectl get statefulset -n phronesis +kubectl get pods -n phronesis +kubectl get svc -n phronesis + +# View logs +kubectl logs -n phronesis phronesis-0 -f + +# Connect to pod +kubectl exec -it -n phronesis phronesis-0 -- /app/bin/phronesis remote_console + +# Scale cluster +kubectl scale statefulset -n phronesis phronesis --replicas=5 + +# Delete deployment +kubectl delete -f deploy/kubernetes/statefulset.yaml +---- + +==== Cluster Configuration + +*StatefulSet Features:* + +* Stable network identities (phronesis-0, phronesis-1, etc.) +* Persistent storage per pod (10Gi default) +* Headless service for DNS-based discovery +* Automatic pod ordering and graceful shutdown +* Security context (non-root user) + +*Resource Limits:* + +[source,yaml] +---- +resources: + requests: + memory: "256Mi" + cpu: "250m" + limits: + memory: "512Mi" + cpu: "500m" +---- + +Adjust based on workload and performance testing. + +==== Service Discovery + +Pods are accessible via: + +.... +.phronesis-headless..svc.cluster.local +.... + +Examples: + +* `phronesis-0.phronesis-headless.phronesis.svc.cluster.local` +* `phronesis-1.phronesis-headless.phronesis.svc.cluster.local` + +=== Load Balancing + +==== Nginx Example + +[source,nginx] +---- +upstream phronesis_cluster { + least_conn; + server phronesis-node1:9100 max_fails=3 fail_timeout=30s; + server phronesis-node2:9100 max_fails=3 fail_timeout=30s; + server phronesis-node3:9100 max_fails=3 fail_timeout=30s; +} + +server { + listen 80; + server_name phronesis.example.com; + + location / { + proxy_pass http://phronesis_cluster; + proxy_set_header Host $host; + proxy_set_header X-Real-IP $remote_addr; + proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for; + proxy_connect_timeout 5s; + proxy_send_timeout 60s; + proxy_read_timeout 60s; + } +} +---- + +==== HAProxy Example + +[source,haproxy] +---- +frontend phronesis_frontend + bind *:80 + default_backend phronesis_cluster + +backend phronesis_cluster + balance leastconn + option httpchk GET /health + server node1 phronesis-node1:9100 check inter 5s + server node2 phronesis-node2:9100 check inter 5s + server node3 phronesis-node3:9100 check inter 5s +---- + +=== Monitoring + +==== Health Checks + +[source,bash] +---- +# Check if node is running +/app/bin/phronesis rpc "node()" + +# Check application status +/app/bin/phronesis rpc "Application.started_applications() |> Enum.any?(fn {app, _, _} -> app == :phronesis end)" + +# Check consensus status +/app/bin/phronesis rpc "Phronesis.Consensus.Server.status()" +---- + +==== Metrics to Monitor + +*Application Metrics:* + +* Policy execution throughput (target: 10k/sec) +* Consensus vote latency +* Error rate per policy +* Active connections + +*System Metrics:* + +* CPU usage per pod/container +* Memory usage (RSS, heap) +* Disk I/O (consensus data writes) +* Network I/O (distribution traffic) + +*BEAM Metrics:* + +* Process count +* Message queue lengths +* Garbage collection frequency +* Reductions per second + +==== Prometheus Integration (Future Work) + +[source,elixir] +---- +# Add to mix.exs +{:telemetry_metrics_prometheus, "~> 1.1"} + +# Configure metrics endpoint +config :phronesis, :telemetry_metrics, + port: 9568, + metrics: [ + summary("phronesis.policy.execution.duration"), + counter("phronesis.policy.execution.count"), + last_value("phronesis.consensus.cluster.size") + ] +---- + +=== Performance Tuning + +==== BEAM VM Flags + +[source,bash] +---- +# Increase scheduler count (match CPU cores) +ERL_FLAGS="+S 4:4" + +# Increase async thread pool +ERL_FLAGS="+A 32" + +# Disable SMP (single-core systems only) +# ERL_FLAGS="-smp disable" + +# Set maximum processes +ERL_FLAGS="+P 1000000" + +# Set maximum ports +ERL_FLAGS="+Q 65536" + +# Example combined +export ERL_FLAGS="+S 4:4 +A 32 +P 1000000 +Q 65536" +---- + +==== Consensus Tuning + +[source,elixir] +---- +# Adjust Ra cluster settings (in code) +%{ + cluster_name: :phronesis_consensus, + log_init_args: %{ + max_segment_size: 16_777_216, # 16MB segments + cache_size: 2048, # 2048 log entries + snapshot_interval: 4096 # Snapshot every 4096 entries + } +} +---- + +==== Database/Storage + +* Use fast SSD storage for consensus data +* Mount `/app/priv/consensus_data` on dedicated volume +* Enable write caching (with UPS or battery backup) +* Use XFS or ext4 filesystem + +=== Security + +==== Network Security + +* Isolate EPMD port (4369) from public access +* Restrict distribution ports (9100-9200) to cluster network +* Use firewall rules to limit inter-node traffic +* Enable TLS for Erlang distribution (production requirement) + +==== Erlang Distribution TLS + +[source,elixir] +---- +# config/releases.exs +config :kernel, + inet_dist_use_interface: {0, 0, 0, 0}, + inet_dist_listen_min: 9100, + inet_dist_listen_max: 9200 + +# Enable SSL distribution +config :ssl, + dist_server_options: [ + certfile: "/etc/phronesis/certs/server.crt", + keyfile: "/etc/phronesis/certs/server.key", + cacertfile: "/etc/phronesis/certs/ca.crt", + verify: :verify_peer, + fail_if_no_peer_cert: true + ] +---- + +==== Secrets Management + +* Store `RELEASE_COOKIE` in Kubernetes Secrets or Docker secrets +* Rotate cluster cookie periodically +* Use key management service (AWS KMS, HashiCorp Vault) +* Never commit secrets to version control + +=== Backup and Recovery + +==== Consensus Data Backup + +[source,bash] +---- +# Stop node gracefully +/app/bin/phronesis stop + +# Backup consensus data +tar -czf consensus-backup-$(date +%Y%m%d).tar.gz /app/priv/consensus_data + +# Restart node +/app/bin/phronesis start + +# Or use volume snapshots (Kubernetes/Docker) +kubectl exec -n phronesis phronesis-0 -- tar -czf - /app/priv/consensus_data > backup.tar.gz +---- + +==== Disaster Recovery + +[arabic] +. Stop all cluster nodes +. Restore consensus data from backup on all nodes +. Restart cluster (leader election will occur) +. Verify cluster health and log integrity + +=== Troubleshooting + +==== Node Won't Join Cluster + +*Check:* + +* RELEASE_COOKIE matches on all nodes +* Network connectivity between nodes (EPMD port 4369, dist port 9100) +* DNS resolution (Kubernetes: headless service) +* Node names are correct and unique + +*Debug:* + +[source,bash] +---- +# Check node connectivity +/app/bin/phronesis rpc "Node.connect(:'node2@phronesis-node2')" + +# List connected nodes +/app/bin/phronesis rpc "Node.list()" + +# Check EPMD +epmd -names +---- + +==== High Memory Usage + +*Causes:* + +* Large consensus log (not snapshotting) +* Message queue buildup +* Memory leak in application code + +*Solutions:* + +* Enable Ra snapshotting +* Increase snapshot frequency +* Monitor process memory with `:observer` + +==== Slow Consensus + +*Causes:* + +* Network latency between nodes +* Disk I/O bottleneck +* Too many nodes in cluster + +*Solutions:* + +* Use faster storage (NVMe SSD) +* Co-locate nodes in same datacenter/region +* Reduce cluster size (3-5 nodes recommended) +* Tune Ra segment size and cache + +=== Hot Code Reloading (Development Only) + +*Enabled by default in development:* + +[source,elixir] +---- +# Manual reload +Phronesis.HotReload.reload_all() + +# Reload specific module +Phronesis.HotReload.reload_module(Phronesis.Parser) + +# Stop hot reload +Phronesis.HotReload.stop() +---- + +*DO NOT use in production* - deploy new releases instead. + +=== Release Management + +==== Creating a Release + +[source,bash] +---- +# Set environment +export MIX_ENV=prod + +# Clean and compile +mix clean +mix deps.get --only prod +mix compile + +# Build release +mix release + +# Output location +_build/prod/rel/phronesis +---- + +==== Deploying a Release + +[source,bash] +---- +# Copy release to server +scp -r _build/prod/rel/phronesis server:/opt/phronesis + +# On server +cd /opt/phronesis +./bin/phronesis daemon # Start as daemon +./bin/phronesis stop # Stop daemon +./bin/phronesis restart # Restart +---- + +=== Appendix + +==== Useful Commands + +[source,bash] +---- +# Remote console (attach to running node) +/app/bin/phronesis remote_console + +# RPC (run command without attaching) +/app/bin/phronesis rpc "Application.get_env(:phronesis, :consensus_enabled)" + +# Ping node +/app/bin/phronesis ping + +# Evaluate Elixir expression +/app/bin/phronesis eval "IO.puts(\"Hello\")" +---- + +==== Configuration Files + +* `config/config.exs` - Compile-time configuration +* `config/dev.exs` - Development overrides +* `config/prod.exs` - Production overrides +* `config/runtime.exs` - Runtime configuration (recommended) +* `config/releases.exs` - Release-time configuration + +==== Resources + +* https://hexdocs.pm/mix/Mix.Tasks.Release.html[Elixir Releases Guide] +* https://github.com/rabbitmq/ra[Ra Documentation] +* https://www.erlang.org/doc/man/erl.html[BEAM VM Tuning] +* https://kubernetes.io/docs/concepts/workloads/controllers/statefulset/[Kubernetes +StatefulSets] + +''''' + +*Maintainer:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk *License:* +MPL-2.0 diff --git a/deploy/DEPLOYMENT.md b/deploy/DEPLOYMENT.md deleted file mode 100644 index fcf4039..0000000 --- a/deploy/DEPLOYMENT.md +++ /dev/null @@ -1,481 +0,0 @@ - -# Phronesis Production Deployment Guide - -## Overview - -This guide covers deploying Phronesis in production with high availability, -distributed consensus, and performance optimization. - -## Performance Baseline - -**Current Performance (as of 2026-01-30):** - -| Component | Throughput | Latency | Status | -|-----------|------------|---------|--------| -| Lexer | 17.3k ops/sec | 57.7 μs/op | ✓ 173% of target | -| Parser | 1.43M ops/sec | 0.7 μs/op | ✓ 14,257% of target | -| Compiler | 14.1k ops/sec | 70.9 μs/op | ✓ 141% of target | -| Interpreter | 3.18M ops/sec | 0.3 μs/op | ✓ 31,786% of target | -| Consensus | 1.05M ops/sec | 0.95 μs/op | ✓ 10,482% of target | -| **End-to-End** | **7.04k ops/sec** | **142 μs/op** | **✓ 70% of target** | - -**Target:** 10,000 policies/sec -**Status:** 5/6 components exceed target, end-to-end at 70% of target - -## Docker Deployment - -### Single Node (Development) - -```bash -# Build image -docker build -t phronesis:latest . - -# Run single node -docker run -d \ - --name phronesis \ - -p 4369:4369 \ - -p 9100:9100 \ - -v phronesis_data:/app/priv/consensus_data \ - -e PHRONESIS_CONSENSUS_ENABLED=false \ - phronesis:latest -``` - -### Multi-Node Cluster (Production) - -```bash -# Set cluster cookie (use secure random value in production) -export PHRONESIS_CLUSTER_COOKIE=$(openssl rand -base64 32) - -# Start 3-node cluster -docker-compose up -d - -# Check cluster health -docker-compose ps - -# View logs -docker-compose logs -f node1 - -# Connect to node 1 -docker exec -it phronesis-node1 /app/bin/phronesis remote_console - -# Stop cluster -docker-compose down - -# Stop and remove volumes -docker-compose down -v -``` - -**Environment Variables:** - -- `RELEASE_DISTRIBUTION` - Distribution type (`name` or `sname`) -- `RELEASE_NODE` - Node name (e.g., `node1@phronesis-node1`) -- `RELEASE_COOKIE` - Erlang cluster cookie (MUST match across nodes) -- `PHRONESIS_CONSENSUS_ENABLED` - Enable distributed consensus (`true`/`false`) -- `PHRONESIS_NODE_ID` - Unique node identifier (`node1`, `node2`, etc.) -- `ERL_DIST_PORT` - Erlang distribution port (default: 9100) - -## Kubernetes Deployment - -### Prerequisites - -- Kubernetes cluster (1.24+) -- kubectl configured -- Storage class for PersistentVolumes - -### Deploy StatefulSet - -```bash -# Create namespace and deploy -kubectl apply -f deploy/kubernetes/statefulset.yaml - -# Check status -kubectl get statefulset -n phronesis -kubectl get pods -n phronesis -kubectl get svc -n phronesis - -# View logs -kubectl logs -n phronesis phronesis-0 -f - -# Connect to pod -kubectl exec -it -n phronesis phronesis-0 -- /app/bin/phronesis remote_console - -# Scale cluster -kubectl scale statefulset -n phronesis phronesis --replicas=5 - -# Delete deployment -kubectl delete -f deploy/kubernetes/statefulset.yaml -``` - -### Cluster Configuration - -**StatefulSet Features:** - -- Stable network identities (phronesis-0, phronesis-1, etc.) -- Persistent storage per pod (10Gi default) -- Headless service for DNS-based discovery -- Automatic pod ordering and graceful shutdown -- Security context (non-root user) - -**Resource Limits:** - -```yaml -resources: - requests: - memory: "256Mi" - cpu: "250m" - limits: - memory: "512Mi" - cpu: "500m" -``` - -Adjust based on workload and performance testing. - -### Service Discovery - -Pods are accessible via: - -``` -.phronesis-headless..svc.cluster.local -``` - -Examples: -- `phronesis-0.phronesis-headless.phronesis.svc.cluster.local` -- `phronesis-1.phronesis-headless.phronesis.svc.cluster.local` - -## Load Balancing - -### Nginx Example - -```nginx -upstream phronesis_cluster { - least_conn; - server phronesis-node1:9100 max_fails=3 fail_timeout=30s; - server phronesis-node2:9100 max_fails=3 fail_timeout=30s; - server phronesis-node3:9100 max_fails=3 fail_timeout=30s; -} - -server { - listen 80; - server_name phronesis.example.com; - - location / { - proxy_pass http://phronesis_cluster; - proxy_set_header Host $host; - proxy_set_header X-Real-IP $remote_addr; - proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for; - proxy_connect_timeout 5s; - proxy_send_timeout 60s; - proxy_read_timeout 60s; - } -} -``` - -### HAProxy Example - -```haproxy -frontend phronesis_frontend - bind *:80 - default_backend phronesis_cluster - -backend phronesis_cluster - balance leastconn - option httpchk GET /health - server node1 phronesis-node1:9100 check inter 5s - server node2 phronesis-node2:9100 check inter 5s - server node3 phronesis-node3:9100 check inter 5s -``` - -## Monitoring - -### Health Checks - -```bash -# Check if node is running -/app/bin/phronesis rpc "node()" - -# Check application status -/app/bin/phronesis rpc "Application.started_applications() |> Enum.any?(fn {app, _, _} -> app == :phronesis end)" - -# Check consensus status -/app/bin/phronesis rpc "Phronesis.Consensus.Server.status()" -``` - -### Metrics to Monitor - -**Application Metrics:** -- Policy execution throughput (target: 10k/sec) -- Consensus vote latency -- Error rate per policy -- Active connections - -**System Metrics:** -- CPU usage per pod/container -- Memory usage (RSS, heap) -- Disk I/O (consensus data writes) -- Network I/O (distribution traffic) - -**BEAM Metrics:** -- Process count -- Message queue lengths -- Garbage collection frequency -- Reductions per second - -### Prometheus Integration (Future Work) - -```elixir -# Add to mix.exs -{:telemetry_metrics_prometheus, "~> 1.1"} - -# Configure metrics endpoint -config :phronesis, :telemetry_metrics, - port: 9568, - metrics: [ - summary("phronesis.policy.execution.duration"), - counter("phronesis.policy.execution.count"), - last_value("phronesis.consensus.cluster.size") - ] -``` - -## Performance Tuning - -### BEAM VM Flags - -```bash -# Increase scheduler count (match CPU cores) -ERL_FLAGS="+S 4:4" - -# Increase async thread pool -ERL_FLAGS="+A 32" - -# Disable SMP (single-core systems only) -# ERL_FLAGS="-smp disable" - -# Set maximum processes -ERL_FLAGS="+P 1000000" - -# Set maximum ports -ERL_FLAGS="+Q 65536" - -# Example combined -export ERL_FLAGS="+S 4:4 +A 32 +P 1000000 +Q 65536" -``` - -### Consensus Tuning - -```elixir -# Adjust Ra cluster settings (in code) -%{ - cluster_name: :phronesis_consensus, - log_init_args: %{ - max_segment_size: 16_777_216, # 16MB segments - cache_size: 2048, # 2048 log entries - snapshot_interval: 4096 # Snapshot every 4096 entries - } -} -``` - -### Database/Storage - -- Use fast SSD storage for consensus data -- Mount `/app/priv/consensus_data` on dedicated volume -- Enable write caching (with UPS or battery backup) -- Use XFS or ext4 filesystem - -## Security - -### Network Security - -- Isolate EPMD port (4369) from public access -- Restrict distribution ports (9100-9200) to cluster network -- Use firewall rules to limit inter-node traffic -- Enable TLS for Erlang distribution (production requirement) - -### Erlang Distribution TLS - -```elixir -# config/releases.exs -config :kernel, - inet_dist_use_interface: {0, 0, 0, 0}, - inet_dist_listen_min: 9100, - inet_dist_listen_max: 9200 - -# Enable SSL distribution -config :ssl, - dist_server_options: [ - certfile: "/etc/phronesis/certs/server.crt", - keyfile: "/etc/phronesis/certs/server.key", - cacertfile: "/etc/phronesis/certs/ca.crt", - verify: :verify_peer, - fail_if_no_peer_cert: true - ] -``` - -### Secrets Management - -- Store `RELEASE_COOKIE` in Kubernetes Secrets or Docker secrets -- Rotate cluster cookie periodically -- Use key management service (AWS KMS, HashiCorp Vault) -- Never commit secrets to version control - -## Backup and Recovery - -### Consensus Data Backup - -```bash -# Stop node gracefully -/app/bin/phronesis stop - -# Backup consensus data -tar -czf consensus-backup-$(date +%Y%m%d).tar.gz /app/priv/consensus_data - -# Restart node -/app/bin/phronesis start - -# Or use volume snapshots (Kubernetes/Docker) -kubectl exec -n phronesis phronesis-0 -- tar -czf - /app/priv/consensus_data > backup.tar.gz -``` - -### Disaster Recovery - -1. Stop all cluster nodes -2. Restore consensus data from backup on all nodes -3. Restart cluster (leader election will occur) -4. Verify cluster health and log integrity - -## Troubleshooting - -### Node Won't Join Cluster - -**Check:** -- RELEASE_COOKIE matches on all nodes -- Network connectivity between nodes (EPMD port 4369, dist port 9100) -- DNS resolution (Kubernetes: headless service) -- Node names are correct and unique - -**Debug:** -```bash -# Check node connectivity -/app/bin/phronesis rpc "Node.connect(:'node2@phronesis-node2')" - -# List connected nodes -/app/bin/phronesis rpc "Node.list()" - -# Check EPMD -epmd -names -``` - -### High Memory Usage - -**Causes:** -- Large consensus log (not snapshotting) -- Message queue buildup -- Memory leak in application code - -**Solutions:** -- Enable Ra snapshotting -- Increase snapshot frequency -- Monitor process memory with `:observer` - -### Slow Consensus - -**Causes:** -- Network latency between nodes -- Disk I/O bottleneck -- Too many nodes in cluster - -**Solutions:** -- Use faster storage (NVMe SSD) -- Co-locate nodes in same datacenter/region -- Reduce cluster size (3-5 nodes recommended) -- Tune Ra segment size and cache - -## Hot Code Reloading (Development Only) - -**Enabled by default in development:** - -```elixir -# Manual reload -Phronesis.HotReload.reload_all() - -# Reload specific module -Phronesis.HotReload.reload_module(Phronesis.Parser) - -# Stop hot reload -Phronesis.HotReload.stop() -``` - -**DO NOT use in production** - deploy new releases instead. - -## Release Management - -### Creating a Release - -```bash -# Set environment -export MIX_ENV=prod - -# Clean and compile -mix clean -mix deps.get --only prod -mix compile - -# Build release -mix release - -# Output location -_build/prod/rel/phronesis -``` - -### Deploying a Release - -```bash -# Copy release to server -scp -r _build/prod/rel/phronesis server:/opt/phronesis - -# On server -cd /opt/phronesis -./bin/phronesis daemon # Start as daemon -./bin/phronesis stop # Stop daemon -./bin/phronesis restart # Restart -``` - -## Appendix - -### Useful Commands - -```bash -# Remote console (attach to running node) -/app/bin/phronesis remote_console - -# RPC (run command without attaching) -/app/bin/phronesis rpc "Application.get_env(:phronesis, :consensus_enabled)" - -# Ping node -/app/bin/phronesis ping - -# Evaluate Elixir expression -/app/bin/phronesis eval "IO.puts(\"Hello\")" -``` - -### Configuration Files - -- `config/config.exs` - Compile-time configuration -- `config/dev.exs` - Development overrides -- `config/prod.exs` - Production overrides -- `config/runtime.exs` - Runtime configuration (recommended) -- `config/releases.exs` - Release-time configuration - -### Resources - -- [Elixir Releases Guide](https://hexdocs.pm/mix/Mix.Tasks.Release.html) -- [Ra Documentation](https://github.com/rabbitmq/ra) -- [BEAM VM Tuning](https://www.erlang.org/doc/man/erl.html) -- [Kubernetes StatefulSets](https://kubernetes.io/docs/concepts/workloads/controllers/statefulset/) - ---- - -**Maintainer:** Jonathan D.A. Jewell -**License:** MPL-2.0 diff --git a/docs/CONSENSUS.md b/docs/CONSENSUS.adoc similarity index 52% rename from docs/CONSENSUS.md rename to docs/CONSENSUS.adoc index c6e57c9..d533cf5 100644 --- a/docs/CONSENSUS.md +++ b/docs/CONSENSUS.adoc @@ -1,82 +1,95 @@ - -# Phronesis Distributed Consensus +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +== Phronesis Distributed Consensus -## Overview +=== Overview -Phronesis uses **Ra** (Erlang Raft implementation) for distributed consensus across multiple nodes. This enables Byzantine fault-tolerant policy voting in production deployments. +Phronesis uses *Ra* (Erlang Raft implementation) for distributed +consensus across multiple nodes. This enables Byzantine fault-tolerant +policy voting in production deployments. -## Architecture +=== Architecture -### Components +==== Components -1. **Consensus.Server** - GenServer wrapper around Ra cluster -2. **Consensus.Server.Machine** - Ra state machine for vote processing -3. **Stdlib.Consensus** - High-level consensus API with automatic fallback +[arabic] +. *Consensus.Server* - GenServer wrapper around Ra cluster +. *Consensus.Server.Machine* - Ra state machine for vote processing +. *Stdlib.Consensus* - High-level consensus API with automatic fallback -### Consensus Modes +==== Consensus Modes -**Mock Mode (Default)** -- Single-node operation -- Simulated voting for development/testing -- No distributed dependencies +*Mock Mode (Default)* -**Distributed Mode** -- Multi-node Raft cluster -- Real consensus with leader election -- Replicated log across nodes -- Automatic failover +* Single-node operation +* Simulated voting for development/testing +* No distributed dependencies -## Running a Distributed Cluster +*Distributed Mode* -### Environment Variables +* Multi-node Raft cluster +* Real consensus with leader election +* Replicated log across nodes +* Automatic failover -```bash +=== Running a Distributed Cluster + +==== Environment Variables + +[source,bash] +---- # Enable distributed consensus export PHRONESIS_CONSENSUS_ENABLED=true # Set unique node ID (node1, node2, node3, etc.) export PHRONESIS_NODE_ID=node1 -``` +---- -### 3-Node Cluster Example +[[3-node-cluster-example]] +==== 3-Node Cluster Example -**Terminal 1 (Node 1 - Leader):** -```bash +*Terminal 1 (Node 1 - Leader):* + +[source,bash] +---- PHRONESIS_CONSENSUS_ENABLED=true \ PHRONESIS_NODE_ID=node1 \ iex --sname node1 --cookie phronesis_cluster -S mix -``` +---- + +*Terminal 2 (Node 2):* -**Terminal 2 (Node 2):** -```bash +[source,bash] +---- PHRONESIS_CONSENSUS_ENABLED=true \ PHRONESIS_NODE_ID=node2 \ iex --sname node2 --cookie phronesis_cluster -S mix -``` +---- -**Terminal 3 (Node 3):** -```bash +*Terminal 3 (Node 3):* + +[source,bash] +---- PHRONESIS_CONSENSUS_ENABLED=true \ PHRONESIS_NODE_ID=node3 \ iex --sname node3 --cookie phronesis_cluster -S mix -``` +---- -### Automated Demo Script +==== Automated Demo Script -```bash +[source,bash] +---- ./examples/consensus_cluster_demo.sh -``` +---- This script starts a 3-node cluster automatically. -## API Usage +=== API Usage ###Submitting a Vote -```elixir +[source,elixir] +---- # Vote on a policy action {:ok, consensus_achieved, votes} = Phronesis.Consensus.Server.vote( @@ -88,11 +101,12 @@ This script starts a 3-node cluster automatically. # Result: # consensus_achieved: true/false # votes: [{"agent1", true}, {"agent2", true}, {"agent3", false}] -``` +---- -### Querying Consensus Log +==== Querying Consensus Log -```elixir +[source,elixir] +---- # Get append-only consensus log {:ok, log} = Phronesis.Consensus.Server.get_log() @@ -104,11 +118,12 @@ This script starts a 3-node cluster automatically. # threshold: 0.67, # timestamp: ~U[2026-01-30 ...] # } -``` +---- -### Cluster Status +==== Cluster Status -```elixir +[source,elixir] +---- {:ok, status} = Phronesis.Consensus.Server.status() # Returns: @@ -121,81 +136,94 @@ This script starts a 3-node cluster automatically. # machine_version: 0, # members: [{:node1, :nonode@nohost}, {:node2, ...}] # } -``` +---- -### Adding Members +==== Adding Members -```elixir +[source,elixir] +---- # Add a new node to the cluster :ok = Phronesis.Consensus.Server.add_member(:node4) -``` +---- -## Stdlib Integration +=== Stdlib Integration -The `Phronesis.Stdlib.Consensus` module automatically uses distributed consensus when available: +The `Phronesis.Stdlib.Consensus` module automatically uses distributed +consensus when available: -```elixir +[source,elixir] +---- # Automatically uses Raft if PHRONESIS_CONSENSUS_ENABLED=true # Falls back to mock consensus otherwise {:ok, consensus_achieved, votes} = Phronesis.Stdlib.Consensus.vote(action, agents, threshold) -``` +---- -## Data Persistence +=== Data Persistence Consensus data is stored in `priv/consensus_data//`: -``` +.... priv/consensus_data/ ├── node1/ # Ra data for node 1 │ ├── snapshots/ │ └── wal/ # Write-ahead log ├── node2/ └── node3/ -``` +.... + +*Important:* Ensure this directory is persisted in production +deployments. + +=== Raft Consensus Properties -**Important:** Ensure this directory is persisted in production deployments. +==== Leader Election -## Raft Consensus Properties +* Automatic leader election on startup +* Re-election on leader failure +* Typical election time: < 1 second -### Leader Election -- Automatic leader election on startup -- Re-election on leader failure -- Typical election time: < 1 second +==== Log Replication -### Log Replication -- All writes go through the leader -- Replicated to majority of nodes before commit -- Strong consistency guarantees +* All writes go through the leader +* Replicated to majority of nodes before commit +* Strong consistency guarantees -### Fault Tolerance -- Tolerates `(N-1)/2` node failures (N = cluster size) -- 3-node cluster: tolerates 1 failure -- 5-node cluster: tolerates 2 failures +==== Fault Tolerance -### Byzantine Fault Tolerance -While Raft provides crash fault tolerance, true Byzantine fault tolerance requires: -1. Minimum 3f+1 nodes (f = Byzantine nodes) -2. Additional validation layers (crypto signatures, etc.) -3. This is Phase 3 future work +* Tolerates `(N-1)/2` node failures (N = cluster size) +* 3-node cluster: tolerates 1 failure +* 5-node cluster: tolerates 2 failures -## Testing +==== Byzantine Fault Tolerance -### Unit Tests +While Raft provides crash fault tolerance, true Byzantine fault +tolerance requires: -```bash +[arabic] +. Minimum 3f+1 nodes (f = Byzantine nodes) +. Additional validation layers (crypto signatures, etc.) +. This is Phase 3 future work + +=== Testing + +==== Unit Tests + +[source,bash] +---- # Mock consensus tests (always run) mix test test/consensus_test.exs # Distributed tests (tagged :skip by default) mix test --include skip test/consensus_test.exs -``` +---- -### Integration Tests +==== Integration Tests Run the demo script and interact with the cluster: -```bash +[source,bash] +---- ./examples/consensus_cluster_demo.sh # In another terminal: @@ -203,13 +231,14 @@ iex --sname client --remsh node1@localhost --cookie phronesis_cluster # Submit votes: Phronesis.Consensus.Server.vote({:accept, "Test"}, ["a1", "a2", "a3"], 0.67) -``` +---- -## Production Deployment +=== Production Deployment -### Docker Compose Example +==== Docker Compose Example -```yaml +[source,yaml] +---- version: '3' services: node1: @@ -246,68 +275,77 @@ volumes: node1_data: node2_data: node3_data: -``` +---- -### Kubernetes Example +==== Kubernetes Example -See `deploy/kubernetes/consensus-statefulset.yaml` for a production-ready StatefulSet configuration. +See `deploy/kubernetes/consensus-statefulset.yaml` for a +production-ready StatefulSet configuration. -## Monitoring +=== Monitoring -### Metrics to Track +==== Metrics to Track -- **Commit Index**: Current committed log position -- **Leader Changes**: Frequency of leader elections -- **Vote Latency**: Time to achieve consensus -- **Node Availability**: Uptime of cluster members +* *Commit Index*: Current committed log position +* *Leader Changes*: Frequency of leader elections +* *Vote Latency*: Time to achieve consensus +* *Node Availability*: Uptime of cluster members -### Health Checks +==== Health Checks -```elixir +[source,elixir] +---- # Check if node is healthy case Phronesis.Consensus.Server.status() do {:ok, %{state: :leader}} -> :healthy {:ok, %{state: :follower}} -> :healthy {:error, _} -> :unhealthy end -``` +---- -## Troubleshooting +=== Troubleshooting -### "system_not_started" Error +==== "system_not_started" Error Ra application not started. Ensure: -```elixir + +[source,elixir] +---- Application.ensure_all_started(:ra) -``` +---- -### Split Brain +==== Split Brain If nodes can't communicate: -1. Check network connectivity between nodes -2. Verify node names and cookies match -3. Check firewall rules (EPMD port 4369, distribution ports) -### Data Corruption +[arabic] +. Check network connectivity between nodes +. Verify node names and cookies match +. Check firewall rules (EPMD port 4369, distribution ports) + +==== Data Corruption If Ra data is corrupted: -```bash + +[source,bash] +---- # Stop all nodes # Delete consensus data rm -rf priv/consensus_data/* # Restart cluster -``` +---- -## References +=== References -- [Ra Documentation](https://github.com/rabbitmq/ra) -- [Raft Paper](https://raft.github.io/raft.pdf) -- [SPEC.core.scm](../SPEC.core.scm) - Phronesis consensus specification +* https://github.com/rabbitmq/ra[Ra Documentation] +* https://raft.github.io/raft.pdf[Raft Paper] +* link:../SPEC.core.scm[SPEC.core.scm] - Phronesis consensus +specification -## Future Work +=== Future Work -- [ ] Byzantine fault tolerance (PBFT integration) -- [ ] Dynamic membership changes -- [ ] Snapshot compression -- [ ] Metrics export (Prometheus) -- [ ] Admin dashboard for cluster management +* ☐ Byzantine fault tolerance (PBFT integration) +* ☐ Dynamic membership changes +* ☐ Snapshot compression +* ☐ Metrics export (Prometheus) +* ☐ Admin dashboard for cluster management diff --git a/LSP-IMPLEMENTATION-SUMMARY.adoc b/docs/LSP-IMPLEMENTATION-SUMMARY.adoc similarity index 100% rename from LSP-IMPLEMENTATION-SUMMARY.adoc rename to docs/LSP-IMPLEMENTATION-SUMMARY.adoc diff --git a/TEST-NEEDS.adoc b/docs/TEST-NEEDS.adoc similarity index 100% rename from TEST-NEEDS.adoc rename to docs/TEST-NEEDS.adoc diff --git a/TESTING-REPORT.adoc b/docs/TESTING-REPORT.adoc similarity index 100% rename from TESTING-REPORT.adoc rename to docs/TESTING-REPORT.adoc diff --git a/TOOLCHAIN-WISHLIST.adoc b/docs/TOOLCHAIN-WISHLIST.adoc similarity index 100% rename from TOOLCHAIN-WISHLIST.adoc rename to docs/TOOLCHAIN-WISHLIST.adoc diff --git a/WOKELANG-FEATURE-COMPARISON.adoc b/docs/WOKELANG-FEATURE-COMPARISON.adoc similarity index 100% rename from WOKELANG-FEATURE-COMPARISON.adoc rename to docs/WOKELANG-FEATURE-COMPARISON.adoc diff --git a/docs/safety_proofs.adoc b/docs/safety_proofs.adoc new file mode 100644 index 0000000..be06b9f --- /dev/null +++ b/docs/safety_proofs.adoc @@ -0,0 +1,598 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +== Phronesis: Safety Proofs + +=== Purpose + +This document formalizes safety guarantees for the Phronesis policy +language: + +[arabic] +. *Sandbox Isolation* - Policies cannot escape their execution +environment +. *Capability Enforcement* - Operations are restricted by capability +tokens +. *Byzantine Fault Tolerance* - Consensus holds under adversarial +conditions + +These proofs complement the operational semantics (termination, type +safety, consensus safety). + +''''' + +[[1-sandbox-isolation]] +=== 1. Sandbox Isolation + +[[11-threat-model]] +==== 1.1 Threat Model + +*Adversary capabilities:* + +* Can author arbitrary policy code +* Can attempt to access system resources +* Cannot modify the interpreter or runtime + +*Security goal:* Policy code cannot: + +* Access filesystem +* Make network connections +* Execute system commands +* Access memory outside its environment + +[[12-isolation-architecture]] +==== 1.2 Isolation Architecture + +.... +┌─────────────────────────────────────────────────────┐ +│ Host System │ +│ ┌───────────────────────────────────────────────┐ │ +│ │ Phronesis Runtime │ │ +│ │ ┌─────────────────────────────────────────┐ │ │ +│ │ │ Policy Sandbox │ │ │ +│ │ │ ┌─────────────────────────────────┐ │ │ │ +│ │ │ │ Policy Execution Context │ │ │ │ +│ │ │ │ - Environment (variables) │ │ │ │ +│ │ │ │ - PolicyTable (read-only) │ │ │ │ +│ │ │ │ - ConsensusLog (append-only) │ │ │ │ +│ │ │ └─────────────────────────────────┘ │ │ │ +│ │ │ ↑ Module Calls ↓ │ │ │ +│ │ │ ┌─────────────────────────────────┐ │ │ │ +│ │ │ │ Capability-Gated Modules │ │ │ │ +│ │ │ │ Std.RPKI, Std.BGP, Std.Consensus│ │ │ │ +│ │ │ └─────────────────────────────────┘ │ │ │ +│ │ └─────────────────────────────────────────┘ │ │ +│ └───────────────────────────────────────────────┘ │ +└─────────────────────────────────────────────────────┘ +.... + +[[13-formal-definition]] +==== 1.3 Formal Definition + +*Definition (Sandbox State):* + +.... +SandboxState = { + environment : Map, + policy_table : Map, + consensus_log : List, + capabilities : Set +} +.... + +*Definition (Valid State Transition):* + +.... +A state transition S → S' is valid iff: + 1. S'.environment ⊇ S.environment (monotonic growth only) + 2. S'.policy_table ⊇ S.policy_table (policies can be added, not removed) + 3. S'.consensus_log = S.consensus_log ++ [new_entries] (append-only) + 4. ∀ operation in transition: required_cap(operation) ∈ S.capabilities +.... + +[[14-isolation-theorem]] +==== 1.4 Isolation Theorem + +*Theorem 1 (Sandbox Isolation):* For any policy P and initial state S₀, +executing P cannot: + +[arabic] +. Read or write files +. Make network connections +. Execute system commands +. Access memory outside the sandbox + +*Proof:* + +*(1) No file operations:* + +By grammar inspection, the only operations are: + +* `EXECUTE(f, args)` - calls a registered function +* `REPORT(msg)` - logs to ConsensusLog +* `REJECT(reason)` - returns result +* `ACCEPT(reason)` - returns result + +None of these map to file operations. The interpreter's +`do_execute_action/2` function handles these exhaustively: + +[source,elixir] +---- +defp do_execute_action({:execute, function, args}, state) do + call_module([function], args, state) # Only registered modules +end +---- + +Module lookup is restricted to the `modules` registry. File operations +are not exposed. ∎ + +*(2) No network connections:* + +Network operations require calling into Erlang's `:gen_tcp`, `:ssl`, or +`:httpc` modules. These are not exposed in the standard library. + +The `Std.*` modules only provide: + +* `Std.RPKI.validate/1` - Pure function (stub or cached lookup) +* `Std.BGP.extract_as_path/1` - Pure function +* `Std.Consensus.require_votes/2` - Uses internal agent registry +* `Std.Temporal.eventually/2` - Uses `Process.sleep` only + +No network primitives are exposed. ∎ + +*(3) No system commands:* + +The interpreter has no path to `System.cmd/3` or `:os.cmd/1`. Function +calls go through `call_module/3` which only resolves: + +* Registered `Std.*` modules +* User-registered modules (controlled by host) + +[source,elixir] +---- +defp call_module(path, args, state) do + case State.lookup_module(state, path) do + {:ok, module} -> module.call(args) # Only registered modules + :error -> resolve_builtin_module(path, args) # Fixed set + end +end +---- + +The fixed builtin set contains no system access. ∎ + +*(4) Memory isolation:* + +The execution state is a pure Elixir struct. Variables are stored in +`state.environment`, a simple `Map`. There is no pointer arithmetic or +memory access beyond the map operations `Map.put/3` and `Map.fetch/2`. + +The BEAM VM provides memory safety guarantees at the language level. ∎ + +*QED: Sandbox Isolation holds.* ∎ + +''''' + +[[2-capability-enforcement]] +=== 2. Capability Enforcement + +[[21-capability-model]] +==== 2.1 Capability Model + +*Definition (Capability):* + +.... +Capability = { + resource : ResourceType, + operations : Set, + constraints : List +} + +ResourceType = RouteTable | ConsensusVote | NetworkInterface | ... +Operation = Read | Write | Execute | Vote | ... +Constraint = TimeBound(start, end) | RateLimited(n, period) | ... +.... + +[[22-capability-tokens]] +==== 2.2 Capability Tokens + +Each policy execution context has a set of capability tokens: + +[source,elixir] +---- +@type capability :: %{ + resource: atom(), + operations: [atom()], + constraints: [constraint()] +} + +@type context :: %{ + capabilities: [capability()], + # ... other fields +} +---- + +[[23-enforcement-points]] +==== 2.3 Enforcement Points + +*Point 1: Module Call* + +[source,elixir] +---- +defp call_module(path, args, state) do + required_cap = capability_for_module(path) + + if has_capability?(state, required_cap) do + module.call(args) + else + {:error, {:capability_denied, path, required_cap}} + end +end +---- + +*Point 2: Action Execution* + +[source,elixir] +---- +defp do_execute_action(action, state) do + required_cap = capability_for_action(action) + + unless has_capability?(state, required_cap) do + raise CapabilityError, action: action, required: required_cap + end + + # ... proceed with execution +end +---- + +[[24-capability-soundness]] +==== 2.4 Capability Soundness + +*Theorem 2 (Capability Soundness):* No operation executes without the +required capability. + +*Proof:* + +By inspection of execution paths: + +[arabic] +. *EXECUTE* actions go through `call_module/3` which checks capabilities +. *Module calls* in expressions go through the same path +. *REPORT* requires `{:consensus_log, [:append]}` +. *REJECT/ACCEPT* require `{:route_decision, [:write]}` + +All paths have enforcement points. ∎ + +*Mechanized (Lean 4):* This argument is machine-checked in +link:../academic/formal-verification/lean4/Phronesis.lean[`../academic/formal-verification/lean4/Phronesis.lean`]. +The execution relation `Executes` is capability-gated _by construction_ +— every leaf rule carries the required-capability membership as a +hypothesis, and there is deliberately no constructor that executes +without an enforcement point — so `capability_soundness` follows by +inversion (the informal "by inspection of execution paths" made formal). +`capability_soundness_ite` extends it through conditional actions. The +two §2.5 side-properties are mechanized as `least_privilege` and +`no_escalation`. All four are `sorry`-free (only Lean's standard +`propext`; confirm with `#print axioms`). + +[[25-capability-composition]] +==== 2.5 Capability Composition + +*Property (Least Privilege):* A policy receives only capabilities +explicitly granted: + +[source,elixir] +---- +def new_policy_context(policy, grants) do + %{ + capabilities: filter_grants(grants, policy.id), + # ... other context + } +end +---- + +*Property (No Capability Escalation):* A policy cannot acquire +capabilities it wasn't granted: + +.... +∀ S, S'. (S → S') ⟹ S'.capabilities ⊆ S.capabilities +.... + +This holds because capabilities are only set at context creation and +never modified during execution. ∎ + +[[26-ethical-verdict-consistency]] +==== 2.6 Ethical Verdict Consistency + +*Theorem (Policy-Arbitration Soundness):* Phronesis resolves conflicting +policies by _priority-ordered first match_ (`lib/phronesis/state.ex` +`policies_by_priority` + the first-match evaluation in +`spec/SPEC.core.scm`). The decision procedure is sound, decisive, and +respects priority: + +[arabic] +. *Soundness* — a verdict is produced only by a policy that genuinely +matches the situation and is in the policy set (no spurious verdicts). +. *Decisiveness* — whenever some policy applies, a verdict is produced. +. *Priority-maximal override* — the deciding policy has maximal priority +among all matching policies; hence a higher-priority verdict is never +overridden by a lower-priority one (e.g. a high-priority `REJECT` cannot +be undercut by a lower-priority `ACCEPT` — the core ethical override). ∎ + +*Mechanized (Lean 4):* Machine-checked in +link:../academic/formal-verification/lean4/Phronesis.lean[`../academic/formal-verification/lean4/Phronesis.lean`] +as `bestMatch_sound`, `bestMatch_none`, `bestMatch_decisive`, and +`bestMatch_maximal` over the real `PhrPolicy` record. Arbitration is +modelled as the `bestMatch` fold (highest-priority matching policy, ties +to the earlier policy); `matches` abstracts condition evaluation, +decoupling arbitration soundness from the expression semantics. All four +are `sorry`-free (only Lean's standard `propext`/`Quot.sound`; confirm +with `#print axioms`). + +''''' + +[[3-byzantine-fault-tolerance]] +=== 3. Byzantine Fault Tolerance + +[[31-system-model]] +==== 3.1 System Model + +*Assumptions:* + +* N total agents (policy evaluators) +* f Byzantine (malicious) agents where N ≥ 3f + 1 +* Asynchronous network with eventual delivery +* Cryptographic primitives are secure + +[[32-consensus-protocol]] +==== 3.2 Consensus Protocol + +Phronesis uses a simplified PBFT-style protocol: + +.... +Phase 1: PROPOSE + Leader proposes action to all agents + +Phase 2: VOTE + Each agent evaluates policy and votes + Votes are signed with agent's key + +Phase 3: COMMIT + If votes ≥ threshold, action commits + Result logged to ConsensusLog +.... + +[[33-safety-properties]] +==== 3.3 Safety Properties + +*Property (Agreement):* All honest agents agree on the execution result. + +*Property (Validity):* If all honest agents have the same input, the +result reflects that input. + +*Property (Termination):* Every action eventually commits or aborts. + +[[34-bft-safety-theorem]] +==== 3.4 BFT Safety Theorem + +*Theorem 3 (Byzantine Safety):* With N ≥ 3f + 1 agents and threshold t = +(2N + 1) / 3: + +[arabic] +. No conflicting actions commit +. Byzantine agents cannot force invalid actions + +*Proof Sketch:* + +*(1) No conflicting actions:* + +Suppose actions A and A' both commit for the same policy invocation. + +* A commits: at least t agents voted for A +* A' commits: at least t agents voted for A' + +With t = (2N + 1) / 3, we have: + +* Votes for A ≥ (2N + 1) / 3 +* Votes for A' ≥ (2N + 1) / 3 +* Total votes ≥ (4N + 2) / 3 > N (contradiction) + +Therefore, at most one action commits. ∎ + +*(2) Byzantine agents cannot force invalid actions:* + +Byzantine agents control at most f votes. Valid commit requires t = (2N ++ 1) / 3 votes. + +For N = 3f + 1: + +* t = (6f + 3) / 3 = 2f + 1 +* f < 2f + 1 = t + +Byzantine agents alone cannot reach threshold. At least f + 1 honest +agents must vote for commit. Honest agents only vote for valid actions +(by definition). Therefore, only valid actions can commit. ∎ + +*QED: Byzantine Safety holds.* ∎ + +*Verified two ways:* + +* *Model-checked (TLA+/TLC):* +link:../formal/PhronesisConsensus.tla[`../formal/PhronesisConsensus.tla`] +exhaustively checks `Agreement`/`Validity`/`ByzantineSafety` for the +instance N = 4, F = 1, with a negative test confirming the `2F+1` +threshold is load-bearing (Agreement fails below it). +* *Mechanized (Lean 4):* +link:../academic/formal-verification/lean4/Phronesis.lean[`../academic/formal-verification/lean4/Phronesis.lean`] +proves the quorum-intersection argument for *all* N, F: +`bft_no_two_quorums` (with `n ≤ 3f+1` and threshold `2f+1`, two distinct +values cannot both reach a quorum) and `bft_agreement` (any two +committed values are equal). Every cardinality fact — +inclusion–exclusion (`countP_incl_excl`), the union bound, and +monotonicity — is _proved_ over `countP`, not assumed. All `sorry`-free +(Lean's standard `propext`/`Quot.sound`/`Classical.choice`; confirm with +`#print axioms`). + +[[35-liveness-under-partial-synchrony]] +==== 3.5 Liveness Under Partial Synchrony + +*Theorem 4 (Eventual Liveness):* After GST (Global Stabilization Time), +all valid actions eventually commit. + +*Proof:* + +After GST, messages are delivered within bound Δ. Honest agents (≥ 2f + +1) will receive proposals and vote. With 2f + 1 ≥ t votes, action +commits. Timeout mechanism ensures progress even with crashed leader. ∎ + +''''' + +[[4-combined-security-analysis]] +=== 4. Combined Security Analysis + +[[41-defense-in-depth]] +==== 4.1 Defense in Depth + +.... +Layer 1: Grammar Restrictions + └── No loops, no recursion, no I/O primitives + +Layer 2: Sandbox Isolation + └── Memory isolation, no system access + +Layer 3: Capability Enforcement + └── Explicit grants for each operation + +Layer 4: Consensus Requirements + └── Multi-party agreement for actions + +Layer 5: Audit Log + └── Immutable record of all executions +.... + +[[42-attack-surface-analysis]] +==== 4.2 Attack Surface Analysis + +[cols=",,",options="header",] +|=== +|Attack Vector |Mitigation |Proof Reference +|Code injection |Grammar rejects unknown constructs |Theorem 1.1 + +|Sandbox escape |No I/O primitives exposed |Theorem 1 + +|Privilege escalation |Capability checking at all entry points |Theorem +2 + +|Byzantine corruption |BFT consensus with f < N/3 |Theorem 3 + +|Denial of service |Termination guarantee |Semantics doc + +|Repudiation |Append-only ConsensusLog |Semantics doc +|=== + +[[43-residual-risks]] +==== 4.3 Residual Risks + +*R1: Side-channel attacks* + +* Timing attacks on module calls +* Mitigation: Constant-time operations where feasible + +*R2: Resource exhaustion* + +* Large policies could consume memory +* Mitigation: Policy size limits, resource quotas + +*R3: Cryptographic weaknesses* + +* Depends on underlying crypto library +* Mitigation: Use well-audited libraries (Erlang :crypto) + +''''' + +[[5-mechanization-status]] +=== 5. Mechanization Status + +[cols=",,",options="header",] +|=== +|Property |Status |Proof System +|Sandbox Isolation |Mechanized (Lean 4) +|`academic/formal-verification/lean4/Phronesis.lean` + +|Capability Soundness |Mechanized (Lean 4) +|`academic/formal-verification/lean4/Phronesis.lean` + +|Ethical Verdict Consistency |Mechanized (Lean 4) +|`academic/formal-verification/lean4/Phronesis.lean` + +|BFT Safety |Model-checked (TLA+/TLC) + Mechanized (Lean 4) +|`formal/PhronesisConsensus.tla`, +`academic/formal-verification/lean4/Phronesis.lean` + +|BFT Liveness |Manual proof |This document + +|Termination |Proven |Semantics doc + +|Type Safety |Sketch |Semantics doc +|=== + +[[51-future-mechanization]] +==== 5.1 Future Mechanization + +*TLA+ (Consensus Protocol):* + +[source,tla] +---- +VARIABLES + votes, \* Map: Agent -> Vote + committed, \* Boolean + log \* Sequence of LogEntry + +BFTSafety == + \A a1, a2 \in CommittedActions: + a1 = a2 \/ ~Conflict(a1, a2) +---- + +*Coq (Language Properties):* + +[source,coq] +---- +Theorem sandbox_isolation: + forall (p : Policy) (s : State), + WellFormed p -> + ~(Executes p FileOp) /\ + ~(Executes p NetworkOp) /\ + ~(Executes p SystemOp). +---- + +''''' + +[[6-for-irtf-submission]] +=== 6. For IRTF Submission + +Include as *Appendix C: Safety Proofs* with: + +[arabic] +. Summary of threat model +. Key theorems (Isolation, Capability, BFT) +. References to formal verification (TLA+, Coq) + +*Abstract for section:* + +____ +"We prove that Phronesis policies execute within a secure sandbox, +enforce capability-based access control, and achieve Byzantine fault +tolerance with N ≥ 3f + 1 agents. These properties ensure that network +policies cannot be corrupted by malicious actors and that all policy +decisions are auditable and non-repudiable." +____ + +''''' + +=== References + +[arabic] +. Castro, M., & Liskov, B. (1999). Practical Byzantine Fault Tolerance. +OSDI. +. Miller, M. S., et al. (2003). Capability Myths Demolished. +. Wahby, R. S., et al. (2017). Verifiable ASICs. +. Patrignani, M., et al. (2019). Formal Approaches to Secure +Compilation. diff --git a/docs/safety_proofs.md b/docs/safety_proofs.md deleted file mode 100644 index 5f13af0..0000000 --- a/docs/safety_proofs.md +++ /dev/null @@ -1,509 +0,0 @@ - -# Phronesis: Safety Proofs - -## Purpose - -This document formalizes safety guarantees for the Phronesis policy language: - -1. **Sandbox Isolation** - Policies cannot escape their execution environment -2. **Capability Enforcement** - Operations are restricted by capability tokens -3. **Byzantine Fault Tolerance** - Consensus holds under adversarial conditions - -These proofs complement the operational semantics (termination, type safety, consensus safety). - ---- - -## 1. Sandbox Isolation - -### 1.1 Threat Model - -**Adversary capabilities:** -- Can author arbitrary policy code -- Can attempt to access system resources -- Cannot modify the interpreter or runtime - -**Security goal:** Policy code cannot: -- Access filesystem -- Make network connections -- Execute system commands -- Access memory outside its environment - -### 1.2 Isolation Architecture - -``` -┌─────────────────────────────────────────────────────┐ -│ Host System │ -│ ┌───────────────────────────────────────────────┐ │ -│ │ Phronesis Runtime │ │ -│ │ ┌─────────────────────────────────────────┐ │ │ -│ │ │ Policy Sandbox │ │ │ -│ │ │ ┌─────────────────────────────────┐ │ │ │ -│ │ │ │ Policy Execution Context │ │ │ │ -│ │ │ │ - Environment (variables) │ │ │ │ -│ │ │ │ - PolicyTable (read-only) │ │ │ │ -│ │ │ │ - ConsensusLog (append-only) │ │ │ │ -│ │ │ └─────────────────────────────────┘ │ │ │ -│ │ │ ↑ Module Calls ↓ │ │ │ -│ │ │ ┌─────────────────────────────────┐ │ │ │ -│ │ │ │ Capability-Gated Modules │ │ │ │ -│ │ │ │ Std.RPKI, Std.BGP, Std.Consensus│ │ │ │ -│ │ │ └─────────────────────────────────┘ │ │ │ -│ │ └─────────────────────────────────────────┘ │ │ -│ └───────────────────────────────────────────────┘ │ -└─────────────────────────────────────────────────────┘ -``` - -### 1.3 Formal Definition - -**Definition (Sandbox State):** -``` -SandboxState = { - environment : Map, - policy_table : Map, - consensus_log : List, - capabilities : Set -} -``` - -**Definition (Valid State Transition):** -``` -A state transition S → S' is valid iff: - 1. S'.environment ⊇ S.environment (monotonic growth only) - 2. S'.policy_table ⊇ S.policy_table (policies can be added, not removed) - 3. S'.consensus_log = S.consensus_log ++ [new_entries] (append-only) - 4. ∀ operation in transition: required_cap(operation) ∈ S.capabilities -``` - -### 1.4 Isolation Theorem - -**Theorem 1 (Sandbox Isolation):** -For any policy P and initial state S₀, executing P cannot: -1. Read or write files -2. Make network connections -3. Execute system commands -4. Access memory outside the sandbox - -**Proof:** - -**(1) No file operations:** - -By grammar inspection, the only operations are: -- `EXECUTE(f, args)` - calls a registered function -- `REPORT(msg)` - logs to ConsensusLog -- `REJECT(reason)` - returns result -- `ACCEPT(reason)` - returns result - -None of these map to file operations. The interpreter's `do_execute_action/2` -function handles these exhaustively: - -```elixir -defp do_execute_action({:execute, function, args}, state) do - call_module([function], args, state) # Only registered modules -end -``` - -Module lookup is restricted to the `modules` registry. File operations -are not exposed. ∎ - -**(2) No network connections:** - -Network operations require calling into Erlang's `:gen_tcp`, `:ssl`, or -`:httpc` modules. These are not exposed in the standard library. - -The `Std.*` modules only provide: -- `Std.RPKI.validate/1` - Pure function (stub or cached lookup) -- `Std.BGP.extract_as_path/1` - Pure function -- `Std.Consensus.require_votes/2` - Uses internal agent registry -- `Std.Temporal.eventually/2` - Uses `Process.sleep` only - -No network primitives are exposed. ∎ - -**(3) No system commands:** - -The interpreter has no path to `System.cmd/3` or `:os.cmd/1`. -Function calls go through `call_module/3` which only resolves: -- Registered `Std.*` modules -- User-registered modules (controlled by host) - -```elixir -defp call_module(path, args, state) do - case State.lookup_module(state, path) do - {:ok, module} -> module.call(args) # Only registered modules - :error -> resolve_builtin_module(path, args) # Fixed set - end -end -``` - -The fixed builtin set contains no system access. ∎ - -**(4) Memory isolation:** - -The execution state is a pure Elixir struct. Variables are stored in -`state.environment`, a simple `Map`. There is no pointer arithmetic -or memory access beyond the map operations `Map.put/3` and `Map.fetch/2`. - -The BEAM VM provides memory safety guarantees at the language level. ∎ - -**QED: Sandbox Isolation holds.** ∎ - ---- - -## 2. Capability Enforcement - -### 2.1 Capability Model - -**Definition (Capability):** -``` -Capability = { - resource : ResourceType, - operations : Set, - constraints : List -} - -ResourceType = RouteTable | ConsensusVote | NetworkInterface | ... -Operation = Read | Write | Execute | Vote | ... -Constraint = TimeBound(start, end) | RateLimited(n, period) | ... -``` - -### 2.2 Capability Tokens - -Each policy execution context has a set of capability tokens: - -```elixir -@type capability :: %{ - resource: atom(), - operations: [atom()], - constraints: [constraint()] -} - -@type context :: %{ - capabilities: [capability()], - # ... other fields -} -``` - -### 2.3 Enforcement Points - -**Point 1: Module Call** -```elixir -defp call_module(path, args, state) do - required_cap = capability_for_module(path) - - if has_capability?(state, required_cap) do - module.call(args) - else - {:error, {:capability_denied, path, required_cap}} - end -end -``` - -**Point 2: Action Execution** -```elixir -defp do_execute_action(action, state) do - required_cap = capability_for_action(action) - - unless has_capability?(state, required_cap) do - raise CapabilityError, action: action, required: required_cap - end - - # ... proceed with execution -end -``` - -### 2.4 Capability Soundness - -**Theorem 2 (Capability Soundness):** -No operation executes without the required capability. - -**Proof:** - -By inspection of execution paths: - -1. **EXECUTE** actions go through `call_module/3` which checks capabilities -2. **Module calls** in expressions go through the same path -3. **REPORT** requires `{:consensus_log, [:append]}` -4. **REJECT/ACCEPT** require `{:route_decision, [:write]}` - -All paths have enforcement points. ∎ - -**Mechanized (Lean 4):** This argument is machine-checked in -[`../academic/formal-verification/lean4/Phronesis.lean`](../academic/formal-verification/lean4/Phronesis.lean). -The execution relation `Executes` is capability-gated *by construction* — every -leaf rule carries the required-capability membership as a hypothesis, and there -is deliberately no constructor that executes without an enforcement point — so -`capability_soundness` follows by inversion (the informal "by inspection of -execution paths" made formal). `capability_soundness_ite` extends it through -conditional actions. The two §2.5 side-properties are mechanized as -`least_privilege` and `no_escalation`. All four are `sorry`-free (only Lean's -standard `propext`; confirm with `#print axioms`). - -### 2.5 Capability Composition - -**Property (Least Privilege):** -A policy receives only capabilities explicitly granted: - -```elixir -def new_policy_context(policy, grants) do - %{ - capabilities: filter_grants(grants, policy.id), - # ... other context - } -end -``` - -**Property (No Capability Escalation):** -A policy cannot acquire capabilities it wasn't granted: - -``` -∀ S, S'. (S → S') ⟹ S'.capabilities ⊆ S.capabilities -``` - -This holds because capabilities are only set at context creation -and never modified during execution. ∎ - -### 2.6 Ethical Verdict Consistency - -**Theorem (Policy-Arbitration Soundness):** -Phronesis resolves conflicting policies by *priority-ordered first match* -(`lib/phronesis/state.ex` `policies_by_priority` + the first-match evaluation in -`spec/SPEC.core.scm`). The decision procedure is sound, decisive, and respects -priority: - -1. **Soundness** — a verdict is produced only by a policy that genuinely matches - the situation and is in the policy set (no spurious verdicts). -2. **Decisiveness** — whenever some policy applies, a verdict is produced. -3. **Priority-maximal override** — the deciding policy has maximal priority among - all matching policies; hence a higher-priority verdict is never overridden by - a lower-priority one (e.g. a high-priority `REJECT` cannot be undercut by a - lower-priority `ACCEPT` — the core ethical override). ∎ - -**Mechanized (Lean 4):** Machine-checked in -[`../academic/formal-verification/lean4/Phronesis.lean`](../academic/formal-verification/lean4/Phronesis.lean) -as `bestMatch_sound`, `bestMatch_none`, `bestMatch_decisive`, and -`bestMatch_maximal` over the real `PhrPolicy` record. Arbitration is modelled as -the `bestMatch` fold (highest-priority matching policy, ties to the earlier -policy); `matches` abstracts condition evaluation, decoupling arbitration -soundness from the expression semantics. All four are `sorry`-free (only Lean's -standard `propext`/`Quot.sound`; confirm with `#print axioms`). - ---- - -## 3. Byzantine Fault Tolerance - -### 3.1 System Model - -**Assumptions:** -- N total agents (policy evaluators) -- f Byzantine (malicious) agents where N ≥ 3f + 1 -- Asynchronous network with eventual delivery -- Cryptographic primitives are secure - -### 3.2 Consensus Protocol - -Phronesis uses a simplified PBFT-style protocol: - -``` -Phase 1: PROPOSE - Leader proposes action to all agents - -Phase 2: VOTE - Each agent evaluates policy and votes - Votes are signed with agent's key - -Phase 3: COMMIT - If votes ≥ threshold, action commits - Result logged to ConsensusLog -``` - -### 3.3 Safety Properties - -**Property (Agreement):** -All honest agents agree on the execution result. - -**Property (Validity):** -If all honest agents have the same input, the result reflects that input. - -**Property (Termination):** -Every action eventually commits or aborts. - -### 3.4 BFT Safety Theorem - -**Theorem 3 (Byzantine Safety):** -With N ≥ 3f + 1 agents and threshold t = (2N + 1) / 3: -1. No conflicting actions commit -2. Byzantine agents cannot force invalid actions - -**Proof Sketch:** - -**(1) No conflicting actions:** - -Suppose actions A and A' both commit for the same policy invocation. - -- A commits: at least t agents voted for A -- A' commits: at least t agents voted for A' - -With t = (2N + 1) / 3, we have: -- Votes for A ≥ (2N + 1) / 3 -- Votes for A' ≥ (2N + 1) / 3 -- Total votes ≥ (4N + 2) / 3 > N (contradiction) - -Therefore, at most one action commits. ∎ - -**(2) Byzantine agents cannot force invalid actions:** - -Byzantine agents control at most f votes. -Valid commit requires t = (2N + 1) / 3 votes. - -For N = 3f + 1: -- t = (6f + 3) / 3 = 2f + 1 -- f < 2f + 1 = t - -Byzantine agents alone cannot reach threshold. -At least f + 1 honest agents must vote for commit. -Honest agents only vote for valid actions (by definition). -Therefore, only valid actions can commit. ∎ - -**QED: Byzantine Safety holds.** ∎ - -**Verified two ways:** - -- **Model-checked (TLA+/TLC):** [`../formal/PhronesisConsensus.tla`](../formal/PhronesisConsensus.tla) - exhaustively checks `Agreement`/`Validity`/`ByzantineSafety` for the instance - N = 4, F = 1, with a negative test confirming the `2F+1` threshold is - load-bearing (Agreement fails below it). -- **Mechanized (Lean 4):** [`../academic/formal-verification/lean4/Phronesis.lean`](../academic/formal-verification/lean4/Phronesis.lean) - proves the quorum-intersection argument for **all** N, F: - `bft_no_two_quorums` (with `n ≤ 3f+1` and threshold `2f+1`, two distinct - values cannot both reach a quorum) and `bft_agreement` (any two committed - values are equal). Every cardinality fact — inclusion–exclusion - (`countP_incl_excl`), the union bound, and monotonicity — is *proved* over - `countP`, not assumed. All `sorry`-free (Lean's standard - `propext`/`Quot.sound`/`Classical.choice`; confirm with `#print axioms`). - -### 3.5 Liveness Under Partial Synchrony - -**Theorem 4 (Eventual Liveness):** -After GST (Global Stabilization Time), all valid actions eventually commit. - -**Proof:** - -After GST, messages are delivered within bound Δ. -Honest agents (≥ 2f + 1) will receive proposals and vote. -With 2f + 1 ≥ t votes, action commits. -Timeout mechanism ensures progress even with crashed leader. ∎ - ---- - -## 4. Combined Security Analysis - -### 4.1 Defense in Depth - -``` -Layer 1: Grammar Restrictions - └── No loops, no recursion, no I/O primitives - -Layer 2: Sandbox Isolation - └── Memory isolation, no system access - -Layer 3: Capability Enforcement - └── Explicit grants for each operation - -Layer 4: Consensus Requirements - └── Multi-party agreement for actions - -Layer 5: Audit Log - └── Immutable record of all executions -``` - -### 4.2 Attack Surface Analysis - -| Attack Vector | Mitigation | Proof Reference | -|---------------|------------|-----------------| -| Code injection | Grammar rejects unknown constructs | Theorem 1.1 | -| Sandbox escape | No I/O primitives exposed | Theorem 1 | -| Privilege escalation | Capability checking at all entry points | Theorem 2 | -| Byzantine corruption | BFT consensus with f < N/3 | Theorem 3 | -| Denial of service | Termination guarantee | Semantics doc | -| Repudiation | Append-only ConsensusLog | Semantics doc | - -### 4.3 Residual Risks - -**R1: Side-channel attacks** -- Timing attacks on module calls -- Mitigation: Constant-time operations where feasible - -**R2: Resource exhaustion** -- Large policies could consume memory -- Mitigation: Policy size limits, resource quotas - -**R3: Cryptographic weaknesses** -- Depends on underlying crypto library -- Mitigation: Use well-audited libraries (Erlang :crypto) - ---- - -## 5. Mechanization Status - -| Property | Status | Proof System | -|----------|--------|--------------| -| Sandbox Isolation | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` | -| Capability Soundness | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` | -| Ethical Verdict Consistency | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` | -| BFT Safety | Model-checked (TLA+/TLC) + Mechanized (Lean 4) | `formal/PhronesisConsensus.tla`, `academic/formal-verification/lean4/Phronesis.lean` | -| BFT Liveness | Manual proof | This document | -| Termination | Proven | Semantics doc | -| Type Safety | Sketch | Semantics doc | - -### 5.1 Future Mechanization - -**TLA+ (Consensus Protocol):** -```tla -VARIABLES - votes, \* Map: Agent -> Vote - committed, \* Boolean - log \* Sequence of LogEntry - -BFTSafety == - \A a1, a2 \in CommittedActions: - a1 = a2 \/ ~Conflict(a1, a2) -``` - -**Coq (Language Properties):** -```coq -Theorem sandbox_isolation: - forall (p : Policy) (s : State), - WellFormed p -> - ~(Executes p FileOp) /\ - ~(Executes p NetworkOp) /\ - ~(Executes p SystemOp). -``` - ---- - -## 6. For IRTF Submission - -Include as **Appendix C: Safety Proofs** with: - -1. Summary of threat model -2. Key theorems (Isolation, Capability, BFT) -3. References to formal verification (TLA+, Coq) - -**Abstract for section:** - -> "We prove that Phronesis policies execute within a secure sandbox, -> enforce capability-based access control, and achieve Byzantine -> fault tolerance with N ≥ 3f + 1 agents. These properties ensure -> that network policies cannot be corrupted by malicious actors -> and that all policy decisions are auditable and non-repudiable." - ---- - -## References - -1. Castro, M., & Liskov, B. (1999). Practical Byzantine Fault Tolerance. OSDI. -2. Miller, M. S., et al. (2003). Capability Myths Demolished. -3. Wahby, R. S., et al. (2017). Verifiable ASICs. -4. Patrignani, M., et al. (2019). Formal Approaches to Secure Compilation. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..2c77ecb --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +[[tech-debt-audit--phronesis--2026-05-26]] +== Tech-Debt Audit — phronesis — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`hyperpolymath/standards` +2026-05-26-estate-*-debt audits]. *Combined severity:* `MEDIUM`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a 'Recommended next move' line; closing the +debt is follow-up work. + +[[1-proof-debt]] +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 5 | Coq-Axm/Adm= 0 | Lean-srry/ax= 1 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 1. *Severity:* `>01`. + +*Marker types* (any non-zero counts above): + +* Coq `Axiom`/`Admitted` — unconditional proof escapes. +* Lean `sorry`/`axiom` — Lean's equivalent. +* Agda `postulate` — accepted axiomatically. +* Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality +assumption. +* Idris2 top-level `partial` — totality-check waived. +* F* `assume val`/`admit_p` — F* admit. +* `TODO PROOF` / `OWED:` — self-documented debt markers. +* `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches +in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in +`docs/proof-debt.md`. + +[[2-licence-debt]] +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`LICENSE` +|SPDX header |`MPL-2.0` +|Manifest licence |`MPL-2.0` +|Body classifier |`Palimp-MPL-2.0` +|Severity |`ok` +|=== + +*Recommended next move:* none for licence. + +[[3-documentation-debt]] +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |143 +|`docs/` files |2 +|`docs/` LoC |762 +|CHANGELOG.md |N +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`MEDIUM` +|=== + +*Recommended next move:* introduce a `docs/` directory. The README at +143 lines has likely grown to do the work of `docs/` — split it into a +thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki +exemplars to copy from: `affinescript`, `boj-server`, `echidna`, +`hypatia`. + +Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one — +adopting a CHANGELOG (or auto-generating via `git-cliff`) is a +recommended estate-wide follow-up. + +=== Cross-references + +* Estate proof-debt audit: +`hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` +* Estate licence-debt audit: +`hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` +* Estate documentation-debt audit: +`hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index d563377..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,72 +0,0 @@ - -# Tech-Debt Audit — phronesis — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `MEDIUM`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 5 | Coq-Axm/Adm= 0 | Lean-srry/ax= 1 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 1. **Severity:** `>01`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `MPL-2.0` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 143 | -| `docs/` files | 2 | -| `docs/` LoC | 762 | -| CHANGELOG.md | N | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `MEDIUM` | - -**Recommended next move:** introduce a `docs/` directory. The README at 143 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`. - -Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/editors/vscode/README.adoc b/editors/vscode/README.adoc new file mode 100644 index 0000000..e80865e --- /dev/null +++ b/editors/vscode/README.adoc @@ -0,0 +1,165 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +== Phronesis VSCode Extension + +VSCode extension for Phronesis policy language with LSP support. + +=== Features + +* *Syntax Highlighting* - Full language support +* *Auto-Completion* - Keywords, stdlib functions, variables +* *Hover Documentation* - Inline docs for functions and keywords +* *Go to Definition* - Jump to policy/constant definitions +* *Real-time Diagnostics* - Syntax errors and warnings +* *Code Formatting* - Auto-format on save + +=== Installation + +==== From Source + +[arabic] +. *Build the extension:* ++ +[source,bash] +---- +cd editors/vscode +npm install +npm run compile +---- +. *Install phronesis CLI:* ++ +[source,bash] +---- +mix escript.build +# Add to PATH or configure extension +---- +. *Install extension:* ++ +[source,bash] +---- +code --install-extension phronesis-0.2.0.vsix +---- ++ +Or copy to extensions directory: ++ +[source,bash] +---- +cp -r . ~/.vscode/extensions/phronesis-0.2.0/ +---- + +==== Configuration + +Open VSCode settings and configure: + +[source,json] +---- +{ + "phronesis.serverPath": "/path/to/phronesis", + "phronesis.trace.server": "off" +} +---- + +=== Usage + +[arabic] +. Open a `.phr` file +. LSP server starts automatically +. Auto-completion: Type `Std.` to see stdlib modules +. Hover over keywords/functions for documentation +. F12 / Cmd+Click for go-to-definition + +=== Features in Detail + +==== Auto-Completion + +* *Keywords*: `POLICY`, `CONST`, `IMPORT`, `ACCEPT`, `REJECT`, etc. +* *Standard Library*: `Std.RPKI.*`, `Std.BGP.*`, `Std.Consensus.*`, +`Std.Temporal.*` +* *Functions*: All stdlib functions with signatures + +Example: + +[source,phronesis] +---- +Std.R # Auto-complete shows: Std.RPKI +Std.RPKI. # Shows: validate, check_origin, validation_status +---- + +==== Hover Documentation + +Hover over any keyword or function to see: + +* Syntax +* Parameters +* Return type +* Examples + +==== Diagnostics + +Real-time error checking: + +* Syntax errors (lexer/parser) +* Linter warnings +* Type issues + +==== Formatting + +Format document: `Shift+Alt+F` or save with format-on-save enabled. + +=== Troubleshooting + +==== LSP server not starting + +[arabic] +. Check phronesis is installed: ++ +[source,bash] +---- +which phronesis +phronesis --version +---- +. Check server path in settings +. View LSP logs: `Output` → `Phronesis Language Server` + +==== No auto-completion + +[arabic] +. Ensure `.phr` file is recognized as Phronesis language +. Restart LSP: `Cmd+Shift+P` → "Restart Language Server" + +=== Development + +==== Build + +[source,bash] +---- +npm install +npm run compile +---- + +==== Watch Mode + +[source,bash] +---- +npm run watch +---- + +==== Package + +[source,bash] +---- +npm install -g vsce +vsce package +---- + +=== License + +MPL-2.0 + +=== Links + +* https://github.com/hyperpolymath/phronesis[Phronesis Repository] +* link:../../docs/draft-phronesis-policy-language.txt[Language +Specification] +* https://microsoft.github.io/language-server-protocol/[LSP +Specification] diff --git a/editors/vscode/README.md b/editors/vscode/README.md deleted file mode 100644 index 2bc69ea..0000000 --- a/editors/vscode/README.md +++ /dev/null @@ -1,145 +0,0 @@ - -# Phronesis VSCode Extension - -VSCode extension for Phronesis policy language with LSP support. - -## Features - -- **Syntax Highlighting** - Full language support -- **Auto-Completion** - Keywords, stdlib functions, variables -- **Hover Documentation** - Inline docs for functions and keywords -- **Go to Definition** - Jump to policy/constant definitions -- **Real-time Diagnostics** - Syntax errors and warnings -- **Code Formatting** - Auto-format on save - -## Installation - -### From Source - -1. **Build the extension:** - ```bash - cd editors/vscode - npm install - npm run compile - ``` - -2. **Install phronesis CLI:** - ```bash - mix escript.build - # Add to PATH or configure extension - ``` - -3. **Install extension:** - ```bash - code --install-extension phronesis-0.2.0.vsix - ``` - - Or copy to extensions directory: - ```bash - cp -r . ~/.vscode/extensions/phronesis-0.2.0/ - ``` - -### Configuration - -Open VSCode settings and configure: - -```json -{ - "phronesis.serverPath": "/path/to/phronesis", - "phronesis.trace.server": "off" -} -``` - -## Usage - -1. Open a `.phr` file -2. LSP server starts automatically -3. Auto-completion: Type `Std.` to see stdlib modules -4. Hover over keywords/functions for documentation -5. F12 / Cmd+Click for go-to-definition - -## Features in Detail - -### Auto-Completion - -- **Keywords**: `POLICY`, `CONST`, `IMPORT`, `ACCEPT`, `REJECT`, etc. -- **Standard Library**: `Std.RPKI.*`, `Std.BGP.*`, `Std.Consensus.*`, `Std.Temporal.*` -- **Functions**: All stdlib functions with signatures - -Example: -```phronesis -Std.R # Auto-complete shows: Std.RPKI -Std.RPKI. # Shows: validate, check_origin, validation_status -``` - -### Hover Documentation - -Hover over any keyword or function to see: -- Syntax -- Parameters -- Return type -- Examples - -### Diagnostics - -Real-time error checking: -- Syntax errors (lexer/parser) -- Linter warnings -- Type issues - -### Formatting - -Format document: `Shift+Alt+F` or save with format-on-save enabled. - -## Troubleshooting - -### LSP server not starting - -1. Check phronesis is installed: - ```bash - which phronesis - phronesis --version - ``` - -2. Check server path in settings -3. View LSP logs: `Output` → `Phronesis Language Server` - -### No auto-completion - -1. Ensure `.phr` file is recognized as Phronesis language -2. Restart LSP: `Cmd+Shift+P` → "Restart Language Server" - -## Development - -### Build - -```bash -npm install -npm run compile -``` - -### Watch Mode - -```bash -npm run watch -``` - -### Package - -```bash -npm install -g vsce -vsce package -``` - -## License - -MPL-2.0 - -## Links - -- [Phronesis Repository](https://github.com/hyperpolymath/phronesis) -- [Language Specification](../../docs/draft-phronesis-policy-language.txt) -- [LSP Specification](https://microsoft.github.io/language-server-protocol/) diff --git a/test_e2e.exs b/examples/test_e2e.exs similarity index 100% rename from test_e2e.exs rename to examples/test_e2e.exs diff --git a/test_framework_demo.exs b/examples/test_framework_demo.exs similarity index 100% rename from test_framework_demo.exs rename to examples/test_framework_demo.exs diff --git a/test_stdlib.exs b/examples/test_stdlib.exs similarity index 100% rename from test_stdlib.exs rename to examples/test_stdlib.exs diff --git a/phronesis b/phronesis deleted file mode 100755 index 9a8a316..0000000 Binary files a/phronesis and /dev/null differ diff --git a/spec/system-specs.adoc b/spec/system-specs.adoc new file mode 100644 index 0000000..750faa3 --- /dev/null +++ b/spec/system-specs.adoc @@ -0,0 +1,100 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell + +[[phronesis--system-specifications]] +== Phronesis — System Specifications + +Phronesis is a language that compiles to and runs on the Elixir/BEAM +platform, inheriting the runtime characteristics of the Erlang virtual +machine. + +=== Memory Model + +Phronesis uses the BEAM virtual machine's memory model: + +* *Process heaps*: Each BEAM process has its own private heap. No shared +mutable state exists between processes, eliminating data races at the +memory level. +* *Immutable data*: All values are immutable once created. "Mutation" +produces new values; the old value remains unchanged until garbage +collected. +* *Per-process GC*: Garbage collection is per-process and generational. +A GC pause in one process does not affect any other process. Short-lived +processes that terminate before triggering GC have their entire heap +reclaimed at once. +* *Binary heap*: Large binaries (>64 bytes) are reference-counted on a +shared binary heap. Small binaries are copied into process heaps. +* *ETS tables*: Erlang Term Storage provides mutable shared-memory +tables outside the process model. Data is copied in and out, preserving +isolation semantics. +* *No manual memory management*: Developers never allocate or free +memory directly. +* *Atoms*: Atoms are interned strings stored in a global atom table. +They are never garbage collected. The atom table has a default limit of +1,048,576 entries. + +=== Concurrency Model + +Phronesis inherits the BEAM actor model: + +* *Processes*: Lightweight BEAM processes (not OS threads). Millions can +run concurrently with ~2KB initial heap each. +* *Message passing*: Processes communicate exclusively via asynchronous +message passing. Each process has a mailbox; messages are +pattern-matched with `receive`. +* *OTP supervisors*: Fault tolerance through supervision trees. +Supervisors monitor child processes and restart them according to +configurable strategies (one-for-one, one-for-all, rest-for-one). +* *Preemptive scheduling*: The BEAM scheduler preempts processes after a +reduction count, ensuring fair scheduling without cooperative yielding. +* *Distribution*: Processes can send messages transparently across nodes +in a cluster. Location transparency is a first-class property. +* *No shared state*: Concurrency bugs related to locks, mutexes, and +shared memory are structurally impossible in the standard process model. +* *Links and monitors*: Processes can be linked (bidirectional failure +propagation) or monitored (unidirectional notification on exit). These +primitives underpin OTP supervisor behaviour. +* *Task module*: For structured concurrency, the `Task` module provides +`async`/`await` semantics built on top of processes, with automatic +linking to the caller. + +=== Effect System + +Phronesis uses a pure functional approach to effects: + +* *Pure by default*: Functions are pure unless they explicitly perform +IO or send messages. The type system tracks purity at the function +level. +* *Explicit IO*: Side effects (file IO, network, database) are performed +through dedicated modules that make the effectful nature visible in the +API. +* *Process effects*: Spawning processes, sending messages, and receiving +messages are the primary effect channels. These are explicit in the +function signatures. +* *With-blocks*: Resource acquisition and release follow the `with` +pattern, ensuring cleanup even when processes crash. +* *Telemetry integration*: Observable effects (metrics, traces) use the +standard BEAM telemetry library for instrumentation without coupling. + +=== Module System + +Phronesis uses the Elixir module system: + +* *Modules*: Defined with `defmodule`. Each module is a namespace +containing functions, macros, structs, and type specifications. +* *`use`*: Injects code from another module via the `__using__/1` macro +callback. Commonly used for behaviours and DSLs. +* *`import`*: Brings functions from another module into the current +scope, allowing them to be called without the module prefix. +* *`alias`*: Creates a short name for a module (e.g., +`alias MyApp.Accounts.User` allows referring to `User` directly). +* *`require`*: Ensures a module is compiled before the current one, +necessary when using macros from that module. +* *Behaviours*: Define callback contracts that implementing modules must +fulfil. Compile-time warnings for missing callbacks. +* *Protocols*: Ad-hoc polymorphism. Protocols define a set of functions +that can be implemented for any data type without modifying the type +itself. +* *Package manager*: Mix for build tooling and task running; Hex for +package registry and dependency resolution. Dependencies declared in +`mix.exs`. diff --git a/spec/system-specs.md b/spec/system-specs.md deleted file mode 100644 index 4def235..0000000 --- a/spec/system-specs.md +++ /dev/null @@ -1,90 +0,0 @@ - -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# Phronesis — System Specifications - -Phronesis is a language that compiles to and runs on the Elixir/BEAM platform, -inheriting the runtime characteristics of the Erlang virtual machine. - -## Memory Model - -Phronesis uses the BEAM virtual machine's memory model: - -- **Process heaps**: Each BEAM process has its own private heap. No shared mutable - state exists between processes, eliminating data races at the memory level. -- **Immutable data**: All values are immutable once created. "Mutation" produces new - values; the old value remains unchanged until garbage collected. -- **Per-process GC**: Garbage collection is per-process and generational. A GC pause - in one process does not affect any other process. Short-lived processes that - terminate before triggering GC have their entire heap reclaimed at once. -- **Binary heap**: Large binaries (>64 bytes) are reference-counted on a shared - binary heap. Small binaries are copied into process heaps. -- **ETS tables**: Erlang Term Storage provides mutable shared-memory tables outside - the process model. Data is copied in and out, preserving isolation semantics. -- **No manual memory management**: Developers never allocate or free memory directly. -- **Atoms**: Atoms are interned strings stored in a global atom table. They are never - garbage collected. The atom table has a default limit of 1,048,576 entries. - -## Concurrency Model - -Phronesis inherits the BEAM actor model: - -- **Processes**: Lightweight BEAM processes (not OS threads). Millions can run - concurrently with ~2KB initial heap each. -- **Message passing**: Processes communicate exclusively via asynchronous message - passing. Each process has a mailbox; messages are pattern-matched with `receive`. -- **OTP supervisors**: Fault tolerance through supervision trees. Supervisors monitor - child processes and restart them according to configurable strategies (one-for-one, - one-for-all, rest-for-one). -- **Preemptive scheduling**: The BEAM scheduler preempts processes after a reduction - count, ensuring fair scheduling without cooperative yielding. -- **Distribution**: Processes can send messages transparently across nodes in a - cluster. Location transparency is a first-class property. -- **No shared state**: Concurrency bugs related to locks, mutexes, and shared memory - are structurally impossible in the standard process model. -- **Links and monitors**: Processes can be linked (bidirectional failure propagation) - or monitored (unidirectional notification on exit). These primitives underpin OTP - supervisor behaviour. -- **Task module**: For structured concurrency, the `Task` module provides - `async`/`await` semantics built on top of processes, with automatic linking to - the caller. - -## Effect System - -Phronesis uses a pure functional approach to effects: - -- **Pure by default**: Functions are pure unless they explicitly perform IO or send - messages. The type system tracks purity at the function level. -- **Explicit IO**: Side effects (file IO, network, database) are performed through - dedicated modules that make the effectful nature visible in the API. -- **Process effects**: Spawning processes, sending messages, and receiving messages - are the primary effect channels. These are explicit in the function signatures. -- **With-blocks**: Resource acquisition and release follow the `with` pattern, - ensuring cleanup even when processes crash. -- **Telemetry integration**: Observable effects (metrics, traces) use the standard - BEAM telemetry library for instrumentation without coupling. - -## Module System - -Phronesis uses the Elixir module system: - -- **Modules**: Defined with `defmodule`. Each module is a namespace containing - functions, macros, structs, and type specifications. -- **`use`**: Injects code from another module via the `__using__/1` macro callback. - Commonly used for behaviours and DSLs. -- **`import`**: Brings functions from another module into the current scope, - allowing them to be called without the module prefix. -- **`alias`**: Creates a short name for a module (e.g., `alias MyApp.Accounts.User` - allows referring to `User` directly). -- **`require`**: Ensures a module is compiled before the current one, necessary - when using macros from that module. -- **Behaviours**: Define callback contracts that implementing modules must fulfil. - Compile-time warnings for missing callbacks. -- **Protocols**: Ad-hoc polymorphism. Protocols define a set of functions that can - be implemented for any data type without modifying the type itself. -- **Package manager**: Mix for build tooling and task running; Hex for package - registry and dependency resolution. Dependencies declared in `mix.exs`. diff --git a/syntax/README.adoc b/syntax/README.adoc new file mode 100644 index 0000000..7093211 --- /dev/null +++ b/syntax/README.adoc @@ -0,0 +1,213 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell +== Phronesis Syntax Highlighting + +This directory contains syntax highlighting definitions for various +editors. + +=== Installation + +[[vscode--vscodium]] +==== VSCode / VSCodium + +[arabic] +. Create extension directory: ++ +[source,bash] +---- +mkdir -p ~/.vscode/extensions/phronesis-lang +---- +. Copy files: ++ +[source,bash] +---- +cp phronesis.tmLanguage.json ~/.vscode/extensions/phronesis-lang/ +---- +. Create `package.json`: ++ +[source,json] +---- +{ + "name": "phronesis", + "displayName": "Phronesis Policy Language", + "description": "Syntax highlighting for Phronesis (.phr files)", + "version": "0.2.0", + "engines": { "vscode": "^1.60.0" }, + "categories": ["Programming Languages"], + "contributes": { + "languages": [{ + "id": "phronesis", + "aliases": ["Phronesis", "phronesis"], + "extensions": [".phr"], + "configuration": "./language-configuration.json" + }], + "grammars": [{ + "language": "phronesis", + "scopeName": "source.phronesis", + "path": "./phronesis.tmLanguage.json" + }] + } +} +---- +. Reload VSCode + +[[vim--neovim]] +==== Vim / Neovim + +[arabic] +. Copy to syntax directory: ++ +[source,bash] +---- +mkdir -p ~/.vim/syntax +cp phronesis.vim ~/.vim/syntax/ +---- +. Add to `~/.vim/ftdetect/phronesis.vim`: ++ +[source,vim] +---- +autocmd BufNewFile,BufRead *.phr set filetype=phronesis +---- +. (Optional) Add to `~/.vim/ftplugin/phronesis.vim`: ++ +[source,vim] +---- +setlocal commentstring=#\ %s +setlocal tabstop=2 +setlocal shiftwidth=2 +setlocal expandtab +---- + +==== Emacs + +[arabic] +. Copy to Emacs config: ++ +[source,bash] +---- +cp phronesis-mode.el ~/.emacs.d/lisp/ +---- +. Add to `~/.emacs` or `~/.emacs.d/init.el`: ++ +[source,elisp] +---- +(add-to-list 'load-path "~/.emacs.d/lisp") +(require 'phronesis-mode) +---- +. Reload Emacs or evaluate: `M-x eval-buffer` + +==== Sublime Text + +TextMate grammars (`.tmLanguage.json`) work in Sublime Text: + +[arabic] +. Open Sublime Text +. `Preferences` → `Browse Packages` +. Create directory: `Phronesis/` +. Copy `phronesis.tmLanguage.json` to +`Phronesis/Phronesis.tmLanguage.json` +. Restart Sublime Text + +[[kate--kwrite]] +==== Kate / KWrite + +TODO: Create `phronesis.xml` syntax file for KDE editors. + +[[github--gitlab]] +==== GitHub / GitLab + +For syntax highlighting on GitHub: + +[arabic] +. Submit `linguist.yml` definition to +https://github.com/github/linguist[github/linguist] +. Or add `.gitattributes` to your repo: ++ +.... +*.phr linguist-language=Phronesis +.... + +=== Features + +All syntax definitions support: + +* *Keywords*: `POLICY`, `CONST`, `IMPORT`, `IF`, `THEN`, `ELSE`, `AND`, +`OR`, `NOT`, `IN` +* *Actions*: `ACCEPT`, `REJECT`, `REPORT`, `EXECUTE`, `BLOCK` +* *Metadata*: `PRIORITY`, `EXPIRES`, `CREATED_BY` +* *Test keywords*: `TEST`, `SCENARIO`, `GIVEN`, `EXPECT` +* *Types*: `Integer`, `String`, `Boolean`, `Float`, `List`, `Map`, +`Route` +* *Constants*: `true`, `false`, `nil`, `null`, `never`, `always` +* *Standard library*: `Std.RPKI.*`, `Std.BGP.*`, `Std.Consensus.*`, +`Std.Temporal.*` +* *Comments*: `# line comments`, `## block comments ##` +* *Strings*: `"double quoted"`, `'single quoted'`, `"${interpolation}"` +* *Numbers*: Integers, floats, hex (`0xFF`) +* *Operators*: `==`, `!=`, `>=`, `<=`, `>`, `<`, `+`, `-`, `*`, `/`, +`%`, `&&`, `||`, `!`, `.`, `?.` + +=== Editor-Specific Features + +==== VSCode + +* Bracket matching +* Auto-indentation +* Code folding + +==== Vim + +* Syntax highlighting +* `commentstring` for comment toggling +* Indentation settings + +==== Emacs + +* Major mode with keybindings: +** `C-c C-c` - Run file +** `C-c C-k` - Check syntax +** `C-c C-p` - Parse and show AST +** `C-c C-r` - Start REPL +* Auto-indentation +* Comment support + +=== Example + +[source,phronesis] +---- +# BGP Security Policy +IMPORT Std.RPKI +IMPORT Std.BGP + +CONST my_asn = 64512 + +POLICY rpki_validation: + Std.RPKI.validate(route) == :invalid + THEN REJECT("RPKI validation failed") + PRIORITY: 200 + EXPIRES: never + CREATED_BY: security_team + +POLICY as_path_loop: + my_asn IN Std.BGP.extract_as_path(route) + THEN REJECT("AS path loop detected") + PRIORITY: 300 +---- + +=== Contributing + +To add support for a new editor: + +[arabic] +. Create syntax definition file +. Test with sample `.phr` files +. Document installation in this README +. Submit PR + +=== License + +MPL-2.0 + +=== Maintainer + +Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk diff --git a/syntax/README.md b/syntax/README.md deleted file mode 100644 index 5d26f2b..0000000 --- a/syntax/README.md +++ /dev/null @@ -1,183 +0,0 @@ - -# Phronesis Syntax Highlighting - -This directory contains syntax highlighting definitions for various editors. - -## Installation - -### VSCode / VSCodium - -1. Create extension directory: - ```bash - mkdir -p ~/.vscode/extensions/phronesis-lang - ``` - -2. Copy files: - ```bash - cp phronesis.tmLanguage.json ~/.vscode/extensions/phronesis-lang/ - ``` - -3. Create `package.json`: - ```json - { - "name": "phronesis", - "displayName": "Phronesis Policy Language", - "description": "Syntax highlighting for Phronesis (.phr files)", - "version": "0.2.0", - "engines": { "vscode": "^1.60.0" }, - "categories": ["Programming Languages"], - "contributes": { - "languages": [{ - "id": "phronesis", - "aliases": ["Phronesis", "phronesis"], - "extensions": [".phr"], - "configuration": "./language-configuration.json" - }], - "grammars": [{ - "language": "phronesis", - "scopeName": "source.phronesis", - "path": "./phronesis.tmLanguage.json" - }] - } - } - ``` - -4. Reload VSCode - -### Vim / Neovim - -1. Copy to syntax directory: - ```bash - mkdir -p ~/.vim/syntax - cp phronesis.vim ~/.vim/syntax/ - ``` - -2. Add to `~/.vim/ftdetect/phronesis.vim`: - ```vim - autocmd BufNewFile,BufRead *.phr set filetype=phronesis - ``` - -3. (Optional) Add to `~/.vim/ftplugin/phronesis.vim`: - ```vim - setlocal commentstring=#\ %s - setlocal tabstop=2 - setlocal shiftwidth=2 - setlocal expandtab - ``` - -### Emacs - -1. Copy to Emacs config: - ```bash - cp phronesis-mode.el ~/.emacs.d/lisp/ - ``` - -2. Add to `~/.emacs` or `~/.emacs.d/init.el`: - ```elisp - (add-to-list 'load-path "~/.emacs.d/lisp") - (require 'phronesis-mode) - ``` - -3. Reload Emacs or evaluate: `M-x eval-buffer` - -### Sublime Text - -TextMate grammars (`.tmLanguage.json`) work in Sublime Text: - -1. Open Sublime Text -2. `Preferences` → `Browse Packages` -3. Create directory: `Phronesis/` -4. Copy `phronesis.tmLanguage.json` to `Phronesis/Phronesis.tmLanguage.json` -5. Restart Sublime Text - -### Kate / KWrite - -TODO: Create `phronesis.xml` syntax file for KDE editors. - -### GitHub / GitLab - -For syntax highlighting on GitHub: -1. Submit `linguist.yml` definition to [github/linguist](https://github.com/github/linguist) -2. Or add `.gitattributes` to your repo: - ``` - *.phr linguist-language=Phronesis - ``` - -## Features - -All syntax definitions support: - -- **Keywords**: `POLICY`, `CONST`, `IMPORT`, `IF`, `THEN`, `ELSE`, `AND`, `OR`, `NOT`, `IN` -- **Actions**: `ACCEPT`, `REJECT`, `REPORT`, `EXECUTE`, `BLOCK` -- **Metadata**: `PRIORITY`, `EXPIRES`, `CREATED_BY` -- **Test keywords**: `TEST`, `SCENARIO`, `GIVEN`, `EXPECT` -- **Types**: `Integer`, `String`, `Boolean`, `Float`, `List`, `Map`, `Route` -- **Constants**: `true`, `false`, `nil`, `null`, `never`, `always` -- **Standard library**: `Std.RPKI.*`, `Std.BGP.*`, `Std.Consensus.*`, `Std.Temporal.*` -- **Comments**: `# line comments`, `## block comments ##` -- **Strings**: `"double quoted"`, `'single quoted'`, `"${interpolation}"` -- **Numbers**: Integers, floats, hex (`0xFF`) -- **Operators**: `==`, `!=`, `>=`, `<=`, `>`, `<`, `+`, `-`, `*`, `/`, `%`, `&&`, `||`, `!`, `.`, `?.` - -## Editor-Specific Features - -### VSCode -- Bracket matching -- Auto-indentation -- Code folding - -### Vim -- Syntax highlighting -- `commentstring` for comment toggling -- Indentation settings - -### Emacs -- Major mode with keybindings: - - `C-c C-c` - Run file - - `C-c C-k` - Check syntax - - `C-c C-p` - Parse and show AST - - `C-c C-r` - Start REPL -- Auto-indentation -- Comment support - -## Example - -```phronesis -# BGP Security Policy -IMPORT Std.RPKI -IMPORT Std.BGP - -CONST my_asn = 64512 - -POLICY rpki_validation: - Std.RPKI.validate(route) == :invalid - THEN REJECT("RPKI validation failed") - PRIORITY: 200 - EXPIRES: never - CREATED_BY: security_team - -POLICY as_path_loop: - my_asn IN Std.BGP.extract_as_path(route) - THEN REJECT("AS path loop detected") - PRIORITY: 300 -``` - -## Contributing - -To add support for a new editor: - -1. Create syntax definition file -2. Test with sample `.phr` files -3. Document installation in this README -4. Submit PR - -## License - -MPL-2.0 - -## Maintainer - -Jonathan D.A. Jewell diff --git a/wiki/CLI-Reference.adoc b/wiki/CLI-Reference.adoc index c2e80c2..3665ca6 100644 --- a/wiki/CLI-Reference.adoc +++ b/wiki/CLI-Reference.adoc @@ -218,7 +218,7 @@ phronesis repl --load policy.phr *REPL Session:* .... -Phronesis v0.1.0 REPL +Phronesis v0.9.0 REPL Type :help for commands, :quit to exit phr> 1 + 2 diff --git a/wiki/Contributing.adoc b/wiki/Contributing.adoc index 16e08c4..a13d500 100644 --- a/wiki/Contributing.adoc +++ b/wiki/Contributing.adoc @@ -393,7 +393,7 @@ What needs to be resolved? Contributors are recognized in: -* link:../CONTRIBUTORS.adoc[CONTRIBUTORS.md] +* link:../MAINTAINERS.adoc[MAINTAINERS.adoc] * Release notes * Project website @@ -401,4 +401,4 @@ Contributors are recognized in: === License -By contributing, you agree that your contributions will be licensed under the link:../LICENSE[AGPL-3.0] license. +By contributing, you agree that your contributions will be licensed under the project's licences: link:../LICENSE[MPL-2.0] for code and CC-BY-SA-4.0 for documentation. diff --git a/wiki/Formal-Semantics.adoc b/wiki/Formal-Semantics.adoc index bf7e0e8..44866a5 100644 --- a/wiki/Formal-Semantics.adoc +++ b/wiki/Formal-Semantics.adoc @@ -415,4 +415,4 @@ state ∈ {Follower, Candidate, Leader} * link:Reference-Grammar.adoc[Reference-Grammar] - Formal grammar * link:Architecture-Interpreter.adoc[Architecture-Interpreter] - Implementation * link:Testing.adoc[Testing] - Verification via testing -* link:../docs/safety_proofs.adoc[docs/safety_proofs.md] - Safety proofs document +* link:../docs/safety_proofs.adoc[docs/safety_proofs.adoc] - Safety proofs document diff --git a/wiki/Installation.adoc b/wiki/Installation.adoc index 8ec8b05..0c5c66a 100644 --- a/wiki/Installation.adoc +++ b/wiki/Installation.adoc @@ -53,7 +53,7 @@ Verify installation: [source,bash] ---- phronesis --version -# Phronesis 0.1.0 +# Phronesis 0.9.0 ---- ==== Method 2: From Source diff --git a/wiki/Quick-Start.adoc b/wiki/Quick-Start.adoc index bb4a7de..75924ab 100644 --- a/wiki/Quick-Start.adoc +++ b/wiki/Quick-Start.adoc @@ -14,7 +14,7 @@ Ensure Phronesis is installed: [source,bash] ---- phronesis --version -# Phronesis 0.1.0 +# Phronesis 0.9.0 ---- If not, see link:Installation.adoc[Installation]. @@ -131,7 +131,7 @@ phronesis repl ---- .... -Phronesis v0.1.0 REPL +Phronesis v0.9.0 REPL Type :help for commands, :quit to exit phr> 1 + 2 * 3