Skip to content

[codex] r3 gate 50 one-shot memoization witness - #2547

Merged
briansrls merged 1 commit into
mainfrom
codex/r3-gate-50-one-shot-no-memo
May 10, 2026
Merged

briansrls merged 1 commit into
mainfrom
codex/r3-gate-50-one-shot-no-memo

Conversation

@briansrls

@briansrls briansrls commented May 10, 2026 •

Copy link
Copy Markdown
Contributor

Summary

  • Converts auto_memoization_no_caching_for_one_shot from the deferred BinaryDimensionReportEquals shape to an executable LensOutputEquals witness.
  • Adds a fixture-scoped runner witness that emits Rust for the claim source and passes only when memo/cache scaffolding is absent.
  • Keeps the repeated pure-call memoization claim deferred to the future purity + cost composition producer.

P5 Receipt

  • Explicit deferral: this adds a narrow hand-Rust LensOutputEquals witness for R3 T-Free-Consequences-Demonstration gate Well-specified TODO tasks #50; it dissolves when the verification lane lands structural AutoMemoizationEvidence / purity+cost memoization evidence for the free-consequences auto-memoization claims. Roadmap row: ROADMAP.md § "Active deferrals" / "Author-now/fire-later claim shells that need real producers".

Validation

Work item: dashboard://work-items/r3-gate-50-2014ac3a

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the dashboard review note. The substring-based absence check is intentional for this narrow gate witness and is scoped with a dissolution note to the future structural AutoMemoizationEvidence producer; no code change is needed for the optional exploratory item. I did push a follow-up commit to remove the conflict marker left after integrating main/gate #45. — sent from sharp-owl-508

@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: b44d5e25 · Trigger: schedule
  • Thinking: 220s wall

BLOCKING (2)

Root Cause

  • src/v3/compiler/src/test_runner.rs the new witness treats an already-typed Int value as decimal text → read the LiteralBits::Int value directly, matching the existing cost_of branch.
  • src/v3/compiler/src/test_runner.rs gate-specific Rust witness was added without an adjacent checkable debt receipt → add the required PR-body or planning-artifact receipt, or retire/shrink an SG-0 scaffold in this change.

⚠️ The witness is on the right R3 gate, but the runner block needs to compile and the hand-Rust P5 receipt needs to be explicit.

// the AutoMemoizationEvidence producer reaches `.dag`.
if lens_decl.name.as_deref() == Some(R3_ONE_SHOT_NO_MEMO_WITNESS_LENS_NAME) {
let expected_int = match expected_decl.value_body.as_ref() {
Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::<i64>() {

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: LiteralBits::Int is already the typed i64 carrier, so calling parse::() on it will not compile; this violates INVARIANTS.md P2 typed-boundary discipline.

};
}

// R3 gate #50 (`auto_memoization_no_caching_for_one_shot`): one-shot call sites must not

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: The new src/v3 hand-Rust runner bridge has a dissolution note but no required P5 receipt: deleted scaffold path, SG-0 shrink, or deferral lane plus concrete ROADMAP row.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the approval feedback against current PR state. The optional ellipsis/string-substring notes are non-blocking and already bounded by the dissolution comment in code. The P5 receipt check was valid for the PR description, so I updated the PR body with a single explicit deferral receipt naming the R3 verification lane and the concrete ROADMAP.md Active deferrals row for author-now/fire-later producers. No code change was needed for this review item. — sent from sharp-owl-508

@briansrls
briansrls force-pushed the codex/r3-gate-50-one-shot-no-memo branch from 366f643 to b3ed4e2 Compare May 10, 2026 06:11
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: b3ed4e2f · Trigger: manual
  • Comparison: main @ f9171c11 ... codex/r3-gate-50-one-shot-no-memo @ b3ed4e2f
  • Conversation: View conversation

1. Story of the diff

This PR turns the R3 one-shot auto-memoization claim from a deferred placeholder into an executable witness. The fixture now contains an actual one-shot pure call, fn bump(x: Int) -> Int = x + 1 followed by let _: Int = bump(41) at src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag:116, and the claim switches from BinaryDimensionReportEquals to a LensOutputEquals witness at src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag:118-121. The runner adds a narrow special case for r3_auto_memoization_one_shot_no_cache_witness, emits Rust for the claim source, and computes 1 when no memo/cache scaffolding marker appears in the emitted text. The integration test expectation is updated accordingly: repeated-call memoization remains fail-closed/deferred, while the one-shot no-cache claim must now pass.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — this is implementation/test-harness and fixture-only. No Dag substrate type, dag.rs field, behavior variant, or cross-pass modeled fact is added; the .dag changes are test fixture witness/claim declarations at src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag:57-60 and :116-121.

  1. INVARIANTS.md + modeling-discipline.md.

Compliant — fail-closed handling is preserved in the new runner branch: malformed expected literals return ClaimResult::Fail at src/v3/compiler/src/test_runner.rs:2405-2413, and Rust emission failure also returns ClaimResult::Fail at src/v3/compiler/src/test_runner.rs:2416-2423 rather than fabricating success. The bridge is also explicitly scoped as a temporary witness at src/v3/compiler/src/test_runner.rs:2397-2399.

  1. CODING.md.

Compliant — the new code uses a named constant for the lens-dispatch key at src/v3/compiler/src/test_runner.rs:62, keeps dependencies explicit by calling crate::emit_rust::emit_rust(&program_dag) at src/v3/compiler/src/test_runner.rs:2416, and returns structured ClaimResult outcomes rather than panicking or adding hidden mutable state.

  1. TESTING.md.

Finding — NON-BLOCKING, behavior witness is brittle. The test’s intended behavior is “no memoization scaffolding for one-shot pure calls,” but the runner proves it with a broad substring absence check: src/v3/compiler/src/test_runner.rs:2425-2429 rejects any emitted text containing "memo", "Memo", "cache", "Cache", or "HashMap". That can false-fail on unrelated user identifiers/provenance containing those strings, and false-pass on real cache scaffolding named with other words or implemented with another carrier such as BTreeMap, OnceLock, or a generated static. Because this is a bounded R3 witness with a named dissolution trigger at src/v3/compiler/src/test_runner.rs:2397-2399, I would not block the PR, but the gate is weaker than the behavior it names.

  1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter locked bootstrap, substrate, zero-floor, or target-realization design documents. It also avoids changing the repeated-call memoization target: the added doc comment keeps repeated-call caching “deferred to the purity+cost lens composition producer” at src/v3/compiler/src/test_runner.rs:59-61, and the integration test docs repeat that “Repeated-call memoization remains deferred” at src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs:7-8.

  1. TRACKED vs UNTRACKED DEBT.

Compliant — the temporary shape is documented, bounded, and has a dissolution trigger. Documentation/scope: src/v3/compiler/src/test_runner.rs:2397-2398 identifies R3 gate #50 and the emitted-Rust-text witness; bound: src/v3/compiler/src/test_runner.rs:2400 limits the special case to the exact lens name; dissolution trigger: src/v3/compiler/src/test_runner.rs:2398-2399 says it dissolves when the AutoMemoizationEvidence producer reaches .dag.

2.5. Top-down PM intent review

Compliant — the PR preserves the high-level memoization intent rather than diluting it. It does not claim repeated-call memoization is complete; it explicitly says repeated-call caching is deferred at src/v3/compiler/src/test_runner.rs:59-61 and src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs:7-8. The concrete PM-level value added here is narrower and valid: a one-shot pure call fixture at src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag:116 now has a passing no-cache witness expectation at src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs:90-96.

3. Verdict

APPROVE_WITH_COMMENTS. No substrate or locked-design concern, and the temporary Rust witness is bounded with an explicit dissolution trigger. The only issue is a non-blocking testing weakness: the emitted-text substring check is a coarse proxy for “no memoization scaffolding,” so it should be treated as a short-lived witness rather than a durable proof surface.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the claude approval against the rebased code at head b3ed4e2. The substring oracle is intentionally fixture-scoped and already carries the AutoMemoizationEvidence dissolution note; the helper extraction suggestion is cleanup across sibling witness blocks, not a correctness issue for gate #50. No code change needed for these non-blocking observations. — sent from sharp-owl-508

@briansrls
briansrls merged commit 9a828c1 into main May 10, 2026
4 checks passed
@briansrls
briansrls deleted the codex/r3-gate-50-one-shot-no-memo branch May 10, 2026 06:21
@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the relayed openai-pro review artifact against PR #2547. It is the same APPROVE_WITH_COMMENTS review already posted on the PR at 2026-05-10T06:19:56Z; its only finding is explicitly non-blocking and matches the bounded substring-oracle concern already addressed by the AutoMemoizationEvidence dissolution note. PR #2547 has already been squash-merged as 9a828c1, so no fix commit is applicable. — sent from sharp-owl-508

briansrls added a commit that referenced this pull request May 10, 2026
…2648)

* docs(r3): §1.8 ledger-receipt sync — 2026-05-10 batch (V Mgr lane)

Flip §1.8 ledger Status from DECLARED/CONSUMER_LANDED to PASSING for V-Mgr
lane gates whose CONSUMER_LANDED PRs landed in main as of 2026-05-10. Each
row cites the merging PR per Director-ratified post-merge ledger-receipt
sync discipline (gunbc#828 c#4415884211).

Gates flipped (17): #9 (#2585), #10 (#2602), #11 (#2603), #12 (#2598),
#14 (#2571), #31 (#2586), #43 (#2495), #44 (#2523), #45 (#2527),
#46 (#2529), #47 (#2532), #48 (#2535), #49 (#2536), #50 (#2547),
#51 (#2577), #52 (#2578), #69 (#2551).

Skipped per discipline: #15 (PR #2604 not landed); #35 already PASSING.

Doc-only; no code or test changes. Closes #2640.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): preserve corpus-quantified + canvas-deferral qualifiers on rows #9/#10/#11

Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text
on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that
must not be silently elided when citing a new slice receipt:

- #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠
  ledger closure; PASSING requires every certification-corpus program.
  Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence.
- #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra,
  inhabitant, law) §Acceptance coverage; distributivity / lattice absorption /
  non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED;
  PR #2602 cited as incremental advancement.
- #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09
  held this canvas-deferred past R3 absent #1972 substrate canvas-tier work.
  Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement
  but not retiring the canvas-deferral (which would require fresh Director
  ratification).

Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such
qualifiers and stay flipped to PASSING.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Merge origin/main into ledger-receipt sync (preserve row #13 update from main)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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