From the third rewrite review (line references originally at rewrite 75c79c3).
The durable contract says live reduction and journal replay validate the same transition relation. They currently do not.
1. Replay is stricter than live
journal.rs rejects incomplete MediaObserved values that live command paths accept and journal. A live-accepted/replay-rejected delta can make the next startup report corruption and discard a valid tail.
Completeness validation currently lives partly in engine call-site guards. Put one predicate at the core mutation boundary and share it with replay so an invalid durable delta is unrepresentable.
The old second example involving empty HistoryImported keys is removed by #79 along with HistoryImported/parked state. Replace it with validation of the native HistoryRecord contract:
- non-empty opaque ID;
- valid
HistoricalFile::Path or non-empty anonymous identifier;
- fixed-point/range-valid optional measurements;
- outcome-specific internal consistency;
- unknown fields absent, not zero-filled.
Import validation and native terminal materialization must use the same core predicate replay uses.
2. Live is stricter than replay
The live reducer rejects terminal completion while an output transaction is unsettled, while replay's terminal validation checks settlement only for a subset of outcomes. Move the common settlement rule into the shared terminal validator.
3. #79 atomic History consequence
Every reportable terminal outcome must create exactly one HistoryRecord atomically with completion under both live reduction and replay. Failed/stopped/non-reportable outcomes must create none.
Do not implement this as two validators or as a later projection from standing verdicts. One terminal transition validator should establish whether the History delta is required, forbidden, and internally consistent.
Acceptance
From the third rewrite review (line references originally at
rewrite75c79c3).The durable contract says live reduction and journal replay validate the same transition relation. They currently do not.
1. Replay is stricter than live
journal.rsrejects incompleteMediaObservedvalues that live command paths accept and journal. A live-accepted/replay-rejected delta can make the next startup report corruption and discard a valid tail.Completeness validation currently lives partly in engine call-site guards. Put one predicate at the core mutation boundary and share it with replay so an invalid durable delta is unrepresentable.
The old second example involving empty
HistoryImportedkeys is removed by #79 along withHistoryImported/parked state. Replace it with validation of the nativeHistoryRecordcontract:HistoricalFile::Pathor non-empty anonymous identifier;Import validation and native terminal materialization must use the same core predicate replay uses.
2. Live is stricter than replay
The live reducer rejects terminal completion while an output transaction is unsettled, while replay's terminal validation checks settlement only for a subset of outcomes. Move the common settlement rule into the shared terminal validator.
3. #79 atomic History consequence
Every reportable terminal outcome must create exactly one
HistoryRecordatomically with completion under both live reduction and replay. Failed/stopped/non-reportable outcomes must create none.Do not implement this as two validators or as a later projection from standing verdicts. One terminal transition validator should establish whether the History delta is required, forbidden, and internally consistent.
Acceptance