retrace

Typed, portable session recording and reconstruction. Callers own safe projections, persistence, clocks and deterministic reducers.

Types

Checkpoint

</>

pub type Checkpoint(model) {
  Checkpoint(
    origin: Origin,
    sequence: Int,
    elapsed_ms: Int,
    model: model,
  )
}

Constructors

Checkpoint(
  origin: Origin,
  sequence: Int,
  elapsed_ms: Int,
  model: model,
)

Entry

</>

Untrusted candidate data. step checks its stream invariants before reducing.

pub type Entry(event) {
  Entry(
    origin: Origin,
    sequence: Int,
    elapsed_ms: Int,
    event: event,
  )
}

Constructors

Entry(
  origin: Origin,
  sequence: Int,
  elapsed_ms: Int,
  event: event,
)

Error

</>

pub type Error(error) {
  InvalidOrigin
  InvalidPosition
  DifferentContract(expected: String, received: String)
  DifferentRecording(expected: String, received: String)
  OutOfOrder(expected: Int, received: Int)
  TimeWentBack(previous_ms: Int, received_ms: Int)
  ReductionFailed(sequence: Int, cause: error)
  CheckpointMismatch(sequence: Int)
}

Constructors

```
InvalidOrigin
```
```
InvalidPosition
```

DifferentContract(expected: String, received: String)

DifferentRecording(expected: String, received: String)

OutOfOrder(expected: Int, received: Int)

TimeWentBack(previous_ms: Int, received_ms: Int)

ReductionFailed(sequence: Int, cause: error)

```
CheckpointMismatch(sequence: Int)
```

Origin

</>

pub type Origin {
  Origin(recording_id: String, contract_id: String)
}

Constructors

Origin(recording_id: String, contract_id: String)

Player

opaque </>

pub opaque type Player(model, event, error)

Recorder

opaque </>

pub opaque type Recorder

Values

checkpoint

</>

pub fn checkpoint(
  recorder: Recorder,
  model: model,
) -> Checkpoint(model)

The caller supplies the safe state after the recorder’s latest entry. This function cannot establish that the supplied model matches the entries.

model

</>

pub fn model(player: Player(model, event, error)) -> model

position

</>

pub fn position(player: Player(model, event, error)) -> Int

record

</>

pub fn record(
  recorder: Recorder,
  event: event,
  elapsed_ms elapsed_ms: Int,
) -> Result(#(Recorder, Entry(event)), Error(Nil))

Number an already accepted safe event. Return the next recorder and the entry to enqueue. This is not a persistence acknowledgement: the application must commit recorder progress together with its outbox to survive crashes. Equal timestamps are allowed. Use a monotonic elapsed clock, not wall time.

replay

</>

pub fn replay(
  checkpoint: Checkpoint(model),
  contract_id: String,
  reduce: fn(model, event) -> Result(model, error),
) -> Result(Player(model, event, error), Error(error))

Start replay at a checkpoint supplied by the application. Validate its identity, compatibility and cursor; model validity belongs to the decoder.

resume

</>

pub fn resume(
  checkpoint: Checkpoint(model),
) -> Result(Recorder, Error(Nil))

Restore a recorder after the caller has atomically recovered its checkpoint and outbox. This trusts the supplied cursor; it does not claim exclusive ownership of a recording. Concurrent writers must use different IDs.

start

</>

pub fn start(
  origin: Origin,
  initial: model,
) -> Result(#(Recorder, Checkpoint(model)), Error(Nil))

Begin at sequence zero. The caller owns the recording ID and clock epoch.

step

</>

pub fn step(
  player: Player(model, event, error),
  entry: Entry(event),
) -> Result(Player(model, event, error), Error(error))

Consume exactly the next entry. Duplicates and gaps are errors; callers own deduplication and missing-range fetching. On error the old player remains usable. Neither a failed reducer nor an invalid entry advances the cursor.

verify

</>

pub fn verify(
  player: Player(model, event, error),
  checkpoint: Checkpoint(model),
  equal: fn(model, model) -> Bool,
) -> Result(Nil, Error(error))

Compare reconstructed state with a checkpoint at the same cursor and time. Caller-defined equality is a consistency check, not an authenticity proof.