sample = {
  object,       // 哪个器件、外设、实例和字段
  value,        // 本次读回值
  moment,       // 启动前、运行中、暂停后、IRQ 入口等
  observer,     // IDE 自动刷新、脚本、固件只读快照等
  semantics,    // 静态、易变、读取清除、写清除、数据端口……
  conditions    // CPU/外设是否暂停，时钟、错误和工具版本
}

假设 H0：TIM2 没有运行
预期链：
  RCC 门控已开
  -> TIM2 PSC/ARR 与设计一致
  -> 启动前 CEN=0
  -> 启动后 CEN=1
  -> 自由运行条件下两个有序 CNT 样本不同
  -> update 事件使 UIF 或回调计数发生变化
  -> 由已知 TIM2CLK、PSC、ARR 推导的周期与独立测量相符

HSI = 16 MHz
  -> PLLM = 16，PLL 输入 = 1 MHz
  -> PLLN = 336，VCO = 336 MHz
  -> PLLP = 2，SYSCLK = 168 MHz
  -> AHB HPRE = /1，HCLK = 168 MHz
  -> APB1 PPRE1 = /4，PCLK1 = 42 MHz
  -> APB1 预分频不为 1，F407 TIM2CLK = 2 * PCLK1 = 84 MHz
  -> RCC_APB1ENR.TIM2EN = 1
  -> TIM2 PSC = 8399，计数 tick = 84 MHz / 8400 = 10 kHz
  -> TIM2 ARR = 9，update 频率 = 10 kHz / 10 = 1 kHz

f_update = f_TIM2CLK / (PSC + 1) / (ARR + 1)

RCC_CR.HSION -> 等待 HSIRDY
  -> 配置 RCC_PLLCFGR
  -> RCC_CR.PLLON -> 等待 PLLRDY
  -> 配置 FLASH latency、HPRE、PPRE1、PPRE2
  -> RCC_CFGR.SW 选择 PLL -> 检查 SWS
  -> RCC_APB1ENR.TIM2EN = 1
  -> 如需恢复已知初态：TIM2RST 置 1 后释放为 0
  -> 写 TIM2 PSC/ARR/EGR/DIER/CR1
  -> CR1.CEN = 1 后才开始计数

#include "stm32f4xx_hal.h"
#include <stdint.h>

typedef enum {
    PROBE_OK = 0,
    PROBE_ERR_CLOCK = 1,
    PROBE_ERR_TIM_INIT = 2,
    PROBE_ERR_TIM_START = 3,
    PROBE_ERR_TIM_STOP = 4
} probe_status_t;

typedef struct {
    uint32_t sequence;
    uint32_t tick_ms;
    uint32_t rcc_apb1enr;
    uint32_t dbgmcu_apb1_fz;
    uint32_t tim_cr1;
    uint32_t tim_dier;
    uint32_t tim_sr;
    uint32_t tim_psc;
    uint32_t tim_arr;
    uint32_t tim_cnt;
    uint32_t update_callback_count;
} probe_tim2_snapshot_t;

static TIM_HandleTypeDef g_htim2;
static volatile uint32_t g_tim2_update_count;
static uint32_t g_snapshot_sequence;

static probe_status_t SystemClock_Config_Reference(void)
{
    RCC_OscInitTypeDef osc = {0};
    RCC_ClkInitTypeDef clk = {0};

    /* 执行前提：已从板级资料确认 VDD=2.7..3.6 V。 */
    __HAL_RCC_PWR_CLK_ENABLE();
    __HAL_PWR_VOLTAGESCALING_CONFIG(PWR_REGULATOR_VOLTAGE_SCALE1);

    osc.OscillatorType = RCC_OSCILLATORTYPE_HSI;
    osc.HSIState = RCC_HSI_ON;
    osc.HSICalibrationValue = RCC_HSICALIBRATION_DEFAULT;
    osc.PLL.PLLState = RCC_PLL_ON;
    osc.PLL.PLLSource = RCC_PLLSOURCE_HSI;
    osc.PLL.PLLM = 16U;
    osc.PLL.PLLN = 336U;
    osc.PLL.PLLP = RCC_PLLP_DIV2;
    osc.PLL.PLLQ = 7U;
    if (HAL_RCC_OscConfig(&osc) != HAL_OK) {
        return PROBE_ERR_CLOCK;
    }

    clk.ClockType = RCC_CLOCKTYPE_SYSCLK | RCC_CLOCKTYPE_HCLK |
                    RCC_CLOCKTYPE_PCLK1 | RCC_CLOCKTYPE_PCLK2;
    clk.SYSCLKSource = RCC_SYSCLKSOURCE_PLLCLK;
    clk.AHBCLKDivider = RCC_SYSCLK_DIV1;
    clk.APB1CLKDivider = RCC_HCLK_DIV4;
    clk.APB2CLKDivider = RCC_HCLK_DIV2;
    if (HAL_RCC_ClockConfig(&clk, FLASH_LATENCY_5) != HAL_OK) {
        return PROBE_ERR_CLOCK;
    }
    return PROBE_OK;
}

void HAL_TIM_Base_MspInit(TIM_HandleTypeDef *htim)
{
    if (htim->Instance == TIM2) {
        __HAL_RCC_TIM2_CLK_ENABLE();
        HAL_NVIC_SetPriority(TIM2_IRQn, 6U, 0U);
        HAL_NVIC_EnableIRQ(TIM2_IRQn);
    }
}

static probe_status_t Probe_TIM2_Init(void)
{
    TIM_MasterConfigTypeDef master = {0};

    g_htim2.Instance = TIM2;
    g_htim2.Init.Prescaler = 8399U;
    g_htim2.Init.CounterMode = TIM_COUNTERMODE_UP;
    g_htim2.Init.Period = 9U;
    g_htim2.Init.ClockDivision = TIM_CLOCKDIVISION_DIV1;
    g_htim2.Init.AutoReloadPreload = TIM_AUTORELOAD_PRELOAD_DISABLE;
    if (HAL_TIM_Base_Init(&g_htim2) != HAL_OK) {
        return PROBE_ERR_TIM_INIT;
    }

    master.MasterOutputTrigger = TIM_TRGO_UPDATE;
    master.MasterSlaveMode = TIM_MASTERSLAVEMODE_DISABLE;
    if (HAL_TIMEx_MasterConfigSynchronization(&g_htim2, &master) != HAL_OK) {
        return PROBE_ERR_TIM_INIT;
    }
    return PROBE_OK;
}

static probe_status_t Probe_TIM2_Start(uint8_t freeze_while_halted)
{
    g_tim2_update_count = 0U;
    if (freeze_while_halted != 0U) {
        __HAL_DBGMCU_FREEZE_TIM2();
    } else {
        __HAL_DBGMCU_UNFREEZE_TIM2();
    }

    if (HAL_TIM_Base_Start_IT(&g_htim2) != HAL_OK) {
        return PROBE_ERR_TIM_START;
    }
    return PROBE_OK;
}

static probe_status_t Probe_TIM2_Stop(void)
{
    if (HAL_TIM_Base_Stop_IT(&g_htim2) != HAL_OK) {
        return PROBE_ERR_TIM_STOP;
    }
    return PROBE_OK;
}

void TIM2_IRQHandler(void)
{
    HAL_TIM_IRQHandler(&g_htim2);
}

void HAL_TIM_PeriodElapsedCallback(TIM_HandleTypeDef *htim)
{
    if (htim->Instance == TIM2) {
        g_tim2_update_count++;
    }
}

static void Probe_TIM2_Sample(probe_tim2_snapshot_t *out)
{
    uint32_t primask;

    if (out == NULL) {
        return;
    }

    primask = __get_PRIMASK();
    __disable_irq();
    __DMB();

    out->sequence = ++g_snapshot_sequence;
    out->tick_ms = HAL_GetTick();
    out->rcc_apb1enr = RCC->APB1ENR;
    out->dbgmcu_apb1_fz = DBGMCU->APB1FZ;
    out->tim_cr1 = TIM2->CR1;
    out->tim_dier = TIM2->DIER;
    out->tim_sr = TIM2->SR;
    out->tim_psc = TIM2->PSC;
    out->tim_arr = TIM2->ARR;
    out->tim_cnt = TIM2->CNT;
    out->update_callback_count = g_tim2_update_count;

    __DMB();
    if (primask == 0U) {
        __enable_irq();
    }
}

int main(void)
{
    probe_tim2_snapshot_t before;
    probe_tim2_snapshot_t after;

    HAL_Init();
    if (SystemClock_Config_Reference() != PROBE_OK) {
        Error_Handler();
    }
    if (Probe_TIM2_Init() != PROBE_OK) {
        Error_Handler();
    }

    Probe_TIM2_Sample(&before);          /* 启动前静态配置证据 */
    if (Probe_TIM2_Start(1U) != PROBE_OK) {
        Error_Handler();
    }

    /* 实际实验应由明确定义的时机触发，不在忙等待中无限采样。 */
    HAL_Delay(10U);
    Probe_TIM2_Sample(&after);           /* 运行状态候选证据 */

    for (;;) {
        /* 将 before/after 交给非 ISR 诊断路径；不要在回调中阻塞打印。 */
    }
}

typedef struct {
    uint32_t half_count;
    uint32_t full_count;
    uint32_t error_count;
    uint32_t adc_error;
    uint32_t dma_error;
    uint32_t dma_lisr;
    uint32_t dma_s0cr;
    uint32_t dma_s0ndtr;
    uint32_t dma_s0par;
    uint32_t dma_s0m0ar;
} probe_adc_dma_snapshot_t;

#define PROBE_DMA_ERROR_UNAVAILABLE UINT32_MAX

extern ADC_HandleTypeDef hadc1;
extern DMA_HandleTypeDef hdma_adc1;

static volatile uint32_t g_adc_half_count;
static volatile uint32_t g_adc_full_count;
static volatile uint32_t g_adc_error_count;
static volatile uint32_t g_adc_error_code;
static volatile uint32_t g_dma_error_code;

void DMA2_Stream0_IRQHandler(void)
{
    HAL_DMA_IRQHandler(&hdma_adc1);
}

void ADC_IRQHandler(void)
{
    HAL_ADC_IRQHandler(&hadc1);
}

void HAL_ADC_ConvHalfCpltCallback(ADC_HandleTypeDef *hadc)
{
    if (hadc->Instance == ADC1) {
        g_adc_half_count++;
    }
}

void HAL_ADC_ConvCpltCallback(ADC_HandleTypeDef *hadc)
{
    if (hadc->Instance == ADC1) {
        g_adc_full_count++;
    }
}

void HAL_ADC_ErrorCallback(ADC_HandleTypeDef *hadc)
{
    if (hadc->Instance == ADC1) {
        g_adc_error_code = HAL_ADC_GetError(hadc);
        g_dma_error_code = (hadc->DMA_Handle != NULL)
                         ? HAL_DMA_GetError(hadc->DMA_Handle)
                         : PROBE_DMA_ERROR_UNAVAILABLE;
        g_adc_error_count++;
    }
}

static void Probe_ADC_DMA_Sample(probe_adc_dma_snapshot_t *out)
{
    uint32_t primask;

    if (out == NULL) {
        return;
    }
    primask = __get_PRIMASK();
    __disable_irq();
    __DMB();

    out->half_count = g_adc_half_count;
    out->full_count = g_adc_full_count;
    out->error_count = g_adc_error_count;
    out->adc_error = g_adc_error_code;
    out->dma_error = g_dma_error_code;
    out->dma_lisr = DMA2->LISR;
    out->dma_s0cr = DMA2_Stream0->CR;
    out->dma_s0ndtr = DMA2_Stream0->NDTR;
    out->dma_s0par = DMA2_Stream0->PAR;
    out->dma_s0m0ar = DMA2_Stream0->M0AR;

    __DMB();
    if (primask == 0U) {
        __enable_irq();
    }
}

#include <assert.h>
#include <stdint.h>
#include <string.h>

#define OBS_HAS_SOURCE       (UINT32_C(1) << 0)
#define OBS_HAS_MOMENT       (UINT32_C(1) << 1)
#define OBS_HAS_SEMANTICS    (UINT32_C(1) << 2)
#define OBS_HAS_EXPECTATION  (UINT32_C(1) << 3)
#define OBS_HAS_CROSS_CHECK  (UINT32_C(1) << 4)
#define OBS_REQUIRED_MASK    (OBS_HAS_SOURCE | OBS_HAS_MOMENT | \
                              OBS_HAS_SEMANTICS | OBS_HAS_EXPECTATION | \
                              OBS_HAS_CROSS_CHECK)

typedef enum {
    FAKE_OK = 0,
    FAKE_ERR_CLOCK_OFF = 1,
    FAKE_ERR_NOT_CONFIGURED = 2,
    FAKE_ERR_BAD_SPEC = 3,
    FAKE_ERR_SOURCE_STOPPED = 4,
    FAKE_ERR_DMA_NOT_CONFIGURED = 5
} fake_status_t;

typedef enum {
    EVIDENCE_STATIC_CONFIG = 0,
    EVIDENCE_RUNTIME_STATE = 1,
    EVIDENCE_EXTERNAL_EFFECT = 2
} evidence_class_t;

typedef struct {
    uint32_t present_fields;
    evidence_class_t claim;
} observation_spec_t;

typedef struct {
    uint8_t clock_enabled;
    uint8_t configured;
    uint8_t running;
    uint8_t paused;
    uint8_t dma_configured;
    uint8_t dma_running;
    uint32_t tick;
    uint32_t psc;
    uint32_t arr;
    uint32_t cnt;
    uint32_t update_flag;
    uint32_t read_clear_event;
} fake_peripheral_t;

typedef struct {
    uint32_t sequence;
    uint32_t tick;
    uint8_t clock_enabled;
    uint8_t configured;
    uint8_t running;
    uint8_t paused;
    uint8_t dma_configured;
    uint8_t dma_running;
    uint32_t psc;
    uint32_t arr;
    uint32_t cnt;
    uint32_t update_flag;
    uint32_t consumed_event;
} fake_snapshot_t;

typedef struct {
    uint32_t next_sequence;
} fake_observer_t;

static void fake_init(fake_peripheral_t *peripheral,
                      fake_observer_t *observer)
{
    memset(peripheral, 0, sizeof(*peripheral));
    memset(observer, 0, sizeof(*observer));
}

static fake_status_t fake_configure(fake_peripheral_t *peripheral,
                                    uint32_t psc,
                                    uint32_t arr)
{
    if (peripheral->clock_enabled == 0U) {
        return FAKE_ERR_CLOCK_OFF;
    }
    peripheral->psc = psc;
    peripheral->arr = arr;
    peripheral->cnt = 0U;
    peripheral->configured = 1U;
    return FAKE_OK;
}

static fake_status_t fake_start(fake_peripheral_t *peripheral)
{
    if (peripheral->clock_enabled == 0U) {
        return FAKE_ERR_CLOCK_OFF;
    }
    if (peripheral->configured == 0U) {
        return FAKE_ERR_NOT_CONFIGURED;
    }
    peripheral->running = 1U;
    return FAKE_OK;
}

static fake_status_t fake_dma_configure(fake_peripheral_t *peripheral)
{
    if (peripheral->running == 0U) {
        return FAKE_ERR_SOURCE_STOPPED;
    }
    peripheral->dma_configured = 1U;
    return FAKE_OK;
}

static fake_status_t fake_dma_start(fake_peripheral_t *peripheral)
{
    if (peripheral->running == 0U) {
        return FAKE_ERR_SOURCE_STOPPED;
    }
    if (peripheral->dma_configured == 0U) {
        return FAKE_ERR_DMA_NOT_CONFIGURED;
    }
    peripheral->dma_running = 1U;
    return FAKE_OK;
}

static void fake_advance(fake_peripheral_t *peripheral, uint32_t ticks)
{
    uint32_t index;

    for (index = 0U; index < ticks; ++index) {
        peripheral->tick++;
        if ((peripheral->clock_enabled != 0U) &&
            (peripheral->running != 0U) &&
            (peripheral->paused == 0U)) {
            if (peripheral->cnt >= peripheral->arr) {
                peripheral->cnt = 0U;
                peripheral->update_flag = 1U;
                peripheral->read_clear_event = 1U;
            } else {
                peripheral->cnt++;
            }
        }
    }
}

static fake_snapshot_t fake_sample(fake_peripheral_t *peripheral,
                                   fake_observer_t *observer)
{
    fake_snapshot_t sample;

    observer->next_sequence++;
    sample.sequence = observer->next_sequence;
    sample.tick = peripheral->tick;
    sample.clock_enabled = peripheral->clock_enabled;
    sample.configured = peripheral->configured;
    sample.running = peripheral->running;
    sample.paused = peripheral->paused;
    sample.dma_configured = peripheral->dma_configured;
    sample.dma_running = peripheral->dma_running;
    sample.psc = peripheral->psc;
    sample.arr = peripheral->arr;
    sample.cnt = peripheral->cnt;
    sample.update_flag = peripheral->update_flag; /* 普通只读模型字段 */
    sample.consumed_event = peripheral->read_clear_event;
    peripheral->read_clear_event = 0U;             /* 明确建模读副作用 */
    return sample;
}

static fake_status_t observation_validate(const observation_spec_t *spec)
{
    if ((spec->present_fields & OBS_REQUIRED_MASK) != OBS_REQUIRED_MASK) {
        return FAKE_ERR_BAD_SPEC;
    }
    return FAKE_OK;
}

static uint8_t claim_is_supported(const observation_spec_t *spec,
                                  const fake_snapshot_t *first,
                                  const fake_snapshot_t *second)
{
    if (observation_validate(spec) != FAKE_OK) {
        return 0U;
    }
    if (spec->claim == EVIDENCE_STATIC_CONFIG) {
        return (uint8_t)((first->clock_enabled != 0U) &&
                         (first->configured != 0U));
    }
    if (spec->claim == EVIDENCE_RUNTIME_STATE) {
        return (uint8_t)((second->sequence > first->sequence) &&
                         (second->tick > first->tick) &&
                         ((second->cnt != first->cnt) ||
                          (second->update_flag != first->update_flag)));
    }
    /* Host Fake 永远不能证明外部电平或真实硬件效果。 */
    return 0U;
}

static void test_clock_gate_and_static_boundary(void)
{
    fake_peripheral_t peripheral;
    fake_observer_t observer;
    fake_snapshot_t first;
    fake_snapshot_t second;
    observation_spec_t static_spec = {
        OBS_REQUIRED_MASK, EVIDENCE_STATIC_CONFIG
    };
    observation_spec_t runtime_spec = {
        OBS_REQUIRED_MASK, EVIDENCE_RUNTIME_STATE
    };

    fake_init(&peripheral, &observer);
    assert(fake_configure(&peripheral, 3U, 9U) == FAKE_ERR_CLOCK_OFF);
    peripheral.clock_enabled = 1U;
    assert(fake_configure(&peripheral, 3U, 9U) == FAKE_OK);
    first = fake_sample(&peripheral, &observer);
    second = first;
    assert(claim_is_supported(&static_spec, &first, &second) == 1U);
    assert(claim_is_supported(&runtime_spec, &first, &second) == 0U);
}

static void test_ordered_runtime_samples(void)
{
    fake_peripheral_t peripheral;
    fake_observer_t observer;
    fake_snapshot_t first;
    fake_snapshot_t second;
    observation_spec_t spec = {
        OBS_REQUIRED_MASK, EVIDENCE_RUNTIME_STATE
    };

    fake_init(&peripheral, &observer);
    peripheral.clock_enabled = 1U;
    assert(fake_configure(&peripheral, 0U, 9U) == FAKE_OK);
    assert(fake_start(&peripheral) == FAKE_OK);
    first = fake_sample(&peripheral, &observer);
    fake_advance(&peripheral, 3U);
    second = fake_sample(&peripheral, &observer);
    assert(second.cnt == 3U);
    assert(claim_is_supported(&spec, &first, &second) == 1U);
}

static void test_read_side_effect(void)
{
    fake_peripheral_t peripheral;
    fake_observer_t observer;
    fake_snapshot_t first;
    fake_snapshot_t second;

    fake_init(&peripheral, &observer);
    peripheral.clock_enabled = 1U;
    assert(fake_configure(&peripheral, 0U, 1U) == FAKE_OK);
    assert(fake_start(&peripheral) == FAKE_OK);
    fake_advance(&peripheral, 2U);
    first = fake_sample(&peripheral, &observer);
    second = fake_sample(&peripheral, &observer);
    assert(first.consumed_event == 1U);
    assert(second.consumed_event == 0U);
    assert(first.update_flag == 1U);
    assert(second.update_flag == 1U);
}

static void test_pause_and_resume_policy(void)
{
    fake_peripheral_t peripheral;
    fake_observer_t observer;
    uint32_t paused_cnt;

    fake_init(&peripheral, &observer);
    peripheral.clock_enabled = 1U;
    assert(fake_configure(&peripheral, 0U, 9U) == FAKE_OK);
    assert(fake_start(&peripheral) == FAKE_OK);
    fake_advance(&peripheral, 2U);
    peripheral.paused = 1U;
    paused_cnt = peripheral.cnt;
    fake_advance(&peripheral, 5U);
    assert(peripheral.cnt == paused_cnt);
    peripheral.paused = 0U;
    fake_advance(&peripheral, 1U);
    assert(peripheral.cnt != paused_cnt);
}

static void test_segmented_failure_and_bad_spec(void)
{
    fake_peripheral_t peripheral;
    fake_observer_t observer;
    fake_snapshot_t first;
    fake_snapshot_t second;
    observation_spec_t incomplete = {
        OBS_HAS_SOURCE | OBS_HAS_MOMENT, EVIDENCE_RUNTIME_STATE
    };
    observation_spec_t external = {
        OBS_REQUIRED_MASK, EVIDENCE_EXTERNAL_EFFECT
    };

    fake_init(&peripheral, &observer);
    assert(fake_start(&peripheral) == FAKE_ERR_CLOCK_OFF);
    assert(fake_dma_configure(&peripheral) == FAKE_ERR_SOURCE_STOPPED);
    assert(fake_dma_start(&peripheral) == FAKE_ERR_SOURCE_STOPPED);
    peripheral.clock_enabled = 1U;
    assert(fake_start(&peripheral) == FAKE_ERR_NOT_CONFIGURED);
    assert(fake_configure(&peripheral, 0U, 9U) == FAKE_OK);
    assert(fake_dma_start(&peripheral) == FAKE_ERR_SOURCE_STOPPED);
    assert(fake_start(&peripheral) == FAKE_OK);
    assert(fake_dma_start(&peripheral) == FAKE_ERR_DMA_NOT_CONFIGURED);
    assert(fake_dma_configure(&peripheral) == FAKE_OK);
    assert(fake_dma_start(&peripheral) == FAKE_OK);
    first = fake_sample(&peripheral, &observer);
    fake_advance(&peripheral, 5U);
    second = fake_sample(&peripheral, &observer);
    assert(second.dma_configured == 1U);
    assert(second.dma_running == 1U);
    assert(observation_validate(&incomplete) == FAKE_ERR_BAD_SPEC);
    assert(claim_is_supported(&external, &first, &second) == 0U);
}

int main(void)
{
    test_clock_gate_and_static_boundary();
    test_ordered_runtime_samples();
    test_read_side_effect();
    test_pause_and_resume_policy();
    test_segmented_failure_and_bad_spec();
    return 0;
}

probe_tim2_snapshot_t before;
probe_tim2_snapshot_t after;

Probe_TIM2_Sample(&before);       /* CEN 应为 0；核对门控、PSC、ARR */
if (Probe_TIM2_Start(1U) != PROBE_OK) {
    Error_Handler();
}
HAL_Delay(10U);
Probe_TIM2_Sample(&after);        /* CEN、CNT/UIF、回调计数形成候选运行证据 */

门控已开：after.rcc_apb1enr 的 TIM2EN 位为 1。
静态配置一致：PSC=8399、ARR=9。
软件请求运行：CR1.CEN 为 1。
发生变化：after 的 CNT/UIF/回调计数至少一项相对 before 改变。
仍未证明：实际 update 频率为 1 kHz；需要独立计时或外部测量。

先写可证伪假设
  -> 定义对象、时机、读取者和字段语义
  -> 从时钟/复位开始分段采样
  -> 限制结论在当前证据层内
  -> 用第二路径交叉验证时间、完整性和外部效果
  -> 先保存现场，再清理和恢复