feat(laurel): paren-free field ++/--, and chained-field-access test coverage (#1382)

Two field-access improvements on the single `fieldAccess` grammar op,
plus test coverage that closes out #1371.

Note: the chained-field-access *capability* (`a#b#c` parsing,
resolution, and heap elimination) already landed via #1328. This PR adds
the one missing ergonomic piece, hardens the chained-access machinery
with the tests it was missing, and a small refactor.

**Grammar — paren-free field `++`/`--`.** `fieldAccess` precedence is
raised 90 → 95. At 90 it tied with the postfix `++`/`--` ops (also 90),
forcing `(c#n)++`; at 95 it binds tighter, so `c#n++` parses paren-free
as `(c#n)++`. (`leftassoc`, already present from #1328, is unchanged.)
Note the new precedence is shared with `call` (also 95, via its
`callee:89`) — the two must stay equal or `a#b(x)` parsing shifts;
documented at the op.

**Resolution — refactor only.** The duplicated type-scope field lookup
in `targetTypeName` and `incrDecrTargetType` is factored into a shared
`fieldTypeInScope` helper. No behavior change. (This helper is also a
dependency of the stacked compound-assignment PR.)

**Tests — fill the chained-access coverage gap.** #1328 shipped chained
access with only a read-side smoke test (no assertions). This adds:
- `T9_ChainedFieldAccess`: chained **write** (`o#inner#count := …`),
read-after-inner-assign, must-alias, depth-3 (`a#mid#inner#count`),
chained reads on both sides of `==`, and paren-free chained
`o#inner#count++` (the one test that exercises this PR's grammar
change), plus three **negative** tests (unconstrained read, two-object
may-alias, write isolation) that pin the encoding as non-vacuous and
frame-sound.
- `T23b_IncrDecrField`: paren-free single-level field `++`/`--`.

Full `lake build` and `lake test` pass.

Author: fabiomadge

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -8,7 +8,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: merged `doWhile` op (post-test loop; parsed to a post-test `While`, lowered by EliminateDoWhile) with the `old` op from #1203.
+-- 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

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