diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ef7773..d0c227e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,108 @@ All notable changes to LOOM will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [1.4.0] - 2026-08-13 + +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. + +Every figure below was measured on this tree, not quoted from a prior report. + +### Fixed + +- **The dead-function sweep could silently re-point a funcref global (#326).** A + latent miscompile of the #196 class, present in v1.3.0 as shipped and reachable + by default: `optimize_fused_module` runs `eliminate_dead_functions` on every + core module. Two facts combined — `ref.func` is not in the pass's liveness + closure (`collect_function_refs_recursive` matches `Call` only), and the + encoder re-emits `global_section_bytes` **verbatim**, so a `ref.func N` frozen + there is never renumbered. A function referenced only by a funcref global was + therefore swept while the frozen index kept designating whichever function + inherited it: valid wasm, wrong behaviour, invisible to structural validation. + The sweep now **declines** such modules (unparseable global section counts as + hazard-present) until `ref.func` is a real root and the section is remapped. + Found while building #239 Phase B, and fixed before anything exercised it. + + Worth recording: 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. The lesson had been applied to the instance, not the class. The doc + comment had also claimed `ref.func` was a liveness root all along; the + documentation asserted a property the code never implemented, and nothing + compared the two. + +### Added + +- **`wsc.facts` now carries facts (#231).** v1.3.0 shipped the emitter and wire + format but nothing populated it. Three structurally-justified sources are + wired: constants, masks (`x & K` ⇒ `[0, K]` for any `x`, non-negative `K`), + and booleans (relops/`eqz` ⇒ `[0, 1]`). Facts remain value-keyed and + drop-safe; the default output is byte-identical (verified with `cmp` against a + binary built from the previous tag). + + Point ranges on operators that **are** literal constants are deliberately not + emitted — they restate what the consumer reads off the instruction the fact is + keyed to. On a real component core that is 314 of 322 facts, in a section that + ships into images measured in kilobytes. Derived point ranges survive: `x & 0` + is `[0,0]` on an `i32.and`, which cannot be read off the operator. + +- **Component-level reachability GC (#239 Phase B).** Mark-and-sweep over + exports → instances → aliases → canon → core funcs; function exports the + component never references are removed and their bodies swept. Motivated by + #303: `cabi_realloc` surviving into a Cortex-M3 image on an all-scalar + interface, where it is provably uncallable — measured downstream as unreachable + branches that no test can ever close, i.e. permanently open rows in an MC/DC + argument. Removal only; no adapter or canon behaviour is altered. Refuses + element-table modules and reference-typed globals, and no-ops rather than + guessing on anything it cannot resolve. + +### Changed + +- **`Cargo.lock` is committed (#320).** loom ships binaries, so the lock belongs + in the repository: builds become reproducible and dependency changes arrive as + reviewable diffs instead of resolving ambiently at CI time. This does not + freeze upgrades — it gates them. + + The bill that motivated it: four red-main incidents this cycle caused by + resolution rather than by any code change (`rand` 0.9→0.10, nightly fuzz deps, + an auto-merged `ordeal` bump that flipped a pin test, and `cranelift-isle` + re-floated **three times** past a comment in `Cargo.toml` explaining precisely + why not to). The third re-float arrived through a different Dependabot + ecosystem than the ignore meant to stop it. Per-pin ignores are whack-a-mole + against an automated player. + + It also matters for the claims: this project publishes "N/N rules proven, N + tests pass, these are the trusted axioms". Those numbers are only meaningful + against a known dependency set. + +- Dependabot `ignore` for `cranelift-isle` now covers **every** cargo ecosystem, + not just the root one. + +### Traceability + +Release scope closed in rivet: `TEST-326-FUNCREF-GLOBAL-GUARD` (new), +`TEST-239B-COMPONENT-REACHABILITY-GC`, `TEST-WSC-FACTS-SOURCE`. + +`TEST-239B-COMPONENT-REACHABILITY-GC` was corrected from `release: v1.3.0` to +`v1.4.0` — Phase B merged after the v1.3.0 tag, so the artifact had been +claiming membership in a release whose tree contains none of its code. + +### Not done — stated so it is not implied + +- Phase B prunes core funcs only. Unreachable canon lifts, aliases and component + types are not pruned; that needs component index-space rewriting, which would + reopen the #196 index-scrambling class. +- Phase B's evidence is structural (validation, export names, function counts). + No behavioral differential; that rides #238. +- The fact source covers the straight-line prefix of a function only — the walk + stops at the first structured control flow, because past that an + `instructions` index is no longer the emitted operator ordinal. +- The core validator still proves value equivalence over a **total** operation + model. Trap preservation remains a gate beside it plus static guards, not the + encoding. Refinement (#300) and the solver migration (#313) are v1.5.0. +- `#240`'s premise hook is inert (#323): `assume_max`/`assume_range` have no + non-test callers, so `fits_below_bit` cannot fire on real input. + ## [1.3.0] - 2026-08-04 Proof-carrying output, a trap gate that is actually on the runtime path, and the diff --git a/Cargo.lock b/Cargo.lock index 4e389fc..9d93237 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1476,7 +1476,7 @@ checksum = "0ceec5bc11778974d1bcb055b18002eba7f4b3518b6a0081b3af5f21666da9ad" [[package]] name = "loom-cli" -version = "1.3.0" +version = "1.4.0" dependencies = [ "anyhow", "clap", @@ -1489,7 +1489,7 @@ dependencies = [ [[package]] name = "loom-core" -version = "1.3.0" +version = "1.4.0" dependencies = [ "anyhow", "criterion", @@ -1511,7 +1511,7 @@ dependencies = [ [[package]] name = "loom-isle" -version = "1.3.0" +version = "1.4.0" dependencies = [ "cranelift-isle 0.132.3", "loom-shared", @@ -1519,7 +1519,7 @@ dependencies = [ [[package]] name = "loom-shared" -version = "1.3.0" +version = "1.4.0" dependencies = [ "anyhow", "cranelift-isle 0.132.3", @@ -1534,7 +1534,7 @@ dependencies = [ [[package]] name = "loom-testing" -version = "1.3.0" +version = "1.4.0" dependencies = [ "anyhow", "criterion", diff --git a/Cargo.toml b/Cargo.toml index b0c491d..9267f23 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ members = [ ] [workspace.package] -version = "1.3.0" +version = "1.4.0" authors = ["PulseEngine "] edition = "2024" license = "Apache-2.0" diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index 0f2a89b..02f08b2 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -530,6 +530,7 @@ artifacts: - run: | cargo test --release --lib -p loom-core --features verification -- mask_yields_zero_to_mask_range_fact constant_folded_value_yields_point_range_fact unjustifiable_values_yield_no_fact walk_stops_at_structured_control_flow value_deleted_by_a_later_pass_is_dropped_not_miskeyed facts_use_the_full_function_index_and_bool_range fact_collection_is_deterministic no_derivable_fact_means_no_section status: verified + release: v1.4.0 tags: [verification, proof-carrying-facts] links: - type: verifies @@ -633,7 +634,7 @@ artifacts: - run: | cargo test --release --lib -p loom-core --features verification -- test_239b_ status: verified - release: v1.3.0 + release: v1.4.0 tags: [v130, component-model, reachability-gc, safety] links: - type: verifies @@ -644,3 +645,48 @@ artifacts: target: REQ-12 - type: verifies target: REQ-3 + + # ============================================================================ + # #326 — a latent silent miscompile of the #196 class, found while building + # #239 Phase B and fixed before it could be exercised. `ref.func` is not in + # the dead-function sweep's liveness closure and the global section is + # re-emitted verbatim, so a funcref global could be left pointing at a + # different function after renumbering. The sweep now declines such modules. + # The CONTROL test is the load-bearing half: without it, a guard that always + # bailed would satisfy the primary assertion. + # ============================================================================ + + - id: TEST-326-FUNCREF-GLOBAL-GUARD + type: feature + title: dead-function sweep declines modules whose globals may hold ref.func (#326) + description: > + Verifies that eliminate_dead_functions REFUSES to sweep a module whose + raw global section may contain a `ref.func` initializer. Two facts made + this a silent miscompile: `collect_function_refs_recursive` matches + `Instruction::Call` only, so `ref.func` is not a liveness root; and the + encoder re-emits `global_section_bytes` verbatim, so a `ref.func N` frozen + there is never renumbered. A function referenced only by a funcref global + was therefore swept while the frozen index kept designating whichever + function inherited it — valid wasm, wrong behaviour, invisible to + structural validation. This is the same hazard #196 shipped through the + element section (remapped since); the global section was never covered. + An unparseable global section is treated as hazard-present. Paired with a + control asserting numeric-only globals still permit the sweep, so the + guard cannot degrade into a blanket disable without failing a test. + fields: + method: automated-test + steps: + - run: | + cargo test --release --lib -p loom-core --features verification -- t326_funcref_global_blocks_the_dead_function_sweep t326_numeric_only_globals_do_not_block_the_sweep + status: verified + release: v1.4.0 + tags: [v140, verification, safety, dead-code] + links: + - type: verifies + target: REQ-1 + - type: verifies + target: REQ-3 + - type: verifies + target: REQ-5 + - type: verifies + target: REQ-12