Repository navigation
Conversation
…lMemo
PureCallMemo admitted calls by function spelling (content_hash, well_formed,
locally_well_formed, fold_node, fold_node_content_hash, node_subtree_count) and keyed
them on the function node plus each argument's allocation identity in source order,
dropping argument labels. Its hit returned before call_function bound or validated
anything, so f(a: x, b: y) then f(b: x, a: y) with the same retained x and y was
served the first result. Reproduced on main by
v2.test.claim.interpreter.pure_call_binding swapped_labels_bind_their_own_parameters_holds
(FAIL on main, PASS here); the same body under an unrostered spelling binds correctly
on both.
The tier is deleted, not re-keyed: a spelling is not purity evidence, and the
eval-frame memo one tier down (eval_pure_named_call, default on, reached only by
functions with no `uses`) already serves pure named calls and verifies argument
names and values (eval_call_memo_args_match) before a hit. The fail-closed lockdown
plan's row for pure_call_memo_key now records the withdrawal.
A warmed invalid-label call is not authorable as accepted source: the call-shape
wall refuses an unknown label at resolve ("no parameter named 'c'"), so no accepted
program reaches the runtime bypass that the deleted hit could have skipped.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6367a86229
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| alignments: [AlignNone, AlignNone, AlignNone], | ||
| rows: [ | ||
| row(cells: [cell(text: "`v1_interpreter.rs` `pure_call_memo_key`"), cell(text: "key-by-address"), cell(text: "keys on `Rc::as_ptr`, not content → stale hit on realloc; structurally-equal args miss")]), | ||
| row(cells: [cell(text: "`v1_interpreter.rs` `pure_call_memo_key` (withdrawn)"), cell(text: "key-by-address, label-blind, admitted by spelling"), cell(text: "keyed on `Rc::as_ptr` in source order without argument labels, so swapped-label calls were served the first result (`v2.test.claim.interpreter.pure_call_binding`); the tier is deleted and pure named calls are served only by the eval-frame memo, which verifies names and values")]), |
There was a problem hiding this comment.
This row now records the cache as withdrawn, but the same authority still says at lines 51 and 55 that pure_call_memo remains live with an address-keyed flake surface, while line 71 retains an unchecked task to kill that address key. After this commit deletes the cache, readers of the lockdown plan receive mutually exclusive current states and may schedule work against a nonexistent tier; update those remaining entries to describe the replacement eval-frame memo or mark the work complete.
Useful? React with 👍 / 👎.
…tements with its withdrawal Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Closed without folding in the v1 closeout bankruptcy (#13641). A seed-interpreter fix; the interpreter isn't part of the one retained seed emission. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604 |
1 participant
Roadmap:
seed-pure-call-binding(D15 census #9).Defect, executed
v1_interpreter.rsPureCallMemoadmitted calls by function spelling:content_hash,well_formed,locally_well_formed,fold_node,fold_node_content_hash,node_subtree_count.call_functionbound or validated anything.New claim module
v2.test.claim.interpreter.pure_call_binding. Its subject is a suppliedwell_formed(a: List<Int>, b: List<Int>) -> List<Int> { a }with two retained lists.swapped_labels_bind_their_own_parameters_holds:well_formed(a: x, b: y)thenwell_formed(b: x, a: y)must give[1]then[2]swapped_labels_bind_under_an_unrostered_spelling_holds: same body asfirst_formalan_identical_repeat_answers_the_same_value_holds: positive controlRepair: withdraw the tier, don't re-key it
A spelling is not purity evidence, so adding labels to the key would still leave an unproved admission. The eval-frame memo one tier down already serves pure named calls:
eval_pure_named_call, on by default;uses, so effectful functions never get there;eval_call_memo_args_match) before a hit.So
PureCallMemois deleted: the struct, the context field, its memory accounting, key/get/put,is_structural_pure_fn, and the serve ineval_call.gunbc.plans.fail_closed_lockdownrecords the withdrawal in its §3 table, its warm==cold paragraph, its suspected-root paragraph and its content-key task; that plan has no committed projection.Warmed invalid-label refusal: I tried to write this control and it is not authorable as accepted source. The direct-call shape wall refuses at resolve (
no parameter named 'c' (declared: [a, b])), so no accepted program reaches the runtime bypass that a hit could have skipped.What still serves before binding: the eval-frame memo can return a result before
call_functionbinds. It does so only aftereval_call_memo_args_matchhas matched every stored argument's label and value against the call, so a call with different labels is a miss, not a hit.Cost: these six producers now go through the eval-frame memo. Its key hashes argument content, memoized per allocation, instead of reading a pointer. I did not measure a wall-time difference.
Evidence (local, runtime change at 6367a86; the follow-up commit edits plan text only)
cargo fmt --all --checkOK;cargo clippy --all-targets -- -D warningsOK.claim_batchPASS. On main's seed (same claim file), the swapped-label claim FAILS.claim_executor --required-ci --required-lane witnesses):planned-and-passed;mtcollins1_kvm_observer_protocol_wet_witness×7 andallocation_client_execution_wet_witness×8, which are local host refusals, plusv41_source_patch_converge_witnessred5, cause unresolved.Not in this PR
Seed retirement and any seed-wide materialization policy stay with their owners. The eval-frame memo's own admission (every
uses-free function) is unchanged here.🤖 Generated with Claude Code