ReadonlybridgesSanctioned cross-graph dependency declarations. Empty under
single-graph IR documents (the common case); populated by a
future cross-graph aggregator. EPIC-2's CrossGraphRead pass
refuses any cross-graph dep not in this list.
ReadonlycommitsOptional commit log, capped by host caller. The checker uses this for replay-based determinism checks.
ReadonlyeventsLifecycle event stream — the closed six-arm discriminated union
EPIC-2's lint passes consume. PR-B1 widens this from PR-A's
readonly never[] placeholder; the engine drains its subscriber
registry, disposal tombstones, tx-set log, and read-trace map
into the array at exportModel() time.
ReadonlynodesSnapshot of every registered node at export time.
Optional ReadonlyreadsWhether the IR's read-set capture was truncated during
serialisation. Per the EPIC-1 brutal-critical review's
recommendation #4 (#584 A17-4): when the exporter caps a
derived's IRRead summary at the K=256 retention bound,
downstream consumers (the checker, the bounded enumerator,
SARIF dashboards) need to know they're reasoning over a
partial picture. A false here is the load-bearing
"no truncation occurred — every read of every derived is
preserved" claim; a true is the honest acknowledgement
that the checker may emit false negatives on rows whose
proof requires reads past the cap.
Defaults to false when omitted (older IR documents and
adopters that construct CauslModel by hand are treated as
complete).
ReadonlyschemaSchema version pinned to CAUSL_MODEL_SCHEMA.
ReadonlyscopesLifecycle scopes referenced by IRSubscribe.scopeId,
IRUnsubscribe.scopeId, and IRDispose.scopeId. The exporter
always emits at least one default scope per graph
({ id: 'g.<graphId>:default', kind: 'infinite', ... }) so every
scopeId resolves. Adopters that need finer scoping pass an
explicit scope option to subscribe(); PR-B1 reserves the wire
shape and a future PR adds the option.
ReadonlytimeEngine GraphTime at export time.
Top-level IR document produced by
graph.exportModel().Remarks
Realises the engine's contract with the bounded model checker: property-based fuzz alone is statistical, so the engine emits this snapshot for an exhaustive bounded enumeration that aims to lift runtime-detection rows (stale-async, dynamic-dependency cleanup, cycle reachability) into compile-time-equivalent CI gates. Hosts cap the commit log via ExportModelOptions to bound checker workload — the same trade
kaniandloommake: out-of-bounds programs (more nodes, more commits, longer message chains than the configured bounds) are not proven by the checker and rely on the property-based fuzz suite plus runtime guards.The shape is closed at two
kindconstants by construction (iasbuilt/causl#359). What used to be optionalresources,conflicts, andmsgsarrays — each carrying its ownkinddiscriminator — was the eleven-NodeKindtaxonomy §4 spent its budget collapsing. Resource state is already an Input value; conflicts are a derived view over an Input map; the Msg union is an application-checker concern. Adapter packages that need richer model state run their own projector against a publicGraphview and emit a sibling document that the checker reads alongside the engine IR — they do not extendCauslModel.