Skip to content

fix(p3-async): mixed-mode stackful, type classification, stream-write over-count#153

Open
avrabe wants to merge 1 commit into
mainfrom
fix/p3-async-detection-bugs
Open

fix(p3-async): mixed-mode stackful, type classification, stream-write over-count#153
avrabe wants to merge 1 commit into
mainfrom
fix/p3-async-detection-bugs

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented May 14, 2026

Summary

Second fix from the post-v0.8.0 Mythos delta-pass sweep. Three independent
defects in `meld-core/src/p3_async.rs`, all silent (no trap, no validator
catch).

The bugs

# LS Site Effect
1 LS-A-12 `uses_stackful_lift()` line 952 Mixed-mode component (one callback lift + one stackful lift) returns `false` because the derived predicate `uses_async_lift && !uses_callback_lift` collapses
2 LS-A-13 `StreamWriteResult::decode` line 813 `written >= requested` folds `n > data_len` into `Complete { written: n }` — caller advances cursor past source buffer
3 LS-A-14 `detect_features` line 964 `desc.contains("stream")` matches `future<stream>` → type lands in `stream_types`

Fixes

  1. LS-A-12 — New independent field `uses_stackful_lift_internal: bool`
    set per-lift in `detect_features`. `uses_callback_lift` (any lift has
    callback) and `uses_stackful_lift_internal` (any lift is stackful) are
    now independent. The dispatcher in `adapter/fact.rs` already routes
    per-site based on the merged module's `[callback]` companion,
    so this never reached the emitter — but downstream consumers following
    the public API would misroute. Bug shipped in feat(p3-async): stackful lifting ABI foundation (#140 phase 1) #146 / v0.8.0.

  2. LS-A-13 — Split `>=` check into three explicit arms:
    `==` → `Complete`, `<` → `Partial`, `>` → `Unknown(ret)`.

  3. LS-A-14 — Classify on the root constructor (prefix up to first `<`),
    not on substring containment.

Tests (4 new)

  • `stackful_lift_is_existential_over_lifts` — replaces the old
    single-lift truth-table test; covers the mixed-mode case
  • `ls_a_12_mixed_mode_component_reports_stackful` — end-to-end
    `detect_features` with both lift kinds
  • `ls_a_13_stream_write_over_count_is_unknown_not_complete`
  • `ls_a_14_future_of_stream_classifies_as_future`

Tier-5 gate

This PR touches `p3_async.rs` (Tier-5). The Mythos gate will fire and
request the `mythos-pass-done` label. The pass IS the work in this PR.

Test plan

  • `cargo test -p meld-core --lib` — 211 pass (208 prior + 3 new SR-32-cluster + 0 others moved)
  • `cargo clippy --all-targets -- -D warnings` — clean
  • `cargo fmt --check` — clean
  • YAML lint on safety/stpa/loss-scenarios.yaml
  • CI green on smithy
  • mythos-pass-done label applied

Note on overlap with #152

This PR is independent of #152 (extended-const fix). Both add entries
to `safety/stpa/loss-scenarios.yaml` and `CHANGELOG.md` Fixed section.
Whichever merges first wins; the other will need a small textual rebase
(additive only, no real semantic conflict).

Refs

  • LS-A-12 (UCA-A-3, H-1 / H-3)
  • LS-A-13 (UCA-A-5, H-1 / H-2)
  • LS-A-14 (UCA-P-10, H-3 / H-4)
  • Discovered by post-v0.8.0 Mythos delta-pass on `p3_async.rs`

🤖 Generated with Claude Code

@avrabe avrabe added the mythos-pass-done Mythos delta-pass completed on Tier-5 file changes; findings (or NO FINDINGS) attached to PR label May 14, 2026
@avrabe
Copy link
Copy Markdown
Contributor Author

avrabe commented May 14, 2026

Mythos delta-pass evidence

Tier-5 file touched: meld-core/src/p3_async.rs.

A fresh agent ran scripts/mythos/discover.md on the file in the post-v0.8.0 sweep, returning 3 findings (LS-A-12 / LS-A-13 / LS-A-14). All three have concrete PoCs that reproduce on current code; validation done via reproducing the PoC tests against pre-fix code (commits before f7dc651).

The agent also verified-and-rejected 3 priors (PAYLOAD_SHIFT docstring vs emitter, missing intrinsic variants, name typos) — those checks remain in the agent transcript and are NOT defects.

Adjacent findings not in this PR:

  • None — this PR fixes all 3 strong findings from the p3_async.rs scan.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 14, 2026

Mythos delta-pass required

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

meld-core/src/p3_async.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.

… over-count

Three independent defects in meld-core/src/p3_async.rs surfaced by the
post-v0.8.0 Mythos delta-pass on the file.

1. LS-A-12 — P3AsyncFeatures::uses_stackful_lift mis-classifies mixed-mode

   uses_stackful_lift() was derived as `uses_async_lift && !uses_callback_lift`,
   a conjunction of two component-wide existential flags. A component
   that declares one callback-mode async lift AND one stackful-mode
   async lift sets both flags to true, so the derived predicate
   returned false even though a stackful lift was present.

   Fix: new independent field `uses_stackful_lift_internal: bool` set
   per-lift in detect_features. uses_callback_lift remains "any lift
   has callback"; uses_stackful_lift_internal is "any lift is stackful".
   The dispatcher in adapter/fact.rs already routes per-site based on
   the merged module's [callback]<export> companion, so this never
   reached the emitter — but downstream consumers following the public
   API would misroute. Bug shipped in #146 / v0.8.0.

2. LS-A-13 — StreamWriteResult::decode folds over-count into Complete

   decode(ret, requested) classified any non-negative ret with
   `written >= requested` as Complete, including the out-of-contract
   `written > requested` case. A buggy or hostile runtime returning
   n > data_len would silently drive callers to advance their producer
   cursor past the source buffer.

   Fix: split into three explicit arms — `==` => Complete, `<` =>
   Partial, `>` => Unknown(ret).

3. LS-A-14 — detect_features substring matching misclassifies
   future<stream<...>>

   detect_features classified P3Async types via desc.contains("stream")
   / desc.contains("future"). A nested type future<stream<u8>> matched
   "stream" first and landed in stream_types instead of future_types.

   Fix: classify on the root constructor of the description (the
   prefix up to the first '<'), not on substring containment.

Tests (4 new):
- stackful_lift_is_existential_over_lifts (replaces single-lift test)
- ls_a_12_mixed_mode_component_reports_stackful
- ls_a_13_stream_write_over_count_is_unknown_not_complete
- ls_a_14_future_of_stream_classifies_as_future

LS-A-12 / LS-A-13 / LS-A-14 added to safety/stpa/loss-scenarios.yaml.
Discovered by the post-v0.8.0 Mythos delta-pass sweep (gate from #151).

Refs: LS-A-12, LS-A-13, LS-A-14

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
@avrabe avrabe force-pushed the fix/p3-async-detection-bugs branch from f7dc651 to 7941f3e Compare May 15, 2026 13:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

mythos-pass-done Mythos delta-pass completed on Tier-5 file changes; findings (or NO FINDINGS) attached to PR

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant