Result: partial
Files: crates/nikaia-std/src/tools/prove_run.nika crates/nikaia-std/src/tools/lowered/prove_run.rs crates/nikaia-std/src/tools/lowered.rs crates/nikaia/src/prove.rs crates/nikaia/src/check/mod.rs scripts/self_hosting.py assets/badges/self-hosted.svg docs/briefs/prove-move.md.report.md
Commit: self-hosting: prove.rs’s rounds move into prove_run.nika
Part: #125
Lines: prove.rs 535 -> 326 (adapter); new tools/prove_run.nika 238, lowered twin 151; self-hosted badge 83.0 % -> 83.1 % (clean worktree at the commit)
Moved: ClaimRun and Comptimes (ProveClaimRun, ProveComptimes; re-exported under the old names), Comptimes::of (prove_comptimes_of; check/mod.rs calls prove::comptimes_of), the round loop of prove() with the walk’s set-up (prove_rounds, prove_walked, prove_state), implies (prove_implies, conditions adopted into one arena: the same node sequence as before), answer_of’s mapping (prove_answer), with_published (prove_with_published)
Kept in Rust: thread-local and process counters (CLAIM_RUNS, SECOND_QUERIES, TOTAL_) as the searched/counted/run closures; the book calls (proofs.rs); Proved and its usize/Finding conversion; condition/reads_back/condition_nodes (the compiler’s parser); changed_contracts’ wrapper; model_of (#1092); call_key deleted (no caller in the repository)
Tests: worktree build green; lower-std at fixpoint; nikaia test –both-settings on the 30 prove_/precondition_/bounds_expectation_ programs 30 ok; it proofs_file:: prove_loops:: prove_through_loops:: lock_column:: prove:: prove_mutables:: 84 ok; it contracts_across:: assert:: comptime_compiled:: bounds_report:: 42 ok; –lib proofs:: prove 5 ok; cargo fmt clean; clippy 1.97 –all-targets -D warnings clean; pre-push-check green on the clean worktree
Deviation: built and tested in a clean detached worktree (/home/user/nikaia-prove, sharing target/) because the shared checkout does not build: the dead agent’s dirty project.rs fails at project.rs:3053 (E0308 expected bool, found Result) against its own project_drive lowering; clippy 1.99.1 (CI’s) not run: 3.8 GB free disk, a second target dir does not fit; a build without a runner passes rounds = 0 and a runner closure that is never called (see Found, optional fn)
Found: #1092 met in prove_model: match asked { ProofsAsked::Refuted(model) => if lg_verify_model(arena, facts, goal, model) { model.values } else { null }, else => null } lowers Refuted(ref model) and rustc refuses moving model.values (E0507); probe /tmp/claude-0/-home-user-Nikaia/b7e2d91b-1a15-5371-a36e-8c201aeab2d2/scratchpad/prove-move/mv.nika (enum A { Refuted(M) }, same arm); model_of stays Rust until #1092
Found: new defect, a narrowed optional function cannot be called: fn go(n: i64, run: (fn(i64) -> i64 sync)?) -> i64 { match run { null => return n, r => { let v: i64 = r(n); return v } } } is refused NK1245 “can’t tell what type r(n) is” (also with let r = run ?? return n); prove() therefore takes rounds: i64 (PROVE_RUN_ROUNDS or 0) instead of run: (fn ..)?; the architect may judge whether that budget is a design or a way around
Needs: architect decision on the optional-fn call defect (file it); #1092 frees model_of
Changelog: none (self-hosting move, no language change)
Rs2nika: not scored (moved by hand, as the owner’s experiment asked)
Pushed: b3472b1b (move); this report in the commit after it
