crtx-core 0.1.1

//! Shared AXIOM/Cortex claim language.
//!
//! AXIOM work records are useful because they separate criteria, hypotheses,
//! capabilities, evidence, and residual risk. Cortex treats those records as
//! structured candidate evidence, never as product authority. This module
//! provides the common vocabulary both sides can serialize without allowing
//! AXIOM formatting to upgrade truth or execution authority.

use schemars::JsonSchema;
use serde::{Deserialize, Serialize};

use crate::claims::{ClaimCeiling, ClaimProofState};

/// AXIOM element kind mapped into Cortex candidate evidence.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum AxiomElementKind {
    /// Completion criterion, e.g. `CHK[1]`.
    CompletionCriterion,
    /// Anti-criterion or forbidden outcome.
    AntiCriterion,
    /// Hypothesis, e.g. `HYP[1]`.
    Hypothesis,
    /// Capability invocation, e.g. `CAP[1]`.
    Capability,
    /// Evidence entry.
    Evidence,
    /// Decision record.
    Decision,
    /// Residual risk.
    ResidualRisk,
}

/// Cortex-side role assigned to an AXIOM element.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum CortexClaimRole {
    /// Candidate claim only; requires normal Cortex admission/promotion gates.
    CandidateClaim,
    /// Proof/evidence reference supporting another candidate.
    EvidenceReference,
    /// Capability provenance reference.
    CapabilityReference,
    /// Constraint that narrows what an agent may claim or do next.
    Constraint,
    /// Residual risk retained for review.
    ResidualRisk,
}

/// AXIOM evidence type.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum AxiomEvidenceKind {
    /// Directly inspected, executed, read, measured, or verified by the agent.
    Observed,
    /// Derived from named evidence.
    Inferred,
    /// Asserted by a source, vendor, user, or model but not independently verified.
    Claimed,
    /// Hypothetical, dry-run, estimated, or modelled.
    Simulated,
    /// Missing or unclassified evidence kind.
    Unknown,
}

impl AxiomEvidenceKind {
    /// Maximum Cortex claim ceiling supported by this AXIOM evidence class.
    ///
    /// Even AXIOM `observed` evidence is still agent-procedure evidence. It may
    /// support local candidate reasoning, but never signed or authority-grade
    /// Cortex claims by itself.
    #[must_use]
    pub const fn claim_ceiling(self) -> ClaimCeiling {
        match self {
            Self::Observed | Self::Inferred => ClaimCeiling::LocalUnsigned,
            Self::Claimed | Self::Simulated | Self::Unknown => ClaimCeiling::DevOnly,
        }
    }
}

/// AXIOM status after CHECK.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum AxiomStatus {
    /// Criterion passed or hypothesis supported.
    Supported,
    /// Criterion/hypothesis is partially supported.
    Partial,
    /// Criterion failed or hypothesis was rejected.
    Rejected,
    /// State is unknown or unresolved.
    Unknown,
    /// Capability was invoked.
    Invoked,
    /// Capability was explicitly not used.
    NotInvoked,
}

impl AxiomStatus {
    /// Proof state implied by the AXIOM status and source-anchor presence.
    #[must_use]
    pub const fn proof_state(self, has_evidence_refs: bool) -> ClaimProofState {
        match self {
            Self::Supported | Self::Invoked if has_evidence_refs => ClaimProofState::Partial,
            Self::Supported | Self::Invoked | Self::Partial => ClaimProofState::Unknown,
            Self::Rejected => ClaimProofState::Broken,
            Self::Unknown | Self::NotInvoked => ClaimProofState::Unknown,
        }
    }
}

/// A candidate AXIOM element before Cortex maps it into shared claim language.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
pub struct AxiomClaimInput {
    /// Stable AXIOM label such as `CHK[1]`, `HYP[2]`, or `CAP[1]`.
    pub axiom_label: String,
    /// AXIOM element kind.
    pub axiom_kind: AxiomElementKind,
    /// Human-readable statement.
    pub statement: String,
    /// CHECK-time status.
    pub status: AxiomStatus,
    /// Evidence kind declared by AXIOM.
    pub evidence_kind: AxiomEvidenceKind,
    /// Concrete source anchors or evidence refs.
    pub evidence_refs: Vec<String>,
    /// Capability/tool invocation refs, when applicable.
    pub capability_refs: Vec<String>,
    /// Residual risks attached to the element.
    pub residual_risks: Vec<String>,
    /// Highest Cortex claim level requested by the producer.
    pub requested_ceiling: ClaimCeiling,
}

impl AxiomClaimInput {
    /// Construct an AXIOM claim input.
    #[must_use]
    pub fn new(
        axiom_label: impl Into<String>,
        axiom_kind: AxiomElementKind,
        statement: impl Into<String>,
        status: AxiomStatus,
        evidence_kind: AxiomEvidenceKind,
    ) -> Self {
        Self {
            axiom_label: axiom_label.into(),
            axiom_kind,
            statement: statement.into(),
            status,
            evidence_kind,
            evidence_refs: Vec::new(),
            capability_refs: Vec::new(),
            residual_risks: Vec::new(),
            requested_ceiling: ClaimCeiling::LocalUnsigned,
        }
    }

    /// Attach source/evidence refs.
    #[must_use]
    pub fn with_evidence_refs<I, S>(mut self, refs: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<String>,
    {
        self.evidence_refs = refs.into_iter().map(Into::into).collect();
        self
    }

    /// Attach capability refs.
    #[must_use]
    pub fn with_capability_refs<I, S>(mut self, refs: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<String>,
    {
        self.capability_refs = refs.into_iter().map(Into::into).collect();
        self
    }

    /// Attach residual risks.
    #[must_use]
    pub fn with_residual_risks<I, S>(mut self, risks: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<String>,
    {
        self.residual_risks = risks.into_iter().map(Into::into).collect();
        self
    }

    /// Set the requested ceiling.
    #[must_use]
    pub const fn with_requested_ceiling(mut self, ceiling: ClaimCeiling) -> Self {
        self.requested_ceiling = ceiling;
        self
    }
}

/// Constraint severity exported from Cortex to AXIOM.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum AxiomConstraintSeverity {
    /// Informational; narrows interpretation but does not block work.
    Advisory,
    /// Limits claim scope.
    Limit,
    /// Hard prohibition.
    Hard,
}

/// Constraint category exported from Cortex to AXIOM.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum AxiomConstraintKind {
    /// Content may be admitted only as a Cortex candidate.
    CandidateOnly,
    /// AXIOM must not emit promotion-shaped output.
    ForbidPromotionShapedOutput,
    /// A concrete source anchor is required.
    RequireSourceAnchor,
    /// Capability/tool provenance is required.
    RequireToolProvenance,
    /// Truth ceiling caps claim language.
    TruthCeiling,
    /// Proof state is unknown, partial, or broken.
    ProofStateLimit,
    /// Open conflict or contradiction exists.
    ConflictPresent,
    /// Redaction policy limits what AXIOM may see or repeat.
    RedactionBoundary,
    /// Low trust prevents stronger claims.
    LowTrust,
    /// Exported constraints do not grant execution authority.
    NoExecutionAuthority,
}

/// Cortex constraint exported to AXIOM.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
pub struct AxiomConstraint {
    /// Constraint kind.
    pub kind: AxiomConstraintKind,
    /// Constraint severity.
    pub severity: AxiomConstraintSeverity,
    /// Operator-facing message.
    pub message: String,
    /// Related references.
    pub refs: Vec<String>,
}

impl AxiomConstraint {
    /// Construct a constraint.
    #[must_use]
    pub fn new(
        kind: AxiomConstraintKind,
        severity: AxiomConstraintSeverity,
        message: impl Into<String>,
    ) -> Self {
        Self {
            kind,
            severity,
            message: message.into(),
            refs: Vec::new(),
        }
    }

    /// Attach refs to the constraint.
    #[must_use]
    pub fn with_refs<I, S>(mut self, refs: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<String>,
    {
        self.refs = refs.into_iter().map(Into::into).collect();
        self
    }
}

/// Cortex representation of one AXIOM element.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
pub struct CortexClaimMapping {
    /// Original AXIOM label.
    pub axiom_label: String,
    /// Original AXIOM element kind.
    pub axiom_kind: AxiomElementKind,
    /// Cortex role assigned to the element.
    pub cortex_role: CortexClaimRole,
    /// Statement retained as candidate evidence.
    pub statement: String,
    /// Declared AXIOM evidence kind.
    pub evidence_kind: AxiomEvidenceKind,
    /// AXIOM status.
    pub status: AxiomStatus,
    /// Evidence refs retained for Cortex admission/review.
    pub evidence_refs: Vec<String>,
    /// Capability refs retained for Cortex admission/review.
    pub capability_refs: Vec<String>,
    /// Residual risks retained for review.
    pub residual_risks: Vec<String>,
    /// Proof state implied by AXIOM status and refs.
    pub proof_state: ClaimProofState,
    /// Effective claim ceiling after AXIOM evidence and proof-state caps.
    pub claim_ceiling: ClaimCeiling,
    /// Constraints generated by the mapping.
    pub constraints: Vec<AxiomConstraint>,
}

impl CortexClaimMapping {
    /// Map one AXIOM element into Cortex shared claim language.
    #[must_use]
    pub fn from_axiom(input: AxiomClaimInput) -> Self {
        let cortex_role = cortex_role_for(input.axiom_kind);
        let proof_state = input.status.proof_state(!input.evidence_refs.is_empty());
        let claim_ceiling = ClaimCeiling::weakest([
            input.requested_ceiling,
            input.evidence_kind.claim_ceiling(),
            proof_state.claim_ceiling(),
        ])
        .expect("fixed-size ceiling set is non-empty");

        let mut constraints = Vec::new();
        constraints.push(AxiomConstraint::new(
            AxiomConstraintKind::CandidateOnly,
            AxiomConstraintSeverity::Hard,
            "AXIOM output is candidate evidence only; Cortex promotion gates still apply",
        ));

        if input.evidence_refs.is_empty()
            && matches!(
                input.axiom_kind,
                AxiomElementKind::CompletionCriterion
                    | AxiomElementKind::Hypothesis
                    | AxiomElementKind::Evidence
                    | AxiomElementKind::Decision
            )
        {
            constraints.push(AxiomConstraint::new(
                AxiomConstraintKind::RequireSourceAnchor,
                AxiomConstraintSeverity::Hard,
                "substantive AXIOM claims require Cortex-readable source anchors",
            ));
        }

        if input.axiom_kind == AxiomElementKind::Capability && input.capability_refs.is_empty() {
            constraints.push(AxiomConstraint::new(
                AxiomConstraintKind::RequireToolProvenance,
                AxiomConstraintSeverity::Hard,
                "AXIOM capability claims require invocation provenance",
            ));
        }

        if proof_state != ClaimProofState::FullChainVerified {
            constraints.push(AxiomConstraint::new(
                AxiomConstraintKind::ProofStateLimit,
                AxiomConstraintSeverity::Limit,
                format!("proof state {proof_state:?} limits Cortex authority"),
            ));
        }

        if claim_ceiling < input.requested_ceiling {
            let requested_ceiling = input.requested_ceiling;
            constraints.push(AxiomConstraint::new(
                AxiomConstraintKind::TruthCeiling,
                AxiomConstraintSeverity::Limit,
                format!("requested ceiling {requested_ceiling:?} downgraded to {claim_ceiling:?}"),
            ));
        }

        Self {
            axiom_label: input.axiom_label,
            axiom_kind: input.axiom_kind,
            cortex_role,
            statement: input.statement,
            evidence_kind: input.evidence_kind,
            status: input.status,
            evidence_refs: input.evidence_refs,
            capability_refs: input.capability_refs,
            residual_risks: input.residual_risks,
            proof_state,
            claim_ceiling,
            constraints,
        }
    }
}

/// Map a batch of AXIOM elements into Cortex shared claim language.
#[must_use]
pub fn map_axiom_claims<I>(inputs: I) -> Vec<CortexClaimMapping>
where
    I: IntoIterator<Item = AxiomClaimInput>,
{
    inputs
        .into_iter()
        .map(CortexClaimMapping::from_axiom)
        .collect()
}

fn cortex_role_for(kind: AxiomElementKind) -> CortexClaimRole {
    match kind {
        AxiomElementKind::CompletionCriterion
        | AxiomElementKind::AntiCriterion
        | AxiomElementKind::Hypothesis
        | AxiomElementKind::Decision => CortexClaimRole::CandidateClaim,
        AxiomElementKind::Capability => CortexClaimRole::CapabilityReference,
        AxiomElementKind::Evidence => CortexClaimRole::EvidenceReference,
        AxiomElementKind::ResidualRisk => CortexClaimRole::ResidualRisk,
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn axiom_observed_claim_maps_to_candidate_not_authority() {
        let mapping = CortexClaimMapping::from_axiom(
            AxiomClaimInput::new(
                "CHK[1]",
                AxiomElementKind::CompletionCriterion,
                "workspace tests passed",
                AxiomStatus::Supported,
                AxiomEvidenceKind::Observed,
            )
            .with_evidence_refs(["cmd:cargo test --workspace"])
            .with_requested_ceiling(ClaimCeiling::AuthorityGrade),
        );

        assert_eq!(mapping.cortex_role, CortexClaimRole::CandidateClaim);
        assert_eq!(mapping.proof_state, ClaimProofState::Partial);
        assert_eq!(mapping.claim_ceiling, ClaimCeiling::LocalUnsigned);
        assert!(mapping
            .constraints
            .iter()
            .any(|constraint| constraint.kind == AxiomConstraintKind::CandidateOnly));
    }

    #[test]
    fn claimed_or_simulated_axiom_evidence_fails_down_to_dev_only() {
        let mapping = CortexClaimMapping::from_axiom(
            AxiomClaimInput::new(
                "HYP[2]",
                AxiomElementKind::Hypothesis,
                "the system is production ready",
                AxiomStatus::Supported,
                AxiomEvidenceKind::Claimed,
            )
            .with_evidence_refs(["agent:final-answer"])
            .with_requested_ceiling(ClaimCeiling::AuthorityGrade),
        );

        assert_eq!(mapping.claim_ceiling, ClaimCeiling::DevOnly);
        assert!(mapping
            .constraints
            .iter()
            .any(|constraint| constraint.kind == AxiomConstraintKind::TruthCeiling));
    }

    #[test]
    fn capability_claim_without_provenance_requires_tool_reference() {
        let mapping = CortexClaimMapping::from_axiom(AxiomClaimInput::new(
            "CAP[1]",
            AxiomElementKind::Capability,
            "tests invoked",
            AxiomStatus::Invoked,
            AxiomEvidenceKind::Observed,
        ));

        assert_eq!(mapping.cortex_role, CortexClaimRole::CapabilityReference);
        assert!(mapping.constraints.iter().any(|constraint| {
            constraint.kind == AxiomConstraintKind::RequireToolProvenance
                && constraint.severity == AxiomConstraintSeverity::Hard
        }));
    }

    #[test]
    fn shared_claim_language_wire_shape_is_stable() {
        let mapping = CortexClaimMapping::from_axiom(
            AxiomClaimInput::new(
                "EVIDENCE[1]",
                AxiomElementKind::Evidence,
                "read docs/LANES.md",
                AxiomStatus::Supported,
                AxiomEvidenceKind::Observed,
            )
            .with_evidence_refs(["file:docs/LANES.md"]),
        );

        let value = serde_json::to_value(&mapping).expect("serialize mapping");
        assert_eq!(value["axiom_label"], serde_json::json!("EVIDENCE[1]"));
        assert_eq!(value["axiom_kind"], serde_json::json!("evidence"));
        assert_eq!(
            value["cortex_role"],
            serde_json::json!("evidence_reference")
        );
        assert_eq!(value["claim_ceiling"], serde_json::json!("local_unsigned"));
    }
}