# Fix v4.33 fallout in the ignored kernel suites: Prop-below call-site surgery + egress hints channel

[johnchandlerburnham]

Fixes the two failures in the post-v4.33 (#572) ignored sweep:

kernel-check-env       × Kernel check failed with 2 failure(s)
kernel-ixon-roundtrip  × 50 roundtrip mismatches

Both are latent bugs that the toolchain bump exposed, not regressions in #572
itself. Neither suite runs in PR CI (--ignored), so they surfaced only on a
local sweep.

Bug 1 — Prop-mutual .below families: ctors and below.casesOn had no call-site surgery (kernel-check-env)

The two failing constants were the _private.…BelowPredicate.{oddp,evenp}_nonneg.match_2
matchers from #571's Prop-mutual fixture, rejected by the kernel with
AppTypeMismatch at depth=0.

Mechanism. On a Prop-valued mutual inductive-predicate family,
IndPredBelow's .below is itself a mutual inductive whose parameters are the
parent params followed by the parent motives — in Lean's source member
order. Our canonical below family is generated from the canonical parent
recursor, so its motive-parameter order follows sort_consts' canonical class
order instead. The two orders coincided for EvenP/OddP until the v4.33
content hashes flipped the structural sort to (OddP, EvenP):

[compile.sort_consts] iter 1 → classes:      # BelowPredicate parent block
  c[0][0] …BelowPredicate.OddP
  c[1][0] …BelowPredicate.EvenP

User references to X.below heads are already reconciled by
below_call_site_plans, and X.brecOn by its derived plans. But a Prop-level
below family exposes two more user-referencable surfaces with the same leading
params, motives telescope, and neither had a plan:

• the below constructors (OddP.below.succ, EvenP.below.zero, …), and
• the regenerated X.below.casesOn wrapper.

Matchers compiled by structural recursion over the predicates reference both
with source-order motives. IX_APP_DIFF (see Bug 3) showed the kernel's
canonical OddP.below.succ receiving the EvenP motive where it expects OddP's:

f:    OddP.below.succ
a_ty: forall (n : Nat), EvenP n -> Prop     # what the matcher passes (source order)
dom:  forall (n : Nat), OddP  n -> Prop     # what the canonical ctor expects

Fix. Register the same derived BRecOnCallSitePlan under each below-ctor
name and the .below.casesOn name (Prop families only — Type-level .below
is a definition with neither), in the existing below_call_site_plans map.
The apply site discriminates the two telescope shapes by the key's last
component (below/below_N = head, which keeps its indices+major application
floor; anything else = family member, with no floor, since a field-less
below ctor like EvenP.below.zero is fully applied at exactly
params+motives). In both shapes everything after the motive segment is kept in
place, so the below branch now emits one identity tail — byte-identical
entries to the old fixed/extra split for heads. X.below.rec is deliberately
not registered: only regenerated wrappers reference it, and those skip surgery
via the aux-regen guard.

Mirrored in lockstep across the Rust and pure-Lean compilers (apply branch,
compile-side registration, decompile-side plan install — the latter derives
the ctor names from the parent inductive via the same suffix transplant
buildBelowIndcCtor uses, since the below inductive is not yet regenerated at
install time). CallSite metadata makes the rewrite self-describing, so the
decompiler restores the source-order spelling with no changes.

This keeps the canonicity architecture as documented (§9.3/§17.2: canonical
bytes are hash-sorted; the Lean-facing view is restored via surgery metadata),
rather than source-ordering the below generation — the alternative considered
and rejected because it would re-introduce source-order dependence into
canonical content.

Bug 2 — ixon_egress dropped the per-name hints channel (kernel-ixon-roundtrip)

The reported "50 mismatches" is compare_envs' error cap, not the total; all
were X.below.casesOn of inductive predicates (Nat.le, List.Forall₂,
Std.DHashMap.Raw.WF, …) whose IH binder decompiled as a bare ih where
v4.33's IndPredBelow now writes hygienic ih._@.<module>.<hash>._hygCtx._hyg.N
names.

Mechanism. kernel_egress.rs::rebuild_named copied a Named entry's
meta and original fields but dropped hints. Decompile reconstructs
DefinitionVal.hints from that per-name channel (absent → Opaque), and
roundtrip_block Phase B validates each decompiled aux constant's Lean-level
hash — which includes hints — against the source env. On the kernel egress leg
every regenerated .casesOn/.recOn/.below/.brecOn therefore failed that
validation (Opaque vs Abbrev; 4,846 spurious Pass-2 errors on a full env),
recovery's own hash check failed the same way, and the raw generated form
shipped in place of the metadata-restored one.

That substitution was invisible while raw regeneration was name-faithful. It
became visible once two things landed on top of it: #571's Phase-3b
below.casesOn regeneration (whose below-rec input is regenerated in the
decompile work env, where the original below ctors are not yet present, so the
IH binder name falls back to a bare ih), and v4.33's _hygCtx hygienic
binder names, which made the fallback diverge from the original for every
inductive predicate's below.casesOn.

Fix. One line: carry hints through rebuild_named (plus the doc
comment). Phase B's metadata restoration now lands, which also shields the
Lean-facing env from any future generation-side binder-name drift.

Bug 3 — the kernel's [app diff] dump was silently dropped

IX_APP_DIFF's AppTypeMismatch trace logged through the log facade, but no
log backend is installed in the CLI or test binaries — the same failure mode
#571's first patch fixed for the inductive.rs canonicity dumps. Emitted on
stderr now, with the failing constant's debug label in the header. (This dump
is how Bug 1 was diagnosed.)

Tests / tooling

• focusConsts gains the two BelowPredicate match_2 matchers, so
  kernel-check-const reproduces this regression class in ~10s
  (IX_KERNEL_FOCUS_CONST=match_2 lake test -- kernel-check-const --ignored).
• Tests/Main.lean gains a kernel-roundtrip-ns=<prefixes> special arg
  mirroring rust-compile: the same compile → ingress → egress → decompile →
  hash-compare pipeline as kernel-ixon-roundtrip, but over the transitive
  closure of the name-prefix-matched constants only.
  kernel-roundtrip-ns=Nat.le reproduced Bug 2 on a 98-constant closure in
  40 ms.

Verification

• kernel-check-env: 219,554/219,554 passed (was 219,549/219,551)
• kernel-ixon-roundtrip: 169,194 constants verified, 0 errors (the old
  run stopped at the 50-error cap partway through the env); Pass-2
  aux_gen diff errors: 4,846 → 0
• validate-aux: 0 failures; aux-gen-diff: all gates PASS (Lean/Rust
  byte-identical, incl. plans + parallel driver gates); decompile-diff: all
  gates PASS incl. callsite-replay
• Full sweep lake test -- --ignored --exclude=tc-pins,tc-accel-diff,tc-anon-diff,tc-init,tc-tutorial,tc-roundtrip,lean4lean
  → exit 0

Non-blocking observations

• The [compile_env] block FAILED inductBadNonSort*/inductTooFewParams/r6Host.mk
  stderr lines during the sweep are expected kernel-tutorial noise
  (intentionally-bad fixtures being rejected). However, r6Host is now
  rejected at compile time (missing constant: r6Host.rec_1 — the fixture
  env lacks the nested-aux recursor a real Lean env would carry) rather than
  by the kernel positivity descent it was written to exercise. Follow-up: give
  the fixture a dummy rec_1 so the R6 descent path is exercised again.

• X.below.rec heads and partial applications of below-family constants below
  the params+motives floor remain outside surgery's reach, matching the
  existing below/brecOn head behavior — such call sites fail loudly in the
  kernel check rather than silently miscompiling.

  Also in this PR

• style: rustfmt — one over-split chain in the new plan-registration code.

• ci: portable codegen for the GitHub-hosted rust-test job — the lint job's
  clippy failure was not a lint: since ci: !benchmark fixes #575 made .cargo/config.toml's
  -Ctarget-cpu=native authoritative in CI, the one job on the heterogeneous
  ubuntu-latest fleet could execute native-built cached artifacts (e.g. a
  tracing-attributes proc-macro dylib inside clippy-driver) on a runner
  without the builder's ISA extensions → SIGILL; nextest --run-ignored all
  had the same runtime exposure. Pin that job to -Ctarget-cpu=x86-64-v3
  (the GitHub-hosted AVX2 baseline) — RUSTFLAGS is in the rust-cache key, so
  this also re-keys away from poisoned caches. Warp jobs keep native per
  ci: !benchmark fixes #575's bench design. Affects every PR's CI, so this hunk can be
  cherry-picked to main independently if preferred.