#![allow(dead_code)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum RuntimeStatus {
Real { proof: &'static str },
Partial { gap: &'static str },
FailsClosed { diagnostic: &'static str },
NotImplemented { finding: &'static str },
Unaudited,
}
impl RuntimeStatus {
pub fn is_unimplemented(self) -> bool {
matches!(self, RuntimeStatus::NotImplemented { .. })
}
}
use RuntimeStatus::*;
pub const ADVERTISED: &[(&str, RuntimeStatus)] = &[
("persona", Real { proof: "flow_dispatcher::pure_shape" }),
("intent", Unaudited),
("flow", Real { proof: "flow_dispatcher::dispatch_node (exhaustive, zero catch-alls)" }),
("reason", Real { proof: "pure_shape::run_reason" }),
("anchor", Real { proof: "anchor_checker" }),
("refine", Real { proof: "pure_shape::run_refine" }),
("memory", Real { proof: "cognitive::run_remember / run_recall (PEM write-through)" }),
("tool", Real { proof: "lambda_tools::dispatch_use_tool_real (§58)" }),
("probe", Real { proof: "pure_shape::run_probe" }),
("weave", Real { proof: "pure_shape::run_weave" }),
("validate", Real { proof: "pure_shape::run_validate" }),
("context", Unaudited),
("know", Unaudited),
("believe", Unaudited),
("speculate", Unaudited),
("doubt", Unaudited),
("par", Real { proof: "parallel::run_par (real fan-out via join_all, §65)" }),
("hibernate", NotImplemented { finding: "§111 F20 — returns \"(hibernating …)\" synchronously; no CPS suspend, no resume, timeout not honored" }),
("dataspace", Real { proof: "dataspace_engine (columnar, first-party)" }),
("ingest", Real { proof: "cognitive::run_ingest — bounds-before-parse, sha256 + Untrusted taint (§108)" }),
("focus", Real { proof: "dataspace_engine::focus_query (σ∘π)" }),
("associate", Real { proof: "dataspace_engine::associate_query (hash equi-join; refuses a keyless join)" }),
("aggregate", Real { proof: "dataspace_engine::aggregate_query (γ)" }),
("explore", Real { proof: "dataspace_engine::explore_profile (zone-map stats)" }),
("deliberate", FailsClosed { diagnostic: "axon-T939 (§111) — the body is discarded at parse time; no budget was ever controlled" }),
("consensus", FailsClosed { diagnostic: "axon-T940 (§111) — no votes, no aggregation, no candidates" }),
("forge", Partial { gap: "§111 F17 — the Poincaré pipeline + NCD novelty gate are real, but `coherence` is hardcoded to 1.0, so a declared `constraints:` coherence floor is INERT" }),
("agent", Unaudited),
("shield", Partial { gap: "§111 — the scanner registry IS consulted and a Reject really fails the step, but OSS ships ZERO registered scanners, so an OSS adopter's shield is an identity pass-through until one is mounted" }),
("savant", Unaudited),
("synth", Unaudited),
("warden", Real { proof: "tests/fase111_c_warden_wired.rs (§111.c — real attested findings, verify()-gated, body runs, fail-closed at 6 joints)" }),
("scope", Real { proof: "tests/fase111_c_warden_wired.rs — the scope catalog is resolved at dispatch and the allowlist enforced (the check §88.c deferred)" }),
("stream", Real { proof: "tests/fase111_e_stream_runs.rs (§111.e — the body is parsed, lowered and EXECUTED; it used to be discarded at parse time)" }),
("effects", Real { proof: "parse_effect_row + type_checker; §85 `cache` derives cacheability from the `effects: pure` proof" }),
("@contract_tool", Unaudited),
("@csp_tool", Unaudited),
("pix", Real { proof: "pix_navigator (embeddings-free structural index)" }),
("navigate", Partial { gap: "§111 F11 — three REAL deterministic engines (MDN store-sourced, MDN in-memory, PIX), BUT with no indexable source in scope it falls back to an LLM prompt that INSTRUCTS the model to fabricate a provenance trail. The one live §108 left in the tree" }),
("drill", Partial { gap: "§111 — real subtree navigation when a source is in scope; degrades to a placeholder string otherwise" }),
("trail", Partial { gap: "§111 — reads the real breadcrumb `navigate` seeds; falls back to a placeholder when no navigate ran. Inherits F11: a trail harvested from the LLM fallback is confabulation wearing an audit's clothes" }),
("corpus", Real { proof: "mdn (signed Epistemic PageRank; §62–§64)" }),
("psyche", Unaudited),
("ots", NotImplemented { finding: "§111 F18 — `apply_ots_to_target` is literally `target.to_string()`; no ots_registry exists anywhere, so the documented \"enterprise override\" has no hook to override" }),
("mcp", Unaudited),
("mandate", NotImplemented { finding: "§111 F18 — `apply_mandate_to_target` is `target.to_string()`; a compliance-bound transformation that transforms nothing and can never fail" }),
("lambda", NotImplemented { finding: "§111 F18 — `apply_lambda_data` returns the string \"lambda:<name>(<target>)\"; no ΛD evaluation, no CPS dispatcher" }),
("compute", Real { proof: "tests/fase111_f_compute_real.rs (§111.f — a named PURE FUNCTION over the §70 expression language, evaluated natively by eval_expr: linear in the term, ZERO tokens, no model in the loop. Every failure refuses rather than binding a string that looks like a number)" }),
("daemon", Real { proof: "daemon.rs — OTP-style supervision + §74 durable event delivery" }),
("listen", Partial { gap: "§111 F7 — TWO disjoint paths sharing one keyword. Inside a DAEMON: real (§74 outbox → deliver_typed_event → execute_server_flow). Inside a FLOW BODY: binds the canned string \"(awaiting <channel>)\". Sub-gap: a daemon listener body executes ONLY `run <Flow>` steps; any other step type is silently dropped" }),
("axonendpoint", Real { proof: "axon_server — typed routes, body/output schemas, Idempotency-Key (§32/§37)" }),
("axpoint", Real { proof: "an ALIAS of axonendpoint — same TokenType (tokens.rs)" }),
("axonstore", Real { proof: "wire_integrations::run_{persist,retrieve,mutate,purge} — parameterized SQL, capability gate, epistemic floor, HMAC-Merkle audit chain" }),
("resource", Real { proof: "tests/fase113_c_resource_is_a_wire.rs (§113.c — an `axonstore { resource: Db }` DERIVES its DSN and its POOL SIZE from the resource: `capacity: 20` produces twenty connections. Before §113 `capacity` was read by zero lines of code in either repo while every pool sat at a hardcoded 10, and `lifetime` — sold as Linear Logic — was read by nothing at all)" }),
("fabric", NotImplemented { finding: "§113 — `within:` gave it SUBJECTS, and disjointness is now unrepresentable by construction (one field ⇒ a resource cannot be in two fabrics). But `provider`/`region`/`zones` are consumed by NOTHING at runtime: in `LiveHandler::provision` the parameter is literally `_fabrics`, and that function refuses anyway. Still governs nothing that runs" }),
("manifest", Partial { gap: "§111 F14 — the κ/compliance half IS genuinely consumed (it feeds attestation + the audit scorer); the \"desired shape\" half is dead" }),
("observe", Real { proof: "tests/fase112_c_cognitive_io_deploy.rs (§112.a/c — a real Handler reaches a real target through a deny-by-default SourceRegistry; an observation that cannot be taken REFUSES. The only prior Handler returned certainty 1.0 unconditionally, without going anywhere)" }),
("reconcile", Real { proof: "tests/fase112_e_reconcile_drift.rs (§112.e — REAL Jaccard drift between the manifest's desired shape and the world's actual shape. It used to compare the belief against ITSELF: when evidence was missing it defaulted to the manifest, so drift was structurally always 0.0)" }),
("lease", Real { proof: "tests/fase113_d_lease_breach_fires.rs (§113.d — post-expiry USE of a leased store is the CT-2 Anchor Breach, and all three `on_expire` policies are honoured. The kernel was NEVER broken: it had no SUBJECT. A flow could not USE a resource, so a guarantee about post-expiry use was VACUOUS — unviolatable, and therefore unkeepable. §113 made the store operation the use)" }),
("ensemble", Real { proof: "tests/fase112_c_cognitive_io_deploy.rs (§112.b/c — the EnsembleAggregator is instantiated from the IR at deploy and aggregates only observations ACTUALLY TAKEN; a refused source is absent, not present-and-failing, which is what lets its quorum gate work honestly)" }),
("topology", Real { proof: "type_checker::check_topology_liveness — a genuine DFS gray/black cycle detector emitting a Honda-liveness violation (narrow sufficient condition, but real)" }),
("session", Real { proof: "type_checker::check_session_duality → session.rs (dual involution, capture-avoiding substitution, coinductive equality). Duality is genuinely DECIDED, not faked" }),
("send", Real { proof: "lowered into the session algebra; an unmatched send fails the duality check" }),
("receive", Real { proof: "lowered into the session algebra; dual of send" }),
("select", Real { proof: "session.rs dual_map — internal/external choice duality is really checked arm-for-arm" }),
("branch", Real { proof: "session.rs dual_map — the dual of select" }),
("immune", Real { proof: "tests/fase112_d_immune_fires.rs (§112.d — the KL sensor detects a REAL deviation from a LEARNED baseline. Wiring it exposed a kernel bug that made it structurally blind: an unseen symbol was scored against the baseline's MINIMUM probability, so a perfectly stable baseline could never register an anomaly at all)" }),
("reflex", Real { proof: "tests/fase112_d_immune_fires.rs (§112.d — a real anomaly FIRES the declared action with an HMAC-signed trace, within its sla:, and the same signature does not re-fire. No reflex may fire while the baseline is still being learned — that would be a false positive by construction)" }),
("heal", Real { proof: "tests/fase112_d_immune_fires.rs (§112.d — the HealKernel is registered from the IR and renders a decision under its declared mode: on a real health report)" }),
("compliance", Partial { gap: "§111 F16 — the language's flagship claim, and exactly ONE genuine κ-coverage rule exists (scoped to `component`). The axon-T890 endpoint rule is a PRESENCE check (`!compliance.is_empty()`), not a coverage law. The checker documents its own gap at type_checker.rs:11726" }),
("component", Partial { gap: "§111 — the compile-time shield-coverage law over regulated κ IS genuinely enforced (a real set difference). But the component renders NOTHING; the README itself defers the renderer" }),
("view", Partial { gap: "§111 — only referential integrity is checked. No `route` check, no session-typed-reactivity check, and it renders nothing" }),
("cache", Real { proof: "cache_runtime — cacheability derives from the type system's `effects: pure` proof (§85)" }),
("voice", Unaudited),
("shell", Unaudited),
("path rewrite", Unaudited),
("PASETO", Unaudited),
("socket", Real { proof: "tests/fase111_i_socket_served.rs (§111.i — the OSS server now SERVES the session-typed WebSocket at GET /ws/{socket}, and enforces the protocol the adopter DECLARED: the missing SessionType compiler lands in session_runtime::compile. An unresolvable protocol is REFUSED, never substituted — enterprise used to hand every socket a hardcoded chat schema, so a protocol proven dual at compile time had a different one enforced at runtime)" }),
("send T", Real { proof: "the session algebra's send, carrying a payload type" }),
("receive T", Real { proof: "the session algebra's receive" }),
("select {ℓᵢ:…}", Real { proof: "session.rs Select — labelled internal choice" }),
("branch {ℓᵢ:…}", Real { proof: "session.rs Branch — labelled external choice" }),
("backpressure: credit(k)", Real { proof: "session_runtime credit window + the PCC credit-positivity witness" }),
("reconnect: cognitive_state", Unaudited),
("step", Real { proof: "flow_dispatcher::pure_shape — the step executor every flow runs through (the same shared seam §114's channel guards read)" }),
("run", Real { proof: "§65 unified executor — runner + execute_server_flow bind flow+persona+context and execute; every fase gate that runs a program runs through it" }),
("type", Real { proof: "type_checker (structural + refinement validation) + store_schema (§38 — declared shapes pinned to SQL column types)" }),
("json", Real { proof: "tests/fase73_c_json_accessors.rs + tests/fase73_e_json_lens.rs (§73 — total navigation; honest fail-closed accessor semantics pinned in axon-rs orchestration tests)" }),
("ledger", Unaudited),
("channel", Partial { gap: "§114.z — durable persistence (§74 outbox) and the σ-shield egress gate (§114, tests/fase114_channel_shield_egress.rs) are proven; `qos:`/`lifetime:` enforcement is unaudited" }),
("emit", Real { proof: "tests/fase114_channel_shield_egress.rs (§114 — the channel's shield scans on EVERY path by IR-resolution; Reject fails closed before any routing) + §74 durable outbox delivery" }),
("publish", Unaudited),
("discover", Unaudited),
("budget", Real { proof: "tests/fase114_a_budget_governs_the_canonical_path.rs (§114.a — the ceiling binds on the canonical `use Tool(…)` path; before, the field was README prose that governed nothing)" }),
("window", Unaudited),
("cors", Unaudited),
("document", Real { proof: "axon-T916 (§99 — compile-time-validated, byte-deterministic OOXML synthesis; the assertion-laundering barrier refuses a sub-believe value in an assertive slot)" }),
("deliver", Real { proof: "delivery.rs + axon-T920 (§105 — provenance travels or the delivery refuses; first top-level egress integrated in the executor, D105.7(B))" }),
("notify", Real { proof: "notification.rs + axon-T933/T934/T935 (§110 — carried lineage or refusal; at-most-once-per-window attention ledger across replicas, ENT mig 033)" }),
("credential", Real { proof: "tests/fase92_mint_runtime.rs (§92 — grants ⊆ minter, TTL ≤ 24h; axon-T893–T896)" }),
("mint", Real { proof: "tests/fase92_mint_runtime.rs (§92 — fail-closed without a minter port; the raw bearer is shown once and never persisted, axon-T896)" }),
("rotate", Real { proof: "tests/fase94_custody_runtime.rs (§94 — rotation_without_revelation: ENUMERATE+ROTATE(CAS)+USE; no term evaluates to a secret value)" }),
("upstream", Real { proof: "tests/fase80_d_upstream_e2e.rs (§80 — config-resolved dial, declared auth, credit flow-control against a real WS server)" }),
("quant", Real { proof: "tests/fase111_d_quant_wired.rs (§111.d — E = ⟨ψ|M|ψ⟩ by real arithmetic; the body RUNS; `depth:` is refused rather than fabricating the physics)" }),
("observable", Real { proof: "tests/fase111_d_quant_wired.rs (§111.d — the DECLARED observable is resolved and measured; no resolvable M ⇒ refusal, because an expectation without an observable is a category error)" }),
("grad", Real { proof: "tests/fase109_grad_runtime.rs (§109 — SYMBOLIC differentiation at compile time; the gradient IS IR under the PCC GradientSoundness witness; the runtime only evaluates)" }),
];
pub const KNOWN_DEBT: &[&str] = &[
"hibernate",
"ots",
"mandate",
"lambda",
"fabric",
];
pub fn status_of(name: &str) -> Option<RuntimeStatus> {
ADVERTISED
.iter()
.find(|(n, _)| *n == name)
.map(|(_, s)| *s)
}
#[cfg(test)]
mod tests {
use super::*;
use std::collections::HashSet;
use std::path::Path;
fn repo_root() -> &'static Path {
Path::new("..")
}
fn readme_advertised() -> Vec<String> {
let readme = std::fs::read_to_string(repo_root().join("README.md"))
.expect("the public README must be readable — it is an INPUT to this build");
let start = readme
.find("<!-- Cognition primitives -->")
.expect("the README's primitive badge block must be findable");
let end = readme[start..]
.find("</p>")
.expect("the badge block must terminate")
+ start;
let block = &readme[start..end];
let mut out = Vec::new();
let mut rest = block;
while let Some(i) = rest.find("<code>") {
rest = &rest[i + 6..];
let j = rest.find("</code>").expect("unterminated <code> badge");
out.push(rest[..j].to_string());
rest = &rest[j + 7..];
}
out
}
#[test]
fn every_advertised_name_is_classified() {
let missing: Vec<String> = readme_advertised()
.into_iter()
.filter(|n| status_of(n).is_none())
.collect();
assert!(
missing.is_empty(),
"the README advertises {} name(s) with NO entry in `ADVERTISED`:\n {}\n\n\
You cannot advertise a primitive without stating what its runtime does. \
That omission is exactly how §111 happened: `warden` and `quant` had a README \
badge, a registry entry, a parser production AND a dispatch arm — and were no-ops.",
missing.len(),
missing.join("\n ")
);
}
#[test]
fn every_advertised_registry_primitive_is_classified() {
let missing: Vec<&str> = crate::primitive_registry::PRIMITIVE_REGISTRY
.iter()
.filter(|i| i.is_advertised)
.map(|i| i.name)
.filter(|n| status_of(n).is_none())
.collect();
assert!(
missing.is_empty(),
"{} registry primitive(s) are `is_advertised` with NO entry in `ADVERTISED`:\n {}\n\n\
The registry is the enumeration source (§114.z). A primitive that is part of \
the public promise cannot exist without someone stating, on the record, what \
its runtime does. That omission is exactly how `budget` (§114.a) happened.",
missing.len(),
missing.join("\n ")
);
}
#[test]
fn every_advertised_registry_primitive_is_badged() {
let badges: HashSet<String> = readme_advertised().into_iter().collect();
let unbadged: Vec<&str> = crate::primitive_registry::PRIMITIVE_REGISTRY
.iter()
.filter(|i| i.is_advertised)
.map(|i| i.name)
.filter(|n| !badges.contains(*n))
.collect();
assert!(
unbadged.is_empty(),
"these `is_advertised` registry primitives have NO `<code>` badge in the README: \
{unbadged:?}\nAdd the badge (and its classification) or flip `is_advertised` — \
deliberately, in the same PR."
);
}
#[test]
fn non_advertised_registry_primitives_are_neither_badged_nor_classified() {
let badges: HashSet<String> = readme_advertised().into_iter().collect();
for info in crate::primitive_registry::PRIMITIVE_REGISTRY {
if info.is_advertised {
continue;
}
assert!(
!badges.contains(info.name),
"`{}` is `is_advertised: false` but carries a README badge — the flag lies",
info.name
);
assert!(
status_of(info.name).is_none(),
"`{}` is `is_advertised: false` but is classified in ADVERTISED — \
either advertise it deliberately or remove the classification",
info.name
);
}
}
#[test]
fn every_classified_name_is_still_advertised() {
let advertised: HashSet<String> = readme_advertised().into_iter().collect();
let zombies: Vec<&str> = ADVERTISED
.iter()
.map(|(n, _)| *n)
.filter(|n| !advertised.contains(*n))
.collect();
assert!(
zombies.is_empty(),
"these names are classified here but are NO LONGER advertised in the README: {zombies:?}\n\
Retracting a primitive means deleting it from BOTH."
);
}
#[test]
fn no_new_unkept_promises() {
let debt: HashSet<&str> = KNOWN_DEBT.iter().copied().collect();
let undeclared: Vec<&str> = ADVERTISED
.iter()
.filter(|(_, s)| s.is_unimplemented())
.map(|(n, _)| *n)
.filter(|n| !debt.contains(*n))
.collect();
assert!(
undeclared.is_empty(),
"these advertised primitives are NotImplemented and are NOT in KNOWN_DEBT: {undeclared:?}\n\n\
You have advertised a promise the code does not keep. Either implement it, retract it \
from the README, or (if you are knowingly shipping the gap) add it to KNOWN_DEBT with \
its finding — so it is a LEDGER ENTRY and not a lie."
);
}
#[test]
fn the_debt_ledger_only_shrinks() {
assert!(
KNOWN_DEBT.len() <= 14,
"KNOWN_DEBT grew to {} — the ratchet only turns one way. §111 inherited 14 unkept \
promises; a new one is not an entry to add, it is a bug to fix.",
KNOWN_DEBT.len()
);
}
#[test]
fn the_debt_ledger_has_no_padding() {
for name in KNOWN_DEBT {
let s = status_of(name)
.unwrap_or_else(|| panic!("KNOWN_DEBT names `{name}`, which is not advertised"));
assert!(
s.is_unimplemented(),
"`{name}` is in KNOWN_DEBT but its status is {s:?} — if it was implemented or \
retracted, delete its ledger row in the same PR."
);
}
}
#[test]
fn every_real_claim_cites_a_proof_that_exists() {
for (name, status) in ADVERTISED {
if let Real { proof } = status {
assert!(
!proof.trim().is_empty(),
"`{name}` claims Real with an empty proof"
);
if let Some(path) = proof.split_whitespace().find(|t| t.starts_with("tests/")) {
let full = repo_root().join("axon-rs").join(path);
let alt = repo_root().join("axon-frontend").join(path);
assert!(
full.exists() || alt.exists(),
"`{name}` claims Real and cites `{path}`, which does not exist. \
A proof that cannot be run is not a proof."
);
}
}
}
}
#[test]
fn every_partial_and_failsclosed_names_its_gap() {
for (name, status) in ADVERTISED {
match status {
Partial { gap } => assert!(
!gap.trim().is_empty(),
"`{name}` is Partial with no stated gap — name it, or it will rot"
),
FailsClosed { diagnostic } => assert!(
!diagnostic.trim().is_empty(),
"`{name}` FailsClosed with no diagnostic named"
),
_ => {}
}
}
}
#[test]
fn the_unaudited_population_only_shrinks() {
let n = ADVERTISED
.iter()
.filter(|(_, s)| matches!(s, Unaudited))
.count();
assert!(
n <= 23,
"the Unaudited population grew to {n} — §111 left 18, §114.z's census widening \
re-baselined at 23. Auditing is the only direction."
);
}
}