[afflom]

Rule30 needs the typed Host interface and practical kernel verification on release/v0.5. This PR ports Host from #389, uses kernel evaluation for closed decisions, and makes bounded byte slices and string joins reducible in the kernel. Runtime changes are authored in LexLean core notation.

• Host is byte-identical to Integrate Host request types and deep package export/replay #389 at afe1a002f218f0eba9ee3f309793d135c45e5e7d. SL-12 covers its fourteen request constructors, eight events and incompatible environment-field mutation. It establishes source types; native host execution and the generated effect driver remain unfinished.
• Closed decide{} proofs and generated data checks use decide +kernel. SM-04 retains recursive computation and false-mutation coverage.
• Byte slicing preserves bounds while taking/dropping the underlying byte list. SM-19 checks a 1,962-byte slice, empty/end cases and a changed expected byte.
• String joining uses a list case and left fold over String.append, preserving the [propext] computational policy and delimiter. SM-19 covers empty, singleton, Unicode and nested joins, including rejection of a missing separator.

The slice and closed-decision regressions retain the fixture's normal timeout. Their former five-second override also failed during prerequisite runtime compilation in CI; these cases establish correctness and mutation rejection, not a five-second performance guarantee.

The runtime/source delta was independently reviewed at 84e38cb0230a1e0f52302f0d144ce10f2d5279c5. It retains the release/v0.5 base a8ad0588155881d6a5437f0bb18c5e05438d1bea, Target and κ source/register changes. Compiler identity remains 0b48547157a44c7dafdc0c59cfd270f185a6a172b83bb42e5af79323d4fb84eb. The source-only follow-up 61b776861c9d51be6776b184ace9ae42c12fee09 enumerates exactly the registered SL-01 through SL-08 and SL-12 claims in README; all existing coverage and duplicate checks remain intact.

Previously recorded official regeneration on that source completed all five production export projects, normalized verification for all 23 projects in without:uor-atlas (2,394 records), goldens including Atlas build artifacts, and model validation. That record does not claim a local Atlas verification pass.

The completed old-head CI run 41702745654 had 28 successful and six failing jobs. Its only failing tests were EX-07 and RP-11: six stale fixture identities and the README range contract. All four platform jobs corroborated those two failures only (481 conformance tests passed on each); rest had 305 passing tests and only RP-11 failing, and production had 38 passing tests and only EX-07 failing. These failures remain part of the evidence; they are not a passing final-head gate.

The missing official fixture phase is now complete:

• Frozen xtask check-fixtures --write ran once, completing all 313 fixtures in 1033.60 seconds. All 2,400 fixture input entries, case invocations/environments, diagnostic-code arrays and exit codes were preserved. Exactly twelve files changed: command/diagnostic expectations in certificate-{b,e}-rejected, certificate-rejected, certificate-heartbeat-rejected, certificate-resource-exhausted and production-expectation-stale. Every change is the observed certificate/source identity; no expected output was edited by hand.
• Both executables were frozen from the reviewed source. Cargo-selected root probes matched the intended checkout and all 905 selected embedded inputs matched admitted bytes; no cleanup or provenance repair was required.
• The first orchestration stopped after the successful writer because its strict comparison omitted the heartbeat identity's two typed diagnostic source-path occurrences. Original logs, snapshots and failure results were retained. Independent review established only the already-observed identity substitutions. A separate validation-only continuation used the exact module/path contexts and preserved all other bytes; it did not repeat the writer.
• The continuation passed model validation (483 IDs, 86 codes, documents current and audits clean), formatting and whitespace checks. A correctly rooted conformance harness selected exactly RP-11 and ran it once: one passed in 0.04 seconds, 482 filtered out.

The final changed head still requires its complete acceptance gate and CI before merge. No complete local just vv or final changed-head CI pass is claimed by this update. The reviewed final update is ready to request that full CI run; merge remains blocked until the required checks pass.

This existing PR addresses #409 only when the accepted change lands. #382, #271, #376 and #301 remain open; native host execution, runner integration and durable publication are separate work. Rule30 continues on its accepted pinned fork while this upstream change is reviewed.

Closes #409.

Final reviewed head: b87ec90f1ddcc33d5558e8bf7776f188a9005659.
Final reviewed tree: 7f85850a6f94f540183e26b9540741a790a46920.

[afflom]

Readiness review at f679376: the successful run 41591030034 is the draft rest partition, not the full gate. There is a concrete stale verification oracle to fix before spending the full-gate run: stdlib/expected/build/manifest.json now has semantic ID beginning 2b985ca7810f112d4c6594714b56ca97, while stdlib/expected/verify/probe/ still contains LexLeanProbe.Pa1474e03900bac4ced36f5859f18cfc6.lean. Verification derives those module names from the current semantic ID, and the examples leg includes stdlib and compares the normalized tree exactly.

Keep this draft until the official cargo xtask verify-examples --write refresh is completed and reviewed on the integration head, then request the full gate once. The evaluator change retains kernel replay and axiom auditing; no additional source correctness defect was found in this review. This does not close #376: decide +kernel alone does not address its hidden byte/string primitive bodies or reflexivity case. The Host interface remains a types slice, with #271's driver/effect work separate.

[afflom]

New integration dependency: draft #405 / issue #404 now tracks the overdue full release/v0.4 → release/v0.5 forward merge, pinned at b37bd79 against 2849449. It includes 122 source-only commits and 553 audited conflict paths; it is not a docs-only or Host-only port. This PR remains the owner of its byte-proof/runtime changes and disclosed incomplete regeneration. Coordinate the final v0.5 integration with #405 and #389's Host+Order/#402 wave so the identical Host module and official artifacts are reconciled once, without starting a parallel regeneration. No integration resolution or new regeneration has been started.

[afflom]

Forward-integration namespace decision from #405's source audit: please move this PR's Host-interface claim from SL-09 to SL-12 before the final integrated writers/gate. Landed Numeral owns SL-09, Order owns SL-10, and #363's current model confirms Json already reserves SL-11. Host interface coverage, Numeral, and #389's PD-10 effects/constructor eligibility are distinct claims; none should be dropped as duplicate merely because Host source is byte-identical.

Update the normative spec/src row and all generated register/table/scenario/dispatch/test/prose references together, following v0.5's source-authority workflow. This coordinates the existing required integration; it does not request an extra independent identity regeneration.

[afflom]

Current-head CI now supplies a concrete regeneration failure set. At 1cf52d6, run 41627026372 / rest job 125889688837 completed with 298 conformance cases passing and six failing after 3459.29 s. EX-09 reports helpdesk classify/package.json differing from the committed export; SL-01/02/05/08 report stdlib ends_with/package.json differing; RB-07 reports no committed verification for compiler/rust/rust-std/adt-evaluation build d318bd2252d4e98ddb5136ded3a930ec1697a638e57d81f5afc160e0c9eee4c5.

These failures are consistent with the disclosed unfinished export/fixture/verification writer phase. They are not evidence for changing acceptance or rerunning the same head. Keep the draft; complete the coordinated official writers with a stable executable, then compare those affected artifacts before requesting the final full gate. This run was only the draft rest partition; honesty and reproducibility passed. The existing SL-12 and #405 integration requirements still apply.

[afflom]

Maintainer self-review of this head: rebased onto a8ad058 and preserved the release line's new κ source/register changes; moved the Host claim to SL-12 to avoid the numeral claim; regenerated specification/model projections through the official project API; refreshed all five production export packages, 2,394 normalized verification records across the 23-project without:uor-atlas partition, and golden artifacts through official writers. Model validation passes with 483 IDs and 86 diagnostics. Generated records were transferred only after checking matching compiler inputs and exact κ source/lock bytes. The published tree matches the locally committed tree b68a09af3b51bff9116e1dbec957dd50b1868c55. Full uor-atlas verification and the full normative gate are not claimed; this remains draft pending exact-head CI and remaining acceptance work.

[afflom]

Independent bounded delta review found no new concrete source blocker. The merge base is current v0.5 a8ad058; Target and κ source are retained. Host matches #389 byte-for-byte and SL-12 is consistent across normative/register/scenario/dispatch/test references. Normalizing the runtime reference graph identifies exactly the intended instSliceableByteArray and join body changes, retaining the slice bound and delimiter-bearing left fold. Kernel evaluator selection and true/false coverage remain present.

Artifact checks support resolution of the prior failures: all 24 committed verification probes match current build semantic IDs, including the formerly missing compiler d318bd2252d4e98ddb5136ded3a930ec record. All five export projects refreshed; sampled ends_with/classify/bootstrap provenance hashes and source IDs match current manifests. The 19 changed compiler negative JSON fixtures alter only source identities. This is an artifact consistency review, not an independent rerun of the official writers.

Honesty/reproducibility passed; full ready CI41702745654 remains required, including Atlas and the previously failing cases. Keep the current run; no unchanged-head rerun or another regeneration is requested. Scope stays #409 only, with #382/#271/#376/#301 open. The earlier self-review's draft wording predates readiness; this COMMENT is not self-approval or merge clearance before complete final-head evidence.

[afflom]

Final-head CI41702745654 has concrete blockers; returning this PR to draft while they are corrected. This is a self-authored COMMENT, not approval.

Production126151210575 fails EX-07 on six stale fixture outputs: certificate-{b,e}-rejected, certificate-rejected, certificate-heartbeat-rejected, certificate-resource-exhausted, and production-expectation-stale. The first five retain LLV7015/7016/7013/7013/LLS8002 respectively but have new generated certificate identities; the last retains LLC0204 with a new source identity. Compared observed/expected JSON is otherwise identical after identity normalization. Complete the official fixture writer against this exact source; do not hand-edit expected output or weaken assertions. The PR records export, verify, golden and model writers but does not record this fixture phase. Coordinate it after the active Host phase; no concurrent identity wave or unchanged-head rerun.

Rest126151210865 fails only RP-11 (305 pass): README claims SL-01..SL-08, SL-12, whereas the existing range contract requires a range to reach the registered family's last ID, now SL-12. Enumerate the nine actually registered SL claims explicitly for this existing PR; do not claim absent SL-09/10/11 or relax coverage/duplicate checks to pass. ARM Linux, Windows and Apple Silicon corroborate EX-07/RP-11 only (481 pass on each).

Keep the current remaining job intact for evidence. After these narrow corrections, review their exact delta and run the final changed-head acceptance once. #409 stays open; #382/#271/#376/#301 remain out of closure scope.

[afflom]

Reviewed source-only follow-up for this PR/#409 is available at 61b776861 on maintainer/396-fixture-followup, based directly on 84e38cb. It explicitly enumerates the nine actually registered SL claims in README and records the six EX-07 identity mismatches in VERIFICATION.md. Static source review confirms exact SL register coverage without duplicate references; the RP-11 gate is unchanged. No expected output or diagnostic bytes were edited; all other source and expected bytes are preserved.

The existing owner still needs the official cargo xtask check-fixtures --write (just fixtures-write) after the active Host phase releases the shared lock. There is no supported per-fixture selector. Use a stable executable from the admitted compiler inputs and record its hashes and compile-time repository root, fixture input preservation, actual writer result and reviewed output delta. CI's six expected/observed JSON pairs are otherwise identical after identity normalization, with their existing diagnostic codes and exit classes preserved.

This branch publishes only the reviewed source correction; the contributor branch is unchanged and no separate PR was opened. No Cargo/build/writer or new CI was run for this follow-up. Integrate it into this existing PR, complete the coordinated official fixture phase, review the exact delta, and then obtain the final changed-head acceptance gate. #409 remains open; this comment is coordination evidence, not acceptance or merge approval.

[afflom]

Maintainer follow-through: I will carry the already-reviewed61b776861 correction and the missing official fixture phase forward through this existing PR. The full run has now finished: Intel corroborates the same EX-07/RP-11 failures only (481 passed,2 failed); no additional source cause was found.

The fixture phase is being prepared for the existing source/identity, after the active Host phase and already-queued #391 focused validation release the shared execution lock. It will use frozen executables with actual selected-artifact/root provenance, preserve fixture inputs and diagnostic/exit semantics, and review the official writer's output delta before publication. No new identity change, concurrent writer, duplicate PR or unchanged-head rerun is planned. If another maintainer is already executing this exact phase, please record its source SHA and phase ownership here before another run starts.

[afflom]

Final maintenance delta independently reviewed and published through this existing PR. Head b87ec90 has tree 7f85850a6f94f540183e26b9540741a790a46920; it preserves 84e38cb and current release/v0.5 a8ad058 ancestry. The 14-path delta from 84e is README, truthful VERIFICATION evidence and twelve official fixture outputs. All 2,400 fixture input entries, diagnostic codes and exits are unchanged; only the six observed certificate/source identities changed. The all-313-fixture writer ran once; the validation-only continuation passed model 483/86, fmt and exact RP11 (1 passed, 482 filtered). The initial strict output-audit omission remains recorded; no writer rerun or hand-edited expectation was used. Marked ready to request the full changed-head CI gate. This COMMENT is source/artifact review, not self-approval or a claim that full CI passed. Merge and #409 closure remain blocked on complete final-head and merged-tree evidence. #382/#271/#376/#301 remain open.

[afflom]

Final merge review: full CI41753286666 completed successfully with all34 jobs, including Intel macOS126323654209; exact-head honesty41753256085 and reproducibility41753256216 also passed. Fresh ownership/comments/reviews/head/base checks found no new blocker. The reviewed head and GitHub synthetic merge19ce114d both have tree7f85850a6f94f540183e26b9540741a790a46920; independent local merge-tree agrees, with current release/v0.5a8ad058 as first parent. Prior source/artifact reviews and the official fixture correction remain applicable. This is a self-authored COMMENT, not self-approval. Proceeding with the expected-head merge, then checking the actual tree before explicitly closing scoped #409. #382/#271/#376/#301 remain open.