{"record":{"id":"fa995f74f82c9aa9","repo":"diem/diem","slug":"not-allowed-to-assume-update-invariant","errorCode":null,"errorMessage":"Not allowed to assume update invariant","messagePattern":"Not allowed to assume update invariant","errorType":"panic","errorClass":null,"httpStatus":null,"severity":"error","filePath":"language/move-prover/bytecode/src/global_invariant_instrumentation_v2.rs","lineNumber":666,"sourceCode":"    /// xlated_invariants that is also in inv_set at the current location,\n    fn assert_or_assume_translated_invariants(\n        &mut self,\n        xlated_invariants: &[(Loc, GlobalId, Exp)],\n        inv_set: &BTreeSet<GlobalId>,\n        prop_kind: PropKind,\n    ) {\n        let global_env = self.builder.global_env();\n        for (loc, mid, cond) in xlated_invariants {\n            if inv_set.contains(mid) {\n                // Check for hard-to-debug coding error (this is not a user error)\n                if inv_set.contains(mid)\n                    && matches!(prop_kind, PropKind::Assume)\n                    && matches!(\n                        global_env.get_global_invariant(*mid).unwrap().kind,\n                        ConditionKind::GlobalInvariantUpdate(..)\n                    )\n                {\n                    panic!(\"Not allowed to assume update invariant\");\n                }\n                self.emit_invariant(loc, cond, prop_kind);\n            }\n        }\n    }\n\n    /// Emit an assert or assume for one invariant, give location and expression for the property\n    fn emit_invariant(&mut self, loc: &Loc, cond: &Exp, prop_kind: PropKind) {\n        self.builder.set_next_debug_comment(format!(\n            \"global invariant {}\",\n            loc.display(self.builder.global_env())\n        ));\n        // No error messages on assumes\n        if prop_kind == PropKind::Assert {\n            self.builder\n                .set_loc_and_vc_info(loc.clone(), GLOBAL_INVARIANT_FAILS_MESSAGE);\n        }\n        self.builder","sourceCodeStart":648,"sourceCodeEnd":684,"githubUrl":"https://github.com/diem/diem/blob/fc4714a8ea273b6efe8b13dbce72ea60aad9a16c/language/move-prover/bytecode/src/global_invariant_instrumentation_v2.rs#L648-L684","documentation":"A safety check in assert_or_assume_translated_invariants: update invariants (GlobalInvariantUpdate) may only be asserted, never assumed, because assuming an update invariant would be unsound (it describes state changes, not state). If the pass would emit an Assume of an update invariant, it panics instead.","triggerScenarios":"A translated invariant set marked as PropKind::Assume contains an update invariant — arising from a bug or modification in how invariants are translated/assigned prop kinds for a bytecode (e.g. around opaque calls or reads where update invariants should only be asserted).","commonSituations":"Patched instrumentation logic emitting assumes at points the original design only asserts; spec-language changes letting update invariants become applicable at assume points.","solutions":["Use unmodified v2 instrumentation logic, which only assumes plain global invariants","If customizing the pass, filter GlobalInvariantUpdate invariants out of Assume sets before calling emit_invariant","Report upstream with the Move function/spec that reproduces it"],"exampleFix":"// before: assuming update invariant\nlet kind = PropKind::Assume;\n// after: only assert update invariants\nlet kind = if is_update_inv { PropKind::Assert } else { PropKind::Assume };","handlingStrategy":"validation","validationCode":"fn safe_prop_kind(inv_kind: &ConditionKind, desired: PropKind) -> PropKind {\n    if matches!(inv_kind, ConditionKind::GlobalInvariantUpdate(_)) { PropKind::Assert } else { desired }\n}","typeGuard":"fn is_update_invariant(kind: &ConditionKind) -> bool {\n    matches!(kind, ConditionKind::GlobalInvariantUpdate(_))\n}","tryCatchPattern":"// in custom emit logic:\nif is_update_invariant(&inv.kind) && matches!(kind, PropKind::Assume) {\n    eprintln!(\"refusing to assume update invariant; emitting assert instead\");\n}","preventionTips":["Never mark GlobalInvariantUpdate invariants with PropKind::Assume in custom passes","Filter update invariants out of assume sets before emitting","Keep instrumentation translation logic aligned with upstream design"],"tags":["move-prover","panic","unsound-assume","global-invariants"],"backgroundTag":"unsound-invariant-assume","analyzedSha":"fc4714a8ea273b6efe8b13dbce72ea60aad9a16c","analyzedAt":"2026-09-04T21:07:05.890Z","contentChangedAt":"2026-09-04T21:07:05.890Z","schemaVersion":2},"datasetVersion":"2026-09-12T02:17:10.037Z"}