quire-spec-language

complete exposes the edition 1-draft authoring boundary. Its declarative grammar table and one bounded interpreter produce a byte-exact CST with typed token kinds, named production nodes and a separate recovery stream. The module also provides revision-checked incremental edits, deterministic formatting and editor snapshots, the closed 176-capability complete bundle, canonical package identity and located diagnostics over the crate's existing code type. These APIs establish source and package admission only; the authority-bound diagnostic catalog and typed causes, checked extension compatibility, checked-package manifests, later checking, runtime and backend stages remain separate typed operations. Public source/editor calls receive only an exact-reference ProfileCatalog. Typed definition/model construction additionally requires a constructor-private ReaderAuthority; Task-054 owns issuance from the concrete checked reader, so raw bytes or caller-asserted capabilities cannot mint package authority here.

parse_native and parse_native_source select the authored edition and return either a historical unit or a typed, source-located 1-draft syntax unit. The composed path extends the existing Logos recognizer and Pratt parser across predicates, state, temporal and choreography forms. Issue #35 tracks this work under FR-035; package linking continues with linking::composed::admit_namespace: exact source inventory, package-wide native names, typed declaration references and cycle/dependent refusals under explicit work limits. linking::composed::binding::bind then resolves exact supplied definition/rule closures, native model exports, lexical/capture scopes and protocol structural references, preserving dependency-local refusals and unfinished work. Its NamesResolved result precedes expression/profile checking and complete runtime-role derivation. checking::composed::admit_types now checks shared values across predicates, state, temporal and protocol declarations. It retains exact nominal types, profiles, query shapes, capture provenance and dependency-local refusals, with pending proof/runtime obligations. Its Typed disposition establishes type admission only; exact authored formal sources supply the existing IR rational normalizer. checking::composed::proofs::discharge then checks supported guarded values through the existing IR prover and exact authored CheckBindings, preserving actual goals and dependent refusals. Ordered queries retain their original binder, collection and body through definedness and native emission. Sum admission checks every prefix in supported integer or denominator-one rational domains; broader rational sum transfer remains explicitly unsupported. General family admission and runtime validation remain open. Existing parse, format, CLI and checked-package APIs retain their historical profile; parsing alone grants no semantic admission or execution.

Embedded normative resources retain their original provenance and licensing.

The protocol_artifact library module supplies typed wire records, a bounded canonical encoder and a parser-free reader under compiler #40. read checks independently selected artifact/source/dependency references, actual admitted model exports, typed local handles and structural control edges. encode_candidate returns transport bytes; its result and reader admission remain separate from native compilation authority. protocol_artifact::native::admit consumes the actual composed proof report and independently selected source, definition and model inputs. It derives a constructor-private FamilyAdmission from supported complete native families; native::emit accepts only that authority and returns canonical bytes. See the wire contract for the exact encoding, identity domains and limits. The numeric component uses tagged canonical decimal strings for signed-64 integers and reduced rationals, with typed validation errors. Real source-to-reader tests exercise native predicate, state, temporal and protocol emission, including static compensation registration, activation, retries and full/partial recovery requirements. The Rust producer recipe combines four source units, queries, population/reference roles and actual model operations, recording the producer's own source identity as a digest over its own source text and retaining independently derived selectors. protocol_artifact::handoff::PUBLISHED_V1_HANDOFF now addresses that committed /1 handoff directly from the crate. Version-explicit member constants name its offer, external reference and Selection record; consumers need no environment variable, producer execution or repository-layout guess. Its Service and Provider roles retain distinct admitted model authorities so a strict consumer linker can enforce duplicate-authority refusal without rejecting the positive corpus. The existing unversioned PUBLISHED_HANDOFF family continues to address the unchanged /2 corpus. General dynamic choice/progress proofs, first-class relationship exports, runtime recovery and B's public consumer acceptance remain open; the supported boundary is stated in the wire contract.

Private native compiler for ix:native, edition 0-draft, profile state-finite/0-draft. It parses and formats source with located diagnostics. The library links exact imports and scoped names against supplied Contract IR formal environments. Its native checker establishes contextual types and guarded definedness through the existing IR prover under explicit runtime input obligations.

The native model admission API now checks explicit scalar, object and operation roles against supplied IR declarations and exact source coordinates, then emits a bounded deterministic model artifact. Its source-derived Rust fixture uses original parsed JSON occurrences. link_native now selects those artifacts, resolves explicit references and operations, and rejects conflicting model inventory identities. LinkedPackage::binding_profile, LinkedModel::native_model and LinkedClause::operation expose that correspondence. Model admission and linkage are qualified under Task-008.

model_source::read(formal_source, model_source::FORMAT, limits) now exposes the existing rule-model frontend to library callers. It derives located IR declarations and native roles from native-rule-model/1 source; ModelDraft::admit then runs the existing model checks. Errors retain the original source and typed cause. The example model shows the admitted source shape. Run cargo test --test it model_source:: for fixed-artifact, failure and runtime cases. Test helpers now call this production frontend.

Explicit model_source::FORMAT_V2 selects native-rule-model/2 and admits exact rational domains through native-state-model/2, retaining the actual IR bounds, units and source locations. Composed model exports consume these types; historical linking refuses a selected /2 model. This supplies the model prerequisite for composed value checking, whose type admission and supported guarded proofs are available through the composed checker. Complete runtime obligations remain open.

checking::check consumes a native linked package, exact CheckBindings and caller-lowered CheckLimits. It returns the original source/AST with native types, authored clause identities, discharged proof goals and required input populations, observations and operation frames. Stable and lexical guard keys preserve captured pre/post values; bounded proof expansion precedes actual IR checks. The 24 checker tests qualify Task-009. The public library contract is in native-model-checking.md; review and handoff are tracked in Plan-005.

runtime::Snapshot::new and runtime::Invocation::new now construct immutable inputs with exact bytes/digests, distinct reference types, structured errors and caller-lowered byte/node/entry/depth limits. Flat arenas preserve duplicate entries and shared values for later model-aware diagnosis. Twenty-one public API tests and a role-separation compile-fail doctest cover construction; its qualification is tracked in Plan-006. See native-runtime-inputs.md for the contract.

runtime::validate now checks exact artifact/clause/model bindings, supplied typed values, finite reference closure, operation captures, population deltas and immutable frames. Its constructor-private context retains the checked package and immutable input; failed reports retain located defects and fresh budget usage. Task-013 is qualified by SR-097 with 35 public API tests. See the review for scope and evidence.

runtime::evaluate executes the original native AST over a borrowed validated context. Reports retain concrete truth or an explicit incomplete/invariant-failure outcome, exact reference costs and original implication events. Borrowed values preserve pre/post captures, ordered sequence occurrences and object identities. Twenty-nine public tests and two private invariant controls cover reference execution, including all small functional graphs and independent budget vectors. See native-runtime-evaluation.md.

Five public pipeline tests now exercise healthy, violating, refused and incomplete parent/aggregate cases, operation captures/frames and immutable retries through actual model admission, parsing, linking, checking, construction, validation and evaluation. SR-099 records their passing review, and Plan-006 records the completed qualification/handoff with its final SR-100 gap audit. Backend projection and Quire integration remain downstream work. Construction establishes structure and byte correspondence; checking establishes static judgments conditional on valid input; validation establishes input conditions before predicate execution.

package::NativePackage::new now exports a checked package's complete selected models, authored clauses, resolutions, runtime obligations and projection dispositions with separate byte and native static identities. Serde owns JSON encoding, with independently measured derivation/canonical/output passes. Task-016 is qualified by SR-111, with fixed canonical/artifact vectors, complete correspondence/capture controls, static dependency mutations and runtime-independent identity checks. NativePackage::read_verified now verifies selected bytes, closed JSON and external bindings, then repeats actual parse/link/check before comparing every serialized claim. Reconstructed packages execute the existing parent, aggregate and operation workflows, preserving refusal, incomplete outcomes and fresh retry budgets. Qualification is tracked in Plan-007. See the package contract.

lowering::lower derives complete Boolean executable projections through the existing strict IR binder, retaining original native authority and explicit model/read/observation correspondence. Object and graph expressions refuse. lowering::lower_for with ProjectionTarget::IntegerIrV1 additionally exports bounded integer arithmetic and comparisons accepted by the strict IR binder. Use quire-spec lower <compile.json> --target integer-ir/v1 for this target; codegen emits executable numeric Rust for obligation-free comparisons. The standalone_fixtures example emits integer-healthy and integer-violating requests for amount < 7. Their native runs return true and false; both export the same integer projection. ProjectionTarget::StateScalarIrV1 additionally projects primitive self fields and pre expressions. NativeProjection::inputs supplies their actual values from a context validated against that exact checked package, retaining snapshot, invocation and object provenance. For the concrete update example, run quire-spec lower <unchanged-version/compile.json> --target state-scalar-ir/v1. This binds self.versionNumber = pre(self.versionNumber) with separate pre/post inputs; native population and frame validation still precedes materialization. Object/graph expressions refuse at the earliest source-owned boundary without a substitute IR expression. Tests that compose these projections with the code generator (generated Rust, strategies, Kani and native parity: IT-008, IT-010 and TC-094) live in agent-ix/quire-integration. See Plan-008.

CLI command and source identity/revision labels must be UTF-8; invalid encoding returns usage exit 20. File operands remain OS paths. JSON paths are display text, which may contain replacement characters; exact labels and the actual byte digest carry the separate source correspondence. See the native diagnostic catalog for stable outcomes.

Library callers can use format::format_with_limit(unit, output_bytes) to lower the inclusive 1 MiB output-content ceiling. It counts every emitted byte, including the final newline, and refuses before an append would exceed the limit. Existing format::format(unit) retains the default ceiling. Allocator capacity is not an exact content-byte accounting promise.

Run and check

The ConfigVersion example supplies the named parent-order, cycle, identity and recorded-update workflow, with 13 native and Markdown request sets and explicit refused/incomplete cases.

The native CLI needs no Node or JVM. Default native commands need no optional features; the Quire consumer is enabled explicitly with quire-extraction. Use --target-dir target where a machine config points Cargo outside the checkout.

On the shared desktop, run Cargo phases one at a time with nice -n 10 and -j 1, and run tests with -- --test-threads=1. Check for competing builds before starting and reuse existing worktree target caches. Do not start another phase until the previous command has completed.

cargo run --locked --target-dir target -- parse agent-ix test:parent fixture fixture:1 tests/fixtures/parent.native
cargo run --locked --target-dir target -- format agent-ix test:value-format fixture fixture:1 tests/fixtures/value-format.native

Run the full local gate with make ci: the committed-binary and index-completeness checks, formatting, clippy and cargo test under default features and --all-features, a clean no-default-features build and the parse example above, cargo doc, seam-probe, string-edge, route-lint, cargo-deny-bans and arch-lint-canonical-encoder. See Makefile for each step.

Run these checks locally while the repository stabilizes. Hosted CI exposes only workflow_dispatch and has a ten-minute job timeout. Pushing commits or opening a pull request does not request CI; hosted execution requires a separate explicit dispatch. Tests fetch the agent-ix/ix-trace-rs Git dependency from its main branch.

CLI arguments are parse|format, source identity, source revision, and file path. parse emits JSON with status parsed; format writes source to stdout and preserves comments/token spellings while normalizing whitespace to LF. Neither command changes a file. Callers must assign the formatted document its appropriate new revision before binding it into evidence. Diagnostics contain original byte, line and Unicode scalar column positions. Exit 0 is success, 1 refusal, 2 usage/I/O failure and 3 resource exhaustion (incomplete). These are local syntax outcomes, not the portable verification result envelope.

The library returns immutable ParsedUnit syntax or a boxed Diagnostic. Source identity/revision are opaque diagnostic labels; they do not implement the future interchange source reference or numeric IR revision mapping. Source::read_verified checks a selected byte digest; parse_source retains that verified immutable source. Source byte spans are half-open; located lines/columns are one-based.

Default ceilings are 1 MiB source, 100,000 tokens, 50,000 syntax nodes and 64 nested delimiters/parser frames. Callers can lower these ceilings. Formatting also bounds output to 1 MiB and can return incomplete if expansion exceeds it. Long flat expressions use an arena; grouping and all original source bytes are retained. Balanced reserved forms refuse as unsupported; malformed tokens and delimiters are syntax errors. No recovery manufactures a successful partial unit.

The source correspondence API checks exact body-to-original segments with explicit layout transformations and returns original document locations. Maps preserve all corresponding byte regions and refuse changed bytes, foreign source bindings, malformed segments and budget exhaustion. Wire decoding and existing-repository extraction remain separate.

mapped::compile carries a verified map and one authored ClauseBinding through the existing parse/link/check/package stages. Its immutable MappedPackage exposes the native package for validation, evaluation and lowering while keeping the original document available for source locations. Failures preserve the native diagnostic or package path; the API does not manufacture source wrappers or change extraction availability. Run cargo test --test it mapped:: for the mapped parent workflow and stage refusals.

With quire-extraction, qsl_source::extract(original, context, selection, limits) from the qsl-source crate calls Quire's actual Rust extractor and returns an ExtractedSource: the verified native body in its document source map, the clause's declared language and Quire's unchanged result. Supply a digest-verified original Source, a loaded Quire SemanticContext (the run command uses qsl_source::clause_context) and a Selection of the authored clause ID, package and body identity. The adapter checks source coordinates and exact bytes, including Quire's omitted final LF on CRLF input, before building the source map. It does not compile. The run command's extraction path (command::extraction) compiles the extracted body with mapped::compile. Both retain Quire's original clause population, availability and diagnostics on success and on refusal. Input is bounded to 1 MiB and 4096 lines before extraction. Extraction cases run with cargo test -p qsl-source --features quire-extraction; the tests show context and selection construction. C's existing-repository CLI/wire adoption remains separate from this working compiler-side Rust integration.

The standalone run command can select Markdown with --features quire-extraction. Its optional program.extraction.body record supplies identity, revision, document and formal_revision for the derived native body; program.source selects the original Markdown bytes and exactly one clause binding selects its heading. This uses a validated clause-only Quire context for the selected package, with no installed archetype schemas. The result's extraction member retains original identity, producer observations and verified byte-map segments; ordinary source, diagnostic and event coordinates refer to the native body.

Generate runnable Markdown fixtures with the existing standalone_fixtures example, then run cargo run --locked --features quire-extraction -- run /tmp/native-workflow/markdown-healthy/request.json. The sibling markdown-violating and markdown-refused requests reproduce false and frame refusal. These requests support source compilation through run; combining them with selected-package execution or compile/lower export refuses explicitly. Default builds reject the extraction field; ordinary native requests are unchanged.

runtime::execute(package, input, selection, limits, poll) now runs native validation and evaluation in one call. The returned report retains the exact package and offered artifacts even on validation failure; truth() returns a Boolean only after completed evaluation. outcome() preserves the original stage diagnostics, measured work and implication events. The existing separate validate and evaluate APIs remain available. Run cargo test --test it runtime_execution:: for aggregate, operation and stopped/retried requests. The standalone quire-spec run <request-file> command now reads selected model/program/runtime files and calls these same APIs. See the runnable workflow for healthy, violating, operation and refused examples, JSON results and exit codes.

Snapshot::read_verified and Invocation::read_verified now read selected native-state-input/1 bytes through closed Serde decoding and the existing structural constructors. They preserve original bytes/digests and refuse stale selections, incompatible envelopes, malformed fields and exhausted budgets. Run cargo test --test it runtime_reading:: for round trips and actual execution of reread inputs. Model-aware validation still occurs during runtime::execute.

The formal source bridge retains exact native source under an explicitly supplied Contract IR source identity. Its forward and reverse mappings check byte, line and scalar-column correspondence, including constructor-valid IR spans whose coordinates disagree with the bytes. Native revision labels remain opaque. This API supplies location correspondence for later checking; the caller owns assigning the formal identity.

Design and status

The requirements index covers LC01–LC05 through discrete Quoin catalog artifacts. These requirements are drafts. The owner adopted specification PR8 for internal LC02 implementation. LC02's test matrix records qualified linking and planned type checking. The new formal linker API owns the exact parsed source and borrows immutable models; CLI parse/format still perform syntax work only. Accepted Contract IR ADR-0054 closes #54 and removes the former Filament-reader prerequisite: generic compilation uses the existing public DeclarationEnvironment/check_expression and executable binder APIs. A concrete archetype projection is specified only for a clause that needs its semantics.

See architecture review for concrete fixes and remaining linking/identity work. The current parser uses declarative Logos tokens and a Pratt expression parser; JSON escapes use serde_json. Binding/lowering will remain modules and use the existing model/IR authorities. No second domain model, backend binder or Markdown expression parser is created here.

New implementation and newly authored implementation fixtures use AGPL-3.0-or-later; dependencies keep their own declared grants. License decision records owner approval and deferred standard-artifact terms. No public release is authorized.

Private tracking: LC01, compiler epic. The shared contracts and LC02–LC05 work are tracked separately, in their own issues.

New tests use the shared ix_trace_rs::trace macro with canonical attributes such as #[trace("TC-156", "FR-059-AC-1")]. Quire's declared grammar binds the IDs; the macro checks argument shape. #[cfg(test)] controls compilation. Read license decision before adding code or normative artifacts. Publication requires a fresh review; do not flip private history public.

Implementation language — owner directive

Executable implementation, including production and qualification tools/tests, is Rust. New TypeScript choices require explicit owner approval; surface all other executable languages. Quoin remains in its current implementation for now: contain its spread through versioned structured interfaces, do not rewrite it wholesale. Filament changes are excluded. See AGENTS.md and the language gate on the owning issue. Normative prose/schema need not be executable Rust.