diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index a5e9b15590..ea2994ec5d 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -463,9 +463,10 @@ final case class AmbiguousThis[G]()(implicit val o: Origin) extends Expr[G] with
   var ref: Option[ThisTarget[G]] = None
 }
 
-final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with ThisObjectImpl[G]
-final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends Expr[G] with ThisModelImpl[G]
-final case class ThisSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
+sealed trait ThisDeclaration[G] extends Expr[G] with ThisDeclarationImpl[G]
+final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisObjectImpl[G]
+final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisModelImpl[G]
+final case class ThisSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisSeqProgImpl[G]
 
 final case class AmbiguousResult[G]()(implicit val o: Origin) extends Expr[G] with AmbiguousResultImpl[G] {
   var ref: Option[ResultTarget[G]] = None
diff --git a/src/col/vct/col/ast/declaration/DeclarationImpl.scala b/src/col/vct/col/ast/declaration/DeclarationImpl.scala
index 6b11a5e6ee..0a93d649de 100644
--- a/src/col/vct/col/ast/declaration/DeclarationImpl.scala
+++ b/src/col/vct/col/ast/declaration/DeclarationImpl.scala
@@ -1,5 +1,6 @@
 package vct.col.ast.declaration
 
+import vct.col.ast.node.NodeImpl
 import vct.col.ast.{AbstractRewriter, Declaration}
 import vct.col.check.{CheckContext, CheckError, TypeError, TypeErrorExplanation, TypeErrorText}
 import vct.col.debug.{DebugRewriteState, Dropped, NotProcessed}
@@ -9,7 +10,7 @@ import vct.col.typerules.{CoercingRewriter, NopCoercingRewriter}
 
 import scala.reflect.ClassTag
 
-trait DeclarationImpl[G] { this: Declaration[G] =>
+trait DeclarationImpl[G] extends NodeImpl[G] { this: Declaration[G] =>
   var debugRewriteState: DebugRewriteState = NotProcessed
 
   def drop(): Unit = debugRewriteState = Dropped
@@ -32,4 +33,7 @@ trait DeclarationImpl[G] { this: Declaration[G] =>
       case CoercingRewriter.IncoercibleText(e, m) => Seq(TypeErrorText(e, m))
       case CoercingRewriter.IncoercibleExplanation(e, m) => Seq(TypeErrorExplanation(e, m))
     }
+
+  override def enterCheckContextDeclarationStack(context: CheckContext[G]): Seq[Declaration[G]] =
+    this +: context.declarationStack
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/declaration/category/ApplicableImpl.scala b/src/col/vct/col/ast/declaration/category/ApplicableImpl.scala
index d8511dc1b6..adee5539de 100644
--- a/src/col/vct/col/ast/declaration/category/ApplicableImpl.scala
+++ b/src/col/vct/col/ast/declaration/category/ApplicableImpl.scala
@@ -1,16 +1,16 @@
 package vct.col.ast.declaration.category
 
+import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.util.Declarator
 import vct.col.ast.{Applicable, Declaration, Node, Type, Variable}
 import vct.col.check.CheckContext
 
-trait ApplicableImpl[G] extends Declarator[G] { this: Applicable[G] =>
+trait ApplicableImpl[G] extends DeclarationImpl[G] with Declarator[G] { this: Applicable[G] =>
   def args: Seq[Variable[G]]
   def returnType: Type[G]
   def body: Option[Node[G]]
 
   override def declarations: Seq[Declaration[G]] = args
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    super.enterCheckContext(context).withApplicable(this)
+  override def enterCheckContextCurrentApplicable(context: CheckContext[G]): Option[Applicable[G]] = Some(this)
 }
diff --git a/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala b/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala
index 51d9be44d4..f5db15a039 100644
--- a/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala
+++ b/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala
@@ -1,5 +1,6 @@
 package vct.col.ast.declaration.global
 
+import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.{Class, Declaration, Endpoint, EndpointGuard, EndpointName, Node, SeqAssign, SeqProg}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
@@ -19,7 +20,7 @@ object SeqProgImpl {
     })
 }
 
-trait SeqProgImpl[G] extends Declarator[G] with SeqProgOps[G] { this: SeqProg[G] =>
+trait SeqProgImpl[G] extends DeclarationImpl[G] with Declarator[G] with SeqProgOps[G] { this: SeqProg[G] =>
   override def declarations: Seq[Declaration[G]] = args ++ endpoints ++ decls
 
   override def layout(implicit ctx: Ctx): Doc =
@@ -30,8 +31,9 @@ trait SeqProgImpl[G] extends Declarator[G] with SeqProgOps[G] { this: SeqProg[G]
       "}"
     ))
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    super.enterCheckContext(context)
-      .withSeqProg(this)
-      .withCurrentParticipatingEndpoints(endpoints)
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] =
+    context.withCurrentParticipatingEndpoints(endpoints)
+
+  override def enterCheckContextCurrentSeqProg(context: CheckContext[G]): Option[SeqProg[G]] =
+    Some(this)
 }
diff --git a/src/col/vct/col/ast/expr/context/ThisDeclarationImpl.scala b/src/col/vct/col/ast/expr/context/ThisDeclarationImpl.scala
new file mode 100644
index 0000000000..4a471cea89
--- /dev/null
+++ b/src/col/vct/col/ast/expr/context/ThisDeclarationImpl.scala
@@ -0,0 +1,14 @@
+package vct.col.ast.expr.context
+
+import vct.col.ast.{Declaration, ThisDeclaration}
+import vct.col.ast.expr.ExprImpl
+import vct.col.check.{CheckContext, CheckError, ThisOutsideScopeError}
+import vct.col.ref.Ref
+
+trait ThisDeclarationImpl[G] extends ExprImpl[G] { this: ThisDeclaration[G] =>
+  def cls: Ref[G, _ <: Declaration[G]]
+
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    if(!context.declarationStack.contains(cls.decl)) super.check(context) ++ Seq(ThisOutsideScopeError(this))
+    else super.check(context)
+}
diff --git a/src/col/vct/col/ast/expr/context/ThisModelImpl.scala b/src/col/vct/col/ast/expr/context/ThisModelImpl.scala
index 92c89775a7..c47135fba8 100644
--- a/src/col/vct/col/ast/expr/context/ThisModelImpl.scala
+++ b/src/col/vct/col/ast/expr/context/ThisModelImpl.scala
@@ -4,7 +4,7 @@ import vct.col.ast.{TModel, ThisModel, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisModelOps
 
-trait ThisModelImpl[G] extends ThisModelOps[G] { this: ThisModel[G] =>
+trait ThisModelImpl[G] extends ThisDeclarationImpl[G] with ThisModelOps[G] { this: ThisModel[G] =>
   override def t: Type[G] = TModel(cls)
 
   override def precedence: Int = Precedence.ATOMIC
diff --git a/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala b/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala
index 32c5c15481..7e0c1bf143 100644
--- a/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala
+++ b/src/col/vct/col/ast/expr/context/ThisObjectImpl.scala
@@ -3,8 +3,9 @@ package vct.col.ast.expr.context
 import vct.col.ast.{TClass, ThisObject, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisObjectOps
+import vct.col.check.{CheckContext, CheckError}
 
-trait ThisObjectImpl[G] extends ThisObjectOps[G] { this: ThisObject[G] =>
+trait ThisObjectImpl[G] extends ThisDeclarationImpl[G] with ThisObjectOps[G] { this: ThisObject[G] =>
   override def t: Type[G] = TClass(cls)
 
   override def precedence: Int = Precedence.ATOMIC
diff --git a/src/col/vct/col/ast/expr/context/ThisSeqProgImpl.scala b/src/col/vct/col/ast/expr/context/ThisSeqProgImpl.scala
index 8facc387d8..5c1edc1d49 100644
--- a/src/col/vct/col/ast/expr/context/ThisSeqProgImpl.scala
+++ b/src/col/vct/col/ast/expr/context/ThisSeqProgImpl.scala
@@ -4,7 +4,7 @@ import vct.col.ast.{TAnyClass, TSeqProg, ThisSeqProg, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisSeqProgOps
 
-trait ThisSeqProgImpl[G] extends ThisSeqProgOps[G] { this: ThisSeqProg[G] =>
+trait ThisSeqProgImpl[G] extends ThisDeclarationImpl[G] with ThisSeqProgOps[G] { this: ThisSeqProg[G] =>
   override def t: Type[G] = TSeqProg(cls)
 
   override def precedence: Int = Precedence.ATOMIC
diff --git a/src/col/vct/col/ast/family/location/FieldLocationImpl.scala b/src/col/vct/col/ast/family/location/FieldLocationImpl.scala
index 6abc4eee7e..b3ef8b9af7 100644
--- a/src/col/vct/col/ast/family/location/FieldLocationImpl.scala
+++ b/src/col/vct/col/ast/family/location/FieldLocationImpl.scala
@@ -1,10 +1,15 @@
 package vct.col.ast.family.location
 
-import vct.col.ast.FieldLocation
+import vct.col.ast.{FieldLocation, Final}
 import vct.col.print._
 import vct.col.ast.ops.FieldLocationOps
+import vct.col.check.{CheckContext, CheckError, FinalPermission}
+
+trait FieldLocationImpl[G] extends FieldLocationOps[G] with LocationImpl[G] { this: FieldLocation[G] =>
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    if(field.decl.flags.collectFirst { case Final() => () }.nonEmpty) Seq(FinalPermission(this)) ++ super.check(context)
+    else super.check(context)
 
-trait FieldLocationImpl[G] extends FieldLocationOps[G] { this: FieldLocation[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     obj.bind(Precedence.POSTFIX) <> "." <> ctx.name(field)
 }
diff --git a/src/col/vct/col/ast/family/location/LocationImpl.scala b/src/col/vct/col/ast/family/location/LocationImpl.scala
index c2826f87a6..7537fa5465 100644
--- a/src/col/vct/col/ast/family/location/LocationImpl.scala
+++ b/src/col/vct/col/ast/family/location/LocationImpl.scala
@@ -1,9 +1,13 @@
 package vct.col.ast.family.location
 
+import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.{AmbiguousLocation, ArrayLocation, FieldLocation, HeapVariableLocation, InstancePredicateLocation, Location, ModelLocation, PointerLocation, PredicateLocation, SilverFieldLocation, Type}
 import vct.col.ast.ops.LocationFamilyOps
+import vct.col.check.{CheckContext, CheckError}
+
+trait LocationImpl[G] extends NodeFamilyImpl[G] with LocationFamilyOps[G] { this: Location[G] =>
+  override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context)
 
-trait LocationImpl[G] extends LocationFamilyOps[G] { this: Location[G] =>
   def t: Type[G] = {
     this match {
       case FieldLocation(obj, field) => field.decl.t
diff --git a/src/col/vct/col/ast/family/parregion/ParBlockImpl.scala b/src/col/vct/col/ast/family/parregion/ParBlockImpl.scala
index 30654e4bef..200700222b 100644
--- a/src/col/vct/col/ast/family/parregion/ParBlockImpl.scala
+++ b/src/col/vct/col/ast/family/parregion/ParBlockImpl.scala
@@ -1,7 +1,7 @@
 package vct.col.ast.family.parregion
 
 import vct.col.ast.util.Declarator
-import vct.col.ast.{Declaration, Expr, Local, ParBlock, Starall, Variable}
+import vct.col.ast.{Declaration, Expr, Local, Node, ParBlock, Starall, Variable}
 import vct.col.check.CheckContext
 import vct.col.origin.{Blame, ReceiverNotInjective}
 import vct.col.print._
@@ -21,8 +21,14 @@ trait ParBlockImpl[G] extends ParRegionImpl[G] with Declarator[G] with ParBlockO
     })
   }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context.copy(roScopes = context.scopes.size, roScopeReason = Some(this)).withScope(declarations)
+  override def enterCheckContextRoScopes(context: CheckContext[G]): Int =
+    context.scopes.size
+
+  override def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] =
+    Some(this)
+
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
+    context.withScope(declarations)
 
   override def layout(implicit ctx: Ctx): Doc = {
     val header = Group(Text("par") <+> ctx.name(decl) <>
diff --git a/src/col/vct/col/ast/family/parregion/ParRegionImpl.scala b/src/col/vct/col/ast/family/parregion/ParRegionImpl.scala
index d4a0515b2d..dc296ebaf4 100644
--- a/src/col/vct/col/ast/family/parregion/ParRegionImpl.scala
+++ b/src/col/vct/col/ast/family/parregion/ParRegionImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.family.parregion
 
-import vct.col.ast.ParRegion
+import vct.col.ast.{Node, ParRegion}
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.origin.{Blame, ParPreconditionFailed}
@@ -9,6 +9,9 @@ import vct.col.ast.ops.ParRegionFamilyOps
 trait ParRegionImpl[G] extends NodeFamilyImpl[G] with ParRegionFamilyOps[G] { this: ParRegion[G] =>
   def blame: Blame[ParPreconditionFailed]
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context.copy(roScopes = context.scopes.size, roScopeReason = Some(this))
+  override def enterCheckContextRoScopes(context: CheckContext[G]): Int =
+    context.scopes.size
+
+  override def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] =
+    Some(this)
 }
diff --git a/src/col/vct/col/ast/node/NodeImpl.scala b/src/col/vct/col/ast/node/NodeImpl.scala
index 7e3d2ec150..d1a6ee6ded 100644
--- a/src/col/vct/col/ast/node/NodeImpl.scala
+++ b/src/col/vct/col/ast/node/NodeImpl.scala
@@ -46,8 +46,30 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
   def serialize(decls: Map[Declaration[G], Long]): scalapb.GeneratedMessage
   def serializeFamily(decls: Map[Declaration[G], Long]): scalapb.GeneratedMessage
 
-  def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context
+  final def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+    CheckContext(
+      enterCheckContextScopes(context),
+      enterCheckContextUndeclared(context),
+      enterCheckContextRoScopes(context),
+      enterCheckContextRoScopeReason(context),
+      enterCheckContextCurrentApplicable(context),
+      enterCheckContextInPostCondition(context),
+      enterCheckContextCurrentSeqProg(context),
+      enterCheckContextCurrentReceiverEndpoint(context),
+      enterCheckContextCurrentParticipatingEndpoints(context),
+      enterCheckContextDeclarationStack(context),
+    )
+
+  def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] = context.scopes
+  def enterCheckContextUndeclared(context: CheckContext[G]): Seq[Seq[Declaration[G]]] = context.undeclared
+  def enterCheckContextRoScopes(context: CheckContext[G]): Int = context.roScopes
+  def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] = context.roScopeReason
+  def enterCheckContextCurrentApplicable(context: CheckContext[G]): Option[Applicable[G]] = context.currentApplicable
+  def enterCheckContextInPostCondition(context: CheckContext[G]): Boolean = context.inPostCondition
+  def enterCheckContextCurrentSeqProg(context: CheckContext[G]): Option[SeqProg[G]] = context.currentSeqProg
+  def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] = context.currentReceiverEndpoint
+  def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = context.currentParticipatingEndpoints
+  def enterCheckContextDeclarationStack(context: CheckContext[G]): Seq[Declaration[G]] = context.declarationStack
 
   /* Check children first, so that the check of nodes higher in the tree may depend on the type and correctness of
     subnodes */
diff --git a/src/col/vct/col/ast/statement/composite/ScopeImpl.scala b/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
index 4a57bd1ff3..bb0301ba51 100644
--- a/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
+++ b/src/col/vct/col/ast/statement/composite/ScopeImpl.scala
@@ -8,7 +8,8 @@ import vct.col.ast.ops.ScopeOps
 
 trait ScopeImpl[G] extends ScopeOps[G] {
   this: Scope[G] =>
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
     context.withScope(locals, toScan = Seq(body))
 
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock
diff --git a/src/col/vct/col/ast/statement/exceptional/EvalImpl.scala b/src/col/vct/col/ast/statement/exceptional/EvalImpl.scala
index 1752f62a57..a65fa1522e 100644
--- a/src/col/vct/col/ast/statement/exceptional/EvalImpl.scala
+++ b/src/col/vct/col/ast/statement/exceptional/EvalImpl.scala
@@ -1,7 +1,7 @@
 package vct.col.ast.statement.exceptional
 
 import vct.col.ast.statement.StatementImpl
-import vct.col.ast.{EndpointUse, Eval, MethodInvocation, Statement, ThisSeqProg}
+import vct.col.ast.{Endpoint, EndpointUse, Eval, MethodInvocation, Statement, ThisSeqProg}
 import vct.col.check.{CheckContext, CheckError, SeqProgInvocation}
 import vct.col.print.{Ctx, Doc}
 import vct.col.ast.ops.EvalOps
@@ -9,10 +9,11 @@ import vct.col.ast.ops.EvalOps
 trait EvalImpl[G] extends StatementImpl[G] with EvalOps[G] { this: Eval[G] =>
   override def layout(implicit ctx: Ctx): Doc = expr.show <> ";"
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = this match {
+  override def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] = this match {
     case Eval(MethodInvocation(EndpointUse(endpoint), _, _, _, _, _, _)) if context.currentSeqProg.isDefined =>
-      context.withReceiverEndpoint(endpoint.decl)
-    case _ => context
+      Some(endpoint.decl)
+    case _ =>
+      context.currentReceiverEndpoint
   }
 
   override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context) ++ (context.currentSeqProg match {
diff --git a/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala
index 3f21bdae58..4ea2a6f88d 100644
--- a/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala
+++ b/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.statement.veymont
 
-import vct.col.ast.SeqAssign
+import vct.col.ast.{Endpoint, SeqAssign}
 import vct.col.ast.statement.StatementImpl
 import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
 import vct.col.print.{Ctx, Doc, Group, Text}
@@ -8,8 +8,8 @@ import vct.col.ast.ops.SeqAssignOps
 
 trait SeqAssignImpl[G] extends StatementImpl[G] with SeqAssignOps[G] { this: SeqAssign[G] =>
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-      context.withReceiverEndpoint(receiver.decl)
+  override def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] =
+    Some(receiver.decl)
 
   override def layout(implicit ctx: Ctx): Doc =
     Group(Text(ctx.name(receiver)) <> "." <> ctx.name(field) <+> ":=" <+> value.show)
diff --git a/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala
index 1f3457fc33..cf970a7a41 100644
--- a/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala
+++ b/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala
@@ -12,7 +12,7 @@ trait SeqBranchImpl[G] extends StatementImpl[G] with SeqBranchOps[G] { this: Seq
   def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
   def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = {
     // Assume SeqProg sets participatingEndpoints
     assert(context.currentParticipatingEndpoints.isDefined)
 
diff --git a/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala
index 8c511857a6..3bf3ccf822 100644
--- a/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala
+++ b/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala
@@ -12,7 +12,7 @@ trait SeqLoopImpl[G] extends StatementImpl[G] with SeqLoopOps[G] { this: SeqLoop
   def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
   def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = {
     // Assume SeqProg sets participatingEndpoints
     assert(context.currentParticipatingEndpoints.isDefined)
 
diff --git a/src/col/vct/col/ast/util/Declarator.scala b/src/col/vct/col/ast/util/Declarator.scala
index 0e480e15db..c75a210f6d 100644
--- a/src/col/vct/col/ast/util/Declarator.scala
+++ b/src/col/vct/col/ast/util/Declarator.scala
@@ -7,7 +7,7 @@ import vct.col.check.{CheckContext, DoesNotDefine, OutOfScopeError}
 trait Declarator[G] extends NodeImpl[G] { this: Node[G] =>
   def declarations: Seq[Declaration[G]]
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
     context.withScope(declarations)
 
   def checkDefines(defn: Declaration[G], use: Node[G]): Seq[DoesNotDefine] =
diff --git a/src/col/vct/col/check/Check.scala b/src/col/vct/col/check/Check.scala
index 20f6e6c7ca..9528bf4166 100644
--- a/src/col/vct/col/check/Check.scala
+++ b/src/col/vct/col/check/Check.scala
@@ -36,6 +36,8 @@ sealed trait CheckError {
         Seq(context(t) -> s"This type variable refers to a name that is not actually a type.")
       case OutOfScopeError(use, ref) =>
         Seq(context(use) -> "This usage is out of scope,", context(ref.decl) -> "since it is declared here.")
+      case ThisOutsideScopeError(use) =>
+        Seq(context(use) -> "`this` may not occur outside the declaration it refers to.")
       case OutOfWriteScopeError(reason, use, ref) =>
         Seq(
           context(use) -> "This may not be rewritten to, since ...",
@@ -61,6 +63,8 @@ sealed trait CheckError {
         Seq(context(clause) -> "This catch clause is redundant, because it is subsumed by the caught types of earlier catch clauses in this block.")
       case ResultOutsidePostcondition(res) =>
         Seq(context(res) -> "\\result may only occur in the postcondition.")
+      case FinalPermission(loc) =>
+        Seq(context(loc) -> "Specifying permission over final fields is not allowed, since they are treated as constants.")
       case SeqProgStatement(s) =>
         Seq(context(s) -> "This statement is not allowed in `seq_prog`.")
       case SeqProgInstanceMethodArgs(m) =>
@@ -95,6 +99,9 @@ case class GenericTypeError(t: Type[_], expectedType: TType[_]) extends CheckErr
 case class OutOfScopeError[G](use: Node[G], ref: Ref[G, _ <: Declaration[G]]) extends CheckError {
   val subcode = "outOfScope"
 }
+case class ThisOutsideScopeError[G](use: ThisDeclaration[G]) extends CheckError {
+  override def subcode: String = "thisOutOfScope"
+}
 case class OutOfWriteScopeError[G](reason: Node[G], use: Node[G], ref: Ref[G, _ <: Declaration[G]]) extends CheckError {
   val subcode = "outOfWriteScope"
 }
@@ -119,6 +126,9 @@ case class RedundantCatchClause(clause: CatchClause[_]) extends CheckError {
 case class ResultOutsidePostcondition(res: Expr[_]) extends CheckError {
   val subcode = "resultOutsidePostcondition"
 }
+case class FinalPermission(loc: FieldLocation[_]) extends CheckError {
+  override def subcode: String = "finalPerm"
+}
 case class SeqProgInstanceMethodNonVoid(m: InstanceMethod[_]) extends CheckError {
   val subcode = "seqProgInstanceMethodNonVoid"
 }
@@ -161,17 +171,21 @@ case class CheckContext[G]
   currentSeqProg: Option[SeqProg[G]] = None,
   currentReceiverEndpoint: Option[Endpoint[G]] = None,
   currentParticipatingEndpoints: Option[Set[Endpoint[G]]] = None,
+  declarationStack: Seq[Declaration[G]] = Nil,
 ) {
-  def withScope(decls: Seq[Declaration[G]]): CheckContext[G] =
-    copy(scopes = scopes :+ CheckContext.ScopeFrame(decls, Nil))
+  def withScope(decls: Seq[Declaration[G]]): Seq[CheckContext.ScopeFrame[G]] =
+    scopes :+ CheckContext.ScopeFrame(decls, Nil)
 
   /**
    * In effect toScan is just scanned for LocalDecl's, and these are added to decls. We want to delay this, because
    * the scanning operation is expensive, and for most of the transformation run the declaration is declared directly
    * anyway.
    */
-  def withScope(decls: Seq[Declaration[G]], toScan: Seq[Node[G]]): CheckContext[G] =
-    copy(scopes = scopes :+ CheckContext.ScopeFrame(decls, toScan))
+  def withScope(decls: Seq[Declaration[G]], toScan: Seq[Node[G]]): Seq[CheckContext.ScopeFrame[G]] =
+    scopes :+ CheckContext.ScopeFrame(decls, toScan)
+
+  def withDeclaration(decl: Declaration[G]): CheckContext[G] =
+    copy(declarationStack = decl +: declarationStack)
 
   def withApplicable(applicable: Applicable[G]): CheckContext[G] =
     copy(currentApplicable = Some(applicable))
@@ -188,15 +202,15 @@ case class CheckContext[G]
   def withReceiverEndpoint(endpoint: Endpoint[G]): CheckContext[G] =
     copy(currentReceiverEndpoint = Some(endpoint))
 
-  def withCurrentParticipatingEndpoints(endpoints: Seq[Endpoint[G]]): CheckContext[G] =
+  def withCurrentParticipatingEndpoints(endpoints: Seq[Endpoint[G]]): Option[Set[Endpoint[G]]] =
     // ListSet to preserve insertion order
-    copy(currentParticipatingEndpoints = Some(ListSet.from(endpoints)))
+    Some(ListSet.from(endpoints))
 
-  def appendCurrentParticipatingEndpoints(newEndpoints: Seq[Endpoint[G]]): CheckContext[G] =
+  def appendCurrentParticipatingEndpoints(newEndpoints: Seq[Endpoint[G]]): Option[Set[Endpoint[G]]] =
     // ListSet to preserve insertion order
     currentParticipatingEndpoints match {
       case None => withCurrentParticipatingEndpoints(newEndpoints)
-      case Some(endpoints) => copy(currentParticipatingEndpoints = Some(endpoints.union(ListSet.from(newEndpoints))))
+      case Some(endpoints) => Some(endpoints.union(ListSet.from(newEndpoints)))
     }
 
   def inScope[Decl <: Declaration[G]](ref: Ref[G, Decl]): Boolean =
diff --git a/src/hre/hre/stages/Stages.scala b/src/hre/hre/stages/Stages.scala
index 3385edcab7..36d26aac13 100644
--- a/src/hre/hre/stages/Stages.scala
+++ b/src/hre/hre/stages/Stages.scala
@@ -16,26 +16,27 @@ trait Stage[-Input, +Output] {
     UnitStages(this).thenRun(stages)
 }
 
-trait ContextStage[-Input, Ctx, +Output] extends Stage[(Input, Ctx), (Output, Ctx)] {
-  def run(in: (Input, Ctx)): (Output, Ctx) =
-    (runWithoutContext(in._1), in._2)
-
-  def runWithoutContext(input: Input): Output
-}
-
 trait Stages[-Input, +Output] {
   def run(in: Input): Either[VerificationError, Output] =
     try {
+      val stages = collect.asInstanceOf[Seq[Stage[Any, Nothing]]]
       Progress.stages(flatNames) { progressNext =>
-        Right(runUnsafely(in, progressNext))
+        var cur: Any = in
+
+        for(stage <- stages) {
+          cur = stage.run(cur)
+          progressNext()
+        }
+
+        Right(cur.asInstanceOf[Output])
       }
     } catch {
       case err: VerificationError => Left(err)
     }
 
-  def runUnsafely(in: Input, progressNext: () => Unit): Output
+  def collect: Seq[Stage[Nothing, Any]]
 
-  def flatNames: Seq[(String, Int)]
+  def flatNames: Seq[(String, Int)] = collect.map(s => s.friendlyName -> s.progressWeight)
 
   def thenRun[NewOutput](stage: Stage[Output, NewOutput]): Stages[Input, NewOutput] =
     thenRun(UnitStages(stage))
@@ -45,15 +46,9 @@ trait Stages[-Input, +Output] {
 }
 
 case class UnitStages[-Input, +Output](stage: Stage[Input, Output]) extends Stages[Input, Output] {
-  override def runUnsafely(in: Input, progressNext: () => Unit): Output = stage.run(in)
-  override def flatNames: Seq[(String, Int)] = Seq((stage.friendlyName, stage.progressWeight))
+  override def collect: Seq[Stage[Nothing, Any]] = Seq(stage)
 }
 
 case class StagesPair[-Input, Mid, +Output](left: Stages[Input, Mid], right: Stages[Mid, Output]) extends Stages[Input, Output] {
-  override def runUnsafely(in: Input, progressNext: () => Unit): Output = {
-    val mid = left.runUnsafely(in, progressNext)
-    progressNext()
-    right.runUnsafely(mid, progressNext)
-  }
-  override def flatNames: Seq[(String, Int)] = left.flatNames ++ right.flatNames
+  override def collect: Seq[Stage[Nothing, Any]] = left.collect ++ right.collect
 }
\ No newline at end of file