agent: builder model: opus max_turns: 120 budget_usd: 30 —

Brief: C7-r1, the first C-7 rest slice: claims refusals, `walked` seeds, attribute marks into Nikaia (#125)

Score: self-hosting lane (docs/priorities.md, C-7 rest, S 2): ~420 Rust lines replaced, no prerequisite; the table row and its risks are in docs/selfhosting-plan.md, C-7 rest and E12 (read it first; line ranges there are at 62a07a1, re-grep before cutting).

The slice (row C7-r1 of that table)

crates/nikaia/src/check/mod.rs: refuse_unproved_claims (now :1193), refuse_assumes_in_std (:1257, called twice from sysroot.rs; ASSERT is dead) -> new tools/check_claims.nika.
check/mod.rs the CheckState seeds walked reads off the item tree: grammars, std_in_scope, std_modules, opaque_handles, foreign_names (:393-459), and payload_of (:77) -> tools/check_walked.nika as check_walked_seed.
check/host.rs place_of (:355; files() becomes world.beside) -> Nikaia; check_host.nika:98 is its trait side.
check/attributes.rs Mark, PLACES, mark_of (:40-87; contracts/mod.rs keeps calling an adapter) -> tools/check_attributes.nika.
Delete the dead a_byte, byte_literal, an_or_a, boxed_member, the two empty impl Checker<'_> {} and the orphan doc comments above them (check/mod.rs ~607-672, ~1135).
Host change: removed CheckHost::payload_of, place_of, written (Nikaia calls check_walked_written with world.words); none added.

Known risks (from the table)

the map loop over ((start, _), claim) is a nested tuple pattern in a for; and n if n <= 0 => continue inside a match that makes a value: bind the count first. A gap that blocks is a compiler fix (CLAUDE.md Fix, do not work around), its own commit with a test; if it cannot be fixed in this run, Result: partial with the probe under Found:.
A new .nika needs one lower-std with the old binary first, and a row in scripts/self_hosting.py (docs/builder-facts.md).

To build (each its own commit, `Part of #125`)

check_claims.nika (the two refusals) + the dead-code deletion.
The walked seeds and payload_of into check_walked.nika; place_of and written off the host.
Mark/PLACES/mark_of into check_attributes.nika.

Done when

All three built; lower-std clean, generated diff committed; nikaia test tests/compiler --both-settings; it filters claims, assume, attributes, walked, sysroot, and the guard set of .claude/agents/builder.md. Report the Rust lines removed (python3 scripts/self_hosting.py) under Tests:. Changelog: none unless a message text changes.

Stop and report if

A design choice the table leaves open (a host method that has to be added), or an error in another agent’s file.

Read docs/builder-facts.md.

Rules (CLAUDE.md; this block is pasted into every brief, also a fix-forward)

Read docs/builder-facts.md first. develop in the main checkout; git status at start: other agents’ uncommitted files are not yours, never touch or stage them.
git add <files> only; commit after each step; git push origin develop fast-forward, no rebase (rejected: report Pushed: rejected, go on committing).
Before pushing: cargo fmt, cargo clippy --all-targets -- -D warnings, scripts/pre-push-check.sh, and the gate of .claude/agents/builder.md (#852).
No version lines, CHANGELOG.md, badges; no new NK code. New tests in Nikaia only; never the full suite. No foreground sleep, no polling; scripts in files.
Disk: NIKAIA_CACHE_LIMIT=2G; at most two clones with target/ in the machine; delete your own clone’s target/ and target/release/nikaia-scratch at the end; report GB freed.

Report (at most 15 lines, to exactly `/home/user/Nikaia/docs/briefs/c7-r1.md.report.md`)

Fields of docs/architect.md, Briefs and reports: Result: done|noop|partial|blocked (the bare word first; Owner: is a question for the owner or none, never a role), Files, Commit, Fixes, Pushed, Tests, Gate (green|red), Deviation, Found, Needs, Changelog, Owner, Disk freed. none where nothing, and then the bare word: Deviation: none (a note) cuts the batch (batch.nika compares exactly); a note goes into the commit message. Found: is only for a defect outside your change (it cuts the batch); how you solved your own step goes into the commit message. Deviation: is only a step of the brief built otherwise than written or not built (a choice the brief left to you, such as keep what X needs and say so, is no deviation: it goes into the commit message); how you verified (e.g. a test not run against the unfixed compiler) goes under Tests:. A noop says why under Tests: (what was probed), not under Deviation:. Final answer, one line: done <sha>, report <path> (or BLOCKED: ... / PUSH REJECTED ...).

Attribution: Co-Authored-By: Claude Opus 5.5 noreply@anthropic.com Claude-Session: https://claude.ai/code/session_01GFeMqxRbtUMiGVyDMxsvEq

This site is open source. Improve this page.

Brief: C7-r1, the first C-7 rest slice: claims refusals, walked seeds, attribute marks into Nikaia (#125)