Infer conservative read-only source effects for method contracts

This commit is contained in:
2026-10-22 15:40:44 +08:00
parent 0513b96dfb
commit cd25f819f2
14 changed files with 236 additions and 13 deletions
+34
View File
@@ -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<String>,