sim/runtime/reference_device/
two_rate.rs

1use sim_kernel::{Expr, Result, Symbol};
2use sim_lib_stream_device::seq_is_monotone;
3use sim_lib_view_device::{
4    AdapterInput, AdapterLoop, FrameClock, GlanceAdapter, GlanceBudget, GlanceInput, GlanceState,
5    StalePolicy,
6};
7use sim_value::build;
8
9use super::{
10    ReferencePose, ReferenceRichAdapter, ReferenceSceneEncoder, reference_caps_source,
11    reference_glance_profile, reference_rich_profile,
12};
13
14/// Result of the hardware-free two-rate proof.
15#[derive(Clone, Debug, PartialEq, Eq)]
16pub struct TwoRateProof {
17    /// Number of content encoder calls.
18    pub encoder_calls: u64,
19    /// Rich loop drop count from coalesced modeled samples.
20    pub rich_dropped: u32,
21    /// Whether the rich loop marks a stale sample.
22    pub rich_stale: bool,
23    /// Compact glance budget cells.
24    pub glance_cells: u8,
25    /// Compact glance ack channel token.
26    pub glance_ack: Symbol,
27    /// Whether the modeled capability stream is monotone.
28    pub modeled_stream_monotone: bool,
29}
30
31impl TwoRateProof {
32    /// Encodes the proof as expression data for cookbook recipes.
33    pub fn to_expr(&self) -> Expr {
34        build::map(vec![
35            ("kind", build::qsym("device/reference", "two-rate-proof")),
36            ("encoder-calls", build::uint(self.encoder_calls)),
37            ("rich-dropped", build::uint(u64::from(self.rich_dropped))),
38            ("rich-stale", Expr::Bool(self.rich_stale)),
39            ("glance-cells", build::uint(u64::from(self.glance_cells))),
40            ("glance-ack", Expr::Symbol(self.glance_ack.clone())),
41            (
42                "modeled-stream-monotone",
43                Expr::Bool(self.modeled_stream_monotone),
44            ),
45        ])
46    }
47}
48
49/// Runs the two-rate modeled timing proof.
50pub fn prove_two_rate() -> Result<TwoRateProof> {
51    let rich_profile = reference_rich_profile();
52    let glance_profile = reference_glance_profile();
53    let mut encoder = ReferenceSceneEncoder::new();
54    let encoded = encoder.encode();
55    let shared_scene = encoded.shared();
56
57    let mut rich_loop = AdapterLoop::new(ReferenceRichAdapter, StalePolicy::Predict);
58    rich_loop.offer(&ReferencePose::new(1, 100));
59    rich_loop.offer(&ReferencePose::new(2, 250));
60    rich_loop.offer(&ReferencePose::new(3, 500));
61    let rich_input = AdapterInput::new(encoded.clone(), 1, ReferencePose::new(3, 500), 3);
62    let fresh = rich_loop.step(
63        &FrameClock::new(3, rich_profile.rate),
64        &rich_input,
65        &rich_profile,
66    )?;
67
68    let stale_input =
69        AdapterInput::from_shared_scene(shared_scene, 1, ReferencePose::new(3, 500), 3);
70    let stale = rich_loop.step(
71        &FrameClock::new(200, rich_profile.rate),
72        &stale_input,
73        &rich_profile,
74    )?;
75
76    let budget = GlanceBudget::mono_hud();
77    let glance_adapter = GlanceAdapter::new(budget, 25);
78    let mut glance_loop = AdapterLoop::new(glance_adapter, StalePolicy::HoldLast);
79    glance_loop.offer(&GlanceState::with_input(GlanceInput::Tap, 4));
80    let glance_input =
81        AdapterInput::new(encoded, 1, GlanceState::with_input(GlanceInput::Tap, 4), 4);
82    let _glance = glance_loop.step(
83        &FrameClock::new(4, glance_profile.rate),
84        &glance_input,
85        &glance_profile,
86    )?;
87
88    Ok(TwoRateProof {
89        encoder_calls: encoder.calls(),
90        rich_dropped: fresh.dropped,
91        rich_stale: stale.stale,
92        glance_cells: budget.cells,
93        glance_ack: budget.ack.to_symbol(),
94        modeled_stream_monotone: seq_is_monotone(&reference_caps_source(), 0, 4),
95    })
96}
sim/runtime/reference_device/two_rate.rs

sim/runtime/reference_device/
two_rate.rs
