Realtime audio meter

This example is a proof recipe for the #[realtime] claim. Its passing file is a standalone audio-style hot path that cpc check accepts without imports. The real-time package in the C+ source tree supplies the same bounded building blocks for applications: vendor/rt/src/rt.cplus ships SpscRingU64, and vendor/rt/src/pool.cplus ships FixedPoolU64. Their hot-path methods are annotated #[no_alloc] and #[no_block].

The important property is not the audio math. The important property is that the compiler rejects code paths that would allocate, block, or exceed the stack budget before the callback can ship.

Claim	How this example checks it
#[realtime] accepts arithmetic-only hot paths	passing.cplus checks cleanly
allocation is rejected	bad/alloc.cplus reports E0901
blocking is rejected	bad/block.cplus reports E0907
oversized stack frames are rejected	bad/stack.cplus reports E0908

Compiler-backed evidence

The source tree has two layers of evidence behind this recipe:

Evidence	What it proves
vendor/rt/src/rt.cplus	SpscRingU64::new, count, is_empty, is_full, push, and pop are fixed-capacity, nonblocking, allocation-free operations marked #[no_alloc] #[no_block]
vendor/rt/src/pool.cplus	FixedPoolU64 provides an allocation-free fixed pool with acquire, release, get, and set marked #[no_alloc] #[no_block]
cpc/tests/e2e.rs	compiler tests reject allocation with E0901, blocking calls with E0907, oversized frames with E0908, and JSON realtime reports with nonzero exit on violations

Representative E2E test names include realtime_profile_rejects_local_allocation, realtime_profile_clean_program_passes, no_alloc_rejects_allocating_method_through_receiver, no_alloc_allows_marked_method_through_receiver, no_alloc_rejects_to_string, no_block_rejects_blocking_method_through_receiver, realtime_report_json_flags_violations, and realtime_report_clean_exits_zero.

Project layout

realtime_meter/
├── passing.cplus
└── bad/
    ├── alloc.cplus
    ├── block.cplus
    └── stack.cplus

Passing callback

The callback reads a block of samples through explicit pointers, applies a gain, writes the output, and returns the peak. It allocates nothing and has no operation that can wait.

const GAIN: f32 = 0.80f32;

#[realtime]
fn abs_f32(x: f32) -> f32 {
    if x < 0.0f32 { return 0.0f32 - x; }
    return x;
}

#[realtime]
#[max_stack(1024)]
fn process_audio(n: usize, restrict input: *f32,
        restrict output: *f32) -> f32 {
    var i: usize = 0usize;
    var peak: f32 = 0.0f32;

    while i < n {
        let y: f32 = input[i] * GAIN;
        output[i] = y;

        let a: f32 = abs_f32(y);
        if a > peak { peak = a; }

        i = i +% 1usize;
    }
    return peak;
}

fn main() -> i32 {
    var input: [f32; 8] = [0.10f32, -0.20f32, 0.30f32, -0.40f32,
        0.25f32, -0.50f32, 0.75f32, -1.00f32];
    var output: [f32; 8] = [0.0f32; 8];
    let peak: f32 = process_audio(8usize, #addr_of(input[0]),
        #addr_of(output[0]));
    if peak == 1.0f32 { return 0; }
    return 1;
}

For an application that publishes the peak to another thread, the rt package follows the same rule. SpscRingU64::push checks capacity and returns false when full; it never waits:

#[no_alloc] #[no_block]
fn push(ref this, v: u64) -> bool {
    let head: u64 = { atomic::load_u64(#addr_of(this._head), atomic::Ordering::Acquire) };
    let tail: u64 = { atomic::load_u64(#addr_of(this._tail), atomic::Ordering::Relaxed) };
    if (tail -% head) >= (1024 as u64) {
        return false;
    }
    let idx: usize = (tail % (1024 as u64)) as usize;
    this._buf[idx] = v;
    { atomic::store_u64(#addr_of(this._tail), tail +% (1 as u64), atomic::Ordering::Release); }
    return true;
}

FixedPoolU64::acquire uses the same contract style: bounded state, no heap, and failure as a value instead of a wait.

#[no_alloc] #[no_block]
fn acquire(ref this) -> option::Option[u32] {
    if this.free_head == pool_none() {
        return option::Option[u32]::None;
    }
    let idx: u32 = this.free_head;
    this.free_head = this.links[idx as usize];
    this.in_use = this.in_use +% (1 as usize);
    return option::Option[u32]::Some(idx);
}

Negative fixture: allocation

This fixture calls an allocator directly. The compiler rejects it inside the realtime contract before a binary is produced.

extern fn malloc(n: usize) -> *u8;

#[realtime]
fn process_bad_alloc() -> i32 {
    let p: *u8 = malloc(16usize);
    if p.is_null() { return 1; }
    return 0;
}

fn main() -> i32 { return process_bad_alloc(); }

Expected diagnostic shape:

bad/alloc.cplus:5:18: error[E0901]: function `process_bad_alloc` is marked `#[no_alloc]` but calls allocating function `malloc`

Negative fixture: blocking

The callback cannot sleep, wait on a timer, block on a mutex, join a thread, or perform blocking I/O. This fixture should be rejected with E0907.

#[no_alloc]
extern fn sleep(seconds: u32) -> u32;

#[realtime]
fn process_bad_block() -> i32 {
    let _rc: u32 = sleep(1u32);
    return 0;
}

fn main() -> i32 { return process_bad_block(); }

Expected diagnostic shape:

bad/block.cplus:6:20: error[E0907]: function `process_bad_block` is marked `#[no_block]` but calls blocking function `sleep`

Negative fixture: stack budget

Large locals are visible to #[max_stack]. This fixture intentionally exceeds a small budget.

#[realtime]
#[max_stack(256)]
fn process_bad_stack() -> i32 {
    let scratch: [u8; 2048] = [0u8; 2048];
    return scratch[0] as i32;
}

fn main() -> i32 { return process_bad_stack(); }

Expected diagnostic shape:

bad/stack.cplus:2:1: error[E0908]: function `process_bad_stack` stack frame exceeds 256 bytes

Reproduce

cpc check passing.cplus
cpc check bad/alloc.cplus --diagnostics=json
cpc check bad/block.cplus --diagnostics=json
cpc check bad/stack.cplus --diagnostics=json

The first command should pass. The three bad/ commands should fail, and the JSON diagnostics should include E0901, E0907, and E0908 respectively.

That is the proof boundary: the claim is not "the programmer remembered not to allocate." The claim is that the compiler rejects the callback if allocation, blocking, or an oversized frame becomes reachable. The public recipe is small, but the backing checks live in the compiler suite and in the rt package source.