aprender-contracts 0.74.0

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation
//! ONT-001 §3.7 — extractors: how each entity type becomes RDF. Every extractor is pure Rust, deterministic
//! (R-15), and registered in Σ `extractors[]` with its reader gate (R-11). ONT-4b implements `pv_contract`; `json`
//! (aprender#3515, for infra's ARBITER-001 §14) reads a tool's own `--json` output through the vocabulary map its
//! contract carries; ONT-4c1 (aprender#3508) implements `gguf` and `apr_model` — the model receipts — and joins
//! the tracked ladder receipts to the rungs (`resolves: receipt`, [`crate::ontology::receipts`]); the rest are
//! declared in Σ and arrive with their rows (ONT-4b2 implements `code` — the bound symbols by a `syn` module-tree walk —
//! and `lean` — the in-tree theorems); ONT-4c implements `readme`, `llm_context` and `csv`, sharing [`claims`].
//!
//! [`all`] is the ONE walk the shapes gate and `pv extract` share, so what the gate grades and what
//! `contracts.nt` records are the same graph (R-18: files are canonical, the graph is derived — from one place).

use std::path::Path;

use crate::ontology::rdf::Graph;
use crate::ontology::receipts;

pub mod apr_model;
pub mod binary;
pub mod claims;
pub mod cli_surface;
pub mod code;
pub mod covering;
pub mod csv;
pub mod example;
pub mod ggplot2_core;
pub mod gguf;
pub mod json;
pub mod kernel;
pub mod kernel_cells;
pub mod lean;
pub mod llm_context;
pub mod parity_receipt;
pub mod pv_contract;
pub mod readme;
pub mod release_cells;
pub mod release_crux;
pub mod release_evidence;
pub mod release_inputs;

/// Every extractor's output over `contract_dir`, plus the input-side warnings the extractors chose to carry
/// rather than hide (a torn JSONL line), plus what the model extractors and the receipt resolver counted.
#[derive(Debug, Clone, Default)]
pub struct Extraction {
    pub graph: Graph,
    pub warnings: Vec<json::Warning>,
    /// Contracts whose `entity.type` this build extracts, by stem.
    pub entities_extracted: Vec<String>,
    /// ONT-4c1: the ladder rungs and GGUF files, and the files this extractor refused.
    pub gguf: gguf::GgufStats,
    /// ONT-4c1: the `.apr` files read, and the files this extractor refused.
    pub apr_model: apr_model::AprStats,
    /// ONT-4c1: the tracked ladder receipts, as read.
    pub receipts: Vec<receipts::Receipt>,
    /// ONT-4c1: witnesses, hex mismatches, unmeasured rows, green / missing hosts.
    pub resolve: receipts::ResolveStats,
    /// ONT-4b2: the bound Rust symbols, resolved by the `syn` walk or not.
    pub code: code::CodeStats,
    /// ONT-4b2: the in-tree Lean theorems and the contracts that cite them.
    pub lean: lean::LeanStats,
    /// #3560 R1: the cargo example targets of the workspace members, and what they name.
    pub example: example::ExampleStats,
    /// ONT-4g: the cargo bin targets, read from the tracked snapshot and joined to the surface-audit ledger.
    pub binary: binary::BinaryStats,
    /// ONT-4c4: the bound `#[kernel]` symbols typed `ont:KernelSymbol`, and their kernel receipts.
    pub kernel: kernel::KernelStats,
    /// ONT-4c3: the logit-parity receipts under `evidence/parity/**`, and the files this extractor refused.
    pub parity: parity_receipt::ParityStats,
    /// ONT-4f: the GitHub snapshots under `evidence/github/<type>/`, per Σ snapshot type, and the refused files.
    pub github: json::github::GithubStats,
    /// ONT-4c: `README.md` — files read, the claim commands CI runs (the MEASURED set), refusals.
    pub readme: claims::DocStats,
    /// ONT-4c: `CLAUDE.md` (`llm-context`) — the same.
    pub llm_context: claims::DocStats,
    /// ONT-4c: CSV datasets read, and the files refused.
    pub csv: claims::DocStats,
    /// PLOT-GG-001: the ggplot2 core rows, the row contracts bound to them, and which rows are proven.
    pub ggplot2: ggplot2_core::Ggplot2Stats,
    /// aprender#3715: the release evidence — `None` unless a release subject was given (an ordinary PR has none).
    pub release: Option<release_evidence::ReleaseStats>,
    /// ONT-4d: how many `rdf:type` triples the Σ closure added.
    pub type_closure_added: usize,
}

/// Σ from `<contract_dir>/ontology.yaml`, when it parses and is well-formed. A malformed Σ is the `sigma`
/// gate's to report (exit 3). Here it just means "no closure", which that gate's refusal already surfaces.
#[must_use]
pub fn sigma_of(contract_dir: &Path) -> Option<crate::ontology::sigma::Sigma> {
    let text = std::fs::read_to_string(contract_dir.join("ontology.yaml")).ok()?;
    let s = crate::ontology::sigma::Sigma::from_yaml(&text).ok()?;
    s.check_integrity().ok()?;
    Some(s)
}

/// ONT-4d: for every `?x rdf:type ont:C` where `C` is a Σ concept, add `?x rdf:type ont:S` for every strict
/// super-concept `S` of `C`. Returns the number of triples added. Idempotent: a second pass adds none.
pub fn materialize_type_closure(graph: &mut Graph, sigma: &crate::ontology::sigma::Sigma) -> usize {
    use crate::ontology::rdf::{ont, Term, RDF_TYPE};
    let mut adds: Vec<(String, String)> = Vec::new();
    for c in sigma.concepts.keys() {
        let supers = sigma.supers(c);
        if supers.is_empty() {
            continue;
        }
        for x in graph.instances_of(&ont(c)) {
            adds.extend(supers.iter().map(|s| (x.to_string(), s.clone())));
        }
    }
    let before = graph.len();
    for (x, s) in adds {
        graph.insert(x, RDF_TYPE, Term::iri(ont(&s)));
    }
    graph.len() - before
}

/// What a walk could not do. Every variant is the DECLARATION's fault (exit 3), never a corpus verdict.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ExtractFailure {
    /// An `entity: {type: json}` contract could not be extracted.
    Json(json::ExtractError),
    /// A ladder receipt under `evidence/dogfood/models/` is unreadable or carries a foreign schema.
    Receipt(receipts::ReceiptError),
    /// aprender#3715: the release subject is malformed, or a release input is unreadable or foreign.
    Release(release_inputs::ReleaseError),
    /// PMAT-4160: a contract declares the reserved entity type [`RESERVED_ENTITY_TYPE`]. Its `entity:` predicates
    /// would be byte-identical to the entity CLASS IRIs, so the extraction is refused rather than written.
    ///
    /// [`RESERVED_ENTITY_TYPE`]: crate::ontology::sigma::RESERVED_ENTITY_TYPE
    ReservedEntityType { contract: String },
    /// ONT-4c4: a file under `evidence/kernels/` is unreadable or carries a foreign schema.
    Kernel(kernel::KernelError),
}

impl std::fmt::Display for ExtractFailure {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Json(e) => write!(f, "{e}"),
            Self::Receipt(e) => write!(f, "receipt {e}"),
            Self::Release(e) => write!(f, "{e}"),
            Self::ReservedEntityType { contract } => write!(
                f,
                "contract `{contract}` declares entity.type `{}`, which is reserved — `<ONT_BASE>entity/` holds \
                 the entity classes, so its entity predicates would collide with them (PMAT-4160)",
                crate::ontology::sigma::RESERVED_ENTITY_TYPE
            ),
            Self::Kernel(e) => write!(f, "{e}"),
        }
    }
}

impl std::error::Error for ExtractFailure {}

/// The corpus as `pv_contract` sees it; then every `entity: {type: json}` contract's document (relative to the
/// contract dir's parent — the repo root, the same base `ont:file` uses); then the `gguf` and `apr-model`
/// entities and the ladder receipts joined to the rungs. `Err` is a declaration's fault.
pub fn all(contract_dir: &Path) -> Result<Extraction, ExtractFailure> {
    all_with(contract_dir, None)
}

/// [`all`], plus — when `release` names a release subject — `extract:release-evidence` (aprender#3715): the
/// release's receipts as the graph `release-readiness-v1` grades. Same one walk (R-18).
pub fn all_with(
    contract_dir: &Path,
    release: Option<&release_inputs::Subject>,
) -> Result<Extraction, ExtractFailure> {
    let mut out = Extraction {
        graph: pv_contract::extract(contract_dir),
        ..Extraction::default()
    };
    let root = contract_dir.parent().unwrap_or(contract_dir);
    for (stem, _rel, doc) in pv_contract::documents(contract_dir) {
        let entity_type = pv_contract::scalar(doc.get("entity").and_then(|e| e.get("type")));
        if entity_type.as_deref() == Some(crate::ontology::sigma::RESERVED_ENTITY_TYPE) {
            return Err(ExtractFailure::ReservedEntityType { contract: stem });
        }
        if !json::applies(&doc) {
            continue;
        }
        let mut warnings =
            json::extract_into(&mut out.graph, &stem, &doc, root).map_err(ExtractFailure::Json)?;
        out.warnings.append(&mut warnings);
        out.entities_extracted.push(stem);
    }
    out.gguf = gguf::extract(contract_dir, &mut out.graph);
    out.apr_model = apr_model::extract(contract_dir, &mut out.graph);
    out.receipts = receipts::read_all(root).map_err(ExtractFailure::Receipt)?;
    out.resolve = receipts::resolve(&mut out.graph, &out.gguf.rungs, &out.receipts);
    out.code = code::extract(contract_dir, &mut out.graph);
    out.kernel = kernel::extract(&repo_root(contract_dir), &mut out.graph)
        .map_err(ExtractFailure::Kernel)?;
    out.lean = lean::extract(contract_dir, &mut out.graph);
    out.example = example::extract(contract_dir, &mut out.graph);
    out.binary = binary::extract(contract_dir, &mut out.graph);
    out.parity = parity_receipt::extract(root, &mut out.graph);
    // ONT-4f: the Σ snapshot types (repo, issue, pull-request, milestone), read by extract:json from the committed
    // snapshots only. No Σ is no snapshot types, so nothing under evidence/github/ is read — the sigma gate reports it.
    let sigma = sigma_of(contract_dir);
    let snapshot_types = sigma
        .as_ref()
        .map(json::github::snapshot_types)
        .unwrap_or_default();
    out.github = json::github::extract(&repo_root(contract_dir), &snapshot_types, &mut out.graph);
    // ONT-4c: the claim fences resolve against the merge-path `run:` lines, computed once per walk
    let ci = claims::ci_run_lines(&repo_root(contract_dir));
    out.readme = readme::extract(contract_dir, &mut out.graph, &ci);
    out.llm_context = llm_context::extract(contract_dir, &mut out.graph, &ci);
    out.csv = csv::extract(contract_dir, &mut out.graph);
    out.ggplot2 = ggplot2_core::extract(contract_dir, &mut out.graph);
    // ONT-4d (R-19): the rdf:type closure over Σ's `subsumes`, materialized AFTER every extractor has run, so a
    // focus node an extractor typed with a sub-concept is also an instance of every super-concept. This is
    // how a shape on a super-concept reaches it (shapes.rs selects focus nodes by rdf:type).
    out.type_closure_added = sigma
        .as_ref()
        .map_or(0, |s| materialize_type_closure(&mut out.graph, s));
    if let Some(subject) = release {
        out.release = Some(
            release_evidence::extract(&mut out.graph, contract_dir, subject)
                .map_err(ExtractFailure::Release)?,
        );
    }
    Ok(out)
}

/// The repo root an extractor resolves against: the contract dir's parent — and `.` when the contract dir is a
/// bare relative name like `contracts`, whose parent is the empty path (`read_dir("")` fails, and an extractor
/// that walked nothing would report an empty workspace as if it had measured one).
#[must_use]
pub fn repo_root(contract_dir: &Path) -> std::path::PathBuf {
    match contract_dir.parent() {
        Some(p) if !p.as_os_str().is_empty() => p.to_path_buf(),
        _ => std::path::PathBuf::from("."),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::ontology::rdf::{ont, Term, RDF_TYPE};

    fn sigma() -> crate::ontology::sigma::Sigma {
        let text = std::fs::read_to_string(
            Path::new(env!("CARGO_MANIFEST_DIR")).join("../../contracts/ontology.yaml"),
        )
        .expect("the repo's Σ is readable");
        crate::ontology::sigma::Sigma::from_yaml(&text).expect("the repo's Σ parses")
    }

    #[test]
    fn the_type_closure_counts_exactly_the_super_types_it_adds_and_a_second_pass_adds_none() {
        let s = sigma();
        let supers = s.supers("Kernel");
        assert!(!supers.is_empty(), "Kernel has a super-concept");
        let mut g = Graph::new();
        for i in 0..5 {
            g.insert(format!("urn:other:{i}"), "urn:p", Term::string("v"));
        }
        // two instances, so the count is >= 2 whatever the depth of Kernel's chain
        for k in ["urn:k", "urn:k2"] {
            g.insert(k.to_string(), RDF_TYPE, Term::iri(ont("Kernel")));
        }
        let before = g.len();
        let added = materialize_type_closure(&mut g, &s);
        assert_eq!(added, 2 * supers.len());
        assert_eq!(g.len(), before + added);
        for sup in &supers {
            let xs = g.instances_of(&ont(sup));
            assert!(xs.contains(&"urn:k") && xs.contains(&"urn:k2"), "{sup}");
        }
        assert_eq!(materialize_type_closure(&mut g, &s), 0, "idempotent");
    }

    #[test]
    fn an_extract_failure_displays_its_cause() {
        let e = ExtractFailure::ReservedEntityType {
            contract: "c.yaml".into(),
        };
        let msg = e.to_string();
        assert!(
            msg.starts_with("contract `c.yaml` declares entity.type `"),
            "{msg}"
        );
        assert!(msg.ends_with("(PMAT-4160)"), "{msg}");
    }
}