Emit struct field writes through array index

Handle arr[i].field = val by emitting:
  let __arr = arr;
  let __idx = idx;
  let __cur = __arr.(__idx);
  let __val = rhs;
  __arr.(__idx) <- { __cur with field = __val };

This uses Pulse-native let-statement bindings to:
- Avoid duplicating arr/idx expressions (side-effect safety).
- Read the current element into a pure variable before the
  record update, which Pulse's type checker requires.

Addresses review feedback:
- Extract emit_assign() helper so the Assign arm no longer
  bypasses the annotated() wrapper in emit_stmt.
- Use let-bindings for arr, idx, current element, and rhs
  to avoid duplicating expressions that may have side effects.
- Add test/struct_array_write.c exercising the pattern.

Verified: the generated Pulse code (with SizeT index) passes
F* verification with all conditions discharged successfully.

Scope limitation: Only handles one level of arr[i].field.
Deeper patterns like arr[i].field.subfield or ptr->arr[i].field
would need further work.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: angelica-moreira

src/pass/emit.rs

@@ -1101,6 +1101,74 @@ impl<'a> Emitter<'a> {
         })
     }
 
+    fn emit_assign(&mut self, env: &Env, x: &Expr, t: &Expr) -> Doc {
+        if let ExprT::Member(inner, field) = &x.val {
+            if let ExprT::Index(arr, idx) = &inner.val {
+                if let Ok(elem_ty) = env.infer_expr(inner) {
+                    let elem_ty = env.vtype_whnf(elem_ty);
+                    if let TypeT::TypeRef(TypeRefKind::Struct(struct_name)) = &elem_ty.val {
+                        let arr_doc = self.emit_rvalue(env, arr);
+                        let idx_doc = self.emit_rvalue(env, idx);
+                        let field_name = self.nm.emit(Name::StructDirectFieldName(
+                            struct_name.val.clone(),
+                            field.val.clone(),
+                        ));
+                        let rhs_doc = self.emit_rvalue(env, t);
+                        return Doc::text("let __arr = ")
+                            .append(arr_doc)
+                            .append(Doc::text(";"))
+                            .append(Doc::line())
+                            .append(Doc::text("let __idx = "))
+                            .append(idx_doc)
+                            .append(Doc::text(";"))
+                            .append(Doc::line())
+                            .append(Doc::text("let __cur = __arr.(__idx);"))
+                            .append(Doc::line())
+                            .append(Doc::text("let __val = "))
+                            .append(rhs_doc)
+                            .append(Doc::text(";"))
+                            .append(Doc::line())
+                            .append(Doc::text("__arr.(__idx)"))
+                            .append(Doc::line())
+                            .append("<-")
+                            .group()
+                            .append(Doc::line())
+                            .append(Doc::text("{ __cur with "))
+                            .append(field_name)
+                            .append(Doc::text(" = __val }"))
+                            .append(";")
+                            .group()
+                            .nest(2);
+                    }
+                }
+            }
+        }
+        if let ExprT::Index(arr, idx) = &x.val {
+            self.emit_rvalue(env, arr)
+                .append(Doc::text(".("))
+                .append(self.emit_rvalue(env, idx))
+                .append(Doc::text(")"))
+                .append(Doc::line())
+                .append("<-")
+                .group()
+                .append(Doc::line())
+                .append(self.emit_rvalue(env, t))
+                .append(";")
+                .group()
+                .nest(2)
+        } else {
+            self.emit_lvalue(env, x)
+                .append(Doc::line())
+                .append(":=")
+                .group()
+                .append(Doc::line())
+                .append(self.emit_rvalue(env, t))
+                .append(";")
+                .group()
+                .nest(2)
+        }
+    }
+
     fn emit_stmt(&mut self, env: &Env, stmt: &Stmt) -> Doc {
         annotated(stmt, {
             match &stmt.val {
@@ -1114,33 +1182,7 @@ impl<'a> Emitter<'a> {
                         .nest(2)
                         .group()
                 }
-                StmtT::Assign(x, t) => {
-                    if let ExprT::Index(arr, idx) = &x.val {
-                        // Array write: arr.(idx) <- val;
-                        self.emit_rvalue(env, arr)
-                            .append(Doc::text(".("))
-                            .append(self.emit_rvalue(env, idx))
-                            .append(Doc::text(")"))
-                            .append(Doc::line())
-                            .append("<-")
-                            .group()
-                            .append(Doc::line())
-                            .append(self.emit_rvalue(env, t))
-                            .append(";")
-                            .group()
-                            .nest(2)
-                    } else {
-                        self.emit_lvalue(env, x)
-                            .append(Doc::line())
-                            .append(":=")
-                            .group()
-                            .append(Doc::line())
-                            .append(self.emit_rvalue(env, t))
-                            .append(";")
-                            .group()
-                            .nest(2)
-                    }
-                }
+                StmtT::Assign(x, t) => self.emit_assign(env, x, t),
                 StmtT::If(c, b1, b2) => Doc::text("if ")
                     .append(parens(self.emit_rvalue(env, c)))
                     .nest(2)

test/struct_array_write.c

@@ -0,0 +1,29 @@
+#include "c2pulse.h"
+#include <stddef.h>
+
+struct point {
+  int x;
+  int y;
+};
+
+void set_x(_array struct point *pts, size_t i, int val)
+  _requires(i < pts._length)
+  _preserves_value(pts._length)
+{
+  pts[i].x = val;
+}
+
+void set_y(_array struct point *pts, size_t i, int val)
+  _requires(i < pts._length)
+  _preserves_value(pts._length)
+{
+  pts[i].y = val;
+}
+
+void set_both(_array struct point *pts, size_t i, int vx, int vy)
+  _requires(i < pts._length)
+  _preserves_value(pts._length)
+{
+  pts[i].x = vx;
+  pts[i].y = vy;
+}