Skip to content

T-019: Task loader (load_image + BSP smoke + UNSAFE-2026-0027)#31

Merged
cemililik merged 10 commits into
mainfrom
t-019-task-loader
May 15, 2026
Merged

T-019: Task loader (load_image + BSP smoke + UNSAFE-2026-0027)#31
cemililik merged 10 commits into
mainfrom
t-019-task-loader

Conversation

@cemililik
Copy link
Copy Markdown
Collaborator

@cemililik cemililik commented May 14, 2026

Summary

  • task_loader::load_image<M, N, R> lands in kernel/src/obj/task_loader.rs as the §Simulation row 1–7 state machine (preflight chain → cap_create_address_space → image-page loop with copy_nonoverlapping byte-copy + cap_map(USER|EXECUTE) → stack-page loop with cap_map(USER|WRITE)LoadedImage return). Rollback helper covers every fallible step with reverse-order cap_unmap + pmm.free_frame + leaf-frame direct free + cap_drop on the AS cap.
  • UNSAFE-2026-0027 opens standalone for the loader's copy_nonoverlapping byte-copy (semantically distant from UNSAFE-2026-0026's PMM zero-fill per justify-unsafe audit-tag scoping). UNSAFE-2026-0025 + UNSAFE-2026-0026 each gain a 2026-05-14 smoke-verification Amendment lifting their Pending QEMU smoke verification status — T-019 is the first runtime exerciser of both.
  • BSP wiring in bsp-qemu-virt/src/main.rs adds an 8-byte mov w0, #42; ret placeholder image, calls load_image after the address-space-arena banner, and prints tyrne: image loaded (entry = 0x800000; sp = 0x802000; image bytes 8; stack bytes 4096; AS cap = idx 1) on every boot. Image is loaded but not executed — runnability gates on B5/B6 per phase-b §B4 §Revision-notes.
  • New arch doc docs/architecture/task-loader.md synthesises the loader sequence, rollback contract, v1 baseline leaks (root L0 + intermediate L1/L2/L3 + AS arena slot — full reclaim arrives with future MemoryRegionCap + per-AS destroy ADR), mapping flags, and audit-log surface. Cross-linked from memory-management.md §"Address-space objects" and boot.md sequence diagram.
  • 3 bisectable commits: 911f2ad (types) → 5711756 (function + audit) → ae31bc8 (BSP + docs). Each commit independently compiles + passes tests.

Test plan

  • cargo fmt --check clean
  • cargo host-test — 247/247 passing (was 231 at T-019 commit 1; +16 from this PR's new tests)
  • cargo host-clippy -- -D warnings clean
  • cargo kernel-clippy -- -D warnings clean
  • cargo kernel-build clean
  • QEMU smoke (debug build) — full demo runs to tyrne: all tasks complete; new tyrne: image loaded (...) line lands in expected position
  • qemu-system-aarch64 -d int,unimp,guest_errors — reports only the pre-existing 629 PL011-disabled-UART warnings (no new fault classes, no Translation/Permission faults)
  • T-019 host-test coverage pins every §Simulation row (rows 1–7) + every rollback-contract path (mid-image-loop failure, mid-stack-loop failure, misaligned VA, zero-pages cap_drop-only) + the 7-variant LoadError taxonomy (within-crate exhaustiveness check)

Linked artefacts

🤖 Generated with Claude Code

Summary by CodeRabbit

  • New Features

    • Adds a task‑loader that loads an embedded userspace placeholder into a freshly created address space for boot-time smoke verification (load-only; not executed).
    • Publishes a loader API and explicit error taxonomy for image/stack validation and mapping outcomes.
  • Documentation

    • Updates boot, memory-management, task‑loader, audits, ADR, and roadmap docs to describe behavior, validation/rollback contracts, and audit amendments (T-019 now In Review).
  • Tests

    • Adds host tests and smoke checks, including deterministic allocation-failure injection and overlap/budget edge-case coverage.

Review Change Stack

cemililik and others added 3 commits May 14, 2026 17:20
…ge + LoadError)

First commit of the T-019 task-loader chain (B4 milestone). Pure
type-level landing — no `load_image` function yet, no `unsafe`, no
audit-log entries. Subsequent commits land the preflight chain
(commit 2), AS creation + image-page loop (commit 3), rollback
machinery + stack loop (commit 4), and BSP wiring + smoke (commit 5)
per the T-019 §Approach plan agreed during ADR-0029's pre-Accept
review pass #1.

**`kernel/src/obj/task_loader.rs`** (new module):

- `LoadedImage` struct — 5 public fields (`as_cap`, `entry_va`,
  `stack_top_va`, `image_bytes`, `stack_bytes`) describing a freshly
  populated address space. `Copy + Clone + Debug + Eq + PartialEq`
  derives (all fields derive these; `CapHandle` and `VirtAddr` are
  both `Copy`). Field doc-comments name the invariants the loader
  upholds (half-open `[stack_base, stack_top_va)` range, tail-zeroing
  via UNSAFE-2026-0026's PMM zero-init contract, raw-flat offset-0
  entry-point convention).
- `LoadError` enum — 7 variants per the T-019 §Acceptance criteria
  taxonomy (`InvalidImage` / `InvalidStackSize` / `InvalidParentCap`
  / `FrameBudgetExceeded { needed, available }` /
  `AddressSpaceCreationFailed` / `OutOfFrames` / `MapFailed`).
  `Copy + Clone + Debug + Eq + PartialEq` derives + `#[non_exhaustive]`
  for forward-compat (future-state variants like `InvalidImageBaseVa`
  are foreseeable per B5+ per-task VA-range ADRs). Variant
  doc-comments cite the T-019 §Rollback contract section as the
  canonical reference for which path rolls back what.

- **Module-level scope-boundary note** explains why `LoadedImage` is
  intentionally NOT a `CapHandle{CapObject::Task(...)}` — kernel
  mappings in userspace AS + EL0 context + syscall entry are B5/B6
  prerequisites; the `task_create_from_image` wrapper lands then,
  per phase-b §B4 §Revision-notes.

- **Module placement decision (from T-019 pre-Accept #1 default):**
  `obj/task_loader.rs` (sibling to `obj/task.rs`) rather than
  `mm/task_loader.rs`. Rationale: the produced `LoadedImage` will
  feed a future `obj::task::create_from_image` wrapper, so the
  module belongs in the obj-side of the kernel.

**`kernel/src/obj/mod.rs`** — adds `pub mod task_loader;` + `pub use
task_loader::{LoadError, LoadedImage};` so callers reach the types
via `crate::obj::{LoadError, LoadedImage}`, matching the
`crate::obj::{Task, TaskHandle}` / `crate::obj::{Endpoint, ...}`
re-export pattern.

**Tests (5 new, all host-side):**

- `loaded_image_struct_literal_round_trips_through_copy_and_eq` —
  pins the public-struct-literal construction convention + `Copy`
  semantics + field-by-field shape. Uses a freshly-minted `CapHandle`
  from `CapabilityTable::insert_root` (the underlying cap object is
  an `Endpoint::test_handle(0, 0)` — irrelevant; the point is to
  construct a real `CapHandle` value).
- `loaded_image_distinguishes_different_field_values` — pins
  `PartialEq` honesty (no accidental wildcards in the struct
  definition).
- `load_error_variants_pattern_match_exhaustively` — pins the
  7-variant taxonomy. `#[non_exhaustive]` only forces external
  consumers to add a wildcard arm; within-crate matches retain
  compiler exhaustiveness checking, so adding an 8th variant breaks
  this test at compile time — strongest possible signal that the
  taxonomy changed.
- `load_error_variants_are_distinct` — pins `PartialEq` across the
  variant set (cross-variant + wrapped-error-different + same-variant-
  different-fields).
- `load_error_frame_budget_exceeded_fields_round_trip` — pins the
  `FrameBudgetExceeded { needed, available }` struct-variant shape.

**Gates: all clean.**

- `cargo fmt --all --check` clean.
- `cargo host-test` — 42 + 146 + 43 = 231 passed (was 226 at PR #30
  merge; +5 here, all in `obj::task_loader::tests`).
- `cargo host-clippy -D warnings` clean.
- `cargo kernel-clippy -D warnings` clean.
- `cargo kernel-build` clean.

No new `unsafe`; no audit-log entries. Next commit: preflight chain
(`load_image` signature + argument preflight + cap preflight + frame
budget preflight; reject-path host tests).

Refs: ADR-0028, ADR-0029

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… audit

`task_loader::load_image<M, N, R>` lands as the §Simulation-row 1–7
state machine: argument preflight → cap preflight → frame-budget
preflight → cap_create_address_space → image-page loop (USER|EXECUTE
+ copy_nonoverlapping byte copy + per-page tail-zeroing) → stack-page
loop (USER|WRITE) → LoadedImage return.

The image/stack loops are fallible mid-loop; the rollback helper
unwinds every committed mapping (cap_unmap + pmm.free_frame, reverse
order) plus the failing iteration's leaf frame, then cap_drops the
AS cap (leaf cap → cap_drop, NOT cap_revoke per T-019 §Rollback
contract). v1 baseline leaks the root L0 + intermediate L1/L2/L3 +
AS arena slot per the documented contract.

UNSAFE-2026-0027 — new audit entry for the post-PMM
copy_nonoverlapping site (semantically distant from
UNSAFE-2026-0026's PMM-internal zero-fill per justify-unsafe's
audit-tag scoping discipline). Pending QEMU smoke verification flips
to Active when commit 3 wires the BSP path.

Tests: 21 task_loader host tests covering every §Simulation row +
the rollback-contract mid-image-loop / mid-stack-loop / misaligned-VA
paths + the rollback helper's zero-pages cap_drop-only shape. Total
host-test count 231 → 247 (+16 new tests over commit 1's type-only
landing).

Gates: cargo fmt, cargo host-test, cargo host-clippy -D warnings,
cargo kernel-clippy -D warnings — all clean. cargo kernel-build
exercised. QEMU smoke comes with commit 3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ents

BSP wiring in `bsp-qemu-virt/src/main.rs`:
  - `USERSPACE_IMAGE` placeholder blob (`mov w0, #42; ret`,
    8 bytes) + `USERSPACE_IMAGE_BASE_VA` (0x0080_0000) +
    `USERSPACE_STACK_PAGES` (1) constants per ADR-0029
    §"Build pipeline (B4 / T-019 — placeholder blob)".
  - `load_image` invocation after the address-space-arena
    banner; new boot-line `tyrne: image loaded (entry = ...,
    sp = ..., image bytes N, stack bytes M, AS cap = idx K)`.
  - Reuses the existing `BOOTSTRAP_AS_TABLE` + `BOOTSTRAP_AS_CAP`
    + `AS_ARENA` + `MMU` + `PMM` statics; loaded AS cap lives in
    `BOOTSTRAP_AS_TABLE` slot 1.

Architecture doc: new `docs/architecture/task-loader.md`
chapter synthesising the loader sequence (§Simulation
rows 1–7) + rollback contract + v1 baseline leaks +
mapping flags + audit-log surface + test surface. Cross-
links added from `memory-management.md` §"Address-space
objects" (rider on T-019 composition) and `boot.md`
sequence diagram (loader step inserted between AS-arena
banner and GIC init).

Audit-log amendments — first runtime-evidence batch for
the post-bootstrap MMU/PMM paths:
  - UNSAFE-2026-0025 (`Mmu::map`/`unmap` page-table
    descriptor writes) lifted from `Pending QEMU smoke
    verification` via 2026-05-14 Amendment.
  - UNSAFE-2026-0026 (PMM `alloc_frame` zero-fill) lifted
    via 2026-05-14 Amendment.
  - UNSAFE-2026-0027 status note updated with the
    2026-05-14 smoke-trace evidence (entry stays Active
    standalone).

Roadmap: new 2026-05-14 banner records the T-019 3-commit
arc; Active task flips Draft → In Review; In review bucket
gains T-019. Task user-story `Status: Draft → In Review`
+ a 4th review-history row documenting the implementation
arc.

QEMU smoke (debug build, full demo to `tyrne: all tasks
complete`): new `tyrne: image loaded (entry = 0x800000;
sp = 0x802000; image bytes 8; stack bytes 4096; AS cap =
idx 1)` line lands in expected position; `-d
int,unimp,guest_errors` reports only the pre-existing 629
PL011-disabled-UART warnings (no new fault classes).
Tests at HEAD: 247/247 host-tests; cargo fmt --check
clean; cargo host-clippy / kernel-clippy -D warnings
clean; cargo kernel-build clean.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@qodo-code-review
Copy link
Copy Markdown

Qodo reviews are paused for this user.

Troubleshooting steps vary by plan Learn more →

On a Teams plan?
Reviews resume once this user has a paid seat and their Git account is linked in Qodo.
Link Git account →

Using GitHub Enterprise Server, GitLab Self-Managed, or Bitbucket Data Center?
These require an Enterprise plan - Contact us
Contact us →

Copy link
Copy Markdown

@sourcery-ai sourcery-ai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry @cemililik, you have reached your weekly rate limit of 500000 diff characters.

Please try again later or upgrade to continue using Sourcery

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 14, 2026

Warning

Rate limit exceeded

@cemililik has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 13 minutes and 29 seconds before requesting another review.

You’ve run out of usage credits. Purchase more in the billing tab.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

We recommend that you space out your commits to avoid hitting the rate limit.

🚦 How do rate limits work?

CodeRabbit enforces hourly rate limits for each developer per organization.

Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout.

Please see our FAQ for further information.

ℹ️ Review info
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 9bcd3d27-6ccd-4b79-90cb-a94ac9c3ac06

📥 Commits

Reviewing files that changed from the base of the PR and between 74694d4 and eb14c51.

📒 Files selected for processing (8)
  • bsp-qemu-virt/src/main.rs
  • docs/analysis/tasks/phase-b/T-019-task-loader.md
  • docs/architecture/task-loader.md
  • docs/decisions/0029-initial-userspace-image-format.md
  • hal/src/mmu/mod.rs
  • kernel/src/mm/mod.rs
  • kernel/src/mm/pmm.rs
  • kernel/src/obj/task_loader.rs
📝 Walkthrough

Walkthrough

Loads an embedded v1 userspace blob into a new address space via task_loader::load_image: precise preflights (alignment, VA bounds, exact frame budgeting, PA-overlap), allocation/mapping with rollback on mid-loop failures, PMM helpers and test injection, BSP smoke invocation, and updated docs/audits/roadmap.

Changes

T-019 Task Loader Implementation

Layer / File(s) Summary
Memory management helpers
kernel/src/mm/mod.rs, kernel/src/mm/pmm.rs
Adds phys_frame_kernel_ptr for kernel-frame pointers, Pmm::could_yield_pa_overlapping for defensive PA-overlap queries, and test-only alloc-failure injection to drive rollbacks.
Task loader API & types
kernel/src/obj/task_loader.rs
Defines intermediate_frame_count, USERSPACE_VA_LIMIT, LoadedImage descriptor, and LoadError enum with alignment/VA-range/overlap/budget/map failure variants.
Core load_image & rollback
kernel/src/obj/task_loader.rs
Implements staged preflights (misaligned base, VA bounds, exact intermediate-frame budget, PA-overlap), address-space creation, image/stack allocation, unsafe copy and cap_map calls, and a rollback helper that unmaps/frees on mid-loop failures.
Comprehensive test suite
kernel/src/obj/task_loader.rs (#[cfg(test)])
Host-side fakes and injection tests covering preflight rejections, intermediate-frame accounting, PA-overlap regressions, mapping flags, tail-zeroing, and rollback semantics.
Module exports and BSP boot smoke
kernel/src/obj/mod.rs, bsp-qemu-virt/src/main.rs
Re-exports task_loader types; BSP boot-phase smoke embeds a placeholder image, calls load_image, and prints returned metadata (entry VA, stack-top VA, image/stack byte counts, AS cap index).
Spec, audits, and ADRs
docs/analysis/tasks/phase-b/T-019-task-loader.md, docs/audits/unsafe-log.md, docs/decisions/0029-*.md
Moves T-019 to In Review, updates LoadError with Misaligned/InvalidBase/ImageOverlapsAllocatableMemory, rewrites simulation/rollback rows, adds UNSAFE-2026-0027 for byte-copy invariants, and syncs placeholder blob bytes.
Architecture docs & roadmap
docs/architecture/task-loader.md, docs/architecture/boot.md, docs/architecture/memory-management.md, docs/roadmap/current.md
Adds task-loader chapter, documents boot-time smoke step (NOT executed), ties first runtime Pmm/Mmu exercise to T-019, and updates roadmap status and next-step planning.

Sequence Diagram(s)

sequenceDiagram
  participant BSP as BSP (kernel_entry)
  participant load_image as task_loader::load_image
  participant Pmm as Pmm
  participant CapTable as CapabilityTable
  participant Mmu as Mmu
  BSP->>load_image: call load_image(image, image_base_va, stack_pages, ...)
  load_image->>load_image: preflight (align, VA bounds, frame budget)
  load_image->>Pmm: could_yield_pa_overlapping(image PA range)
  load_image->>CapTable: cap_create_address_space(parent_as_cap)
  load_image->>Pmm: alloc_frame() for image pages
  load_image->>load_image: copy_nonoverlapping -> phys_frame_kernel_ptr(dst)
  load_image->>Mmu: cap_map(image page, USER|EXECUTE)
  load_image->>Pmm: alloc_frame() for stack pages
  load_image->>Mmu: cap_map(stack page, USER|WRITE)
  alt mapping/allocation failure
    load_image->>Mmu: unmap committed pages (rollback)
    load_image->>Pmm: free returned frames
    load_image->>CapTable: drop AS cap
  else success
    load_image->>BSP: return LoadedImage (as_cap, entry_va, stack_top_va, byte counts)
  end
Loading

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~60 minutes

Possibly related PRs

  • cemililik/Tyrne#28: BSP address-space scaffolding (BOOTSTRAP_AS_CAP/BOOTSTRAP_AS_TABLE) that T-019 builds upon.
  • cemililik/Tyrne#23: Prior boot ordering/MMU setup changes that affect where the loader smoke runs.
  • cemililik/Tyrne#26: PMM bring-up and alloc semantics changes used by the task-loader (alloc/query integration).

Poem

🐰 I hopped a blob into a brand-new space,

with checks and rollbacks in careful place.
Pages aligned, the PMM gave room,
a tiny userspace bud began to bloom,
B4's trail marked with a rabbit's trace.

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The PR title accurately summarizes the main change: implementing T-019 task loader with load_image function, BSP QEMU smoke integration, and UNSAFE-2026-0027 audit logging.
Docstring Coverage ✅ Passed Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch t-019-task-loader

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

Copy link
Copy Markdown

@gemini-code-assist gemini-code-assist Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code Review

This pull request implements the task loader (T-019), enabling the loading of raw-flat userspace images into new address spaces with allocated stacks. It includes the task_loader module, extensive documentation, and BSP wiring for smoke testing. Feedback highlights opportunities to improve portability by abstracting physical-to-virtual address conversion, enhance robustness with VA range overflow checks, and avoid potential fragility by explicitly defining required capability rights in the smoke test.

Comment thread kernel/src/obj/task_loader.rs Outdated
// [audit]: https://github.com/cemililik/Tyrne/blob/main/docs/audits/unsafe-log.md
unsafe {
let src = chunk.as_ptr();
let dst = frame.as_usize() as *mut u8;
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The cast from usize (physical address) to *mut u8 relies on the identity mapping invariant of the v1 kernel. While this is documented in the audit log, it makes the code less portable to future high-half kernel designs. Consider introducing a phys_to_virt helper or using a HAL-provided method to materialise the pointer, which would centralise the identity-mapping assumption.

Comment on lines +518 to +522
let stack_top_va = VirtAddr(
stack_base_va
.0
.saturating_add(stack_pages.saturating_mul(PAGE_SIZE)),
);
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The stack_top_va calculation uses saturating_add. If the stack region overflows the 64-bit address space (or the 48-bit userspace range), stack_top_va will saturate to usize::MAX. This value is not page-aligned and does not accurately represent 'one-past-the-highest' mapped address in an overflow scenario. A preflight check for the total VA range [image_base_va, stack_top_va) against the architected userspace VA bounds would be more defensive.

Comment thread bsp-qemu-virt/src/main.rs
table,
arena,
parent_cap,
CapRights::empty(),
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The smoke test passes CapRights::empty() for the new address space. If cap_map or cap_unmap (called during rollback) enforce specific rights (e.g., CapRights::MAP), the loader will fail. While the smoke test currently passes, this suggests either a lack of rights enforcement in the capability wrappers or a potential fragility if enforcement is added later. Passing a minimal set of required rights (e.g., CapRights::MAP | CapRights::UNMAP) would be more robust.

cemililik and others added 2 commits May 15, 2026 09:58
Address 4 findings from PR #31 review-round 1 (2 reviewer passes;
R1: P2 + P3 + P2; R2: P1 + P2 + P3 + P3; overlap on stale dead-code
allow + missing test names).

**P1 (R2 F1) — `load_image` non-overlap precondition runtime-enforced.**
The safe `load_image` API's `copy_nonoverlapping` non-overlap invariant
was previously upheld at the BSP-wiring layer (`.rodata` ⊆ PMM-reserved
range per ADR-0027 + ADR-0035); the type system did not enforce it. Fix:
new `pub fn Pmm::could_yield_pa_overlapping(pa_range)` query + new
§Simulation row 4 preflight in `load_image` (`image.as_ptr() as usize`
→ PA range under v1 identity-mapped kernel AS per ADR-0027) + new
`LoadError::ImageOverlapsAllocatableMemory` variant. Per-call invariant
now runtime-enforced; BSP-layout discipline remains the production
reality but is no longer the load-bearing soundness argument.
UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording the change.

**P2 (R1 F3 / R2 F2) — missing OutOfFrames rollback test.** Added
`task_loader::tests::rolls_back_on_pmm_exhausted_mid_image_loop` driven
by a new `#[cfg(test)] pub(crate) fn Pmm::force_alloc_failure_after`
injection hook (cleaner than a Pmm decorator since `Pmm` is a concrete
generic, not a trait). Pins the defensive `LoadError::OutOfFrames`
rollback path that is structurally unreachable in v1 post-FrameBudget
preflight but lives in the code for forward-concurrency scenarios.
§Simulation table refreshed to actual test names: row 2 names the split
`rejects_invalid_parent_cap_lookup` + `_wrong_kind`; row 5 names
`returns_loaded_image_with_correct_metadata` (no
`creates_fresh_as_via_cap_create_address_space` ever existed).

**P3 (R1 F1 / R2 F3) — stale `#[allow(dead_code)]` on BOOTSTRAP_AS_CAP.**
The cap is now read by T-019's BSP wiring as the loader's `parent_as_cap`
(`main.rs:988`); attribute + comment removed and replaced with a "Live
as of T-019" doc comment.

**P3 (R1 F2) — placeholder byte sequence decoded wrong.** `[0x40, 0x00,
0x80, 0xd2, ...]` LE word 0 = `0xd2800040` = `MOVZ x0, #2` (sf=1 → 64-bit
MOVZ), not the documented `mov w0, #42`. Corrected to `[0x40, 0x05,
0x80, 0x52, ...]` (LE word 0 = `0x52800540` = correct `MOVZ w0, #42`)
in all 4 sites (BSP, ADR-0029 ×2, T-019 user-story ×2, architecture
chapter). Placeholder is not executed in B4 so the prior encoding was
non-functional, but documented intent now matches the bytes.

**P3 (R2 F4) — `current.md` stale "Next task to open: T-019".** T-019
is already In Review per the same file's banner; replaced with B4-closure
+ B5 syscall-ABI ADR pair (ADR-0030 + ADR-0031) wording.

Pipeline narrative reflows from 7 to 8 steps (new row 4 preflight);
`LoadError` variant count from 7 to 8. `docs/architecture/task-loader.md`
Mermaid diagram + pipeline text + test surface list updated; T-019
user-story §Simulation table + §Rollback contract + §Acceptance criteria
LoadError list + Review history all updated.

Tests at HEAD: **250/250** host-test count (+3 from 247: 2 overlap-
preflight tests + 1 OutOfFrames rollback test). All gates clean:
`cargo fmt --check`, `cargo host-test`, `cargo host-clippy -D warnings`,
`cargo kernel-clippy -D warnings`, `cargo kernel-build`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Address PR #31 review-round 2 (3 gemini-code-assist findings, all P2).
Two valid fixes, one reject-with-documentation.

**(F1, P2) — `task_loader.rs:479` destination cast portability.**
The `dst = frame.as_usize() as *mut u8` cast in the image-page loop
now routes through a new public kernel helper
`crate::mm::phys_frame_kernel_ptr` (located in `kernel/src/mm/mod.rs`).
Centralises v1's identity-mapping invariant per ADR-0027 §Decision
outcome (a) so the future ADR-0033 high-half migration replaces one
helper body instead of every kernel-side caller. The cast itself is
safe Rust (integer-to-pointer cast); only the dereference at
`copy_nonoverlapping`'s call site is `unsafe` and is covered by
UNSAFE-2026-0027's existing safety argument. The PMM zero-fill site
(UNSAFE-2026-0026) is intentionally NOT migrated in this commit —
its existing inline doc-comment already names the future-migration
plan; both adopters update at the ADR-0033 commit per the
audit-entry append-only discipline. UNSAFE-2026-0027 gained a
2026-05-15 Amendment recording the helper introduction.

**(F2, P2) — `task_loader.rs:569` `stack_top_va` saturating overflow.**
§Simulation row 3 now bundles a VA-range preflight alongside the
existing frame-budget check:
  image_base_va.saturating_add((image_pages + stack_pages) * PAGE_SIZE)
    <= USERSPACE_VA_LIMIT
where `USERSPACE_VA_LIMIT = 1 << 48` per ADR-0027's
`TCR_EL1.T0SZ = 16`. Pre-fix, an `image_base_va` near `usize::MAX`
would silently saturate `stack_top_va` to `usize::MAX` (not page-
aligned, not a meaningful "one-past-the-highest" address); post-fix,
the row 3 preflight rejects with new variant
`LoadError::InvalidImageBaseVa { base, end }` (with
`end == VirtAddr(usize::MAX)` as the documented sentinel for the
saturated path) before any state change. `LoadError` variant count
flips 8 → 9. Three new host tests pin the contract:
  - `rejects_image_base_va_past_userspace_va_limit` (base above limit)
  - `rejects_image_base_va_saturating_overflow` (saturated-end sentinel)
  - `accepts_image_base_va_exactly_at_userspace_va_limit_minus_span`
    (half-open `end == USERSPACE_VA_LIMIT` boundary is permitted)

**(F3, P2) — `main.rs:997` `CapRights::empty()` for BSP smoke.**
Reject-with-documentation. v1's cap-rights model is **kind-only**,
not per-operation (per `resolve_address_space_cap`'s doc-comment in
`kernel/src/mm/address_space.rs`); the `CapRights` enum
(`kernel/src/cap/rights.rs`) accordingly exposes only
`DUPLICATE / DERIVE / REVOKE / TRANSFER / SEND / RECV / NOTIFY` —
there is no `MAP` / `UNMAP` bit defined to pass. The BSP smoke call
site gained a multi-line comment recording the v1 contract + the
additive-update path that lands with the future per-operation
rights ADR (B5+). UNSAFE-2026-0027's Amendment also documents the
rejection rationale.

Docs: `docs/architecture/task-loader.md` row-3 pipeline narrative
extended with the VA-range check + test surface list refreshed.
T-019 user-story §Simulation table row 3 + §Acceptance criteria
LoadError list updated; new review-history row records this round.

Tests at HEAD: **253/253** (was 250, +3 from the F2 VA-range tests).
All gates clean: cargo fmt --check, cargo host-test,
cargo host-clippy -D warnings, cargo kernel-clippy -D warnings,
cargo kernel-build. QEMU smoke byte-stable — full demo through
`tyrne: all tasks complete`; `-d int,unimp,guest_errors` reports
only the pre-existing 629 PL011-disabled-UART warnings.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Review-round 2 (gemini-code-assist line-level) addressed in commit 164522d. All 3 findings handled:

F1 (P2) — task_loader.rs:479 destination cast portability. ✅ Fixed. New public kernel helper crate::mm::phys_frame_kernel_ptr(PhysFrame) -> *mut u8 in kernel/src/mm/mod.rs centralises v1's identity-mapping invariant per ADR-0027 §Decision outcome (a); the load_image byte-copy site now routes through it. Future ADR-0033 high-half migration updates one helper body instead of every kernel-side caller. The PMM zero-fill site (UNSAFE-2026-0026) is intentionally NOT migrated in the same commit — its existing inline doc-comment already names the future-migration plan; both adopters update at the ADR-0033 commit per the audit-entry append-only discipline. UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording the helper introduction.

F2 (P2) — task_loader.rs:569 stack_top_va saturating overflow. ✅ Fixed. §Simulation row 3 now bundles a VA-range preflight: image_base_va.saturating_add((image_pages + stack_pages) * PAGE_SIZE) <= USERSPACE_VA_LIMIT (= 1 << 48 per ADR-0027 TCR_EL1.T0SZ = 16). New variant LoadError::InvalidImageBaseVa { base, end } (with end == VirtAddr(usize::MAX) as the documented sentinel for the saturated path). Three new host tests pin the contract: rejects_image_base_va_past_userspace_va_limit, rejects_image_base_va_saturating_overflow, accepts_image_base_va_exactly_at_userspace_va_limit_minus_span (half-open end == USERSPACE_VA_LIMIT boundary is permitted).

F3 (P2) — main.rs:997 CapRights::empty() for BSP smoke. ❌ Rejected with documentation. v1's cap-rights model is kind-only, not per-operation (per resolve_address_space_cap's doc-comment in kernel/src/mm/address_space.rs); the CapRights enum (kernel/src/cap/rights.rs) accordingly exposes only DUPLICATE / DERIVE / REVOKE / TRANSFER / SEND / RECV / NOTIFY — there is no MAP / UNMAP bit defined to pass. The suggested CapRights::MAP | CapRights::UNMAP does not compile against v1. The BSP smoke call site gained a multi-line comment recording the v1 contract + the additive-update path that lands with the future per-operation rights ADR (B5+); UNSAFE-2026-0027's Amendment also documents the rejection rationale.

Tests at HEAD 164522d: 253/253 (+3 from the F2 VA-range tests; baseline 250 → 253). All gates clean: cargo fmt --check, cargo host-test, cargo host-clippy -D warnings, cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke byte-stable — full demo through tyrne: all tasks complete; -d int,unimp,guest_errors reports only the pre-existing 629 PL011-disabled-UART warnings.

@cemililik
Copy link
Copy Markdown
Collaborator Author

@coderabbitai full review

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 15, 2026

✅ Actions performed

Full review triggered.

Address PR #31 review-round 3 (5 findings: 4 × P2 + 1 × P3). Two
substantive contract fixes + 3 documentation syncs. No change to the
audited unsafe operation; both substantive fixes harden the safe-API
boundary in front of it.

**(F1, P2) — Frame-budget intermediate-frame undercount.** The
previous `pub const INTERMEDIATE_FRAME_BUDGET: usize = 6` claimed a
"safe upper bound" but undercounted whenever the image span crossed
more than one 2 MiB L2 slot — each additional 2 MiB boundary requires
one extra L3 page-table frame. Worked example surfaced by review:
8 MiB image at VA `0x0080_0000` covers L2 slots 4–7 (4 distinct) +
a 1-page stack lands in slot 8 = 5 distinct L3 tables + 1 L2 + 1 L1
= **7 intermediates, not 6**. Under the old constant a budget
preflight would have returned `Ok` for a request that, on commit,
would have run out of intermediate frames mid-`cap_map` and surfaced
as `LoadError::MapFailed(MmuMapError(OutOfFrames))` — rollback still
correct but the public `LoadError` taxonomy drifted from the
§Simulation row-3 promise.

Fix: removed `INTERMEDIATE_FRAME_BUDGET`; introduced
`pub fn intermediate_frame_count(image_base_va, image_pages,
stack_pages) -> usize` that walks the VMSAv8 4-level index
decomposition (shifts 21/30/39) to produce the **exact** distinct-
table count via
  `(last_byte >> shift) - (start >> shift) + 1`
at each level. Image and stack are contiguous by construction so the
combined span's distinct-slot count at each level is a closed range,
and dedup is trivial.

Five helper unit tests pin the contract:
  - intermediate_frame_count_minimal_single_l2_slot (= 3)
  - intermediate_frame_count_8mib_image_one_stack_page_crosses_five_l2
    (regression for reviewer's example; = 7)
  - intermediate_frame_count_l1_boundary_crossing (= 5)
  - intermediate_frame_count_zero_span_defensive
  - intermediate_frame_count_saturated_total_pages

**(F2, P2) — VA-range overflow shadowed by frame-budget.** Pre-fix,
§Simulation row 3 ran frame-budget first. A saturated request like
`image = &[1], stack_size_pages = usize::MAX` caused `needed` to
saturate to `usize::MAX` and triggered `FrameBudgetExceeded` instead
of the documented `InvalidImageBaseVa { end: VirtAddr(usize::MAX) }`
sentinel.

Fix: row 3 now runs VA-range check first, then frame-budget. New
regression test `va_range_preflight_runs_before_frame_budget` pins
the order: a saturated `stack_size_pages = usize::MAX` returns
`InvalidImageBaseVa`, not `FrameBudgetExceeded`.

**(F3, P2) — `docs/roadmap/current.md` stale.** Banner refreshed
to reflect HEAD: 6 commits, 259/259 tests, 9-variant `LoadError`,
PR #31 In Review.

**(F4, P2) — `docs/architecture/memory-management.md` misattribution.**
Corrected the §"Address-space objects" / §"FrameProvider integration"
attribution: T-018 installed the AS-object surface but does NOT call
`Pmm::alloc_frame` at runtime (BSP wraps the live `.boot_pt` L0 via
`wrap_bootstrap`; no `Mmu::create_address_space` per ADR-0028
§Simulation row 0). T-019 is the first runtime exerciser of
`Pmm::alloc_frame`, `cap_create_address_space`, post-bootstrap
`Mmu::map`, and accordingly the first runtime exerciser of
UNSAFE-2026-0025, 0026, and 0027 (the latter newly introduced by
T-019).

**(F5, P3) — Minor doc counter/prose drift.**
  - docs/architecture/task-loader.md test count `24 → 33`
  - docs/architecture/boot.md stage-3 prose now mentions the
    `task_loader::load_image` step (Mermaid sequence already had
    it; prose was inconsistent)

UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording the F1+F2
fixes (the audit's invariant (4) "source and destination do not
overlap" is unchanged; both fixes are about resource accounting and
preflight ordering, not the byte-copy site).

Tests at HEAD: **259/259** (was 253 at commit 5; +6 from F1's five
helper unit tests + F2's reorder regression test). All gates clean:
cargo fmt --check, cargo host-test, cargo host-clippy -D warnings,
cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke
byte-stable — full demo through `tyrne: all tasks complete`;
`-d int,unimp,guest_errors` reports only the pre-existing 629
PL011-disabled-UART warnings.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Review-round 3 addressed in commit 5b1f153. All 5 findings handled (4 × P2 substantive + 1 × P3 doc).

F1 (P2) — intermediate-frame budget undercount. ✅ Fixed. Removed the hard-coded pub const INTERMEDIATE_FRAME_BUDGET: usize = 6 (which under-counted for image spans crossing > 1 L2 slot); introduced pub fn intermediate_frame_count(image_base_va, image_pages, stack_pages) -> usize that walks VMSAv8 4-level index decomposition (shifts 21/30/39) for an exact distinct-table count. The reviewer's 8 MiB image example now yields exactly 7 intermediates (1 L1 + 1 L2 + 5 L3) as expected. Five helper unit tests pin the contract: _minimal_single_l2_slot (= 3), _8mib_image_one_stack_page_crosses_five_l2 (regression for reviewer's example; = 7), _l1_boundary_crossing (= 5), _zero_span_defensive, _saturated_total_pages.

F2 (P2) — VA-range overflow shadowed by frame-budget. ✅ Fixed. Reordered §Simulation row 3 to run VA-range check first, then frame-budget. New regression test va_range_preflight_runs_before_frame_budget pins the order: image = &[0xAA], stack_size_pages = usize::MAX now returns InvalidImageBaseVa { end: VirtAddr(usize::MAX) } (the documented saturated sentinel) instead of being masked by FrameBudgetExceeded.

F3 (P2) — current.md stale. ✅ Fixed. Banner refreshed: 6-commit arc ending at 5b1f153, 259/259 tests, full 9-variant LoadError taxonomy listed (including InvalidImageBaseVa + ImageOverlapsAllocatableMemory), PR #31 In Review.

F4 (P2) — memory-management.md misattribution. ✅ Fixed. Corrected the §"Address-space objects" / §"FrameProvider integration" attribution: T-018 installs the AS-object surface but uses wrap_bootstrap on the live .boot_pt L0 (per ADR-0028 §Simulation row 0); T-019 is the first runtime exerciser of Pmm::alloc_frame + cap_create_address_space + post-bootstrap Mmu::map, and accordingly of UNSAFE-2026-0025 / 0026 / 0027.

F5 (P3) — Minor counter/prose drift. ✅ Fixed. docs/architecture/task-loader.md test count 24 → 33; docs/architecture/boot.md stage-3 prose now mentions the task_loader::load_image step (Mermaid already had it).

UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording the F1+F2 contract fixes (the audited unsafe operation is unchanged — both fixes harden the safe-API boundary in front of it). T-019 user-story §Simulation row 3 rewritten to reflect the new ordering + exact-count budget; new review-history row records this round.

Tests at HEAD 5b1f153: 259/259 (was 253, +6: F1's 5 helper unit tests + F2's reorder regression test). All gates clean: cargo fmt --check, cargo host-test, cargo host-clippy -D warnings, cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke byte-stable — full demo through tyrne: all tasks complete; -d int,unimp,guest_errors reports only the pre-existing 629 PL011-disabled-UART warnings.

Address PR #31 review-round 4 (3 findings: 1 × P2 + 2 × P3). The P2
fix closes a preventable PMM frame leak path; the two P3 fixes
tighten test determinism + doc-comment accuracy. No change to the
audited unsafe operation; all three fixes harden the safe-API
boundary in front of it.

**(F1, P2) — Preventable root-frame leak on misaligned image_base_va.**
Pre-fix, an unaligned `image_base_va` surfaced as
`MmuError::MisalignedAddress` from the first cap_map call inside the
image-page loop — but by that point cap_create_address_space had
already allocated the root L0 frame, which then leaked via the v1
baseline rollback. The existing test
`rolls_back_on_misaligned_image_base_va` *asserted* this leak
(`pmm.stats().free_frames == pmm_before - 1`), accepting it as the
documented v1 trade-off, but the leak is preventable by argument
validation.

Fix: row 1's argument preflight now checks
`image_base_va.0.is_multiple_of(PAGE_SIZE)` and rejects with new
variant `LoadError::MisalignedImageBaseVa(VirtAddr)` before any
cap_create_address_space invocation — PMM byte-stable on rejection
(no root-frame leak). The renamed test
`rejects_misaligned_image_base_va_with_pmm_byte_stable` now asserts
`pmm.stats().free_frames == pmm_before`. The
`rejects_image_base_va_saturating_overflow` test was retargeted from
`VirtAddr(usize::MAX - PAGE_SIZE)` (unaligned, now intercepted by
row 1) to `VirtAddr(usize::MAX & !(PAGE_SIZE - 1))` (page-aligned)
so the row-3 saturating-overflow path remains testable.

`LoadError` taxonomy grows 9 → 10 variants. The exhaustiveness
regression test (`load_error_variants_pattern_match_exhaustively`)
is updated and would compile-fail if the new variant is silently
removed. Distinctness test gained 2 sub-cases asserting
`MisalignedImageBaseVa(_)` is distinct from itself with different
VAs + distinct from `InvalidImageBaseVa { base, end }` even when
the base matches.

**(F2, P3) — Non-deterministic `accepts_image_disjoint_from_pmm_extent`
test.** Pre-fix, the test used a heap-allocated `Vec<u8>` for the
image and silently `return`-ed (passing without asserting) when the
host allocator happened to place the Vec inside the PMM-extent
host-backing region.

Fix: switched to a `.rodata`-resident `static DISJOINT_RODATA_IMAGE:
[u8; 8]`. Disjointness from the heap-backed PMM extent is now
structurally guaranteed (`.rodata` and heap are in different
segments); the prior silent-skip `if {...} return` is replaced with
a hard `assert!` that fail-loudly if `.rodata` ever lands inside the
PMM extent (toolchain regression signal). Also mirrors the
production BSP wiring shape (`static USERSPACE_IMAGE: &[u8] = ...`).

**(F3, P3) — Stale `LoadError::FrameBudgetExceeded` doc-comment.**
The variant's doc-comment still said "intermediate_budget = 6 is
the safe upper bound..." after the F1-of-round-3 fix replaced the
constant with an exact-count helper.

Fix: refreshed to reference `intermediate_frame_count(...)` with a
back-reference to round-3 Finding 1's rationale.

UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording all three
fixes (the audited unsafe operation is unchanged; F1 eliminates an
internal-API-misuse PMM leak path, F2+F3 are test/doc hardening in
front of the byte-copy site).

Docs updated: T-019 §Acceptance criteria LoadError list, §Simulation
row 1 (alignment check added + test rename), new review-history row;
arch chapter row 1 test surface list refreshed; `current.md` banner
+ active-task paragraph updated for 7-commit arc, 10-variant
`LoadError`.

Tests at HEAD: **259/259** (no net new tests; round 4 reframes the
misaligned-VA test rather than adding new ones, the distinctness
assertion gained 2 sub-cases inside an existing test, and the
disjoint test's `assert!` replaces the prior `return` skip path).
All gates clean: cargo fmt --check, cargo host-test,
cargo host-clippy -D warnings, cargo kernel-clippy -D warnings,
cargo kernel-build. QEMU smoke byte-stable — full demo through
`tyrne: all tasks complete`; `-d int,unimp,guest_errors` reports
only the pre-existing 629 PL011-disabled-UART warnings.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Review-round 4 addressed in commit 95efd62. All 3 findings handled (1 × P2 + 2 × P3).

P2 — Preventable root-frame leak on misaligned image_base_va. ✅ Fixed. Row 1's argument preflight now checks image_base_va.0.is_multiple_of(PAGE_SIZE) and rejects with new variant LoadError::MisalignedImageBaseVa(VirtAddr) before any cap_create_address_space invocation. The renamed test rejects_misaligned_image_base_va_with_pmm_byte_stable asserts pmm.stats().free_frames == pmm_before (no root-frame leak). The rejects_image_base_va_saturating_overflow test was retargeted from VirtAddr(usize::MAX - PAGE_SIZE) (unaligned, now intercepted by row 1) to VirtAddr(usize::MAX & !(PAGE_SIZE - 1)) (page-aligned) to preserve the row-3 saturating-overflow coverage. LoadError taxonomy: 9 → 10 variants; exhaustiveness regression test would compile-fail if the variant is silently removed.

P3 #1 — Non-deterministic accepts_image_disjoint_from_pmm_extent test. ✅ Fixed. Switched to a .rodata-resident static DISJOINT_RODATA_IMAGE: [u8; 8]; disjointness from the heap-backed PMM extent is structurally guaranteed. The silent-skip if {...} return replaced with a hard assert! that fail-loudly on toolchain regression. Also mirrors the production BSP wiring shape.

P3 #2 — Stale LoadError::FrameBudgetExceeded doc-comment. ✅ Fixed. Refreshed from "intermediate_budget = 6 is the safe upper bound..." (stale since round-3 F1) to a reference to the exact intermediate_frame_count(...) helper.

UNSAFE-2026-0027 gained a 2026-05-15 Amendment recording all three fixes (the audited unsafe operation is unchanged; P2 closes an internal-API-misuse PMM leak path; P3s harden test/doc accuracy in front of the byte-copy site).

Tests at HEAD 95efd62: 259/259 (no net new tests — round 4 reframes the misaligned-VA test rather than adding new ones; the distinctness assertion gained 2 sub-cases inside an existing test; the disjoint test's assert! replaces the prior return skip path). All gates clean: cargo fmt --check, cargo host-test, cargo host-clippy -D warnings, cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke byte-stable — full demo through tyrne: all tasks complete; -d int,unimp,guest_errors reports only the pre-existing 629 PL011-disabled-UART warnings.

@cemililik
Copy link
Copy Markdown
Collaborator Author

@coderabbitai full review

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 15, 2026

✅ Actions performed

Full review triggered.

Copy link
Copy Markdown

@coderabbitai coderabbitai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 5

🧹 Nitpick comments (1)
kernel/src/mm/mod.rs (1)

96-140: 💤 Low value

Forward-compat doc snippet uses .expect(...) which is denied in this crate.

The forward-compat note at line 122 sketches the future high-half body as KERNEL_PHYS_BASE.checked_add(frame.as_usize()).expect(...). Per the existing crate convention clippy::expect_used is denied, so a future maintainer copying this verbatim would hit a lint failure. Consider rephrasing the example to use unwrap_or(...) with a sentinel or a debug_assert!-guarded path so the doc-suggested form is lint-clean when ADR-0033 lands.

Based on learnings: "In the Tyrne kernel crate (Rust files under kernel/src/), avoid using .expect() (clippy lint clippy::expect_used is denied)."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@kernel/src/mm/mod.rs` around lines 96 - 140, The forward-compat doc for
phys_frame_kernel_ptr suggests using
KERNEL_PHYS_BASE.checked_add(frame.as_usize()).expect(...), which violates the
crate's denied clippy::expect_used; update the doc example to show a lint-clean
alternative (e.g. use checked_add(...).unwrap_or(fallback) or
checked_add(...).unwrap_or_else(|| { debug_assert!(false, "..."); fallback }) or
perform a debug_assert! before an unwrap) so future maintainers copying the
example won't introduce .expect(); mention KERNEL_PHYS_BASE and ADR-0033 in the
revised snippet.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@bsp-qemu-virt/src/main.rs`:
- Around line 977-983: Update the existing safety comment for the new unsafe
block that manipulates PMM, MMU, AS_ARENA, BOOTSTRAP_AS_TABLE and
BOOTSTRAP_AS_CAP: explicitly state (a) why unsafe is required (e.g., temporarily
creating &mut aliases to just-initialized static storage and performing
low-level initialization steps that the compiler cannot prove safe), (b) the
exact invariants being upheld (single-core/cooperative context, initialization
order guarantees, momentary scope-limited &mut borrows that do not cross
scheduler start, and references to audit IDs UNSAFE-2026-0010 and
UNSAFE-2026-0014), and (c) why a safer alternative was rejected (e.g., boxing or
runtime-checked wrappers would add unacceptable boot-time dynamic overhead or
cannot express the required initialization ordering/aliasing constraints). Keep
it brief and tied to the named symbols (PMM, MMU, AS_ARENA, BOOTSTRAP_AS_TABLE,
BOOTSTRAP_AS_CAP) so reviewers can verify the invariants.

In `@docs/analysis/tasks/phase-b/T-019-task-loader.md`:
- Around line 91-92: The Markdown table cells containing the flag expressions
`USER|EXECUTE` and `USER|WRITE` are being parsed as column separators; update
those occurrences (near the row that references
`task_loader::tests::maps_image_pages_with_user_execute_flags` and
`task_loader::tests::maps_stack_with_user_write_flags`) to escape the pipe
characters (e.g., change `USER|EXECUTE` -> `USER\|EXECUTE` and `USER|WRITE` ->
`USER\|WRITE`) or wrap them in inline code backticks to prevent them being
treated as table delimiters.

In `@docs/architecture/task-loader.md`:
- Line 153: Replace the outdated test name
rolls_back_on_misaligned_image_base_va with the renamed test identifier
rejects_misaligned_image_base_va_with_pmm_byte_stable in the rollback contract
list so the document consistently references
rejects_misaligned_image_base_va_with_pmm_byte_stable alongside the other
rollback tests (e.g., rolls_back_on_cap_map_failure_mid_image_loop,
rolls_back_on_pmm_exhausted_mid_image_loop,
rolls_back_on_cap_map_failure_mid_stack_loop,
rollback_helper_zero_pages_only_drops_cap).

In `@docs/roadmap/current.md`:
- Line 7: Update the banner's HEAD placeholder in the docs/roadmap/current.md
entry that begins "**2026-05-15 update — T-019 implementation In Review on PR
`#31`; branch `t-019-task-loader`**" by replacing the literal HEAD `<TBD>` token
with the actual final commit SHA for the HEAD commit (the commit referenced as
"HEAD `<TBD>`" in the 7-commit list), ensuring the commit SHA is the one created
in the final review-round commit before merging.

In `@kernel/src/obj/mod.rs`:
- Around line 35-40: The module-level rustdoc for the obj module is now out of
date because task_loader (pub mod task_loader and the exported types LoadError
and LoadedImage) was made public; update the doc comment at the top of mod.rs to
mention the new task_loader surface, remove or revise the claim that "all v1
code here is safe Rust" if it no longer holds, and briefly describe the four
public kinds (Endpoint, Notification, Task, and the task_loader API) so the
top-level docs for tyrne_kernel::obj accurately reflect the exported symbols
Endpoint/EndpointArena/EndpointHandle,
Notification/NotificationArena/NotificationHandle, Task/TaskArena/TaskHandle,
and task_loader::{LoadError, LoadedImage}.

---

Nitpick comments:
In `@kernel/src/mm/mod.rs`:
- Around line 96-140: The forward-compat doc for phys_frame_kernel_ptr suggests
using KERNEL_PHYS_BASE.checked_add(frame.as_usize()).expect(...), which violates
the crate's denied clippy::expect_used; update the doc example to show a
lint-clean alternative (e.g. use checked_add(...).unwrap_or(fallback) or
checked_add(...).unwrap_or_else(|| { debug_assert!(false, "..."); fallback }) or
perform a debug_assert! before an unwrap) so future maintainers copying the
example won't introduce .expect(); mention KERNEL_PHYS_BASE and ADR-0033 in the
revised snippet.
🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 72c3d158-413b-4dfa-953a-759cbcc32c3c

📥 Commits

Reviewing files that changed from the base of the PR and between e09755d and 95efd62.

📒 Files selected for processing (12)
  • bsp-qemu-virt/src/main.rs
  • docs/analysis/tasks/phase-b/T-019-task-loader.md
  • docs/architecture/boot.md
  • docs/architecture/memory-management.md
  • docs/architecture/task-loader.md
  • docs/audits/unsafe-log.md
  • docs/decisions/0029-initial-userspace-image-format.md
  • docs/roadmap/current.md
  • kernel/src/mm/mod.rs
  • kernel/src/mm/pmm.rs
  • kernel/src/obj/mod.rs
  • kernel/src/obj/task_loader.rs

Comment thread bsp-qemu-virt/src/main.rs Outdated
Comment thread docs/analysis/tasks/phase-b/T-019-task-loader.md Outdated
Comment thread docs/architecture/task-loader.md Outdated
Comment thread docs/roadmap/current.md Outdated
Comment thread kernel/src/obj/mod.rs
Six valid review nits surfaced after commit 95efd62; all addressed
in this single follow-up commit. No production-code behaviour
change — every fix is documentation, SAFETY-comment hygiene, or
test-listing accuracy.

**(1) bsp-qemu-virt/src/main.rs SAFETY-comment expansion.** The
`load_image` invocation's `unsafe { ... }` block had a terse
SAFETY comment that partially satisfied the CLAUDE.md
non-negotiable #2 (a)/(b)/(c) discipline. Expanded to explicitly
state (a) why unsafe is required (materialising `&mut`/`&` to
write-once `StaticCell` payloads via `assume_init_*`), (b) the
exact invariants — initialisation order across the five named
statics + single-core cooperative + scope-limited momentary `&mut`
not crossing the cooperative switch + ADR-0021's discipline +
audit IDs UNSAFE-2026-0010 + UNSAFE-2026-0014, and (c) why safer
alternatives were rejected (`Box<Mutex<T>>` requires a heap allocator
v1 doesn't have; `OnceCell`/`LazyCell` cannot express the boot-flow
ordering constraints; the `StaticCell` write-once pattern is the
minimal `Sync` shape that matches the actual boot semantics).

**(2) docs/analysis/tasks/phase-b/T-019-task-loader.md §Simulation
table rows 6+7.** Pipes inside `\`USER|EXECUTE\`` and `USER | WRITE`
were breaking the GFM table-column parser. Escaped both as
`USER\|EXECUTE` and `USER \| WRITE`.

**(3) docs/architecture/task-loader.md §Rollback contract test list.**
Stale test name `rolls_back_on_misaligned_image_base_va` replaced
with the renamed identifier
`rejects_misaligned_image_base_va_with_pmm_byte_stable`; added a
parenthetical clarifying that this is the "no-rollback-needed" leg
of the contract (the row-1 alignment preflight catches the
misalignment before any state change).

**(4) docs/roadmap/current.md banner.** Resolved the `HEAD <TBD>`
placeholder to `95efd62` (the round-4 follow-up commit). The
7-commit list now names every commit by SHA; subsequent on-branch
commits (this polish + any future) are framed as "post-review
doc/style polish" rather than as part of the substantive arc.

**(5) kernel/src/obj/mod.rs module rustdoc.** Refreshed the stale
module-level documentation:
  - Removed the "all v1 kernel-object code is safe Rust" claim
    (no longer true: `task_loader` introduces one audited
    `unsafe` block at the `copy_nonoverlapping` byte-copy site,
    covered by UNSAFE-2026-0027).
  - Added a §"Public surface (v1)" section listing the four
    exported families: Endpoint, Notification, Task, and the
    Task-loader API (`load_image` + `LoadedImage` + `LoadError`).
  - Pointed at ADR-0029 + phase-b §B4 §Revision-notes for the
    loader's scope boundary (LoadedImage descriptor, not a
    runnable task cap — runnability gates on B5/B6).

**(6) kernel/src/mm/mod.rs `phys_frame_kernel_ptr` forward-compat
example.** The doc-comment showed a future-ADR-0033 migration
snippet using `.expect(...)`, which would lint-fail under the
kernel crate's `#![deny(clippy::expect_used)]` discipline if a
maintainer copy-pasted it. Rewrote the example with two lint-clean
patterns:
  - Pattern A: `checked_add(...).unwrap_or_else(|| {
    debug_assert!(...); fallback })` — branches on overflow, no
    panic in release.
  - Pattern B: `saturating_add(...)` — matches the rest of the
    kernel's `clippy::arithmetic_side_effects` discipline.
Both reference `KERNEL_PHYS_BASE` and ADR-0033 explicitly so the
example is concrete.

Tests at HEAD: **259/259** (no test changes — pure doc/style).
All gates clean: cargo fmt --check, cargo host-test,
cargo host-clippy -D warnings, cargo kernel-clippy -D warnings,
cargo kernel-build. QEMU smoke byte-stable.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Post-review-round-4 doc/style polish addressed in commit `74694d4`. All 6 nits verified valid against current code; all fixed in a single follow-up commit with no production-code behaviour change.

# Location Fix
1 `bsp-qemu-virt/src/main.rs` SAFETY comment ✅ Expanded to satisfy CLAUDE.md non-neg #2 (a)/(b)/(c): why unsafe is required (StaticCell `assume_init_*` materialisation), exact invariants (initialisation order + single-core cooperative + scope-limited `&mut` + ADR-0021 no-`&mut`-across-switch + UNSAFE-2026-0010 / 0014 audit IDs), why safer alternatives rejected (no heap → no `Box`; `OnceCell` can't express boot-flow ordering)
2 T-019 §Simulation table rows 6+7 ✅ Escaped pipes: `USER\|EXECUTE` and `USER \| WRITE`
3 `docs/architecture/task-loader.md` §Rollback contract ✅ Renamed `rolls_back_on_misaligned_image_base_va` → `rejects_misaligned_image_base_va_with_pmm_byte_stable` + parenthetical noting it's the "no-rollback-needed" leg
4 `docs/roadmap/current.md` banner ✅ Resolved `HEAD ` → `95efd62` (the round-4 follow-up commit); subsequent on-branch commits framed as post-review polish rather than substantive arc
5 `kernel/src/obj/mod.rs` module rustdoc ✅ Removed stale "all v1 kernel-object code is safe Rust" claim (no longer true: `task_loader` has one audited `unsafe` for `copy_nonoverlapping` per UNSAFE-2026-0027); added §"Public surface (v1)" listing all 4 exported families
6 `kernel/src/mm/mod.rs` `phys_frame_kernel_ptr` forward-compat doc ✅ Replaced `.expect(...)` example (which would lint-fail under the kernel's `#![deny(clippy::expect_used)]`) with two lint-clean patterns: (A) `checked_add(...).unwrap_or_else(

Tests at HEAD `74694d4`: 259/259 (no test changes). All gates clean: `cargo fmt --check`, `cargo host-test`, `cargo host-clippy -D warnings`, `cargo kernel-clippy -D warnings`, `cargo kernel-build`. QEMU smoke byte-stable.

@cemililik
Copy link
Copy Markdown
Collaborator Author

@coderabbitai full review

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 15, 2026

✅ Actions performed

Full review triggered.

Copy link
Copy Markdown

@coderabbitai coderabbitai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 3

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)
kernel/src/mm/pmm.rs (1)

879-885: 🛠️ Refactor suggestion | 🟠 Major | ⚡ Quick win

Expand these test SAFETY comments to match the repo rule.

These comments cover the memory-validity part, but they still omit why unsafe is required here and why a safer alternative was rejected. The production unsafe blocks in this PR already follow that pattern, so the test blocks should be brought up to the same bar.

As per coding guidelines, "Every unsafe block must have a comment explaining (a) why it is needed, (b) what invariants it upholds, (c) why safer alternatives were rejected."

Also applies to: 896-899

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@kernel/src/mm/pmm.rs` around lines 879 - 885, Expand the existing SAFETY
comment above the unsafe block that calls core::ptr::write_bytes(ptr, 0xA5u8, 16
* 4096) to follow the repo rule: state explicitly (a) why unsafe is required
here (calling raw pointer write via core::ptr::write_bytes requires unsafe), (b)
the invariants being upheld (ptr is PAGE_SIZE-aligned and points to the head of
a 16-frame host-allocated Vec<u8> kept alive by _buf for the test duration, the
write length exactly matches the Vec payload so no out-of-bounds or aliasing
occurs, and no other aliasing mutable references exist), and (c) why a safer
alternative was rejected (e.g., using safe slice APIs would require reborrowing
or moving ownership of _buf which would change test semantics or cannot
guarantee the same alignment/size for the specific low-level test). Apply the
same expanded comment pattern to the other test unsafe block that writes to ptr
at the later location (lines referenced in the review).
🧹 Nitpick comments (1)
kernel/src/mm/mod.rs (1)

165-168: ⚡ Quick win

Prefer pub(crate) unless an out-of-crate caller already needs this.

The doc positions this as a kernel-internal migration shim, so exporting it as pub widens the API around the current identity-mapping assumption and makes ADR-0033 harder to change cleanly later. If the only callers are inside kernel, tightening the visibility here keeps the surface area smaller.

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@kernel/src/mm/mod.rs` around lines 165 - 168, The function
phys_frame_kernel_ptr is currently exported pub but should be restricted to
pub(crate) to keep the kernel-internal shim from widening the public API; change
the declaration from pub fn phys_frame_kernel_ptr(...) to pub(crate) fn
phys_frame_kernel_ptr(...) in mod.rs, then search for callers of
phys_frame_kernel_ptr to ensure none are outside the kernel crate (update or
re-export only if truly needed) and run cargo check to verify visibility changes
compile cleanly.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@docs/analysis/tasks/phase-b/T-019-task-loader.md`:
- Line 134: The draft contains unresolved `<TBD>` placeholders in the changelog:
replace the `<TBD>` commit placeholder in the three-commit arc (after commits
`911f2ad` and `5711756` on branch `t-019-task-loader`) with the actual final
commit hash that adds BSP wiring (the commit that introduces `USERSPACE_IMAGE`,
`USERSPACE_IMAGE_BASE_VA`, `USERSPACE_STACK_PAGES` and the `load_image`
invocation), and replace the Smoke trace HEAD `<TBD>` with the exact smoke line
emitted by the BSP wiring commit (the `tyrne: image loaded (entry = 0x...; sp =
0x...; image bytes ...; stack bytes ...; AS cap = idx ...)` string). Ensure the
UNSAFE references (`UNSAFE-2026-0025`, `UNSAFE-2026-0026`, `UNSAFE-2026-0027`)
and the Amendment/smoke-verification notes point to the final commit hash and
update the docs/architecture/task-loader.md cross-links if they reference the
placeholder; run the full gate suite (`cargo fmt --check`, `cargo host-test`,
`cargo host-clippy -D warnings`, `cargo kernel-clippy -D warnings`, `cargo
kernel-build`) and include the resulting green verification line in place of
`<TBD>`.

In `@docs/decisions/0029-initial-userspace-image-format.md`:
- Line 44: This change mutates the accepted ADR text in
docs/decisions/0029-initial-userspace-image-format.md (specifically the "Build
pipeline (B4 / T-019 — placeholder blob)" paragraph) which violates the repo's
ADR append-only policy; instead revert this inline edit and add an append-only
amendment: create a new dated revision note or a superseding ADR that references
0029 and describes the intended correction (or additional context) about the
T-019 placeholder blob and build pipeline, so the original ADR remains unchanged
while the new document records the update.

In `@kernel/src/obj/task_loader.rs`:
- Around line 897-899: The unsafe call to FakeMmu::create_address_space (seen as
mmu.create_address_space(frame(0x4000_0000))) needs a three-part justification
comment: state why unsafe is required (calling an FFI/host-only operation or
invoking an API that can break Rust safety), enumerate the invariants that make
this particular call safe (e.g., frame is page-aligned, mmu is a test-only
FakeMmu with no UB, lifetime/aliasing guarantees), and explain why a safe
alternative was not used (test-only helper, no safe wrapper exists or would be
impractical). Add the same style of comment to the other test-only unsafe call
sites mentioned (the other create_address_space and similar unsafe blocks around
task loader initialization) so every unsafe block contains the required
(a)/(b)/(c) explanation.

---

Outside diff comments:
In `@kernel/src/mm/pmm.rs`:
- Around line 879-885: Expand the existing SAFETY comment above the unsafe block
that calls core::ptr::write_bytes(ptr, 0xA5u8, 16 * 4096) to follow the repo
rule: state explicitly (a) why unsafe is required here (calling raw pointer
write via core::ptr::write_bytes requires unsafe), (b) the invariants being
upheld (ptr is PAGE_SIZE-aligned and points to the head of a 16-frame
host-allocated Vec<u8> kept alive by _buf for the test duration, the write
length exactly matches the Vec payload so no out-of-bounds or aliasing occurs,
and no other aliasing mutable references exist), and (c) why a safer alternative
was rejected (e.g., using safe slice APIs would require reborrowing or moving
ownership of _buf which would change test semantics or cannot guarantee the same
alignment/size for the specific low-level test). Apply the same expanded comment
pattern to the other test unsafe block that writes to ptr at the later location
(lines referenced in the review).

---

Nitpick comments:
In `@kernel/src/mm/mod.rs`:
- Around line 165-168: The function phys_frame_kernel_ptr is currently exported
pub but should be restricted to pub(crate) to keep the kernel-internal shim from
widening the public API; change the declaration from pub fn
phys_frame_kernel_ptr(...) to pub(crate) fn phys_frame_kernel_ptr(...) in
mod.rs, then search for callers of phys_frame_kernel_ptr to ensure none are
outside the kernel crate (update or re-export only if truly needed) and run
cargo check to verify visibility changes compile cleanly.
🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: f75a0c2e-60cc-49c3-82e8-ef68b9d0cf64

📥 Commits

Reviewing files that changed from the base of the PR and between e09755d and 74694d4.

📒 Files selected for processing (12)
  • bsp-qemu-virt/src/main.rs
  • docs/analysis/tasks/phase-b/T-019-task-loader.md
  • docs/architecture/boot.md
  • docs/architecture/memory-management.md
  • docs/architecture/task-loader.md
  • docs/audits/unsafe-log.md
  • docs/decisions/0029-initial-userspace-image-format.md
  • docs/roadmap/current.md
  • kernel/src/mm/mod.rs
  • kernel/src/mm/pmm.rs
  • kernel/src/obj/mod.rs
  • kernel/src/obj/task_loader.rs

Comment thread docs/analysis/tasks/phase-b/T-019-task-loader.md Outdated
[adr-0034-placeholder]: 0027-kernel-virtual-memory-layout.md
- **VA placement.** A fixed userspace base VA is implementation-detail of T-019, not this ADR — the VA range scoping decision is owned by [T-019's Approach](../analysis/tasks/phase-b/T-019-task-loader.md) and bounded by [ADR-0027 §Decision outcome (a)](0027-kernel-virtual-memory-layout.md)'s `TTBR0_EL1` range. The loader maps the blob at a single contiguous VA range determined at compile time per the userspace linker script.
- **Build pipeline (B4 / T-019 — placeholder blob).** T-019 ships with a **hand-coded** placeholder blob: a small `&[u8]` literal (e.g. `[0x40, 0x00, 0x80, 0xd2, 0xc0, 0x03, 0x5f, 0xd6]` for `mov w0, #42; ret`) embedded into the BSP at compile time — sufficient to exercise the loader's `cap_create_address_space` + `cap_map` + `LoadedImage`-return path under host tests + the smoke trace without depending on a userspace toolchain. **No `cargo build`-to-`objcopy` pipeline lands with T-019.**
- **Build pipeline (B4 / T-019 — placeholder blob).** T-019 ships with a **hand-coded** placeholder blob: a small `&[u8]` literal (`[0x40, 0x05, 0x80, 0x52, 0xc0, 0x03, 0x5f, 0xd6]` — LE word 0 = `0x52800540` (`MOVZ w0, #42`) + LE word 1 = `0xd65f03c0` (`RET`); together `mov w0, #42; ret`) embedded into the BSP at compile time — sufficient to exercise the loader's `cap_create_address_space` + `cap_map` + `LoadedImage`-return path under host tests + the smoke trace without depending on a userspace toolchain. **No `cargo build`-to-`objcopy` pipeline lands with T-019.**
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | ⚡ Quick win

Don’t rewrite accepted ADR body content; record this as an append-only update.

These edits directly mutate the accepted ADR narrative. Per repo ADR governance, post-acceptance corrections should be captured as a dated revision/amendment note (or superseding ADR), not by rewriting original decision text.

As per coding guidelines, "ADRs are append-only; to override an old decision, write a new ADR that supersedes it."

Also applies to: 78-78

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/decisions/0029-initial-userspace-image-format.md` at line 44, This
change mutates the accepted ADR text in
docs/decisions/0029-initial-userspace-image-format.md (specifically the "Build
pipeline (B4 / T-019 — placeholder blob)" paragraph) which violates the repo's
ADR append-only policy; instead revert this inline edit and add an append-only
amendment: create a new dated revision note or a superseding ADR that references
0029 and describes the intended correction (or additional context) about the
T-019 placeholder blob and build pipeline, so the original ADR remains unchanged
while the new document records the update.

Comment thread kernel/src/obj/task_loader.rs Outdated
Verified all 5 review findings against current code state; all valid.
This commit applies minimal fixes: doc-only contract clarifications
for P1+P2, doc/rationale fixes + test count for P3, and one new
host test pinning the P2 conservatism.

**P1 (P1 severity)** — `tyrne_hal::Mmu::map` trait failure-semantics
contract was implicit. The kernel's safe `load_image` rollback path
runs `pmm.free_frame(frame)` after a failed `cap_map`, which is
sound under the *current* `QemuVirtMmu` impl (leaf descriptor write
is the last fallible step), but a future BSP impl that wrote the
leaf *before* a final fallible check would create aliasing through
safe code (the rollback would free a still-mapped frame). Fix:
tighten the `Mmu::map` trait doc-comment in `hal/src/mmu/mod.rs`
with a new `# Failure semantics` section explicitly stating three
clauses any BSP impl MUST satisfy:
  (1) on Err, no mapping installed at `va` (translation walk returns
      the same as before the call)
  (2) on Err, `pa` is not consumed — the caller retains ownership
      and may safely return it to its `FrameProvider`
  (3) intermediate page-table frames pulled from `frames` on Err are
      NOT promised back to the caller (they may be retained by `as_`)
The `task_loader::load_image` rollback comments now explicitly cite
clause (2) as the load-bearing safety argument. Current
`QemuVirtMmu` satisfies the new contract by construction (leaf write
is the last step in the walker — see UNSAFE-2026-0025); the contract
just makes that invariant explicit so future BSP impls cannot drift
from it.

**P2 (P2 severity)** — `Pmm::could_yield_pa_overlapping` only checks
extent + reserved-ranges, NOT the live bitmap. An image staged in a
currently-`Allocated` PMM frame is reported as a yield candidate
even though `alloc_frame()` cannot return that frame until it is
freed. The reviewer flagged this as documented contract drift; the
false-positive case was untested.

Fix: doc-comment tightened with a new `# Conservatism
(over-approximation)` section explaining the bitmap is deliberately
not consulted (the staged region becomes a yield candidate the
moment its owner calls `free_frame`, so the soundness argument
stays independent of allocation timing). New host test
`could_yield_pa_overlapping_treats_allocated_frame_as_yieldable`
pins the conservative behaviour and explicitly negates against the
reserved-range exclusion case to keep both legs of the contract
under regression coverage.

**P3a (P3 severity)** — Two doc sites claimed `image_base_va =
0x0080_0000` "mirrors" the kernel image's PA offset (`0x4008_0000`
= 0.5 MiB into the RAM segment). The math doesn't check out:
0x0080_0000 = 8 MiB, not 0.5 MiB. The claim is retired — the
actual rationale is "page-aligned, well clear of the null-page
region, structurally aligned at 8 MiB, far below
USERSPACE_VA_LIMIT". Both `bsp-qemu-virt/src/main.rs` and
`docs/architecture/task-loader.md` rewritten.

**P3b (P3 severity)** — `kernel/src/obj/task_loader.rs` module
rustdoc links to ADR-0030 via a markdown reference whose URL points
to `docs/decisions/0030-syscall-abi.md` — a file that does not
exist (ADR-0030 is a placeholder slot, not yet authored). Other
references to ADR-0030 across the repo (T-016, T-015, T-019
user-story, fundamentals doc, current.md) all treat it as a plain-
text forward-reference. Dropped the dead link; kept the textual
reference with a "(placeholder; not yet authored)" qualifier
consistent with the existing ADR-0033 placeholder convention.

**P3c (P3 severity)** — `docs/architecture/task-loader.md` test
count `34 → 33` (actual `#[test]` count via `grep -c "#\[test\]"`).

Tests at HEAD: **260/260** (+1: the new
`could_yield_pa_overlapping_treats_allocated_frame_as_yieldable`
PMM regression). All gates clean: cargo fmt --check,
cargo host-test, cargo host-clippy -D warnings,
cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke
byte-stable — full demo through `tyrne: all tasks complete`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Review-round 5 addressed in commit `5078944`. All 5 findings verified valid; minimal-change fixes applied — no LoadError variants added, no production-behaviour changes, one new regression test.

P1 — `Mmu::map` trait failure-semantics contract was implicit. ✅ Fixed. `hal/src/mmu/mod.rs`'s `Mmu::map` doc-comment gained a new # Failure semantics (load-bearing contract for `unsafe`-free callers) section with three explicit clauses any BSP impl must satisfy: (1) on Err, no mapping installed at `va`; (2) on Err, `pa` is not consumed (caller retains ownership); (3) intermediate frames pulled from `frames` mid-walk may be retained by `as_`. The loader's rollback path now explicitly cites clause (2) as its safety argument. Current `QemuVirtMmu` satisfies the tightened contract by construction (leaf write is the last fallible step — see UNSAFE-2026-0025); the contract just makes the invariant explicit so future BSP impls cannot drift.

P2 — `Pmm::could_yield_pa_overlapping` doesn't consult the bitmap. ✅ Fixed. Doc-comment gained a new # Conservatism (over-approximation) section explicitly stating the bitmap is deliberately not consulted: a currently-`Allocated` frame is still reported as a yield candidate because the staged region becomes a yield candidate the moment its owner calls `free_frame`, so the soundness argument stays independent of allocation timing. New regression test `could_yield_pa_overlapping_treats_allocated_frame_as_yieldable` pins the conservative behaviour + negates against the reserved-range exclusion case.

P3a — `0x0080_0000` "mirrors kernel offset" math drift. ✅ Fixed. The previous rationale claimed userspace VA `0x0080_0000` (8 MiB) "mirrors the 0.5 MiB-into-segment offset" of the kernel image at PA `0x4008_0000`. The math doesn't check out (8 MiB ≠ 0.5 MiB). Both `bsp-qemu-virt/src/main.rs:316-322` and `docs/architecture/task-loader.md:107` rewritten with the honest rationale (page-aligned, null-page-clear, structurally aligned at 8 MiB, far below `USERSPACE_VA_LIMIT`; not algebraically derived from kernel PA layout). The arch-doc revision explicitly retires the prior "mirror" claim so it doesn't re-emerge.

P3b — Dead ADR-0030 link. ✅ Fixed. `kernel/src/obj/task_loader.rs:59` module rustdoc linked to `docs/decisions/0030-syscall-abi.md` which doesn't exist (verified via `ls`). All other repo references (T-016, T-015, T-019 user-story, fundamentals doc, current.md) treat ADR-0030 as a plain-text forward-reference. Dropped the markdown link; kept the textual reference with a "(placeholder; not yet authored)" qualifier consistent with the existing ADR-0033 placeholder convention.

P3c — Stale test count `34 → 33`. ✅ Fixed. `docs/architecture/task-loader.md:144` now matches `grep -c "#\[test\]" kernel/src/obj/task_loader.rs` = 33.

Tests at HEAD `5078944`: 260/260 (+1: the new `could_yield_pa_overlapping_treats_allocated_frame_as_yieldable` PMM regression). All gates clean: `cargo fmt --check`, `cargo host-test`, `cargo host-clippy -D warnings`, `cargo kernel-clippy -D warnings`, `cargo kernel-build`. QEMU smoke byte-stable — full demo through `tyrne: all tasks complete`.

Verified all 5 review findings against current code state; all valid.
Minimal-change fixes: 4 doc-only, 1 visibility narrowing.

**(1) T-019 user-story §Review-history line 134 — unresolved `<TBD>`
placeholders.** The 2026-05-14 implementation-arc row carried two
literal `<TBD>` tokens (the BSP-wiring commit hash and the smoke-
trace HEAD reference) that subsequent review-round commits never
back-filled. Resolved both to `ae31bc8` (the round-3 BSP-wiring
commit). The accompanying narrative (test count, gate names, smoke
line content) was the state at commit `ae31bc8` and stays as the
historical record per the user-story file's append-only convention.

**(2) ADR-0029 §"Build pipeline (B4 / T-019)" + §"Host-side loader
tests" — in-place edit of an Accepted ADR violated append-only
policy.** Commit `196d3fb` (T-019 commit 4) silently rewrote the
placeholder-byte literal from `[0x40, 0x00, 0x80, 0xd2, ...]` (the
Accept-state form) to `[0x40, 0x05, 0x80, 0x52, ...]` (the
documented-intent `mov w0, #42; ret` form). Per CLAUDE.md non-neg
#5 + the ADR README §Format, ADRs are append-only — corrections
land in §Revision notes, not via body rewrites. Fix:
  - Reverted both byte literals (lines 44 + 78) to their Accept-
    state form.
  - Added a new §Revision notes section before §References with a
    2026-05-16 entry recording the byte-encoding correction,
    decoding both literals explicitly (Accept-state bytes →
    `MOVZ x0, #2; RET`; corrected bytes → `MOVZ w0, #42; RET`),
    citing the canonical kernel-source bytes in
    `bsp-qemu-virt/src/main.rs::USERSPACE_IMAGE`, and noting the
    discrepancy was non-load-bearing because the placeholder is
    not executed in B4.

The kernel-source bytes are unchanged (BSP `USERSPACE_IMAGE` is
the production reality and stays at the corrected form).

**(3) `kernel/src/obj/task_loader.rs` test-only `unsafe`
`FakeMmu::create_address_space` call sites — brief SAFETY comments
missing (a)/(b)/(c) discipline.** Four sites use the pattern:
  - `fixture` helper (the canonical one) at line 908
  - `missing_derive_surfaces_via_address_space_creation_failed`
    test body
  - `FailingMapMmu::create_address_space` `unsafe fn` body
  - `fixture_with_failing_mmu` helper

Fix: expanded the `fixture` helper's SAFETY comment with the full
(a) why-unsafe-required / (b) invariants-upheld /
(c) why-safer-alternative-rejected discipline. Cross-referenced
the three peer sites by name with brief "same argument as fixture"
notes, including the `unsafe fn` body which separately documents
the `unsafe_op_in_unsafe_fn` lint requirement.

**(4) `kernel/src/mm/pmm.rs` test `unsafe` blocks for
`core::ptr::write_bytes` and `*returned_ptr.add(off)` — brief SAFETY
comments missing (a)/(b)/(c).** Both blocks (the pre-poison fill +
the per-byte zero-fill assertion) were one-liners covering only
(b). Expanded both to the full (a)/(b)/(c) discipline, naming
`aligned_backing`'s host-allocation contract and the per-byte
loop's in-bounds reasoning.

**(5) `kernel/src/mm/mod.rs::phys_frame_kernel_ptr` — visibility
widened public API unnecessarily.** Helper is only called from
inside the kernel crate (`task_loader::load_image`'s byte-copy
site; verified via `grep -rn phys_frame_kernel_ptr`). Narrowed
`pub` → `pub(crate)` to keep the kernel-internal shim out of the
crate's public API surface; no external (bsp / hal / test-hal)
caller exists.

Tests at HEAD: **260/260** (no test changes; all fixes are
doc/visibility). All gates clean: cargo fmt --check,
cargo host-test, cargo host-clippy -D warnings,
cargo kernel-clippy -D warnings, cargo kernel-build. QEMU smoke
byte-stable — full demo through `tyrne: all tasks complete`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@cemililik
Copy link
Copy Markdown
Collaborator Author

Review-round 6 addressed in commit `eb14c51`. All 5 findings verified valid against current code; minimal-change fixes applied — no production-code behaviour change, 1 visibility narrowing, 4 doc fixes.

# Finding Status / fix
1 T-019 user-story line 134 carried two unresolved `` placeholders (BSP-wiring commit hash + smoke-trace HEAD) ✅ Resolved both to `ae31bc8` (the round-3 BSP-wiring commit). The accompanying numbers/gates wording stays as the historical record at commit `ae31bc8`. `grep -r '' docs/ kernel/ bsp-qemu-virt/ hal/` confirms no remaining placeholders
2 ADR-0029 §"Build pipeline" + §"Host-side loader tests" — in-place edit of an Accepted ADR (196d3fb rewrote placeholder bytes from `[0x40, 0x00, 0x80, 0xd2, ...]` to `[0x40, 0x05, 0x80, 0x52, ...]` after Accept) violates CLAUDE.md non-neg #5 + ADR README §Format append-only policy ✅ Reverted both byte literals to Accept-state form. Added new §Revision notes section before §References with a 2026-05-16 entry decoding both literals (Accept-state → `MOVZ x0, #2; RET`; corrected → `MOVZ w0, #42; RET`), citing `bsp-qemu-virt/src/main.rs::USERSPACE_IMAGE` as canonical source, noting the discrepancy is non-load-bearing (placeholder not executed in B4). Kernel-source bytes unchanged
3 `kernel/src/obj/task_loader.rs` test `unsafe` `FakeMmu::create_address_space` sites missing (a)/(b)/(c) discipline ✅ Expanded `fixture` helper's SAFETY (canonical site) with full (a) why-unsafe / (b) invariants / (c) why-safer-rejected. Cross-referenced 3 peer sites by name (`missing_derive_surfaces_...`, `FailingMapMmu::create_address_space` body, `fixture_with_failing_mmu`). `FailingMapMmu` body separately documents the `unsafe_op_in_unsafe_fn` lint requirement
4 `kernel/src/mm/pmm.rs` 2 test `unsafe` blocks (write_bytes pre-poison + per-byte zero-fill assert) — one-liners only covering invariants (b) ✅ Both expanded to full (a)/(b)/(c) — naming `aligned_backing`'s host-allocation contract for invariants and rejecting `from_raw_parts`-based slice forms (would re-introduce same audit obligation)
5 `kernel/src/mm/mod.rs::phys_frame_kernel_ptr` — `pub` widens public API unnecessarily ✅ Narrowed `pub` → `pub(crate)`. `grep -rn phys_frame_kernel_ptr kernel/ bsp-qemu-virt/ hal/ test-hal/` confirms only one in-crate caller (`task_loader::load_image`); no external caller exists

Tests at HEAD `eb14c51`: 260/260 (no test changes — all fixes are doc/visibility). All gates clean: `cargo fmt --check`, `cargo host-test`, `cargo host-clippy -D warnings`, `cargo kernel-clippy -D warnings`, `cargo kernel-build`. QEMU smoke byte-stable — full demo through `tyrne: all tasks complete`.

@cemililik cemililik merged commit 7f876af into main May 15, 2026
6 checks passed
@cemililik cemililik deleted the t-019-task-loader branch May 25, 2026 12:49
cemililik added a commit that referenced this pull request May 29, 2026
current.md + T-021 task file cite PR #34 (base main, 9 commits, bundles T-020 +
T-021 in one combined review per the maintainer's call). Matches the project's
PR-reference convention (cf. T-019/PR #31, B4/PR #33).

Refs: ADR-0030, ADR-0031
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
cemililik added a commit that referenced this pull request May 29, 2026
…-021) (#34)

* docs(adr): propose ADR-0030/0031 — syscall ABI + initial syscall set

ADR-0030 settles the EL0->EL1 syscall calling convention (x8 = number,
x0-x5 args, x0 status + x1-x7 payload, SVC #0), the dedicated-status
error encoding, and the K2-5 split of IpcError::InvalidCapability into
StaleHandle / WrongObjectKind / MissingRight (with the per-subject-cap
security argument and the arena-staleness ordering caveat). ADR-0031
fixes the v1 syscall set (send, recv, console_write [capability-gated +
release debug-gated], task_yield, task_exit), reserves number 0 as
invalid, and pins each call's register layout; every object-naming
syscall performs a capability check (P1/P4).

Opens T-020 (error taxonomy + Capability/CapObject Debug redaction — the
pure-Rust foundation, In Progress) and T-021 (SVC trap trampoline +
panic-free dispatcher + copy-from/to-user — Ready, the security-critical
hardware-facing half) to ground both ADRs' dependency chains per ADR-0025
Rule 1. Both ADRs land at Proposed; Accept follows in a separate commit.

Refs: ADR-0030, ADR-0031

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs(adr): accept ADR-0030/0031 after careful re-read + maintainer review

Flip ADR-0030 and ADR-0031 Proposed -> Accepted in a commit separate from
the propose draft, per write-adr skill section 10. The careful re-read plus
a same-day maintainer review surfaced and corrected several drafting issues
*before* this Accept — all folded into the proposed bodies above, so the
Accepted text is correct from the start (no post-Accept body edit):
  - an SVC from a B5 EL1 kernel-stub takes the current-EL (VBAR_EL1+0x200)
    sync vector, not the lower-EL (+0x400) EL0 vector, so the real EL0
    round-trip is runtime-verified in B6, not B5;
  - console_write is capability-gated on a debug-console capability (it was
    ambient authority, a P1/P4 violation); the release debug-gate is a
    separate, independent defense-in-depth gate;
  - the syscall numbers 1..5 are a fixed decision (tests regression-verify
    them), and the payload registers are x1..x7.
Adds the additive ADR-0017 revision rider recording that the IpcError
taxonomy is refined (not superseded) and the three-primitive surface is
unchanged.

Refs: ADR-0030, ADR-0031

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* feat(ipc): split IpcError::InvalidCapability into three typed variants

Per ADR-0030's K2-5 bundle, replace the collapsed IpcError::InvalidCapability
with StaleHandle / WrongObjectKind / MissingRight so the in-kernel and the
future userspace error spaces agree and each failure is a distinct, handleable
case. Validation now resolves in the order resolve -> type-check -> authority
(kind before rights), matching CapError's InvalidHandle/WrongKind/
InsufficientRights shape, across validate_ep_cap, validate_notif_cap, and
sched::resolve_ep_cap; the four arena-staleness sites map to StaleHandle.
Revealing which check failed is safe for a per-subject, unforgeable capability
table (ADR-0030 security argument). Remaps the existing rights/stale test
assertions and adds 5 new tests pinning each variant (incl. wrong-kind-with-
right, proving kind-before-rights, and a destroyed-endpoint StaleHandle).
InvalidTransferCap is intentionally left intact (note C3-008). Updates
docs/architecture/ipc.md taxonomy section.

Security-relevant (capabilities + IPC). fmt / host-test (194 kernel) /
host-clippy / kernel-clippy / kernel-build / miri (no UB) all green.

Refs: ADR-0030

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* feat(cap): redact Capability and CapObject Debug to hide object identity

Per ADR-0030 "Security of the taxonomy split" / B5 sub-item 6 (K3-9, security
review section 6): a userspace-reachable log path (the future console_write
syscall) must never disclose the kernel object a capability names. Replace the
derived Debug on Capability with a hand-written impl that shows rights but
prints the object as <redacted>, and redact CapObject likewise (kind-only
Debug, hiding the wrapped slot index + generation). The individual kernel-
object handle types keep their derived Debug for kernel-internal diagnostics
(they never cross to userspace; T-021's console_write review gates that). Two
host tests pin both redaction layers. Broadens security-model.md's
"no unredacted Debug/Display" rule to capabilities.

The CapObject redaction was folded in from an adversarial self-review that
flagged it as a latent defense-in-depth gap (no current production formatter,
but conservative per CLAUDE.md rule 1). Security-relevant.

Refs: ADR-0030

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* test(ipc): pin StaleHandle + WrongObjectKind on ipc_cancel_recv

Add two tests so ipc_cancel_recv pins all three split variants
(it already had MissingRight): a Task cap carrying RECV proves the
kind-before-rights ordering (WrongObjectKind), and a cap whose endpoint
was destroyed exercises the arena-staleness branch (StaleHandle). This
makes ADR-0030's row-3 verification mapping accurate for cancel_recv
(it previously over-claimed cancel coverage). Kernel host tests 194 -> 196.

Refs: ADR-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs(roadmap): T-020 In Review; narrow B5 acceptance to current-EL proxy

Address the remaining maintainer-review findings (the ADR append-only fix
landed via the propose/accept rebase; this commit covers the rest):

- Major: phase-b §B5 acceptance over-promised a real EL0->EL1 round-trip,
  which ADR-0030 shows is impossible at B5 (an EL1 kernel-stub SVC takes
  the current-EL 0x200 vector, not the lower-EL 0x400 EL0 vector). Narrow
  B5 to "dispatch mechanism verified via the current-EL kernel-stub" and
  move the real EL0 0x400 round-trip to the B6 acceptance criteria.
- Minor: current.md banner said "In Progress" while the fields said
  "In Review"; fix the banner and the two broken T-021 links (../).
- Move T-020 to In Review in the task index + task doc; record the
  maintainer-review round and the row-to-verification mapping (now incl.
  the two new cancel_recv variant tests) in T-020's review history.
- Add EL0/EL1, SVC, Syscall, and Syscall ABI glossary entries and note
  the taxonomy split on the ipc.md architecture status row.

Refs: ADR-0030, ADR-0031
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* test(ipc): make wrong-kind tests actually prove kind-before-rights

Second-round review found the four *_wrong_object_kind tests handed the
cap the operation's own right, so they returned WrongObjectKind under
*both* the chosen kind-first order and a hypothetical rights-first
regression — i.e. ordering-agnostic, proving nothing (a rights-first flip
would not fail them). Fix: each test now uses a wrong-kind cap that also
LACKS the required right (CapRights::empty()), the only input that
discriminates the order (WrongObjectKind under kind-first, MissingRight
under rights-first), so a regression to rights-first now fails the tests.
Updates the section comment and T-020 AC#4 to state what each test
actually proves; corrects T-020's stale test counts (AC#6 194 -> 196;
review history "8 new" -> "9 new").

(The stale-variant references in the Turkish technical-analysis IPC
chapter were also refreshed on disk for local reference, but that tree is
gitignored, so it is not part of this commit / the repo.)

No production code change; fmt / host-test 196 / clippy / build / miri
(no UB) all green.

Refs: ADR-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* feat(syscalls): EL0→EL1 SVC dispatch — trampoline, panic-free dispatcher, copy-user

Land the security-critical hardware-facing half of B5 (T-021): the EL0→EL1
SVC trap path that instantiates ADR-0030's calling convention and ADR-0031's
five-syscall v1 set.

New architecture-agnostic, panic-free, host-tested kernel `syscall` module:
- error.rs: SyscallError composing CapError/IpcError via From, with a stable
  numeric status encoding (0 = Ok; 1-3 top-level; 0x10x = Cap; 0x20x = Ipc).
- abi.rs: SyscallNumber decode (release debug-gate on console_write via
  cfg!(debug_assertions)), the register frame types, value↔register packing
  for Message/outcomes, and the Option<CapHandle> null-handle sentinel.
- user_access.rs: UserAccessWindow + validated copy_from_user/copy_to_user
  (range-check-then-copy; wrap and zero-length handled; never derefs an
  unvalidated user pointer).
- dispatch.rs: the panic-free dispatcher + per-syscall handlers + the
  debug-console capability check; control-plane syscalls (task_yield/exit)
  return a SyscallEffect directive rather than touching the scheduler.

Capability surface: CapObject::DebugConsole (singleton, no handle) +
CapRights::CONSOLE_WRITE (bit 7, added to KNOWN_BITS) + CapHandle::from_raw
(ABI-decode constructor; reconstructed handles are validated by lookup).

BSP (hardware-facing): tyrne_sync_trampoline in vectors.s installed at both
VBAR_EL1+0x200 (current-EL, the B5 path) and +0x400 (lower-EL AArch64, the B6
EL0 path) — saves the full x0-x30 + SP_EL0 + ELR_EL1 + SPSR_EL1 frame, routes
ESR_EL1.EC==SVC64 to a Rust syscall_entry, else to the existing panic path.
SyscallTrapFrame (272 B, #[repr(C)], const-asserted to match the asm).
kernel_entry runs an EL1 kernel-stub SVC smoke (console_write + bad-number).

Gates: fmt / host-clippy / kernel-clippy / kernel-build clean; host tests 236
(+40); cargo test --release green (the debug-gate release-path tests);
cargo miri test --workspace --exclude tyrne-bsp-qemu-virt clean (43+236+53).
QEMU smoke (debug): two SVCs taken at the current-EL vector (ESR 0x15/SVC64,
EL1→EL1), clean ERET; console_write emits its buffer via the syscall path
(status 0x0, 63 bytes); a reserved-invalid number returns BadSyscallNumber
(0x1); -d int,unimp,guest_errors shows no new fault class; the cooperative
demo still runs to "tyrne: all tasks complete".

The real EL0 +0x400 round-trip (EL0↔EL1 transition + copy-user against a
separate userspace TTBR0_EL1) is wired but runtime-verified in B6 per
ADR-0030 §Simulation.

Refs: ADR-0030, ADR-0031
Audit: UNSAFE-2026-0029, UNSAFE-2026-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* test(syscalls): T-021 review-round follow-up — dispatch tests + compile-time payload guard

Apply the actionable findings from the T-021 adversarial review-round (which
confirmed no live B5 defect). All changes are test coverage, a behavior-
preserving defensive refactor, and B6 forward-gate tracking — no production
behavior change (QEMU trace byte-stable; the const-generic emits identical
register values).

Test coverage (+4 dispatch-level tests; host tests 236 -> 240) closing gaps the
review surfaced:
- send_with_transfer_cap_then_recv_returns_cap_in_x6 — the x5 transfer-handle
  decode -> ipc_send cap_take AND ipc_recv -> encode_recv_outcome x6 cap-pack,
  end-to-end through dispatch (previously untested; verified non-vacuous via a
  mutation check — breaking the x6 pack makes it fail).
- send_with_stale_transfer_handle_returns_invalid_transfer_cap — status 0x205.
- recv_with_no_sender_returns_pending_packing — Pending packing (x1=pending,
  x2..x7 zeroed).
- console_write_exactly_one_chunk_emits_all_bytes — the len == CONSOLE_WRITE_CHUNK
  loop boundary (debug-gated).

Hardening (nit): SyscallReturn::with_payload is now a const-generic
with_payload::<IDX> with `const { assert!(IDX < 7) }`, turning the (already
unreachable-from-untrusted-input) runtime index panic into a compile-time error
at the call site — matching the kernel's compile-time-guard idiom. Call sites
updated to the ::<N> turbofish.

Clarity: the three scattered "unreachable re-validation" comments in
sys_console_write consolidated into one inequality-chain proof.

Docs: phase-b.md §B6 gains an explicit "T-021 carry-forward gates" list (per-task
console_write window + per-page user-VA translation returning FaultAddress not
panic; SP_EL1 init on the +0x400 entry; SYSCALL_STUB_TABLE -> current-task table)
so B6 cannot miss them; T-021 review history records the round.

Gates re-run green: fmt / host-clippy / kernel-clippy / kernel-build clean;
host-test 240; test --release green; miri --workspace excl BSP clean (43+240+53,
0 UB); QEMU smoke round-trip byte-stable.

Refs: ADR-0030, ADR-0031
Audit: UNSAFE-2026-0029, UNSAFE-2026-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs(roadmap): record PR #34 (combined T-020 + T-021 B5 review)

current.md + T-021 task file cite PR #34 (base main, 9 commits, bundles T-020 +
T-021 in one combined review per the maintainer's call). Matches the project's
PR-reference convention (cf. T-019/PR #31, B4/PR #33).

Refs: ADR-0030, ADR-0031
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(syscalls): T-021 review-round 2 — overlap-safe copy-user + scope/guard fixes

Address the second review-round on PR #34. Fix only still-valid issues; one
finding (release-wrap of a const) was refuted but its requested guard kept as a
clearer compile-time tripwire; one (test-scaffolding helper) skipped.

Soundness (headline): copy_from_user / copy_to_user are SAFE `pub fn`s, so they
must be sound for every input — but `UserAccessWindow::validate` proves *bounds*,
not *disjointness*, and under the v1 identity map (VA == PA) a caller could pass
a user_ptr range that aliases the kernel-owned dst/src slice, making
`copy_nonoverlapping`'s non-overlap precondition violable from safe code (UB).
Switch both moves to `core::ptr::copy` (memmove), which is correct for any
overlap; drop the unprovable "source and destination are disjoint" claim from
the SAFETY comments and document why `copy` (not `copy_nonoverlapping`) is the
sound choice. Behaviour is identical for the non-overlapping case (all current
callers are disjoint), so QEMU/Miri/host evidence is unchanged. UNSAFE-2026-0030
gains an append-only Amendment recording the change (title/anchor preserved).

Hardening (compile-time guards, no runtime cost):
- abi.rs: a `const _: () = assert!(NULL_CAP_HANDLE > max-packable-handle-word)`
  locks the sentinel-collision-freedom invariant — a future CapHandle widening
  that could push a packed word into the sentinel's bit range fails the build.
- bsp syscall.rs: an explicit `const _: () = assert!(PMM_EXTENT_END >=
  PMM_EXTENT_START)` with a clear message in front of SYSCALL_USER_WINDOW_LEN.
  (The reviewer's "wraps in release" premise is incorrect — the subtraction is a
  `const`, and const-eval rejects underflow at build time, never wraps — but the
  named assert gives a clearer failure than a raw const-eval overflow error.)

Docs:
- T-021 §Informs: scope the ADR-0030 §Simulation discharge — rows 2/4 in full +
  the mechanism half of rows 0/1/5 via the EL1-stub proxy at the current-EL
  +0x200 vector; the EL0-runtime half of rows 0/1/5 (the +0x400 vector, the
  EL0↔EL1 transition, copy-user vs a separate userspace TTBR0_EL1) is deferred to
  B6, not discharged here.
- current.md: remove the blank lines between adjacent banner paragraphs so they
  form one contiguous `>` blockquote (matches the file's existing multi-paragraph
  style; resolves markdownlint MD028).

Skipped: extracting a SyscallContext test-builder — the scaffolding verbosity is
largely forced by the borrow structure (tests declare + later inspect the
borrowed locals), so a helper saves only the struct-literal line per test and
isn't worth churning the just-reviewed test suite on an in-review PR.

Gates re-run green: fmt / host-clippy / kernel-clippy / kernel-build; host-test
240; test --release 233; miri --workspace excl BSP clean (0 UB); QEMU smoke
round-trip byte-stable.

Refs: ADR-0030, ADR-0031
Audit: UNSAFE-2026-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* audit(syscalls): correct UNSAFE-2026-0030 amendment — disjointness is the soundness basis

Review-round on PR #34 (two findings; each verified against current code):

1. UNSAFE-2026-0030 amendment (docs/audits/unsafe-log.md) — VALID, fixed. The
   amendment added in 2c713c0 (a) lacked the commit SHA the audit-log format
   wants and (b) over-claimed that switching to `core::ptr::copy` makes the copy
   "overlap-tolerant". An empirical Miri probe disproved that: an overlapping
   (user_ptr, kernel-slice) pair is UB *regardless* of the copy primitive —
   `copy_from_user`'s `dst: &mut [u8]` (and `copy_to_user`'s `src: &[u8]`)
   parameter is exclusive / shared, so an aliasing access through the exposed
   `user_ptr` violates that borrow (Stacked Borrows: "not granting access to tag
   <wildcard> … strongly protected"). The amendment now carries SHA 2c713c0,
   marks the original `copy_nonoverlapping` §Operation / invariant(3) /
   rejected-alternatives wording as superseded, and states the true soundness
   basis: the user/kernel **disjointness** invariant (user_ptr = userspace,
   kernel slice = distinct allocation in v1 / separate AS in B6), under which
   both `copy` and `copy_nonoverlapping` are sound. `core::ptr::copy` is kept as
   the conservative primitive. The copy_from_user / copy_to_user SAFETY comments
   are corrected to match (invariant 3 = disjointness, not "overlap-tolerant").

2. Add overlapping-copy regression tests — SKIPPED, with reason. The requested
   tests assert "overlapping copies are allowed", but overlap is UB here (see
   above — Miri-confirmed via a temporary probe, now removed), independent of
   `copy` vs `copy_nonoverlapping`. Such tests would (a) break the Miri gate and
   (b) codify an unsound expectation. The real invariant is disjointness, which
   the existing tests + the structural user/kernel split already cover; an
   overlapping call correctly fails under Miri's borrow model.

No code-behaviour change (the `core::ptr::copy` calls are unchanged; only SAFETY
comments + the audit amendment text). Gates: fmt / host-clippy / kernel-clippy /
kernel-build clean; host-test 240; miri (syscall) 0 UB. Production code is
byte-identical to 2c713c0, already validated with full miri + test --release +
QEMU smoke.

Refs: ADR-0030, ADR-0031
Audit: UNSAFE-2026-0030
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant