Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 71 additions & 0 deletions .aristo/index.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
[__meta__]
schema_version = 1
generated_by = "aristo stamp 0.2.0"
generated_at = "2026-06-05T07:51:33.45819636Z"
source_root = "."

[backfill_watermark_advances_only_after_durable]
kind = "intent"
text = "The published backfill watermark advances only after the database-file pages it covers have been durably written and synced, so a crash can never leave the log treating frames as applied to the database when the database does not yet hold them."
verify = "neural"
status = "unknown"
text_hash = "sha256:41ecf517973ba246f2906d32769b4fc1dbe366b30a71431402629bff6306d4dd"
body_hash = "sha256:f85e009b6961916b91528b745d43e4173eb76499e296dd2315daf0290ce76209"
file = "core/storage/wal.rs"
site = "impl Wal for WalFile::publish_backfill (line 3783)"
covered_region = "function"

[committed_frames_visible_only_after_durable]
kind = "intent"
text = "Appended frames become visible to readers only after they have been durably written and synced, so a reader never observes a frame whose data a crash could still lose."
verify = "neural"
status = "unknown"
text_hash = "sha256:74c9ab83ffb8f941a7af5f5c9917f2d082bc6753ca8bb0f62de7dac42fe1f83f"
body_hash = "sha256:3bfdda02e38c710c89ec74ae8c18d240fd73133d61839848f0fb63fd71979bc7"
file = "core/storage/wal.rs"
site = "impl Wal for WalFile::finish_append_frames_commit (line 3953)"
covered_region = "function"

[log_restart_rotates_salts]
kind = "intent"
text = "Restarting the log changes the WAL salts and increments the checkpoint sequence, so frames written under a previous epoch cannot be mistaken as valid once the log file is reused."
verify = "neural"
status = "unknown"
text_hash = "sha256:c52bf25b41ba56279e7c1c7066ae6318ff82a99c1af858ec82c269dec6882d12"
body_hash = "sha256:b00775bc779b3fcf3713676b6675ea5c354d64b207daa71437d77a884b3ff35f"
file = "core/storage/wal.rs"
site = "impl ShmWalCoordination::restart_snapshot_from_authority (line 1710)"
covered_region = "function"

[truncate_failure_surfaced_as_error]
kind = "intent"
text = "A failed WAL truncation, or its post-truncation sync, during a TRUNCATE checkpoint is surfaced as a checkpoint error and is never reported to the caller as a successfully emptied log."
verify = "neural"
status = "unknown"
text_hash = "sha256:ec1910d45dab26c962378a05fb3b082b98e9cc1da455b77c521ffebb2a21146b"
body_hash = "sha256:05185c3220c7a3336b932e56abace4aeb02d2e59791bd490705d036c41afd850"
file = "core/storage/wal.rs"
site = "impl WalFile::truncate_log (line 4891)"
covered_region = "function"

[wal_initialized_only_after_header_durable]
kind = "intent"
text = "The WAL counts as initialized only after its header has been durably written and its sync has completed successfully; a failed header write or sync leaves the WAL uninitialized so the header is re-issued before the next append, so the initialized state never reports durability the on-disk header has not actually reached."
verify = "neural"
status = "unknown"
text_hash = "sha256:29cfd50757584c85fc404e9c3d112aa47fe794bfaee0fc0f1ddff4059bfc24bf"
body_hash = "sha256:074f1f17f8ba26ffd1109158b3d49d5ad5ded5187c1ba8f678bd80544b495885"
file = "core/storage/wal.rs"
site = "trait WalCoordination::mark_initialized (line 574)"
covered_region = "function"

[wal_records_changes_before_apply]
kind = "intent"
text = "An append-only log that records page-level changes before they are applied to the database, so a system crash can be recovered by replaying the log."
verify = "neural"
status = "unknown"
text_hash = "sha256:85270d4acbf9d93ad70d71d3c5a3a4863616dba36abb529bd7d12244e615e79e"
body_hash = "sha256:3627e8fd855d64d269a1c927fe4a88b02e1edd4db64e2ffc93b704d24b701552"
file = "core/storage/wal.rs"
site = "trait Wal (line 608)"
covered_region = "type"
34 changes: 34 additions & 0 deletions .github/workflows/aristo.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
# Lints Aristo intent annotations on every PR.
#
# Runs the cheap, local annotation checks via the shared aristo-action — no
# token needed, everything runs on the runner:
# - stamp: the index is fresh relative to source (new/changed intents indexed)
# - lint: annotation prose is clean (no placeholders, weasel words, etc.)
#
# Heavy canon verification (`aristo verify`) is intentionally not run here; it
# needs an ARETTA_TOKEN secret and belongs in a separate nightly workflow.
name: Aristo intents

on:
workflow_dispatch:
push:
branches:
- main
pull_request:
branches:
- main

concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true

jobs:
lint:
name: Lint intent annotations
timeout-minutes: 10
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: aretta-ai/aristo-action@v1
with:
checks: stamp, lint
24 changes: 24 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -413,6 +413,30 @@ And launch an Antithesis test run with:
scripts/antithesis/launch.sh
```

## Annotating intent with Aristo

Turso uses [Aristo](https://github.com/aretta-ai/aristo) to capture design intent that the code alone doesn't spell out — invariants a refactor could silently break — as `#[aristo::intent("...")]` annotations attached to the code. They're optional; reach for one only when a property is invisible from the signature and not already guarded by a test. For example, on the WAL trait in `core/storage/wal.rs`:

```rust
#[aristo::intent(
"An append-only log that records page-level changes before they are \
applied to the database, so a system crash can be recovered by \
replaying the log.",
verify = "neural",
id = "wal_records_changes_before_apply",
)]
pub trait Wal: Debug + Send + Sync { ... }
```

The macros are a workspace dependency, so annotated code builds normally. To author and lint annotations, install the CLI:

```console
cargo install aristo-cli # provides the `aristo` command
aristo lint # lint annotation prose (also runs in CI on every PR)
```

To machine-check annotations, run `/aristo-neural-verify` in Claude Code.

## Adding Third Party Dependencies

When you want to add third party dependencies, please follow these steps:
Expand Down
21 changes: 21 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

28 changes: 28 additions & 0 deletions aristo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
[verify.cache]
strategy = "local"
commit_specs = true

[stamp]
hooks = "pre-commit"
hash_crate_root = false

[telemetry]
enabled = false

[lint]
pre_commit = "check"
strict = false

[corpus]
contribute = false

[doc]
commit_artifacts = true
position = "before"

[index]

[canon]
enabled = true
threshold_stamp = 0.85
threshold_critique = 0.65
1 change: 1 addition & 0 deletions core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,7 @@ bigdecimal = "0.4"
num-bigint = "0.4"
num-traits = "0.2"
stacker = { version = "0.1", optional = true }
aristo = "0.2.0"

[target.'cfg(not(any(target_family = "wasm", all(target_os = "windows", target_arch = "aarch64"))))'.dependencies]
simsimd = "6.5.3"
Expand Down
47 changes: 47 additions & 0 deletions core/storage/wal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -571,6 +571,16 @@ trait WalCoordination: Debug + Send + Sync {
fn prepare_wal_header(&self, io: &dyn IO, page_size: PageSize) -> Option<WalHeader>;

/// Mark the WAL header durable after the header sync completes.
#[aristo::intent(
"The WAL counts as initialized only after its header has been \
durably written and its sync has completed successfully; a \
failed header write or sync leaves the WAL uninitialized so the \
header is re-issued before the next append, so the initialized \
state never reports durability the on-disk header has not \
actually reached.",
verify = "neural",
id = "wal_initialized_only_after_header_durable"
)]
fn mark_initialized(&self);

/// Record a newly appended frame in the backend's page-to-frame lookup state.
Expand All @@ -595,6 +605,13 @@ trait WalCoordination: Debug + Send + Sync {
}

/// Write-ahead log (WAL).
#[aristo::intent(
"An append-only log that records page-level changes before they are \
applied to the database, so a system crash can be recovered by \
replaying the log.",
verify = "neural",
id = "wal_records_changes_before_apply"
)]
pub trait Wal: Debug + Send + Sync {
/// Begin a read transaction.
/// Returns whether the database state has changed since the last read transaction.
Expand Down Expand Up @@ -1690,6 +1707,13 @@ impl ShmWalCoordination {
}
}

#[aristo::intent(
"Restarting the log changes the WAL salts and increments the \
checkpoint sequence, so frames written under a previous epoch \
cannot be mistaken as valid once the log file is reused.",
verify = "neural",
id = "log_restart_rotates_salts"
)]
fn restart_snapshot_from_authority(
&self,
snapshot: SharedWalCoordinationHeader,
Expand Down Expand Up @@ -3756,6 +3780,15 @@ impl Wal for WalFile {
)
}

#[aristo::intent(
"The published backfill watermark advances only after the \
database-file pages it covers have been durably written and \
synced, so a crash can never leave the log treating frames as \
applied to the database when the database does not yet hold \
them.",
verify = "neural",
id = "backfill_watermark_advances_only_after_durable"
)]
fn publish_backfill(&self, max_frame: u64) {
self.coordination.publish_backfill(max_frame);
}
Expand Down Expand Up @@ -3917,6 +3950,13 @@ impl Wal for WalFile {
}

#[instrument(skip_all, level = Level::DEBUG)]
#[aristo::intent(
"Appended frames become visible to readers only after they have \
been durably written and synced, so a reader never observes a \
frame whose data a crash could still lose.",
verify = "neural",
id = "committed_frames_visible_only_after_durable"
)]
fn finish_append_frames_commit(&self) -> Result<()> {
let max_frame = self.max_frame.load(Ordering::Acquire);
let last_checksum = *self.last_checksum.read();
Expand Down Expand Up @@ -4848,6 +4888,13 @@ impl WalFile {
}

/// Truncate WAL file to zero and sync it. Called by pager AFTER DB file is synced.
#[aristo::intent(
"A failed WAL truncation, or its post-truncation sync, during a \
TRUNCATE checkpoint is surfaced as a checkpoint error and is \
never reported to the caller as a successfully emptied log.",
verify = "neural",
id = "truncate_failure_surfaced_as_error"
)]
fn truncate_log(
&self,
result: &mut CheckpointResult,
Expand Down
Loading