从私有 RAM 执行区维护 H743 Flash

本页规定选定 STM32H743ZIT6 V 修订／Cache off 配置中同步编程和擦除的 RAM 维护边界。普通选定链接必须先通过显式数据操作数闭包与按真实字节检查的汇编返回 gate，才能准入镜像。这些检查保留下文的调用者、C/ABI 和外部 owner 前提。图示在原始实现及证据退出条件满足前保留 target IO-24 身份。本页不建立软件候选或物理资格。物理 HIL 为 not_executed。

公共 Flash face 仍暴露物理几何与同步操作。选定 provider 现在要求冷态 RAM 准备；不再回退到原普通 Flash 驻留路径执行物理脉冲。已有镜像／控制别名保护、编程时序和时钟所有权仍是前提。源代码接入或链接成功本身不能建立整个 IO-24 退出。

所有选定 Flash 配置均要求 V 修订 0x2003，包括固定 HSI32/64 和 HSI64/PLL384；未知 cut 被拒绝。该限制和选定 RAM 工作区不扩展到其他外设 provider 或未选 Flash 的装配；它们仍以各自现有配置合同为准。

保持单一控制器 owner 与冷态 factory

FIG-17 target：静态 face 查找与显式准备独立于直接运行调用；私有 RAM 边界拥有 CPU 保护和 Flash 结清责任

FIG-17 表示 target 架构及所需所有权边界，不宣称全部实现和生产 ELF 退出已通过。实线表示其标签明确说明的查找、调用或复制关系；虚线外部前提由调用者负责，不是平台任务。factory 返回既有不可变 Flash face，不执行 MMIO、分配、执行区复制或维护。取得 face 后，普通 I/O 通过其共享只读操作表直接进入选定私有 provider。

所有者

目标设计中的责任

生成的 Platform 生命周期

仅选入所需私有工作区与代码；安排准备与逆序清理；保留清理失败责任

H743 Flash provider

校验物理操作、区域、源与目标；为单一执行 owner 暂存命令／输入

私有 RAM owner 与 bridge

证明复制／布局／上下文，安装私有栈与 RAM 向量，保存 CPU 状态并使整个忙事务留在 RAM

私有 MPU guard

暂时拥有 selector、选定描述符与控制修改；证明安装及精确恢复

既有 System

拥有单调 TIM2 时间域与 epoch；RAM 维护必须保持该合同

外部维护调用者

作为单一执行 owner 串行调度调用；撤回并 join 其他总线 master 与使用者，提供已证明新擦除的消费区域，并选择看门狗／恢复策略

不新增第二个 Flash owner、运行期 registry、heap、强制 OS 锁、隐藏 worker 或自动喂狗。应用任务、升级策略、分区、认证和复位策略仍由外部仓库负责。

公共 Flash 合同要求单一执行 owner，且不得并发调用 program/erase。调度由外部调用者负责；active 状态检查不构成隐藏的并发锁。

生成的 Platform 拥有唯一一个既有私有 Flash 工作区及其内嵌 MPU guard。公共 consumer 在所编写的 TOML 中选择 Flash，通过 nx_factory_flash 取得不可变 face，并使用普通 Platform start/stop 生命周期完成准备和清理；无需提供工作区或包含私有 SDK 类型。冷态构造在复制或发布所有权前拒绝外来工作区；准入、外部缓冲区检查和清理维持相同的固定绑定。物理绑定还要求官方 FLASH、TIM2、SCB 身份以及未交换 Bank 的物理 Flash 基址。这不会增加 RAM 存储、分配器或运行时 registry。

在 Flash 进入忙状态前准备字节与上下文

冷态准备必须校验选定 LOAD/RUN 范围，将已审查代码／literal 复制到准入的 AXI SRAM，并在发布就绪前核验实际布局。整个忙区间内，私有向量、栈、命令、deadline 操作数、工作区与终止诊断都必须留在准入 RAM。选定 RAM 不得与提交缓冲区、可执行／LOAD 字节、向量、控制 MMIO、当前 System 状态或其他私有元数据重叠。半开区间检查必须先于访问拒绝溢出与部分别名。

公共 read、program 路径的已擦除区域预检，以及每个已编程 flashword 的读回，都会检查双 Bank 当前的 SNECCERR/DBECCERR sticky 标志。观察到标志时返回 IO；这些物理数据读检查自身不会通过 W1C 清除标志。这也包括入口处已经锁存的事件：状态不能确定其来源，也不能证明 DBECC 异常已恢复。纠正后的数据仍可能比较相等，因此必须先报告已观察事件，不能让全 FF 输入的无操作路径或后续脉冲将其掩盖。这不会取消 erase／脉冲准备中独立的目标 Bank W1C 阶段。

最终调用必须重新观测实际特权 Thread 上下文、屏蔽状态、Cache 和浮点状态；冷态准备成功本身不能证明后续调用上下文。入口要求 PRIMASK、BASEPRI 和 FAULTMASK 均为零；IRQ 调用或仍有 lazy FP 活动上下文均不可准入。deadline 必须在既有 System TIM2 时间域内且有限；不支持 NX_DEADLINE_NEVER。bridge 保留独立 MSP、PSP、包含 FPCA 的 CONTROL 和传入 PRIMASK。在 C 运行前，它将传入 MPU CTRL、RNR 及 region15 RBAR/RASR 捕获到 r8-r11，并拥有 selector 效果及经验证的回滚责任。选定 C 指令不得写这些捕获寄存器。C 事务在安装 guard 前发布并读回 RAM VTOR；C 清理后，汇编 gate 对照受保护的捕获值检查硬件并恢复链接器已知的原始向量，随后 bridge 才能恢复调用者的精确 CPU 状态。

在 bridge 入口处，调用者必须拥有传入 MSP 下方和活动 Thread 栈指针下方各至少 260 字节可读写存储：36 字节用于保存寄存器，另保守预留 224 字节用于两层嵌套扩展异常帧及对齐。这些预留量不包含普通 provider C 栈帧；它们覆盖私有 MSP／RAM VTOR 取得所有权前及撤回后的过渡阶段。私有栈的 ELF 界限另行包含其异常预留量，不能证明任意传入应用栈的范围。原始 NMI/HardFault 别名必须保持已准入的非返回 default 行为。在 RAM 窗口内，两个 handler 均直接使用固定工作区，并停留于非返回 RAM 诊断路径。

源码／ELF 闭包必须覆盖实际指令、veneer、literal、直接与间接调用、handler、终止路径以及编译器生成的 helper。section 名、C attribute、调用者自称的 ram_safe 标志或未使用的匹配 literal 均不足为证。固件保持 C11；测试机制不进入固件依赖。

选定 H743 Flash 装配的正常固件链接现在执行自动 RAM 审计。审计针对真实 ELF section 和 LOAD segment 校验完整复制 pod 与 workspace：RX run range 有唯一匹配的 Flash load range，字节一致；vector、stack 和 workspace extent 与 pod 互不重叠，并完全位于可写 RAM。不可变 Flash image guard 必须包含真实链接端点，并覆盖每个带文件内容的 LOAD。这些检查属于正常链接流程，而不只是合成 checker fixture。修改真实固件 ELF 的 guard 字节会被同一审计拒绝。

审计解码真实 CPU bridge、返回 gate、编程 leaf 的字节、RAM 直接控制流及字面量驻留位置。每个选定的显式 read 和 store 都必须解析为精确拥有的 workspace／System 字段、允许的 MMIO 寄存器及访问宽度、已证明的栈槽或 pod 内字面量；未知操作数被拒绝。RAM C 代码不得改写已暂存命令、源字和已保存命令字段。唯一动态写基址隔离在已检查的编程 leaf 中：每次调用执行八次固定暂存字读取和八次按地址递增的 32 位写入，不通过目标地址读取数据。有界调用／CFG 分析将每个事务限制为至多一次此类调用，并拒绝会增加调用次数的环。

保守私有栈界限使用编译器实际生成的 .su 记录及异常预留量。寄存器／栈／调用汇合保留包括 Unknown 在内的有限候选；超过候选数量或操作数乘积上限时拒绝镜像。栈地址分析跟踪真实直接调用的输入输出、固定 push/pop 槽及栈传参。寄存器偏移 SP 加载和栈派生指针的显式 spill 按失败处理。布局报告分别列出复制字节、workspace 字节及合计静态 RAM 范围；范围外的对齐开销计入普通资源报告。这些是在明确的编译器 AAPCS、C 对象生存期与独占所有权前提下，对选定字节／地址及协议的检查，不建立通用 C 内存安全、实测栈使用、时序或物理行为结论。

阻止 CPU 对 Code 域的推测访问

此参考配置必须关闭 Cache，但这不证明分支预测已关闭。PM0253 Rev6 说明了对 Normal memory 和分支目标的推测读取；CCR.BP 只读且恒为一，BPIALL 未实现。DSB 完成之前的显式访问，不会禁用之后的预测。AN4838 Rev11 第 3.4 节建议通过 MPU 内存属性阻止推测预取。因此目标设计将独立审查的显式访问闭包与临时 Code 域内存类型 guard 结合。

首个准入实现要求实际统一 16-region MPU。传入 MPU 已启用、TYPE 不支持，或未 ENABLE 却设置 HFNMIENA 时均拒绝。禁用 CTRL 值 0 与 4 必须精确保留。 **CTRL=0 不能证明所有描述符都已禁用：**必须观测全部 16 个 RASR.EN。存在启用的外来描述符时，必须在写入策略前拒绝。扫描 RNR 本身就是已取得的 selector 效果，每条返回路径都必须回退；若回退被拒绝，责任保留在 RAM。

选定 region 15 字段

目标值

基址与半开范围

0；[0, 0x20000000)

SIZE / SRD / ENABLE

28 / 0 / 1：512 MiB，全部子区域启用

XN / AP

1 / 001：禁止取指；特权读写

TEX / C / B / S

0 / 0 / 0 / 0：Strongly-ordered，隐式共享

RASR

0x11000039

CTRL

7：ENABLE、PRIVDEFENA 和 HFNMIENA

XN 禁止 Code 域取指；Strongly-ordered 替换允许推测读取的 Normal memory 类型。 AP001 允许编程一个 32-byte flashword 所需的八次显式 CPU store。AP000 会阻止这些 store，因此不适用于统一的编程／擦除路径。AP001 也允许显式读取：独立审查的 RAM 调用图必须排除这些读取。这不是一项全面禁止总线访问的权限检查。

owner 在首次 selector 写入前保存精确观测到的 CTRL 和 RNR；选定 region15 并读回确认选择后，在首次描述符写入前捕获对应 RBAR/RASR。bridge 独立保存在 r8-r11 中的捕获值，避免最终返回 gate 将可变 guard 状态自身当作完整性证明。RBAR 读回包含选定 region 编号，因此基址比较按真实寄存器字段进行掩码处理。禁用描述符字段不必为零，恢复时必须保留。任何 program store 或 erase START 前，必须通过读回和 DSB/ISB 证明 guard 已安装。HFNMIENA 使该策略在 NMI/HardFault 中仍然有效。最终汇编 gate 对照捕获值独立检查已恢复的 CTRL、选定描述符和 selector。每次临时 selector 效果均在写入前记录，且只在精确恢复／读回后清除。在此窗口内不得调用普通 Flash 驻留 Arch 或 vendor MPU helper。

deadline 到期不能取消物理脉冲

FIG-18 target：deadline 到期只锁存结果；RAM 事务保留保护，等待真实双 Bank 排空并恢复状态后才能返回

FIG-18 表示协议阶段，不新增公共 request enum。每条箭头都是具有条件的控制流迁移。返回路径必须满足以下顺序；终止路径没有返回普通代码的边。

  1. 在 trigger 前拒绝无效输入或已到期 deadline。双 Bank 空闲时，证明已取得的每项 trigger 前 selector／保护效果均已回滚。每条 C 事务返回路径，包括向量发布被拒绝以及 guard／deadline 拒绝，均在私有 MSP 上到达汇编 gate。该 gate 在恢复 VTOR 前证明双 Bank 空闲、无保留 guard 效果、精确已保存目标 control 加 LOCK，以及 MPU 硬件已恢复。任何无法证明的条件都进入 RAM fail-stop。

  2. 暂存已校验命令与输入，进入 RAM bridge，安装 RAM 向量，并在启动物理操作前证明 MPU guard。

  3. 只执行已明确校验的编程 store 或擦除 START。观测两个 Bank 的真实 BSY/QW/WBNE，保留全部命令／工作区所有权。

  4. 触发后绝对 deadline 到期时，锁存 TIMEOUT 并继续真实 RAM 轮询。不得清除 busy 位、撤回保护、释放存储，或跳到 Flash 错误 handler 制造已结清假象。

  5. 双 Bank 实际空闲后，在 C 中证明目标 LOCK、完成所需 barrier，并恢复／读回 MPU 状态。随后汇编返回 gate 对照受保护捕获值独立检查硬件，恢复并读回链接器已知的 g_pfnVectors，并完成 DSB/ISB。只有此 gate 成功后，bridge 才能恢复调用者的精确上下文并返回普通代码。

  6. 报告已结清结果。硬件失败报告 IO；否则已锁存到期报告 TIMEOUT，成功完成报告 SUCCESS。

永久 busy 的硬件不会到达返回路径；它停留于 RAM 排空路径并保留保护与存储。无法证明的 lock、保护、向量或时间域状态也进入非返回 RAM fail-stop。bridge、受保护捕获值和最终硬件 gate 均按真实 ARM 字节检查；仅有一个具名 C 返回函数或为零的软件 ledger，不能授权返回。host watchdog 可以观察并终止独立测试进程，但这不是设备排空或产品恢复。本设计不承诺隐藏复位、watchdog 服务、RTOS 推进或有界墙钟返回时间。

选定 deadline 使用既有 TIM2 时间域与 epoch。任何回绕扩展都必须具有实际可支持的 service／pulse 上界；单个待处理 UIF 不能计数屏蔽期间任意多次回绕。丢失或耗尽的 epoch 不能以貌似合理的零继续向 deadline consumer 提供时间。RTOS/SysTick 补偿和产品时间恢复需要各自审查的合同。长时间屏蔽中断的 Flash 维护不能继承 Arch 短临界区的延迟合同。

CPU 保护不能替代系统静止

该 MPU guard 约束 CPU，不会停止 DMA1/2、MDMA、Ethernet、USB、显示引擎和调试访问，也不会 join 它们迟到的 IRQ 或 publication 路径。调用维护前，外部 owner 必须撤回并 join 每个能访问忙 Flash 域的 master，包括描述符与输入源；或者提供独立证明的互不干扰计划。地址范围本身不能证明 worker 或总线 master 已停止。

同一调用者还必须决定产品如何容忍中断屏蔽、看门狗到期、掉电和不返回故障。平台不选择这些策略，也不根据 Board 参考推断策略。本设计不准入 Cache-on 编程、已启用的外来 MPU region、bank swap、option/OTP 写入、所有 H7 cut、bootloader 接管或运行期时钟变化。

将成本与证据绑定实际字节

按选择生成 source 与实例时，未选入镜像不得含 RAM 执行区、工作区或调用。实际 selected/unselected ELF 比较必须分别报告 Flash LOAD／footprint、复制的可执行字节、静态 RAM、对齐填充，以及实际调用／异常栈需求。数组大小或 host sizeof 不是链接成本、实测栈使用、吞吐量或 WCET。本页不声明测得成本、栈高水位、吞吐量或 WCET。

选定的 PLL384 外设参考仅在 h743-high-peripherals.toml 中手写一次。维护的装配清单、普通 preset、生成的宿主 factory 和已安装的 Source SDK consumer 均使用同一输入。移动其源码权威位置不会改变 V 修订、baremetal、Cache-off 或 poll-word 限制。

既有 performance.yml 中仅执行资格验证的路径接受此规范输入，并要求显式的 gpio 工作负载和精确的源码 SHA。该工作负载启动选定的 Platform 并执行 GPIO；它不获取公共 Flash face。因此，仅在链接镜像中保留 RAM pod，不能证明每个公共 Flash 操作也都已保留。已安装的公共 Flash consumer 和精确链接保留检查仍须作为独立证据。未来运行即使成功，也只能建立其实际源码、镜像和复现范围内的证据；它不关闭完整 IO-24 退出条件，也不将物理 HIL 从 not_executed 改为已执行。

同一 ELF 审计报告 public_flash_linkage。retained_verified 表示观测到的只读操作表包含四个 Thumb 指针，并已关联到 flash.c 中已知公共操作。not_retained 表示没有观测到该命名操作表。retained_not_proved 保留这样的事实：可执行目标仍在，但因 LTO 重命名或元数据不足，无法证明方法身份；它既不拒绝合法构建，也不声称已验证方法身份。显式空指针、非 Thumb 指针或已识别的非法条目仍被拒绝。这一区分不放宽现有 RAM 闭包证明；RAM pod 保留不能替代公共 face 链接证据。

linked_resources 通过既有资源观察器报告整镜像分配。RAM pod 和 workspace 是这些总量的子集，不能再次相加。这些观测审计实际链接字节，不执行 Flash 编程脉冲、不建立栈峰值，也不测量 busy-bank 行为。

软件退出前所需证据

边界

真实 GoogleTest/GoogleMock RED 后 GREEN

实际 provider／bridge 边界、失败、迟到排空和实例隔离；不 mock 实现

正常 TOML／生成生命周期与 factory 测试

单份 authored 装配、不可变 IR、实际按需 constructor 与保留清理

实际发出的 ARM 固件与闭包报告

复制字节、解码调用／literal／寄存器流、guard 值、不提前返回、向量／栈／时间与镜像／控制别名

选入与未选入 ARM 资源检查

精确生成 source graph、retention 与分别统计的 RAM／Flash 成本

clean SDK、完整 gates 与候选证据

精确 source／配置／依赖／工具；不复用旧 commit 结果

实际 station 执行

真实 silicon／PCB／电气条件、推测流量、脉冲时序、掉电、看门狗和中断行为

合成 checker 夹具只证明其相应 checker 行为。host 寄存器模型不测量真实分支预测器、总线竞争或 IRQ 延迟。物理 RAM 函数及异常入口直接使用既有生成工作区、既有 System epoch 和官方 MMIO 身份。汇编返回 gate 接收 C 结果及受保护 MPU 捕获值；它在恢复调用者前检查排空、LOCK、保护已恢复及固定原始向量。按真实字节定义的检查会拒绝读取、比较、barrier 或失败分支的缺失或重排，不依赖函数名或调用实参作为证明。

选定审计通过，表示在已声明调用者、编译器和所有权前提下，取得其有界显式操作数及返回协议证明；它不是通用 C 解释器、推测总线访问测量或硬件资格。缺失的生产证明仍是开放退出项。IO-01–42 台账 仍为实现状态权威；逐配置执行、源码身份、SDK 检查和剩余软件候选义务记录在交付证据中。

实现分为冷态准备与准入、CPU bridge 与汇编返回 gate、RAM 向量发布、MPU 事务和物理脉冲／时间观测。私有工作区与已核对的 C／汇编前缀在RAM 合同中声明。这些链接用于定位当前工作，不能替代所需执行和生产 ELF 证据。

主要参考为 PM0253 Rev6 第 2.3、4.6–4.8 节，AN4838 Rev11 第 3.4 节、RM0433 Rev9 的 Flash 映射／read-while-write 规则，以及 ES0392 Rev15 第 2.1.2 节。实现评审必须附 source 身份记录和选定 provider 证据。另见 H743 provider 范围、 V-only 时钟合同、I/O 增量架构、 Arch 合同与资格边界。