The store

Engine, Module, Store

Loading splits into three objects with distinct ownership.

Engine   the shared, immutable schema; one per process
  Module   one loaded .oxbin: concepts, relations, rules, seed facts; immutable; shared by many stores
    Store    one execution context: the live, mutable set of facts; answers queries, takes mutations

The split between an immutable Module and a mutable Store is what makes many isolated contexts cheap: thousands of stores share one loaded schema, each with its own facts. A query reads a store; a mutate writes one; the module underneath them never changes.

The store is an append-only log

The storage layer has no mutable tables. The whole database is one append-only log of axiom events. A schema declaration, a fact assertion, a retraction — each is a new row, and rows are never edited in place. A retraction closes a row’s time window rather than deleting it; physical erasure happens only through the capability-gated forget operation.

There are 26 kinds of axiom event. The catalog is ontology-neutral — a foundational ontology like UFO contributes zero variants, because its meta-properties are ordinary meta_property events whose body names an axis, target, and value — and the Lean inductive is its canonical source. Each row carries its kind and body, the standpoint and module it belongs to, its valid- and transaction-time ranges, a polarity, its tier, and its provenance. So when a mutate body runs insert iof(p, Person), nothing updates a “persons” table: the runtime appends an instance-of assertion. Asking for the current persons replays the log and keeps the rows live now. The reference fixes the storage model under the storage layer.

Two clocks

Every event carries two independent times, and the log is what makes both queryable.

• Transaction time — when the system recorded a fact. “We entered the lease on March 3; we corrected the rent on April 9.”
• Valid time — when the fact is true in the world. “The lease runs January through December.”

Because the two are independent, a query reads along either. Reading at a past transaction time answers what did we believe then; reading at a past valid time answers how was the world then. A query carries the coordinate with as_of: a transaction stamp pins the read to a past belief state, a date pins it to a past state of the world. After a scenario hires someone as a minor and later corrects their age, the same adults query returns nothing at the early transaction stamp and the now-adult individual at the later one — the read snapshot moved past the correction. Argon by Example carries the worked bitemporal programs, temporal_promotion over transaction time and effective_dated_tax_v0 over valid time. Retroactive correction and “as we knew it then” audits are native to the log, not bolted on as history tables.