RFD 0002 — #[comptime] attribute

• State: discussion
• Opened: 2026-05-27
• Decides: surface syntax and semantics of compile-time evaluation in Argon. Affects oxc-parser (attribute recognition), oxc-instantiate (compile-time lifting), oxc-reasoning (the engine, run at build time on a subset of rules), oxc-oxbin (materialized fact storage), and diagnostic codes OE1307/OE1308.

Question

Argon’s reasoner can evaluate rules at runtime (the keystone path) or at compile time (when all inputs are statically known). The compile-time path is strictly faster: facts get materialized into the .oxbin at build time and shipped as data, eliminating runtime evaluation for that rule entirely. When and how should the modeler opt in to compile-time evaluation? What does it mean per rule mode? What’s the auto-vs-explicit story?

Context

Why compile-time evaluation matters

Argon’s central thesis is the reasoner IS the data system. The same engine that derives adult(p) at query time can derive adult(p) at build time — if its inputs (Person(p), hasAge(p, n)) are statically known. Materializing the derivation at build time gives:

1. Runtime queries see literal facts, not derivations. Faster, simpler query path.
2. The .oxbin ships the closed-world extent. Downstream consumers (other compilation units, runtime, federation peers) don’t re-derive.
3. Compile-time errors for impossible derivations. A check rule that fails at build time is a build error, not a runtime exception.
4. A natural staging surface. Modelers can mark which derivations are “decided at build” vs “decided at runtime” — explicit control over the deployment-time computational tier.

What “compile-time” means here

The reasoner has two distinct invocation points:

• Runtime mode — Engine instantiated inside oxc-runtime::Store; rules evaluate against live event state; result is queried via Store::query_derive.
• Compile-time mode — same Engine, instantiated inside oxc-instantiate during .oxbin lowering; rules evaluate against the source’s declarative facts (iof_assertion events from insert operations in mutations declared inside the workspace); result is emitted into the .oxbin’s events section as fresh axiom events (with derivation provenance pointing to the comptime rule).

The “engine is the engine” property holds: same code, same semantics, different invocation context.

What’s a “static input”?

A predicate is statically known at build time if its extent is fully determined by:

• Axioms declared in source code (pub kind, pub rel, pub mutate invocations baked into module initialization).
• Outputs of other comptime-eligible rules (the comptime fixpoint propagates).

A predicate is runtime-bound if any contributing fact comes from:

• Caller-invoked mutations (user runs register(...) against a running Store).
• External federation peers.
• Network/IO sources.

Today’s MVP only has declarative axioms — everything is statically known. But the distinction is structural, not implementation-momentary.

Decision

Attribute surface

#[comptime]
pub derive adult(p) :- Person(p), hasAge(p, n), n >= 18;

The #[comptime] attribute applies to a single declaration. Binary form in v1 — no arguments. Argument form is parser-reserved for v2 (see Open Questions).

Per-mode semantics

Auto-lifting

The compiler automatically lifts any rule (regardless of #[comptime]) whose body predicates are all statically known and whose result fits within the declared comptime budget. The lift is transparent — produces the same axiom events as if the rule had been declared #[comptime].

#[comptime] is therefore a promise (“this rule MUST be evaluable at build time”), not just an enable. If the modeler declares #[comptime] on a rule whose body references a runtime-only predicate, the build fails with OE1307 ComptimeNotStatic.

This makes #[comptime] checkable: it’s a verification that a property holds, not just a performance hint.

Diagnostic codes

• OE1307 ComptimeNotStatic — rule declared #[comptime] depends on runtime state (a mutation-bound predicate, a federation-bound predicate, or an indirect dependency through another runtime-only rule).
• OE1308 ComptimeForbiddenOnMutate — #[comptime] applied to a mutate declaration.
• OE0227 AttributeArgsNotYetImplemented (existing) — #[comptime(...)] with any arguments emits this; arg-form is parser-reserved for v2.

Materialization output

A #[comptime] derive p(x) :- A(x), B(x) rule produces, at build time:

1. The derivation: every tuple in p’s extent emitted as an iof_assertion or relation_tuple axiom event.
2. The provenance: each emitted event carries derivation set to the rule’s AxiomKey (per RFD 0001) so retraction propagates correctly.
3. A comptime_lifted: bool field in RuleDeclBody indicating “this rule’s facts are pre-materialized; runtime evaluators may skip it.” (Adds 1 byte to RuleDeclBody.)

Reasoning about freshness

If the source code changes such that a comptime-lifted rule’s inputs change, the .oxbin is rebuilt and the materialized facts are recomputed. The Salsa-style incremental compilation layer (book §18.2) treats comptime_lifted rules as memoization targets — their inputs are tracked, and only changed-input rules re-materialize.

Rationale

Why per-mode semantics, not uniform

The five rule modes (fn / derive / query / mutate / check) have genuinely different meanings, and “compile-time” means something different for each:

• derive produces facts → comptime means baking those facts into the artifact.
• query produces a result value → comptime means embedding that value.
• check produces a verdict → comptime means asserting at build time.
• fn is a function call → comptime means const-evaluation in the Rust/C++ tradition.
• mutate mutates state → comptime makes no sense; mutations are by definition runtime.

A single uniform “evaluate at build time” semantics would erase these distinctions. The mode-aware semantics match the modeler’s mental model.

Why auto-lift + explicit attribute (not just one)

Auto-lift alone risks silent performance cliffs: the modeler doesn’t know whether a rule is being materialized or runtime-evaluated. Adding a runtime-only predicate elsewhere could silently degrade performance.

Explicit-only would force the modeler to annotate every rule, even the obvious cases.

Auto-lift plus #[comptime] as a checked promise gives both: most rules auto-lift transparently; the modeler can opt-in to “this MUST be comptime” for ones where the property matters. Same pattern as Rust’s const fn — the compiler can evaluate any expression at compile time when possible, but const fn is the promise that this function is callable in const context.

Why argument-form is reserved, not implemented in v1

Four argument variants we expect to want:

• #[comptime(strict)] — fail build if auto-lift can’t reduce all inputs (stronger than the default OE1307 — even runtime-derivable-but-not-yet-evaluated counts as failure).
• #[comptime(profile)] — emit a build-time report of cost/cardinality for this rule.
• #[comptime(embed)] — for query mode: embed the result inline in source as a literal, not just in the .oxbin (useful for let X: extent = query foo inside a fn).
• #[comptime(lazy)] — comptime-eligible but defer materialization until first runtime access (useful for very-large extents).

None of these are necessary in v1. We commit the parser-level syntax (#[comptime(...)] parses without error) but emit OE0227 on any non-empty arg list. This lets us add the arg-form in v2 without changing parser surface.

Why OE1307 distinguishes “comptime-eligible but not yet evaluated” from “comptime-impossible”

A comptime rule depending on another rule that’s itself comptime-eligible but not yet processed should propagate up the comptime fixpoint, not fail. The build’s job is to find the comptime fixpoint over the rule graph; only rules that hit a runtime-only predicate or a cycle (that can’t be broken by other comptime rules) fail with OE1307.

Why mutate is forbidden, not silently no-op

Mutations modify state. State at compile time is the static fact base; “running” a mutation against it would change what’s baked into the artifact, which violates the closed-world property (the .oxbin’s facts are what the modeler wrote, plus what derivations they declared). Allowing #[comptime] mutate ... would either:

• Silently no-op (confusing — modeler thinks something happened).
• Modify the build’s fact base (dangerous — implicit data mutation hidden in code).

Better to forbid loudly via OE1308.

Alternatives considered

Alt 1: No comptime at all — everything is runtime

The status quo. All rules evaluate at runtime; the .oxbin carries only declared facts plus rule definitions.

Rejected: gives up the major performance win of build-time materialization. Loses the natural “compile-time assertion” surface for check rules. Forces every cross-cutting query to pay runtime evaluation cost.

Alt 2: Implicit only — no attribute, just auto-lift

Every rule the compiler can prove statically-decidable is auto-materialized. No modeler annotation.

Rejected: silent performance cliffs as discussed. Loses the “this MUST hold” checkable property. Loses the natural place to thread future args (strict/profile/lazy).

Alt 3: Explicit only — every comptime rule must be annotated

No auto-lift; only #[comptime] rules are materialized at build.

Rejected: forces annotation noise on the obvious cases. Modelers will either over-annotate (defensive #[comptime] everywhere) or under-annotate (missing perf wins). Loses the simplicity of “the compiler does the right thing by default.”

Alt 4: #[const] instead of #[comptime]

Borrow Rust’s terminology for symmetry.

Rejected: “const” connotes value-level immutability in Rust, which is a different concept from “evaluated at build time.” Argon’s facts are already immutable once asserted; the relevant axis is when they’re asserted (build vs runtime), not whether they’re mutable. comptime is clearer.

Alt 5: Zig-style comptime (full compile-time computation)

Zig’s comptime does general compile-time evaluation including type-level computation. Argon could expose the same generality.

Rejected as the v1 design. Zig’s comptime is a much larger surface — it includes generic instantiation, type erasure decisions, and runtime/compile-time polymorphism. Argon’s #[comptime] is scoped to the substrate’s reasoning capability: which rules get materialized. Generalizing to Zig-shape comptime is interesting future work, but it’s a different feature.

Consequences

Wire format

RuleDeclBody gains a comptime_lifted: bool field. 1 byte added per rule decl. Negligible.

Build performance

Comptime-eligible rules add to build time (the engine runs at build). Trade-off: build is slower; runtime is faster + simpler. For workloads where the .oxbin is built once and queried many times, this is strictly positive. For dev-loop scenarios (rebuild frequently), Salsa-style incremental compilation memoizes most of the work.

Diagnostic surface

Two new emission sites (OE1307, OE1308 — already reserved in grammar.toml from the earlier diagnostic landing). The parser keeps the existing OE0227 for non-empty arg form.

Code volume

Modest:

• Parser change: ~10 lines to recognize #[comptime] attribute on declarations.
• oxc-instantiate change: build-time engine invocation for comptime-eligible rules, comptime fixpoint analysis, OE1307 emission. ~200-300 LOC.
• oxc-oxbin change: emit derivation events from comptime rules into the events section. ~50 LOC.
• RuleDeclBody schema: comptime_lifted field. ~5 LOC.

Determinism preserved

Comptime evaluation produces the same axiom events from the same source — the engine is deterministic, and the inputs are entirely from source. Byte-identical .oxbin guaranteed (per RFD 0001).

Open questions

• The argument form in v2 — #[comptime(strict|profile|embed|lazy)]. Specific semantics deferred to a follow-up RFD when we have benchmarking to validate the tradeoffs. The parser-level syntax stays reserved.

• Comptime budget — should there be a soft limit on how much work a comptime rule can do (e.g., “evaluate up to N facts; if exceeded, emit a warning and fall back to runtime”)? Useful for guarding against accidentally exponential comptime work. Likely yes, with a default of 10M facts and a CLI/config override.

• Comptime + standpoint federation — when standpoint A imports from standpoint B and B has comptime-lifted rules, A sees B’s materialized facts. But if A re-evaluates a derived predicate against its own facts plus B’s, does the comptime materialization compose correctly under the FDE info-join? Likely yes (it’s just facts), but worth a separate verification when standpoint federation is mechanized in the Lean.

• Interaction with retraction — a comptime-materialized rule’s derived facts have a derivation lineage. If a contributing axiom is retracted at runtime (via delete operation), the derived facts must also be retracted. The retraction propagation needs to traverse the derivation graph. Architectural: yes; implementation: needs the Phase-4-style dense provenance index from RFD 0001 to be efficient.

• Comptime + temporal — for rules with explicit temporal qualifiers (at(t), during(...)), does comptime still make sense? The rule’s truth depends on t. Probably comptime should be allowed only when temporal qualifiers are themselves static (e.g., literal timestamps), and emit a diagnostic when they’re symbolic. Defer to the temporal-substrate work track.