Repository navigation
[superseded, do not merge] R1: optional R2IL reading of a DT64 MethodBinding - #1892
Conversation
…are/run) binding::prepare resolves an admitted DT64 MethodBinding once, cold: frame, focus, scope and route guards, class basis, admit, then per effect the lens (OGAR's R2IL fold reading), the word's label resolved to exactly one opcode by OGAR's vocabulary, the translatable subset, and OGAR's arity against the lens's declared arity and the argument count. binding::run executes the bound opcodes through FoldDialect, hot, rechecking only the guards, the route and an explicit execution permit, and returns a receipt bounded by the plan's step count. This reading is optional: no consumer is required to execute through it. Unsupported shapes (WHEN guards, three-valued truth, immediates, sinks, out-of-range lane constants, unbound fields) are refused by name. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
…rces BindStore::register refuses an effect whose argument count differs from the lens's declared arity, so comparing OGAR's arity with the declared one could never fire on its own (a disable run left every test green). The check is OGAR's arity against the argument count; the declared arity is still reported in the refusal. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
 |
…DT64 Five scouts, three co-architects. The premise splits: R2IL is one vocabulary with no method identity, so the canonical body belongs in the OGAR IR (ActionDef -> ogar-loco Program) with a derived body revision; DT64 carries a reference; reasoning runs cold; receipts name body, plan and target. Draft #1892 is the reverse translator ruled out today and is marked superseded. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
AdaWorldAPI
changed the title
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: a2786e317f
ℹ️ 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".
| Arg::Field(p) => match values.get(&p) { | ||
| Some(&v) => v, | ||
| None => lane(dialect, fields, i, p)?, |
There was a problem hiding this comment.
When a binding uses a computed mask in more than one fold, such as m = a < 5; s = SUM(m, b); n = PopCount(m), the second fold fails with FoldError::StaleSlot. FoldDialect::finalize_and_run clears the pending mask operations and advances the epoch at the first fold, but values retains the old slot and supplies it unchanged to subsequent effects. This is an otherwise admitted sequence using only executable opcodes. Preserve the mask's expression and re-emit it when a later effect needs it in a new epoch, as the existing procedure layer does for repeated selections.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed by reading binding.rs:311-336 and lib.rs:501-515. run caches each step's result in values: BTreeMap<u8, Val>. A Val::Slot carries the epoch it was minted in, and the first fold advances the dialect epoch. Reusing a mask field after a fold therefore reaches expr_of with an old epoch and fails with StaleSlot. The defect is in the binding layer: it treats a slot as a named value. The procedure layer re-emits the selection, which is the right shape.
Not fixed on this PR, because it is superseded (see the description). Recorded as a requirement for the redo of the hot run path: a field bound to a mask holds its expression, and a slot is re-emitted in the current epoch at each use.
Generated by Claude Code
| dialect | ||
| .call(step.opcode, [0, 0, 0], &mut stack) | ||
| .map_err(|error| ExecRefusal::Fold { effect: i, error })?; |
There was a problem hiding this comment.
With the default BoolMode::InPlace, an admitted sequence such as m1 = a < 5; m2 = b < 10; m3 = IntAnd(m1, m2); n = PopCount(m2) counts the intersection instead of the original m2. The field map retains copies of mask slots, but FoldDialect::and_peephole gates the last predicate in place and returns that predicate's existing slot. Consequently, writing m3 silently changes the value still associated with m2. Use alias-safe lowering, such as the fused expression mode or an independent mask result when the operand remains live, before exposing these calls as ordered field assignments.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed by reading lib.rs:650-665. Under BoolMode::InPlace, and_peephole gates the last emitted Pred under the other operand and returns that predicate's own slot. run keeps that slot under the earlier field too, so writing m3 = IntAnd(m1, m2) changes what m2 refers to. The peephole assumes stack discipline, where an operand is consumed once. A binding that names its intermediate values breaks that assumption.
Not fixed on this PR, because it is superseded. Recorded for the redo: either the binding lowers in the fused expression mode, or the peephole is skipped while the operand is still live.
Generated by Claude Code
… compiled)
Seven arms on SUM { a : a < t }: direct ndarray, ClassId → LazyLock
prebound callable, prebound plus the dt64 guard R1 runs, mask-risc
prepared, R2IL prepared (FoldDialect once, CompiledProgram kept),
FoldDialect per call, and R1 binding::run.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
…tup) Measured on 4 cores, median ns per call, answers asserted equal across arms: 64 rows: direct 29.4, prebound 30.0, +guard 60.9, mask-risc prepared 103.3, r2il prepared 103.2, dialect 205.9, R1 run 398.4. R1 runs FoldDialect once per call and allocates 5 times per call; prepared paths allocate 0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
…clusion The R1 arm discarded failures with if let Ok; every arm now counts calls that returned the oracle's answer and the run fails unless that count equals the call count. Board entry records the 4-row-size table (65,536 included), the conclusion (prepared R2IL equals prepared mask-risc; R1's extra cost is its interpreter and receipt) and the operator decision on #1892. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
Superseded, do not merge. Kept intact as measured evidence until a clean successor replaces it. The OGAR-body rationale in the original description below is itself superseded by the operator. It is not a merge requirement for anything.
Benchmark result
crates/math-polyfill-probe/examples/r1_vs_prebound.rsruns seven arms over the same operation,SUM{a : a < t}, with identical inputs, outputs and preparation boundaries. Every timed call of every arm is checked against the oracle, and the run fails unless the count of correct answers equals the call count.Median ns per call,
MPF_REPS=31, 4 cores. Three runs: one was disturbed by load and is not used; the other two agree.Allocations per call: 0 for every prepared arm, 1 for the dialect run, 5 for R1.
Conclusion.
FoldDialecton every run, keeps per-runBTreeMapvalues, rebuilds the stack, and allocates the receipt.Successor (in progress)
The successor prepares executable mask-risc programs once, through the
FoldDialectcompilation andCompiledProgrammachinery D-MPF-4 proved. It keeps multi-fold ordering and every refusal, and keeps frame, route, focus, scope and permit validation independent.ExecPermitstays a lab permission, not a production authorization claim.Original description
binding::preparelowers the hand-authored DT64MethodBinding::effectsinto R2IL opcodes, with an optional R2IL reading of an admitted DT64MethodBindingsplit into a coldprepareand a hotrun. Words bind to opcodes by label through OGAR's vocabulary, with a bounded receipt. 14 tests and 11 disable runs, all red as expected. It found one defect:FoldDialect's lane compares saturate out-of-range constants.🤖 Generated with Claude Code
https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF