WCET analysis for verified engines: prove bounded execution time for all Relay components

[avrabe]

Context

The Spar AADL model for Wohl specifies WCET bounds (e.g., WaterLeakMonitor: 1ms, TemperatureMonitor: 2ms). These are estimates. For safety-critical deployment (ASIL-D, DAL-A), WCET must be PROVEN, not estimated.

What needs proving

For each verified engine:

• relay-lc: evaluate() iterates MAX_WATCHPOINTS (128) × compare() = bounded
• relay-sch: process_tick() iterates MAX_SCHEDULE_SLOTS (256) × match check = bounded
• relay-sc: process_tick() iterates ATS (256) + RTS (16×64) = bounded
• relay-hk: collect() iterates MAX_COPY_ENTRIES (128) × byte copy = bounded
• relay-cs: check_batch() iterates MAX_REGIONS (64) × CRC32 = bounded

All loops have decreases clauses (Verus proves termination). What's missing: cycle-count bounds.

Approach

1. Verus decreases → loop bound extraction

Each loop already has a Verus-proven decreases clause. Extract the maximum iteration count as a const.

2. Per-instruction cycle cost model

For Synth-compiled ARM Thumb-2:

• Compare: 1 cycle
• Branch: 1-3 cycles
• Memory load: 1-2 cycles (TCM) or 2-5 cycles (SRAM)
• Array index: 2-3 cycles

3. WCET formula

WCET = max_iterations × per_iteration_cycles + setup + teardown

For relay-lc evaluate():
WCET = 128 × ~20 cycles + 10 = ~2570 cycles
At 480MHz (STM32H7): ~5.4μs. Well under 1ms deadline.

4. Lean proof of WCET bound

Formalize the cycle cost model in Lean, prove the WCET formula, connect to the Verus loop bounds.

Connects to

• Spar AADL timing analysis (wohl_system.aadl thread WCET properties)
• Gale scheduler (SC01-SC16) for preemption analysis