Skip to content

Commit 8cd7428

Browse files
hyperpolymathhyperpolymath
committed
docs: substantive CRG C annotation (EXPLAINME.adoc)
1 parent fa0b2d5 commit 8cd7428

1 file changed

Lines changed: 163 additions & 0 deletions

File tree

‎EXPLAINME.adoc‎

Lines changed: 163 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Phronesis — Show Me The Receipts
3+
:toc:
4+
:icons: font
5+
6+
The README makes claims. This file backs them up.
7+
8+
== A Provably Safe Language for Agentic Ethical Reasoning
9+
10+
[quote, README]
11+
____
12+
Phronesis is a neuro-symbolic, agentic language designed to formalize ethical
13+
reasoning in autonomous systems. It fuses the precision of Symbolic AI with the
14+
adaptability of neural networks, enforcing provable safety and fault tolerance
15+
through a dedicated BEAM VM runtime.
16+
____
17+
18+
Phronesis is a compiled policy language, not a library. The pipeline is:
19+
source text → `Phronesis.Lexer` → `Phronesis.Parser` → AST → `Phronesis.Compiler`
20+
→ bytecode (`.phrc` files) → `Phronesis.Interpreter`. The Elixir implementation
21+
lives in `lib/phronesis/`. The language has 15 keywords including `ACCEPT`,
22+
`REJECT`, `REPORT`, and `EXECUTE`, plus probabilistic type literals
23+
(`BeliefFunction`, `ProbabilityDistribution`) and a mandatory `REPORT` action
24+
for flagging model-reality inconsistencies (the "map-territory mandate"). Running
25+
on the BEAM gives fault tolerance via OTP supervisor trees.
26+
https://erlang.org/doc/design_principles/des_princ.html[OTP Design Principles]
27+
28+
**Caveat:** The production Rust/BEAM compiler is Phase 2 roadmap. The current
29+
implementation is the Elixir prototype. Probabilistic types are represented as
30+
runtime values, not statically checked by the type checker at this stage.
31+
Consensus (Raft) is a TLA+ spec in `formal/` and a skeleton in
32+
`lib/phronesis/consensus/`; it is not yet a deployable runtime.
33+
34+
- Lexer: `lib/phronesis/lexer.ex`
35+
- Parser: `lib/phronesis/parser.ex`, `lib/phronesis/parser/`
36+
- Type checker: `lib/phronesis/type_checker.ex`
37+
- Compiler: `lib/phronesis/compiler.ex`
38+
- Interpreter: `lib/phronesis/interpreter.ex`
39+
- Learn more: https://en.wikipedia.org/wiki/Phronesis
40+
41+
== Formal Verification: TLA+ Consensus Spec
42+
43+
[quote, README]
44+
____
45+
BEAM/Raft Architecture: BEAM VM + Raft consensus for ethical loop execution.
46+
Ensures fault-tolerant, distributed reasoning.
47+
____
48+
49+
`formal/PhronesisConsensus.tla` is a TLA+ specification of the Raft-based
50+
consensus protocol for multi-node Phronesis execution. `formal/PhronesisConsensus.cfg`
51+
is the TLC model checker configuration. These are model-checked artefacts, not
52+
executable code, but they are the authoritative spec from which the
53+
`lib/phronesis/consensus/` Elixir implementation derives.
54+
https://lamport.azurewebsites.net/tla/tla.html[TLA+]
55+
56+
**Caveat:** The Elixir consensus implementation in `lib/phronesis/consensus/`
57+
is a scaffold. The TLA+ spec has not been formally published or independently
58+
reviewed.
59+
60+
- Spec: `formal/PhronesisConsensus.tla`
61+
- Config: `formal/PhronesisConsensus.cfg`
62+
- Implementation: `lib/phronesis/consensus/`
63+
- Test: `test/consensus_test.exs`
64+
65+
== Incremental Lexer and Parser
66+
67+
[quote, README]
68+
____
69+
Strong Static Typing: Prevents runtime errors in safety-critical systems.
70+
____
71+
72+
`lib/phronesis/incremental_lexer.ex` and `lib/phronesis/incremental_parser.ex`
73+
support re-parsing only the changed portion of a document — the critical path
74+
for the LSP integration. The incremental infrastructure feeds `lib/phronesis/lsp/`
75+
which provides hover, completion, and diagnostics to editors. Incremental
76+
correctness is verified in `test/incremental_lexer_test.exs` and
77+
`test/incremental_parser_test.exs`.
78+
79+
**Caveat:** Incremental reparsing is bounded by expression boundaries. Edits
80+
spanning multiple top-level policy blocks still trigger a full re-parse.
81+
82+
- Implementation: `lib/phronesis/incremental_lexer.ex`, `lib/phronesis/incremental_parser.ex`
83+
- LSP: `lib/phronesis/lsp/`
84+
- Tests: `test/incremental_lexer_test.exs`, `test/incremental_parser_test.exs`, `test/lsp_integration_test.exs`
85+
86+
== Standard Library and Package Manager
87+
88+
[quote, README]
89+
____
90+
Running all ethical scenarios is the definitive measure of correctness.
91+
____
92+
93+
`lib/phronesis/stdlib/` provides the built-in policy predicates and ethical
94+
reasoning primitives. `lib/phronesis/library/` contains reusable policy modules.
95+
`lib/phronesis/package_manager.ex` and `lib/phronesis/package_manager/` implement
96+
a Phronesis-native package system for distributing policy modules. The conformance
97+
test suite in `test/conformance_test.exs` and `conformance/` exercises the
98+
mandatory ethical scenario set.
99+
100+
**Caveat:** The package registry is local-only. There is no hosted registry or
101+
cryptographic signing for packages yet.
102+
103+
- Standard library: `lib/phronesis/stdlib/`
104+
- Package manager: `lib/phronesis/package_manager.ex`, `lib/phronesis/package_manager/`
105+
- Conformance suite: `conformance/`, `test/conformance_test.exs`
106+
107+
== Dogfooded Across The Account
108+
109+
[cols="1,2"]
110+
|===
111+
| Technology | Also Used In
112+
113+
| **Elixir / BEAM** | https://github.com/hyperpolymath/http-capability-gateway, https://github.com/hyperpolymath/burble
114+
| **TLA+ formal spec** | https://github.com/hyperpolymath/ephapax (Raft consensus for linear type proofs)
115+
| **LSP integration** | https://github.com/hyperpolymath/universal-language-server-plugin
116+
| **Incremental parsing** | https://github.com/hyperpolymath/tree-sitter-k9 (grammar-level incremental parse)
117+
| **Containerfile (Podman)** | https://github.com/hyperpolymath/session-sentinel, https://github.com/hyperpolymath/stapeln
118+
|===
119+
120+
== File Map
121+
122+
[cols="1,2"]
123+
|===
124+
| Path | Proves
125+
126+
| `lib/phronesis/lexer.ex` | Tokenises Phronesis source: 15 keywords, IPv4/6 literals, DateTimes, probabilistic type tokens
127+
| `lib/phronesis/parser.ex`, `lib/phronesis/parser/` | Recursive-descent parser producing typed AST nodes
128+
| `lib/phronesis/type_checker.ex` | Static type checker (probabilistic types, scope resolution)
129+
| `lib/phronesis/compiler.ex` | AST → `.phrc` bytecode with constant folding and dead-code elimination
130+
| `lib/phronesis/interpreter.ex` | Tree-walking interpreter for prototyping and REPL use
131+
| `lib/phronesis/tracing_interpreter.ex` | Interpreter with execution trace hooks for debugger/profiler
132+
| `lib/phronesis/incremental_lexer.ex` | Incremental re-lexing for LSP edit support
133+
| `lib/phronesis/incremental_parser.ex` | Incremental re-parsing bounded by expression boundaries
134+
| `lib/phronesis/lsp/` | Language Server Protocol implementation (hover, completion, diagnostics)
135+
| `lib/phronesis/stdlib/` | Built-in policy predicates and ethical reasoning primitives
136+
| `lib/phronesis/library/` | Reusable distributable policy modules
137+
| `lib/phronesis/package_manager.ex` | Package manager entry point
138+
| `lib/phronesis/package_manager/` | Package resolution, fetching, caching
139+
| `lib/phronesis/diagnostics.ex`, `diagnostics/` | Error reporting with source spans
140+
| `lib/phronesis/debugger.ex`, `debugger/` | Interactive debugger and trace viewer
141+
| `lib/phronesis/profiler.ex` | Execution profiler
142+
| `lib/phronesis/hot_reload.ex` | Live policy reload without process restart
143+
| `lib/phronesis/consensus/` | Elixir Raft consensus scaffold
144+
| `formal/PhronesisConsensus.tla` | TLA+ Raft consensus specification (model-checked)
145+
| `formal/PhronesisConsensus.cfg` | TLC model checker configuration
146+
| `conformance/` | Ethical scenario conformance test fixtures
147+
| `test/lexer_test.exs` | Lexer unit tests
148+
| `test/parser_test.exs` | Parser unit tests
149+
| `test/type_checker_test.exs` | (via phronesis_test.exs) Type checker coverage
150+
| `test/compiler_test.exs` | Compiler bytecode tests
151+
| `test/interpreter_test.exs` | Interpreter execution tests
152+
| `test/conformance_test.exs` | Mandatory ethical scenario suite
153+
| `test/lsp_integration_test.exs` | LSP integration tests
154+
| `test/e2e_test.exs`, `test_e2e.exs` | End-to-end pipeline tests
155+
| `src/` | Supplementary source assets (non-Elixir)
156+
| `spec/` | Language specification documents
157+
| `syntax/` | Syntax highlighting definitions
158+
| `editors/` | Editor plugin scaffolds
159+
| `Containerfile` | Podman container definition (Chainguard base)
160+
| `.machine_readable/` | A2ML state, meta, ecosystem files
161+
| `TESTING-REPORT.adoc` | Test results narrative
162+
| `LSP-IMPLEMENTATION-SUMMARY.md` | LSP feature coverage summary
163+
|===

0 commit comments

Comments
 (0)