aver/types/
trace.rs

1//! Trace — opaque builtin exposing a function's structural trace in
2//! verify-trace assertions.
3//!
4//! In Oracle v1, `fn.trace` returns a `Trace` value representing the
5//! sequence of effect emissions that occurred during an evaluation of
6//! `fn` under a verify-law's stub bindings. Users query it via:
7//!
8//! - `.event(k) : Option<EffectEvent>` — event at position k
9//! - `.length() : Int` — number of events
10//! - `.contains(event) : Bool` — does trace contain this exact event
11//! - `.contains(effect_ref) : Bool` — any event with this effect type
12//!
13//! Navigation primitives (`.group(N)`, `.branch(idx)`, `.path()`) and
14//! the replay-bridge methods follow in later commits.
15//!
16//! Internal representation: a record `{ events: List<EffectEvent> }`.
17//! User code never constructs Trace values directly — they materialize
18//! only as the result of `fn.trace` in verify-trace context.
19
20use crate::nan_value::Arena;
21
22pub const TYPE_NAME: &str = "Trace";
23pub const FIELD_EVENTS: &str = "events";
24
25pub fn register(arena: &mut Arena) {
26    arena.register_record_type(TYPE_NAME, vec![FIELD_EVENTS.into()]);
27}
28
29#[cfg(test)]
30mod tests {
31    use super::*;
32
33    #[test]
34    fn trace_type_registers_with_events_field() {
35        let mut arena = Arena::new();
36        register(&mut arena);
37        assert!(arena.find_type_id(TYPE_NAME).is_some());
38    }
39}
aver/types/trace.rs

aver/types/
trace.rs
