语义保持证明结构（依赖与调用关系概览）

1. 总体结构（Compiler.v）

• driver/Compiler.v 定义完整编译链，并提供：
  • transf_c_program_match
  • cstrategy_semantic_preservation
  • c_semantic_preservation
  • transf_c_program_correct
• 这些定理将各 pass 的语义保持定理组合为“端到端”语义保持。

2. 单个 pass 的标准证明结构

多数 *_proof.v 文件使用相似结构： 1) 结构保持引理 - symbols_preserved, senv_preserved, functions_translated, function_ptr_translated, sig_preserved 2) 匹配关系定义 - match_states / match_env / match_cont 等，用于连接源/目标语义状态 3) 逐步仿真定理 - transf_step_correct 或 step_simulation 4) 初始/终止状态保持 - transl_initial_states, transl_final_states 5) 主正确性定理 - transl_program_correct 或 transf_program_correct

3. 前端阶段证明依赖

3.1 SimplExprproof

• 关键：表达式语义与语句序列的对应关系
• 使用 match_cont / leftcontext 的栈式匹配结构
• 主结论：transl_program_correct

3.2 SimplLocalsproof

• 关键：局部变量提升前后环境一致性
• 依赖：match_env 与调试注释保持

3.3 Cshmgenproof

• 关键：运算/类型转换/内存访问构造器的正确性（make_*_correct）
• 主结论：transl_program_correct

3.4 Cminorgenproof

• 关键：栈布局与变量地址映射的正确性
• 使用 match_callstack / match_env 维护内存块对应关系

4. 后端阶段证明依赖

4.1 Selectionproof

• 关键：指令选择后语义等价
• 依赖：Op、Values 的代数性质

4.2 RTLgenproof

• 关键：结构化语句 → CFG 的语义保持
• 依赖：Smallstep 的多步仿真框架

4.3 RTL 级优化（Tailcall/Inlining/Renumber/Constprop/CSE/Deadcode）

• 关键：优化前后状态的 match_states，以及对副作用的保守处理
• 通常提供 transf_program_correct

4.4 Unusedglobproof

• 关键：删除未用全局定义后仍保留可见符号与主函数
• 依赖：全局环境匹配与内存注入性质

4.5 Allocation proof（Allocproof）

• 关键：外部寄存器分配结果的“验证”正确性
• 通过 dataflow 等式约束证明 RTL 与 LTL 对应

4.6 Tunneling/Linearize/CleanupLabels

• 关键：控制流重写保持
• transf_step_correct 与 transf_program_correct

4.7 Debugvarproof

• 关键：调试注释不改变程序语义
• 证明仅插入 EF_debug 相关 builtin 的可忽略性

4.8 Stacking/Asmgenproof

• 关键：栈帧布局、调用约定与指令映射正确性
• 依赖：Memory, Values, ABI 约束

5. 关键依赖模块（共通层）

• common/Smallstep.v：star/plus 仿真框架
• common/Events.v：可观察事件与 trace 等价
• common/Memory.v / Values.v：内存与值注入/弱化定理
• common/Globalenvs.v：符号/函数指针保持

6. 实际调用关系（顶层）

• 各 *_proof.v 的 transf_program_correct 被 Compiler.v 组合
• Compiler.v 的 c_semantic_preservation 证明最终端到端正确性