diff --git a/crates/core/tests/method_contracts.rs b/crates/core/tests/method_contracts.rs
index e8b7e1b..40bda5d 100644
--- a/crates/core/tests/method_contracts.rs
+++ b/crates/core/tests/method_contracts.rs
@@ -448,13 +448,19 @@ fn native_overrides_preserve_union_inputs_and_do_not_expand_effects() {
 }
 
 #[test]
+/// 构类时可暂缓未知前向注解，调用时必须解析并重验覆盖；未知和已知但不兼容都不能进入源码体。
 fn unknown_forward_names_defer_until_call_without_entering_the_body() {
+    // 独立 VM 隔离全局与方法重绑定，避免其他场景状态干扰快照证明。
     let mut vm = Vm::new().unwrap();
+    // 显式类型自举根，用于实例与绑定方法测试，最终归还并收集类型环。
     let roots = vm.bootstrap_types().unwrap();
+    // 启用普通覆盖验证，前向未知仅在定义阶段暂缓，调用阶段不豁免。
     vm.set_source_type_checks(true).unwrap();
+    // 源码名查找环境，更新其中键可改变契约或调用图，不能把首次查询缓存为永久证明。
     let globals = vm.new_dict().unwrap();
     vm.dict_set(globals, Value::Text("ran".into()), Value::Number(0.into()))
         .unwrap();
+    // 父方法要求 Number 参数，子类尚未定义的 Later 参数暂缓到调用检查。
     let base_fn = source(
         &mut vm,
         globals,
@@ -463,7 +469,9 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() {
         "Number",
         Value::Number(0.into()),
     );
+    // 父定义先合法创建，后代契约需相对这份真实定义检查。
     let base = class(&mut vm, "Base", roots.object, base_fn).unwrap();
+    // 子类使用尚未解析的 Later 名称，不代表可永久跳过参数替换验证。
     let child_fn = source(
         &mut vm,
         globals,
@@ -472,7 +480,9 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() {
         "Number",
         Value::Number(0.into()),
     );
+    // 定义阶段允许未知名称的派生创建，实例调用时会重新核对。
     let child = class(&mut vm, "Child", base, child_fn).unwrap();
+    // 实例提供实际接收者身份，绑定效果分析可据此查 helper，未绑定函数则未知。
     let receiver = vm.new_object().unwrap();
     vm.attach_type(receiver, child).unwrap();
     assert!(matches!(
@@ -482,6 +492,7 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() {
         ),
         Err(VmError::UnknownAnnotation(_))
     ));
+    // Later 最终解析为独立名义类型，不接纳父参数 Number，故由未知错误变为覆盖不兼容。
     let later = vm
         .new_type("Later", roots.object, TypeConstructor::Record)
         .unwrap();
@@ -498,6 +509,7 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() {
         vm.dict_get(globals, &Value::Text("ran".into())).unwrap(),
         Some(Value::Number(0.into()))
     );
+    // 归还测试拥有根，内部方法/签名/类型边由堆维护，避免重复 release。
     for object in [
         receiver,
         child,
@@ -511,16 +523,23 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() {
     ] {
         vm.release(object).unwrap();
     }
+    // 回收无根函数/全局/类型环，最终对象数应为零。
     vm.collect_cycles();
     assert_eq!(vm.object_count(), 0);
 }
 
 #[test]
+/// 已验证源码只读效果约束原生覆盖；Mutating/External 拒绝，Delegated 仍为未知而不是确定只读。
 fn verified_source_read_only_effects_constrain_native_overrides() {
+    // 独立 VM 隔离全局与方法重绑定，避免其他场景状态干扰快照证明。
     let mut vm = Vm::new().unwrap();
+    // 显式类型自举根，用于实例与绑定方法测试，最终归还并收集类型环。
     let roots = vm.bootstrap_types().unwrap();
+    // 启用普通覆盖验证，前向未知仅在定义阶段暂缓，调用阶段不豁免。
     vm.set_source_type_checks(true).unwrap();
+    // 源码名查找环境，更新其中键可改变契约或调用图，不能把首次查询缓存为永久证明。
     let globals = vm.new_dict().unwrap();
+    // 手工指令使控制流和调用目标来源可精确观察，构造器先验证栈高/跳转。
     let code = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadFast, 1),
@@ -541,26 +560,35 @@ fn verified_source_read_only_effects_constrain_native_overrides() {
     })
     .unwrap();
     assert!(code.is_statically_read_only());
+    // 代码数据只验证与分配，call_effect 不应实际执行其中指令。
     let code = vm.new_code(code).unwrap();
+    // 源码方法只装载参数并返回，可由本地白名单直接证明 ReadOnly。
     let source = vm
         .new_function("check", code, globals, vec![], vec![])
         .unwrap();
+    // 父定义先合法创建，后代契约需相对这份真实定义检查。
     let base = class(&mut vm, "PureBase", roots.object, source).unwrap();
+    // 后代继承已证明只读的方法，候选原生覆盖不能扩大已知效果。
     let child = vm.new_type("Child", base, TypeConstructor::Record).unwrap();
     assert_eq!(vm.call_effect(source).unwrap(), Some(CallEffect::ReadOnly));
+    // 实例提供实际接收者身份，绑定效果分析可据此查 helper，未绑定函数则未知。
     let receiver = vm.new_object().unwrap();
     vm.attach_type(receiver, child).unwrap();
+    // 绑定对象拥有函数和实际接收者边，分析可用 receiver 区分实例方法/字段。
     let Value::Object(bound) = vm.bind_attr(receiver, "check").unwrap() else {
         panic!("bound method")
     };
     assert_eq!(vm.call_effect(bound).unwrap(), Some(CallEffect::ReadOnly));
+    // 保存所有候选原生函数拥有根，避免只清理最后成功安装的方法。
     let mut functions = vec![];
+    // 四种原生声明分别测试；未知 Delegated 不等于允许在只读域执行任意目标。
     for effect in [
         CallEffect::Mutating,
         CallEffect::External,
         CallEffect::ReadOnly,
         CallEffect::Delegated,
     ] {
+        // 函数持有其代码/全局边，效果查询从当前载荷及环境读取快照。
         let function = vm
             .allocate(ContextNativeFunction::new(
                 "check",
@@ -572,8 +600,11 @@ fn verified_source_read_only_effects_constrain_native_overrides() {
                 vec![],
             ))
             .unwrap();
+        // 失败更新不能改变后代定义版本，用于证明检查在提交方法表之前完成。
         let version = vm.change_version(child).unwrap();
+        // 保存更新结果，再按已知效果是否扩大区分成功与拒绝。
         let update = vm.define_method(child, "check", function);
+        // Mutating/External 扩大 ReadOnly；其余候选按当前规则检查与查询。
         if matches!(effect, CallEffect::Mutating | CallEffect::External) {
             assert!(matches!(
                 update,
@@ -592,6 +623,7 @@ fn verified_source_read_only_effects_constrain_native_overrides() {
         );
         functions.push(function);
     }
+    // 归还测试拥有根，内部方法/签名/类型边由堆维护，避免重复 release。
     for object in functions.into_iter().chain([
         bound,
         receiver,
@@ -605,12 +637,15 @@ fn verified_source_read_only_effects_constrain_native_overrides() {
     ]) {
         vm.release(object).unwrap();
     }
+    // 回收无根函数/全局/类型环，最终对象数应为零。
     vm.collect_cycles();
     assert_eq!(vm.object_count(), 0);
 }
 
 #[test]
+/// 局部共享引用赋值可能修改旧对象，Cell 写入/未知调用也不能由本地白名单直接证明纯。
 fn shared_local_assignment_and_dynamic_calls_are_not_inferred_pure() {
+    // StoreFast 可能触发旧对象共享引用赋值，不能仅因目标是局部变量就判纯。
     let assignment = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadFast, 1),
@@ -627,6 +662,7 @@ fn shared_local_assignment_and_dynamic_calls_are_not_inferred_pure() {
     )
     .unwrap();
     assert!(!assignment.is_statically_read_only());
+    // StoreDeref 修改已有捕获 Cell，必须从本地只读白名单排除。
     let captured = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadConst, 0),
@@ -642,6 +678,7 @@ fn shared_local_assignment_and_dynamic_calls_are_not_inferred_pure() {
     )
     .unwrap();
     assert!(!captured.is_statically_read_only());
+    // 动态 Call 没有本地目标证明，is_statically_read_only 不能直接通过。
     let call = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadGlobal, 0),
@@ -659,7 +696,9 @@ fn shared_local_assignment_and_dynamic_calls_are_not_inferred_pure() {
     assert!(!call.is_statically_read_only());
 }
 
+/// 效果测试辅助，手工建立调用指定全局名并返回的源码函数，不在查询时执行。
 fn global_caller(vm: &mut Vm, globals: ObjectRef, name: &str) -> ObjectRef {
+    // 手工指令使控制流和调用目标来源可精确观察，构造器先验证栈高/跳转。
     let code = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadGlobal, 0),
@@ -674,18 +713,25 @@ fn global_caller(vm: &mut Vm, globals: ObjectRef, name: &str) -> ObjectRef {
         },
     )
     .unwrap();
+    // 代码数据只验证与分配，call_effect 不应实际执行其中指令。
     let code = vm.new_code(code).unwrap();
+    // 函数持有其代码/全局边，效果查询从当前载荷及环境读取快照。
     let function = vm
         .new_function("caller", code, globals, vec![], vec![])
         .unwrap();
+    // 辅助函数归还临时代码根，函数仍保留代码对象。
     vm.release(code).unwrap();
     function
 }
 
 #[test]
+/// 调用效果快照随全局遮蔽、内置回退、闭包 Cell 及递归边变化重新求证，不保留过期目标。
 fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
+    // 独立 VM 隔离全局与方法重绑定，避免其他场景状态干扰快照证明。
     let mut vm = Vm::new().unwrap();
+    // 源码名查找环境，更新其中键可改变契约或调用图，不能把首次查询缓存为永久证明。
     let globals = vm.new_dict().unwrap();
+    // 函数创建时捕获该内置字典身份，全局缺名才回退这里。
     let builtins = vm.new_dict().unwrap();
     vm.dict_set(
         globals,
@@ -693,6 +739,7 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
         Value::Object(builtins),
     )
     .unwrap();
+    // 明确声明 ReadOnly 的原生目标，作为可证明调用边。
     let pure = vm
         .allocate(ContextNativeFunction::new(
             "pure",
@@ -704,6 +751,7 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
             vec![],
         ))
         .unwrap();
+    // 声明 Mutating/External 的目标，使源码整体调用效果无法证明 ReadOnly。
     let impure = vm
         .allocate(ContextNativeFunction::new(
             "impure",
@@ -717,7 +765,9 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
         .unwrap();
     vm.dict_set(builtins, Value::Text("target".into()), Value::Object(pure))
         .unwrap();
+    // 第一层从环境解析 target，初始由内置字典提供 pure。
     let wrapper = global_caller(&mut vm, globals, "target");
+    // 外层再经全局 wrapper 调用，检验传递分析不只看一跳。
     let outer = global_caller(&mut vm, globals, "wrapper");
     vm.dict_set(
         globals,
@@ -732,7 +782,9 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
     vm.dict_delete(globals, &Value::Text("target".into()))
         .unwrap();
     assert_eq!(vm.call_effect(outer).unwrap(), Some(CallEffect::ReadOnly));
+    // 闭包捕获目标通过共享 Cell 更新，函数身份不变而调用图可变化。
     let cell = vm.new_cell(Some(Value::Object(pure))).unwrap();
+    // 手工指令使控制流和调用目标来源可精确观察，构造器先验证栈高/跳转。
     let code = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadDeref, 0),
@@ -747,7 +799,9 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
         },
     )
     .unwrap();
+    // 代码数据只验证与分配，call_effect 不应实际执行其中指令。
     let code = vm.new_code(code).unwrap();
+    // 源码经 LoadDeref 取目标再 Call，分析需读 Cell 当前内容而不执行函数体。
     let closure = vm
         .new_function("closure", code, globals, vec![], vec![cell])
         .unwrap();
@@ -756,6 +810,7 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
     assert_eq!(vm.call_effect(closure).unwrap(), None);
     vm.cell_set(cell, Value::Object(pure)).unwrap();
     assert_eq!(vm.call_effect(closure).unwrap(), Some(CallEffect::ReadOnly));
+    // 全局同名绑定回自己形成不终止调用图；查询必须通过去重收敛而非执行。
     let recursive = global_caller(&mut vm, globals, "recursive");
     vm.dict_set(
         globals,
@@ -763,7 +818,7 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
         Value::Object(recursive),
     )
     .unwrap();
-    // No function body is executed, including this non-terminating call graph.
+    // 查询不会执行任何源码体；即使图有无限自递归，visited 去重也应使分析结束。
     assert_eq!(
         vm.call_effect(recursive).unwrap(),
         Some(CallEffect::ReadOnly)
@@ -775,19 +830,25 @@ fn transitive_effect_queries_follow_rebinding_closures_and_recursive_graphs() {
     )
     .unwrap();
     assert_eq!(vm.call_effect(recursive).unwrap(), None);
+    // 归还测试拥有根，内部方法/签名/类型边由堆维护，避免重复 release。
     for object in [
         recursive, closure, code, cell, outer, wrapper, pure, impure, builtins, globals,
     ] {
         vm.release(object).unwrap();
     }
+    // 回收无根函数/全局/类型环，最终对象数应为零。
     vm.collect_cycles();
     assert_eq!(vm.object_count(), 0);
 }
 
 #[test]
+/// 条件两路径必须汇合事实，目标不一致时不可保留旧的已知纯目标；恢复相同目标后可重新证明。
 fn effect_control_flow_joins_do_not_keep_a_stale_known_call_target() {
+    // 独立 VM 隔离全局与方法重绑定，避免其他场景状态干扰快照证明。
     let mut vm = Vm::new().unwrap();
+    // 源码名查找环境，更新其中键可改变契约或调用图，不能把首次查询缓存为永久证明。
     let globals = vm.new_dict().unwrap();
+    // 明确声明 ReadOnly 的原生目标，作为可证明调用边。
     let pure = vm
         .allocate(ContextNativeFunction::new(
             "pure",
@@ -799,6 +860,7 @@ fn effect_control_flow_joins_do_not_keep_a_stale_known_call_target() {
             vec![],
         ))
         .unwrap();
+    // 声明 Mutating/External 的目标，使源码整体调用效果无法证明 ReadOnly。
     let impure = vm
         .allocate(ContextNativeFunction::new(
             "impure",
@@ -810,10 +872,12 @@ fn effect_control_flow_joins_do_not_keep_a_stale_known_call_target() {
             vec![],
         ))
         .unwrap();
+    // 两个分支初始指向同一 pure 身份，汇合可以保留该确定目标。
     for name in ["left", "right"] {
         vm.dict_set(globals, Value::Text(name.into()), Value::Object(pure))
             .unwrap();
     }
+    // 手工指令使控制流和调用目标来源可精确观察，构造器先验证栈高/跳转。
     let code = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadFast, 0),
@@ -834,7 +898,9 @@ fn effect_control_flow_joins_do_not_keep_a_stale_known_call_target() {
         },
     )
     .unwrap();
+    // 代码数据只验证与分配，call_effect 不应实际执行其中指令。
     let code = vm.new_code(code).unwrap();
+    // 函数持有其代码/全局边，效果查询从当前载荷及环境读取快照。
     let function = vm
         .new_function("choose", code, globals, vec![], vec![])
         .unwrap();
@@ -851,21 +917,29 @@ fn effect_control_flow_joins_do_not_keep_a_stale_known_call_target() {
         vm.call_effect(function).unwrap(),
         Some(CallEffect::ReadOnly)
     );
+    // 归还测试拥有根，内部方法/签名/类型边由堆维护，避免重复 release。
     for object in [function, code, pure, impure, globals] {
         vm.release(object).unwrap();
     }
+    // 回收无根函数/全局/类型环，最终对象数应为零。
     vm.collect_cycles();
     assert_eq!(vm.object_count(), 0);
 }
 
 #[test]
+/// 绑定接收者提供方法目标身份；类方法更新和实例字段遮蔽都必须影响效果查询。
 fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
+    // 独立 VM 隔离全局与方法重绑定，避免其他场景状态干扰快照证明。
     let mut vm = Vm::new().unwrap();
+    // 显式类型自举根，用于实例与绑定方法测试，最终归还并收集类型环。
     let roots = vm.bootstrap_types().unwrap();
+    // 源码名查找环境，更新其中键可改变契约或调用图，不能把首次查询缓存为永久证明。
     let globals = vm.new_dict().unwrap();
+    // Receiver 名义类型保存 helper/check 方法，实例可另以字段遮蔽 helper。
     let definition = vm
         .new_type("Receiver", roots.object, TypeConstructor::Record)
         .unwrap();
+    // 明确声明 ReadOnly 的原生目标，作为可证明调用边。
     let pure = vm
         .allocate(ContextNativeFunction::new(
             "helper",
@@ -877,6 +951,7 @@ fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
             vec![],
         ))
         .unwrap();
+    // 声明 Mutating/External 的目标，使源码整体调用效果无法证明 ReadOnly。
     let impure = vm
         .allocate(ContextNativeFunction::new(
             "helper",
@@ -888,6 +963,7 @@ fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
             vec![],
         ))
         .unwrap();
+    // 手工指令使控制流和调用目标来源可精确观察，构造器先验证栈高/跳转。
     let code = EndorCode::from_instructions(
         &[
             Instruction::new(Opcode::LoadFast, 0),
@@ -905,14 +981,18 @@ fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
         },
     )
     .unwrap();
+    // 代码数据只验证与分配，call_effect 不应实际执行其中指令。
     let code = vm.new_code(code).unwrap();
+    // 函数持有其代码/全局边，效果查询从当前载荷及环境读取快照。
     let function = vm
         .new_function("check", code, globals, vec![], vec![])
         .unwrap();
     vm.define_method(definition, "helper", pure).unwrap();
     vm.define_method(definition, "check", function).unwrap();
+    // 实例提供实际接收者身份，绑定效果分析可据此查 helper，未绑定函数则未知。
     let receiver = vm.new_object().unwrap();
     vm.attach_type(receiver, definition).unwrap();
+    // 绑定对象拥有函数和实际接收者边，分析可用 receiver 区分实例方法/字段。
     let Value::Object(bound) = vm.bind_attr(receiver, "check").unwrap() else {
         panic!("bound")
     };
@@ -927,6 +1007,7 @@ fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
     assert_eq!(vm.call_effect(bound).unwrap(), None);
     vm.del_attr(receiver, "helper").unwrap();
     assert_eq!(vm.call_effect(bound).unwrap(), Some(CallEffect::ReadOnly));
+    // 归还测试拥有根，内部方法/签名/类型边由堆维护，避免重复 release。
     for object in [
         bound,
         receiver,
@@ -941,6 +1022,7 @@ fn bound_source_effects_follow_the_actual_receiver_method_and_instance_field() {
     ] {
         vm.release(object).unwrap();
     }
+    // 回收无根函数/全局/类型环，最终对象数应为零。
     vm.collect_cycles();
     assert_eq!(vm.object_count(), 0);
 }