Lesson 56. Design by Contract in embedded C

1. Today's topic

Design by Contract formalises system rules directly in code:

precondition: what the caller must satisfy
postcondition: what the function guarantees after success
invariant: what is always true in a stable object state

The main idea: an assertion does not check the outside world. It catches a violation of an internal promise made by the program.

2. Why this matters

For EC25, an invariant:

transaction_active == false -> active_command == NONE
transaction_active == true -> transaction_id != 0

For the phase FSM:

RED && GREEN -> quality == CONFLICT
input_stale -> quality != VALID
off_threshold < on_threshold

For DMA:

CPU_OWNED and DMA_OWNED cannot both be true at the same time

The same invariant checker is used in production, unit tests, fuzzing and replay.

3. Theory

Four classes of errors

A. Untrusted external input:

invalid MQTT payload, CAN CRC error, an excessively long AT line

Response: reject/error/resynchronise, not assert. B. Expected runtime failure:

EC25 failed to register, DNS timeout, CAN bus-off

Response: FSM recovery, retry/backoff. C. Internal contract violation:

double free buffer, ONLINE without registration, retry_count > limit

Response: contract fault. D. Loss of a safe state:

the output state or correctness of phase data cannot be guaranteed

Response: enter a safe state, latch the fault, then perform controlled recovery/reboot.

Invariant checker

typedef enum {
    MODEM_INV_OK = 0,
    MODEM_INV_NULL,
    MODEM_INV_COMMAND_WITHOUT_TRANSACTION,
    MODEM_INV_MQTT_WITHOUT_ONLINE_MODEM,
    MODEM_INV_RETRY_OVERFLOW,
} modem_invariant_result_t;
static modem_invariant_result_t modem_invariants_check(const modem_core_t *m)
{
    if (m == NULL) return MODEM_INV_NULL;
    if (!m->transaction_active && m->active_command != MODEM_COMMAND_NONE)
        return MODEM_INV_COMMAND_WITHOUT_TRANSACTION;
    if (m->mqtt_state == MQTT_STATE_CONNECTED && m->state != MODEM_STATE_ONLINE)
        return MODEM_INV_MQTT_WITHOUT_ONLINE_MODEM;
    if (m->retry_count > m->policy.retry_limit)
        return MODEM_INV_RETRY_OVERFLOW;
    return MODEM_INV_OK;
}

Check before and after handle_event().

Compile-time contracts

_Static_assert(SPSC_CAPACITY != 0U &&
               (SPSC_CAPACITY & (SPSC_CAPACITY - 1U)) == 0U,
               "SPSC capacity must be a nonzero power of two");

_Static_assert((SPSC_CAPACITY & (SPSC_CAPACITY - 1U)) == 0U,
               "SPSC capacity must be power of two");

Assertions without side effects

Incorrect:

assert(queue_pop(&queue, &item));

Correct:

bool popped = queue_pop(&queue, &item);
APP_INVARIANT(popped);

Fail-fast does not mean an instant reboot

The correct path:

contract violation -> capture minimal state -> safe-state -> fault record -> controlled abort/reboot or local recovery

4. Common mistakes

1. Using an assertion on external MQTT/UART input.
2. Using ESP_ERROR_CHECK() for a network timeout.
3. Continuing execution after a “should never happen” condition.
4. Using assertions with side effects.
5. Checking only ptr != NULL, without logical invariants.
6. Using different invariant functions for production/fuzz/replay.
7. Using one giant invariant without a specific violation ID.
8. Taking a mutex or writing NVS from an ISR contract handler.
9. Checking an expensive O(N) invariant for every ADC sample.
10. Disabling all critical checks in a release.
11. Treating the watchdog as a replacement for assertions.
12. Treating assertions as a replacement for normal error handling.
13. Using default: break for an impossible enum state.

5. Practical task

Implement modem_invariants_check() and call it on entry to and exit from the modem event handler. Add an intentional bug: on AT_OK, clear transaction_active=false but do not clear active_command. The invariant should immediately report MODEM_INV_COMMAND_WITHOUT_TX. Add _Static_assert for buffer sizes:

_Static_assert(MODEM_MAX_AT_COMMAND_LENGTH < MODEM_TX_BUFFER_SIZE,
               "AT command can overflow TX buffer");

Then connect the same checker to the fuzz target and replay runner.

6. What to try next

• Separate contract levels: critical always-on, normal debug and deep audit.
• Store contract ID, state, transaction ID, configuration generation and boot ID in the production fault record.
• Use separate types for remote commands: raw_command_t, verified_command_t and authorized_command_t.