Part of #199 (Phase 3, unsafe hygiene). All file:line references are pinned to origin/main at 9da9b9f. Follow-through of the marker rules once adopted.
Measured today: // SAFETY: on 29 of 418 unsafe blocks (strided-view 0 of 23, strided-perm 0 of 27, kernel 24 of 269); // INVARIANT: zero; 33 of 35 #[allow] without adjacent rationale.
Priority sites where the proof is real but remote and unwritten (from the audit): erased.rs:2036, :2067, :2105, :2347, :2603 (new_unchecked from erased descriptors; proof lives in validate_bounds at descriptor construction), static_indexing_plan.rs:161, :186, map_view.rs:1847 (broadcast strides), the uninit blocks listed in the audit at static_indexing_plan.rs:462, :613, :668, copy_plan.rs:194 (execute_uninit_then, the RMW receipt producer, has no rustdoc at all), and the two SAFETY comments that overstate what was checked (gather_plan.rs:736, :1025).
Part of #199 (Phase 3, unsafe hygiene). All file:line references are pinned to
origin/mainat 9da9b9f. Follow-through of the marker rules once adopted.Measured today:
// SAFETY:on 29 of 418 unsafe blocks (strided-view 0 of 23, strided-perm 0 of 27, kernel 24 of 269);// INVARIANT:zero; 33 of 35#[allow]without adjacent rationale.Priority sites where the proof is real but remote and unwritten (from the audit):
erased.rs:2036,:2067,:2105,:2347,:2603(new_uncheckedfrom erased descriptors; proof lives invalidate_boundsat descriptor construction),static_indexing_plan.rs:161,:186,map_view.rs:1847(broadcast strides), the uninit blocks listed in the audit atstatic_indexing_plan.rs:462,:613,:668,copy_plan.rs:194(execute_uninit_then, the RMW receipt producer, has no rustdoc at all), and the two SAFETY comments that overstate what was checked (gather_plan.rs:736,:1025).#[allow].unreachable!guarded bysupports_*,extent-spanning receipts).