1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
//! AXON compiler frontend.
//!
//! Pure frontend of the AXON language: lexer, parser, AST, epistemic
//! type primitives, type checker, IR generator, and the top-level
//! compile-time checker that glues them together.
//!
//! # Design contract
//!
//! This crate has **zero runtime dependencies**. The only allowed
//! external dep is `serde` (plus its proc-macro chain). Any addition
//! of a runtime dep (tokio, axum, sqlx, reqwest, aws-*, jsonwebtoken,
//! …) is rejected at CI time.
//!
//! # Consumers
//!
//! - `axon` crate (the AXON runtime in `../axon-rs/`) re-exports these
//! modules so existing callers keep working.
//! - `axon-lsp` (Language Server, separate repo) consumes the frontend
//! directly without dragging runtime deps.
//!
//! # Byte-identical parity
//!
//! Outputs must match the Python reference implementation
//! (`../axon/`) on the golden-file test corpus. Divergences are
//! release blockers.
/// v4.0.0 — the closed regulatory vocabulary Κ, in the crate that
/// type-checks it. The rich per-class metadata stays in
/// `axon-rs::esk::compliance`, which now derives its membership from here.
/// v2.87.0 — the closed catalog of declared `effect`s + the design decision's bare-name
/// resolution. ONE derivation, shared by the IR generator and the type-checker,
/// so the two can never disagree about which effect owns an operation.
/// v2.87.0 — the static effect discipline: D9 exhaustiveness (interprocedural,
/// over the flow call graph), the design decision's resolution diagnostics, D10's structural
/// one-shot law, and the clause-scope law for `resume`/`abort`/`forward`.
/// v2.65.0 — the symbolic differentiator + simplifier over the
/// closed `Expr` (the proof-carrying derivative).
// v1.4.0 — compile-time catalogs used by the type checker.
// `refinement` declares the closed Trust<T> catalog; `stream_effect`
// declares the closed backpressure policy catalog. Both are pure
// enum-like definitions with `std::fmt` only — no runtime deps.
// The matching runtime implementations (`trust_verifiers`,
// `stream_runtime`) live in the `axon` runtime crate.
/// v2.83.0 — the `mandate` stability judgment (`D < |Kp+Ki+Kd| < 1/L`),
/// shared verbatim with the runtime controller in axon-rs.
/// v2.83.0 — the `fabric` substrate judgment (provider ↔ region ↔
/// jurisdiction), shared verbatim with the runtime.
// v1.4.0 — closed catalogue of regulatory authorisations
// (GDPR/CCPA/SOX/HIPAA/GLBA/PCI-DSS) used by the type checker to
// enforce `@legal_basis` annotations. Pure catalog, no runtime deps.
// v1.4.0 — OTS (Ontological Tool Synthesis) compile-time slug
// catalogs. Runtime pipeline execution lives in `axon::ots` and
// re-exports these for backward compatibility.
// v1.6.0 — LSP-facing analysis primitives for typed channels.
// Pure AST helpers consumed by `axon-lsp` (sibling repo) to implement
// hover, completion, go-to-definition and find-references. Zero
// runtime deps — stays inside the v1.4.2 contract.
// v2.3.0 — session types: the pure algebra of typed bidirectional
// dialogue (WebSocket as a cognitive primitive). The session-type
// grammar + the duality involution `(·)⊥` + regular-coinductive
// equality for `μ`-types + the connection law (`peer ≡ self⊥`).
// Grounded in Caires–Pfenning (session types = intuitionistic linear
// propositions). Pure — no runtime deps; the `socket` surface (41.b),
// credit-refined backpressure (41.c) and the typed-WS runtime (41.d,
// in the `axon` crate) build on this. See
// docs/paper_websocket_cognitive_primitive.md.
// v2.3.0 — multiparty session types (Honda–Yoshida–Carbone). A
// `GlobalType` declares an n-party protocol; projection `G⌐r` extracts
// each role's binary `SessionType` (the v2.3.0 algebra). The safe-
// realizability gate is `project_all`: a `Result::Ok` is the structural
// certificate that independent per-role runtimes faithfully realise `G`.
// v1.2.0 — the closed registry of every primitive AXON exposes as
// a named language construct. Single source of truth for the ℰMCP
// coverage gate + scaffold CLI + future LSP completions / docs-site
// generators. Pure const data, no runtime deps. See the module-level
// docs for the discipline (registry + corpus = atomic addition).
/// v2.67.0 — the anti-drift gate. The public README is parsed at test time and
/// every primitive it advertises must carry a human-attested statement of what
/// its runtime actually does. A presence-only gate would not have caught a single
/// v2.67.0 defect (`warden` and `quant` had a badge, a registry entry, a parser
/// production AND a dispatch arm — and were no-ops), so this one forces the
/// question no linter can decide.
// v2.76.0 — the Epistemic Module System, rebuilt natively in Rust
// (papers/paper_ems_axon.md). The retired Python EMS (v0.23.0,
// gone since v2.0.0) advertised separate compilation the Rust toolchain
// never had: `import` parsed, lowered, and resolved NOTHING. v2.76.0 makes
// it real — and goes one phase further: the LINKER exists, so a
// multi-module program executes. Pure modules, zero new deps (SHA-256 is
// the v1.31.0 hand-rolled `sha256_hex`); in-memory-first so the LSP and the
// enterprise bundle loader resolve without a filesystem.
pub use ;
// v2.37.0 — the blessed upstream preset catalog (versioned, forkable,
// ordinary `.axon` source per the design decision) + the `from Preset@vN` expansion the
// parser runs before type-check. Pure const data + a pure AST pass.
// v2.37.0 — `voice` macro-expansion to source text (the `axon desugar`
// payload). Pure AST pass run by the parser before preset expansion.
// v2.39.0 — Remote Hands: the pure, shared argv-template classifier + risk
// catalog used by BOTH the type-checker and the runtime dispatcher.
/// v2.46.0 — convert a duration literal (the lexer's `Duration` token
/// shape: digits + one of `s`/`ms`/`m`/`h`/`d`) into whole seconds. Pure,
/// total over the token grammar; `None` for anything else (a malformed
/// literal is `axon-T894` at the type-check layer). `ms` floors to whole
/// seconds — a sub-second credential TTL is `0` and rejected by the same
/// law. Shared by the IR lowering and the type checker so the two can
/// never disagree about what a `ttl:` means.