feat(sema): require mutable buffer locals for native fills

HANDOFF.md

@@ -5,8 +5,8 @@ about the present state, the next decision, and operational facts. The former
 per-PR journal is preserved in
 [`docs/archive/HANDOFF-2026-07-25.md`](docs/archive/HANDOFF-2026-07-25.md).
 
-_Last updated: 2026-08-01. `main` includes the shipped wave through #683. L2b-a2-am-f
-return completeness is complete; am-w task-wait dominance is next.
+_Last updated: 2026-08-01. `main` includes the shipped wave through #685. L2b-a2-am-w
+task-wait dominance is complete; am-v native output-buffer mutability is next.
 #667 adds the canonical recursive Drop plan and sound `Option<string>` fields;
 #668 admits one direct recursively Move payload per tagged arm; #669 admits multiple Move payloads;
 #670 completes nested tagged payload representation and the exact pkg.db L1b acceptance shape.
@@ -100,6 +100,7 @@ facts must live in this repository.
 #673  named/direct/imported parameter-root inference
 #674  product return-provenance refinement
 #675  eager MIR continuation closure
+#685  path-complete task-wait dominance
 ```
 
 #639 fixes Unit-call values across direct, indirect, pipeline, and per-unit
@@ -301,6 +302,30 @@ Required verification was slow but progressing: the final locked all-target Clip
 11m56s, and several test binaries had their known long startup delay. Those timings do not
 justify weakening the gate.
 
+### PR #685 delivery retrospective
+
+PR #685 was squash-merged as `257c704`. Its earliest-commit-to-merge proxy was 5h17m;
+the public PR was open for 4h18m. The implementation changed 4 files by +1,042/-18,
+including the complete compiler-only task-wait proof checker and its owner tests. The
+vertical remained intentionally atomic because splitting proof state, control joins, or
+TaskGet diagnostics could authorize an uninitialized task result or reject an outer proof.
+
+The avoidable delay was review execution and checkpoint churn, not the final compiler fix.
+The first host review spent its bound reading the large repository context and repeatedly
+hit macOS `xcodebuild` cache errors. A later host pass found a real P1: join tokens were
+keyed by incoming generation/epoch, so loop headers could allocate a new token on every
+state change and miss the required fixed point. The fix made join generation/epoch tokens
+stable by syntax site, then replaced an invalid owner fixture that tried to move a Task
+directly out of a conditional expression with a legal branch/loop reassignment twin.
+
+Durable rules: a review that has no verdict is never a clean result; inspect process state,
+log growth, and the last completed action, then stop at the hard bound and rerun against a
+small explicit complete patch. For control-flow token interning, keys that define a join
+identity are syntax-site-only; incoming state may key Spawn/Wait/Err events but must not
+create fresh identities for the same loop or branch join. Finally, every owner fixture must
+be legal under the language's own Move/arena rules before it can test compiler-only proof
+transport.
+
 #660's final verification records 48/48 `align_driver` `par_map` tests,
 including 65,537-element worker-range tests for both materializing chunks and
 direct chunk reduction, a chunk filter, a cross-worker i8 wrapping fold, and

crates/align_driver/tests/capability_linking.rs

@@ -83,7 +83,7 @@ fn http_client_requests_the_full_tls_set() {
 fn ct_equal_and_random_touch_no_library() {
     // `crypto.ct_equal` is a constant-time byte compare and `crypto.random` is OS getrandom — neither
     // links libcrypto. This guards against over-linking the whole `std.crypto` surface.
-    let src = "import std.crypto\nfn main() -> Result<(), Error> {\n  b := buffer(16)\n  crypto.random(b)\n  print(b.len() as i64)\n  return Ok(())\n}\n";
+    let src = "import std.crypto\nfn main() -> Result<(), Error> {\n  mut b := buffer(16)\n  crypto.random(b)\n  print(b.len() as i64)\n  return Ok(())\n}\n";
     assert_eq!(gated_link_libs("cap-rand", src), Vec::<String>::new());
 }
 

crates/align_driver/tests/m11_crypto.rs

@@ -130,7 +130,7 @@ fn random_fills_and_two_fills_differ() {
 import std.crypto
 import std.encoding
 pub fn main() -> Result<(), Error> {
-  b := buffer(32)
+  mut b := buffer(32)
   crypto.random(b)
   print(b.len())
   h1 := encoding.hex_encode(b.bytes())
@@ -156,7 +156,7 @@ fn random_large_fill_not_all_zero() {
 import std.crypto
 import std.encoding
 pub fn main() -> Result<(), Error> {
-  b := buffer(4096)
+  mut b := buffer(4096)
   crypto.random(b)
   print(b.len())
   print(encoding.hex_encode(b.bytes()))
@@ -180,7 +180,7 @@ fn random_impure_rejected_by_par_map() {
     let src = "\
 import std.crypto
 fn f(x: i64) -> i64 {
-  b := buffer(8)
+  mut b := buffer(8)
   crypto.random(b)
   return x + b.len()
 }
@@ -210,7 +210,7 @@ pub fn main() -> Result<(), Error> {
     assert!(check_errs("m11cr-noimport", src), "crypto.* without `import std.crypto` must error");
     let diags = check_diagnostics(
         "m11cr-diag",
-        "pub fn main() -> Result<(), Error> {\n  b := buffer(8)\n  crypto.random(b)\n  return Ok(())\n}\n",
+        "pub fn main() -> Result<(), Error> {\n  mut b := buffer(8)\n  crypto.random(b)\n  return Ok(())\n}\n",
     );
     assert!(diags.contains("import std.crypto"), "diagnostic should name the capability: {diags}");
 }
@@ -344,13 +344,13 @@ fn sha256_large_input_deterministic() {
     let prog = "\
 import std.crypto
 pub fn main() -> Result<(), Error> {
-  b := buffer(1048576)
+  mut b := buffer(1048576)
   crypto.random(b)
   print(b.len())                          // the input is 1 MiB
   d1 := crypto.sha256(b.bytes())
   d2 := crypto.sha256(b.bytes())
   print(crypto.constant_time_equal(d1[0..d1.len()], d2[0..d2.len()]))  // same input → same digest
-  c := buffer(1048576)
+  mut c := buffer(1048576)
   crypto.random(c)
   e := crypto.sha256(c.bytes())
   print(crypto.constant_time_equal(d1[0..d1.len()], e[0..e.len()]))    // different input → differ
@@ -697,9 +697,9 @@ fn aead_round_trips_both_ciphers() {
     let prog = "\
 import std.crypto
 pub fn main() -> Result<(), Error> {
-  k := buffer(32)
+  mut k := buffer(32)
   crypto.random(k)
-  n := buffer(12)
+  mut n := buffer(12)
   crypto.random(n)
   // Empty plaintext → 16-byte tag-only output; opens back to empty.
   s0 := crypto.aes_gcm_seal(k.bytes(), n.bytes(), \"\", \"aad\")?
@@ -711,7 +711,7 @@ pub fn main() -> Result<(), Error> {
   o1 := crypto.chacha20_poly1305_open(k.bytes(), n.bytes(), s1.bytes(), \"\")?
   print(crypto.constant_time_equal(o1.bytes(), \"hello world\"))
   // Large ~1 MiB plaintext round-trips (aes).
-  big := buffer(1048576)
+  mut big := buffer(1048576)
   crypto.random(big)
   s2 := crypto.aes_gcm_seal(k.bytes(), n.bytes(), big.bytes(), \"meta\")?
   print(s2.len())
@@ -745,12 +745,12 @@ fn aead_open_failures_are_invalid_and_yield_nothing() {
             "\
 import std.crypto
 pub fn main() -> Result<(), Error> {{
-  k := buffer(32)
+  mut k := buffer(32)
   crypto.random(k)
-  n := buffer(12)
+  mut n := buffer(12)
   crypto.random(n)
   sealed := crypto.aes_gcm_seal(k.bytes(), n.bytes(), \"top secret\", \"ctx\")?
-  wrong := buffer(32)
+  mut wrong := buffer(32)
   crypto.random(wrong)
   pt := {open_expr}?
   print(pt.len())
@@ -792,9 +792,9 @@ fn aead_cross_cipher_confusion_is_invalid() {
     let prog = "\
 import std.crypto
 pub fn main() -> Result<(), Error> {
-  k := buffer(32)
+  mut k := buffer(32)
   crypto.random(k)
-  n := buffer(12)
+  mut n := buffer(12)
   crypto.random(n)
   sealed := crypto.aes_gcm_seal(k.bytes(), n.bytes(), \"secret\", \"aad\")?
   pt := crypto.chacha20_poly1305_open(k.bytes(), n.bytes(), sealed.bytes(), \"aad\")?
@@ -820,9 +820,9 @@ fn aead_wrong_key_or_nonce_length_is_invalid() {
             "\
 import std.crypto
 pub fn main() -> Result<(), Error> {{
-  k := buffer(64)
+  mut k := buffer(64)
   crypto.random(k)
-  input := buffer(64)
+  mut input := buffer(64)
   crypto.random(input)
   r := crypto.{op}(k.bytes()[0..{key_slice}], k.bytes()[0..{nonce_slice}], input.bytes(), \"aad\")?
   print(r.len())
@@ -861,9 +861,9 @@ fn aead_impure_rejected_by_par_map() {
     let seal_src = "\
 import std.crypto
 fn f(x: i64) -> i64 {
-  k := buffer(32)
+  mut k := buffer(32)
   crypto.random(k)
-  n := buffer(12)
+  mut n := buffer(12)
   crypto.random(n)
   r := crypto.aes_gcm_seal(k.bytes(), n.bytes(), \"pt\", \"\")
   return x + match r { Ok(b) => b.len(), Err(_) => 0 }
@@ -881,9 +881,9 @@ pub fn main() -> i32 {
     let open_src = "\
 import std.crypto
 fn f(x: i64) -> i64 {
-  k := buffer(32)
+  mut k := buffer(32)
   crypto.random(k)
-  n := buffer(12)
+  mut n := buffer(12)
   crypto.random(n)
   r := crypto.chacha20_poly1305_open(k.bytes(), n.bytes(), \"0123456789abcdef\", \"\")
   return x + match r { Ok(b) => b.len(), Err(_) => 0 }

crates/align_driver/tests/m11_net.rs

@@ -174,7 +174,7 @@ pub fn main(args: array<str>) -> Result<(), Error> {
   w := conn.writer()
   w.write(\"ping\\n\")?
   r := conn.reader()
-  b := buffer(64)
+  mut b := buffer(64)
   n := r.read(b)?
   print(n)
   io.stdout.write(b.bytes())?
@@ -362,13 +362,13 @@ pub fn main(args: array<str>) -> Result<(), Error> {
   conn1 := l.accept()?
   r1 := conn1.reader()
   w1 := conn1.writer()
-  b1 := buffer(64)
+  mut b1 := buffer(64)
   n1 := r1.read(b1)?
   w1.write(b1.bytes())?
   conn2 := l.accept()?
   r2 := conn2.reader()
   w2 := conn2.writer()
-  b2 := buffer(64)
+  mut b2 := buffer(64)
   n2 := r2.read(b2)?
   w2.write(b2.bytes())?
   return Ok(())
@@ -531,7 +531,7 @@ fn make(p: str) -> Result<reader, Error> {
 }
 pub fn main(args: array<str>) -> Result<(), Error> {
   r := make(args[1])?
-  buf := buffer(4)
+  mut buf := buffer(4)
   n := r.read(buf)?
   print(n)
   return Ok(())
@@ -546,14 +546,12 @@ pub fn main(args: array<str>) -> Result<(), Error> {
     );
 }
 
-/// Adversarial-review F1: the conservative counterpart to the test above. `open_it`'s own reader is
-/// an unrelated fixed-path `fs.open` — it borrows nothing from `tag` — but `region_of(Call)` has no
-/// per-fn "does this borrow arg i" fact, so it folds in *every* argument's region regardless. Passing
-/// a `Frame`-region argument (a `string` local auto-borrowed to `str`, MMv2 slice 7b) taints the call
-/// result, so returning it out of `steal` (past the frame) is conservatively rejected — sound (never
-/// miscompiles), just imprecise. (Documented on `tracks_region`'s `Reader | Writer` arm.)
+/// Adversarial-review F1: a direct constructor's named return summary is `None`, so an unrelated
+/// frame-region argument does not taint the returned owned reader. This is the precise counterpart
+/// to the static-argument constructor test above: only a callee that explicitly returns a view of an
+/// argument contributes that argument's region to the call result.
 #[test]
-fn reader_through_call_with_frame_arg_conservatively_rejected() {
+fn reader_through_call_with_frame_arg_direct_constructor_is_precise() {
     let src = "\
 import std.fs
 fn open_it(tag: str) -> Result<reader, Error> {
@@ -571,8 +569,8 @@ pub fn main() -> Result<(), Error> {
 }
 ";
     assert!(
-        check_errs("m11net-reader-call-frame-arg", src),
-        "a reader returned through a user call with a Frame-region argument must be conservatively rejected"
+        !check_errs("m11net-reader-call-frame-arg", src),
+        "an unrelated frame-region argument must not taint a direct owned-reader constructor"
     );
 }
 
@@ -613,7 +611,7 @@ pub fn main(args: array<str>) -> Result<(), Error> {
   c.flag_i64(\"peer\", 0)
   p := c.parse(args)?
   u := udp.bind(\"127.0.0.1\", p.get_i64(\"port\"))?
-  b := buffer(64)
+  mut b := buffer(64)
   n := u.recv_from(b)?
   u.send_to(b.bytes(), \"127.0.0.1\", p.get_i64(\"peer\"))?
   return Ok(())

crates/align_driver/tests/m12_file_io.rs

@@ -54,7 +54,7 @@ pub fn main(args: array<str>) -> Result<(), Error> {
   f.pwrite(\"Hello, \", 0)?
   f.pwrite(\"World!\", 7)?
   f.pwrite(\"Z\", 20)?
-  buf := buffer(6)
+  mut buf := buffer(6)
   n := f.pread(buf, 7)?
   io.stdout.write(buf.bytes())?
   return Ok(())
@@ -257,6 +257,6 @@ fn file_constructors_require_std_fs_import() {
     // With the import, a bound file's methods type-check (regression: the gates don't over-reach).
     assert!(!check_errs(
         "m12-file-bound-ok",
-        "import std.fs\nimport std.io\npub fn main(args: array<str>) -> Result<(), Error> {\n  f := fs.create_rw(args[1])?\n  f.pwrite(\"hi\", 0)?\n  buf := buffer(2)\n  n := f.pread(buf, 0)?\n  print(f.len()?)\n  return Ok(())\n}\n",
+        "import std.fs\nimport std.io\npub fn main(args: array<str>) -> Result<(), Error> {\n  f := fs.create_rw(args[1])?\n  f.pwrite(\"hi\", 0)?\n  mut buf := buffer(2)\n  n := f.pread(buf, 0)?\n  print(f.len()?)\n  return Ok(())\n}\n",
     ), "a bound file's pwrite/pread/len must stay allowed");
 }

crates/align_driver/tests/m12_read_line.rs

@@ -50,7 +50,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(8)
+  mut buf := buffer(8)
   w := io.stdout
   mut acc: array_builder<string> := array_builder()
   loop {
@@ -92,7 +92,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(64)
+  mut buf := buffer(64)
   w := io.stdout
   n := r.read_line(buf)?
   line := buf.bytes().as_str()?
@@ -133,7 +133,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(64)
+  mut buf := buffer(64)
   n := r.read_line(buf)?
   print(n)
   w := fs.create(args[2])?
@@ -179,7 +179,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(16)
+  mut buf := buffer(16)
   n := r.read_line(buf)?
   line := buf.bytes().as_str()?
   print(line.len())
@@ -206,7 +206,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(8)
+  mut buf := buffer(8)
   mut count := 0
   loop {
     n := r.read_line(buf)?
@@ -237,7 +237,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(8)
+  mut buf := buffer(8)
   n := r.read_line(buf)?
   print(buf.len())
   print(n)
@@ -266,7 +266,7 @@ Rec { n: i64 }
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(8)
+  mut buf := buffer(8)
   mut total := 0
   loop {
     k := r.read_line(buf)?
@@ -294,7 +294,7 @@ import std.fs
 import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   r := fs.open(args[1])?
-  buf := buffer(8)
+  mut buf := buffer(8)
   n := r.read_line(buf)?
   print(n)
   return Ok(())
@@ -322,7 +322,7 @@ import std.io
 pub fn main(args: array<str>) -> Result<(), Error> {
   base := fs.open(args[1])?
   r := base.buffered()
-  buf := buffer(8)
+  mut buf := buffer(8)
   n := r.read_line(buf)?
   line := buf.bytes().as_str()?
   print(line.len())
@@ -364,17 +364,18 @@ fn unbuffered_read_path_unchanged() {
     let prog = "\
 import std.fs
 import std.io
-fn drain(r: reader, buf: buffer, w: writer) -> Result<(), Error> {
-  n := r.read(buf)?
-  if n == 0 { return Ok(()) }
-  w.write(buf.bytes())?
-  return drain(r, buf, w)
+fn drain(r: reader, w: writer) -> Result<(), Error> {
+  mut buf := buffer(4)
+  loop {
+    n := r.read(buf)?
+    if n == 0 { break Ok(()) }
+    w.write(buf.bytes())?
+  }
 }
 pub fn main(args: array<str>) -> Result<(), Error> {
   r := fs.open(args[1])?
-  buf := buffer(4)
   w := io.stdout
-  drain(r, buf, w)?
+  drain(r, w)?
   return Ok(())
 }
 ";