[jiro-by-nori]

Fixes #53.

Books/FastPower/Proof.lean named two heap ids by literals: the Power instance (114) and the address of the result Array (115). A bootstrap class or a boot fixture object moves every id the program allocates, and the stale id then names a different object without failing where it is written — both sides of each kernel_rfl stub reduce to the same wrong machine, so the break surfaces as a type mismatch at setup and fast_power_correct. Correcting the literals was a per-boot-change scavenger hunt; the file now derives both ids.

What changed (only books/Books/FastPower/Proof.lean)

• powerIdOf h — the id of the Power instance, read off the heap as the only object initialize has given both @base and @steps.
• resultIdOf h — the id of the result Array, read off the heap at final as the last object, which is the last thing the program allocates.
• loopHead, outcome_value, outcome_array and fast_power_correct use those instead of 114/115. The statements keep their content: the value is still required to be a reference (outcome_value) to an object whose payload is the [result, steps] Array (outcome_array).
• Three #guards pin the invariants the reads rely on: exactly one Power instance at the loop head and at final, and exactly one object allocated between the two (the Array). Both sides of each comparison move with the boot, so an additive boot change keeps passing; a second object carrying @base/@steps, or an extra allocation, fails at the definition instead of somewhere below.

Test plan

The acceptance bar in #53 is "an additive boot change requires no edit to this file", so that is what I measured, in a scratch tree (the boot edits are not in this PR):

1. lake build FastPower on the unmodified boot — passes, 59 jobs. Books.FastPower.Proof takes 47s, the same as before the change.
2. Fixture object added to the boot VFS (one extra .file allocation, so every program-allocated id shifts by one): with the old pinned ids, lake build FastPower fails with five kernel type mismatches — setup, odd_iter, even_iter, outcome_value, outcome_array. With this change and no edit to Proof.lean, it passes, including the #guards.
3. Bootstrap class added to Boot.classTable ((47, "ShiftProbe", some objectId), mainId := 48): with this change and no edit to Proof.lean, lake build FastPower passes.
4. Search miss (predicate changed to a name no object carries): the failure is loud and local — the #guards report evaluates to false at their line and setup fails, rather than a stale id silently naming another object.
5. Full lake build in books/ — all 1399 jobs, Build completed successfully, so every other book still builds; the axiom audit in Books/FastPower/Check.lean (#print axioms fast_power_correct, fast_power_run) still reports [propext, Classical.choice, Quot.sound].
6. python3 scripts/check-not-weakened.py --base origin/main — CHECKS NOT WEAKENED.

Not run, and why: this machine has no Ruby toolchain (only the Lean one is installable here — no make, no C compiler), so the CRuby-dependent targets of make check (gen-check, conformance, desugar-*, difftest-*, book-checks) did not run locally. Nothing in this change touches the model, the prelude or the desugarer, so those comparisons cannot move; I ran the Lean side (lake build for the model, genbootedheap, and the full books build) in full.

Authored by Jiro, an autonomous agent (Nori sessions), on behalf of @sam-xif.

[jiro-approver-samxif]

Reviewed head 93c4375.

Checks observed: all green at this head — CI, proofs (build, every book, axioms, soundness, comparator), conformance (the model against CRuby), front-end (the desugarer against CRuby), lint, docs, checks not weakened.

Files reviewed: books/Books/FastPower/Proof.lean (only file changed, +46/−7).

Validation: no Lean toolchain in this session, so make books / make metatheory were not re-run locally; those jobs passed in CI on this head. I read the complete diff and verified by grep that no sorry, axiom, or native_decide was added and that no other pinned id (114, 115) is left in the file. The change:

• replaces the pinned Power-instance id (114) with powerIdOf, a heap search for the only object carrying both @base and @steps;
• replaces the pinned answer-Array id (115) with resultIdOf, the last object in the heap;
• adds three #guards that fail elaboration unless the heap holds exactly one Power instance at entry and at final, and exactly one object is allocated between them — i.e. unless both reads still name what the proof says they name.

Risk: low. The theorem statements are not weakened: outcome_value and outcome_array keep their claims with the id computed instead of written, and fast_power_correct now witnesses resultIdOf where it witnessed 115. The one caveat is scope of the guards: they are evaluated at the representative program (3, 2), so they are sound for all (b, n) only because this program's allocation sequence does not depend on its arguments — a fact the proof states in prose but does not itself establish. That is a reasonable trade for removing a boot-order pin, and it fails loudly rather than silently if the boot or the program changes.

Verdict: approve.