关键模块的定理结构（概览）

1. lib/Integers.v（机器整数）

模块目标：形式化 N 位机器整数（模 2^N），定义算术/位运算语义，并证明代数与位级性质。

定理结构分层 1) 表示与范围 - modulus, max_unsigned, max_signed 等定义 - Z_mod_modulus_range, unsigned_range, signed_range：表示范围与归一化性质 - repr_unsigned, unsigned_repr, signed_repr：Z 与 int 的互转一致性

2. 等价关系与判等

• eqm 等价（同余）性质：eqm_refl/sym/trans
• eq_dec, eq_spec, eq_true/eq_false：可判等与性质

3. 算术运算

• add_*, sub_*, mul_* 等定理：交换律、结合律、分配律
• divu/divs/modu/mods：与 Euclid 性质对应的定理族

4. 位运算与移位/旋转

• and/or/xor/not 的交换/结合/吸收律
• shl/shr/shru 与位级性质 (bits_* 系列)
• rol/ror/rolm 与位运算组合性质

5. 幂与优化相关定理

• is_power2_*, mul_pow2, divu_pow2 等
• 用于后端优化的代数变换基础

依赖关系 - 依赖 Zbits、Coqlib 的整数性质与位操作 - 为 Values.v、Op.v、后端优化提供基础代数事实

2. common/Values.v（值域与值运算）

模块目标：统一中间语言使用的值类型与基础运算语义。

定理结构分层 1) 类型匹配 - has_type, has_argtype, has_rettype 与相关判定定理 - has_subtype, has_subtype_list：弱类型系统中的子类型保持

2. 归一化与载入结果

• normalize_type, normalize_idem
• load_result_type, load_result_same：内存读取与类型一致性

3. 算术与逻辑运算等式

• add_commut, mul_assoc 等运算性质
• negate_cmp* / swap_cmp*：比较运算等价变换

4. 语义弱化/注入性质

• lessdef 系列：允许未定义值的语义弱化
• val_inject / val_inject_list：内存注入/重映射下值保持
• *_lessdef / *_inject 定理族

依赖关系 - 依赖 Integers, Floats, AST - 为各语言语义（C/Clight/RTL 等）提供统一值语义基础

3. common/Memory.v（内存模型）

模块目标：定义内存状态与 load/store/alloc/free 语义，并提供关键性质。

定理结构分层 1) 权限与合法性 - perm / range_perm 及其推理规则 - valid_block 与 perm_valid_block - perm_cur/max 等权限单调性

2. 操作性质

• load/store 的行为一致性
• alloc/free 的块范围与可达性性质
• store_valid_block, free_valid_block（在文件中进一步展开）

3. 注入与等价

• 与 Memtype/Memdata 配合的注入与扩展性质
• 与外部调用、全局环境一致性相关的 lemmas

依赖关系 - 依赖 Memdata, Memtype, Values, AST - 为语义保持证明中的“内存一致性”提供基础

4. common/Smallstep.v（小步语义框架）

模块目标：提供通用小步语义闭包与仿真框架。

定理结构分层 1) 闭包与组合 - star / plus 的构造与组合性质 - star_trans, plus_star 等组合律

2. 步进与轨迹

• trace 拼接与 E0 相关性质
• 用于证明多步仿真/多步保持

3. 仿真框架基础

• 作为 *_proof.v 中仿真/语义保持的标准工具层

依赖关系 - 依赖 Events, Globalenvs, Integers - 贯穿所有语义保持证明