$projectRoot = (Resolve-Path (Join-Path $PSScriptRoot '..')).Path
$mainSource = Get-Content -Raw (Join-Path $projectRoot 'Core/Src/main.c')
$interruptSource = Get-Content -Raw (Join-Path $projectRoot 'Core/Src/stm32f4xx_it.c')

function Require-SourcePattern
{
    param(
        [string]$Source,
        [string]$Pattern,
        [string]$Message
    )

    if ($Source -notmatch $Pattern)
    {
        throw $Message
    }
}

Require-SourcePattern $mainSource `
    'HAL_NVIC_SetPriority\(SysTick_IRQn, CPU_CFG_KA_IPL_BOUNDARY, 0U\)' `
    'SysTick priority must use CPU_CFG_KA_IPL_BOUNDARY.'
Require-SourcePattern $interruptSource 'OS_CPU_SysTickHandler\(\)' `
    'SysTick must use the uC/OS-II port wrapper.'
Require-SourcePattern $mainSource `
    'static HAL_StatusTypeDef AppRecoverUartReception\(void\)' `
    'UART recovery helper is missing.'
Require-SourcePattern $mainSource 'ModbusReceptionNeedsRecovery' `
    'UART pending-recovery state is missing.'

$sysTickHandler = [regex]::Match(
    $interruptSource,
    'void SysTick_Handler\(void\)\s*\{(?s:.*?)\n\}\s*/\*\*').Value
if (($sysTickHandler -match 'OSIntEnter\(\)') `
    -or ($sysTickHandler -match 'OSTimeTick\(\)') `
    -or ($sysTickHandler -match 'OSIntExit\(\)'))
{
    throw 'SysTick must not contain a handwritten uC/OS-II tick sequence.'
}

$uartErrorCallback = [regex]::Match(
    $mainSource,
    'void HAL_UART_ErrorCallback\(UART_HandleTypeDef \*uartHandle\)\s*\{(?s:.*?)\n\}\s*/\*\*').Value
if (($uartErrorCallback -match 'HAL_UART_Receive_IT') `
    -or ($uartErrorCallback -match 'HAL_UART_AbortReceive_IT'))
{
    throw 'UART error callback must defer recovery to the Modbus task.'
}

Write-Output 'RTU runtime invariants are present.'