stdlib collection/mem/string と静的検査の安全設計

core/mem

現状の core/mem は byte allocator、raw load/store、bulk copy/move、typed MemPtr wrapper、RegionToken を 1 module に持つ。

良い点:

• mem_copy<T> / mem_move<T> は T: Copy に制約され、non-Copy の浅い byte copy を public helper から行いにくくなっている。
• RegionToken<T> を使う string / ByteBuf の確定経路が増え、確定前 owner を local raw address ではなく token に置く方向へ進んでいる。
• Resource IR は raw allocation の free obligation、raw cell initialized state、borrow state を追跡し始めている。

問題:

• MemPtr<T> は stdlib コメント上は Copy な non-owning pointer であり、ByteBuf / ByteBuilder / StringBuilder / Vec の public owner field からは外れた。残る問題は、RegionToken<T> 自体が forge 可能な owner token である点である。
• RegionToken<T> は region_new で stdlib code から allocator-issued raw owner identity を束ね直せるため、compiler-issued capability ではない。
• dealloc_region<T> は storage-only free と initialized payload destruction を API 上で分けない。non-Copy payload collection では、OwnedBuffer<T> / initialized cell state / drop traversal が入るまで .T: Copy 境界を維持する。
• raw i32 API と safe-ish typed API が同じ名前空間にあり、self-host 側が discipline を誤って広げやすい。

結論として、現状の core/mem 方針は過渡期の安全強化としては妥当だが、最終設計としては不適切である。根本修正は MemPtr の強化ではなく、役割分割である。

alloc/string

現状の string は [len:i32][bytes...] layout を使い、str 自体は UTF-8 保証された immutable value として扱う。

改善済みの点:

• string_alloc_region / string_region_data_ptr / string_finish により、出力 str の確定前 owner を RegionToken<u8> に寄せている。
• StringBuilder は固有の Option<MemPtr<u8>> field を持たず、ByteBuilder owner を保持する wrapper になった。
• append は ByteBuilder の typed push_* / push_str / push_str_slice / push_bytebuf に委譲し、text builder 側では raw byte 書き込みを行わない。
• UTF-8 lead byte の分類など、一部で enum / match による分岐へ移行している。
• numeric conversion は root facade から分離済みで、integer conversion は integer/common が bool/digit/radix/u128 helper、integer/format が文字列化、integer/parse が解析と範囲検査を所有する形へ整理されている。float conversion も float/format が f64/f32 文字列化と raw output allocation、float/parse が小数・指数解析を所有する。

残る問題:

• string_addr / string_from_addr_unchecked は storage.nepl 内の private helper に閉じた。access.nepl / scanner.nepl が必要とする str_addr 由来 observer も各 module の private helper にし、通常 source が direct import して raw i32 observer や raw address finalizer として使う経路は残さない。
• string_finish_base は MemPtr<u8> から str を作れる不要な確定 helper だったため削除した。str への所有権移行は RegionToken<u8> を消費する string_finish だけが担当する。
• scanner_string_byte_at_unchecked は scanner 内部の範囲正規化後だけに使う private helper にした。public scanner API は range helper / byte classification helper に限定する。
• alloc/string/access は safe public API に寄せ、byte_at が len で範囲確認した後に private raw helper を呼ぶ。旧 string_byte_at_unchecked は root facade から再公開せず、過渡的な alloc/string/unchecked_access も削除した。既存 hot path は alloc/string/byte_index の private StringByteIndex witness を使う checked helper へ移行済みで、任意 i32 が raw read へ直接届かない。
• StringBuilder 固有の raw owner field は解消済みである。残る理想形は ByteBuilder / ByteBuf 側を OwnedBytes / OwnedRegion<u8> へ移すことである。

alloc/io

ByteBuf と ByteBuilder は現時点で stdlib memory model の先行実装になっている。module 責務は alloc/io root facade、io/bytebuf、io/bytebuilder、io/traits に分離済みで、raw memory capability は io/bytebuf と io/bytebuilder の exact path に限定する。

良い点:

• ByteBuf / ByteBuilder の free obligation は RegionToken<u8> field に集約され、MemPtr<u8> は参照から得る non-owning view としてだけ扱う。
• 空 storage は ByteBufStorage::Empty / ByteBuilderStorage::Empty で表し、zero-size sentinel RegionToken は持たない。所有 storage だけが Owned(RegionToken<u8>) payload を持つ。
• ByteBuf の free / to-str 変換は RegionToken owner を centralized cleanup へ渡す。
• ByteBuilder は append 成功時に payload pointer を取り出して包み直さず、owner field 全体を移す。
• ByteBuilder は reserve / append / finish 失敗時にも internal free で owner transfer を隠さず、ByteBuilderError / ByteBuilderByteBufError へ owner を戻す。
• stream trait 群は io/traits に分離され、raw memory operation を持たない抽象境界として監視される。

残る問題:

• RegionToken<T> はまだ stdlib code から region_new で allocator-issued raw owner identity を束ねて構築できるため、compiler-issued capability ではない。
• empty / allocated と capacity / initialized prefix の一部は ByteBuf / ByteBuilder の struct discipline に残る。

alloc/collections

collections は self-host に必要な基礎構造だが、現状は安全設計として最も再設計が必要な領域である。

現状:

• HashMap / HashSet は Empty / Full / Tombstone の enum と typed storage へ移行済みで、raw bucket status に戻さない source policy を持つ。
• Queue / Deque / RingBuffer / Stack / BinaryHeap は raw header を廃止し、Vec<Option<T>> storage へ移行済みである。live slot と inactive slot は Some / None で表す。Stack / Queue / Deque / RingBuffer / BinaryHeap の pop は更新後 owner と item を同時に返し、Deque.push_front / push_back と BinaryHeap.push の grow failure は元 owner と diagnostic を専用 error payload で返す。
• BTreeMap / BTreeSet は sorted-array 形式の typed Vec<Option<T>> storage へ移行済みであり、raw key/value pointer layout ではない。
• List は raw node chain を廃止し、items: Vec<T> storage へ移行済みである。論理先頭を Vec 末尾に置くことで先頭追加と tail を owner-preserving に実装している。map / filter の failure も ListTransformError<T> に入力 owner を戻すため、fallible transform が Diag だけへ owner を隠す入口は閉じた。
• CountingBloomFilter / BitSet / AdjacencyMatrix / BloomFilter / SparseSet / Fenwick / SegmentTree / DisjointSet は Vec<u8> / Vec<i32> storage へ移行済みである。payload は主に Copy だが、基礎 Vec 自体はまだ raw memory backed storage boundary を持つ。
• Vec<T> は buffer: OwnedBuffer<T> だけを持ち、OwnedBuffer<T> が len/initialized_len/cap/storage を束ねる。空 Vec は VecStorage<T>::Empty、allocated storage は VecStorage<T>::Owned(RegionToken<T>) で表す。型/storage/access/transform/query/mutation/sort の責務は submodule に分離済みで、MemPtr<T> は data_mem_view<T>(&Vec<T>) の VecDataView::Data payload からだけ得る。VecDataView::Empty と VecDataView::Invalid(reason) は enum branch として分離し、null pointer sentinel で同一視しない。ただし基礎型 OwnedBuffer<T> はまだ forgeable RegionToken<T> と Copy-only raw element helper に依存するため、owner model の完成には compiler-issued owner token と initialized cell state が必要である。
• get_ref<T: Copy> のように Copy 読み取りへ制限した API はあるが、get(Vec<T>) -> Option<T> や pop などは move-out と owner state の扱いが明確でない。
• free<T>(Vec<T>) などの storage free は、要素の Drop / consume と storage-only dealloc を完全には分けていない。

問題:

• MemPtr<T> field が owner なのか borrowed view なのか、型から分からない。
• 空/非空、初期化済み prefix、未初期化 capacity、tombstone、moved-out cell が構造化されていない。
• push(Vec<T>, T) -> Result<Vec<T>, E> のような fallible update は major collection では owner-preserving error payload へ移行済みだが、新しい owner-consuming fallible API が bare Diag / StdErrorKind を返さないことを source policy で継続監視する必要がある。
• replace / clear / remove は non-Copy payload の旧値を drop/return する責務を API で表せていない。
• raw header layout は Resource IR にとって追跡対象が増え、静的検査が複雑化する。

1. memory role の分離

最終的な概念分離は次の形にする。

MemPtr<T> は最後まで non-owning に固定する。Option<MemPtr<T>> は過渡的には許容するが、長期的には Option<OwnedRegion<T>> または StorageState<T> へ移す。

2. storage state は enum で表す

null pointer、数値 status、len == 0 による owner 有無の暗黙表現はやめる。

概念例:

enum StorageState<.T>:
    Empty
    Allocated OwnedRegion<.T>

struct OwnedBuffer<.T>:
    storage <StorageState<.T>>
    len <i32>
    cap <i32>

hash table の bucket も数値ではなく enum にする。

enum BucketState<.K,.V>:
    Empty
    Full Bucket<.K,.V>
    Tombstone

これにより match が網羅性検査の対象になり、status 値の typo や未知状態を静的に扱える。

3. collection API を owner discipline ごとに分ける

collection は少なくとも次の API class に分ける。

Result<Vec<T>, E> だけでは、失敗時に入力 owner を返すのか、free するのか、item を保持するのかが分からない。non-Copy payload を扱う API は、失敗時の owner を型に含める。

概念例:

enum PushResult<.C,.T,.E>:
    Ok .C
    Err PushError<.C,.T,.E>

struct PushError<.C,.T,.E>:
    collection <.C>
    item <.T>
    error <.E>

短期的に Result<Vec<T>, E> を維持する場合は、対象を T: Copy に限定するか、Err path で collection/item を完全に consume/drop することを API 名と doc に出す。ただし self-host の compiler data structure では、owner を暗黙に破棄する API を標準にしない。

4. Vec を collection の基礎型として再設計する

Vec<T> は次の不変条件を持つ typed collection にする。

• 0 <= len <= cap
• storage = Empty なら len = 0 かつ cap = 0
• storage = Allocated(region) なら region size は cap * size_of<T>
• 0..len は initialized
• len..cap は uninitialized storage
• T: Copy でない値を byte copy / byte move しない
• grow では initialized prefix を move し、旧 storage は storage-only 状態にしてから free する
• free では initialized prefix を drop/consume し、storage-only になってから dealloc する

現在の Vec<T> { len, cap, storage: VecStorage<T> } は MemPtr<T> owner field と split RegionToken<T> field を消し、Empty と allocated token の相関を型で表せるようにした点では前進だが、initialized prefix / moved slot / drop obligation を型と compiler-issued token で表せないため、根本的には OwnedBuffer<T> へ置き換える。

5. string / byte buffer は collection 設計の先行実装として扱う

ByteBuf / ByteBuilder は RegionToken<u8> owner に移行し、MemPtr<u8> を owner field として公開しない形になった。ただしこれは完成形ではない。RegionToken は compiler-issued token ではなく、initialized prefix / capacity の証明も OwnedBytes ほど明示的ではない。StringBuilder は ByteBuilder wrapper へ移したため、独立した raw owner field は持たない。

理想:

• OwnedBytes は storage owner と len/cap を持つ。
• ByteBuilder は OwnedBytesBuilder を持ち、finish で ByteBuf へ owner を移す。
• StringBuilder は UTF-8 生成専用 builder で、ByteBuilder / ByteBuf owner boundary を通して str へ確定する。将来は finish で OwnedStringRegion から str へ確定する。
• str は immutable finalized value であり、通常 API から raw address へ戻せない。
• unchecked conversion は compiler/internal boundary に閉じ、source policy で public stdlib からの使用を監視する。

type safety

• str と i32、MemPtr<T> と i32、owner token と pointer projection を型で混同させない。
• bucket status、diagnostic code、token kind、resource state は enum で表し、文字列や数値で管理しない。
• match は enum variant の網羅性を検査する。safety-critical enum では wildcard arm に逃げない。
• T: Copy が必要な raw copy / read API は trait bound と Resource IR の両方で検査する。

memory safety

• allocation は owner token を生成し、owner token は exactly once で return / move / free される。
• MemPtr<T> の copy は free obligation を複製しない。
• raw load<T> は T: Copy の copy read と non-Copy の move-out を区別する。
• raw store<T> は uninitialized cell の initialize と initialized cell の overwrite を区別する。non-Copy overwrite は旧値の drop/consume が証明される場合だけ許可する。
• dealloc / realloc は initialized non-Copy cell が残る storage を拒否する。
• branch / loop / match merge は owner / cell / borrow state を MaybeMoved / MaybeFreed として保守的に合流し、曖昧な場合は拒否する。
• function summary は aggregate field、enum payload、raw storage cell、borrow token を projection 単位で保持する。

diagnostics

• Resource IR diagnostic は resource.owner.*、resource.cell.*、resource.borrow.*、resource.raw.*、resource.lower.* のように意味分類を失わない。
• self-host の diagnostic id も Rust 側の enum-first 設計に合わせる。内部主キーに文字列や数値を使わない。

Stage A: safety policy の固定

• MemPtr を owner field として使う新規 public API を禁止する source policy を追加する。
• null pointer owner、direct Result::Ok Vec ... mem_ptr_wrap 0、bucket status magic number の監査テストを追加する。
• 既存の ByteBuf / builder owner boundary 回帰テストは維持する。

2026-05-13 追記:

• nodesrc/test_stdlib_memptr_owner_field_policy.js を追加し、stdlib 全体の struct field に直接現れる MemPtr / Option<MemPtr> を集約して監視する。
• この policy は MemPtr field を安全証明として認めるものではない。現時点で残る RegionToken.ptr を Stage B/F の移行対象として固定し、それ以外の新規 MemPtr owner-like field を禁止する。
• source policy runner に組み込み、module 個別 policy の外で raw-memory-backed owner field が増える退行を検出する。

2026-05-14 追記:

• StreamWriter.buf は StreamWriter が buffer owner を ByteBuilder に集約したことで移行済みになった。残件 baseline は 8 field ではなく 7 field であり、nodesrc/test_stdlib_memptr_owner_field_policy.js の transitional allowlist と一致させる。
• StreamScanner.header は StreamScanner が input owner を ByteBuf field、cursor position を typed Vec<i32> storage へ分けたことで移行済みになった。残件 baseline は 7 field ではなく 6 field であり、nodesrc/test_stdlib_memptr_owner_field_policy.js の transitional allowlist と一致させる。
• compiler core 側では、RegionToken<T> の direct constructor restriction と同じ StructConstructorPolicy::RawMemoryBoundaryOnly(OwnerToken) を Copy capability impl target validation にも接続した。これにより stdlib public API 移行中でも、owner token を構造的 Copy 型として trait 層から複製可能にする経路を閉じる。
• VecDataLen<T> は Vec.data: MemPtr<T> と len を public struct field として再包装するだけの raw storage view carrier だったため削除した。当時の呼び出し側は raw view と len<T>(&Vec<T>) を明示的に別々に扱う方針へ移行し、その後 2026-05-20 に raw view observer は data_mem_view<T>(&Vec<T>) -> VecDataView<T> へ置き換えた。残件 baseline は 6 field ではなく 5 field であり、VecDataLen.data を transitional allowlist から外した。
• StringBuilder は ByteBuilder と重複して Option<MemPtr<u8>> / len / cap を持つ設計をやめ、ByteBuilder owner を保持する typed wrapper へ移した。残件 baseline は 5 field ではなく 4 field であり、StringBuilder.data を transitional allowlist から外した。
• ByteBuf / ByteBuilder は Option<MemPtr<u8>> owner field をやめ、storage owner を RegionToken<u8> 由来の typed storage enum に集約した。ByteBufStorage::Empty | Owned(RegionToken<u8>) と ByteBuilderStorage::Empty | Owned(RegionToken<u8>) により、空 storage は zero-size RegionToken sentinel を持たず、所有 storage だけが free obligation owner payload を持つ。region_ptr / io_bytebuf_data_ptr_ref / byte_builder_data_ptr_ref は参照から non-owning MemPtr view だけを返す。残件 baseline は 4 field ではなく 2 field であり、ByteBuf.ptr と ByteBuilder.ptr を transitional allowlist から外した。
• Vec<T> は data: MemPtr<T> owner field をやめ、storage owner を region: RegionToken<T> field に集約した。その後 data_mem_ptr<T> も削除し、現在は data_mem_view<T> が VecDataView<T> として valid empty / valid data / invalid invariant を分ける。残件 baseline は 2 field ではなく 1 field であり、Vec.data を transitional allowlist から外した。

2026-05-15 追記:

• Vec.data_ptr<T>(&Vec<T>) -> i32 は public raw address observer として残さず削除した。さらに 2026-05-20 に data_mem_ptr<T>(&Vec<T>) -> MemPtr<T> も削除し、raw i32 address への変換は data_mem_view<T> の VecDataView::Data branch を持つ raw-memory-boundary 実装箇所に限定する。
• kpsearch の lower/upper bound / unique 内部 raw helper は private とし、公開面は Vec<i32> owner wrapper だけに揃えた。ordinary source の利用例は raw buffer 構築ではなく Vec<i32> による doctest で表す。
• vec_storage_mem_ptr<T>(VecStorageState, &RegionToken<T>) は public helper として残さず削除した。storage state から data view への projection は data_mem_view<T>(&Vec<T>) が直接 match して所有し、結果を VecDataView<T> の enum branch として返す。
• VecStorageState と split region: RegionToken<T> field は廃止し、VecStorage<T>::Empty | Owned(RegionToken<T>) へ移行した。vec_free_storage<T> は owner-carrying enum を消費し、Empty branch では free obligation が存在しないこと、Owned branch では RegionToken<T> を消費することを source type と match で証明する。borrowed observer は &VecStorage<T> match により payload を参照として束縛し、owner token を move/copy しない。
• Vec の in-place sort family は storage を書き換える API なので、raw write helper、quick / heap / simple sort、raw slice sort adapter、owner-returning sort wrapper、default sort を impure *> signature へ揃えた。observer の sort_is_sorted と比較 helper は pure のまま残し、effect contract でも観察と破壊的更新を分離する。
• alloc/collections/vec/sort root facade は raw MemPtr helper と raw slice adapter を再公開しない。さらに direct-importable な sort/raw/* helper module、sort/merge/buffer、sort/merge/range も残さず、raw traversal は sort_quick / sort_heap / simple sort / merge/api など、len・storage view・scratch owner を扱う検査済み implementation file 内の private boundary に閉じる。ordinary caller は Vec の sort API と sort_is_sorted observer だけを使う。
• root alloc/collections/vec facade は unchecked raw element helper を再公開しないだけでなく、alloc/collections/vec/raw という直接 import 可能な bypass module 自体を残さない。Copy element の raw load/store は、get/push/replace/pop/map/filter/prefix など、len・storage variant・capacity を検査する public 操作と同じ source file 内に置き、検査条件と raw operation を分離しない。
• RegionToken<T> の realloc は core/mem/pointer/region.nepl の realloc_region_bytes_keep<T> へ集約した。Vec / ByteBuilder は token の ptr / size を直接分解して realloc_ptr を呼ばず、成功時は新 owner、失敗時は旧 owner を RegionReallocError<T> 経由で受け取る。Resource IR owner checker は region_ptr(&region) から得た非所有 MemPtr の raw-address alias を集約値コピー越しに保持するため、realloc_region_bytes_keep の Ok / Err 両 payload が free obligation owner を返すことを compiler 側で証明する。
• Vec.push の grow capacity は vec_next_capacity<T> で .T の element size と allocator payload 上限から証明してから決定する。unchecked cap * 2 は push hot path から外し、上限超過は CapacityExceeded として VecPushError に元 Vec owner を戻す。
• root std/fs / std/stdio facade は raw ABI submodule を再公開しない。WASI / LLVM syscall helper と raw scratch helper は std/fs/raw / std/stdio/raw を明示 import した implementation boundary だけに置き、通常の filesystem / standard I/O import は safe public surface に限定する。

2026-05-16 追記:

• RegionToken<T> は ptr: MemPtr<T> を持たず、raw: i32, size: i32 の owner token layout に移行した。MemPtr<T> は region_ptr<T>(&RegionToken<T>) / region_ptr_at<T,U> の checked non-owning projection としてだけ使う。
• region_new<T> は internal boundary で allocator / realloc helper が返した raw owner identity と size を束ねて token を構築する。MemPtr<T> は non-owning view なので region_new の入力にはしない。通常 source は RegionToken constructor、raw field projection、region_token_raw_ref のような raw identity accessor を直接使えず、compiler owner aggregate boundary と source capability が検査する。
• Resource IR owner summary は direct raw memory op だけでなく、callee summary が消費する raw owner alias も seed する。これにより dealloc_region<T> が RegionToken.raw から一時 MemPtr.raw を作り dealloc_ptr<T> へ渡す場合も、caller では RegionToken<T> owner が消費されたことが証明される。
• nodesrc/test_stdlib_memptr_owner_field_policy.js の transitional allowlist は 0 件になった。今後 stdlib の struct field に MemPtr / Option<MemPtr> を owner-like field として戻すことは禁止する。
• ただし RegionToken<T> はまだ compiler-issued OwnedRegion<T> ではない。Stage B/D/F の最終目標は、RegionToken を過渡 owner token として閉じ、OwnedBuffer<T> / StorageState<T> / initialized prefix / compiler-issued free obligation owner へ進めることである。
• 追加調査で確認した public alloc_ptr<T> / realloc_ptr<T> / dealloc_ptr<T> は ISS-20260515T163252091Z-PUBLIC-ALLOC-PTR-APIS-STILL-ENCODE-F-EECDD686 で削除済みである。2026-05-16 時点で、safe facade だけでなく direct import 可能な core/mem/pointer/alloc module 自体も残さない。
• std/stdio/write/byte.nepl の print_byte は 1 byte scratch buffer を RegionToken<u8> owner と non-owning MemPtr<u8> view に分けた。続く stdio fd write/read、std/fs fd write/read/open/stat、LLVM fallback C string、std/env/cliarg raw scratch も同じ方針で RegionToken owner と raw ABI view を分離済みである。
• std/stdio/write/fd.nepl も iov / nwritten scratch owner を RegionToken<u8> に移し、raw iovec layout は std/stdio/raw.nepl の stdio_fd_write_from_result へ閉じた。stdout/stderr write path では MemPtr<u8> を free owner として扱わない。
• Vec<T> は buffer: OwnedBuffer<T> だけを持つ public facade へ移行した。OwnedBuffer<T> が len/cap/storage と storage owner enum を保持し、observer / mutation / transform / sort wrapper はすべて OwnedBuffer<T> 経由で storage を参照または消費する。source policy は旧 Vec<T> len cap storage constructor と Vec<T> 直下の len/cap/storage field の復活を拒否する。残件は initialized prefix、move-out / replace / drop traversal、compiler-issued owner token の接続である。

2026-05-19 追記:

• Resource IR owner summary は host memory span だけでなく raw memory operation の readable / writable span も caller requirement として要約する。string_from_mem_unchecked_result / string_from_utf8_mem_result のような stdlib callee 内 raw span helper は、caller 側の RegionToken extent と length の照合を要求する。
• これは MemPtr<T> に owner 責務を戻す変更ではない。MemPtr<T> は non-owning view のままで、proof は backing owner と span requirement の対応から導出する。
• cstr_to_str_bounded_result のような loop-guarded scanner では、while i < max_len と load_u8(mem_ptr_add p i) から p[0..max_len] を要約する汎用 path-conditioned span proof がまだ不足している。これは ISS-20260519T144811685Z-RESOURCE-IR-RAW-SPAN-SUMMARIES-MISS--FA49E19D で扱う。

2026-05-20 追記:

• raw-memory-backed API の staged effect migration parent は、ISS-20260427T204839136Z-STDLIB-RAW-MEMORY-BACKED-APIS-REQUIR-E503CD84 として closure audit 済みである。raw memory primitive は compiler の internal effect / Resource IR gate / source capability proof に接続され、public raw MemPtr surface は source policy で監視されている。
• collection free が non-Copy payload を受け入れて要素 Drop を呼ばない旧バグは、ISS-20260425T000000Z-RV-STDLIB-004-91534828 の closure audit で fixed とした。現行 public surface は Copy-only 境界と source policy で guarded である。
• これは non-Copy collection の完成を意味しない。compiler-issued owner token、moved slot、drop traversal、InitializedCell / Resource IR 接続による final support は ISS-20260520T152218366Z-NON-COPY-COLLECTION-PAYLOAD-SUPPORT--A6A88543 で扱い、self-host 実装はそれまで safe subset を使う。
• 2026-05-21 に ISS-20260521T020307778Z-COLLECTION-SLOT-OWNER-TRANSFER-NEEDS-403A919A で、同一関数内の non-Copy slot owner-transfer は raw StoreValue / MoveOutLoadedCell fact を消費する generic proof として通せるようになった。summary replay の branch / loop / indirect call でも CellTable を path merge するため、片方の summary path だけの raw value-flow fact は後続 proof に使えない。これは positive support の最初の段階であり、callee summary certified proof と drop traversal はまだ parent issue の残件である。
• 2026-05-21 に ISS-20260521T025115696Z-COLLECTION-SLOT-SUMMARIES-NEED-CERTI-92379E7C で、callee 内で証明済みの raw value-flow proof を summary event の owner-transfer proof として載せるようになった。caller replay はその certified proof を obligation と照合し、caller-local raw fact の再要求や stdlib helper allowlist なしに non-Copy slot initialize / move-out を通す。
• 2026-05-21 に ISS-20260521T031943441Z-COLLECTION-SLOT-DROP-LIFECYCLE-NEEDS-DCBDB1EC で、raw load された payload owner の value origin と ResourceOp::Drop / auto-drop を DropLoadedCell proof として結び、droppable DropInitialized / ReplaceDropOld を state-only annotation ではなく actual drop proof で通せるようにした。summary event proof は owner-transfer proof と slot-drop proof を別フィールドで保持し、callee-certified drop proof を caller replay へ伝える。ReplaceDropOld は old payload drop proof と new payload store proof の両方を要求する。
• 2026-05-21 に ISS-20260521T050436552Z-SOURCE-LEVEL-NON-COPY-COLLECTION-SLO-D0BB9BAF で、手書き Resource IR だけでなく compiler-owned stdlib source path でも raw store/load fact が collection slot lifecycle proof と同じ raw cell に結び付くことを固定した。raw address alias と explicit [+0] は同一セルとして扱うが、非ゼロ offset は同じ proof として扱わないため、generic proof boundary を広げすぎない。
• 2026-05-21 に ISS-20260521T054050076Z-SOURCE-LEVEL-DROPPABLE-COLLECTION-SL-7041CED9 で、compiler-owned stdlib source path でも DropInitialized / ReplaceDropOld が actual loaded-value drop proof と replacement store proof を消費することを固定した。これは Vec 専用 proof や stdlib helper allowlist ではなく、source lowering された raw load / assignment overwrite drop / raw store と collection slot lifecycle event が同じ generic Resource IR proof boundary に到達することを確かめる regression である。
• 2026-05-21 に ISS-20260521T055400560Z-SOURCE-LEVEL-COLLECTION-SLOT-PROOF-L-B5FB8CDA で、indexed collection slot の symbolic offset も compiler-owned stdlib source path で固定した。同じ off local から raw store/load と lifecycle event が別 temporary として下がっても、scalar origin に正規化して同一 slot proof として扱う。一方、off + size_of<T> のように別 offset へ進んだものは証明しないため、動的 slot proof を広げすぎない。
• 2026-05-21 に ISS-20260521T062752580Z-COLLECTION-SLOT-LIFECYCLE-LOWERING-I-653BBF1A で、collection slot lifecycle producer と storage relocate producer を Resource lowering coverage の typed count に追加した。これにより compiler-owned stdlib source の lifecycle intrinsic が Resource IR producer へ下がらない回帰は、target place coverage だけで隠れず ResourceCoverageKind::CollectionSlotLifecycle / CollectionStorageRelocate の CountMismatch として検出される。
• 2026-05-21 に ISS-20260521T064245727Z-COLLECTION-SLOT-BORROWREAD-LACKS-SOU-1999DF36 で、source-level BorrowRead を固定した。BorrowRead は owner-transfer や drop proof を消費せず initialized slot state を維持するが、MoveOut 後の slot には BorrowRead / Moved の typed refutation を返す。これは observer API を Copy read や raw load に読み替えず、generic slot lifecycle state の precondition として扱うための回帰である。
• 2026-05-21 に ISS-20260521T065624831Z-COLLECTION-SLOT-STATE-RETURN-SUMMARY-4591B626 で、callee が Result::Err(storage) のような enum payload に owner を包んで返す場合の slot state transfer を固定した。return summary は Result 固有処理ではなく、Resource IR の construct / branch / match / local forwarding を辿って return payload suffix を構成するため、fallible owner-preserving API でも caller の match bind 後に live slot state を失わない。
• 2026-05-21 に ISS-20260521T071641871Z-COLLECTION-SLOT-RETURN-SUMMARY-MISSE-6D5CDC78 で、callee summary の return_transfers を wrapper return summary へ合成するようにした。これにより、fallible API が identity_storage などの owner-preserving helper を呼び、その call output を enum payload に包んで返す場合でも、caller actual の slot state が wrapper return payload へ generic に追従する。stdlib/module allowlist ではなく Resource IR call target summary、call args、place suffix、raw owner alias canonicalization だけで証明する。

2026-05-21 追記:

• CollectionSlotLifecycleEvent / CollectionSlotStateTable は、ResourceOp::CollectionSlotLifecycle として Resource IR の通常命令に接続した。これにより non-Copy collection slot の Initialize / BorrowRead / MoveOut / Replace / Drop / StorageDealloc は、stdlib module ごとの個別許可ではなく compiler core の generic typed proof boundary として検査される。
• initialized checker は CollectionSlotStateTable を関数状態に含め、branch / loop / match の各 path を CollectionSlotStateTable::merge_paths で合流する。片側だけ initialized な slot や片側だけ storage release 済みの状態は MaybeInitialized / MaybeReleased として残り、合流後の reinit / move / drop / storage dealloc を typed refutation で拒否する。
• ResourceCheckDiagnostic::CollectionSlotRefuted と ResourceCollectionSlotDiagnosticCode を追加し、slot lifecycle の失敗理由を enum のまま保持する。diagnostic id は serialization 用の dotted string であり、checker 内の authority にはしない。
• 今回の接続で Resource IR 上の手書き operation は検査対象になったが、stdlib collection lowering が実際の Vec<T> / OwnedBuffer<T> operation から ResourceOp::CollectionSlotLifecycle を発行する段階は未完である。次段階では source policy や module allowlist に逃がさず、collection API の source semantics から generic slot lifecycle event を生成する。
• callee 内の slot lifecycle effect は CollectionSlotLifecycleFunctionSummary として caller へ伝播する。summary は parameter projection 上の Event / Merge / Loop であり、direct call は actual arg へ suffix を置換して再適用し、function alias indirect call は候補関数ごとに state path を merge する。これにより helper 関数を跨いだ live slot / moved slot / partial branch slot state は caller の CollectionSlotStateTable に残る。関連 issue は ISS-20260520T200325099Z-COLLECTION-SLOT-LIFECYCLE-EFFECTS-DO-6E6407FC。
• callee が owner parameter をそのまま返す owner-preserving helper では、callee 内に新しい slot lifecycle event がなくても caller actual の slot state を call output へ transfer する必要がある。CollectionSlotLifecycleFunctionSummary は return_transfers を持ち、return value と parameter prefix の関係から generic summary fact を作る。call site では raw alias canonicalization を通して actual arg prefix から output prefix へ slot state を移すため、stdlib module allowlist なしに owner-preserving API を跨いだ live slot を検出できる。関連 issue は ISS-20260521T004808159Z-COLLECTION-SLOT-SUMMARIES-DO-NOT-TRA-2AA84347。
• InitializeEmpty / MoveOut / ReplaceReturnOld / ReplaceDropOld は payload value-flow proof と結び付いていなければならない。slot state transition だけを annotation として許すと、実際の payload consume / materialize が欠落しても Resource IR が所有権移動を信じてしまうため、2026-05-21 時点では non-Copy payload の owner-transfer lifecycle event を OwnerTransferRequiresValueProof として拒否する。Copy payload の state marker は維持するが、non-Copy collection API の positive support は payload place proof と compiler-owned slot-drop lowering を実装してから開く。collection slot の place 正規化も raw value origin ではなく owner-cell canonicalization を使い、value move 後の storage dealloc が移動先 live slot を見落とさないようにした。関連 issue は ISS-20260521T010410090Z-COLLECTION-SLOT-OWNER-TRANSFER-LIFEC-3C1056B2。
• DropInitialized / ReplaceDropOld は droppable payload であれば、slot から raw load された value origin が actual ResourceOp::Drop / assignment overwrite auto-drop / scope auto-drop に到達した proof を消費する。raw load fact は materialize proof であって destructor execution proof ではないため、MoveOutLoadedCell だけで slot を dropped に進めることは禁止する。source-level regression でもこの境界を固定し、actual drop が lifecycle event より後ろにしか現れない code は通さない。関連 issue は ISS-20260521T031943441Z-COLLECTION-SLOT-DROP-LIFECYCLE-NEEDS-DCBDB1EC と ISS-20260521T054050076Z-SOURCE-LEVEL-DROPPABLE-COLLECTION-SL-7041CED9。
• production lowering / annotation path は ISS-20260520T200531197Z-COLLECTION-SLOT-LIFECYCLE-HAS-NO-PRO-298A1B25 で対応済みである。CollectionSlotLifecyclePrimitive、SourceCapabilityUseSite::CollectionSlotLifecycleBoundary、typecheck gate、Resource IR lowering producer を接続し、compiler-proven source evidence を持つ exact span からだけ ResourceOp::CollectionSlotLifecycle を生成する。
• collection slot lifecycle producer は stdlib function name allowlist ではない。compiler-owned intrinsic を typed enum で分類し、source capability proof と Resource IR checker が同じ lifecycle event を見る。anchor は MemPtr<T> / RegionToken<T> の element type と intrinsic type args を照合し、storage dealloc は owner token anchor に限定する。これにより、Vec/Stack/Queue など module ごとの proof machine を増やさず、generic CollectionSlotStateTable へ集約する。
• collection slot lifecycle intrinsic の public stdlib wrapper は追加しない。通常 import 可能な wrapper は user source に lifecycle event 偽造の入口を与えるため、stdlib collection 実装が必要な箇所で compiler-proven source evidence を持つ境界として使う。現行 Copy-only Vec に無理に注釈を付けるのではなく、non-Copy API と drop traversal を導入する段階でこの producer を使う。
• 関連 issue: ISS-20260520T192939566Z-RESOURCE-IR-DOES-NOT-CARRY-COLLECTIO-5585A1D7。

Stage B: core/mem の internal/public 分離

• 前提として、typecheck の import visibility が pub / private item boundary を binding authority として扱う必要がある。現状の blocker は ISS-20260512T235355207Z-IMPORT-VISIBILITY-DOES-NOT-ENFORCE-P-30FB5573 で追跡する。
• raw i32 allocator / load/store は internal raw module に移す。
• public API は MemPtr view、OwnedRegion owner、initialized cell 操作を分ける。
• region_new のような token forging API を廃止する。
• dealloc_region は storage-only region にだけ許可する。

Stage C: string / byte buffer を owner wrapper へ移行

• ByteBuf / ByteBuilder の Option<MemPtr<u8>> owner field は削除済みである。ByteBuf は ByteBufStorage::Empty | Owned(RegionToken<u8>)、ByteBuilder は ByteBuilderStorage::Empty | Owned(RegionToken<u8>) に移し、empty sentinel も削除済みである。ByteBuilder の fallible reserve / append / finish は owner-preserving error payload に揃えた。次は forgeable RegionToken<u8> を StorageState<u8> または compiler-issued OwnedBytes に移す。
• string_finish_base は削除済みであり、raw address から str への変換も private string_from_addr_unchecked に閉じた。次は RegionToken<u8> を OwnedStringRegion / compiler-issued owner token へ移す。
• fallback API と Result API の責務を整理し、allocation failure を空値 success に潰さない入口を標準にする。

Stage D: OwnedBuffer<T> と Vec 再実装

• Vec<T> を OwnedBuffer<T> 上に再実装する。2026-05-16 時点で public facade と backing storage owner の分離は完了し、Vec<T> 直下の len/cap/storage は削除済みである。
• Copy read、borrow read、move-out、replace、clear、free を別 API に分ける。
• fallible push/grow は Err path で collection / item owner を返す設計にする。
• Vec<T> の doctest は T: Copy と non-Copy payload の両方を持つ。

Stage E: derived collections の raw header 廃止

• Stack / Queue / Deque / BinaryHeap は raw header ではなく Vec / OwnedBuffer wrapper へ戻す。
• bitset / bloom filter / adjacency matrix は OwnedBytes を使う。
• HashMap / HashSet は移行済みの BucketState enum と typed bucket storage 契約を維持する。
• BTreeMap / BTreeSet の sorted-array 実装は小規模 ordered table 用であることを名前と doc に出す。

Stage F: Resource IR special-case の削減

• stdlib 側が owner wrapper を持った後、raw alias summary / external raw root special-case を減らす。
• 残すべきものは unsafe/internal boundary の検査に限定する。
• self-host ResourceIR は最初からこの設計に合わせ、過去の HIR 直走査 special-case を移植しない。