Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Axioval Engine

Axioval Engine validates federated engineering data without making any source format or geometry kernel its internal model.

The runtime compiles normalized Axioval packages into trusted capability invocations. Source adapters provide semantic objects and evidence. Geometry adapters provide optional exact geometric evidence. Findings retain source identity and provenance.

Why a dedicated IR?

IFC remains an important adapter, but its schema inheritance, STEP identity, file-centric lifetime and serialization history are not suitable as a universal runtime contract. A dedicated IR also admits proprietary CAD, database-backed digital twins, ICDD collections, and future IFCX-style layered compositions.

Current status

The engine is being extracted from the production Solibri compatibility implementation. The migration ledger records what is actually cut over; unchecked entries are not claims of support.

Architecture

Dependency direction

axioval-ir
    ↑
axioval-engine ← axioval-rules
    ↑                 ↑
    ├─ axioval-openbim│
    ├─ axioval-axiolid│
    └─ axioval-icdd   │
          ↑           │
        axioval facade

axioval-ir, axioval-engine, and axioval-rules may not import source formats, federation containers, geometry kernels, or vendor types. Adapters depend inward; core never depends outward.

Execution

  1. A normalized package is deserialized under a deny-unknown-fields contract.
  2. The compiler binds selectors and parameters to trusted capability descriptors.
  3. Compilation produces an immutable ordered execution plan.
  4. An EvidenceSession binds the project to one immutable revision, fingerprint, and optional schema per declared source. Every trusted evidence service must expose its own source snapshots; registration rejects unbound, duplicate, unknown, or non-identical revision/fingerprint/schema bindings.
  5. A run selects that session-bound ProjectView and negotiates required evidence capabilities.
  6. Capabilities evaluate semantic facts and typed evidence.
  7. Findings retain rule, source, object, evidence, precision and diagnostic provenance.
  8. Stable ordering produces reproducible reports.

Project model

A project is a collection of source contributions and links. A view is an immutable interpretation of that collection: one source, a raw federation, or a composed/layered result. The engine does not prescribe how the view was serialized.

Identity is always source-qualified. External IDs such as IFC GlobalId are aliases and never universal primary keys.

Trust boundary

Rule packages contain data, not code. Capability IDs resolve only through an application-created trusted registry. Packages cannot load dynamic libraries, issue network requests, choose file paths, or instantiate arbitrary Rust types.

Geometry boundary

Rules request semantic evidence such as footprints, bounds, intersections, routes or clearances. The evidence provider owns backend handles and reports exactness/provenance. Axiolid is the default adapter but is not part of the public engine IR.

Failure model

Unavailable, unsupported, invalid, budget-exceeded and backend-failure are distinct from false. A rule may only pass when its required evidence is available at the declared exactness.

ADR 0001: Source-neutral engine and independent adapters

  • Status: accepted
  • Date: 2026-08-31

Context

IFC STEP is the current dominant source and ICDD is the current federation container, but IFC5/IFCX may introduce layered composition and other CAD systems must be first-class. Axiolid is an independent geometry organization usable by IFC and non-IFC products.

Decision

The engine owns an immutable source-neutral semantic IR, typed evidence contracts, compilation, execution and findings.

axioval-openbim maps OpenBIM semantics only. axioval-axiolid maps source-neutral geometry requests to Axiolid only. They are peer adapters and may be installed independently. There is no combined OpenBIM-Axiolid adapter.

ICDD contributes sources and links through axioval-icdd; it is not the engine’s project model. Future IFCX adapters can contribute composed/layered views through the same project interfaces.

Consequences

  • Core crates prohibit OpenBIM, IFC, STEP, ICDD, Axiolid and Solibri dependencies.
  • Geometry-free rules run without any geometry adapter.
  • Non-IFC CAD sources can use Axiolid directly.
  • IFC consumers can select another geometry implementation without changing rule policy.
  • Findings use source-qualified opaque object IDs and provenance rather than STEP IDs or IFC GUIDs as universal identity.

Source-neutral IR

Package compatibility

The compiler currently accepts normalized Axioval Schema 0.1.0 packages only. Both definition packages and rulesets are checked before binding; unknown versions fail with UnsupportedSchemaVersion rather than being interpreted as the current contract.

The IR describes what a checker can observe without mirroring any source schema.

Identity

  • ProjectId identifies a validation project.
  • SourceId identifies one contribution.
  • ViewId identifies a stable composition used for a run.
  • ObjectId is opaque and valid only with its SourceId.
  • ObjectRef combines source and object identity.

Adapters may expose external aliases, but aliases never replace source-qualified identity.

Semantic data

Objects expose canonical concepts, typed properties, classifications and directed relationships. Canonical concept IDs are package vocabulary identifiers; source-specific names are adapter bindings. Stored property values are observations, not proof that an omitted key is absent. Conclusive property checks use the typed property-resolution service and exact request-bound evidence.

Values distinguish null/unavailable from concrete values and preserve units where relevant. Adapters must not silently coerce malformed source values.

Views and layers

A project can expose raw source views and composed views. This supports today’s single IFC model and ICDD federation as well as future IFCX-style layers without changing rule capability APIs.

Provenance

Every imported fact and computed evidence can reference its source record, adapter, derivation and precision. Findings carry the provenance needed to explain or reproduce a decision.

Reports

Report keeps conclusive findings separate from not_evaluated outcomes. Every not-evaluated record identifies its rule, optionally identifies the affected object, carries a typed reason, and includes a diagnostic. Runtime ordering is deterministic. An empty findings list is not a pass when not-evaluated outcomes exist.

No source leakage

Core architecture checks reject references to IfcModel, STEP entity handles, ICDD container types, Axiolid meshes, OpenCascade, CGAL, and Solibri types.

Capability model

A capability is trusted executable policy registered by a host application.

Each descriptor declares:

  • stable capability ID and version;
  • execution scope;
  • accepted selector shapes;
  • typed parameter signature and defaults;
  • required semantic/evidence capabilities;
  • result and exactness contract.

Compilation rejects unknown capabilities, duplicate registrations, missing/extra parameters, invalid values and unsatisfied static contracts.

Execution is also fallible. Runtime::run rejects a plan if its runtime registry no longer contains every compiled capability; registry drift can never turn a rule into an implicit pass.

At runtime, missing evidence does not become a pass. CapabilityEvaluation carries conclusive findings separately from object- or rule-level not-evaluated outcomes. The runtime binds every such outcome to the compiled RuleId, sorts it deterministically, and exposes it through Report::not_evaluated(). Reasons distinguish an invalid declaration, a missing service, backend outage, incomplete evidence, invalid evidence, and resource exhaustion.

A capability may return findings and not-evaluated outcomes together when only part of its selected universe was computable. Consumers must not interpret an empty findings list as a pass while not_evaluated is non-empty.

Built-ins

axioval-rules contains reusable, vendor-neutral implementations. Vendor identity, proprietary format handling, localized Solibri text and oracle-only ordering remain adapters in vendor/solibri.

axioval:capability.property-exists, axioval:capability.property-required, axioval:capability.property-value-equals, and axioval:capability.property-predicate resolve values through PropertyResolutionServiceHandle. The integer predicate accepts equal, not_equal, greater_than, greater_or_equal, less_than, and less_or_equal; failed predicates retain exact source evidence. A present value must be bound to the complete request—including its source-qualified object identity—and carry exact reviewable evidence. A missing value is conclusive only when the provider returns exact request-bound CompletePropertyAbsenceEvidence; service absence, partial extraction, cross-object substitution, mismatched responses, or inexact provenance remain not evaluated. Property selectors use the same resolver, so incomplete applicability data cannot silently skip an object. property-exists checks exact presence and intentionally does not reinterpret a present typed value. property-required applies the stronger required-value contract: exact absence, null, or blank text emits an evidence-backed finding, while booleans, integers, finite numbers/quantities, and nonblank text satisfy it. property-value-equals accepts a typed property reference and boolean expected value; a non-boolean resolution is invalid evidence rather than a pass or violation.

axioval:capability.property-comparison currently covers exact property-to-property targets with an independent selector-valued candidate scope, checked/shared/related modes, target-side factors, and each or at_least_one quantifiers. It compares booleans, strings, exact integers, finite decimals, and canonical quantities with matching dimensions. Missing properties emit evidence-backed missing-information findings; incompatible types or unavailable evidence remain not evaluated. Constant targets, count, and sum are deliberately rejected until their oracle fixtures and issue contracts land, so this registration is not a full Solibri parity claim.

axioval:capability.free-floor-circle and axioval:capability.free-floor-rectangle check whether each selected spatial scope can contain an exact supported vertical shape. Circle parameters are diameter_metres and height_metres; rectangle parameters are width_metres, length_metres, and height_metres, all in canonical metres. Each request covers every other project object as a candidate obstacle and requires exact whole-base support on the selected scope with zero hidden gap. A complete exact no-placement proof emits the shape-specific NO_FREE_FLOOR_SPACE_* finding; missing services, backend outages, or invalid/incomplete evidence emit not-evaluated outcomes instead.

Adding a capability

  1. Define or reuse canonical schema concepts and parameters.
  2. Add failing contract and behavior tests.
  3. Implement policy only; put source interpretation in an adapter.
  4. Declare all evidence requirements.
  5. Add deterministic and missing-evidence tests.
  6. Register in the built-in registry.
  7. Record Solibri parity and cutover in the migration ledger when applicable.

Connectivity and routes

axioval-engine owns the deterministic, source-neutral topology contract. It does not prove geometry and does not infer edges from IFC, CAD, ICDD, or vendor relationships.

Complete graph contract

A ConnectivityGraph is built over an explicit universe of source-qualified ObjectId values. Construction requires CompleteTopologyEvidence: exact adapter provenance that every node and candidate transition in the requested scope was assessed. Construction fails when:

  • a node identity is duplicated;
  • a connection references an object outside that universe;
  • an undirected connection is duplicated;
  • an edge is self-referential;
  • its clear width is invalid;
  • edge evidence is approximate or lacks a provenance locator;
  • graph-coverage evidence is incomplete or lacks a provenance locator.

This distinction is intentional: a known isolated object is unreachable, while an unknown object is a TopologyError. Missing input can therefore never become a clean negative result.

Exact edges

Only trusted host code may create VerifiedConnection values. Each edge carries exact adapter evidence and an exact clear width in metres. Source-format relationships can nominate portal candidates, but they are not connection evidence.

A host may independently obtain:

  • semantic candidates and identities from axioval-openbim or a proprietary CAD adapter;
  • aperture, landing, and free-space proofs from axioval-axiolid or another geometry adapter;
  • container/project assembly from axioval-icdd.

The host composes those results before constructing the graph. There is deliberately no axioval-openbim-axiolid adapter or dependency direction.

Determinism

Reachable components are returned in source-qualified identity order. Shortest-hop routing uses deterministic breadth-first traversal; equal-length alternatives select the lexically first path. Every query applies a minimum clear-width threshold without mutating the graph.

Metric geometry paths, portal verification, collision checks, free-space construction, and vertical-connector recognition remain geometry-kernel responsibilities. The engine consumes their typed evidence rather than backend handles.

Metric routing

Metric routing is a typed host service, not an algorithm embedded in the rule engine. MetricRoutingService may be implemented by Axiolid or another trusted geometry backend. OpenBIM may supply semantic route candidates, but it does not own geometry and no combined OpenBIM–Axiolid adapter is required.

Canonical request

A MetricRouteRequest carries:

  • source-qualified, object-grounded origin and destination points;
  • coordinates in canonical metres;
  • a validated mobility profile: radius, clear height, maximum step, and maximum slope.

NaN, infinity, and negative dimensions are rejected before backend execution. MetricRoutingServiceHandle validates that a backend response starts and ends at the requested points. The handle is a concrete type that can be registered in ServiceRegistry and consumed through RuleContext.

Bounded shortest-distance evidence

LengthInterval stores inclusive lower and upper bounds. Exact evidence has equal bounds. Policy comparison is intentionally three-valued:

  • Satisfied: the upper bound meets the maximum;
  • Violated: the lower bound exceeds the maximum;
  • Indeterminate: the interval straddles the threshold.

A known longer route plus an unavailable shortcut can therefore prove route existence, but cannot produce an exact shortest-distance verdict. Raster or tolerance-based backends may return conservative bounds rather than silently upgrading an approximation.

Negative results

MetricRouteOutcome::Blocked requires CompleteMetricEvidence: exact, reviewable provenance that topology and relevant obstacles were complete for the query. BlockedMetricRouteEvidence binds that proof to the complete request, including endpoints and mobility profile; the service handle rejects evidence returned for another request. Missing geometry, partial obstacle composition, unsupported connectors, resource limits, and backend failures return MetricRoutingError; they never become Blocked or a passing rule result.

The engine contract contains no mesh, B-rep, IFC entity, Axiolid kernel, OpenCascade, or vendor type.

Free space and clearance

Free-space computation is a typed host service. The engine owns validated source-neutral requests and evidence; Axiolid or another trusted geometry provider owns rasterization, CSG, collision tests, search, and spatial indexes.

Fixed clearance volumes

ClearanceRequest combines:

  • an object-grounded MetricFrame in canonical metres;
  • orthonormal right, forward, and up directions;
  • a validated box or cylinder;
  • a deterministic source-qualified obstacle candidate set selected by the trusted rule capability.

Semantic filtering stays outside geometry: the provider evaluates exactly the supplied candidate objects. This represents directional component clearance without leaking IFC placements, meshes, B-reps, or kernel types into the engine.

The result is asymmetric:

  • Obstructed needs one exact, non-empty obstruction witness;
  • Clear needs exact and complete obstacle coverage for the request.

Partial geometry therefore cannot produce a false clear result.

PlacementRequest asks whether a box or cylinder can fit in a source-qualified search scope. A PlacementDomain makes the admissible candidate set explicit:

  • Unconstrained preserves generic searches without implying support;

  • Supported requires the whole candidate base on a source-qualified support object within a maximum gap;

  • FrameOffsets limits right/forward/up translation in an anchor frame;

  • SupportedFrameOffsets requires both support and anchor-relative bounds.

  • Found carries one exact, scope-grounded placement frame. Supported domains additionally require exact evidence that the whole candidate base is supported by the requested source-qualified object at that exact frame and within the requested gap.

  • NoPlacement requires complete exact search evidence.

A bounded or partial search cannot claim that no placement exists. Connected corridor requirements use metric routing with an appropriate mobility profile rather than inventing a second path contract.

Free-area bounds

FreeAreaRequest measures accessible area for a scope and mobility profile. AreaInterval stores conservative square-metre bounds. Minimum-area comparisons are three-valued:

  • the lower bound meets the minimum: satisfied;
  • the upper bound is below the minimum: violated;
  • bounds straddle the minimum: indeterminate.

Runtime boundary

FreeSpaceServiceHandle is registered in ServiceRegistry. It validates that every response is bound to the exact request. Missing geometry, unsupported composition, resource limits, and incomplete evidence return FreeSpaceError; none become clear, no-placement, or passing results.

The contract contains no IFC, STEP, ICDD, Axiolid, OpenCascade, CGAL, or vendor-specific type.

Walkability topology

WalkabilityService converts a complete geometry scene into a source-neutral graph of derived walkable regions. Axiolid or another trusted geometry backend owns free-space extraction, obstacle subtraction, portal verification, and region decomposition.

The request supplies deterministic source-qualified sets of:

  • walkable surface objects;
  • entrance or portal objects;
  • obstacle objects;
  • the required clear width and optional elevation band;
  • verified-portal and moving-envelope policy.

Semantic selectors run before this service. IFC placements, meshes, B-reps, and native kernel types never enter the request.

Snapshot guarantees

A WalkabilitySnapshot is accepted only when it carries complete exact provenance. Every passage must have exact reviewable evidence, declared endpoints, and a conservative clear-width interval. Duplicate passages, unrequested object mappings, and portals outside the request policy are rejected.

Object-to-region membership lets reusable capabilities ask whether selected spaces, entrances, or components share traversable free space without exposing backend cells as model objects.

Three-valued routes

For the request minimum width, the engine evaluates two deterministic graphs:

  1. definite graph: passage lower bound meets the width;
  2. possible graph: passage upper bound meets the width.

A route in the definite graph is Reachable. No route in the possible graph is Unreachable. A route only in the possible graph is Indeterminate. Approximate width evidence therefore cannot become a pass or a false negative.

Corridor metric lengths remain owned by the separate metric-routing service. End-clearance placement remains owned by the free-space placement service.

Typed host services

The engine passes a RuleContext containing the immutable project view and a type-indexed ServiceRegistry to trusted capabilities. Applications register semantic or computational services explicitly; duplicate concrete service types are rejected instead of silently replacing an implementation.

Adapter crates are peers:

  • OpenBIM implementations can provide semantic/property/relationship services.
  • Axiolid implementations can provide geometry services for IFC, proprietary CAD, or any source able to lower geometry into Axiolid.
  • ICDD implementations can provide project assembly and cross-document link services.
  • Alternate geometry backends register the same source-neutral service interfaces.

Rule packages cannot register services and cannot supply executable code. Missing required services must produce an explicit not-evaluated/backend-unavailable outcome, never a pass.

Property resolution is exposed through PropertyResolutionServiceHandle. A present response is a ResolvedProperty bound to the complete PropertyRequest, including the source-qualified object identity and property key; absence requires equivalent exact request-bound evidence. The handle rejects cross-object substitution, mismatched property keys, absent provenance, approximate values, non-finite numerics, and non-reviewable absence claims. Built-in property capabilities and property-based selectors require this service rather than treating a missing entry in an object map as proof of absence.

Relationship-based comparison candidates are exposed through RelationshipSelectionServiceHandle. A request binds the checked object, the complete selector-derived candidate universe, and either a shared-group or directional traversal query. Successful responses must stay inside that universe, use canonical unique object IDs and evidence, and prove exact completeness. Source adapters interpret native containment, hosting, and relationship structures; the engine does not read Object.relationships as authoritative source semantics.

Metric routing is exposed as MetricRoutingServiceHandle. The concrete handle wraps a backend-neutral trait object so it remains type-indexable in ServiceRegistry. Engine capabilities consume validated metric requests and bounded evidence; adapters keep native mesh and B-rep types behind the service.

Free-space area, fixed directional clearance, and constrained placement search are exposed through FreeSpaceServiceHandle. The handle enforces exact request binding and preserves asymmetric proof requirements: one obstruction or placement witness may be sufficient, while clear and no-placement verdicts require complete evidence. Placement domains distinguish unrestricted, support-grounded, and anchor-frame offset searches. Supported found witnesses require exact whole-base support evidence bound to the requested object, found frame, and maximum gap. See Free space and clearance.

Walkable-region topology is exposed through WalkabilityServiceHandle. A trusted geometry backend supplies a complete exact snapshot; engine routing distinguishes definite-width, impossible, and uncertain-width paths without importing backend cells or geometry. See Walkability topology.

Independent adapters

Adapters are peers around the source-neutral engine. No adapter receives special privileges.

OpenBIM

axioval-openbim provides a production IFC4 STEP path for exact direct properties: strict bytes become a SHA-256 fingerprinted EvidenceSession; IFC objects become source-qualified Axioval objects; and ifc-properties::exact_property backs the session’s property service with occurrence/type provenance and exact absence. The property resolver owns and declares the same source/revision/fingerprint/schema snapshot registered by the session; mismatched service composition is rejected. Parser diagnostics, unsupported schemas, malformed traversal, conflicts, and unsupported values fail closed.

Direct-property completeness does not imply relationship completeness. The IFC session deliberately registers no relationship-selection service yet. The adapter does not depend on Axiolid and does not own geometry policy.

Axiolid

axioval-axiolid supplies geometry evidence for any source capable of exposing Axiolid-compatible geometry handles. A proprietary CAD adapter can use it directly without importing OpenBIM or IFC.

ICDD

axioval-icdd opens an ICDD package, dispatches member payloads to registered source decoders, maps linksets, and assembles a project. ICDD serialization types do not cross into the engine IR.

Alternate geometry kernels

An OpenCascade or CGAL adapter may implement the same evidence traits in an external crate. Native/FFI code is never enabled by the default pure-Rust distribution.

Conformance

Every source adapter must prove source-qualified identity, deterministic enumeration, provenance and strict malformed-data behavior. Every geometry adapter must prove exactness reporting, backend-failure propagation, transform/unit handling and cache isolation.

Migration from Solibri

A box is checked only when the Axioval implementation is the production owner, Solibri consumes it, and parity evidence passes.

Current capability waves

  • Property comparison: the bounded published 0.1.0 slice is consumed by Solibri and recorded in the machine ledger as in_progress; unsupported operators and modes remain outside the cutover.
  • Required property: axioval:capability.property-required is published in the 0.1.1 facade and tested in the engine. It is deliberately not marked migrated until Solibri’s production checker executes it with exact source evidence.

Shared runtime

  • Normalized package contract and strict binder
  • Capability registry/compiler
  • Deterministic runtime/reporting
  • Source/evidence sessions and caches
  • Selection engine and quantifiers
  • Pairwise/spatial engine
  • Circulation/path/free-space graph
  • Exact recognizers
  • Typed property sources

Capability families

  • Information and property
  • Relationship and assignment
  • Space and topology
  • Spatial clearance/distance
  • Building
  • Accessibility
  • Life safety
  • Federation and comparison

Host rewiring

  • spec normalizes to Axioval contracts
  • checker executes Axioval plans
  • CLI and Python use Axioval reports
  • IFC parsing/modeling uses openbimrs/ifc
  • Geometry evidence uses axioval-axiolid
  • ICDD uses openbimrs/icdd plus axioval-icdd
  • BCF/report adapters consume generic findings
  • Duplicate engine/model/geometry ownership removed

Required evidence per row

Record the Axioval tests, Solibri tests, oracle corpus, discrepancy count, performance measurement, cutover commit and rollback switch. Unsupported behavior remains unchecked and documented; it is never represented by an empty module or unconditional success.

Solibri compatibility migration

migration/solibri-capabilities.json is the machine-readable source of truth for cutover status. It records all 65 source runtime entries from the pinned Solibri commit and requires five independent proofs before an entry may be marked ported.

Completion means

  1. A source-neutral capability implementation exists in axioval-rules.
  2. Tests exercise that implementation without IFC or Solibri types.
  3. Solibri translates its inputs into Axioval IR/evidence and calls the Axioval capability.
  4. Result and oracle parity tests pass.
  5. The Solibri copy no longer owns the rule policy.

Compilation, a facade wrapper, or a migration checkbox without those proofs is not a completed port.

Order

Shared prerequisites are migrated before families:

  1. project/source identity, typed properties and provenance;
  2. complete graph/path/free-space systems;
  3. exact recognizers;
  4. pairwise and geometry evidence;
  5. individual information, relationship, space, building, spatial, accessibility, life-safety and federation capabilities.

Legacy Solibri runtime-fidelity labels are retained as source metadata. They neither promote nor block an Axioval entry automatically.

Contributing

See the repository contributor guide.

The shortest acceptable loop is RED–GREEN–REFACTOR followed by ./scripts/check.sh. Architecture-boundary changes require an ADR or an architecture-document update and a test that proves the forbidden dependency gate can fail.

Use scoped Conventional Commits on linear main. Keep logical changes atomic so git revert is a safe rollback mechanism.

Before a release, commit the candidate and run ./scripts/package.sh. It packages and verifies every workspace crate through Cargo’s temporary local registry, including unpublished intra-workspace dependencies.

Security

See the security policy for private reporting.

The primary application-security invariant is that rule packages are untrusted data. They cannot execute code, select arbitrary filesystem paths, issue network requests, or load native libraries. Only capabilities registered by the host application may run.

Adapters must bound input sizes, recursion, graph traversal, decompression, geometry work and report volume. Resource exhaustion is an explicit run outcome rather than a process crash or silent partial pass.

Dependency policy is enforced by cargo-deny: known advisories, unapproved licenses, wildcard requirements, unknown registries and unknown Git sources fail the gate. GitHub Actions use immutable commit SHAs, and downloaded documentation tooling is checksum-verified before execution.

Rust API

Generated rustdoc is deployed under this book: