feat(laurel): chained field access and paren-free field increment

Chained field access (`a#b#c`) and paren-free field increment (`c#n++`)
were both blocked by the `fieldAccess` grammar op. Combine the fixes:

* Grammar: `fieldAccess` becomes `@[prec(95), leftassoc]`. prec(95) binds
  tighter than the postfix incr/decr ops (prec 90) so `c#n++` parses as
  `(c#n)++` without parens; `leftassoc` lets `a#b#c` left-recurse.

* Resolution: `targetTypeName` is generalized to resolve a chained
  `.Var (.Field tgt f)` target by recursing on `tgt` and looking the field
  up in the inner type's scope. The recursion is kept total via fuel
  (cf. `underlyingBaseType`), not `partial`. The shared type-scope field
  lookup is factored into `fieldTypeInScope`, which `incrDecrTargetType`
  now reuses instead of duplicating.

* Heap: the field-read arm recurses into its target so a nested
  `FieldSelect` is eliminated. This single line unblocks *both* chained
  reads and chained writes: the write arm already calls `recurseOne` on its
  target, but for a nested target that recursion bottoms out in the read
  arm, so neither path worked before. Without the fix, an un-eliminated
  `FieldSelect` hits a downstream guard and aborts with a `strata-bug`
  (confirmed by ablation).

Tests:
* T9_ChainedFieldAccess: chained read/write, read-after-inner-assign,
  must-alias, depth-3 (`a#mid#inner#count`), chained read on both sides of
  a comparison, paren-free chained incr/decr, plus three negative tests
  (unconstrained read, two-object may-alias, write isolation) pinning the
  encoding as non-vacuous and frame-sound.
* T23b_IncrDecrField: paren-free field `++`/`--`; header comment updated
  (parens are no longer required).

Implements #1371.

Author: fabiomadge

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -12,7 +12,7 @@ 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.
--- Last grammar change: renamed strConcat token to `^`; added preIncr/preDecr/postIncr/postDecr; `return` value is now Option StmtExpr (supports a valueless return).
+-- Last grammar change: fieldAccess prec raised 90 -> 95 (paren-free `c#n++`); shares prec(95) with `call`.
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -40,8 +40,10 @@ op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr =>
 // Instantiation
 op new(name: Ident): StmtExpr => "new " name;
 
-// 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;
+// Field access. prec coupled to `call` (also 95, via its `callee:89`): keep them
+// equal or `a#b(x)` parsing shifts. prec 95 > postfix `++`/`--` (90) is what lets
+// `c#n++` parse paren-free as `(c#n)++`.
+op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(95), leftassoc] obj "#" field;
 
 // Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier
 op identifier (name: Ident): StmtExpr => name;

Strata/Languages/Laurel/Resolution.lean

@@ -236,7 +236,22 @@ def resolveRef (name : Identifier) (source : Option FileRange := none)
 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. -/
+/-- Declared type of `fieldName` in the scope of composite type `typeName`; `none` if
+    unknown. Shared by `targetTypeName` and `incrDecrTargetType`. (`resolveFieldInTypeScope`
+    below is the same walk returning the field's *id* instead of its type.) -/
+private def fieldTypeInScope (typeName : String) (fieldName : Identifier) : ResolveM (Option HighType) := do
+  let s ← get
+  match s.typeScopes.get? typeName with
+  | some typeScope =>
+    match typeScope.get? fieldName.text with
+    | some (_, node) => pure (some node.getType.val)
+    | none => pure none
+  | none => pure none
+
+/-- UserDefined type name of a resolved target: a local directly, or a chained field
+    access (`a#b#c`) by recursing on the inner target then `fieldTypeInScope`.
+    Self-recursive on `.Var (.Field inner _)`; the `decreasing_by` proof below holds
+    only because `inner` is a strict subterm of `target`, so recurse only on subterms. -/
 private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := do
   let s ← get
   match _h : target.val with
@@ -251,15 +266,9 @@ private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := d
     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
+      match (← fieldTypeInScope innerTy fieldName) with
+      | some (.UserDefined typRef) => pure (some typRef.text)
+      | _ => pure none
   | _ => pure none
   termination_by sizeOf target
   decreasing_by
@@ -516,13 +525,7 @@ private def incrDecrTargetType (target : VariableMd) : ResolveM (Option HighType
     | none => pure none
   | .Field tgt fieldName =>
     match (← targetTypeName tgt) with
-    | some typeName =>
-      match s.typeScopes.get? typeName with
-      | some typeScope =>
-        match typeScope.get? fieldName.text with
-        | some (_, node) => pure (some node.getType.val)
-        | none => pure none
-      | none => pure none
+    | some typeName => fieldTypeInScope typeName fieldName
     | none => pure none
   | .Declare param => pure (some param.type.val)
 

StrataTest/Languages/Laurel/Examples/Fundamentals/T23b_IncrDecrField.lean

@@ -31,9 +31,10 @@ local (`$tmp_i` or `$heap`), so its snapshot mechanism — which is keyed on
 `liftAssignExpr` (which falls through `| _ => pure ()`) is defensive but
 never reached in this pipeline order.
 
-The parentheses around `(c#n)` are needed in the surface syntax because
-`#field` and `++` are both trailing operators with the same precedence
-(90); `c#n++` parses ambiguously without them.
+`c#n++` now parses paren-free: `fieldAccess` is at `prec(95)`, above the
+postfix incr/decr ops (`prec(90)`), so `#` binds tighter than `++` and
+`c#n++` reads as `(c#n)++`. The parenthesised spelling `(c#n)++` remains
+valid; `parenFreeFieldIncrDecr` below covers the paren-free form.
 -/
 
 #eval testLaurel <|
@@ -123,4 +124,21 @@ procedure postDecrFieldInExpression()
   assert c#n == 4;
   assert y == 5
 };
+
+procedure parenFreeFieldIncrDecr()
+  opaque
+{
+  // Paren-free field incr/decr: `c#n++` parses as `(c#n)++` because `fieldAccess`
+  // (prec 95) binds tighter than postfix `++`/`--` (prec 90).
+  var c: IncrDecrCounter := new IncrDecrCounter;
+  c#n := 10;
+  c#n++;
+  assert c#n == 11;
+  c#n--;
+  assert c#n == 10;
+  // Postfix in expression position yields the OLD value (10); c#n becomes 11.
+  var y: int := c#n++;
+  assert c#n == 11;
+  assert y == 10
+};
 #end

StrataTest/Languages/Laurel/Examples/Objects/T9_ChainedFieldAccess.lean

@@ -0,0 +1,182 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+/-!
+Chained field access on nested composites (`o#inner#count`), both read and
+write. Single-level field access (`o#inner`, `i#count`) already worked; this
+exercises the chaining enabled by three changes:
+
+  * Parse — `fieldAccess` is now `leftassoc`, so `a#b#c` left-recurses.
+  * Resolution — `targetTypeName` resolves a `.Var (.Field ..)` target by
+    recursing on the inner target and looking the field up in that type's scope.
+  * Heap — the field-read arm recurses into its target, so a nested
+    `FieldSelect` is eliminated rather than leaking raw into `readField`.
+-/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Inner {
+  var count: int
+}
+
+composite Outer {
+  var inner: Inner
+}
+
+// Three nested composite levels, for the depth-3 chain `a#mid#inner#count`.
+composite Innermost {
+  var count: int
+}
+
+composite Middle {
+  var inner: Innermost
+}
+
+composite Outermost {
+  var mid: Middle
+}
+
+procedure chainedReadWrite()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+
+  o#inner#count := 7;
+  assert o#inner#count == 7;
+
+  // Write through the chain again and read it back.
+  o#inner#count := o#inner#count + 1;
+  assert o#inner#count == 8;
+
+  // The chained read agrees with the single-level read of the same object.
+  assert i#count == 8
+};
+
+procedure chainedReadAfterInnerAssign()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  i#count := 3;
+  o#inner := i;
+  // Reading through the chain sees the value written on `i` directly.
+  assert o#inner#count == 3
+};
+
+procedure chainedAliasing()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+  o#inner#count := 1;
+
+  // `i` and `o#inner` alias the same Inner, so a write through one is seen
+  // through the other.
+  i#count := 42;
+  assert o#inner#count == 42
+};
+
+procedure depth3ReadWrite()
+  opaque
+{
+  var a: Outermost := new Outermost;
+  var b: Middle := new Middle;
+  var c: Innermost := new Innermost;
+  a#mid := b;
+  b#inner := c;
+
+  a#mid#inner#count := 9;
+  assert a#mid#inner#count == 9;
+  // The depth-3 chain agrees with the single-level read of the same object.
+  assert c#count == 9
+};
+
+procedure chainedReadOnBothSides()
+  opaque
+{
+  var o: Outer := new Outer;
+  var p: Outer := new Outer;
+  var i: Inner := new Inner;
+  var j: Inner := new Inner;
+  o#inner := i;
+  p#inner := j;
+  i#count := 4;
+  j#count := 4;
+  // Chained read on both operands of a comparison.
+  assert o#inner#count == p#inner#count
+};
+
+// Paren-free chained incr/decr: `o#inner#count++` parses as `(o#inner#count)++`
+// because `fieldAccess` (prec 95) binds tighter than postfix `++`/`--` (prec 90),
+// and `leftassoc` lets the chain `o#inner#count` left-recurse.
+procedure chainedParenFreeIncrDecr()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+  o#inner#count := 10;
+  o#inner#count++;
+  assert o#inner#count == 11;
+  o#inner#count--;
+  assert o#inner#count == 10;
+  // Postfix in expression position yields the OLD value (10); the cell becomes 11.
+  var y: int := o#inner#count++;
+  assert o#inner#count == 11;
+  assert y == 10
+};
+
+// Negative: an unconstrained chained field has no known value, so asserting a
+// concrete value must NOT be provable. Pins the chained read as non-vacuous.
+procedure chainedReadUnconstrainedFails()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  o#inner := i;
+  assert o#inner#count == 7
+//^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+
+// Negative (frame soundness): two distinct outers whose inner fields MAY alias.
+// A write through `a#inner` may be observed through `b#inner`, so the post-write
+// value of `b#inner#count` is not provably its pre-write value.
+procedure chainedMayAliasFails()
+  opaque
+{
+  var a: Outer := new Outer;
+  var b: Outer := new Outer;
+  var i: Inner := new Inner;
+  a#inner := i;
+  b#inner := i;
+  a#inner#count := 5;
+  assert b#inner#count == 0
+//^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+
+// Negative (write isolation): a write through one chain must not be observable on
+// a genuinely disjoint, freshly-allocated object.
+procedure chainedWriteIsolationFails()
+  opaque
+{
+  var o: Outer := new Outer;
+  var i: Inner := new Inner;
+  var d: Inner := new Inner;
+  o#inner := i;
+  o#inner#count := 7;
+  assert d#count == 7
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end