Axiom-ADT variant catalog
The canonical axiom_events table (The single-event-log architecture) carries one of 27 axiom-kind variants. Each variant has a stable string tag (the axiom_kind column value) and a canonical-CBOR body shape (the body BYTEA payload).
The catalog is ontology-neutral. UFO contributes zero variants; UFO-specific meta-properties (rigidity, sortality, identity-provision) are meta_property events whose body declares (axis, target, value). Other vocabulary packages (BFO, DOLCE, MLT) contribute zero variants on the same principle.
The variants mirror Argon’s CoreIR 1:1. The canonical source is the Lean inductive Argon/Storage/AxiomKind.lean (variant set and order) and Argon/Storage/AxiomBody.lean (per-variant body shapes); the Rust mirror is oxc-protocol::storage::AxiomKind, pinned against drift by oxc-protocol/tests/drift.rs. When CoreIR shakes during compiler development, the Lean drives and this catalog follows. For the exact CBOR field shape of any variant, read AxiomBody.lean — it is authoritative; the body shapes are not reproduced here.
The 27 variants
Tag (axiom_kind) | Group | Notes |
|---|---|---|
concept_decl | Declarations (11) | Ontology-neutral; UFO axes via meta_property |
relation_decl | is_iof / is_subsumption flags identify privileged relations | |
struct_decl | ADT-product type | |
enum_decl | ADT-sum type | |
metaxis_decl | A meta-axis exists; vocab packages ship their axes here | |
metatype_decl | Bundles axis-value commitments for a concept-introducer | |
metarel_decl | Structural mirror of metatype_decl, for relations | |
standpoint_decl | Multi-parent DAG; rigidity per node | |
module_decl | Carries the composition signature (Composition signature) | |
trait_decl | Trait surface | |
impl_decl | Conditional impls supported | |
iof_assertion | Assertions (7) | “individual is an instance of concept”; bitemporal-aware |
iof_refutation | Strong (classical) negation of an iof_assertion (RFD 0010); maps to Truth4::Not at federation; same body as iof_assertion | |
relation_tuple | n-ary relation tuple; literal codomains allowed | |
relation_tuple_refutation | Strong-negation counterpart of relation_tuple (RFD 0010); same body as relation_tuple | |
property_assertion | Literal-valued specialization of relation_tuple; declared-symbol carrier | |
individual_property_assertion | Per-instance mut-field set (RFD 0006); per-instance IndividualId carrier | |
meta_property | Vocab-specific axis values land here, not in catalog columns | |
subsumption_axiom | Axioms (2) | sub <: super edge; multi-parent via multiple events |
partition_axiom | Vocab-neutral cover; MLT’s partitions(T) lowers onto this | |
rule_decl | Rule-modes (4) | Unifies fn / derive / query / mutate / check via a rule_mode field |
query_decl | Distinct from rule_decl to index queries; query-specific attrs (group_by, order_by, limit, offset) | |
mutation_decl | Named pub mutate; operations include forget (capability-gated, Capability surface) | |
compute_decl | Inline-compute (tier: recursive by definition) | |
bridge_decl | Federation (1) | Bridge rules bridge rule — directional inference between standpoints; added in δ.2 |
test_decl | Tests (1) | testing / The test atom — ox test in-language unit test (RFD 0048); body is a mutate-body Vec<Operation> plus Operation::Assert, run by ox test. Inert at query/serve time — carries no rule-mode semantics |
relation_tuple_amendment | Markers (1) | Belief-time-amendment marker (amend, RFD 0076): names the relation tuple withdrawn as false ab initio. Asserts no fact — no read or materializer consults it — but the freeze fold subtracts a marked tuple from the freeze witness. Body shape mirrors relation_tuple |
Total: 27. The body encoding is canonical CBOR (deterministic per RFC 8949 §4.2.1); content_id = SHA-256(body), so identical bodies deduplicate. UUIDs encode as bytes(16). The per-variant body maps are specified in Argon/Storage/AxiomBody.lean.
The set is MVP-final but not closure-locked. Additive variant additions bump core_ir_version minor; breaking changes bump major. Semantics-ACTIVATION of a variant already in this table — a producer beginning to emit an event kind it never emitted, which a runtime gate then depends on — is itself a major event, not a minor one: a reader predating the activation already recognizes the kind, so it decodes the artifact cleanly and skips the event as it always did, executing with the new gate silently absent. The worked case and the version arithmetic are recorded at CURRENT_CORE_IR_VERSION in compiler/crates/oxc-oxbin/src/versioning.rs.
A .oxbin reader that encounters an unknown axiom_kind in the events section MUST report OE1220 UnknownAxiomKind(kind) and refuse the load — unless the artifact is lenient-validated (The OxbinRuntime trait surface), in which case the unknown events are dropped from the in-memory representation but kept on disk. Strict runtimes always fail.