axon/pcc/
effects.rs

1//! §Fase 51.b — the PCC checker's independent effect specification.
2//!
3//! Proof-Carrying Code requires the consumer's checker to embed the
4//! PROPERTY SPECIFICATION it verifies — it cannot delegate to the
5//! producer's (compiler's) internal logic, or it would not be
6//! independent (D51.2). This module is the checker's own statement of
7//! "what a well-formed effect row is": the closed base-effect catalog
8//! + the qualifier discipline.
9//!
10//! **Source of truth + drift:** this catalog mirrors
11//! `axon_frontend::type_checker::VALID_EFFECTS` (private const) +
12//! the §λ-L-E Fase 11.a qualifier rules. axon-frontend's catalog is
13//! the canonical compiler-side spec; this is the checker-side spec.
14//! They MUST agree. §51.f (which exposes `VALID_EFFECTS` as `pub` for
15//! the `axon pcc verify` CLI) adds the cross-crate drift gate asserting
16//! equality. Until then the equality is maintained by review + the
17//! `EFFECT_BASES` doc-comment pin. The stream-qualifier catalog
18//! ([`crate::stream_effect::BACKPRESSURE_CATALOG`]) IS public and is
19//! referenced directly (no duplication needed there).
20
21/// The closed catalog of valid base effects. Mirror of
22/// `axon_frontend::type_checker::VALID_EFFECTS` (v2.4.0). A tool's
23/// effect-row entry `base` or `base:qualifier` is well-formed only if
24/// `base` is in this set.
25pub const EFFECT_BASES: &[&str] = &[
26    "io",
27    "network",
28    "pure",
29    "random",
30    "storage",
31    "stream",
32    "trust",
33    "sensitive",
34    "legal",
35    "ots",
36];
37
38/// Effects that REQUIRE a `:qualifier` to be sound. `stream` needs a
39/// backpressure policy (else the runtime cannot enforce backpressure);
40/// `trust` needs a proof kind (else the trust claim is unverifiable).
41/// A bare `stream` / `trust` is an unsound effect declaration.
42pub const QUALIFIER_REQUIRED_BASES: &[&str] = &["stream", "trust"];
43
44/// Split an effect-row entry into `(base, Option<qualifier>)`.
45/// `"network"` → `("network", None)`; `"stream:drop_oldest"` →
46/// `("stream", Some("drop_oldest"))`. Total.
47pub fn split_effect(entry: &str) -> (&str, Option<&str>) {
48    match entry.split_once(':') {
49        Some((b, q)) => (b, Some(q)),
50        None => (entry, None),
51    }
52}
53
54/// Whether `base` is in the closed catalog.
55pub fn is_known_base(base: &str) -> bool {
56    EFFECT_BASES.contains(&base)
57}
58
59/// §Fase 53.c.2 — the built-in `epistemic:<level>` provenance axis.
60/// Mirror of `axon_frontend::type_checker::VALID_EPISTEMIC_LEVELS`.
61/// `epistemic` is NOT an enforceable base — it is a ΛD confidence
62/// annotation (PROVENANCE-class), carrying no runtime capability. The
63/// frontend parser captures `epistemic:<level>` into a dedicated field,
64/// but the IR generator re-injects it into the tool's effect_row as the
65/// string `epistemic:<level>` (`ir_generator.rs`). So the PCC checker
66/// MUST recognize it as a valid provenance entry — else every tool
67/// declaring an epistemic level is wrongly refuted as an unknown base
68/// (the pre-§53.c.2 bug Kivi brief #15 hit, forcing them to strip the
69/// ΛD wedge). This is the built-in analogue of an `extension`-declared
70/// provenance base (§53.d).
71pub const EPISTEMIC_LEVELS: &[&str] = &["believe", "doubt", "know", "speculate"];
72
73/// Whether `entry` is a built-in `epistemic:<level>` provenance member.
74pub fn is_epistemic_provenance(entry: &str) -> bool {
75    matches!(entry.split_once(':'), Some(("epistemic", level)) if EPISTEMIC_LEVELS.contains(&level))
76}
77
78/// Whether `base` requires a qualifier to be sound.
79pub fn requires_qualifier(base: &str) -> bool {
80    QUALIFIER_REQUIRED_BASES.contains(&base)
81}
82
83/// Whether a `stream:<q>` qualifier is a valid backpressure policy.
84/// Delegates to the PUBLIC `BACKPRESSURE_CATALOG` (no duplication).
85pub fn is_valid_stream_qualifier(qualifier: &str) -> bool {
86    crate::stream_effect::BACKPRESSURE_CATALOG.contains(&qualifier)
87}
axon/pcc/effects.rs

axon/pcc/
effects.rs
