fix(rt): normalize singleton-array volatile pubkey writes

docs/proof-issues/ISSUE-001-write-volatile-pubkey-array.md

@@ -0,0 +1,78 @@
+## Summary
+
+`test_process_close_account_multisig` reaches a stuck leaf while closing an account through
+`delete_account -> AccountInfo::assign -> std::ptr::write_volatile`.
+
+The observed stuck family writes a `[u8; 32]` payload through a cast from `*const Pubkey` to
+`*mut [u8; 32]`. This is the shape used by `solana_account_info::AccountInfo::assign`.
+
+## Source Proof
+
+- proof target: `test_process_close_account_multisig`
+- source run: `proof-unknown-ae54c481`
+- source node: `132`
+- known out-of-scope case: issue #181 uninitialized multisig OOB is not this blocker
+
+## Minimal Reproducer
+
+- file: `kmir/src/tests/integration/data/prove-rs/write_volatile_pubkey_array.rs`
+- start symbol: `repro`
+- failing baseline: `FAILED`, `nodes=3`, `pending=0`, `failing=1`, `stuck=1`
+- current regression status: `PASSED`, `nodes=3`, `pending=0`, `failing=0`, `stuck=0`, `terminal=2`
+
+## Leaf Shape
+
+The failing leaf is both `failing` and `stuck` at node `132`.
+
+The head of the stuck state is:
+
+```text
+#traverseProjection(... projectionElemSingletonArray projectionElemField(fieldIdx(0), ...)
+ projectionElemConstantIndex(...))
+~> #derefTruncate(staticSize(32), .ProjectionElems)
+~> #writeProjection(Range(ListItem(Integer(0, 8, false)) ...))
+```
+
+This suggests the semantics gets as far as a projected writeback into a wrapped `[u8; 32]`
+representation, but cannot normalize or complete the final projection/write step.
+
+The standalone reproducer reached the same projection family before the fix:
+
+```text
+#traverseProjection(
+  ...,
+  Aggregate(variantIdx(0), ListItem(Range(...))),
+  projectionElemSingletonArray projectionElemField(fieldIdx(0), ty(64))
+  projectionElemConstantIndex(... offset: 0, minLength: 0, fromEnd: false),
+  .Contexts
+)
+~> #derefTruncate(staticSize(32), .ProjectionElems)
+~> #writeProjection(Range(...))
+```
+
+## Rust Behavior
+
+`solana_account_info::AccountInfo::assign` uses:
+
+```rust
+std::ptr::write_volatile(
+    self.owner as *const Pubkey as *mut [u8; 32],
+    new_owner.to_bytes(),
+)
+```
+
+`Pubkey` is represented as a tuple struct over `[u8; 32]`, so the write path naturally introduces
+field and singleton-array projections around the byte array payload.
+
+## Hypothesis
+
+The blocker is in `mir-semantics` projection normalization or projected writeback for
+`write_volatile(*mut [u8; 32], ...)`, not in the multisig spec itself.
+
+## Plan
+
+1. Add a minimal `prove-rs` reproducer that performs the same `AccountInfo::assign`-style cast and
+   `write_volatile`.
+2. Confirm it fails in the same stuck family.
+3. Repair the relevant projection/writeback semantics.
+4. Re-run the scoped reproducer and then the full `test_process_close_account_multisig` proof.

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -329,6 +329,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
                    | CtxIndex( List , Int ) // array index constant or has been read before
                    | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
                    | CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length)
+                   | "CtxSingletonArray" // special context dropping a synthetic singleton-array wrapper on writeback
                    | "CtxWrapStruct" // special context adding a singleton Aggregate(0, _) around a value
 
   syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us
@@ -364,6 +365,14 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
     requires size(INNER) ==Int END -Int START // ensures updateList is defined
      [preserves-definedness] // START,END indexes checked before, length check for update here
 
+  // removing an artificial singleton-array wrapper added by a SingletonArray projection
+  rule #buildUpdate(Range(ListItem(VALUE) .List), CtxSingletonArray CTXS)
+    => #buildUpdate(VALUE, CTXS)
+
+  // nested updates may already have reconstructed the original element shape
+  rule #buildUpdate(VALUE, CtxSingletonArray CTXS)
+    => #buildUpdate(VALUE, CTXS)
+
   // removing a struct wrapper added by a WrapStruct projection
   rule #buildUpdate(Aggregate(variantIdx(0), ListItem(VALUE) .List), CtxWrapStruct CTXS)
     => #buildUpdate(VALUE, CTXS)
@@ -390,6 +399,18 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
   // high-priority rules to cancel out projection pairs at the head
   rule consP(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) PS:ProjectionElems) => PS [priority(40)]
   rule consP(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray PS:ProjectionElems) => PS [priority(40)]
+  rule consP(
+         projectionElemSingletonArray,
+         projectionElemField(fieldIdx(0), TY) projectionElemConstantIndex(0, 0, false) PS:ProjectionElems
+       )
+    => projectionElemField(fieldIdx(0), TY) PS
+    [priority(40)]
+  rule consP(
+         projectionElemConstantIndex(0, 0, false),
+         projectionElemField(fieldIdx(0), TY) projectionElemSingletonArray PS:ProjectionElems
+       )
+    => projectionElemField(fieldIdx(0), TY) PS
+    [priority(40)]
   rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)]
   // this rule is not valid if the original pointee has more than one field
   // rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)]
@@ -452,6 +473,16 @@ This is done without consideration of the validity of the Downcast[^downcast].
 [^downcast]: See discussion in https://github.com/rust-lang/rust/issues/93688#issuecomment-1032929496.
 
 ```k
+  rule <k> #traverseProjection(
+             DEST,
+             Aggregate(IDX, ARGS),
+             projectionElemSingletonArray projectionElemField(fieldIdx(0), TY) projectionElemConstantIndex(0, 0, false) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, Aggregate(IDX, ARGS), projectionElemField(fieldIdx(0), TY) PROJS, CTXTS) ... </k>
+    requires size(ARGS) ==Int 1
+    [preserves-definedness, priority(110)]
+
   rule <k> #traverseProjection(
              DEST,
              Aggregate(IDX, ARGS),
@@ -519,6 +550,21 @@ The following rule resolves this situation by using the head element.
     [preserves-definedness, priority(100)]
 ```
 
+The dual to `projectionElemWrapStruct` is `projectionElemSingletonArray`, which is introduced by pointer casts from
+an element pointer to an array pointer. When cancellation with `ConstantIndex(0)` does not happen immediately,
+the traversal still needs to materialize a singleton `Range` so that later projections can proceed.
+
+```k
+  rule <k> #traverseProjection(
+             DEST,
+             VALUE,
+             projectionElemSingletonArray PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, Range(ListItem(VALUE)), PROJS, CtxSingletonArray CTXTS) ... </k>
+    [preserves-definedness, priority(100)]
+```
+
 #### Unions
 ```k
   // Case: Union is in same state as field projection
@@ -1234,6 +1280,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
   // rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS)
   rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS)
   rule #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS)
+  rule #projectionsFor(CtxSingletonArray      CTXS, PROJS) => #projectionsFor(CTXS,          projectionElemSingletonArray PROJS)
   rule #projectionsFor(  CtxWrapStruct       CTXS, PROJS) => #projectionsFor(CTXS,                 projectionElemWrapStruct PROJS)
 
   // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.

kmir/src/kmir/kdist/mir-semantics/rt/types.md

@@ -65,7 +65,18 @@ It also implements cancellation of inverse projections (such as casting from one
   // special cancellation rules with higher priority
   rule maybeConcatProj(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) REST:ProjectionElems) => REST [priority(40)]
   rule maybeConcatProj(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray REST:ProjectionElems) => REST [priority(40)]
-
+  rule maybeConcatProj(
+         projectionElemSingletonArray,
+         projectionElemField(fieldIdx(0), TY) projectionElemConstantIndex(0, 0, false) REST:ProjectionElems
+       )
+    => projectionElemField(fieldIdx(0), TY) REST
+    [priority(40)]
+  rule maybeConcatProj(
+         projectionElemConstantIndex(0, 0, false),
+         projectionElemField(fieldIdx(0), TY) projectionElemSingletonArray REST:ProjectionElems
+       )
+    => projectionElemField(fieldIdx(0), TY) REST
+    [priority(40)]
   rule maybeConcatProj(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) REST:ProjectionElems) => REST [priority(40)]
   // this rule would not be valid if the original pointee had more than one field. In the calling context, this won't occur, though.
   rule maybeConcatProj(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct REST:ProjectionElems) => REST [priority(40)]

kmir/src/tests/integration/data/prove-rs/write_volatile_pubkey_array.rs

@@ -0,0 +1,37 @@
+#![allow(invalid_reference_casting)]
+
+fn main() {
+    let _keep: fn(&AccountInfo<'_>, Pubkey) = repro;
+}
+
+#[inline(never)]
+#[no_mangle]
+pub fn repro(account: &AccountInfo<'_>, replacement: Pubkey) {
+    account.assign(replacement);
+    assert_eq!(*account.owner, replacement);
+}
+
+struct AccountInfo<'a> {
+    owner: &'a Pubkey,
+}
+
+impl<'a> AccountInfo<'a> {
+    #[inline(never)]
+    fn assign(&self, new_owner: Pubkey) {
+        unsafe {
+            std::ptr::write_volatile(
+                self.owner as *const Pubkey as *mut [u8; 32],
+                new_owner.to_bytes(),
+            );
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);
+
+impl Pubkey {
+    fn to_bytes(self) -> [u8; 32] {
+        self.0
+    }
+}

kmir/src/tests/integration/test_integration.py

@@ -41,6 +41,7 @@
     'iter-eq-copied-take-dereftruncate': ['repro'],
     'spl-multisig-iter-eq-copied-next-fail': ['repro'],
     'spl-multisig-signer-index': ['repro'],
+    'write_volatile_pubkey_array': ['repro'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',