diff --git a/crates/core/src/README.md b/crates/core/src/README.md index ee5e9f1..cd94d7b 100644 --- a/crates/core/src/README.md +++ b/crates/core/src/README.md @@ -5,7 +5,7 @@ | 文件 | 职责 | | --- | --- | | [lib.rs](lib.rs) | VM 类型导出、objects 类型兼容重导出（含 ReadAccess/CallSignature/CallType/CallEffect）、宿主调用与字节码 rustdoc 示例 | -| [vm.rs](vm.rs) | Vm 拥有 ObjectStore 与错误位置记录；对象操作和宿主 new_class 和显式/类型化Trait注册/关系查询显式委托给 objects；函数／字段检查统一开关、统一参数区间查询与函数类型配置 | +| [vm.rs](vm.rs) | Vm 拥有 ObjectStore 与错误位置记录；对象操作和宿主 new_class 和显式/类型化Trait注册/关系查询显式委托给 objects；函数／字段检查统一开关、统一参数区间/已知调用效果查询与函数类型配置 | | [frame.rs](frame.rs) | EndorFrame、栈条目、源码与原生委托返回契约执行根、执行位置元数据、ExecutionLimits | | [eval.rs](eval.rs) | execute／call、只读调用与依赖结果、参数绑定、原生实现前数量/类型/效果检查和原生/类型化Trait委托返回检查、可选注解/动态覆写兼容检查、源码类字段环境绑定、帧切换、取指分派、MakeFunction、结果根转移与失败清理 | diff --git a/crates/core/src/vm.rs b/crates/core/src/vm.rs index 910d640..db76a42 100644 --- a/crates/core/src/vm.rs +++ b/crates/core/src/vm.rs @@ -25,6 +25,11 @@ impl Vm { self.source_type_checks = enabled; Ok(()) } + /// Known whole-call effect; unproved source/delegated calls return None. + pub fn call_effect(&self, function: ObjectRef) -> Result, VmError> { + self.objects.call_effect(function) + } + pub fn call_arity(&self, function: ObjectRef) -> Result, VmError> { self.objects.call_arity(function) } diff --git a/crates/core/tests/README.md b/crates/core/tests/README.md index 9bf8de9..9764b8f 100644 --- a/crates/core/tests/README.md +++ b/crates/core/tests/README.md @@ -9,7 +9,7 @@ | [execution.rs](execution.rs) | wordcode 与校验、控制流、参数／默认值、嵌套帧、字节码函数创建／默认值／环境捕获、闭包、返回值存活、失败清理、限额 | | [types.rs](types.rs) | 名义身份、继承与实例关系、类型边保活／循环回收、只读类型元数据与外来句柄、显式Trait身份/继承/参数约束及后代更新原子性；统一函数分类、原生数量元数据/副作用前拒绝/能力更新/默认参数与返回类型错误根清理；仅远端执行 | | [typed_traits.rs](typed_traits.rs) | 类型化Trait登记、原子拒绝、源码检查关闭时的显式约束、宽参数调用、类型强边GC、体后实际能力结果检查与临时验证集合恢复；仅远端执行 | -| [method_contracts.rs](method_contracts.rs) | 源码/原生方法覆写参数逆变/返回协变、联合参数、效果、祖先替换原子性、动态名称重绑定/前向名称与体前拒绝/恢复及清理；仅远端执行 | +| [method_contracts.rs](method_contracts.rs) | 源码/原生方法覆写参数逆变/返回协变、联合参数、已证明源码只读/原生效果及共享赋值保守分类、祖先替换原子性、动态名称重绑定/前向名称与体前拒绝/恢复及清理；仅远端执行 | | [native_context.rs](native_context.rs) | 原生作用域根、分配失败清理、原生签名/联合与可空类型/固定与Delegated效果和委托返回根、绑定方法元数据、委托、只读结果分配／写入拒绝／依赖／校验与普通读取区分及失败恢复、弱引用过期及有界变更；仅远端执行 | 核心对象现由 objects 定义，本目录保留既有 endor_core 导入与 Vm 方法的兼容性检查。独立对象存储检查见 [objects/tests](../../objects/tests/README.md)。堆内部伪造句柄与计数溢出检查在 objects 的 src/heap.rs，公开示例由 src/lib.rs rustdoc 提供。文件职责见 [src](../src/README.md)，检查方式和结果边界见 [验证](../../../docs/operations/validation.md)。本地不执行测试；存在测试文件不代表某次提交已通过。返回 [core](../README.md)。 diff --git a/crates/core/tests/method_contracts.rs b/crates/core/tests/method_contracts.rs index 82fc04d..1b781af 100644 --- a/crates/core/tests/method_contracts.rs +++ b/crates/core/tests/method_contracts.rs @@ -24,6 +24,7 @@ fn source( vec![Value::Number(42.into()), result], CodeLayout { parameters: (0..parameters.len()).map(|i| format!("p{i}")).collect(), + locals: (0..parameters.len()).map(|i| format!("p{i}")).collect(), names: vec!["ran".into()], ..CodeLayout::default() }, @@ -339,7 +340,7 @@ fn native_overrides_preserve_union_inputs_and_do_not_expand_effects() { assert!(matches!( vm.define_method(child, "check", effect_fn), Err(VmError::OverrideViolation { - reason: "override expands native effects", + reason: "override expands known effects", .. }) )); @@ -443,3 +444,147 @@ fn unknown_forward_names_defer_until_call_without_entering_the_body() { vm.collect_cycles(); assert_eq!(vm.object_count(), 0); } + +#[test] +fn verified_source_read_only_effects_constrain_native_overrides() { + 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), + Instruction::simple(Opcode::ReturnValue), + ], + vec![], + CodeLayout { + parameters: vec!["self".into(), "value".into()], + locals: vec!["self".into(), "value".into()], + ..CodeLayout::default() + }, + ) + .unwrap() + .with_source_signature(SourceSignature { + parameters: vec!["PureBase".into(), "Number".into()], + return_type: "Number".into(), + method_owner: Some("PureBase".into()), + }) + .unwrap(); + assert!(code.is_statically_read_only()); + let code = vm.new_code(code).unwrap(); + 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)); + let receiver = vm.new_object().unwrap(); + vm.attach_type(receiver, child).unwrap(); + 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![]; + for effect in [ + CallEffect::Mutating, + CallEffect::External, + CallEffect::ReadOnly, + CallEffect::Delegated, + ] { + let function = vm + .allocate(ContextNativeFunction::new( + "check", + Native(CallSignature::exact( + vec![T::Any, T::Number], + T::Number, + effect, + )), + vec![], + )) + .unwrap(); + let version = vm.change_version(child).unwrap(); + let update = vm.define_method(child, "check", function); + if matches!(effect, CallEffect::Mutating | CallEffect::External) { + assert!(matches!( + update, + Err(VmError::OverrideViolation { + reason: "override expands known effects", + .. + }) + )); + assert_eq!(vm.change_version(child).unwrap(), version); + } else { + update.unwrap(); + } + assert_eq!( + vm.call_effect(function).unwrap(), + (effect != CallEffect::Delegated).then_some(effect) + ); + functions.push(function); + } + for object in functions.into_iter().chain([ + bound, + receiver, + child, + base, + source, + code, + globals, + roots.object, + roots.type_type, + ]) { + vm.release(object).unwrap(); + } + vm.collect_cycles(); + assert_eq!(vm.object_count(), 0); +} + +#[test] +fn shared_local_assignment_and_dynamic_calls_are_not_inferred_pure() { + let assignment = EndorCode::from_instructions( + &[ + Instruction::new(Opcode::LoadFast, 1), + Instruction::new(Opcode::StoreFast, 0), + Instruction::new(Opcode::LoadFast, 0), + Instruction::simple(Opcode::ReturnValue), + ], + vec![], + CodeLayout { + parameters: vec!["target".into(), "value".into()], + locals: vec!["target".into(), "value".into()], + ..CodeLayout::default() + }, + ) + .unwrap(); + assert!(!assignment.is_statically_read_only()); + let captured = EndorCode::from_instructions( + &[ + Instruction::new(Opcode::LoadConst, 0), + Instruction::new(Opcode::StoreDeref, 0), + Instruction::new(Opcode::LoadConst, 0), + Instruction::simple(Opcode::ReturnValue), + ], + vec![Value::Nil], + CodeLayout { + free_variables: vec!["captured".into()], + ..CodeLayout::default() + }, + ) + .unwrap(); + assert!(!captured.is_statically_read_only()); + let call = EndorCode::from_instructions( + &[ + Instruction::new(Opcode::LoadGlobal, 0), + Instruction::simple(Opcode::PushNull), + Instruction::new(Opcode::Call, 0), + Instruction::simple(Opcode::ReturnValue), + ], + vec![], + CodeLayout { + names: vec!["dynamic".into()], + ..CodeLayout::default() + }, + ) + .unwrap(); + assert!(!call.is_statically_read_only()); +} diff --git a/crates/core/tests/typed_traits.rs b/crates/core/tests/typed_traits.rs index f935af4..50ad5a2 100644 --- a/crates/core/tests/typed_traits.rs +++ b/crates/core/tests/typed_traits.rs @@ -39,6 +39,7 @@ fn source( vec![Value::Number(42.into()), value], CodeLayout { parameters: (0..types.len()).map(|i| format!("p{i}")).collect(), + locals: (0..types.len()).map(|i| format!("p{i}")).collect(), names: vec!["ran".into()], ..CodeLayout::default() }, diff --git a/crates/objects/src/README.md b/crates/objects/src/README.md index 8e53fef..f46c230 100644 --- a/crates/objects/src/README.md +++ b/crates/objects/src/README.md @@ -6,7 +6,7 @@ | --- | --- | | [lib.rs](lib.rs) | 包边界、对象类型／ObjectStore 公开导出（含Trait/MethodRequirement/TypedMethodRequirement/SourceSignature/AnnotationType/CallArity/CallSignature/CallType/CallEffect/ReadAccess）与独立存储 rustdoc 示例 | | [object.rs](object.rs) | Value、CompareOp、ObjectPayload（含显式函数标记）、ObjectHeader、EndorObject、Record、可发布数量元数据的 NativeFunction | -| [types.rs](types.rs) | 托管名义类型、显式 Object/Type 引导、继承查询、受管方法表／接收者绑定、类字段、显式/类型化Trait定义、强类型签名边与声明约束、实例方法遮蔽检查和宿主缓存依赖名、原生构造委托、统一源码/原生/绑定方法参数区间查询与能力验证、声明环境托管边、字段构造／写入检查与标记为校验读取的注解解析／匹配 | +| [types.rs](types.rs) | 托管名义类型、显式 Object/Type 引导、继承查询、受管方法表／接收者绑定、类字段、显式/类型化Trait定义、强类型签名边与声明约束、实例方法遮蔽检查和宿主缓存依赖名、原生构造委托、统一源码/原生/绑定方法参数区间和已知效果查询与能力验证、声明环境托管边、字段构造／写入检查与标记为校验读取的注解解析／匹配 | | [contracts.rs](contracts.rs) | 方法参数逆变/返回协变、名义/能力/联合包含关系、祖先方法更新的后代检查、动态注解调用前复查、类型化能力替换/返回约束与临时递归验证集合 | | [native.rs](native.rs) | NativeContext、CallArity/CallSignature 类型、Delegated/固定效果元数据、调用前检查、签名类型强边、上下文原生函数、作用域语言函数工厂、显式能力声明入口、函数标记、根与非递归委托调用 | | [changes.rs](changes.rs) | 合并变更批次、变更键与有界通知额度 | @@ -16,7 +16,7 @@ | [store.rs](store.rs) | ObjectStore、空堆创建、字段检查配置／属性写入屏障、详细读取区域结果、逐线程临时能力检查集合、对象操作、retain／release 和回收入口、弱 Function 类型配置与分配分类 | | [store_builtins.rs](store_builtins.rs) | 载荷校验、代码／函数工厂、Dict／Cell 操作及键语义 | | [instruction.rs](instruction.rs) | Opcode、Instruction、wordcode 编解码、MakeFunction／比较参数与跳转读取接口 | -| [code.rs](code.rs) | CodeLayout、EndorCode／EndorCodeObject、可选源码签名、共享不可变代码和操作数／控制流／栈验证 | +| [code.rs](code.rs) | CodeLayout、EndorCode／EndorCodeObject、可选源码签名、保守只读字节码证明、共享不可变代码和操作数／控制流／栈验证 | | [error.rs](error.rs) | 对象、代码与执行共用的 VmError（含TraitViolation、OverrideViolation、UnknownAnnotation、TypeMismatch），避免反向依赖 core | 对象操作变更同步 [对象模型](../../../docs/runtime/objects.md)，内置载荷同步 [基本对象](../../../docs/runtime/builtins.md)。新增操作码需要同时修改本包 instruction.rs／code.rs 和 core 的 eval.rs 分派，见 [字节码 VM](../../../docs/runtime/bytecode.md)。 diff --git a/crates/objects/src/code.rs b/crates/objects/src/code.rs index 2fe18ee..da7592e 100644 --- a/crates/objects/src/code.rs +++ b/crates/objects/src/code.rs @@ -106,6 +106,40 @@ impl EndorCode { self.signature.as_ref() } + /// Conservative proof over validated instructions. Local assignment is not + /// automatically pure: shared-reference assignment may update its old value. + /// Unknown calls and writes remain unknown, even when they could be safe for + /// a particular invocation. New opcodes require an explicit audit here. + pub fn is_statically_read_only(&self) -> bool { + self.instructions.iter().all(|decoded| { + matches!( + decoded.instruction.opcode, + Opcode::Nop + | Opcode::LoadConst + | Opcode::LoadFast + | Opcode::DeleteFast + | Opcode::LoadGlobal + | Opcode::PopTop + | Opcode::Copy + | Opcode::Swap + | Opcode::PushNull + | Opcode::ReturnValue + | Opcode::JumpForward + | Opcode::JumpBackward + | Opcode::PopJumpIfFalse + | Opcode::PopJumpIfTrue + | Opcode::ToBool + | Opcode::UnaryNot + | Opcode::CompareOp + | Opcode::LoadDeref + | Opcode::LoadClosure + | Opcode::LoadAttr + | Opcode::BuildMap + | Opcode::MakeFunction + ) + }) + } + pub fn with_location( mut self, name: impl Into, diff --git a/crates/objects/src/contracts.rs b/crates/objects/src/contracts.rs index ae9612e..f44f491 100644 --- a/crates/objects/src/contracts.rs +++ b/crates/objects/src/contracts.rs @@ -170,7 +170,7 @@ impl ObjectStore { parameters, variadic: None, returns: resolve(&signature.return_type)?.into(), - effect: None, + effect: self.call_effect(function)?, })) } fn own_method( @@ -303,7 +303,7 @@ impl ObjectStore { CallEffect::External | CallEffect::Delegated => true, }; if !compatible { - return Err(invalid("override expands native effects")); + return Err(invalid("override expands known effects")); } } Ok(()) diff --git a/crates/objects/src/types.rs b/crates/objects/src/types.rs index 5b614a8..ceaff24 100644 --- a/crates/objects/src/types.rs +++ b/crates/objects/src/types.rs @@ -485,6 +485,33 @@ impl ObjectStore { Ok(signature) } + /// Known whole-call effect, after unwrapping bound receivers. Delegated + /// native wrappers and source code with unproved operations remain unknown. + /// This query does not execute code or freeze dynamic globals/call targets. + pub fn call_effect(&self, function: ObjectRef) -> Result, VmError> { + let mut current = function; + loop { + let payload = self.object(current)?.payload(); + if let Some(bound) = payload.as_any().downcast_ref::() { + current = bound.function; + continue; + } + if let Some(source) = payload + .as_any() + .downcast_ref::() + { + return Ok(self + .payload::(source.code(), "code")? + .code() + .is_statically_read_only() + .then_some(crate::CallEffect::ReadOnly)); + } + return Ok(self.native_signature(current)?.and_then(|signature| { + (signature.effect != crate::CallEffect::Delegated).then_some(signature.effect) + })); + } + } + /// Unified source/native positional interval, after any bound receivers. /// None means no published native metadata (including generic Type construction). pub fn call_arity(&self, function: ObjectRef) -> Result, VmError> { diff --git a/docs/README.md b/docs/README.md index d8cff76..bf75a2c 100644 --- a/docs/README.md +++ b/docs/README.md @@ -6,7 +6,7 @@ | 解释执行、资源修订与引擎升级 | [执行与版本](architecture/execution-and-versions.md) | frontend／compiler／core | | EndorObject、句柄、默认操作 | [对象模型](runtime/objects.md) | objects/src | | 原生上下文、只读调用、子调用读取依赖及校验分类、统一参数数量/类型/联合/固定与委托效果、委托返回与变更通知 | [原生调用](runtime/native-calls.md) | objects/src/native.rs、changes.rs、core/src/eval.rs | -| 托管类型、宿主类注册、原生分配继承、字段存储、显式/类型化能力、函数分类、声明字段/源码注解与方法覆写检查 | [名义类型/方法覆写](runtime/types.md) | objects/src/types.rs、contracts.rs | +| 托管类型、宿主类注册、原生分配继承、字段存储、显式/类型化能力、函数分类/已知效果、保守源码只读证明、声明字段/源码注解与方法覆写检查 | [名义类型/方法覆写](runtime/types.md) | objects/src/types.rs、contracts.rs | | Number、String、Dict、Cell、Function | [基本对象](runtime/builtins.md) | objects/src | | 源码读取与来源 | [Reader](runtime/reader.md) | frontend/src/reader.rs | | 词法、语法、裸赋值和诊断 | [Frontend](runtime/frontend.md) | frontend/src/lexer.peg／grammar.peg | diff --git a/docs/contributing/handoff.md b/docs/contributing/handoff.md index c022e55..8580c8c 100644 --- a/docs/contributing/handoff.md +++ b/docs/contributing/handoff.md @@ -21,7 +21,7 @@ Aster 是可嵌入引擎，只保留 objects、core、frontend、compiler。Obje ## 当前缺口 -平台资源版本／依赖锁、源码闭包、数值算术、完整异常传播、内存配额、可靠取消、不可信代码沙箱、自动 GC 和宿主 panic 后执行根恢复尚未完成。源码函数参数／返回注解已支持默认关闭的运行时检查，Tessera 显式启用；普通名称按调用时函数全局解析，声明字段构造／写入检查已接入同一可选开关；完整初始化、静态类型／效果与原生参数/返回类型签名仍未完成；统一位置参数数量已接入原生调用与显式能力检查，见[类型机制](../runtime/types.md#源码函数注解检查)。不引入 Python 元类。UI 接入适配由 Tessera 实现。通用 ObjectPayload::assign_from 允许宿主对象选择共享引用赋值；协议和根计数归 Aster，UI 挂载、布局、绘制仍归 Tessera，见字节码 VM 的共享引用章节。 +平台资源版本／依赖锁、源码闭包、数值算术、完整异常传播、内存配额、可靠取消、不可信代码沙箱、自动 GC 和宿主 panic 后执行根恢复尚未完成。源码函数参数／返回注解已支持默认关闭的运行时检查，Tessera 显式启用；普通名称按调用时函数全局解析，声明字段构造／写入检查已接入同一可选开关；完整初始化、完整静态类型／传递效果仍未完成；原生参数/返回签名、类型化Trait、覆写方差、统一位置参数数量、实例方法遮蔽检查与保守源码只读证明已接入原生调用和显式能力检查，见[类型机制](../runtime/types.md#源码函数注解检查)。不引入 Python 元类。UI 接入适配由 Tessera 实现。通用 ObjectPayload::assign_from 允许宿主对象选择共享引用赋值；协议和根计数归 Aster，UI 挂载、布局、绘制仍归 Tessera，见字节码 VM 的共享引用章节。 ## 工作约定 diff --git a/docs/runtime/README.md b/docs/runtime/README.md index b48c436..10aa624 100644 --- a/docs/runtime/README.md +++ b/docs/runtime/README.md @@ -2,7 +2,7 @@ | 文档 | 内容 | | --- | --- | -| [types.md](types.md) | 托管 Object／Type、名义继承、方法覆写/类型化Trait/动态检查、声明字段／函数注解检查、构造与类型边生命周期 | +| [types.md](types.md) | 托管 Object／Type、名义继承、方法覆写/类型化Trait/已知效果与源码只读证明/动态检查、声明字段／函数注解检查、构造与类型边生命周期 | | [objects.md](objects.md) | 对象、句柄与默认操作 | | [native-calls.md](native-calls.md) | 原生上下文、读取分类、统一参数数量/类型/联合/固定与委托效果、非递归委托返回、弱引用、托管赋值与变更批次 | | [builtins.md](builtins.md) | Number、String、Dict、Cell、Function、异常数据 | diff --git a/docs/runtime/native-calls.md b/docs/runtime/native-calls.md index 74fb9b8..b363f56 100644 --- a/docs/runtime/native-calls.md +++ b/docs/runtime/native-calls.md @@ -100,7 +100,7 @@ NativeCallable::signature 默认 None，明确表示尚未发布类型/效果契 NativeResult::Invoke 仍是尾委托，不递归进入 Rust/VM。VM 为每层已声明的返回契约保留检查项；委托原生立即返回或 Endor 帧返回时，按由内到外顺序验证全部契约。返回定义作为执行根保留，原生载荷替换、释放原委托者或源码全局重绑定不会使检查丢失。准备失败、帧限额、指令限额、错误返回与正常完成都释放这些执行根。委托不会为检查额外创建 VM 帧；仍共享每次原生分派和 Endor 指令预算。NativeContext::execute 单独返回 Invoke 时，调用者须使用具有等效最终返回检查的求值器；通常直接使用 Vm::call。 -CallEffect::ReadOnly 声明只读现存对象，可分配临时结果；Delegated 声明原生包装自身只读，但后续委托的整体效果动态确定，VM 保持同一只读/预算作用域并检查实际目标；Mutating 与 External 在 ObjectStore 只读作用域内、进入实现前拒绝。普通执行允许这些效果。ReadOnly 声明不绕过已有写屏障，也不证明可信 Rust 不会进行隐藏 I/O；未知旧原生函数仍沿原调用/宿主检查，不能把 None 理解为纯函数。这不是静态效果推断、完整 I/O 沙箱或对阻塞原生代码的抢占。 +CallEffect::ReadOnly 声明只读现存对象，可分配临时结果；Delegated 声明原生包装自身只读，但后续委托的整体效果动态确定，VM 保持同一只读/预算作用域并检查实际目标；Mutating 与 External 在 ObjectStore 只读作用域内、进入实现前拒绝。普通执行允许这些效果。ReadOnly 声明不绕过已有写屏障，也不证明可信 Rust 不会进行隐藏 I/O；未知旧原生函数仍沿原调用/宿主检查，不能把 None 理解为纯函数。这不是完整 I/O 沙箱或对阻塞原生代码的抢占。统一已知效果查询和保守源码只读证明见[类型主题](types.md#已知调用效果与保守源码证明)。 Tessera 的 measure/arrange/paint/hitTest、Point 几何查询、Window、Block/Container/Page、Mount、Task、Event、Subscription 方法和 ObjectList.at 发布签名。Page.open 的 Window | Unit、Page.window 的 Window | Unit 返回，以及 Block.on 的 Bool | String 可选阶段有准确元数据；Mount 的父/子/同级/Page 弱查询为可空结果。Mount.bounds 现在返回带 Bounds 名义类型的现有几何记录，可直接组合到 Point.inside 或视觉方法。滚动位置/字典等通用记录仍声明 Object，不冒充新语言类型；任务 owner 的具体资源资格仍按原域检查。构造器和其他管理 API 的签名覆盖仍未全部接入。已接入的方法覆写方差与动态名称规则见类型主题。旧能力注册保留数量模式；类型化能力还检查类型/已知效果，并在实际返回和尾委托结果处保留能力返回约束。 diff --git a/docs/runtime/types.md b/docs/runtime/types.md index c8feada..352385a 100644 --- a/docs/runtime/types.md +++ b/docs/runtime/types.md @@ -126,7 +126,7 @@ new_class 在发布之前校验本类覆写，失败释放候选定义。define_ 未知前向注解在类建立和方法更新时暂缓，其他已知不兼容以 OverrideViolation 报类名、方法名和原因。启用 VM 类型检查时，源码和原生调用均在进入实现前检查实际接收者所属方法的当前替换契约；UnknownAnnotation 此时不能暂缓。普通函数的首参数恰好是对象，不会因此被视为方法。默认接收者也使用实际默认参数值参与复查。每次复查动态全局注解，所以 REPL 重绑定使旧覆写不兼容时，函数体执行前拒绝；恢复兼容绑定后可继续普通调用。不回滚先前已发生的其他输入副作用。 -已知原生效果只允许缩小：ReadOnly 基类只能被 ReadOnly 原生覆写；Mutating 基类不允许 External 覆写；External 可接受三者。源码和原生 Delegated 的整体效果均未知，不能声称已经证明其纯度；实际只读布局/绘制仍通过原有堆屏障与原生效果入口限制执行。未知旧基类类型签名仍是未证明的兼容边界，旧 new_trait 仍仅校验数量；new_typed_trait 提供独立类型与已知效果要求，见下文。 +已知调用效果只允许缩小：ReadOnly 基类不能被已知 Mutating/External 覆写；Mutating 基类不允许 External 覆写；External 可接受三者。已证明只读的源码方法参与同一检查；其余源码和原生 Delegated 的整体效果均未知，不能声称已经证明其纯度；实际只读布局/绘制仍通过原有堆屏障与原生效果入口限制执行。未知旧基类类型签名仍是未证明的兼容边界，旧 new_trait 仍仅校验数量；new_typed_trait 提供独立类型与已知效果要求，见下文。 回归源码 core/tests/method_contracts.rs 覆盖合法参数扩大/返回缩小、错误参数/返回、祖先替换对已有覆写后代的原子拒绝、调用前动态重绑定拒绝和恢复、前向名称、原生联合与效果及根清理，仅编译，不在本地执行。 @@ -145,6 +145,17 @@ ObjectStore/Vm::new_typed_trait(name, Vec) 以每项 nam 嵌套能力比较按线程/定义/能力保留临时验证集合，对已经在校验的同一名义能力关系按递归约束处理，避免无限递归；它不建立新声明关系。集合不持有 GC 根，RAII 在成功、错误和展开路径清理，不让失败验证成为后续成功缓存。没有长期签名缓存；动态名称每次仍从原环境解析。 -源码和 Delegated 包装的整体效果仍未知，类型化 ReadOnly 要求不等于已经证明源码纯度。已知原生效果会比较，真正只读布局/绘制继续执行堆屏障；普通输入中源码副作用仍按现有运行模式处理。没有泛型/关联类型/效果推断或 Trait 源码声明语法。Tessera 的四个宿主能力使用类型化要求，其中 Presentable 允许普通展示构造副作用，不额外宣称纯函数。 +部分源码可由已验证字节码证明只读（见下文）；其余源码和 Delegated 包装的整体效果仍未知，类型化 ReadOnly 要求不等于已经证明这些函数纯度。已知效果会比较，真正只读布局/绘制继续执行堆屏障；普通输入中源码副作用仍按现有运行模式处理。没有泛型/关联类型/完整传递效果推断或 Trait 源码声明语法。Tessera 的四个宿主能力使用类型化要求，其中 Presentable 允许普通展示构造副作用，不额外宣称纯函数。 core/tests/typed_traits.rs 覆盖登记失败原子性、参数扩大仍可直接调用、全局检查关闭时的显式能力实际参数/返回检查、签名类型保活/回收，以及体内动态改变返回对象能力后的最终拒绝和验证集合恢复，仅编译未本地执行。 + + +## 已知调用效果与保守源码证明 + +ObjectStore/Vm::call_effect(function) 返回已知的整体 CallEffect 或 None，解包绑定方法后检查真实目标；原生签名照常验证，Delegated 包装整体未知，旧函数和通用Type构造也不猜测。查询不执行函数，不固定动态全局名称，不新增托管强边。参数/返回类型签名查询仍由 native_signature 和源码注解承担。 + +EndorCode::is_statically_read_only 只在全部已验证指令都在只读白名单内时返回true。读取、控制流、局部删除、创建新Dict/Function允许；Call、所有Store、DeleteGlobal/DeleteDeref、BuildClass及未来未审阅指令均保守未知。StoreFast也不能直接视为纯度：已有局部值可能通过共享引用赋值更新原对象。未知不表示一定有写入；创建新结果后填字段或调用纯函数仍可能安全，但本证明不作别名/新鲜性或调用图推断。不可达指令也参与保守扫描，嵌套函数代码不被当作工厂已执行的函数体。 + +源码方法的此项只读证明用于方法替换/类型化能力的已知效果比较，不扩大全局源码检查开关的范围，也不拒绝目前未知的源码实现。只读执行的堆屏障和实际原生目标检查继续沿原VM帧、预算和尾委托作用域传递；它们不能被静态结果替代。可信ObjectPayload读取/比较仍属于宿主约定，不构成Rust隐藏I/O沙箱；只读不证明终止。完整调用图、可变全局/闭包目标和新对象写入的静态证明仍未实现。 + +method_contracts.rs新增已证明源码基类的原生效果扩大拒绝/原子性、绑定查询，以及共享局部赋值、自由Cell写入、动态调用保持未知的回归源码。仅编译，不在本地执行。