aprender-contracts 0.71.3

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

pub mod artifact;
mod clause;
pub mod composition;
pub mod external_corpora;
pub mod kaizen;
mod kind;
mod parser;
mod types;
mod validator;

pub use artifact::{classify_artifact, validate_artifact, ArtifactKind};
pub use clause::{Clause, FormalStatus};
pub use external_corpora::{
    is_external_corpora_schema, parse_external_corpora_str, validate_external_corpora,
    ExternalCorpora, ExternalCorpus,
};
pub use parser::{is_contract_yaml, parse_contract, parse_contract_str};
pub use types::*;
pub use validator::validate_contract;

/// A contract from the workspace's `contracts/` directory, read at RUN time, for tests (#4129).
///
/// Several tests here used `include_str!("../../../../contracts/…")`, which is a path OUTSIDE this
/// crate, so `cargo test` from the published aprender-contracts tarball could not compile at all.
/// The in-tree decision is the one shared rule in [`crate::tree`]: in tree a missing contract
/// FAILS, and only a build outside the aprender workspace returns `None` with a named SKIP.
#[cfg(test)]
pub(crate) fn workspace_contract_or_skip(test: &str, rel: &str) -> Option<String> {
    crate::tree::workspace_file_or_skip_at(
        test,
        std::path::Path::new(env!("CARGO_MANIFEST_DIR")),
        &format!("contracts/{rel}"),
    )
}