Repository navigation
T emit go/rust bounds - #681
Conversation
|
Review finding: This test does not establish the receipt it names. That means CI can go green while checking only Rust, with If this is meant to be a real closure gate, the test should fail or be explicitly ignored/skipped at the test level when the required toolchains are unavailable. As written, it is a useful local parity harness, but not a truthful proof that |
…3 Python exclusions python.dag was missing seven Int operator realizations that Rust and Go already had: mul (*), div (//), ne (!=), lt (<), le (<=), gt (>), ge (>=). This unblocked list_map_then_fold_twelve (uses *), list_filter_then_fold_seven (uses >), and nested_list_builtins_inside_lambda_six (uses * inside a lambda) from Python emission — all three were excluded from PYTHON_EMIT_EXCLUDE with a MissingOperatorRealization note. After regenerating bootstrap and lifting those exclusions, the Python determinism matrix now covers 8/9 PROGRAM_FIXTURES (same as Go), and the emit_omni_demo_fixtures_green closure test checks 8 fixtures instead of 5. The sole remaining Python exclusion is recursive_function_call_six (Loop). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…h python.dag snapshot Register `tests/boundary/m1_5_emit_omni_demo_test.rs` in `EXPECTED_HAND_AUTHORED` with director-approved receipt (T-Emit lane closure, sharp-heron-47). Refresh `parse_corpus_manifest.txt` to reflect `python.dag`'s updated item count and hash after gaining 7 operator realizations (`mul`, `div`, `ne`, `lt`, `le`, `gt`, `ge`). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…in assert Split the single test into two: - `emit_omni_demo_rust_roundtrip` (non-ignored): CI gate that runs unconditionally; proves the omni fixture set emits valid, executable Rust. - `emit_omni_demo_fixtures_green` (#[ignore]): T-Emit lane closure receipt. Marked ignore because go/python3 are absent in CI. When run with --ignored it asserts both toolchains are reachable and fails hard if either is missing — a missing toolchain is an unmet receipt, not a skip. Addresses review finding: prior implementation returned None for absent toolchains and passed with 0/N targets checked, making it a useful local harness but not a truthful lane-closure proof. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Review metadata
Findings
Neither is a substrate / invariant / modeling-discipline violation. The boundary test is properly documented as class-5 in VerdictAPPROVE_WITH_COMMENTS — Small, narrowly-scoped diff: six Python operator realizations, a three-way parity boundary test, and the exclusion list shrink this unlocks. Modeling discipline and census bookkeeping are respected. Only the Python floor-div semantic mismatch is worth following up on before the omni-fixture set grows. |
![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: 8a52a8fd64
ℹ️ 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".
| language: python_language | ||
| target: Int | ||
| op: OrderedRing.div | ||
| carrier: "//" |
There was a problem hiding this comment.
Using "//" for OrderedRing.div makes Python Int division floor toward negative infinity, while the existing Go/Rust realizations use "/" on int64/i64 (truncate toward zero). This introduces cross-target semantic drift for any program that can produce negative operands (for example, (-3) / 2 yields -2 in Python but -1 in Go/Rust), so emitted Python behavior can now disagree with the same DAG on other targets.
Useful? React with 👍 / 👎.
python_int_div: add comment at definition site pinning the known floor-vs-truncated divergence for negative dividends (-7/2 → -4 in Python, -3 in Rust/Go). Omni fixtures don't exercise this case; the constraint is pinned rather than fixed until a target-appropriate truncating-div primitive is modeled. m1_5_emit_omni_demo_test: replace bare temp-dir allocation with a RAII `TmpDir` wrapper whose `Drop` impl calls `remove_dir_all`. Repeated local runs with three toolchains × N fixtures no longer accumulate `v3_emit_omni_roundtrip_*` directories indefinitely. Regenerate bootstrap and refresh parse-corpus manifest for the python.dag comment addition. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Review metadata
Findings
Verdict |
…_idiv
Python's `//` is floor division, which diverges from Rust/Go integer `/`
(truncate toward zero) for negative dividends (-7/2 → -4 in Python, -3
in Rust/Go). This is a semantic correctness violation for any DAG that
produces negative integer division.
Fix:
- Add `__v3_idiv(a, b)` preamble helper using `divmod`-based adjustment:
if the remainder is non-zero and operand signs differ, adds 1 to the
floor quotient to restore C-style truncation toward zero.
- Change `python_int_div` carrier from `"//"` to the full-expression
template `"__v3_idiv({lhs}, {rhs})"`.
- Extend the Python emitter's binary-op rendering to detect full-expression
carriers (those containing `{lhs}`) and render them directly instead
of inserting into the `({lhs} {op} {rhs})` infix template.
Regenerate bootstrap and refresh parse-corpus manifest.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Both the floor-div finding (flagged P1 by Codex, P2 here) and the tmp-dir leakage have been addressed in subsequent commits on this branch. Current HEAD is Python
The earlier "pin comment" approach was superseded by the actual fix before this review was relayed. |
|
Review metadata
Findings
Exploratory observations
Verdict APPROVE_WITH_COMMENTS — lifts three Python exclusions with correct semantics (truncation-toward-zero pinned on all three targets), adds a real three-way parity test with an honest toolchain-assert (no silent skips), and labels the scaffold with a dissolution trigger. The carrier-overloading above is the only substrate concern and is narrow enough to defer. |
|
Review metadata
Findings
Verdict |
…expression templates
`ExpressionSyntax.binary_op` and `OperatorRealization.carrier` both
claimed authority over how binary expressions are rendered. The emitter
had to reverse-engineer carrier string content (`carrier.contains("{lhs}")`)
to decide which path to take — a string-sentinel violation of the modeling
discipline (INVARIANTS.md P2, Practice 5-6).
Fix: make `OperatorRealization.carrier` the sole authority.
- Remove `binary_op` from `ExpressionSyntax` in `std/emit_model.dag`.
- Remove `binary_op` from `python_expressions`, `go_expressions`, and
`rust_expressions` in all three spec files.
- Convert all infix operator carriers ("+", "-", "*", "/", "==", "!=",
"<", "<=", ">", ">=", "&&", "||", "and", "or") to full-expression
templates: `"({lhs} + {rhs})"` etc. Python's `__v3_idiv` carrier
gains outer parens to match: `"(__v3_idiv({lhs}, {rhs}))"`.
- All three emitters (`emit.rs`, `python_target.rs`, `rust_target.rs`):
remove `binary_op` field from the expression-syntax binding struct,
remove the `syntax_field_string("binary_op")` load, and replace the
three-binding template call with a direct two-binding render on the
carrier. The `carrier.contains("{lhs}")` probe in python_target.rs
is also removed — it is no longer needed.
Every `OperatorRealization.carrier` is now self-describing: it is always
a full-expression template with `{lhs}` and `{rhs}` placeholders, with
no external format convention required to interpret it.
Regenerate bootstrap and refresh parse-corpus manifest.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Review metadata
FindingsNone blocking. This PR is a textbook coprod-dissolution:
Exploratory observation (non-blocking)Authority for "binary-op carriers must reference VerdictAPPROVE — clean dual-authority dissolution, tracked scaffolding, honest receipts, semantic fidelity on Python |
|
Review metadata
Findings
Verdict: APPROVE_WITH_COMMENTS. The modeling/single-authority side looks clean, and the Rust omni roundtrip passed locally. My only concern is that the new Python operator behavior is not covered by an always-on behavior assertion. |
… lists PR #692 landed Behavior::Loop emission for both Python and Go. The sole remaining entry in GO_EMIT_EXCLUDE and PYTHON_EMIT_EXCLUDE was recursive_function_call_six (blocked on Loop support). Both lists are now empty; all 9 PROGRAM_FIXTURES are covered by the omni set and by the 5× determinism matrix for every target. Update stale comments in determinism_test.rs to reflect the current state. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…_structurally
The test was asserting `carrier == "+"` (old infix symbol form). After the
carrier unification in the previous commit, rust_int_add's carrier is now
`"({lhs} + {rhs})"`. Update the assertion to match.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…holders
`render_named_template` is silent when a carrier lacks the expected
placeholders — a carrier like "+" would emit literally "+" instead of a
binary expression. Add a load-time check in all three emitters that rejects
any OperatorRealization whose carrier does not contain both {lhs} and {rhs},
turning a silent runtime divergence into a fail-closed load error.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The new Python Int operators (mul, div, ne, lt, le, gt, ge) only had determinism coverage in CI — the rendered template content was never asserted. Add emit_python_int_operators_use_correct_expression_templates: five always-on (non-ignored) checks that verify each operator emits the expected Python token/call without requiring a Python toolchain. Specifically: * emits the * operator, / emits __v3_idiv(...), != emits !=, < emits <, > emits >. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Review metadata
Verdict: APPROVE. The diff looks clean and is directionally aligned with the rubric: removing Focused verification passed: |
Rebased session/eager-wren-78 onto origin/main (squashed prior merge skew). - Extend std.verification with AlgebraicLawKind + scaffold TestPredicate variants (ExecuteCommand, ForAllTargets, LensOutputEquals, DifferentialEquals, AlgebraicLaw) and documented dissolution triggers; single authority note on TestClaim. - Regenerate bootstrap fixtures + parse_corpus_manifest.txt for the new surface. - Add M1.5 verification + testgen integration coverage (fail-closed shell handling, runner-deferred boundaries without global panic-hook mutation). Emit/spec/boundary files match main (#681 emit paths retained). Made-with: Cursor
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a26eb13a· Trigger:schedule - Thinking:
353s wall
Non-blocking — Strengths
src/v3/std/emit_model.dagRemoving ExpressionSyntax.binary_op and moving full binary expression templates into OperatorRealization.carrier aligns with single-authority emission.
✅ No blocking concerns in the current diff.
1 participant
Opened from session-dashboard for session
sharp-heron-47.