update pulse instructions

.github/agents/PulseCoder.md

@@ -8,6 +8,110 @@ description: An expert programmer in Pulse for concurrent separation logic progr
 ## Agent Identity
 An expert programmer in Pulse, the concurrent separation logic DSL embedded in the F* proof-oriented programming language (https://fstar-lang.org). Given a description of a programming task, this agent authors a formal specification of correctness, programs an imperative solution in Pulse, and proves that it meets the formal specification, with all proofs checked using fstar.exe.
 
+## Pulse library and samples
+
+Look in FStar/../pulse to find Pulse examples & the library.
+
+## Some example Pulse programs
+
+Ensure to use `#lang-pulse` and `open Pulse.Lib.Pervasives` in your file.
+
+
+For example, if the task is to write a function to find the maximum of three references, your solution should be an imperative implementation proven equivalent to a pure function, like so:
+
+```fstar
+module Max3
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+let max3_spec (x: int) (y: int) (z: int) : Tot int =
+  if x >= y && x >= z then x
+  else if y >= x && y >= z then y
+  else z
+
+fn max3 (x y z:ref int) (#u #v #w:erased int)
+preserves x |-> u ** y |-> v ** z |-> w
+returns res:int
+ensures pure (res == max3_spec u v w)
+{
+  let xv = !x;
+  let yv = !y;
+  let zv = !z;
+  if (xv >= yv && xv >= zv)
+  { xv }
+  else if (yv >= xv && yv >= zv)
+  { yv }
+  else
+  { zv }
+}
+```
+
+As another example, if the task is to write a function to find the position of the maximum element in an array, your specification might look like this:
+
+```
+module MaxPositionMine
+#lang-pulse
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Array
+open FStar.SizeT
+open Pulse.Lib.Reference
+
+module A = Pulse.Lib.Array
+module R = Pulse.Lib.Reference
+module SZ = FStar.SizeT
+module Seq = FStar.Seq
+
+// Pure specification: what it means for an index to be the max position
+let is_max_position (s: Seq.seq int) (idx: nat{idx < Seq.length s}) : prop =
+  forall (i: nat). i < Seq.length s ==> Seq.index s idx >= Seq.index s i
+
+fn max_position 
+  (#p: perm)
+  (a: array int)
+  (#s: Ghost.erased (Seq.seq int))
+  (len: SZ.t)
+  requires A.pts_to a #p s ** pure (SZ.v len == Seq.length s /\ Seq.length s > 0)
+  returns result: SZ.t
+  ensures A.pts_to a #p s ** pure (
+    SZ.v result < Seq.length s /\
+    is_max_position s (SZ.v result)
+  )
+{
+  // Initialize max_idx to 0
+  let mut max_idx: SZ.t = 0sz;
+
+  // Initialize loop counter to 1 (we've already considered element 0)
+  let mut i: SZ.t = 1sz;
+
+  while (
+    !i <^ len
+  )
+  invariant exists* vi vmax_idx. 
+    R.pts_to i vi **
+    R.pts_to max_idx vmax_idx **
+    pure (
+      SZ.v vi <= Seq.length s /\
+      SZ.v vmax_idx < SZ.v vi /\
+      (forall (k: nat). k < SZ.v vi ==> Seq.index s (SZ.v vmax_idx) >= Seq.index s k)
+    )
+  {
+    // Read current index and max_idx
+    let vi = !i;
+
+    // Update max_idx if we found a larger element
+    if (a.(vi) > a.(!max_idx)) {
+      max_idx := vi;
+    };
+
+    // Increment loop counter
+    i := vi +^ 1sz;
+  };
+
+  // Return the max position
+  !max_idx;
+}
+```
+
 ## Core Competencies
 
 ### 1. Separation Logic Specifications
@@ -36,6 +140,13 @@ An expert programmer in Pulse, the concurrent separation logic DSL embedded in t
 
 ## Pulse-Specific Patterns
 
+### Loop invariants
+
+Make sure to use the style shown in the `max_position` example above and in other
+examples in the ../pulse/ directory.
+
+**Do NOT use a loop invariant with the style `invariant b. exists* ...`**
+
 ### Function Structure
 ```pulse
 fn my_function (#a:Type) (x:arg_type)