Data integrity and verification

Audience: developers, decision-makers · Read route: rebuild, understand · Reflects specification v0.1

Data integrity here is checkable: you can prove the record was not altered and reconstruct exactly what happened, and in what order, without trusting the copy of the data that any single operator keeps. If two versions of the history ever diverged, the divergence would show. That is the whole promise of this page, and a decision-maker can stop reading here with the right mental model: a tamper-evident log, where every deviation is detectable and provable.

The rest of this page is for a developer who wants to know why that promise holds.

Why it holds: three properties of deterministic replay

The previous page, Runtime and replay, described the mechanism: state is rebuilt by applying an ordered log of recorded actions through pure method bodies. Three properties fall out of that mechanism, and together they are what "data integrity" reduces to.

• Audit without trust. Anyone holding the log can compute what state the runtime should be in. There is no need to trust the operator's storage or the operator's reporting, because the log, not the operator, is the authority. If the operator's stored state disagrees with the log, the log wins and the disagreement is visible.
• Time travel. Because state at any point is the result of applying every action up to that point, any past state is recoverable by replaying up to the moment you want. Nothing is thrown away; the history is the state.
• Pure method bodies. A method body is a function of state and the incoming action, with no hidden input. This is what makes replay reproducible, and, as a side benefit, it makes every method testable in isolation.

Where this page stops and the mechanism pages take over

This page owns the property and its consequences: integrity, audit without trust, and recoverable history. It does not restate the mechanism. The roles, the replay procedure, the drift halt, and schema evolution are on Runtime and replay; how a change is made tamper-evident on a shared log is on Anchoring and the audit log. Read those two for how; read this for what it gives you.

The rules behind this page

The verification and replay rules that make integrity checkable are in the specification, Section 3.5. This page describes the properties those rules produce and does not restate the rules themselves.