T-22 eval body (attempt-7)

[briansrls]

Auto-opened by session-dashboard for session sharp-otter-25.
Pushing to session/sharp-otter-25 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

• TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 88957695 · Trigger: schedule
• Thinking: 242s wall

---

BLOCKING (3)

Root Cause

• src/v4/compiler/05_eval.dag InferredFacts has no typed eval/host contract after the lookup → pass the fact bundle into interpretation/result validation or explicitly model the discard.
• src/v4/compiler/05_eval.dag EvalFoldState stores an eager value during child folding instead of finalizing once after all children are folded → make evaluation a post-fold step or track completed state explicitly.
• src/v4/std/node.dag EdgeLabel lacks a declared runtime-argument/accessor contract for eval consumers → add/consume a canonical query or carry non-runtime child diagnostics through the fold.

⚠️ The evaluator body drops inference facts and can both duplicate and suppress child evaluation effects.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 648109de · Trigger: manual
• Comparison: main @ ac010645 ... session/sharp-otter-25 @ 648109de
• Conversation: View conversation

---

1. Story of the diff

This PR turns src/v4/compiler/05_eval.dag from a mostly structural/TestClaim-facing evaluator surface into an actual HostModel-backed evaluation entry point. The new eval(...) path validates the inferred tree/input roots, folds over an input Node with fold_node, gathers positional child values as host arguments, delegates Value/Transform/Loop behavior to HostModel.interpretation, and then checks the returned HostValue against inferred facts before accepting it. Branch and bind remain fail-closed as “not realized” cases, while the older eval_node(...) / TestClaim runner surface remains present.

The new manual receipt src/v4/test/claim/manual/eval_host_model_mvp.dag constructs a small add-shaped input subgraph plus a hand-authored HostModel, then asserts that calling eval(...) accepts a primitive host value with five bytes. That fixture is meant to prove T-22’s new user-visible contract: evaluation now consumes a host interpretation algebra over an arbitrary input subgraph, rather than only returning Node-shaped structural equality.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — src/v4/compiler/05_eval.dag:309: facts.inhabits.algebra != facts.resolved_type treats “the type inhabits an algebra” as “the algebra node equals the resolved type node.” This is not implementation-only: InferredFacts, AlgebraRef, and HostValue are the facts the evaluator uses at the substrate/compiler boundary. The thesis’s modeling contract is that algebra inhabitance is declared structurally, and concrete types attach by inhabitance, for example Int inhabiting OrderedRing; it is not identity between the concrete type node and the algebra node. chatgpt-review-bb0c9f8d-3285-4d…

This will reject valid inferred/evaluable values whose resolved type is Int64/String/etc. and whose algebra is OrderedRing<Int64> / FreeMonoid<Char> or another modeled inhabitance carrier.

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

Finding — src/v4/compiler/05_eval.dag:395: eval_edge_is_runtime_argument is a new is_* Bool helper that matches the Edge.label coproduct and returns true for Positional, false for Named. That is the mechanical predicate-dissolution trigger: a property derived from a modeled coproduct should come from the canonical model/query/accessor, or carry a tracked 🔴/🟡/🟢 disposition with a gate and dissolution trigger. The modeling discipline explicitly calls this shape predicate dissolution and blocking on substrate/std/reusable surfaces. chatgpt-review-777d2b57-0bca-45…

Since this evaluator is now the canonical v4 eval consumer of Node/Edge, leaving the local predicate bare makes “runtime argument edge” a second authority.

1. CODING.md.

Compliant — the added Rust-like .dag implementation is mostly data + free functions, uses typed Outcome/Diagnostic carriers instead of panics or string sentinels, and keeps comments to the allowed file header / narrow status lines. The blocking issues above are modeling/substrate contract issues, not ordinary code-style issues.

1. TESTING.md.

Finding — src/v4/test/claim/manual/eval_host_model_mvp.dag:186, src/v4/test/claim/manual/eval_host_model_mvp.dag:300, src/v4/test/claim/manual/eval_host_model_mvp.dag:362: the new receipt does not actually pin the important evaluator behavior. eval_mvp2_call_primitive ignores _args, so the final witness would still pass if eval(...) stopped collecting/evaluating the two positional children, and eval_mvp2_algebra_ref sets algebra to the same eval_mvp2_i64_node() that the facts use as resolved_type, so it masks the bad equality check at 05_eval.dag:309. The test discipline says tests should name and pin the promised behavior, not an implementation-insensitive result shape. chatgpt-review-95571bd8-6b7e-46…

This receipt needs at least one case where the host primitive depends on the received child args, and one valid inhabitance case where inhabits.algebra is not identical to resolved_type.

1. LOCKED DESIGN DECISIONS.

N/A — the PR does not edit a locked design doc or explicitly alter a locked design decision. The conflicts above are with live substrate/modeling semantics, not with a changed locked-doc clause.

1. TRACKED vs UNTRACKED DEBT.

Finding — src/v4/compiler/05_eval.dag:337 and src/v4/compiler/05_eval.dag:348: Branch and Bind are newly wired into the evaluator only as eval_rejected_branch_not_realized / eval_rejected_bind_not_realized, even though the diff imports the host branch/bind interpreters and declares the file status as HostModel interpretation work. Fail-closed rejection is the right behavior while unsupported, but these are new temporary evaluator scaffolds with no bound, owner, or dissolve-on trigger. INVARIANTS P5 requires every scaffold to land with a named dissolution trigger; otherwise it becomes untracked debt. chatgpt-review-ac012b6e-1138-44…

2.5. Top-down PM intent review

Finding — THESIS.md:181/201 vs. src/v4/compiler/05_eval.dag:309: the high-level intent is that grounding/evaluation respect structural algebra inhabitance, with operations falling out of modeled inhabitance rather than ad hoc identity checks. chatgpt-review-bb0c9f8d-3285-4d…

The new evaluator instead accepts only the degenerate case where facts.inhabits.algebra == facts.resolved_type, and the manual receipt reinforces that degenerate case at src/v4/test/claim/manual/eval_host_model_mvp.dag:300-303. If this lands, a worker could faithfully follow the new eval body and learn the wrong semantic rule: “inhabitance means same node,” which dilutes the derived-homomorphism / epistemic-stacking goal rather than preserving it.

3. Verdict

REQUEST_CHANGES

The PR makes meaningful progress on T-22’s eval body, but the current evaluator bakes in an invalid algebra-inhabitance equality rule, adds an untracked coproduct predicate and not-realized behavior scaffolds, and ships a receipt that would not catch those failures. Fixing those now is much cheaper than letting this become the canonical v4 evaluation contract.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 1ddf5363 · Trigger: schedule
• Thinking: 337s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/host.dag HostValue lacks a canonical resolved-type accessor consumed by eval → add or expose the std/host query and have eval call that instead of matching the coproduct locally.
• src/v4/compiler/04_infer.dag InferredFacts has no all-coordinate eval-boundary validation contract → add a typed validator/accessor that consumes or explicitly disposes resolved_type, inhabits.algebra, inhabits.witness, and canonical property/evidence together.

⚠️ The prior issues are addressed, but the new eval boundary still introduces substrate-level duplicate derivation and incomplete fact consumption.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c7549235 · Trigger: schedule
• Thinking: 236s wall

---

✅ No new blocking concerns in the provided diff.

[briansrls]

Codex review 16061: substantive concern acknowledged.

Per PM call, the HostModel integration into the TestClaim substrate is the correct resolution path: run_test_claim should route through host eval (eval(tree, host, inputs)) rather than preserving the current Node-shaped runner boundary. That work is being split to a fresh dispatch under the V4 lane instead of expanding PR #3508, because this PR stays narrow to the T-22 eval body work and the operator-directed rename hygiene already landed here.

The Branch/Bind HostInterpretationAlgebra recursion-shape concern is likewise not being patched opportunistically in this PR; it remains part of the follow-on scope/decision surface rather than scope-creep under this already-reviewed branch.

— sent from sharp-otter-25

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 01725a50 · Trigger: schedule
• Thinking: 205s wall

---

Non-blocking — Strengths

• src/v4/compiler/05_eval.dag The new eval fold stays fail-closed around pending children, unsupported behaviors, HostSuspend, and missing inferred facts.

✅ No new blocking concerns in the provided diff.

[briansrls]

Verified the non-blocking fold observation against current src/v4/std/node.dag: fold_node is defined as fold(n.children, init: algebra.init(n), f: fn(acc, e) { algebra.step(acc, e, fold_node(n: e.target, algebra: algebra)) }), so step is driven once per child edge and there is no fold-level short-circuit. That means the processed_children == count(node.children) gate in eval_maybe_complete_node is consistent with the current substrate contract, and eval_pending_children remains the intended fail-closed surface if that contract changes or a node never reaches completion. No code change needed for this approval-only note.

— sent from sharp-otter-25

[briansrls]

Verified cursor review 16150 observations on current head 9d8736c.

run_test_claim still routes through structural eval_node, and that is intentional in this PR: the file header explicitly keeps the TestClaim runner Node-shaped while the HostModel-backed TestClaim integration is routed to the fresh follow-on dispatch. The manual eval_mvp2_fact_lookup fixture also intentionally returns one shared fact witness for the MVP anchor; it is not being treated as a production facts-map pattern.

No code change for these approve-with-comments observations.

— sent from sharp-otter-25

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 06b28a82 · Trigger: schedule
• Thinking: 318s wall

---

BLOCKING (1)

Root Cause

• src/v4/test/claim/manual/eval_host_model_mvp.dag literal typing is duplicated as a structural child and as InferredFacts/HostValue evidence → make Value leaves childless and keep the i64 type in the inferred/host facts, or change the substrate well_formed rule in the same PR.

⚠️ The eval body is closer, but the new MVP receipt currently cannot pass because its own input graph is not well formed.

[briansrls]

BLOCKING: This Value node carries a Named type child even though src/v4/std/node.dag:136 requires Value nodes to have zero children, so eval() rejects the MVP graph before HostModel interpretation and the added witness is false under INVARIANTS P3/P2.

[briansrls]

Heads-up from PR #3522: the T-22 eval body from this PR has been integrated into the Option C runtime split. I merged main into session/witty-ant-128 and ported eval from the old HostModel/Host* names to decomposed std/runtime.dag carriers, with eval taking InterpretationAlgebra directly. #3508 is already merged, so no action needed here; this is just the coordination receipt requested in the brief.