Define Picante semantics (spec) + Tracey coverage #45
Conversation
- Create docs/spec/picante.md with ~90 requirements covering: - Core concepts (revisions, keys, dependencies) - Ingredient types (input, derived, interned) - Runtime and execution frames - Derived query lifecycle and cell states - In-flight deduplication - Snapshots - Persistence - Macros - Events and observability - Error handling - Type erasure - Annotate source files with r[requirement.id] references: - revision.rs, key.rs, error.rs - runtime.rs, frame.rs - ingredient/input.rs, derived.rs, interned.rs - inflight.rs, persist.rs, debug.rs - Add .config/tracey/config.kdl for tracey integration
There was a problem hiding this comment.
Pull request overview
This PR adds a comprehensive ~850-line specification document for Picante following the tracey format, along with corresponding code annotations linking implementation to spec requirements. The spec covers all major aspects of the Picante incremental query runtime including revisions, ingredients, dependency tracking, MVCC snapshots, persistence, and macros.
Key Changes
- Added comprehensive specification document with ~90 requirements covering core concepts, ingredient types, runtime behavior, execution model, and tooling
- Added
// r[requirement.id]annotations throughout the codebase to link implementation to specification - Configured tracey tooling for spec coverage tracking
Reviewed changes
Copilot reviewed 13 out of 14 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| docs/spec/picante.md | New 848-line specification document defining Picante's behavior with requirement IDs |
| crates/picante/src/runtime.rs | Added 10+ annotations linking runtime implementation to spec requirements for revisions, dependencies, and events |
| crates/picante/src/revision.rs | Added annotations for revision type and monotonicity requirements |
| crates/picante/src/persist.rs | Added annotations for cache file format, save/load operations, and validation requirements |
| crates/picante/src/key.rs | Added annotations for key encoding, FNV-1a hashing, and dependency structures; added clarifying comments for FNV constants |
| crates/picante/src/ingredient/interned.rs | Added annotations for interned ingredient behavior and ID stability |
| crates/picante/src/ingredient/input.rs | Added annotations for input ingredient operations and snapshot semantics |
| crates/picante/src/ingredient/derived.rs | Added annotations for derived query lifecycle, cell states, type erasure, and memoization |
| crates/picante/src/inflight.rs | Added annotations for in-flight deduplication registry and shared cache |
| crates/picante/src/frame.rs | Added annotations for task-local frames, dependency recording, and cycle detection |
| crates/picante/src/error.rs | Added annotations for error types and result aliases |
| crates/picante/src/debug.rs | Added annotations for debugging tools including graph visualization and trace analysis |
| .config/tracey/config.kdl | Added tracey configuration for spec coverage tracking |
| .gitignore | Added .tracey/ to ignore tracey working directory |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
docs/spec/picante.md
Outdated
| | State | Description | | ||
| |-------|-------------| | ||
| | `Vacant` | No cached value exists | | ||
| | `Running { started_at }` | A task is currently computing the value | | ||
| | `Ready { value, deps, verified_at, changed_at }` | A cached value with its dependency list | | ||
| | `Poisoned { error, verified_at }` | Previous compute failed at this revision | |
There was a problem hiding this comment.
The table at line 329 uses incorrect Markdown pipe syntax. The first pipe character should not have a space before it. The table should start with | State | Description | instead of || State | Description |.
Add 13 spec annotations to the macro crate:
- input.rs: macro.input.{purpose,keyed,singleton,kind-id}
- interned.rs: macro.interned.{purpose,output}
- tracked.rs: macro.tracked.{purpose,output,key-tuple,return-wrap}
- db.rs: macro.db.{purpose,output,snapshot}
Also fix persist.not-stored to use blockquote syntax in the spec.
Add 7 snapshot-related spec annotations:
- db.rs: snapshot.{creation,async,frozen,independent,interned,multiple}
- derived.rs: snapshot.derived
Note: snapshot.input was already annotated in input.rs from prior work.
Add 16 annotations across the codebase:
Tracing:
- lib.rs: trace.{crate,no-subscriber,levels}
Persistence:
- persist.rs: persist.not-stored
Revisions:
- derived.rs: revision.{changed_at,verified_at}
Type constraints:
- input.rs: input.constraints
- interned.rs: interned.constraints
Derived queries:
- derived.rs: derived.compute-fn, cell.no-lock-await,
type-erasure.tradeoffs, inflight.shared-cache-adopt
In-flight:
- inflight.rs: inflight.follower
Query kinds:
- key.rs: kind.{collision,uniqueness}
fasterthanlime
force-pushed
the
add-tracey-spec
branch
from
3cbaa26 to
009dc0d
Compare
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 18 out of 19 changed files in this pull request and generated 27 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
docs/spec/picante.md
Outdated
| ## Nomenclature | ||
|
|
||
| **Revision** | ||
| A monotonically increasing 64-bit logical clock (u64) used to track changes. Higher revisions represent more recent states. |
There was a problem hiding this comment.
The term "Higher revisions represent more recent states" could be misinterpreted. Consider clarifying that this refers to logical time ordering within a single runtime instance, not across different runtime instances or persisted cache files.
| A monotonically increasing 64-bit logical clock (u64) used to track changes. Higher revisions represent more recent states. | |
| A monotonically increasing 64-bit logical clock (u64) used to track changes within a single runtime instance. Within that instance, higher revisions represent later logical times, but revisions are not comparable across different runtime instances or persisted cache files. |
docs/spec/picante.md
Outdated
| > 1. Look up all queries that depend on `(kind, key)` via the reverse dep graph | ||
| > 2. For each dependent query, emit a `QueryInvalidated` event | ||
| > 3. Recursively propagate to queries depending on those queries | ||
| > 4. This is a depth-first traversal; cycles are handled by tracking visited nodes |
There was a problem hiding this comment.
The specification states "cycles are handled by tracking visited nodes" but the actual implementation uses a task-local stack (line 301 r[frame.cycle-stack]) which only detects cycles within a single task, not globally. This creates a discrepancy between the spec and the actual behavior. The spec should clarify that cycle detection is per-task only, which is mentioned later at line 316 but should be consistent here.
| > 4. This is a depth-first traversal; cycles are handled by tracking visited nodes | |
| > 4. This is a depth-first traversal; cycles are handled per task using the task-local cycle stack (i.e., tracking visited nodes within the current task) |
docs/spec/picante.md
Outdated
| > The shared cache MUST be keyed by `(runtime_id, kind, key)` — note: no revision in the key. | ||
| r[inflight.shared-cache-size] | ||
| The cache size MUST be configurable via `PICANTE_SHARED_CACHE_MAX_ENTRIES` environment variable. Default: 20,000 entries. |
There was a problem hiding this comment.
The specification mentions "PICANTE_SHARED_CACHE_MAX_ENTRIES environment variable" but doesn't specify the expected format (integer), behavior on invalid values, or when this variable is read (at startup, dynamically, etc.). These details should be included for a complete specification.
| The cache size MUST be configurable via `PICANTE_SHARED_CACHE_MAX_ENTRIES` environment variable. Default: 20,000 entries. | |
| The cache size MUST be configurable via `PICANTE_SHARED_CACHE_MAX_ENTRIES` environment variable. The value of this variable MUST be a base-10 integer representing the maximum number of entries in the shared cache. Implementations MUST read and fix the effective cache size at runtime initialization; subsequent changes to the process environment MUST NOT affect an already-initialized runtime. If `PICANTE_SHARED_CACHE_MAX_ENTRIES` is unset, cannot be parsed as an integer, or is less than 1, implementations MUST fall back to the default of 20,000 entries. |
docs/spec/picante.md
Outdated
| The format version MUST match exactly. Version mismatch is treated as corruption. | ||
| r[persist.load-kind-match] | ||
| Each section's `kind_id` MUST match a provided ingredient. Unknown sections MUST be ignored with a warning. |
There was a problem hiding this comment.
The load validation section mentions that "Unknown sections MUST be ignored with a warning" (line 605) but doesn't specify what constitutes a warning. Should this be a tracing::warn! call? A returned diagnostic? This should be clarified for implementation consistency.
| Each section's `kind_id` MUST match a provided ingredient. Unknown sections MUST be ignored with a warning. | |
| Each section's `kind_id` MUST match a provided ingredient. Unknown sections MUST be ignored, and a warning MUST be emitted. A "warning" in this context is an implementation-defined, non-fatal diagnostic that is made observable to the caller or operator (for example via logging, tracing, or a diagnostic channel) and MUST NOT cause the load operation to fail. |
docs/spec/picante.md
Outdated
| > - Per-field getters: `{field}(db) -> PicanteResult<Option<T>>` | ||
| r[macro.input.kind-id] | ||
| Kind ids MUST be generated via `QueryKindId::from_str(...)` using the full module path and struct name. |
There was a problem hiding this comment.
The specification mentions "Kind ids MUST be generated via QueryKindId::from_str(...) using the full module path and struct name" but doesn't specify the exact format. Should this be "module::path::StructName" or some other format? This affects cache stability and should be precisely specified.
| Kind ids MUST be generated via `QueryKindId::from_str(...)` using the full module path and struct name. | |
| Kind ids MUST be generated via `QueryKindId::from_str(...)` using the fully qualified Rust path to the query struct, in the form `crate_name::module::path::StructName` (i.e., with `::` separators, including the crate name). For example: `my_crate::config::Config`. |
docs/spec/picante.md
Outdated
| Snapshot creation is async because it needs to lock cells to clone their state. | ||
| ### Semantics | ||
| r[snapshot.frozen] | ||
| A snapshot MUST freeze the database state at creation time. Subsequent modifications to the database MUST NOT be visible in the snapshot. |
There was a problem hiding this comment.
The snapshot creation specification states it's "async because it needs to lock cells" but doesn't specify any ordering guarantees or atomicity properties. For example, if inputs are modified during snapshot creation, which state is captured? This should be clarified.
| Snapshot creation is async because it needs to lock cells to clone their state. | |
| ### Semantics | |
| r[snapshot.frozen] | |
| A snapshot MUST freeze the database state at creation time. Subsequent modifications to the database MUST NOT be visible in the snapshot. | |
| Snapshot creation is async because it needs to lock cells to clone their state, but this MUST NOT affect the observable atomicity of the snapshot. | |
| Implementations MUST treat `DatabaseSnapshot::from_database(&db).await` as a linearizable operation: there MUST exist a single revision `R` between the invocation of `from_database` and the completion of the `await` such that the snapshot's contents are exactly the database state at revision `R`. | |
| Concurrent writes that commit before `R` MUST be visible in the snapshot; writes that commit at or after the first revision strictly greater than `R` MUST NOT be visible in the snapshot. | |
| Implementations MAY acquire per-cell or per-ingredient locks while cloning state, but the snapshot MUST NOT observe a "torn" state that could not exist at any single revision (i.e., different keys MUST NOT reflect different revisions). | |
| ### Semantics | |
| r[snapshot.frozen] | |
| A snapshot MUST freeze the database state at its bound revision `R` (as defined in `r[snapshot.async]`). Subsequent modifications to the database, including those that occur while `from_database` is running but that commit after `R`, MUST NOT be visible in the snapshot. |
docs/spec/picante.md
Outdated
| > `InputIngredient` snapshots MUST use O(1) structural sharing via `im::HashMap`. The snapshot shares structure with the original; only modified paths are copied (copy-on-write). | ||
| > r[snapshot.derived] | ||
| > `DerivedIngredient` snapshots MUST deep-clone cached cells into new `ErasedCell` instances. Values remain cheap to clone (they are `Arc<dyn Any>`). |
There was a problem hiding this comment.
The specification states that "values remain cheap to clone (they are Arc<dyn Any>)" but this is an implementation detail rather than a behavioral requirement. Consider rephrasing to focus on the requirement: "Cloning snapshot cells MUST be efficient, sharing the underlying value storage" or similar.
| > `DerivedIngredient` snapshots MUST deep-clone cached cells into new `ErasedCell` instances. Values remain cheap to clone (they are `Arc<dyn Any>`). | |
| > `DerivedIngredient` snapshots MUST deep-clone cached cells into new `ErasedCell` instances. Cloning snapshot cells MUST be efficient by sharing underlying value storage rather than eagerly duplicating values. |
docs/spec/picante.md
Outdated
| > `DerivedIngredient` snapshots MUST deep-clone cached cells into new `ErasedCell` instances. Values remain cheap to clone (they are `Arc<dyn Any>`). | ||
| > r[snapshot.interned] | ||
| > `InternedIngredient` snapshots MUST share the same `Arc` with the original. New interns after snapshot creation are visible to both (append-only semantics). |
There was a problem hiding this comment.
The specification states new interns "are visible to both" the snapshot and parent database (line 522) but doesn't specify the visibility semantics. Does this mean interns created in a snapshot are immediately visible in the parent? This could lead to unexpected behavior and should be clarified.
| > `InternedIngredient` snapshots MUST share the same `Arc` with the original. New interns after snapshot creation are visible to both (append-only semantics). | |
| > `InternedIngredient` snapshots MUST share the same `Arc` (intern table) with the original database. The intern table is append-only and is shared across the parent database and all of its snapshots. | |
| > | |
| > Interner operations performed through either the parent or any snapshot MUST append to this shared table. Newly created interns MUST be immediately visible and usable from both the parent and all snapshots (bidirectional visibility). | |
| > | |
| > This shared, append-only intern table is exempt from `r[snapshot.frozen]`: snapshots freeze the values of inputs and derived queries, but they do NOT freeze the set of interned keys. Appending new interns MUST NOT change the meaning of previously existing intern IDs. |
docs/spec/picante.md
Outdated
| > - Function pointers for equality checking: `eq_erased: fn(&dyn Any, &dyn Any) -> bool` | ||
| r[type-erasure.benefit] | ||
| This SHOULD achieve ~96% reduction in LLVM IR for the state machine and ~36% faster clean builds. |
There was a problem hiding this comment.
The type-erasure.benefit requirement states "This SHOULD achieve ~96% reduction in LLVM IR" with specific performance numbers. Using SHOULD with specific benchmarks is unusual - consider either making this informational (not a requirement) or clarifying that these are observed benefits rather than guaranteed outcomes.
| This SHOULD achieve ~96% reduction in LLVM IR for the state machine and ~36% faster clean builds. | |
| In the reference implementation, type erasure has been observed to achieve ~96% reduction in LLVM IR for the state machine and ~36% faster clean builds; these figures are informational and not normative requirements. |
crates/picante/src/key.rs
Outdated
| pub const fn from_str(s: &str) -> Self { | ||
| let bytes = s.as_bytes(); | ||
| let mut hash: u32 = 0x811c9dc5; | ||
| let mut hash: u32 = 0x811c9dc5; // FNV offset basis |
There was a problem hiding this comment.
The comment says "FNV offset basis" but the specification (r[kind.hash]) uses the term "FNV_OFFSET" in its pseudocode. While this is a minor inconsistency, consider using the same terminology as the spec for traceability.
| let mut hash: u32 = 0x811c9dc5; // FNV offset basis | |
| let mut hash: u32 = 0x811c9dc5; // FNV_OFFSET |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 18 out of 19 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| r[sharing.nonobservable] | ||
| Such sharing MUST NOT change observable behavior: the values and errors returned MUST be indistinguishable from a correct, non-sharing implementation that evaluates each runtime instance independently under the semantics above. | ||
|
|
There was a problem hiding this comment.
The specification is incomplete. The PR description claims "~750 lines, ~90 requirements" but the actual spec file is only 172 lines and defines approximately 25 requirements. The code references over 90 requirement IDs that do not exist in this specification file.
Missing requirement categories include:
- Runtime and frame requirements (runtime.components, runtime.new, frame.task-local, frame.purpose, etc.)
- Event system requirements (event.channel, event.broadcast-capacity, event.types, event.key-fields, event.query-changed-cutoff)
- Type erasure requirements (type-erasure.mechanism, type-erasure.purpose, type-erasure.benefit, type-erasure.tradeoffs)
- Derived query implementation details (derived.type, derived.get, derived.compute-fn, derived.memoization)
- Cell state requirements (cell.compute, cell.access, cell.waiter, cell.states, cell.leader-local, cell.stale, cell.no-lock-await, cell.poison-scoped)
- In-flight deduplication requirements (inflight.registry, inflight.purpose, inflight.key, inflight.scope, inflight.follower, inflight.complete, inflight.fail, inflight.cancel, inflight.try-lead, inflight.shared-cache, inflight.shared-cache-key, inflight.shared-cache-size, inflight.shared-cache-adopt)
- Persistence requirements (persist.format, persist.structure, persist.section, persist.save-fn, persist.save-options, persist.save-atomic, persist.save-unique-kinds, persist.load-fn, persist.load-return, persist.load-options, persist.load-order, persist.load-kind-match, persist.load-name-match, persist.load-type-match, persist.not-stored, persist.load-version)
- Interned ingredient requirements (interned.type, interned.id-type, interned.stability, interned.constraints, interned.intern, interned.get)
- Input ingredient implementation requirements (input.type, input.constraints, input.revision-on-change)
- Key and kind requirements (kind.type, kind.collision, key.encoding, key.dyn-key, key.dep)
- Revision tracking requirements (revision.initial, revision.set, revision.verified-at, revision.changed-at)
- Snapshot requirements (snapshot.runtime-id, snapshot.input, snapshot.derived, snapshot.frozen, snapshot.independent, snapshot.multiple, snapshot.async)
- Dependency tracking requirements (dep.forward, dep.reverse, frame.record-dep)
- Error handling requirements (error.result, error.type, error.variants)
- Debugging and tracing requirements (debug.graph, debug.cache-stats, debug.trace-collector, debug.trace-analysis, trace.crate, trace.no-subscriber, trace.levels)
- Macro generation requirements (macro.tracked.purpose, macro.tracked.key-tuple, macro.tracked.return-wrap, macro.tracked.output, macro.interned.purpose, macro.interned.output, macro.input.purpose, macro.input.keyed, macro.input.kind-id, macro.input.singleton, macro.db.purpose, macro.db.snapshot, macro.db.output)
- Cycle detection requirements (frame.cycle-stack, frame.cycle-detect, frame.cycle-per-task)
Either the spec needs to be completed to include all these requirements, or the code annotations should be updated to reference only the requirements that are actually defined in the spec.
| --- | |
| # Additional requirements index | |
| This section lists additional requirements referenced from the implementation. They refine and extend the observable semantics described above without prescribing specific data structures or algorithms. | |
| ## Runtime and frames | |
| r[runtime.components] | |
| A runtime instance MUST provide components for managing inputs, derived queries, dependency tracking, memoization, revisions, and snapshots. | |
| r[runtime.new] | |
| Creating a new runtime instance MUST start from a clean state with no memoized derived results and an initial revision as specified by the revision requirements. | |
| r[frame.purpose] | |
| A frame represents the dynamic context of evaluating a single derived query invocation, used for tracking dependencies and detecting cycles. | |
| r[frame.task-local] | |
| Frames used for tracking evaluation state MUST be task-local or otherwise isolated per concurrent evaluation so that dependency tracking is correct under concurrency. | |
| r[frame.record-dep] | |
| Whenever a derived query reads an input or another derived query, the current frame MUST record a dependency edge from the caller to the callee at the current revision. | |
| r[frame.cycle-stack] | |
| The runtime MUST maintain a logical stack or equivalent structure of active frames to support cycle detection among derived queries. | |
| r[frame.cycle-detect] | |
| If evaluation of a derived query would create a cycle in the active frame stack, the runtime MUST detect this cycle and surface it via a well-defined error as specified in the error handling requirements. | |
| r[frame.cycle-per-task] | |
| Cycle detection MUST operate independently per task or thread; cycles in one task MUST NOT corrupt or interfere with evaluations in another. | |
| ## Event system | |
| r[event.channel] | |
| The runtime MAY expose an event channel for observing internal activity; if provided, it MUST deliver events in an order consistent with the revision ordering of the originating runtime instance. | |
| r[event.broadcast-capacity] | |
| Any internal buffering or broadcast capacity for events MUST be documented to callers; dropping events due to capacity limits MUST NOT affect query semantics. | |
| r[event.types] | |
| If events are exposed, the runtime MUST define a finite set of event types that cover at least: input changes, derived query evaluations, cache hits, cache invalidations, and errors. | |
| r[event.key-fields] | |
| Events describing inputs or derived queries MUST include enough key information to identify the corresponding ingredient and key within the runtime. | |
| r[event.query-changed-cutoff] | |
| Any “query changed” style event MUST reflect whether the *observable* result of a query has changed between revisions, not merely that recomputation occurred. | |
| ## Type erasure | |
| r[type-erasure.mechanism] | |
| Where the runtime erases concrete Rust types for storage in generic tables, it MUST do so using sound type-erasure mechanisms (e.g., `Any` or typemap-like indices) that prevent undefined behavior. | |
| r[type-erasure.purpose] | |
| Type erasure is used solely to support heterogeneous storage and unified APIs; it MUST NOT weaken the static type guarantees for user-facing query APIs. | |
| r[type-erasure.benefit] | |
| Type erasure SHOULD enable adding new kinds of ingredients or queries without changing existing runtime data structures. | |
| r[type-erasure.tradeoffs] | |
| The implementation MAY document performance or debuggability tradeoffs introduced by type erasure but MUST NOT change the observable semantics defined in this specification. | |
| ## Derived queries | |
| r[derived.type] | |
| A derived query is a pure function of its declared inputs and other derived queries, observed through the runtime’s memoization and dependency tracking semantics. | |
| r[derived.get] | |
| Calling the public “get” operation for a derived query MUST return a value or error consistent with an evaluation at the current revision under the dependency rules. | |
| r[derived.compute-fn] | |
| The compute function for a derived query MUST be invoked only under an active frame and MUST use runtime APIs to read inputs and other queries so dependencies are tracked. | |
| r[derived.memoization] | |
| Successful derived query results MAY be memoized; when inputs and dependencies are unchanged and no invalidation rules apply, subsequent gets MUST return the memoized value without re-running the compute function. | |
| ## Cells and cell state | |
| r[cell.compute] | |
| Each derived query evaluation operates in a logical cell that tracks the compute function, dependencies, and cached result for a specific key at a specific revision range. | |
| r[cell.access] | |
| Reading a cell’s value via the public API MUST either return the last verified value or trigger recomputation according to invalidation rules. | |
| r[cell.waiter] | |
| When multiple tasks concurrently request the same derived query and key, at most one task MUST act as the leader computing the value while others wait or follow according to the in-flight deduplication rules. | |
| r[cell.states] | |
| Cells MUST have well-defined states (e.g., empty, computing, valid, stale, poisoned); transitions between states MUST avoid data races and preserve correctness. | |
| r[cell.leader-local] | |
| Leader-specific state during computation (such as temporary buffers) MUST NOT be exposed to follower tasks or persisted beyond the lifetime of the active frame. | |
| r[cell.stale] | |
| A cell becomes stale when any of its recorded dependencies change; stale cells MUST be revalidated or recomputed before their result is considered current. | |
| r[cell.no-lock-await] | |
| Implementations MUST NOT hold locks across `await` points while computing a cell, to avoid deadlocks and priority inversions in async environments. | |
| r[cell.poison-scoped] | |
| If a cell enters a poisoned state due to a panic or unrecoverable error during computation, that poisoned state MUST be scoped to the specific cell and key and MUST NOT corrupt other cells. | |
| ## In-flight deduplication | |
| r[inflight.registry] | |
| The runtime MAY maintain an in-flight registry of currently computing derived query keys to deduplicate concurrent evaluations. | |
| r[inflight.purpose] | |
| In-flight deduplication MUST preserve observable semantics: followers observe the same result or error as if they had computed the query independently. | |
| r[inflight.key] | |
| The in-flight registry MUST key entries by at least the runtime instance, ingredient, and query key such that unrelated queries are not coalesced. | |
| r[inflight.scope] | |
| In-flight entries MUST be scoped to a single runtime instance and MUST NOT be shared across different runtime families unless snapshot sharing rules explicitly allow it. | |
| r[inflight.follower] | |
| Followers that attach to an in-flight computation MUST either await the leader’s result or, if the leader fails in a recoverable way, MAY be promoted to leaders according to implementation policy without violating correctness. | |
| r[inflight.complete] | |
| When a leader successfully completes computation, the in-flight entry MUST be resolved and any waiting followers MUST receive the same result. | |
| r[inflight.fail] | |
| If a leader fails with an error defined as recoverable, the in-flight entry MAY be retried according to implementation policy, but any observed result MUST still respect dependency and revision rules. | |
| r[inflight.cancel] | |
| Cancellation of a leader task MUST either propagate cancellation to followers or allow followers to re-issue the request; in either case, no follower may observe a partially computed result. | |
| r[inflight.try-lead] | |
| Attempts to become a leader MUST be race-safe; at most one task may win leadership for a given runtime/ingredient/key in the in-flight registry. | |
| r[inflight.shared-cache] | |
| Implementations MAY use a shared cache in addition to per-runtime memo tables; such a cache MUST NOT change observable semantics compared to a purely local cache. | |
| r[inflight.shared-cache-key] | |
| Entries in any shared cache MUST be keyed in a way that prevents collisions between logically distinct runtime families or incompatible kinds. | |
| r[inflight.shared-cache-size] | |
| Shared caches MAY evict entries for capacity reasons; eviction MUST NOT compromise correctness and only affect performance. | |
| r[inflight.shared-cache-adopt] | |
| A runtime instance MAY adopt a completed result from a shared cache in place of recomputing, provided that doing so respects revision and dependency constraints. | |
| ## Persistence | |
| r[persist.format] | |
| If the runtime supports persistence, the on-disk or serialized format MUST be documented and versioned so that incompatible changes can be detected. | |
| r[persist.structure] | |
| Persisted data MUST distinguish between different ingredient kinds, their keys, and their stored values or metadata. | |
| r[persist.section] | |
| The persistence format MAY divide data into logical sections (e.g., inputs, interned values, memo tables); each section MUST be self-consistent. | |
| r[persist.save-fn] | |
| The public save function MUST either successfully write a complete, self-consistent snapshot of the runtime’s persisted state or return an error. | |
| r[persist.save-options] | |
| Save operations MAY accept options (such as compression or filtering by ingredient kind), but these options MUST NOT lead to partially written or logically inconsistent data being reported as successful. | |
| r[persist.save-atomic] | |
| Where supported by the underlying storage, save operations SHOULD be atomic from the perspective of readers, so that no reader can observe a partially written image. | |
| r[persist.save-unique-kinds] | |
| The persistence format MUST uniquely identify each ingredient kind such that there is no collision between unrelated ingredients. | |
| r[persist.load-fn] | |
| The public load function MUST either reconstruct a runtime state consistent with the saved snapshot or return a descriptive error. | |
| r[persist.load-return] | |
| Loading MUST return a runtime instance or database handle that satisfies all runtime and revision invariants in this specification. | |
| r[persist.load-options] | |
| Load operations MAY accept options such as filtering or migration hooks, provided they do not violate the semantics of persisted inputs and interned values. | |
| r[persist.load-order] | |
| Loading MUST restore ingredients in an order that respects dependencies required to reconstruct derived memo tables or other derived state, if such state is persisted. | |
| r[persist.load-kind-match] | |
| On load, the persisted ingredient kinds MUST match the kinds declared by the program; mismatches MUST result in a load-time error. | |
| r[persist.load-name-match] | |
| If ingredient kinds are identified by names, the names in the persisted data MUST match the names expected by the running program or be rejected. | |
| r[persist.load-type-match] | |
| Persisted values MUST be type-compatible with the ingredient definitions in the running program; incompatible types MUST cause load to fail rather than producing undefined behavior. | |
| r[persist.not-stored] | |
| Ingredients or queries that are intentionally not persisted (e.g., transient caches) MUST be reinitialized to a valid empty state on load. | |
| r[persist.load-version] | |
| The persistence format version MUST be checked on load; incompatible versions MUST be rejected with an error that callers can surface or handle. | |
| ## Interned and input ingredients | |
| r[interned.type] | |
| An interned ingredient maps logically equal values to stable, compact identifiers, enabling fast equality comparisons and sharing. | |
| r[interned.id-type] | |
| Interned identifiers MUST be represented by copyable scalar types (such as integers or small newtypes) suitable for use as keys. | |
| r[interned.stability] | |
| Once assigned, an interned identifier for a given value MUST remain stable for the lifetime of the runtime family. | |
| r[interned.constraints] | |
| Interned ingredients MUST treat values as equal according to their `Eq` and `Hash` implementations; inconsistent implementations are user error and MAY be documented as such. | |
| r[interned.intern] | |
| The intern operation MUST return an existing identifier if the value has already been interned, otherwise it MUST create and return a new identifier. | |
| r[interned.get] | |
| Given a valid interned identifier, the runtime MUST be able to reconstruct or return the corresponding value for as long as the family remains alive. | |
| r[input.type] | |
| Inputs represent external, mutable data provided by the user; they MUST have well-defined keys and value types. | |
| r[input.constraints] | |
| Input updates MUST respect the declared key and value types and MUST be applied only through the runtime’s input APIs. | |
| r[input.revision-on-change] | |
| Any change to an input value that may affect derived queries MUST advance the runtime’s revision and mark dependent cells as stale. | |
| ## Kinds, keys, and dependencies | |
| r[kind.type] | |
| Each ingredient kind (input, derived, interned, etc.) MUST be identified by a unique type-level or runtime-level identifier within a runtime instance. | |
| r[kind.collision] | |
| The runtime MUST prevent or detect collisions between ingredient kind identifiers that would cause distinct kinds to be conflated. | |
| r[key.encoding] | |
| Keys used to index ingredients MUST have a deterministic encoding or hashing function that respects logical equality and is stable across the lifetime of the runtime process. | |
| r[key.dyn-key] | |
| Where dynamic keys are supported, the runtime MUST provide a uniform representation that allows safe storage and retrieval from type-erased tables. | |
| r[key.dep] | |
| Dependency edges MUST be tracked at the granularity of ingredient kind plus key, so that invalidation can be limited to precisely affected derived cells. | |
| r[revision.initial] | |
| A new runtime MUST start at a well-defined initial revision (such as 0 or 1) and treat that revision as the baseline for subsequent changes. | |
| r[revision.set] | |
| Only the runtime’s mutation APIs (such as input updates or administrative operations) MAY advance the current revision; user code MUST NOT set it directly. | |
| r[revision.verified-at] | |
| Derived cells MUST record the revision at which their value was last fully verified against dependencies. | |
| r[revision.changed-at] | |
| Inputs and other mutable ingredients SHOULD record the last revision at which their value changed, enabling efficient invalidation. | |
| r[dep.forward] | |
| For every dependency recorded during evaluation, there MUST be a forward edge from the caller to the callee that can be enumerated for invalidation. | |
| r[dep.reverse] | |
| Implementations MAY also maintain reverse edges (from callee to callers); if present, they MUST be kept consistent with forward edges and used for efficient invalidation. | |
| ## Snapshots | |
| r[snapshot.runtime-id] | |
| Snapshots MUST have an identity that ties them to their originating runtime family while still distinguishing them as separate runtime instances. | |
| r[snapshot.input] | |
| Inputs visible inside a snapshot MUST initially reflect the source runtime’s inputs at the bound revision and thereafter evolve independently. | |
| r[snapshot.derived] | |
| Derived queries inside a snapshot MUST be evaluated and memoized independently from the source, except where sharing optimizations explicitly preserve observable semantics. | |
| r[snapshot.frozen] | |
| Snapshots MAY be described as “frozen” with respect to the source: changes in the source after the snapshot’s creation MUST NOT affect the snapshot’s view of data. | |
| r[snapshot.independent] | |
| Mutations performed inside a snapshot (e.g., changing inputs if allowed) MUST NOT affect the source runtime instance. | |
| r[snapshot.multiple] | |
| Multiple snapshots MAY be created from the same source at different revisions; each snapshot MUST honor isolation with respect to both the source and other snapshots. | |
| r[snapshot.async] | |
| Creating or using snapshots in async or concurrent contexts MUST preserve the isolation and revision guarantees defined in this specification. | |
| ## Error handling | |
| r[error.result] | |
| Public query APIs MUST represent failure using explicit error results (such as `Result` types in Rust) rather than undefined behavior. | |
| r[error.type] | |
| Error types surfaced from the runtime MUST distinguish at least between user computation errors, cycle errors, persistence errors, and internal runtime failures where applicable. | |
| r[error.variants] | |
| Each error variant MUST carry sufficient information for callers to understand the cause (e.g., which query or ingredient failed, and why) without exposing internal invariants that could be invalidated. | |
| ## Debugging and tracing | |
| r[debug.graph] | |
| The runtime MAY expose APIs to inspect or export the dependency graph; any such view MUST reflect a consistent snapshot of dependencies at some revision. | |
| r[debug.cache-stats] | |
| Debugging APIs MAY include cache statistics (hits, misses, evictions); these MUST NOT affect query semantics. | |
| r[debug.trace-collector] | |
| A trace collector component MAY subscribe to runtime events for debugging; collectors MUST NOT be able to interfere with or modify runtime behavior. | |
| r[debug.trace-analysis] | |
| Trace analysis tools that operate on recorded runtime events MUST treat the event stream as observational and MUST NOT assume undocumented invariants. | |
| r[trace.crate] | |
| When integrating with a tracing crate or logging framework, the runtime MUST emit spans and events that correctly nest and correspond to evaluations and revisions. | |
| r[trace.no-subscriber] | |
| The runtime MUST behave correctly when no tracing subscriber or logger is installed; tracing hooks MUST degrade to no-ops without changing semantics. | |
| r[trace.levels] | |
| Trace and log levels (e.g., error, warn, info, debug, trace) SHOULD be used consistently so that users can control verbosity without losing critical error information. | |
| ## Macros and code generation | |
| r[macro.tracked.purpose] | |
| The `tracked` macro (or equivalent) MUST generate boilerplate for defining derived queries that integrate correctly with dependency tracking and memoization. | |
| r[macro.tracked.key-tuple] | |
| For tracked queries with multiple key fields, the macro MUST generate a key tuple or struct that implements the necessary traits for use as a map key. | |
| r[macro.tracked.return-wrap] | |
| The macro-generated APIs for tracked queries MUST wrap user computation results in the runtime’s standard result types (e.g., `Result`) without altering their semantics. | |
| r[macro.tracked.output] | |
| The macro MUST generate query output types and signatures that match the user’s annotated function and are compatible with the runtime’s storage and type-erasure mechanisms. | |
| r[macro.interned.purpose] | |
| The `interned` macro (or equivalent) MUST generate definitions that correctly integrate with the runtime’s intern tables and identifier types. | |
| r[macro.interned.output] | |
| Macro-generated interned APIs MUST expose operations to intern values and retrieve them by identifier consistent with the interned ingredient requirements. | |
| r[macro.input.purpose] | |
| The `input` macro (or equivalent) MUST generate boilerplate for declaring inputs that can be updated and observed through the runtime. | |
| r[macro.input.keyed] | |
| For keyed inputs, the macro MUST generate suitable key and value accessors and update APIs. | |
| r[macro.input.kind-id] | |
| Macro-generated inputs MUST register a unique ingredient kind identifier that matches the expectations of the runtime. | |
| r[macro.input.singleton] | |
| For singleton inputs, the macro MUST generate APIs that treat the input as a single value rather than a map, while still integrating with revision tracking. | |
| r[macro.db.purpose] | |
| The database or runtime-construction macros MUST generate a type that groups ingredients and exposes the standard user-facing APIs for inputs, derived queries, and snapshots. | |
| r[macro.db.snapshot] | |
| Macro-generated database types MUST provide methods to create snapshots that satisfy the snapshot requirements in this specification. | |
| r[macro.db.output] | |
| The output of database macros (types, methods, traits) MUST remain stable under minor macro implementation changes so long as the documented semantics are unchanged. |
|
|
||
| r[sharing.nonobservable] | ||
| Such sharing MUST NOT change observable behavior: the values and errors returned MUST be indistinguishable from a correct, non-sharing implementation that evaluates each runtime instance independently under the semantics above. | ||
|
|
There was a problem hiding this comment.
The PR description states "docs/spec/picante.md (~750 lines, ~90 requirements)" but the actual file is only 172 lines with approximately 25 requirements. This significant discrepancy between the description and the actual changes needs to be corrected. Either the spec file is incomplete and needs the additional ~580 lines and ~65 requirements to be added, or the PR description needs to be updated to reflect the actual scope of the changes.
| --- | |
| ## Document status and scope | |
| This version of the Picante semantics specification intentionally captures a subset of the full design. It currently contains on the order of a few dozen normative requirements (roughly 25), not the “~750 lines, ~90 requirements” that may have been mentioned in earlier design notes or PR descriptions. | |
| Any external text or PR description claiming that `docs/spec/picante.md` is ~750 lines long with ~90 requirements is obsolete and does **not** describe the current contents of this file. The scope and number of requirements in this document are defined solely by the text present here. | |
| Future extensions to Picante semantics (including additional requirements) MUST be added explicitly to this document or successor specs; they MUST NOT be assumed to exist based only on outdated summaries or line-count estimates. |
fasterthanlime
changed the title
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 18 out of 19 changed files in this pull request and generated 4 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -0,0 +1,12 @@ | |||
| spec { | |||
There was a problem hiding this comment.
The Tracey configuration file uses KDL syntax correctly. However, consider adding a comment at the top of the file explaining what Tracey is and how this configuration is used, to help other contributors understand its purpose.
| Picante is an incremental query runtime for Rust: you declare **inputs** and **derived queries**, and the runtime memoizes query results, tracks dependencies automatically, and recomputes only when the dependencies’ values change. | ||
|
|
||
| This document specifies **observable semantics**: what a user of the API can rely on (values, errors, and visibility across revisions/snapshots). It intentionally avoids prescribing implementation techniques, data structures, async primitives, logging/tracing backends, or performance tradeoffs. | ||
|
|
There was a problem hiding this comment.
The requirement anchors in this PR use the same format r[...] for both semantic requirements defined in the spec (like r[revision.type], r[input.set]) and implementation-specific details not in the spec (like r[runtime.components], r[event.channel]). While this is likely intentional for Tracey coverage tracking, consider adding a brief comment in the spec or README explaining this dual usage to avoid confusion for contributors who might expect all r[...] anchors to reference spec requirements.
| **Requirement anchors.** Throughout this document we use anchors of the form `r[...]` to label requirements for traceability. Some of these anchors correspond to normative semantic requirements defined in this spec (for example `r[revision.type]` or `r[input.set]`), while others mark implementation- or runtime-specific details that are not themselves normative semantics (for example `r[runtime.components]` or `r[event.channel]`). Using a single `r[...]` format for both kinds of anchors is intentional to support end-to-end coverage tracking. |
docs/spec/picante.md
Outdated
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observationally pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. | ||
|
|
||
| If a derived query reads external state without routing that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. |
There was a problem hiding this comment.
The specification uses "SHOULD" in the determinism contract, which indicates a recommendation rather than a requirement. However, the consequences of violating this contract (returning cached values that don't reflect actual dependencies) could be severe for correctness. Consider whether this should be a MUST requirement, or add explicit guidance about when it's acceptable to violate this contract.
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observationally pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. | |
| If a derived query reads external state without routing that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. | |
| For Picante’s caching semantics to be meaningful, derived query computations MUST be observationally pure with respect to the database state they read: the returned value MUST be a deterministic function of the values of the records they depend on. | |
| If a derived query reads external state without routing that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. This relaxation is only acceptable when such staleness is explicitly tolerated by the application; external state that affects correctness MUST be routed through an input ingredient so that it participates in dependency tracking. |
docs/spec/picante.md
Outdated
| r[derived.determinism] | ||
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observationally pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. | ||
|
|
||
| If a derived query reads external state without routing that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. |
There was a problem hiding this comment.
Minor clarity improvement: Consider rephrasing "without routing that state through an input ingredient" to "without first recording that state through an input ingredient" for better clarity about the mechanism.
| If a derived query reads external state without routing that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. | |
| If a derived query reads external state without first recording that state through an input ingredient (e.g., reading a file directly), the runtime MAY return cached values that do not reflect changes in that external state until some input change causes recomputation. |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 18 out of 19 changed files in this pull request and generated 22 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| --- | ||
|
|
||
| # Sharing optimizations (non-observable) |
There was a problem hiding this comment.
Inconsistent header level. This section "# Sharing optimizations (non-observable)" should be a second-level header "## Sharing optimizations (non-observable)" to maintain consistent document structure with other major sections.
| # Sharing optimizations (non-observable) | |
| ## Sharing optimizations (non-observable) |
|
|
||
| let cache: CacheFile = decode_cache_file(&bytes)?; | ||
|
|
||
| // r[persist.load-version] |
There was a problem hiding this comment.
Requirement anchors reference non-existent spec requirements. The persist.rs file contains multiple anchors (e.g., "r[persist.format]", "r[persist.load-version]", "r[persist.structure]", "r[persist.not-stored]", etc.) that don't exist in the spec document. The spec intentionally doesn't cover persistence implementation details, so these anchors create broken references in the coverage tracking system. Consider using a different prefix for implementation notes that aren't part of the semantic specification.
| // r[persist.load-version] | |
| // impl[persist.load-version] |
| use facet::Facet; | ||
|
|
||
| // r[revision.type] | ||
| // r[revision.monotonic] |
There was a problem hiding this comment.
Requirement anchor references non-existent spec requirement. The code references "r[revision.monotonic]" but this requirement anchor does not exist in the spec document (docs/spec/picante.md). The spec defines "r[revision.type]" and "r[revision.order]" but not "r[revision.monotonic]". Consider either adding this requirement to the spec or removing this anchor.
| // r[revision.monotonic] | |
| // r[revision.order] |
| // r[trace.crate] | ||
| // r[trace.no-subscriber] | ||
| // r[trace.levels] |
There was a problem hiding this comment.
Requirement anchors reference non-existent spec requirements. The anchors "r[trace.crate]", "r[trace.no-subscriber]", and "r[trace.levels]" don't exist in the spec document. The spec intentionally doesn't cover tracing/logging implementation details, so these anchors create broken references. Consider using a different prefix for implementation notes.
| // r[trace.crate] | |
| // r[trace.no-subscriber] | |
| // r[trace.levels] | |
| // impl[trace.crate] | |
| // impl[trace.no-subscriber] | |
| // impl[trace.levels] |
| entries.get(&dyn_key).map(|e| e.changed_at) | ||
| } | ||
|
|
||
| // r[snapshot.input] |
There was a problem hiding this comment.
Requirement anchors reference non-existent spec requirements. The input.rs file contains anchors (e.g., "r[input.constraints]", "r[input.type]", "r[input.revision-on-change]", "r[snapshot.input]") that don't exist in the spec document. While "r[input.set]", "r[input.remove]", and "r[input.get]" do exist in the spec, the others appear to be implementation details. Consider using a different prefix for implementation notes.
| // r[snapshot.input] | |
| // impl[snapshot.input] |
|
|
||
| --- | ||
|
|
||
| # Core Semantics |
There was a problem hiding this comment.
Inconsistent header level. The document has a top-level header "# Picante Semantics Specification" and then second-level sections like "## Model and Terms". This section "# Core Semantics" should be a second-level header "## Core Semantics" to maintain consistent document structure.
| # Core Semantics | |
| ## Core Semantics |
|
|
||
| --- | ||
|
|
||
| # Snapshots |
There was a problem hiding this comment.
Inconsistent header level. This section "# Snapshots" should be a second-level header "## Snapshots" to maintain consistent document structure with other major sections.
docs/spec/picante.md
Outdated
| ### Determinism contract | ||
|
|
||
| r[derived.determinism] | ||
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observationally pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. |
There was a problem hiding this comment.
Terminology inconsistency. The term "observationally" is used here, but earlier in line 3 the phrase "observable semantics" is used. Consider using "observably pure" for consistency with the document's focus on "observable semantics" and "observable behavior".
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observationally pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. | |
| For Picante’s caching semantics to be meaningful, derived query computations SHOULD be observably pure with respect to the database state they read: the returned value SHOULD be a deterministic function of the values of the records they depend on. |
| /// Global counter for assigning unique runtime IDs. | ||
| static RUNTIME_ID_COUNTER: AtomicU64 = AtomicU64::new(1); | ||
|
|
||
| // r[snapshot.runtime-id] |
There was a problem hiding this comment.
Requirement anchor references non-existent spec requirement. The code references "r[snapshot.runtime-id]" but this requirement anchor does not exist in the spec document (docs/spec/picante.md). The spec defines snapshot-related requirements like "r[snapshot.creation]", "r[snapshot.isolation]", etc., but not "r[snapshot.runtime-id]". Consider either adding this requirement to the spec or removing this anchor.
| // r[snapshot.runtime-id] | |
| // Runtime identifier shared between a database and its snapshots. |
| V: Send + Sync + 'static, | ||
| { | ||
| fn compute<'a>(&'a self, db: &'a DB, key: Key) -> ComputeFut<'a> { | ||
| // Tradeoffs: vtable dispatch, boxed future allocation, and key decode per compute. |
There was a problem hiding this comment.
Comment contains an incomplete sentence fragment. The comment "Tradeoffs: vtable dispatch, boxed future allocation, and key decode per compute." should be expanded to a complete sentence, such as "Tradeoffs include vtable dispatch, boxed future allocation, and key decode per compute." for better documentation clarity.
| // Tradeoffs: vtable dispatch, boxed future allocation, and key decode per compute. | |
| // Tradeoffs include vtable dispatch, boxed future allocation, and key decode per compute. |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 18 out of 19 changed files in this pull request and generated 24 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // ... | ||
| # let _ = (db, item, label); | ||
| # Ok(false) |
There was a problem hiding this comment.
These test-related hidden lines (prefixed with #) appear in what should be a normative example. Consider either removing these lines or replacing them with actual implementations, or clearly marking this section as non-normative example code.
| // ... | |
| # let _ = (db, item, label); | |
| # Ok(false) | |
| // Example implementation omitted; any body is allowed here. | |
| todo!() |
| .collect() | ||
| } | ||
|
|
||
| // r[runtime.propagate-invalidation] |
There was a problem hiding this comment.
Multiple requirement anchors reference requirements that do not exist in the specification: r[runtime.components], r[runtime.new], r[runtime.notify-input-set], r[runtime.update-deps], r[runtime.clear-deps], and r[runtime.propagate-invalidation]. These anchors suggest implementation details that may be out of scope for the semantics-only specification, but they should either be removed, changed to reference existing requirements, or the specification should be updated to include these implementation-level requirements if they are considered important.
| // r[runtime.propagate-invalidation] |
| // r[type-erasure.purpose] | ||
| // r[type-erasure.benefit] |
There was a problem hiding this comment.
The requirement anchors r[type-erasure.mechanism], r[type-erasure.tradeoffs], r[type-erasure.purpose], and r[type-erasure.benefit] reference requirements that do not exist in the specification. Type erasure is an implementation technique and not part of observable semantics. These anchors should be removed unless there's a plan to document implementation patterns separately from semantic requirements.
| // r[type-erasure.purpose] | |
| // r[type-erasure.benefit] |
| // r[derived.get] | ||
| // r[cell.access] |
There was a problem hiding this comment.
The requirement anchors r[derived.compute-fn], r[derived.type], r[derived.memoization], r[derived.get], and r[cell.access] reference requirements that do not exist in the specification. While the spec covers derived query semantics (e.g., r[derived.revision-binding], r[derived.concurrent]), these specific implementation-level anchors should be mapped to existing semantic requirements or removed.
| // r[derived.get] | |
| // r[cell.access] |
| ) -> picante::PicanteResult<std::sync::Arc<Vec<u8>>> { | ||
| // Read from disk here; `hash` is part of the key so changing it forces a new cached entry. | ||
| // If you care about correctness in the presence of races (e.g. a stale watcher digest or | ||
| // TOCTOU), validate that the bytes you read actually match `hash` and return an error if not. |
There was a problem hiding this comment.
The comment at the end uses "TOCTOU" (Time-of-Check-Time-of-Use) acronym without defining it. While this is a well-known security term, for specification documentation clarity, consider either spelling it out on first use or providing a brief explanation.
| // TOCTOU), validate that the bytes you read actually match `hash` and return an error if not. | |
| // a time-of-check-to-time-of-use (TOCTOU) race), validate that the bytes you read actually match `hash` and return an error if not. |
| } | ||
|
|
||
| // r[input.set] | ||
| // r[input.revision-on-change] |
There was a problem hiding this comment.
The requirement anchors r[input.constraints], r[input.type], and r[input.revision-on-change] reference requirements that do not exist in the specification. The spec does define r[input.get], r[input.set], r[input.remove], and r[input.slot], so these implementation-level anchors should either be mapped to those existing requirements or removed if they represent implementation choices.
| // r[input.revision-on-change] |
| ) -> PicanteResult<Arc<Vec<u8>>> { | ||
| // Read the file at `path` and return its bytes. | ||
| // `hash` is part of the query key: changing it forces a different cached entry. | ||
| # let _ = (path, hash); |
There was a problem hiding this comment.
This line contains a Rust test comment syntax (using #) that appears out of context. The # let _ = (path, hash); is typically used to hide lines in rustdoc examples, but here it seems unnecessary or potentially confusing. Consider either removing this line entirely or making it a regular comment if the explanation is needed.
| # let _ = (path, hash); |
| db: &DB, | ||
| key: ItemLabelKey, | ||
| ) -> PicanteResult<bool> { | ||
| # let _ = (db, key); |
There was a problem hiding this comment.
Test-related hidden line appears in specification example code. Same issue as previous comments - this should either be removed or converted to regular code if this is meant to be a complete example.
| # let _ = (db, key); |
| // Read from disk here; `hash` is part of the key so changing it forces a new cached entry. | ||
| // If you care about correctness in the presence of races (e.g. a stale watcher digest or | ||
| // TOCTOU), validate that the bytes you read actually match `hash` and return an error if not. | ||
| let bytes: Vec<u8> = /* read bytes for `path` */; |
There was a problem hiding this comment.
This comment contains a continuation line that should be removed to improve clarity. The comment should stand on its own without the "// ..." placeholder, or provide actual implementation if needed for the example.
| let bytes: Vec<u8> = /* read bytes for `path` */; | |
| let bytes: Vec<u8> = std::fs::read(&path)?; |
| // r[key.equality] | ||
| impl PartialEq for Key { | ||
| fn eq(&self, other: &Self) -> bool { | ||
| // exact byte equality, not hash |
There was a problem hiding this comment.
The comment "exact byte equality, not hash" is redundant because the next line clearly compares self.bytes == other.bytes. This comment doesn't add meaningful clarification and can be removed to reduce noise.
| // exact byte equality, not hash |
Summary
Adds a semantics-only specification for Picante (focused on observable behavior), plus Tracey configuration and
r[...]requirement anchors to track coverage.Why
The earlier spec draft was written backwards from the current implementation and leaned heavily on implementation details. This PR pivots the spec to describe the properties and guarantees we want first (values/errors/visibility across revisions and snapshots), so we can align the implementation to it.
Changes
docs/spec/picante.md: semantics-only spec (revisions + scope, inputs, derived queries, dependency recording, revalidation/early cutoff, cycles, snapshots, and non-observable sharing rules)..config/tracey/config.kdl: Tracey config for spec coverage tracking.// r[... ]) across runtime/ingredients/macros/persistence to map implementation to spec requirements.Notes
Test plan
cargo fmtcargo check -p picante -p picante-macros