Skip to content

[codex] Close gate 61 function-valued data receipt - #3114

Merged
briansrls merged 24 commits into
mainfrom
session/gentle-eagle-11
May 14, 2026
Merged

briansrls merged 24 commits into
mainfrom
session/gentle-eagle-11

Conversation

@briansrls

@briansrls briansrls commented May 14, 2026 •

Copy link
Copy Markdown
Contributor

What changed

  • Extended the R3 gate Workflow capabilities integration #61 function-valued data fixture with a canonical DimensionReport<Int> return path.
  • Added report_int: fn(Int) -> DimensionReport<Int> as function-valued data whose body constructs canonical DimensionOk through the E6-G0d variant-constructor path.
  • Added an integration ratchet that evaluates the new caller through the public evaluator and asserts the DimensionOk payload carries composed = 42.

Why

Gate #61 needs executable evidence that function-valued data is not just structurally lowered as an arrow, but can produce the canonical report-shaped data through evaluator execution. The fixture now consumes v3.std.dimensions::DimensionReport / Witness directly and seeds the witness list with the same Empty / Cons pattern used by existing canonical dimension-report fixtures.

P5 receipt

INVARIANTS.md P5 receipt for the expanded hand-Rust integration harness is this PR body plus the existing registered row for src/v3/compiler/tests/integration/r3_class_2_function_valued_data_test.rs: R3 §1.4 Class 2 / §1.8 row #61 substrate_gap_function_valued_data_closed. The new checkable receipt is substrate_gap_function_valued_data_produces_dimension_report, which compiles the gate #61 fixture, evaluates test_function_valued_dimension_report through the public evaluator, and asserts the E6-G0d constructor path produces canonical DimensionOk with composed = 42.

Dissolution remains the existing row's trigger: retire this hand-Rust harness when §1.8 row #61 can be expressed as a .dag TestClaim over evaluator output without direct Rust DAG inspection.

Validation

  • cargo test -p v3-compiler --test integration r3_class_2_function_valued_data_test -- --nocapture

@briansrls
briansrls marked this pull request as ready for review May 14, 2026 17:17

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: f81222d6 · Trigger: schedule
  • Thinking: 188s wall

BLOCKING (1)

Root Cause

  • src/v3/compiler/tests/fixtures/r3_class_2_function_valued_data.dag The fixture closes a DimensionReport gate with a fixture-local report carrier -> import and return the canonical DimensionReport/DimensionOk shape, or narrow the claim to a generic user-coproduct evaluator test.

ROADMAP — Incomplete

  • docs/r3-program-plan.md §1.8 row #61: The diff exercises function-valued data returning a bespoke coproduct, but the row #61 receipt names the canonical DimensionReport carrier.

⚠️ One modeling issue blocks this as a gate-61 closure receipt.

@@ -1,5 +1,15 @@
// R3 Class 2 gap representative: function-valued data is first-class.

type Gate61DimensionReport<Carrier>

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: Gate61DimensionReport duplicates the existing DimensionReport carrier instead of consuming v3.std.dimensions, so gate #61's DimensionReport receipt remains unproven and MODELING M6/single-authority is violated.

@briansrls
briansrls merged commit 03bcc9f into main May 14, 2026
4 checks passed
@briansrls
briansrls deleted the session/gentle-eagle-11 branch May 14, 2026 20:47
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