Backported assignment contexts from symphony.
Initial support for operation call obligations.
Add explicit operation contexts at function entry point.
Add obligation for operation call when op has precondition.