chore(release): v1.4.0 — funcref-global miscompile fix, wsc.facts source, component reachability GC, committed lockfile - #329
Merged
Conversation
A correctness fix that should not have waited, the second half of proof-carrying facts, component dead-code removal, and the end of the floating-dependency class. Version 1.3.0 -> 1.4.0 (minor: new capabilities, no breaking API change). Release scope closed in rivet -- `rivet release status v1.4.0` reports cuttable, 3 artifacts, all verified: TEST-326-FUNCREF-GLOBAL-GUARD (new) #326 latent miscompile, guarded TEST-239B-COMPONENT-REACHABILITY-GC #239 Phase B TEST-WSC-FACTS-SOURCE #231 fact source Two traceability defects corrected rather than carried: * TEST-239B-COMPONENT-REACHABILITY-GC claimed `release: v1.3.0`, but Phase B merged AFTER the v1.3.0 tag -- the v1.3.0 tree contains none of its code (verified: zero occurrences of `reachability` in component_optimizer.rs at that tag). The artifact was asserting membership in a release that does not contain it. Re-scoped to v1.4.0; v1.3.0 is back to the 3 artifacts that actually shipped in it. * The #326 fix -- a latent silent miscompile of the #196 class -- had NO rivet artifact at all. A correctness fix with no verification node is precisely what the traceability gate exists to catch. TEST-326-FUNCREF-GLOBAL-GUARD added, linking REQ-1/3/5/12, and confirmed not flagged by `rivet check verification-evidence`. Cargo.lock updated for the version bump -- the first release since the lock was committed, and it behaved correctly. `rivet validate` PASS (44 warnings vs the 42 baseline; both additions are the id-naming-convention warning every existing TEST-* artifact already carries -- no new errors). The CHANGELOG carries an explicit "Not done" section so the remaining gaps (Phase B prunes core funcs only and has no behavioral differential, the fact source covers the straight-line prefix only, the validator is still a total model, #240's premise hook is inert) are stated rather than implied closed. Refs #231, #239, #320, #326, #323
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
1 participant
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.
Cuts v1.4.0 (1.3.0 → 1.4.0 — minor: new capabilities, no breaking API change).
Scope — closed in rivet
rivet release status v1.4.0→ ✓ Cuttable, 3 artifacts, all verified.rivet validatePASS.TEST-326-FUNCREF-GLOBAL-GUARD(new)TEST-239B-COMPONENT-REACHABILITY-GCTEST-WSC-FACTS-SOURCETwo traceability defects corrected rather than carried
TEST-239Bclaimedrelease: v1.3.0— but Phase B merged after the v1.3.0 tag, and that tagged tree contains zero reachability-GC code (verified). The artifact was asserting membership in a release that doesn't contain it. Re-scoped; v1.3.0 is back to the 3 artifacts that actually shipped.Headline: a correctness fix that is latent in v1.3.0
#326 —
ref.funcisn't in the dead-function sweep's liveness closure, and the global section is re-emitted verbatim, so a funcref global could be silently re-pointed after renumbering. Valid wasm, wrong behaviour, invisible to structural validation, and reachable by default on every core module. This is #196 with one variable changed: after that bug scrambled a function-pointer table through the element section, the element section was remapped — the identical hazard in the global section was never covered.Also in
wsc.factssection — loom forwards Z3-discharged invariants to synth #231 fact source —wsc.factsfinally carries facts (constants, masks, booleans). Literal point-ranges are suppressed: on a real component core that was 314 of 322 facts, i.e. ~97% restatement of what the consumer reads off the operator.Cargo.lockcommitted — ends the class that caused four red-main incidents, one pin re-floated three times. Its first release, and it correctly picked up the version bump.Not done — in the CHANGELOG, not implied closed
Phase B prunes core funcs only, no behavioral differential; the fact source covers straight-line prefixes only; the core validator is still a total operation model (refinement #300 and the solver migration #313 are v1.5.0); #240's premise hook is inert (#323).
Known systemic reds:
Rocq Formal Proofs,Verification Gate.