diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index a36593c66..9d7dafd76 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -303,13 +303,20 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       return mkStmtExprMd (.AsType target (mkHighTypeMd (.UserDefined typeName) src)) src
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
-      let calleeName := match callee.val with
-        | .Var (.Local name) => name
-        | _ => ""
       let argsList ← match argsSeq with
         | .seq _ .comma args => args.toList.mapM translateStmtExpr
         | _ => pure []
-      return mkStmtExprMd (.StaticCall calleeName argsList) src
+      -- `obj#method(args)` parses as `call(fieldAccess(obj, method), args)`.
+      -- Treat such calls as instance-method calls; everything else stays a
+      -- static call by callee text (empty when the callee is a higher-order
+      -- expression — preserved to match prior behavior).
+      match callee.val with
+      | .Var (.Field target fieldName) =>
+        return mkStmtExprMd (.InstanceCall target fieldName argsList) src
+      | .Var (.Local name) =>
+        return mkStmtExprMd (.StaticCall name argsList) src
+      | _ =>
+        return mkStmtExprMd (.StaticCall (mkId "") argsList) src
     | q`Laurel.return, #[arg0] =>
       let value ← match arg0 with
         | .option _ (some valArg) => some <$> translateStmtExpr valArg
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 34304667b..80f80911b 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -3,9 +3,12 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+-- Grammar updated: renamed Optional* categories (op names updated)
+-- Grammar updated: `call` callee at prec 89 to accept fieldAccess (prec 90) chains
+-- Grammar updated: `fieldAccess` is leftassoc so `a#b#c` parses as `(a#b)#c`
 -- Grammar updated: added bitvector literal support (bvLiteral)
-module
 
+module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index b5c72c7ab..acbab7cfb 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -34,13 +34,14 @@ op initializer(value: StmtExpr): Initializer => " := " value:0;
 op varDecl (name: Ident, varType: Option TypeAnnotation, assignment: Option Initializer): StmtExpr
   => @[prec(0)] "var " name varType assignment;
 
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr =>
+  @[prec(95)] callee:89 "(" args ")";
 
 // Instantiation
 op new(name: Ident): StmtExpr => "new " name;
 
-// Field access
-op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
+// Field access. `leftassoc` so chained access (`a#b#c`) parses as `(a#b)#c`.
+op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90), leftassoc] obj "#" field;
 
 // Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier
 op identifier (name: Ident): StmtExpr => name;
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index ea785e1f2..38894e196 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -286,7 +286,8 @@ where
           | return [⟨ .Hole, source ⟩]
 
         let valTy := (model.get fieldName).getType
-        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩
+        let selectTarget' ← recurseOne selectTarget
+        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget', mkMd (.StaticCall qualifiedName [])], source ⟩
         -- Unwrap Box: apply the appropriate destructor
         recordBoxConstructor model valTy.val
         return [mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr]]
@@ -544,16 +545,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
     return proc
 
 def heapParameterization (model: SemanticModel) (program : Program) : Program :=
-  let program := { program with
-    types := program.types
-    staticProcedures := program.staticProcedures }
-  let instanceProcs := program.types.foldl (fun acc td =>
-    match td with
-    | .Composite ct => acc ++ ct.instanceProcedures
-    | _ => acc) ([] : List Procedure)
-  let allProcs := program.staticProcedures ++ instanceProcs
-  let heapReaders := computeReadsHeap allProcs
-  let heapWriters := computeWritesHeap allProcs
+  -- Instance procedures are already lifted to `staticProcedures` by an earlier
+  -- pass, so they're covered by the calls below.
+  let heapReaders := computeReadsHeap program.staticProcedures
+  let heapWriters := computeWritesHeap program.staticProcedures
   let initState : TransformState := { heapReaders, heapWriters }
   let (procs', state1) := (program.staticProcedures.mapM (heapTransformProcedure model)).run initState
   -- Collect all qualified field names and generate a Field datatype
@@ -563,18 +558,14 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program :=
     | _ => acc) ([] : List Identifier)
   let fieldDatatype : TypeDefinition :=
     .Datatype { name := "Field", typeArgs := [], constructors := fieldNames.map fun n => { name := n, args := [] } }
-  -- Remove fields from composite types since they are now stored in the heap
-  -- Also transform instance procedures, accumulating used Box constructors
-  let (types', state2) := program.types.foldl (fun (accTypes, accState) td =>
+  -- Remove fields from composite types since they are now stored in the heap.
+  let types' := program.types.map fun td =>
     match td with
-    | .Composite ct =>
-      let (instProcs', s') := (ct.instanceProcedures.mapM (heapTransformProcedure model)).run accState
-      (accTypes ++ [.Composite { ct with fields := [], instanceProcedures := instProcs' }], s')
-    | other => (accTypes ++ [other], accState))
-    ([], state1)
+    | .Composite ct => .Composite { ct with fields := [] }
+    | other => other
   -- Generate Box datatype from all constructors used during transformation
   let boxDatatype : TypeDefinition :=
-    .Datatype { name := "Box", typeArgs := [], constructors := state2.usedBoxConstructors }
+    .Datatype { name := "Box", typeArgs := [], constructors := state1.usedBoxConstructors }
   { program with
     staticProcedures := heapConstants.staticProcedures ++ procs',
     types := fieldDatatype :: boxDatatype :: heapConstants.types ++ types' }
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 8b01e99c3..e0f2c7137 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -18,7 +18,7 @@ import Strata.Languages.Laurel.EliminateDeterministicHoles
 import Strata.Languages.Laurel.CoreDefinitionsForLaurel
 import Strata.Languages.Laurel.LiftImperativeExpressions
 import Strata.Languages.Laurel.ConstrainedTypeElim
-
+import Strata.Languages.Laurel.LiftInstanceProcedures
 import Strata.Languages.Laurel.TypeAliasElim
 public import Strata.Languages.Laurel.LaurelPass
 public import Strata.Languages.Core
@@ -96,6 +96,7 @@ def laurelPipeline : Array LaurelPass := #[
   typeAliasElimPass,
   filterNonCompositeModifiesPass,
   eliminateValueInReturnsPass,
+  liftInstanceProceduresPass,
   heapParameterizationPass,
   typeHierarchyTransformPass,
   modifiesClausesTransformPass,
@@ -183,6 +184,15 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     | none => Strata.Pipeline.PipelineContext.create (outputMode := .quiet)
   runPipelineM options.keepAllFilesPrefix do
     let (program, model, passDiags, stats) ← runLaurelPasses pctx program
+    -- Sanity check: `LiftInstanceProcedures` should have cleared every
+    -- composite's `instanceProcedures` list.
+    let mut passDiags := passDiags
+    for td in program.types do
+      if let .Composite ct := td then
+        for proc in ct.instanceProcedures do
+          passDiags := passDiags ++ [diagnosticFromSource proc.name.source
+            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' was not lifted before Core translation (pipeline-ordering bug)"
+            DiagnosticType.StrataBug]
     let unorderedCore := transparencyPass program
     emit "transparencyPass" "core.st" unorderedCore
 
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index c909121e8..29e97f770 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -722,7 +722,6 @@ abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel)
 
 /--
 Translate a `CoreWithLaurelTypes` program to a `Core.Program`.
-The `program` parameter is the lowered Laurel program, used for type definitions.
 -/
 def translateLaurelToCore (options: LaurelTranslateOptions) (ordered : CoreWithLaurelTypes): TranslateM Core.Program := do
 
diff --git a/Strata/Languages/Laurel/LiftInstanceProcedures.lean b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
new file mode 100644
index 000000000..ec66abb17
--- /dev/null
+++ b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
@@ -0,0 +1,132 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.Resolution
+public import Strata.Languages.Laurel.LaurelPass
+
+/-!
+# Lift Instance Procedures
+
+A Laurel-to-Laurel pass that lifts every instance procedure (a procedure
+defined inside a `composite` block) to a top-level static procedure with a
+mangled name `<CompositeName>$<methodName>`, then rewrites every call site
+that resolved to such an instance procedure to use the lifted name.
+
+After this pass:
+- `CompositeType.instanceProcedures` is empty for every composite.
+- `program.staticProcedures` contains the lifted procedures.
+- Every `InstanceCall` (from `obj#method(args)` surface syntax) points
+  at the lifted name. For `InstanceCall`, the receiver is prepended to
+  the argument list to match the lifted procedure's `self : <CompositeName>`
+  parameter.
+-/
+
+namespace Strata.Laurel
+
+/-! ## Lifting + call-site rewriting
+
+Lift instance procedures to static scope (e.g., procedure `proc`
+of composite type `T` will be lifted to `T$proc`).
+Then, rewrite caller-side of `obj#proc` to call the lifted procedure
+
+-/
+
+/-- Top-level name produced for a lifted instance procedure. -/
+def liftedProcName (typeName methodName : Identifier) : Identifier :=
+  mkId s!"{typeName.text}${methodName.text}"
+
+/-- Rewrite a single node so that any callee resolving to an instance procedure
+    is replaced by its lifted name. -/
+private def rewriteCallNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
+  match expr.val with
+  | .StaticCall callee args =>
+    match model.get? callee with
+    | some (.instanceProcedure typeName _) =>
+      let lifted := liftedProcName typeName callee
+      { expr with val := .StaticCall lifted args }
+    | _ => expr
+  | .InstanceCall target callee args =>
+    -- `obj#method(args)` surface syntax parses to InstanceCall. Flatten it to
+    -- a static call against the lifted name, prepending the receiver as the
+    -- first argument to match the lifted procedure's `self` parameter.
+    match model.get? callee with
+    | some (.instanceProcedure typeName _) =>
+      let lifted := liftedProcName typeName callee
+      { expr with val := .StaticCall lifted (target :: args) }
+    | _ => expr
+  | _ => expr
+
+/-- Apply call-site rewriting to every expression in a procedure. -/
+private def rewriteCallsInProc (model : SemanticModel) (proc : Procedure) : Procedure :=
+  let f := mapStmtExpr (rewriteCallNode model)
+  let resolveBody : Body → Body := fun body => match body with
+    | .Transparent b => .Transparent (f b)
+    | .Opaque ps impl modif =>
+      .Opaque (ps.map (·.mapCondition f)) (impl.map f) (modif.map f)
+    | .Abstract ps => .Abstract (ps.map (·.mapCondition f))
+    | .External => .External
+  { proc with
+    body := resolveBody proc.body
+    preconditions := proc.preconditions.map (·.mapCondition f)
+    decreases := proc.decreases.map f
+    invokeOn := proc.invokeOn.map f }
+
+/-- Apply call-site rewriting to a constrained type's constraint and witness. -/
+private def rewriteCallsInType (model : SemanticModel) (td : TypeDefinition) : TypeDefinition :=
+  match td with
+  | .Constrained ct =>
+    let f := mapStmtExpr (rewriteCallNode model)
+    .Constrained { ct with constraint := f ct.constraint, witness := f ct.witness }
+  | _ => td
+
+public section
+
+/--
+Lift every `proc ∈ ct.instanceProcedures` to a top-level static procedure
+named via `liftedProcName`, rewrite call sites that resolved to an instance
+procedure, and clear `instanceProcedures` on every composite.
+-/
+def liftInstanceProcedures (model : SemanticModel) (program : Program) : Program :=
+  -- Step 1: collect lifted clones
+  let liftedProcs : List Procedure :=
+    program.types.foldl (init := []) fun acc td =>
+      match td with
+      | .Composite ct =>
+        acc ++ ct.instanceProcedures.map fun proc =>
+          { proc with name := liftedProcName ct.name proc.name }
+      | _ => acc
+
+  if liftedProcs.isEmpty then program else
+
+  -- Step 2: rewrite call sites in procedure bodies and constrained-type
+  let rewrittenStaticProcs := program.staticProcedures.map (rewriteCallsInProc model)
+  let rewrittenLiftedProcs := liftedProcs.map (rewriteCallsInProc model)
+  let rewrittenTypes := program.types.map (rewriteCallsInType model)
+
+  -- Step 3: clear instanceProcedures on every composite.
+  let cleanedTypes := rewrittenTypes.map fun td =>
+    match td with
+    | .Composite ct => .Composite { ct with instanceProcedures := [] }
+    | _ => td
+
+  -- Step 4: append lifted procs.
+  { program with
+    staticProcedures := rewrittenStaticProcs ++ rewrittenLiftedProcs
+    types := cleanedTypes }
+
+end -- public section
+
+/-- Pipeline pass: lift instance procedures to top-level static procedures
+    and rewrite call sites to use the lifted names. -/
+public def liftInstanceProceduresPass : LaurelPass where
+  name := "LiftInstanceProcedures"
+  documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization."
+  needsResolves := true
+  run := fun p m => (liftInstanceProcedures m p, [], {})
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index e407c8a49..35dc0786a 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -158,10 +158,15 @@ def resolveRef (name : Identifier) (source : Option FileRange := none)
     modify fun s => { s with errors := s.errors.push diag }
     return { name with uniqueId := none }
 
+/-- Scope key for a name nested inside a container (composite, datatype),
+    used to disambiguate members in the flat global scope. -/
+private def containerScopedName (containerName memberName : Identifier) : Identifier :=
+  mkId s!"{containerName.text}${memberName.text}"
+
 /-- Extract the UserDefined type name from a resolved target expression by looking up its scope entry. -/
 private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := do
   let s ← get
-  match target.val with
+  match _h : target.val with
   | .Var (.Local ref) =>
     match s.scope.get? ref.text with
     | some (_, node) =>
@@ -169,7 +174,26 @@ private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := d
       | .UserDefined typRef => pure (some typRef.text)
       | _ => pure none
     | none => pure none
+  | .Var (.Field inner fieldName) => do
+    match (← targetTypeName inner) with
+    | none => pure none
+    | some innerTy =>
+      match s.typeScopes.get? innerTy with
+      | none => pure none
+      | some typeScope =>
+        match typeScope.get? fieldName.text with
+        | some (_, node) =>
+          match node.getType.val with
+          | .UserDefined typRef => pure (some typRef.text)
+          | _ => pure none
+        | none => pure none
   | _ => pure none
+  termination_by sizeOf target
+  decreasing_by
+    have := AstNode.sizeOf_val_lt target
+    have : sizeOf target.val = sizeOf (StmtExpr.Var (Variable.Field inner fieldName)) := congrArg sizeOf _h
+    simp at this
+    omega
 
 /-- Try to resolve a field name via a type scope lookup. Returns `some id` on success. -/
 private def resolveFieldInTypeScope (typeName : String) (fieldName : Identifier) : ResolveM (Option Identifier) := do
@@ -456,8 +480,16 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
     pure (.IsType target' ty')
   | .InstanceCall target callee args =>
     let target' ← resolveStmtExpr target
-    let callee' ← resolveRef callee source
+    -- Look up under the container-scoped key matching `preRegisterTopLevel`.
+    -- Fall back to the bare name when the target's type can't be determined.
+    let lookupKey ← match (← targetTypeName target') with
+      | some tyName => pure (containerScopedName (mkId tyName) callee)
+      | none => pure callee
+    let resolved ← resolveRef lookupKey source
       (expected := #[.instanceProcedure, .staticProcedure])
+    -- Preserve the user-facing callee text for diagnostics;
+    -- only stamp the resolved `uniqueId` from the lifted lookup.
+    let callee' := { callee with uniqueId := resolved.uniqueId }
     let args' ← args.mapM resolveStmtExpr
     pure (.InstanceCall target' callee' args')
   | .Quantifier mode param trigger body =>
@@ -557,7 +589,9 @@ def resolveField (ownerName : Identifier) (field : Field) : ResolveM Field := do
 
 /-- Resolve an instance procedure on a composite type. -/
 def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : ResolveM Procedure := do
-  let procName' ← resolveRef proc.name
+  let scopedKey := containerScopedName typeName proc.name
+  let resolved ← resolveRef scopedKey
+  let procName' := { proc.name with uniqueId := resolved.uniqueId }
   withScope do
     let savedInstType := (← get).instanceTypeName
     modify fun s => { s with instanceTypeName := some typeName.text }
@@ -955,7 +989,9 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
         let qualifiedName := ct.name.text ++ "." ++ field.name.text
         let _ ← defineNameCheckDup field.name (.field ct.name field) (some qualifiedName)
       for proc in ct.instanceProcedures do
+        let scopedKey := (containerScopedName ct.name proc.name).text
         let _ ← defineNameCheckDup proc.name (.instanceProcedure ct.name proc)
+                                   (some scopedKey)
     | .Constrained ct =>
       let _ ← defineNameCheckDup ct.name (.constrainedType ct)
     | .Datatype dt =>
@@ -989,15 +1025,6 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
 public def resolve (program : Program) (existingModel: Option SemanticModel := none) : ResolutionResult :=
   -- Phase 1: pre-register all top-level names, then assign IDs and resolve references
   let phase1 : ResolveM Program := do
-
-    for td in program.types do
-      if let .Composite ct := td then
-        for proc in ct.instanceProcedures do
-          let diag := diagnosticFromSource proc.name.source
-            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported"
-            DiagnosticType.NotYetImplemented
-          modify fun s => { s with errors := s.errors.push diag }
-
     preRegisterTopLevel program
     let types' ← program.types.mapM resolveTypeDefinition
     let constants' ← program.constants.mapM resolveConstant
diff --git a/StrataTest/Languages/Laurel/DuplicateNameTests.lean b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
index d00a480ad..1ca1640a0 100644
--- a/StrataTest/Languages/Laurel/DuplicateNameTests.lean
+++ b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
@@ -61,10 +61,8 @@ procedure foo(x: int, x: bool) opaque { };
 program Laurel;
 composite Foo {
   procedure bar() opaque { };
-//          ^^^ not-yet-implemented: Instance procedure 'bar' on composite type 'Foo' is not yet supported
   procedure bar() opaque { };
-//          ^^^ not-yet-implemented: Instance procedure 'bar' on composite type 'Foo' is not yet supported
-//          ^^^ error: Duplicate definition 'bar' is already defined in this scope
+//          ^^^ error: Duplicate definition 'Foo$bar' is already defined in this scope
 }
 #end
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
index a605006ec..08638d1c7 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
@@ -4,27 +4,237 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+/-
+Tests for the `obj#method(args)` syntax for calling instance procedures.
+
+Each instance procedure declared inside a `composite` block is lifted to a
+top-level static procedure named `<CompositeName>$<methodName>` by the
+`LiftInstanceProcedures` pass. Resolution registers the instance proc in
+global scope under the lifted key, so two composites can share a method
+name without colliding. `c#m(args)` parses as `InstanceCall c m args` and
+the lifting pass rewrites it to `StaticCall Counter$m (c :: args)`.
+-/
+
 import StrataTest.Util.TestLaurel
 
 open StrataTest.Util
 open Strata
 
+/-! ## 1. Basic instance method call: `c#reset()` -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Counter {
+  var count: int
+  procedure reset(self: Counter)
+    opaque
+    ensures self#count == 0
+    modifies self
+  {
+    self#count := 0
+  };
+}
+
+procedure useCounter()
+  opaque
+{
+  var c: Counter := new Counter;
+  c#reset();
+  assert c#count == 0
+};
+#end
+
+/-! ## 2. Two composites with the same method name resolve independently.
+    Without per-composite scoping, `tick` would collide in the global scope
+    during pre-registration. -/
+
 #eval testLaurel <|
 #strata
 program Laurel;
 composite Counter {
   var count: int
-  procedure self_increment(self: Counter)
-//          ^^^^^^^^^^^^^^ not-yet-implemented: Instance procedure 'self_increment' on composite type 'Counter' is not yet supported
+  procedure tick(self: Counter)
+    opaque
+    ensures self#count == 1
+    modifies self
+  {
+    self#count := 1
+  };
+}
+
+composite Clock {
+  var time: int
+  procedure tick(self: Clock)
+    opaque
+    ensures self#time == 1
+    modifies self
+  {
+    self#time := 1
+  };
+}
+
+procedure runCounter()
+  opaque
+{
+  var c: Counter := new Counter;
+  c#tick();
+  assert c#count == 1
+};
+
+procedure runClock()
+  opaque
+{
+  var k: Clock := new Clock;
+  k#tick();
+  assert k#time == 1
+};
+#end
+
+/-! ## 3. Method with multiple parameters: `c#setTo(v)` -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Cell {
+  var value: int
+  procedure setTo(self: Cell, v: int)
+    opaque
+    ensures self#value == v
+    modifies self
+  {
+    self#value := v
+  };
+}
+
+procedure useCell(x: int)
+  opaque
+{
+  var b: Cell := new Cell;
+  b#setTo(x);
+  assert b#value == x
+};
+#end
+
+/-! ## 4. Boolean-typed field updated through an instance method, and read
+    back via field access in the caller's `assert`. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Widget {
+  var enabled: bool
+  procedure activate(self: Widget)
     opaque
+    ensures self#enabled
+    modifies self
   {
-    self#count := self#count + 1
+    self#enabled := true
   };
+}
+
+procedure useWidget()
+  opaque
+{
+  var w: Widget := new Widget;
+  w#activate();
+  assert w#enabled == true
+};
+#end
+
+/-! ## 5. Calling an instance method from a top-level procedure that takes
+    the receiver as a parameter. The caller's own modifies clause covers
+    only `a`; the unused `b` parameter is included to confirm method
+    dispatch picks the right receiver. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Counter {
+  var count: int
   procedure reset(self: Counter)
-//          ^^^^^ not-yet-implemented: Instance procedure 'reset' on composite type 'Counter' is not yet supported
     opaque
+    ensures self#count == 0
+    modifies self
   {
     self#count := 0
   };
 }
+
+procedure resetTwoCounters(a: Counter, b: Counter)
+  opaque
+  ensures a#count == 0
+  modifies a
+{
+  a#reset()
+};
+#end
+
+/-! ## 6. Instance method whose extra parameter is unused in the body:
+    confirms an extra (unused) method parameter doesn't break call
+    dispatch or framing. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Account {
+  var balance: int
+  procedure deposit(self: Account, amount: int)
+    opaque
+    ensures self#balance == 1
+    modifies self
+  {
+    self#balance := 1
+  };
+}
+
+procedure useAccount()
+  opaque
+{
+  var a: Account := new Account;
+  a#deposit(100);
+  assert a#balance == 1
+};
+#end
+
+/-! ## 7. Instance method called through a field-selected receiver:
+    `obj#field#method()`. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Inner {
+  var x: int
+  procedure isOne(self: Inner) returns (r: bool)
+    opaque
+    ensures r == (self#x == 1)
+  ;
+}
+
+composite Outer {
+  var inner: Inner
+}
+
+procedure useOuter()
+  opaque
+{
+  var o: Outer := new Outer;
+  var b: bool := o#inner#isOne()
+};
+#end
+
+/-! ## 8. Chained field read: `obj#field#x`. -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Inner { var x: int }
+composite Outer { var inner: Inner }
+
+procedure useOuter()
+  opaque
+{
+  var o: Outer := new Outer;
+  var v: int := o#inner#x
+};
 #end