Enum PropertyClass 

pub enum PropertyClass {
    ComplianceCoverage,
    EffectRowSoundness,
    CapabilityIsolation,
    ResourceBounds,
    ShieldHaltGuarantee,
    CapabilityContainment,
    ToolCallSoundness,
}

The closed catalog of properties a ProofTerm can certify.

§Fase 51.a ships Self::ComplianceCoverage. The §51.b-e classes (EffectRowSoundness, CapabilityIsolation, ResourceBounds, ShieldHaltGuarantee) land as the proof-term language generalizes (D51.4 — “universal” is the architecture, shipped one class at a time). Adding a variant here requires a matching witness variant + checker arm — the §51.a drift gate pins this lockstep.

Variants

ComplianceCoverage

Every regulatory class an apx/axonendpoint declares in compliance: is (a) a known class in the closed crate::esk::compliance registry and (b) backed by a present, resolvable shield (shield_ref non-empty AND that shield exists in the program IR). Catches phantom compliance classes (a typo’d HIPPA) and compliance-claimed-without-enforcement (declaring GDPR with no attached shield).

EffectRowSoundness

§51.b — every entry in a tool’s effects: <...> row is well-formed: its base is in the closed effect catalog (crate::pcc::effects::EFFECT_BASES); stream / trust carry a qualifier (stream’s in the backpressure catalog); and pure is exclusive (a tool cannot be both pure and effectful). Catches phantom effects (typo’d network), bare stream without a backpressure policy, and pure/impure contradictions.

CapabilityIsolation

§51.c — every capability gate an axonstore declares (its Pillar IV capability slug, §Fase 35.j) is a well-formed §32.g capability scope (matches the closed grammar ^[a-z][a-z0-9_]*(\.[a-z][a-z0-9_]*)*$, via the OSS axon_frontend::parser::is_valid_capability_slug). A malformed gate is a Pillar IV defect: it can never match a properly-formed bearer capability, so the store is either locked out or — worse, if a consumer treats “unparseable gate” as “no gate” — silently bypassed.

Scope (honest): this is the gate-integrity half. The containment half — an apx’s reachable store gates ⊆ its declared requires: set — needs the endpoint requires_capabilities (AST / enterprise deploy metadata, NOT lowered to the frontend IR) + flow→store reachability, and is deferred to §51.x (enterprise PCC consumption, where requires lives).

ResourceBounds

§51.d — declared resource bounds are within sane limits: an apx/axonendpoint’s retries is in [0, MAX_RETRIES] (negative is nonsensical; above the ceiling is a retry storm), and a socket carrying a DECLARED backpressure: credit(k) has k >= 1 (a credit window of 0 deadlocks the §Fase 41.b typed-resource gate). Unspecified socket credit is a legitimate type state and is NOT refuted. timeout is out of scope by design — it is a closed duration enum ({5s,15s,30s,60s}) already bounded at parse time, not an unbounded-resource risk.

ShieldHaltGuarantee

§51.e — a shield’s breach policy provides a real guarantee: on_breach is a recognized policy (closed catalog — catches a typo’d hault, which the parser does NOT reject since it reads on_breach as a bare identifier), and a shield declaring on_breach: halt actually scans something (a halt shield with an empty scan: [] can never detect a breach, so the halt never fires — a vacuous guarantee / security theater).

CapabilityContainment

§51.x — the CONTAINMENT half of capability isolation (the deferral §51.c flagged): every capability gate on a store the apx’s execute_flow REACHES is covered by the endpoint’s declared requires: scopes. Otherwise the flow touches a store gated by capability G the endpoint does not declare requiring — a request satisfying the endpoint’s declared requires could still reach a store it is not authorized for (capability leak / privilege escalation). Reachability is a SOUND over-approximation: every statically-reachable store op (both conditional branches + the loop body) is counted. An unresolvable execute_flow is REFUTED (cannot certify containment for a flow the artifact does not contain).

ToolCallSoundness

§58.i — every structured use <Tool>(k = v, …) call satisfies the called tool’s declared parameters: input schema: no argument names a parameter the tool does not declare; no argument is supplied twice; every required (non-optional) parameter is supplied; and every UNAMBIGUOUS-LITERAL argument’s type aligns with the declared type. This makes the §58.d CT-2 caller-blame check an INDEPENDENTLY-VERIFIABLE proof — the tool schema rides the bundle and the verifier re-derives the call’s soundness from the artifact, never trusting the compiler that ran the type-check (D1). Literal-type alignment is CONSERVATIVE (only Int/Float/Bool literals; bare identifiers + ${…} interpolations are runtime-resolved and skipped — zero false positives), so the structural facts (unknown / duplicate / missing) are always certified and the literal-type facts are certified where decidable statically. A schema-less tool (no parameters:) and the legacy use <Tool> on <arg> form carry no contract → no proof (D5).

Implementations

impl PropertyClass

pub fn slug(&self) -> &'static str

Stable wire slug for the property class.

Trait Implementations

impl Clone for PropertyClass

fn clone(&self) -> PropertyClass

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PropertyClass

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for PropertyClass

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for PropertyClass

impl PartialEq for PropertyClass

fn eq(&self, other: &PropertyClass) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for PropertyClass

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for PropertyClass