Time-travel: a refinement’s verdict changes over time

Area: Bitemporal time Teaches: how an iff-refinement composes with bitemporal time-travel — as a field rises across transaction-time, the individual’s membership in the refinement changes per snapshot. The classifier is re-run against the field value as of each instant. Prerequisites: as_of time-travel, and refinement (iff). Run: ox build examples/temporal_promotion && ox run-scenario examples/temporal_promotion

In temporal_as_of_surface the query moved through time. Here the classification moves: an employee crosses a threshold, and the refinement that depends on that field flips from non-member to member — but only for snapshots taken after the crossing.

What to read in hr.ar

FullTime is the iff-refinement over an employee’s weekly hours:

pub type Employee { mut weekly_hours: Int }
pub type FullTime <: Employee iff { self.weekly_hours >= 35 };

pub query all_employees() -> Employee;
pub query full_timers()   -> FullTime;

There is no as_of on these declared queries; the time-travel here is driven by the --as-of flag on ox query, which reads the FullTime extent visible at a chosen transaction-time.

Running it

The demo.toml scenario hires alice at 20 hours/week (below the threshold), then promotes her to 40. The latest snapshot has her full-time:

$ ox run-scenario examples/temporal_promotion
query hr::all_employees: 1 row(s)  alice
query hr::full_timers:   1 row(s)  alice      — 40 >= 35 in the latest state

Travel back, and the verdict flips. The same FullTime extent, read at different transaction-times:

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 1
extent(hr::FullTime as_of 1): 0 individual(s)             — alice still at 20h, not FullTime

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 100
extent(hr::FullTime as_of 100): 1 individual(s)  alice    — past the promotion, 40 >= 35

The decisive contrast is --as-of 1 vs --as-of 100: one individual, one refinement, two snapshots — empty before the promotion, {alice} after. The field value is read as of the same instant the membership is evaluated (the latest property assertion with tx_from <= tx wins per field), so the iff classifier sees 20 in the past and 40 in the present.

Honest caveats (what runs today)

• --as-of takes a transaction-time stamp as an integer. A stamp before any event (--as-of 1) reads the pre-promotion state; a large stamp (--as-of 100) reads the latest.
• The --as-of flag lives on ox query; ox run-scenario prints the latest snapshot for the declared queries.

This example is compiled and run in CI; the corpus test (oxc-runtime/tests/examples_corpus.rs::corpus_temporal_promotion_full_time_eligibility_changes_over_time) pins exactly this — the FullTime extent differing across transaction-time as the hours rise — so the refinement-over-time composition can’t drift.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Bitemporal time-travel queries.

mod hr;

hr.ar

//! Bitemporal time-travel queries.
//!
//! An employee's eligible status changes as their hours go up over
//! time. The refinement `FullTime <: Employee iff { hours >= 35 }`
//! evaluates per-snapshot.
//!
//! Demonstrates:
//!   * Bitemporal substrate: every mutation-emitted event gets a
//!     monotonic transaction-time stamp
//!   * Time-travel queries: `Store::query_extent_as_of(tx)` returns
//!     the extent visible at a given transaction-time
//!   * Refinement composition with bitemporal: field values are
//!     read AS OF the same instant (latest property assertion
//!     with `tx_from <= tx_nanos` wins per field)
//!
//! Expected runtime behavior:
//!   * After hire(alice, 20): `FullTime` extent = {}     (alice at 20h)
//!   * After update(alice, 40): `FullTime` extent = {alice}
//!   * Time-travel: `query_extent_as_of(t_before_update)` returns {}
//!   * Time-travel: `query_extent_as_of(t_after_update)` returns {alice}

pub type Employee {
    mut weekly_hours: Int,
}

pub type FullTime <: Employee iff { self.weekly_hours >= 35 };

pub mutate hire(p: Employee, hours: Int) {
    insert iof(p, Employee);
    update p: Employee set { weekly_hours = hours }
}

pub mutate promote(p: Employee, hours: Int) {
    update p: Employee set { weekly_hours = hours }
}

pub query all_employees() -> Employee;
pub query full_timers() -> FullTime;