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

@@ -9,7 +9,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 now @[prec(95), leftassoc] (paren-free `c#n++` and chained `a#b#c`).
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -39,8 +39,11 @@ op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" arg
 // Instantiation
 op new(name: Ident): StmtExpr => "new " name;
 
-// Field access
-op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
+// Field access.
+// prec(95) binds tighter than the postfix incr/decr ops (prec 90) so `c#n++`
+// parses paren-free as `(c#n)++`. leftassoc lets `a#b#c` left-recurse for
+// chained field access.
+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/HeapParameterization.lean

@@ -285,6 +285,13 @@ where
         let some qualifiedName := resolveQualifiedFieldName model fieldName
           | return [⟨ .Hole, source ⟩]
 
+        -- Recurse into the target so a nested field access (`a#b#c`) has its
+        -- inner `FieldSelect` eliminated. Without this, the un-eliminated
+        -- `FieldSelect` reaches a downstream guard and aborts with a
+        -- `strata-bug`. This is the single point that unblocks *both* chained
+        -- reads and chained writes: the write arm's `recurseOne target`
+        -- bottoms out here for any nested target.
+        let selectTarget ← recurseOne selectTarget
         let valTy := (model.get fieldName).getType
         let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩
         -- Unwrap Box: apply the appropriate destructor

Strata/Languages/Laurel/Resolution.lean

@@ -158,18 +158,41 @@ def resolveRef (name : Identifier) (source : Option FileRange := none)
     modify fun s => { s with errors := s.errors.push diag }
     return { name with uniqueId := none }
 
-/-- 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
+/-- Look up the declared type of `fieldName` within the scope of the composite
+    type named `typeName`. Returns `none` if the type or field is unknown. -/
+private def fieldTypeInScope (typeName : String) (fieldName : Identifier) : ResolveM (Option HighType) := do
   let s ← get
-  match target.val with
-  | .Var (.Local ref) =>
-    match s.scope.get? ref.text with
-    | some (_, node) =>
-      match node.getType.val with
-      | .UserDefined typRef => pure (some typRef.text)
-      | _ => pure none
+  match s.typeScopes.get? typeName with
+  | some typeScope =>
+    match typeScope.get? fieldName.text with
+    | some (_, node) => pure (some node.getType.val)
     | none => pure none
-  | _ => pure none
+  | none => pure none
+
+/-- Determine the user-defined type name of a target expression.
+    Handles a local variable (`.Var (.Local _)`, scope lookup) and a chained
+    field access (`.Var (.Field tgt f)`, recursing on `tgt` then looking the
+    field up in the inner type's scope). `fuel` keeps the function total;
+    chains longer than `fuel` simply stop (the conservative, no-false-positive
+    direction, as with `underlyingBaseType`). -/
+private def targetTypeNameAux (fuel : Nat) (target : StmtExprMd) : ResolveM (Option String) := do
+  match fuel with
+  | 0 => pure none
+  | fuel + 1 =>
+    let ty? ← match target.val with
+      | .Var (.Local ref) => pure ((← get).scope.get? ref.text |>.map (·.2.getType.val))
+      | .Var (.Field tgt fieldName) =>
+        -- Resolve the inner target's type, then look the field up in its scope.
+        match (← targetTypeNameAux fuel tgt) with
+        | some innerTypeName => fieldTypeInScope innerTypeName fieldName
+        | none => pure none
+      | _ => pure none
+    match ty? with
+    | some (.UserDefined typRef) => pure (some typRef.text)
+    | _ => pure none
+
+private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) :=
+  targetTypeNameAux 100 target
 
 /-- 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
@@ -269,13 +292,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