decoder: remove dead stub-immediate path, fix stale docstrings - #127
Merged
Conversation
`stubImmediateCount` unconditionally returns `none` (all GC ops are decoded for real now), which makes the `some n => consumeStubAtoms …` branch that calls it statically unreachable and `consumeStubAtoms` dead. This removes both and folds the branch to its only reachable arm (`.ok rest`), keeping the live `consumeBrOnCastImmediates` case untouched — behaviour is unchanged. It also refreshes several comments that no longer match the decoder: the top-of-file and `parseModule` docstrings (type/table/memory/global/elem/data/tag content is fully parsed now, not discarded), the `parsePlainOp` catch-all (floats and SIMD are modelled; the fallback only stubs still-unmodelled proposals like atomics), and the `isMemOp` comments (memory ops emit real load/stores).
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-127.vercel.app (This URL is stable for this PR — it always points to the latest build of 89cfc64.) |
El3ssar
marked this pull request as ready for review
July 6, 2026 16:31
Address code-review findings on the decoder cleanup and the new slice corpus: - Wat.lean: the module-header and `parseModule` docstrings claimed non-func imports are "dropped"; they are in fact parsed into `globals`/`tables`/`memory` and recorded in `importedGlobals`/`importedTables`/`importedMemories`. Reword to match. Also remove the now-unreachable `br_on_cast` arm in the `parsePlainOp` fallback (handled by an explicit arm) and its orphaned `consumeBrOnCastImmediates`. - Array trunk: add chunk-generic `unSliceBodyTerminates`; `isEmptyBodyTerminates` and the new symmetric `lenBodyTerminates` are one-line instances, so the `len` callee bridge no longer hand-rolls the `of_returns_wp` glue. Drop the now-unused op-specific `lenBodyWp`/`isEmptyBodyWp` (subsumed by the generic `unBodyReturnsWp`). - RustArray/Spec.lean: bridges first, internal specs reuse them at `initialStore` (matching RustArrayTests) instead of duplicating the callee term. - Add `open_slice_export` macro factoring the uniform export-proof head; apply to all six slice export proofs. Verified: codelib and programs both `lake build` clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
mfornet
approved these changes
Jul 14, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
decoder: remove dead stub-immediate path, fix stale docstrings
stubImmediateCountunconditionally returnsnone(all GC ops are decoded forreal now), which makes the
some n => consumeStubAtoms …branch that calls itstatically unreachable and
consumeStubAtomsdead. This removes both and foldsthe branch to its only reachable arm (
.ok rest), keeping the liveconsumeBrOnCastImmediatescase untouched — behaviour is unchanged.It also refreshes several comments that no longer match the decoder: the
top-of-file and
parseModuledocstrings (type/table/memory/global/elem/data/tagcontent is fully parsed now, not discarded), the
parsePlainOpcatch-all(floats and SIMD are modelled; the fallback only stubs still-unmodelled proposals
like atomics), and the
isMemOpcomments (memory ops emit real load/stores).