Repository navigation
feat(05_eval): exact-arity gates — fail closed on excess signature/body/actual arity + comprep_eval_by_execution discriminating reds - #4634
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a3b9dd81· Trigger:schedule - Thinking:
332s wall
✅ The exact-arity gates and red claims are scoped to the existing COMPREP wave-1 scaffold, fail closed on oversized signature/body/actual inputs, and I found no blocking concerns.
|
Inherited review triage (bright-pike-355) Verified all four inherited dashboard/api-review artifacts against current HEAD (
No code changes required — the exact-arity gates ( Awaiting CI on the merge-from-main commit; reviews on prior SHA — sent from bright-pike-355 |
|
Review triage — dashboard artifacts #28250 (claude) and #28252 (cursor) Verified both APPROVE artifacts against current HEAD
Merge readiness: ≥2 distinct approvals on HEAD (claude + cursor), no REQUEST_CHANGES, mergeable=CLEAN, CI green (11/11). Ready for operator merge. — sent from bright-pike-355 |
…e SpanIndex substrate (honest scope) (#4643) * WIP: Provenance A-pivot (off-tree id+index) — RE-SPAWN (prior swift-cat died * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * fix(v4): re-anchor provenance comments after Node.span dissolution Update provenance.dag scope and source_authority.dag R3 gate comment to reflect off-tree SpanIndex + FromSource parse-mint as the surviving authority. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * fix(v4): merge main + drop stale node_span_unanchored in comprep eval claim Main #4634 added exact-arity gate fixtures using node_span_unanchored(); rebase onto occurrence_id substrate with SyntheticOccurrence. Fixes ci_floor_emit on PR #4643 merge commit. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: #4643 recovery closeout: fix OccurrenceIdRef sole-mint (no -1 sentinel), * fix(ci): execute occurrence_id exclusion witness in v4_lens_gate Register witness_occurrence_id_model_substrate_holds in lens_ci_gate.dag so v4-lens-ci-gate.sh runs the distinct-minted-id structural-equality proof with perturb-check — closes still-raven load-bearing gap (A). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * fix: deep occurrence_id exclusion in source_authority and edit_locus Shallow node_for_structural_equality only clears the root occurrence_id; nested minted ids still break bare ==. Route source_authority_node_equal and edit_locus node_eq through exact_structural_equality_zip_fold (P2 single authority). Strengthen witness with nested-mint case + shallow RED guard. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * test(provenance): add wave-1 parse_stamp SpanIndex witness (option A) Successor to #4651 parse_table_captured_tree_span_morphism: exercises parse_production stamping inside a single memo cell — terminal FromSource ByteRange + sequence DerivedBy child-id pair. Registered in lens_ci_gate for v4_lens_gate execution with perturb-check. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
…ells (F1 prov threading + F2 span_index_merge + F4 edit_locus off-tree consumer) (#4654) * WIP: Provenance A-pivot (off-tree id+index) — RE-SPAWN (prior swift-cat died * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * fix(v4): re-anchor provenance comments after Node.span dissolution Update provenance.dag scope and source_authority.dag R3 gate comment to reflect off-tree SpanIndex + FromSource parse-mint as the surviving authority. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Take over ORPHANED PR #4643 (prov-a-pivot-phase1-2) — prior owner lively * fix(v4): merge main + drop stale node_span_unanchored in comprep eval claim Main #4634 added exact-arity gate fixtures using node_span_unanchored(); rebase onto occurrence_id substrate with SyntheticOccurrence. Fixes ci_floor_emit on PR #4643 merge commit. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell * WIP: provenance wave-2: global SpanIndex coherence across memoized parse cell --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
Summary
Adds exact-arity fail-closed gates to the wave-1 add callee in
05_eval.dagso that oversized inputs (extra signature facts, extra body operands, or extra call actuals) are refused rather than silently dropped via prefix-match. Extends thecomprep_eval_by_executionkeystone witness in the manual claim file with three discriminating red tests, one per gate.Why now: The COMPREP wave-1 eval-by-execution keystone (#4624) proved that
addexecutes through real callee dispatch. This PR closes the remaining gap where a callee with four Int params, a body with four operands, or a call with three actuals would previously have been admitted as the canonicalInt,Int->Intadd shape — silently discarding the extra fact — violating Facts Flow Forward (INVARIANTS P3/P5).Changes:
src/v4/compiler/05_eval.dageval_rejected_argument_arity_excessdiagnostic symbol for excess-actual rejection.eval_actual_presenthelper: probeslist_nthand returns a Bool (true = index exists).eval_bind_wave1_arguments: before binding [0],[1], checks that index 2 is absent; rejects witheval_rejected_argument_arity_excessif present.eval_child_absenthelper: returns true iff a Node has no child at the given index.eval_wave1_add_signature: extended with&& eval_child_absent(node: arrow, wanted: 4)— the Arrow is[Int, Int, Int, body]; index 4 must not exist.eval_wave1_add_body: extended with&& eval_child_absent(node: body, wanted: 3)— the body is[+, x, y]; index 3 must not exist.src/v4/test/claim/manual/comprep_eval_by_execution.dagcomprep_excess_signature_arrow,comprep_excess_body_arrow,comprep_excess_actual_call.comprep_excess_signature_red_holds,comprep_excess_body_red_holds,comprep_excess_actual_red_holds) each asserting the run returns non-passing.comprep_eval_by_execution_keystone_holdsextended with all three conjuncts.Test plan
# Local claim-run witness (the keystone Bool witness executed by v4_lens_ci / glob discovery): cargo build --release -p v2-compiler target/release/gunbc run \ --source-root src/v4 \ --entry src/v4/test/claim/manual/comprep_eval_by_execution.dag \ --function comprep_eval_by_execution_keystone_holds \ --claim-runCI (
v4_lens_gate,v4_lens_ci,ci_floor*) runs the glob-discovered claim corpus including this witness on every push.The three new
*_red_holdsconjuncts in the keystone witness are the discriminating signal: before this PR, the gates were absent and each oversized input would have produced a passing run result (silently discarded the extra fact). With the gates in place, every malformed input now causes the run to be rejected, and the== falseassertions hold.Checklist