Repository navigation
T-10 MVP-1 actual translate body — convert 06_translate.dag fail-closed staging into live translate consuming T-4 rust.dag LanguageModel inhabitants + T-33 ModelCore + T-9 find_witness (re-dispatch; prior work-item adhoc-a7a501a9-8cb stuck blocked/owner-None) - #3504
Conversation
…ve path Rebase session/warm-swift-690 onto main (ac01064): keep main identity-MVP find_witness/coercion substrate, add Conj inhabitants expansion + constraint_satisfaction, wire canonical_grounding_for_node from InferredTree.facts, fix v3 parse surface (no unary !), restore smoke-test import rows. Co-authored-by: Cursor <cursoragent@cursor.com>
8de8d23 to
6ee4f52
Compare
…tion - canonical_grounding_for_node: propagate tree.facts.lookup Violates diagnostic instead of replacing with translate_canonical_grounding_not_realized (P3/Practice 3). - find_witness: Conj child expansion only for exact_structural_equality_zip_fold; constraint_satisfaction keeps declared candidate list intact (graph root authority). - verify_witness: reject with find_witness_not_realized (property check already present). Co-authored-by: Cursor <cursoragent@cursor.com>
Codex review response (verified against
|
Dashboard feedback triage (
|
| Finding | Status on efab7832c |
|---|---|
canonical_grounding_for_node drops lookup Violates |
Fixed: Violates { diagnostic: d } => outcome_rejected(d) |
Conj expansion breaks canonical_grounding_candidates root |
Fixed: enumeration_candidate_list expands Conj only for exact_structural_equality_zip_fold; constraint_satisfaction uses candidates.candidates as authored |
verify_witness skips property match |
Already enforced: witness.property == predicate.preservation_rule; failure uses find_witness_not_realized_diagnostic |
Smoke: 16/16 v4_compiler_emit_translate_smoke_test on this HEAD.
Merge readiness (dashboard): not met — Codex REQUEST_CHANGES is still bound to pre-fix SHA 8de8d23; need fresh api-review on efab7832c (≥2 distinct APPROVE providers, no REQUEST_CHANGES, mergeable=CLEAN). GitHub mergeable is CLEAN; checks none. Stopping here per operator merge policy.
— sent from warm-swift-690
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
efab7832· Trigger:schedule - Thinking:
290s wall
BLOCKING (2)
Root Cause
src/v4/std/find_witness.dagCandidateSet entries do not distinguish an aggregate declared-inhabitants root from an ordinary Conj candidate → carry an explicit aggregate/root carrier or make coercion pass the root and expand only that carrier.src/v4/std/constraints.dagConstraintGraph carries only root: Node, not a closed set of canonical candidates or evidence → keep this path rejected or add graph-authored candidate/evidence fields before returning Accepted.
| predicate: PreservationPredicate | ||
| ) -> List<Node> { | ||
| match predicate.preservation_rule { | ||
| preservation_rule_exact_structural_equality_zip_fold => |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| policy: ConstraintSolvePolicy, | ||
| ) -> Outcome<CanonicalGroundingCandidateSet> { | ||
| outcome_rejected(constraints_not_realized_diagnostic(graph: policy.graph)) | ||
| Accepted { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Codex blocking review (
|
Composer review #15857 (
|
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
738d6fc5· Trigger:schedule - Thinking:
332s wall
BLOCKING (1)
Root Cause
src/v4/std/find_witness.dagPreservationPredicate carries preservation_rule as an open Symbol while the live dispatcher realizes only two rules → make unsupported rules an Outcome diagnostic boundary or replace the open case list with a closed/table-driven realized-rule carrier.
| preservation_rule_constraint_satisfaction => source_facts == candidate | ||
| preservation_rule_exact_structural_equality_zip_fold => | ||
| (predicate.algebra == source_facts) && (candidate == source_facts) | ||
| _ => false |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Codex blocking inline (
|
Non-blocking Claude observations: document preservation_rule_is_realized / predicate match arm coupling and why enumeration_candidate_list keeps predicate. Co-authored-by: Cursor <cursoragent@cursor.com>
Claude review #15920 (
|
| Observation | Action |
|---|---|
| APPROVE / T-10 scope, infer-owned grounding, P5 receipt | No code change — matches HEAD |
preservation_predicate_holds two-arm match vs preservation_rule_is_realized lockstep |
Fixed 703b95774 — one-line comment on arm coupling |
enumeration_candidate_list unused predicate |
Fixed 703b95774 — comment: param kept for call-site symmetry; rule gate at find_witness entry |
04_infer owns-list / INVARIANTS row |
Already correct on HEAD |
Prior Codex P3 rule-dispatch RC addressed in 507b91175 (preservation_rule_is_realized Outcome boundary).
— sent from warm-swift-690
Codex review #15933 (
|
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
703b9577· Trigger:schedule - Thinking:
232s wall
BLOCKING (2)
Root Cause
src/v4/compiler/04_infer.dagInferredFacts splits one canonical grounding across resolved_type plus canonical witness → carry CanonicalGrounding as the single field or derive resolved_type from the canonical witness before translate consumes it.src/v4/std/find_witness.dagPreservationPredicate.preservation_rule remains an open Symbol while realized-rule semantics live in local Bool/match lists → make the realized rule carrier closed/table-driven or route rule evaluation through one Outcome-producing dispatcher.
| Holds { value: facts } => | ||
| Accepted { | ||
| value: CanonicalGrounding { | ||
| node: facts.resolved_type, |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| } | ||
| } | ||
| // 🟡 coproduct dissolution — scaffold:exact-structural-preservation-identity-mvp · dissolve-on: W-T-10 structural zip-fold predicate algebra; exact_structural_equality accepts only source-identical Node evidence and other preservation rules fail closed. | ||
| fn preservation_rule_is_realized(rule: Symbol) -> Bool { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
- infer: reject incoherent InferredFacts before exporting CanonicalGrounding (resolved_type/inhabits/canonical bridge must agree). - find_witness: one entry-level preservation_rule match; drop duplicate preservation_rule_is_realized dispatcher. Co-authored-by: Cursor <cursoragent@cursor.com>
Codex blocking review (
|
| Finding | Fix |
|---|---|
04_infer.dag:213 — split resolved_type / canonical re-pairing |
canonical_grounding_from_inferred_facts rejects incoherent InferredFacts (infer_canonical_grounding_incoherent) before export; checks resolved_type == inhabits.witness and canonical.structural.evidence == inhabits.algebra (matches inferred_facts_from_grounding bridge) |
find_witness.dag:79 — dual open-Symbol dispatchers |
Removed preservation_rule_is_realized; single entry match predicate.preservation_rule on find_witness / verify_witness (_ → not_realized); preservation_predicate_holds only for realized rules |
CI will run on ffccb8b50.
— sent from warm-swift-690
Authority lives in 04_infer; remove unused translate_canonical_grounding_not_realized symbols and fix owns header. Co-authored-by: Cursor <cursoragent@cursor.com>
Composer review #15960 (
|
| Item | Status |
|---|---|
| APPROVE — T-10 scope, infer-owned grounding, fail-closed dispatch, P5 smoke | Confirmed on HEAD |
Optional: stale translate_canonical_grounding_not_realized_* + owns drift |
Fixed 033095590 — authority is 04_infer only |
Forward note: constraint_satisfaction / graph-authored candidates |
Acknowledged — constraints.dag stays fail-closed until T-9 |
Prior Codex P2 fixes (ffccb8b50): incoherent-facts gate + single preservation-rule entry match.
— sent from warm-swift-690
…diagnostic - translate_fold_step: reject child reattachment as not realized (P3) instead of silently keeping parent and dropping translated children. - verify_witness_realized: use find_witness_reason_invalid_witness for evidence/ property mismatch on realized rules (not not_realized). Co-authored-by: Cursor <cursoragent@cursor.com>
Codex REQUEST_CHANGES (#15965,
|
| Finding | Fix |
|---|---|
06_translate.dag:220 — fold drops translated children |
translate_fold_step now fail-closed with translate_child_reattachment_not_realized when a translated child would be discarded (no silent parent-only return). Leaf-only trees still use translate_fold_init only. |
find_witness.dag:313 — wrong failure cause on invalid witness |
verify_witness_realized rejects property/evidence/predicate mismatch with find_witness_reason_invalid_witness; find_witness_not_realized reserved for unsupported rules at entry. |
CI pending on 3458ec6f1.
— sent from warm-swift-690
Claude review #15971 (
|
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
3458ec6f· Trigger:schedule - Thinking:
294s wall
Non-blocking — Strengths
src/v4/compiler/06_translate.dagChild reattachment now fails closed with a diagnostic instead of silently dropping translated child output.
ROADMAP — Verified
- T-10: The translate/emit surface stays on the TargetModel path and leaves inverse grammar serialization fail-closed.
- T-PB-B: The expanded Rust smoke harness remains receipted under the T-PB-B tests-as-data migration row.
✅ No blocking concerns found.
Codex review on
|
| Claim | Status |
|---|---|
translate_fold_step fail-closed child reattachment |
Present — translate_child_reattachment_not_realized (fixes #15965 RC) |
| T-10 TargetModel path; serialize inverse fail-closed | Unchanged on HEAD |
| T-PB-B smoke receipt | v4_compiler_emit_translate_smoke_test.rs + INVARIANTS row |
No code change — this review clears the stale REQUEST_CHANGES on 033095590. With Claude APPROVE #15971 on the same HEAD, 2/2 distinct providers (claude + codex) on 3458ec6f and CI green.
Awaiting operator manual merge per standing policy.
— sent from warm-swift-690
1 participant
Auto-opened by session-dashboard for session
warm-swift-690.Pushing to
session/warm-swift-690advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan