[P1] [SPX-AI-004] Add a bounded feature-combination and differential backend conformance corpus

SPX-AI-004 — Add a bounded feature-combination and differential backend conformance corpus

Priority: P1 | Workstream: reliability | Import action: New implementation issue
Planning baseline: wavect/semaprax@ae25c6a49dc09ec4613c7a6f52a27daa69dcd3f3 (11 September 2026).
Implementation prerequisites: SPX-AI-003
Important: prerequisites mean the required implementation/evidence is accepted, not merely that its GitHub issue exists.

Outcome

Test composition rather than only isolated language features. Detect disagreements in values, status, evaluation order and ownership settlement across interpreter, native C11 and Core Wasm using a deterministic, reviewable corpus.

Current evidence and distinction from existing work

The two reported bugs concern combinations of already-admitted views, calls, profiles and matching. AGENTS.md requires equivalent checked behavior on claimed backends and canonical cleanup order. The project already has extensive owned-data and replay harnesses; this issue extends them rather than replacing them.

Read these owners first

Directory pointers are navigation roots. Resolve current files with rg --files; proposed new files must follow the current module ownership. The referenced snapshot may be older than the implementing branch.

Bounded scope and non-goals

Use finite explicit cases plus bounded seeded variation. Cover supported combinations and stable rejection for unsupported ones. Do not pretend every Cartesian-product combination is already admitted; do not add live hostile targets or exploit payloads. Local compiler-generated malformed fixture tests remain confined to this repository.

Implementation steps

Define dimensions: view origin, local/call/return use, conditional/loop/match context, ownership transfer, imported/standalone route, profile and backend. Start with pairwise coverage plus the known high-risk multi-way cases from Core Wasm: byte_range inside a while body emits a corrupt slice carrier #100/useful-text-consumer.v1 cannot resolve core.option, so byte_get is unusable in std.text #101.
For each admitted row store a source fixture, expected value/status and ordered semantic events. For unsupported rows store the existing diagnostic expectation; never count a rejected valid scenario as a passing execution test.
Reuse current fixture builders and cleanup/accounting probes. Normalize only nonsemantic host details when comparing outcomes; do not erase status codes, active-variant data, ordered calls or owner counts.
Add bounded seeded input variation around zero/one/maximum size, empty/nonempty branches, allocation failure points and short-circuit behavior. Keep seeds and input bytes in failure logs.
When a mismatch occurs retain the failing source, input, compiler identity and backend command. Provide a deterministic reduction helper or documented manual reduction sequence; preserve the original unreduced fixture.
Add a fast required smoke corpus and a broader explicitly provisioned job using the existing CI ownership. Derive expected case counts from the manifest and assert that every selected row executed.
Add an intentionally wrong test-only implementation or expected-result mutation that the harness must detect. Keep independent acceptance expectations outside the backend being tested.

Required tests and failure cases

Exact result and sticky status agreement for all admitted rows on every selected backend.
Evaluation once and left-to-right order around nested owner-producing calls; lazy branches remain unexecuted.
Zero live owners after success, rejected allocation and contract failure, with no duplicate settlement.
A fixed seed reproduces the same failing input and classification.
Missing rows, unavailable required tools, zero test selections and a deliberately altered result all fail visibly.

Starting commands

Run these from the implementing checkout. A command containing /absolute/path/... requires an explicit local output path. Use the current --help for option details and verify that test filters select actual tests. These are starting points, not a claim that this pack executed the compiler.

cargo test --locked -p semaprax --test owned_data -- --list
cargo test --locked -p semaprax --test project -- --list

Definition of done

A finite auditable composition matrix is enforced in CI.
All failures retain sufficient replay data and do not disappear through normalization.
The corpus augments existing invariants rather than lowering admission or support requirements.

Guardrails for the implementing agent

Read the current AGENTS.md, affected RFC/specification, completion rows and architecture owners before implementation. This pack is pinned planning input, not permission to ignore newer code or decisions.
Use a private worktree and a private CARGO_TARGET_DIR inside it. Do not use git stash, overwrite sibling worktrees, or share compiler/test scratch output. Add tests to the existing owning harness, not a new compiler-linking top-level test binary unless repository rules require it.
Preserve source/graph/schema compatibility where contracted, left-to-right evaluation, lazy operands, ownership transfer, canonical cleanup order and sticky failure. Do not weaken tests, diagnostics, range checks or authority checks to get green.
A proposed new shape/API below is a design target, not a claim that syntax or a command already exists. Run --help and discover exact test selectors. Zero selected tests, unavailable tools and skipped required rows are not execution evidence.
Keep model output as untrusted data; compiler facts and evidence never mint capabilities. Human support/publication decisions, paid model calls and real registry/Git writes require their own explicit authority.
Reuse implemented Agent v2, migrations, iterators, closures, semantic candidates, persistent HIR cache and hosted PG grammar/metadata work. If the requested slice already landed, verify its gate and close only the residual gap rather than building a competitor implementation inside this repo.

Evidence to attach before closing

For the implementation handoff, include: exact starting and finishing commit; changed files and their owning invariants; the pre-fix failure or negative-control result; exact commands, exit status and nonzero selected test counts; target/toolchain/provider identity; artifact/log locations; and remaining limitations. Run the repository's complete required quality profile (scripts/quality.sh full on supported Unix, or the documented platform equivalent) before merge. A local focused pass is not hosted evidence and a green framework is not a completed model experiment. For architecture/ABI/ownership changes, obtain independent semantic review before promotion. Do not mark an execution issue complete using authored tests or documentation alone.

test(differential): add a bounded view/ownership feature-composition …

fix(std,tests): correct a false admission claim about byte_range in a…

Landed on main (merge b7e9d191, commit d39683d6). Not closing — one composition dimension is bounded out by a backend capability, and that bound is worth keeping visible.

Tranche 1 — the ordinal-timing lead inherited from #240

Investigated whether interpreter/Wasm's batch-gated recording versus native's record-then-check also affects LeafAllocationStarted, LeafAllocationCommitted and LeafPayloadCopied, not just the InputValuePrepared that #240 pinned.

Confirmed by reading InterpreterProvider::input_prepare: injecting on any of the three sets fail_after and breaks the loop before machine.prepare_input() — the single call that records the whole batch — ever runs. So interpreter and Wasm show none of the four batched labels, while native's spx_pg_fill_leaves records each label immediately before its own check, so the injected-upon label always appears.

Verdict: SPECIFIED — a permanently permitted difference, for the same architectural reason #240 declined to fix InputValuePrepared. Reconciling it means reworking one engine's injection-timing architecture, not patching an ordinal. Now pinned as an exact assertion in compare_case, with three negative controls, one per label, proving each assertion is real and failable. The existing full-corpus test still passes with the new assertions active, so the predicted trace shapes hold in practice, not only in the reading.

Tranche 2 — the bounded composition corpus

Bound: 2 × 3 = 6 cells, enumerated in full — view origin (whole buffer / byte_range sub-view) × context (if / while / match). With two to three values per dimension, full enumeration is smaller than a pairwise covering array and every cell is independently meaningful, so pairwise would have cost coverage for nothing. Plus one case generalizing #100's own shape, and a separate borrow-versus-transfer ownership pair. All differential: same source, same call, values compared exactly across engines.

Findings:

The 6-cell matrix and the growing-range-in-while case: interpreter, native -O0, native -O2 and Core Wasm agree exactly. No divergence.
Ownership route (borrow-only vs. real own Bytes transfer): interpreter and native agree exactly. Core Wasm is bounded out for a verified reason, not neglect — wasm::build_web_with_scalar_exports's whole-program Public Scalar Export Profile v1 rejects Match, ByteRange, and any non-Value-ownership binding anywhere in the program. Confirmed empirically: an earlier draft hit SPX-W115 … binds a non-value scalar on an ordinary let view = bytes_as_slice(data) local. No per-function multi-dispatch Wasm build exists in this repository that admits Bytes/view/Option composition. Documented as an architectural bound rather than silently dropped — an uncompared engine must never look like an agreeing one.

The finding that corrected an error of mine

Writing the byte_range-in-while case, the first draft was a rejection test — and it passed compilation instead of failing. Reading the validator showed why: ResolvedExprKind::ByteRange has its own admission arm in hir::validation::iterator_loops requiring an authenticated byte-slice alias, and never reaches require_admitted_while_operation at all.

Rather than deleting the false test, the lane ran the now-admitted shape differentially across all four engines — all agree exactly, so this is a stale claim, not a latent bug. I have since verified it directly myself, corrected the comment in std/data-toml/src/toml.spx (commit 130d7dd8), and posted a correction on #218, where I had repeated the false claim.

Evidence class: local re-runnable, clang and node present, no hosted run. settlement_corpus → 13 passed (10 pre-existing + 3 new controls); scalar_status_backend_equivalence view_ownership_composition → 3 passed.

Remaining for closure: the Core Wasm ownership-transfer cell, which needs either a widened Public Scalar Export Profile or a per-function multi-dispatch Wasm build. That is a profile-spec decision, not a test to write.

ci: arm three test-lane require flags that no workflow ever set

Audit of this issue's corpus against its own Definition of done and its seven implementation steps. Not closing — but a real CI-enforcement defect it exposed is fixed and pushed as ed29319e.

What is genuinely met

Item	Verdict	Evidence
DoD 1 — finite auditable matrix (structure)	MET	`view_ownership_composition.rs:278-286` (`CASES`, explicit 2×3 + 1), `:350` (`OWNERSHIP_CASES`), `scalar_status_backend_equivalence.rs:96-130` (`EXPORT_IDS` + `EXPECTED_TRANSCRIPT`, 15 explicit rows) — real enumerable manifests, not logic implicit in test bodies
DoD 2 — replay data survives normalization	MET	`differential/observe.rs:49-64`, `:447-521` keep exact domain/code/value; the only normalization anywhere is `\r\n`→`\n` (`:278-289`, `:413-421`)
DoD 3 — augments, does not lower requirements	MET	the Core-Wasm ownership-transfer cell is explicitly bounded out with a cited reason (`view_ownership_composition.rs:73-92`), not silently dropped
Step 6 — every selected row executed	MET	`view_ownership_composition.rs:764-767` asserts each backend returned exactly `CASES.len()` rows, `:776-778` asserts per-row id equality
Step 7 — intentional mutation control	MET	`differential/injection.rs:111-197` relabels genuinely mutated backend values and failure selections and drives them through the real `compare` path; `view_ownership_composition.rs:861-864`
Checklist 1 — exact result/status agreement	MET	`view_ownership_composition.rs:705-737` cross-checks interpreter, native-O0, native-O2 and Core Wasm against the pinned expectation and against each other
Checklist 4 — fixed seed reproduces	MET	`differential.rs:55-72`, `:313-331`

The defect this audit found, now fixed

DoD 1's "enforced in CI" was not met, and the reason generalises past this issue. view_ownership_composition.rs:352 declares its own arming flag, SEMAPRAX_REQUIRE_VIEW_OWNERSHIP_COMPOSITION, which makes a missing clang/node a hard failure instead of an early return. No workflow set it. The matrix ran only because the Linux runner happens to provision those tools, and would have gone silently back to skipping the moment that changed — while the step selecting it still reported success.

Grepping every SEMAPRAX_REQUIRE_* flag in the tree against every workflow found three disarmed, not one:

SEMAPRAX_REQUIRE_VIEW_OWNERSHIP_COMPOSITION — this issue's own matrix.
SEMAPRAX_REQUIRE_INTERPRETER_BACKEND_PARITY — tests/interpreter_v1.rs and tests/language/interpreter_scalar_widen.rs.
SEMAPRAX_REQUIRE_AGENT_PROPOSAL_CLIENTS — worst of the three. generated_proposal_clients_compile_execute_and_round_trip (tests/agent_runtime_v1/agent_proposal_client_execution.rs:404) returns before its body unless the flag is set. It has passed by skipping on every runner since it landed.

All three are now armed, and every_declared_require_flag_is_armed_by_some_workflow walks the declared flags out of the test sources rather than pinning a list, so the next one is refused until it is armed or deliberately recorded with a reason. Verified red by disarming one flag; ci_release_gate:: → 10 passed.

This is the same blackout class as the two CI-selection gaps found earlier this month, in a third form: not "a test with no selector", but a test whose selector runs it and which then returns early. That is harder to see, because the step is green either way.

What still blocks closure

Core-Wasm ownership-transfer cell — the blocker already recorded above; needs a widened Public Scalar Export Profile or per-function multi-dispatch Wasm build.
OS scope — ci.yml:1044 gates the whole scalar_status_backend_equivalence binary on if: runner.os == 'Linux', though the verify job's matrix is all three OSes. macOS and Windows never run the composition matrix at all. I left this as-is and did not widen it, because arming it elsewhere without evidence that clang and Node are provisioned there would convert a silent skip into a red build. It needs a decision, not a guess.
Checklist 3 — no case in this corpus exercises a rejected allocation or asserts live owners reach zero afterwards. That property is covered only by the separate, pre-existing tests/public_generic_native_adapter_v1/settlement_corpus.rs, which is not this issue's deliverable.
Checklist 2 — "lazy branches remain unexecuted" is evidenced only probabilistically. differential.rs:343-357 counts lazy_operators > 0 and zero_divisors > 0 as separate aggregate counters and never their intersection, so nothing asserts any seed actually combines a short-circuiting left operand with a would-fail right one.
Checklist 5 — nothing guards against a selector silently matching zero tests, which this repository has already been bitten by (--test standard_library matches zero tests; the harness binary is tests/project.rs).

One correction to guard against

run_examples_and_conformance (tests/project/standard_library.rs:660-809) asserts each backend independently returned 0 — interpreter at :690-695, native via run_returns_zero at :485-494, Core Wasm at :754 — and no line in it compares one backend's output to another's. It is not this issue's deliverable and predates it, but any future closure rationale that cites it as cross-backend equivalence evidence would be wrong. That gap is precisely what this issue's corpus exists to fill.

Cover lazy boolean and checked-failure backend composition

Progress pushed to main in 5eafd55 (integrated through eb943c0): a deterministic feature-intersection fixture places checked division failure inside lazy boolean operands. It exercises false && ... and true || ... through the existing canonical/graph/differential harness.

The focused regression passed locally with explicit NativeO0, NativeO2, and CoreWasm observations; interpreter results also passed. All three generated-code lanes ran, rather than being counted as unavailable.

This is one additional corpus intersection, not completion of the entire issue or a hosted support claim. Remaining corpus/profile evidence stays open.

Exercise borrowed view call composition across backends (Refs #103)

Pushed b543274b to main (start 5ac1331d): new source-language composition corpus crosses whole-array versus ranged byte view, direct versus forwarded borrowed Slice call, and conditional versus loop context (eight explicit cells). Each cell checks length and actual first/last bytes, so correct-length/wrong-offset forwarding is detectable. The same expected scalar inventory runs through interpreter, generated C11 O0/O2, and actual Core-Wasm. The Wasm observer reuses the owning byte-carrier host instead of a second incomplete host model.

Actual focused command: cargo test --locked -p semaprax --test scalar_status_backend_equivalence view_call_boundary_composition -- --test-threads=1 --nocapture — 3 passed, including the eight-cell differential gate, stable SPX-T264 refusal of escaping Slice returns, and a deliberately wrong Core-Wasm observation rejected by the comparator. Log .agent-logs/0913-view-call-composition4.log in the private integration checkout. Current macOS arm64, Rust 1.98, clang and Node 24.3; no tool skip. Earlier draft fixture failures were corrected before this pass. No production admission or backend behavior was changed.

#103 remains open for remaining dimensions and evidence: imported/standalone interaction, allocation-rejection and ordered settlement composition, bounded variation/reduction inventory, and CI enforcement of the complete matrix. This slice claims exact values/status success for borrowed views; it does not invent owner-settlement counters or count rejected view returns as execution support. A duplicate generic-adapter settlement draft was removed during review and is not included. Hosted CI remains delegated separately.

Exercise priced adapter boundaries and imported byte views (#113, #103)

Pushed 87a3ab72 → 7360e0745d9242853d94a989548a9b7e375486c9.

Added one actual imported-package view-composition lane in the existing project harness: tests/project/standard_library/imported_view_composition.rs. A temporary Project selects useful-data.v1, imports the real std.bytes.field_start / field_end, passes a borrowed array view through a local callable boundary, and derives a nonzero-offset sub-view. Independent oracle: [a, comma, b, comma, c] gives start2/end3, byte98 and out-of-range fallback0, selecting328. The interpreter, native C11 O0/O2, and actual Core Wasm agree. The Wasm test host validates owned array temporaries and borrowed range descriptors and requires zero retained owners. A perturbed-backend comparator control fails as intended. Windows is explicitly ignored for this Unix native-command fixture; no Windows support claim.

Owning command cargo test --locked -p semaprax --features unstable-workflow-profiling --test project imported_view_composition -- --test-threads=1: 2 passed, log .agent-logs/0913-imported-view-final.log. Exact local environment: macOS arm64, Rust1.98, Node24.3, clang; static independent review accepted the corrected host/oracle. Negative development runs caught noncanonical test source, missing useful-data profile, invalid scalar export shape, and the incomplete Wasm byte host; all corrected before the owning pass. Formatting, module-size, and bundle checks passed. No compiler semantic change or hosted-CI claim.

This fills a bounded imported/package case beyond the earlier standalone borrowed-view compositions. The issue remains open for the remaining allocation/settlement combinations, variation/reduction inventory, and integration/CI criteria; one imported case is not the whole corpus.

Main 54d8606f5d89d84af29802d4f13ff46f01382676 adds the result-allocation rejection / ordered-input-release case under the existing public generic native adapter harness.

Interpreter and Wasm assert AllocationFailure, exact input leaf release order [1,0], and zero live handles/allocations; native C11 O0/O2 asserts the same status and resource result using the real compiled corpus probe. A [0,1] negative control invokes the identical order oracle and is rejected. Native leaf-index ordering is not claimed by this case. The drafted double injection was removed after inspecting the actual ordering: input cleanup happens before result allocation, so injecting it would prevent reaching the allocation boundary.

Final registered selector cargo test --locked -p semaprax --features unstable-workflow-profiling --test public_generic_native_adapter_v1 allocation_rejection_order -- --nocapture: 2 passed on macOS arm64/Rust 1.98/clang. Log .agent-logs/0913-allocation-registration-final.log; native probe paths are retained in that log. The child is registered through the existing settlement failure module, preserving the root module-size budget. Broader corpus/completion and hosted requirements remain open; this is one concrete extension, not full issue closure.

Accepted 70e3ce9 → bbf9a95 on main.

Added a real imported std.io + JSON decode/write owned-cursor chain. Interpreter and native C11 O0/O2 preserve the selected contract failure; Core Wasm records all three simultaneously live owners settling once in exact reverse lexical order, twice in succession. An executed wrong-order oracle is rejected; zero-live-owner and duplicate-drop checks remain active.

Focused execution: .agent-logs/0913-final2-composition.log (1 nonzero selected test). Source is canonicalized before Project admission. No production backend relaxation, full gate, or hosted execution.

#103 remains open while the matrix/campaign integration is completed; this fixture alone is not evidence for every composition dimension.

Completed in b7a9f79, after accepted graph/owned-cursor checkpoint bbf9a95 and runtime checkpoint c02b49e. Independent final review mapped the issue criteria to the ten-row V1 inventory and found no remaining functional gap after the focused refusal gate.

Finite composition matrix: ten documented rows with source-owner and complete registration-chain inventory; missing/duplicate negative controls. Existing fixed scalar/status, seven view-origin/context cells, eight call-boundary cells, ownership route, lazy evaluation, generated seeds, imported Project and generic allocation/settlement owners remain in their original harnesses.
Exact execution and unsupported shapes: new imported owned cursor chain preserves sticky contract failure on interpreter/C11 O0/O2 and exact zero-owner Wasm settlement across two runs, with an executed wrong-order negative. The actual owned-transfer source now has an exact SPX-W115 scalar-export refusal regression; unsupported execution is never counted as parity.
Replay and variation: existing fixed seeds, bounded reducer, failure artifacts and hostile comparison controls remain authoritative. The provisioned campaign now rejects unavailable lanes and invalid/zero seed counts; it checks exactly native O0/O2 and Core Wasm for each generated seed.
Enforcement: existing Linux standard-library CI now selects the exact owned-failure test and complete inventory; an explicit dispatch-only workflow runs 1..256 strict generated seeds, rejects zero test selections and retains logs. The frozen source/status/owner oracles were not weakened.

New focused local evidence: .agent-logs/0913-composition-all-inventory.log (2 pass), .agent-logs/0913-composition-w115.log (1 pass), .agent-logs/0913-composition-strict-one.log (1 seed, exactly three generated backend lanes plus interpreter), and .agent-logs/0913-composition-zero-negative.log (expected refusal). Owned cursor gate passed in .agent-logs/0913-final2-composition.log. The combined final build passed. Earlier unchanged owners retain their separately reported accepted evidence.

Closing as implemented with focused local evidence under the user's explicit instruction to skip full/hosted gates. The authored 256-seed hosted workflow was NOT executed here; there is no hosted, non-Linux native, or expanded Wasm profile claim.

Main now verified at a6ec86e, containing implementation b7a9f79 and preserving the concurrently merged VS Code extension update 812212e. The integration merge changed only the independent editor files; focused corpus evidence and limitations above are unchanged.

Navigation Menu

Repository navigation

[P1] [SPX-AI-004] Add a bounded feature-combination and differential backend conformance corpus #103

SPX-AI-004 — Add a bounded feature-combination and differential backend conformance corpus

Outcome

Current evidence and distinction from existing work

Read these owners first

Bounded scope and non-goals

Implementation steps

Required tests and failure cases

Starting commands

Definition of done

Guardrails for the implementing agent

Evidence to attach before closing

Tranche 1 — the ordinal-timing lead inherited from #240

Tranche 2 — the bounded composition corpus

The finding that corrected an error of mine

What is genuinely met

The defect this audit found, now fixed

What still blocks closure

One correction to guard against

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[P1] [SPX-AI-004] Add a bounded feature-combination and differential backend conformance corpus #103

Description

SPX-AI-004 — Add a bounded feature-combination and differential backend conformance corpus

Outcome

Current evidence and distinction from existing work

Read these owners first

Bounded scope and non-goals

Implementation steps

Required tests and failure cases

Starting commands

Definition of done

Guardrails for the implementing agent

Evidence to attach before closing

Activity

wsdt commented on Sep 12, 2026

Tranche 1 — the ordinal-timing lead inherited from #240

Tranche 2 — the bounded composition corpus

The finding that corrected an error of mine

wsdt commented on Sep 12, 2026

What is genuinely met

The defect this audit found, now fixed

What still blocks closure

One correction to guard against

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions