Quire Contract IR

Contract IR is the target-neutral model of a Quire contract. The Quire Specification Language compiler (QSL) checks a rule and writes a checked package, a canonical JSON file. This repository reads those bytes strictly, decides whether they can be trusted, and turns the parts a backend asks for into one versioned, canonical contract package.

It exists so that the tools that generate code or run proofs do not each parse the checked package their own way. If every backend decoded the file itself, two of them could disagree about what a rule means, or about which node is which. Contract IR gives them one reader, one set of node identities and one canonical encoding, and it says "refused", "unsupported" or "incomplete" instead of guessing when it cannot read or lower something.

Status: public prerelease. The API is not stable yet, the crates are versioned 0.1.0 and are not published to a registry (publish = false), and the repository is developed spec-first.

What it reads

A quire.checked-package/v2 has eight members. The reader checks every one: it refuses a package whose contract_version is not v2, whose bytes are not canonical JSON, whose package_id does not match the content it names, or whose required capabilities are missing. Evidence the package names (the domain package documents and any library packages it depends on) is handed in by the caller; the reader recomputes digests itself and never fetches anything.

Reading has three outcomes, and none of them is a guess:

Outcome	Meaning
Admitted	The package is complete and immutable, and safe to lower.
Refused	The input is invalid, with a typed code (malformed_wire, noncanonical_wire, stale_dependency, invalid_semantic_graph, unknown_contract_version and others) and the JSON pointer of the value at fault.
Incomplete	The input exceeded a limit the caller set, so no conclusion was reached.

What it lowers to

Lowering takes the keys a backend asks for and a lowering profile: which node families the backend supports, whether unbounded types must be bounded, and a work budget. Each request is answered on its own, so one bad key never changes the answer for another. Everything that lowered is assembled into a single quire.contract-package/v1 with canonical bytes and a package identity.

Smallest example

Read a package, then lower two keys, one of which is not in the graph. The reader half is read in tests/it/checked_package_v2_reader.rs and the lowering half is in tests/it/checked_package_v2_lowering.rs (profile and tc_050_non_lowered_records_are_terminal_and_independent); both run under make test.

use quire_contract_model::{
    CheckedPackageEvidence, CheckedPackageReadLimits, CheckedPackageV2,
    CheckedPackageV2ReadResult, CompleteLoweringProfileV2, CompleteLoweringRecordV2,
    LoweringProfileRef,
};

// `bytes` are canonical checked-package bytes; `evidence` holds the domain
// package documents the package names.
let package = match CheckedPackageV2::read(&bytes, CheckedPackageReadLimits::bounded(), &evidence) {
    CheckedPackageV2ReadResult::Admitted(package) => package,
    other => panic!("expected V2 admission, got {other:?}"),
};

let profile = CompleteLoweringProfileV2 {
    reference: LoweringProfileRef {
        authority: "quire".into(),
        identity: "complete-v1".into(),
    },
    supported_tags: all_node_families, // a BTreeSet<CheckedNodeTag>
    require_bounds: false,
    work_limit: u64::MAX,
};

// `missing` is a node key that is not in the graph; `present` is one that is.
let result = package.lower(&[missing.clone(), present], &profile);
assert_eq!(
    result.records[0],
    CompleteLoweringRecordV2::InvalidInput { node_id: missing }
);
// records[1] is `Lowered`, and `result.package` holds only that node.

Crates

The repository is a Cargo workspace with two packages and a one-way dependency.

Crate	What it holds
quire-contract-model	The stable model: the checked-package reader, lowering, canonicalization, diagnostics, wire checks, limits, bindings and the conformance runner. Owner crates depend on this package alone.
quire-contract-ir	The root crate, which depends on the model and adds the versioned bounded-Kani interface (quire_contract_ir::kani: profile, finite-input ABI, dispatch index and outcome types). It re-exports no model item; take those from quire_contract_model. It also builds the quire-contract-conformance binary.

Conformance corpus

corpus/contract-v0.1 is a language-neutral corpus of fixtures with expected results, and schemas/ holds the JSON schemas it is checked against. Run it without linking the Rust library:

quire-contract-conformance run --corpus corpus/contract-v0.1 --schemas schemas

The runner writes one JSON line per fixture and exits 0 when all match, 1 when any fixture mismatches and 2 on an invalid invocation or corpus. make corpus runs the same command through cargo. See corpus/contract-v0.1/README.md and schemas/README.md.

The Quire ecosystem

Contract IR sits in the main chain, between the compiler and the backends. It reads the checked packages that quire-spec-language writes, and its model is what code generation (quire-contract-codegen) and analysis (quire-analyze) work from. The model crate depends on quire-canonical for canonical JSON and digests, quire-walk for iterative walks over deep terms, and quire-verification-contracts for the checked-operation catalogue.

Building and testing

The toolchain is pinned in rust-toolchain.toml (Rust 1.98.1).

make test           # cargo test over the workspace, plus doctests
make lint           # clippy with -D warnings
make corpus         # the conformance corpus
make ci             # every local gate: fmt-check, lint, test, corpus, spec, deny, audit
make help           # all targets, including the lanes that need a QSL or QSpec checkout

Some conformance lanes (make conformance-qspec, conformance-qsl-ir769 and others) need a checkout of quire-specification (private) or quire-spec-language and are outside make test; make help names what each one needs.

Contributing

Every contribution needs a signed Contributor License Agreement, which the CLA bot walks you through on your first pull request. Requirements and acceptance criteria are updated before implementation, and the repository's specification, review and test gates must pass. See CONTRIBUTING.md and CLA.md.

License

Licensed under the GNU Affero General Public License, version 3 or (at your option) any later version (AGPL-3.0-or-later). See LICENSE.