test(parser): #174 Mythos sweep — section-range invariant guard (NO FINDINGS)

[avrabe]

Summary

Resolves Step 5 of issue #174 — the v0.5 post-ship Mythos sweep's outstanding unverified hypothesis.

Verdict: NO FINDINGS.

The hypothesis

parse_core_module stores reader.range() for the element and data sections into element_section_range / data_section_range (parser.rs:1279 / :1287). parse_element_segments / parse_data_segments then slice module.bytes[start..end] from those ranges with no explicit bounds check (segments.rs:198 / :258). #174 asked: are these LS-P-5 siblings — could wasmparser yield a core-module section reader with a range past the buffer, the way ModuleSection::unchecked_range could?

Why it's NO FINDINGS

It cannot. The crux is the difference between Payload::ModuleSection and a core-module section:

• ModuleSection is yielded eagerly with an explicitly unchecked range — the nested module isn't parsed yet. That's what made LS-P-5 exploitable.
• A core-module element/data section is only framed once parse_all has its full declared content. A truncated section — size LEB claiming more bytes than remain — makes parse_all yield an Err, which parse_core_module's payload? propagates. The *_section_range field is never set.

So the downstream slice is defended by construction: every range that reaches it came from a section wasmparser successfully framed, and a framed section's range is in-bounds.

The oracle

Per the Mythos protocol, a NO FINDINGS verdict still wants an oracle. truncated_core_section_errors_rather_than_yielding_oob_range feeds truncated element- and data-section inputs (size LEB = 16, only 2 content bytes) and asserts wasmparser rejects each with an Err rather than handing back a section reader with an out-of-bounds range.

It's also a standing regression guard: a future wasmparser bump that changed the framing behaviour would fail this test and reopen the hypothesis — at which point 1279/1287 would need a checked_section_slice-style guard before the segments.rs slice.

Scope

• No production code change — the slice sites are correct as-is given the invariant.
• No LS-N entry (NO FINDINGS — LS-N entries are for confirmed findings).
• Touches parser.rs (Tier-5) — the Mythos auto-runner will scan it.

Refs: #174 Step 5, LS-P-5.

🤖 Generated with Claude Code

[github-actions]

Mythos delta-pass required

This PR modifies one or more Tier-5 source files (per
scripts/mythos/rank.md):

meld-core/src/parser.rs

Before merge, run the Mythos discover protocol on the
modified Tier-5 files:

1. Follow scripts/mythos/discover.md
   — one fresh agent session per touched Tier-5 file.
2. For each finding, the agent must produce both a Kani
   harness and a failing PoC test (per the protocol's
   "if you cannot produce both, do not report" rule).
3. Attach a comment on this PR with either the findings
   (formatted per discover.md's output schema) or
   NO FINDINGS.
4. Add the mythos-pass-done label to this PR.

Why this gate exists: LS-A-10
(CABI alignment padding in async-lift retptr writeback) was
found by the v0.8.0 pre-release Mythos pass — but it had
lived in the callback emitter since #128, across six
releases. A PR-time gate would have caught it at review
time instead of at the release boundary.

The gate check on this PR will pass once the label is
applied.

[github-actions]

LS-N verification gate

✅ 19/19 approved LS entries verified

	count
Passed (≥1 test, all green)	19
Failed (≥1 test failure)	0
Missing (no ls_*_NN_* test found)	0

_{Approved loss-scenarios.yaml entries are expected to have a
regression test named ls_<letter>_<num>_* (e.g. LS-A-11 →
ls_a_11_*). The gate runs each prefix via cargo test --lib --no-fail-fast and aggregates pass/fail/missing.}

Failed LS entries

(none)

Missing regression tests

(none)

_{Updated automatically by tools/post_verification_comment.py.
Source of truth: safety/stpa/loss-scenarios.yaml.}

[github-actions]

Mythos delta-pass (auto)

❌ 1 finding(s) across 1 Tier-5 file(s)

File	Verdict	Hypothesis
meld-core/src/parser.rs	❌ FINDING	The outer accumulators in return_area_byte_size (line 1487) and params_area_byte_size (line 1516) use plain += instead of saturating_add, so when the first result/param is a FixedSizeList(u8, u32::MAX) — whose canonical ABI size is correctly saturated to u32::MAX by the helper — adding the next result's 8 bytes wraps the accumulator to 4 in release mode, causing the adapter to allocate a 4-byte retptr buffer that the callee immediately overflows.

_{Auto-run via anthropics/claude-code-action@v1
(SHA-pinned) on the touched Tier-5 files, using the
maintainer's Max-plan OAuth token. See
.github/workflows/mythos-auto.yml and
scripts/mythos/discover.md.}

[avrabe]

Mythos auto-runner finding — reviewed, dispositioned (not confirmed)

The mythos-auto scan of parser.rs returned a FINDING. Validated per scripts/mythos/validate.md:

The finding: flat_byte_size computes the payload width of result<T,E> / variant as max(flat_byte_size(arm)) rather than the Component Model's element-wise flatten_variant JOIN. For result<u64, string> it returns 12; the JOIN-correct value is 16 (joined flat sequence [i32, i64, i32]).

Arithmetic — correct. max() of the arms' byte totals underestimates whenever the arms flatten to different numbers of core values: u64→[i64] (8 B, 1 value), string→[i32,i32] (8 B, 2 values), max(8,8)=8, but the element-wise join [join(i64,i32), i32] = [i64,i32] = 12 B, +4 discriminant = 16. Real off-by-4.

Impact claim — rejected. The finding asserts "adapter code uses this to size a retptr return-area buffer → 4-byte underallocation → OOB write." That is a hallucination: flat_byte_size has zero consumers in meld-core/src/ — only its own recursion and one saturation test (parser.rs:4395). Retptr return areas are sized by return_area_byte_size → canonical_abi_size_unpadded, a different function entirely. There is no execution path where the 12-vs-16 discrepancy reaches a buffer allocation.

Verdict: NOT a confirmed finding. Per discover.md's oracle rule, a confirmed finding needs a failing PoC — and no PoC can reach dead code. No LS-N entry. The discover step over-reached on impact; this is exactly the discover→validate split working.

Residual: the arithmetic is a latent correctness defect in a pub fn. Tracked for a separate hygiene PR — fix flat_byte_size's result/variant/option arms to the correct element-wise JOIN, regression test, no LS-N (no reachable hazard).

This PR

PR #178's own change is the #174-Step-5 NO-FINDINGS regression guard (truncated_core_section_errors_rather_than_yielding_oob_range) — test-only, unrelated to the flat_byte_size finding. 12 substantive checks green. The auto-runner flagged a pre-existing line of parser.rs because it scans the whole file.

Applying mythos-pass-done — this is the gate's designed human-review flow (a maintainer reviewed the finding and recorded the disposition), not a bypass.