diff --git a/.aristo/index.toml b/.aristo/index.toml new file mode 100644 index 0000000000..1b950d11a0 --- /dev/null +++ b/.aristo/index.toml @@ -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" diff --git a/.github/workflows/aristo.yml b/.github/workflows/aristo.yml new file mode 100644 index 0000000000..48c6e8ff1d --- /dev/null +++ b/.github/workflows/aristo.yml @@ -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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index fabbaabe57..669c869f2f 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -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: diff --git a/Cargo.lock b/Cargo.lock index 9a2bdea365..ecb3c9ef6a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -225,6 +225,26 @@ version = "1.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "69f7f8c3906b62b754cd5326047894316021dcfe5a194c8ea52bdd94934a3457" +[[package]] +name = "aristo" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e8a6b4e39193428654239618ced859b97f48b996afa92579e6a0f4191dc1094" +dependencies = [ + "aristo-macros", +] + +[[package]] +name = "aristo-macros" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "855bf1b08a5653549110e4b1540223e453e1d98f82eb4e5b5d407782dae7409e" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.100", +] + [[package]] name = "arrayref" version = "0.3.9" @@ -6641,6 +6661,7 @@ dependencies = [ "allocator-api2 0.4.0", "antithesis_sdk", "arc-swap", + "aristo", "bigdecimal", "bitflags 2.9.4", "branches", diff --git a/aristo.toml b/aristo.toml new file mode 100644 index 0000000000..1f7623e178 --- /dev/null +++ b/aristo.toml @@ -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 diff --git a/core/Cargo.toml b/core/Cargo.toml index cd81fd8113..90123264c0 100644 --- a/core/Cargo.toml +++ b/core/Cargo.toml @@ -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" diff --git a/core/storage/wal.rs b/core/storage/wal.rs index a7bcda8f1b..10859eac08 100644 --- a/core/storage/wal.rs +++ b/core/storage/wal.rs @@ -571,6 +571,16 @@ trait WalCoordination: Debug + Send + Sync { fn prepare_wal_header(&self, io: &dyn IO, page_size: PageSize) -> Option; /// 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. @@ -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. @@ -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, @@ -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); } @@ -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(); @@ -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,