Skip to content

feat(evaluator): wire algebraic commutativity runner - #1359

Merged
briansrls merged 1 commit into
mainfrom
feat/pr-b3-algebraic-law-runner
May 1, 2026
Merged

briansrls merged 1 commit into
mainfrom
feat/pr-b3-algebraic-law-runner

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

  • add a bounded COMMUTATIVITY_WITNESS_PAIRS sample table alongside associativity witnesses
  • wire AlgebraicLaw(Commutativity, lens_ref) through the runner using the existing predicate surface and a shared structural-value comparator
  • keep Identity fail-closed with the missing identity-element edge called out, and keep distributivity routed to the P1 substrate enum-extension path
  • add focused runner tests for commutativity pass/fail and the identity blocker

Verification

  • cargo fmt --all --check
  • git diff --check

Attempted focused test: cargo test -p v3-compiler test_runner_algebraic_law_commutativity --test integration.

  • With the default target dir it failed with No space left on device while writing dependency files on the /Users worktree volume.
  • Retried with CARGO_TARGET_DIR=/tmp/gunbc-pr-b3-target; dependency compilation proceeded but remained in v2-compiler compilation for about 30 minutes, so I stopped it rather than leave a runaway job.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: d937f10a · Trigger: schedule
  • Comparison: origin/main @ 79e61ba0 ... review/pr-1359-d937f10a @ d937f10a
  • Thinking: 93s wall

Findings

  • src/v3/compiler/tests/integration/test_runner_test.rs:1018-1021 (and similarly 1051-1054): New tests assert on human-readable ClaimResult strings via .contains(...). TESTING.md (“Anti-patterns” → don’t pin error message text) treats that as a brittle contract; for the subtraction case, matches!(..., ClaimResult::Fail(_)) (or a typed/stable carrier if one exists) would assert the behavior without coupling to wording.

Verdict

APPROVE_WITH_COMMENTS — The runner change mirrors the existing associativity pattern: bounded witness table in lens_apply.rs, compile-time len() > 1 ratchet, explicit “operational witness, not substrate proof” + dissolution language in test_runner.rs, and Identity stays fail-closed / NYI with a clear rationale. Nothing here looks like substrate duplication of authority beyond the already-documented runner scaffold. The only rubric-aligned nit is the new substring-based test assertions above.

Exploratory (optional)

  • src/v3/compiler/src/test_runner.rs:305: The unreachable! after string matching is conventional for “validated twice” flow; if you ever want to avoid panic surfaces in this helper entirely, the inner match could return the same UnsupportedLaw/MalformedPayload path instead (implementation taste, not a modeling violation).

@briansrls
briansrls merged commit 0994d76 into main May 1, 2026
2 of 4 checks passed
@briansrls

Copy link
Copy Markdown
Contributor Author

Follow-up PR opened for the review nit about substring-based assertions: #1363

It replaces the message substring checks with typed ClaimResult::Fail(_) / ClaimResult::NotYetImplemented(_) matches. git diff --check and cargo fmt --all --check passed; focused test still stalls in dependency compilation in this environment, matching the original PR note.

— sent from snappy-moth-795

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