Skip to content

R3 gate #40: symbolic cost expr equals executable - #2450

Merged
briansrls merged 14 commits into
mainfrom
session/royal-ferret-515
May 10, 2026
Merged

briansrls merged 14 commits into
mainfrom
session/royal-ferret-515

Conversation

@briansrls

@briansrls briansrls commented May 9, 2026 •

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session royal-ferret-515.
Pushing to session/royal-ferret-515 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (below).
  • Tests run: see Test plan (CI v3 + local commands).
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

Implements R3 gate #40 (symbolic_cost_expr_equals_executable): SymbolicCostExprEquals compiles TestClaim.source, runs symbolic_cost_of on the emitted top-level value bind, and compares to the fixture-declared expected SymbolicCost using normalized equality patterns (including SizeVariable identity on source_port, per algebra.dag, not display_name alone).

lower.rs adds a narrow ConstantCost(<Int literal>) structural lowering for data …: SymbolicCost = …, seeds anonymous SymbolicCost variant carrier ids into the symbol map so surface names resolve to canonical substrate constructors, and rejects shadowed ConstantCost calls via declaration-id equality (same discipline as repeat_string).

INVARIANTS P5(b) — single checkable receipt

This PR expands hand-authored Rust under src/v3/. Per INVARIANTS.md Dispatch-Discipline P5(b), the PR description states exactly one checkable receipt:

Cited ROADMAP.md dissolution: This work lands the runner/evaluation called out in ROADMAP.md (Verification / R3): the row that SymbolicCostExprEquals was typed but NotYetImplemented in test_runner — i.e. “typed carrier landed ≠ verification landed” for gate symbolic_cost_expr_equals_executable (search ROADMAP.md for symbolic_cost_expr_equals_executable / SymbolicCostExprEquals). That debt is dissolved here by making the predicate executable with fail-closed diagnostics, not by claiming closure on shape-only.

(Rustdoc on the ConstantCost lowering hook intentionally does not substitute for this PR-level receipt.)

Test plan

  • cargo fmt --all --check
  • cargo clippy -p v3-compiler --all-targets -- -D warnings
  • cargo test -p v3-compiler symbolic_cost_expr_equals (unit + integration smoke)
  • cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify (CI ci job)
  • Full cargo test -p v3-compiler via CI v3 workflow job

@briansrls
briansrls marked this pull request as ready for review May 9, 2026 22:42
…al decode, decoder tests

- Document ROADMAP gate #40 / SymbolicCostExprEquals NYI dissolution on ConstantCost lowering (P5 + class-5 gap #3 narrow slice).
- Decode optional string fields by payload shape first; fall back to exact Some/None constructor names only (remove ends_with heuristic).
- Add unit tests for SumCost/ProductCost pattern decoding and optional payload classification.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Follow-up on APPROVE_WITH_COMMENTS items:

  1. P5 / SymbolicCost lowering (lower.rs) — The doc comment on try_lower_symbolic_cost_constant_cost_data now states an explicit P5 receipt: it dissolves the ROADMAP SymbolicCostExprEquals NYI row / R3 gate Add external tool dependency management with gcloud support #40 (symbolic_cost_expr_equals_executable), as an intentional narrow class-5 gap . #3 slice until general SymbolicCost data literals lower structurally (aligned with lower_data_item / DOWNSTREAM_REQUIREMENTS).

  2. optional_string_field_for_record — Dropped ends_with("Some"|"None"). We classify optional strings by payload shape first (classify_optional_string_payload: empty payload → absent, single string literal → present), then fall back to exact constructor names Some / None only when shape alone does not resolve.

  3. Decoder coverage beyond ConstantCost smoke — Added #[cfg(test)] tests in test_runner.rs that construct bootstrap-backed FieldValues for SumCost and ProductCost over two ConstantCost terms (NonSingletonList shape), plus a unit test for classify_optional_string_payload.

@briansrls

Copy link
Copy Markdown
Contributor Author

Dashboard routing note: The quoted item is not a new reviewer finding — it is the existing PR resolution summary (same three bullets already landed on the branch: P5 receipt comment on try_lower_symbolic_cost_constant_cost_data, payload-first optional decoding + classify_optional_string_payload, and symbolic_cost_expr_equals_decoder_tests). No additional commit is required for that text.

Current tree still matches that narrative (lower.rs P5 receipt block; optional_string_field_for_record → shape-first + exact Some/None fallback; decoder unit tests in test_runner.rs).

— sent from royal-ferret-515

briansrls and others added 9 commits May 9, 2026 19:09
Composer review: avoid calling this ConstantCost lowering path "the" P5 receipt —
P5(b) names PR-description evidence (SG-0 census, deleted scaffold, cited ROADMAP deferral).
Describe gate #40 / class-5 gap progress explicitly; keep Practice 5 authority wording for ctor ids.

Co-authored-by: Cursor <cursoragent@cursor.com>
Codex: comparing LinearCost/LogCost/PolynomialCost by display_name only dropped
algebra.dag identity (source_port), letting unrelated unnamed costs collide.

- Encode equality patterns with source_port raw only; validate optional display_name
  payload shape without using it in Eq (matches SizeVariable PartialEq).
- Decode source_port from structural SizeVariable FieldValues (Int literal).
- Add unit tests for port discrimination and display-independent matching.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Re-checked against current HEAD: composer-2’s APPROVE still matches the tree.

  • P5(b): try_lower_symbolic_cost_constant_cost_data rustdoc in lower.rs still distinguishes R3 gate Add external tool dependency management with gcloud support #40 / class-5 slice progress from INVARIANTS P5(b) per-PR checkable receipts (PR description / census / cited deferral) — no code claims to satisfy P5(b) by itself.
  • Practice 5: seed_symbolic_cost_variant_constructors_for_symbols + resolved callee vs canonical ConstantCost carrier id remain the authority story for that lowering arm.
  • P3: eval_symbolic_cost_expr_equals_shape still fails closed on compile failure, missing top-level value bind, and symbolic_cost_of miss paths.

No rubric-grounded defect was identified in the relayed review; no additional commit for this artifact.

Exploratory notes (test_runner.rs size / Practice 4 enum labeling) are acknowledged as non-blocking follow-ups only.

— sent from royal-ferret-515

@briansrls
briansrls merged commit 5417452 into main May 10, 2026
4 checks passed
@briansrls

Copy link
Copy Markdown
Contributor Author

composer-2 relay (8550) — verified

  • Rubric claims checked against current HEAD: seed_symbolic_cost_variant_constructors_for_symbols, canonical ConstantCost callee id + type_decl_is_symbolic_cost, runner compile_to_dag → symbolic_cost_of → normalized comparison with explicit Fail strings, and anonymous-variant decoding via SymbolicCost Disj metadata — all present as described.
  • P5(b): Per your exploratory note, the PR description is updated (no longer TODO-only): it now states one checkable receipt — cited ROADMAP.md dissolution for the SymbolicCostExprEquals / gate symbolic_cost_expr_equals_executable debt row (runner was NotYetImplemented).
  • Merge readiness: CI ci/fmt/v3 green on run 25615389710; GraphQL mergeStateStatus: CLEAN, mergeable: MERGEABLE.
  • Verdict: APPROVE grep: GitHub issue/review-comment APIs here did not surface dashboard-formatted Verdict: lines (artifacts live outside normal GH reviews).
  • Squash-merge: Attempted locally (gh pr merge --squash) failed due to local worktree/git checkout contention; REST merge returned 404 (likely token scope / permissions from this environment). Please squash-merge from an authorized client if policy allows.

— sent from royal-ferret-515

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