Skip to content

shell_exec_run: judge the witness argv as a whole value (optional-equality rule) - #13589

Closed
gunbai-bot[bot] wants to merge 1 commit into
mainfrom
session/eager-cat-664-optional-equality-fix
Closed

gunbai-bot[bot] wants to merge 1 commit into
mainfrom
session/eager-cat-664-optional-equality-fix

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

One file, one function. The composed floor (merge_group run 37766479936) refused 3 diagnostics from the optional-equality rule at src/v2/test/claim/execution/emit_host_shell_exec_run_equals_eval_test.dag:44-45: the eval leg compared List.first() against string literals, and first() is Optional-typed, so first() == "bash" is refused.

Per the #13581 finding, the tempting Present-pattern rewrite executes FALSE at runtime (first() yields the bare head), so the fix is whole-value equality: the witness argv is judged against its expected list ["bash", "-s"] directly -- no Optional constructed, no first() call, and the condition is exactly the old conjunction (length 2 AND first two elements).

Verified by execution on the runner: claim_batch on the three claims returns PASS on all (eval octet = 1, the equals-eval leg holds, the wrong-oracle leg still refuses), BATCH_EXIT=0 -- not just compile-clean.

…al-equality rule refuses first()-vs-literal equality

The eval leg matched List.first() against a string literal twice (lines 44-45). The
optional-equality checker refuses first() == literal (first() is Optional-typed), and
per 13581's runtime finding the Present-pattern workaround executes FALSE because
first() yields the bare head. Whole-value equality needs neither: the witness argv is
judged against its expected list directly, no Optional is constructed, and the
condition is exactly the old one (length 2 AND first two elements). Verified by
execution: claim_batch PASS on all three claims (eval octet = 1, the equals-eval leg,
the wrong-oracle refusal), BATCH_EXIT=0.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved at abfb678. The one-line rewrite is semantically equivalent to the old predicate: equality with ["bash", "-s"] requires exactly two elements in exactly that order, while evaluating the argv producer once and avoiding both Optional-vs-required comparisons and the runtime-false == Present { ... } form. The three claim roles remain intact: the eval oracle yields 1 only for the declared argv, the native/eval agreement consumes that octet, and the complemented oracle must still refuse. The diff is confined to this helper. Exact-head witnesses run 37796383849 is queued; queue only after the aggregate turns green.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 8, 2026
@gunbai-bot
gunbai-bot Bot removed this pull request from the merge queue due to a manual request Oct 9, 2026
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 9, 2026
@briansrls
briansrls removed this pull request from the merge queue due to a manual request Oct 9, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 9, 2026
@briansrls
briansrls removed this pull request from the merge queue due to a manual request Oct 9, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 9, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 9, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 9, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 9, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 9, 2026
@briansrls
briansrls removed this pull request from the merge queue due to a manual request Oct 9, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 9, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Oct 9, 2026
@gunbai-bot

gunbai-bot Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Closing as superseded: main fixed the same witness independently in d0f2067 (match the Optional from first(), the runtime-sound form per #13581). This PR now conflicts and adds nothing. — sent from lively-ram-153

@gunbai-bot gunbai-bot Bot closed this Oct 9, 2026
@gunbai-bot gunbai-bot Bot mentioned this pull request Oct 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant