[devin-ai-integration]

What and why

SequenceFunctions::excludingAt reported ErrIndexOutOfRange for a start one past the end, an end past the end or an inverted range — (1, 2, 3)->excludingAt(4) and (1, 2, 3)->excludingAt(3, 2) failed with "start index 4 is outside 1..3" / "end index 2 is outside 2..3" — where its normative library body answers the sequence unchanged. builtinSequenceExcludingAt validated both endpoints against the sequence before modelling the two subsequence calls of the body; the compiled Go and C helpers (sysmlExcludingAt, sysml_excluding_at) did the same.

The body is now followed literally in all three places: the positions before startIndex, then the positions after endIndex. The only remaining checks are the ones the body itself makes — a start beyond size + 1 makes subsequence(1, startIndex - 1) evaluate seq#(size + 1) (an index error), and an index below 1 is no Positive.

Before → after, on (1, 2, 3):

expression	before	after (= body)
excludingAt(2), excludingAt(1, 2)	[1, 3], [3]	unchanged
excludingAt(4) (start = size + 1)	ErrIndexOutOfRange	[1, 2, 3]
excludingAt(4, 9)	ErrIndexOutOfRange	[1, 2, 3]
excludingAt(2, 9) (straddling)	ErrIndexOutOfRange	[1]
excludingAt(3, 2) (inverted by one)	ErrIndexOutOfRange	[1, 2, 3]
excludingAt(3, 1) (wider inversion)	ErrIndexOutOfRange	[1, 2, 2, 3] — subsequence(1, 2) then subsequence(2), the overlap repeated
()->excludingAt(1)	ErrIndexOutOfRange	()
excludingAt(2, 9223372036854775807)	ErrIndexOutOfRange	[1] (the tail is selected only when the end lies inside the sequence, so no end + 1 arithmetic on an unbounded end)
excludingAt(5) (start > size + 1)	ErrIndexOutOfRange	ErrIndexOutOfRange ("start index 5 is outside 1..4": seq#(4) in subsequence(1, 4))
excludingAt(0), excludingAt(1, 0)	ErrIndexOutOfRange	ErrIndexOutOfRange (no Positive)
subsequence(2, 5)	ErrIndexOutOfRange	ErrIndexOutOfRange (unchanged: 2..5 evaluates seq#(4))

subsequence was checked against the same body and left as it is: (startIndex..endIndex)->collect {in i; seq#(i)} evaluates every position of the range, so an end past the end reaches a genuine seq#(i) out-of-range and stays that typed error; an inverted range is empty and stays the empty sequence. seq#(i) out-of-range semantics are untouched.

Over an undetermined operand (xs : Real[2..4]): excludingAt(xs, 5) is now <undetermined> (a four-element value admits it), excludingAt(xs, 6) is the error; the other definite-error probes (excludingAt(xs, 0), excludingAt(xs, 1, 0), subsequence(xs, 2, 5)) are unchanged.

The v1 migration notes for ExcludeAt/excludeAt/removeAt and ReplacingAt/replacingAt/replaceAt (internal/translate/migrate/primitives.go, docs/reference/sysml-v1-migration.md) say the narrowed difference: v2 now fails only on an index outside 1..Size(seq)+1, and replacingAt appends at Size(seq)+1.

Specification basis

KerML 1.1 Beta 2 §9.4.14 Sequence Functions has no prose for excludingAt or subsequence; the bodies in the normative library (vendored Kernel Libraries/Kernel Function Library/SequenceFunctions.kerml) are the definition:

function excludingAt{ in seq: Anything[0..*] ordered nonunique;
    in startIndex: Positive[1]; in endIndex: Positive[1] default startIndex;
    return : Anything[0..*] ordered nonunique =
        (seq->subsequence(1, startIndex - 1), seq->subsequence(endIndex + 1)); }
function subsequence{ in seq: Anything[0..*] ordered nonunique;
    in startIndex: Positive[1]; in endIndex: Positive[1] default size(seq);
    return : Anything[0..*] = (startIndex..endIndex)->collect {in i; seq#(i)}; }

docs/project/spec-compliance.md: the row "An endpoint of subsequence or excludingAt that is outside the sequence …" (⚠️ Approximate, describing this gap) is rewritten to the fixed behaviour with the body quoted, ✅ Faithful; the SequenceFunctions summary row loses its "except the out-of-range endpoints" qualifier. The pinned pilot evaluates excludingAt natively, not by the body, and is split (agrees for in-range and by-one inverted, throws for a start or end past the end, drops the overlap of a wider inversion); the row says the body wins.

How it was verified

New tests (four layers):

• golden AST tests/parser/testdata/parse/calc_sequence_excluding_at.{sysml,golden}
• execution conformance calc_sequence_excluding_at, _past_the_end, _straddling, _inverted, _out_of_range, _zero, calc_sequence_subsequence_past_the_end (no trace fixture: nothing here is ordering-sensitive)
• internal/exec/runtime/robustness_excluding_at_test.go TestRuntimeRobustnessExcludingAt
• TestCollectionResults / TestCollectionOperationErrors / TestDefiniteLibraryErrorsSurviveOpenOperands / TestUndeterminedLibraryResults re-adjudicated to the body (the old error expectations for excludingAt(4), (2, 1), (2, 9), ()->excludingAt(1) become result expectations; excludingAt(5), (0), (1, 0), ()->excludingAt(2) keep the error)
• tests/codegen Seq::ExAt gains the past-the-end, straddling, inverted, zero-end and empty-source cases, interpreter as oracle, Go and C targets

Gates (corpora fetched: training examples, pilot corpora, spec examples, pilot library XMI, PSSM suite; Reference FMUs not fetched, that gate skipped here):

• go build ./... ✓, go vet ./... ✓, gofmt -l . empty ✓
• go test ./... ✓ (every package ok; cmd/sysml and tests/codegen hit the default 10 m timeout under the full-suite load on this machine and pass when re-run with -timeout 40m, 310 s and 342 s)
• python3 scripts/changelog.py check ✓, mkdocs build --strict ✓

Pilot-exec referee (go run -C tools ./cmd/pilot-exec-diff, pilot 0.62.0, develop's pin), 500 → 504 cases; every moved or new row:

case	before	after	which side is right
w6d:excluding-at-out-of-range (1,2,3)->excludingAt(4)	both-error	pilot-error	body: [1, 2, 3]; pilot throws IllegalArgumentException: fromIndex(4) > toIndex(3) from a Java sublist
undetermined:excludingat-unbound-past excludingAt(xs, 5), xs : Real[2..4]	both-error	pilot-error	body: <undetermined> (a four-element xs admits start 5); pilot throws IndexOutOfBoundsException over its one unevaluated element
w6d:excluding-at-beyond-the-end excludingAt(5) (new)	—	both-error	both fail; ours is seq#(4)
w6d:excluding-at-straddling excludingAt(2, 9) (new)	—	pilot-error	body: [1]; pilot throws fromIndex(9) > toIndex(3)
w6d:excluding-at-inverted excludingAt(3, 2) (new)	—	agree	[1, 2, 3]
w6d:excluding-at-inverted-overlap excludingAt(3, 1) (new)	—	disagree	body: [1, 2, 2, 3]; pilot [1, 2, 3] (its native implementation drops the overlap)

Bucket totals: agree 228 → 229, disagree 37 → 38, pilot-error 4 → 7, both-error 17 → 16, the rest unchanged. The referee has no committed baseline; docs/project/pilot-execution-referee.md and the testing-pilot-execution-referee skill anchor record the counts as measured (case total, bucket lists and the prose on excludingAt(xs, 5)). After the merge of develop (#1538's ten empty_second_operand.cases, all pilot-unevaluated) both files say 514 cases over twenty-three fixtures and agree 229 · kind-only 1 · order-only 0 · disagree 38 · differs-by-design 5 · pilot-unevaluated 167 · pilot-silent 24 · pilot-error 7 · ours-error 10 · ours-undetermined 17 · both-error 16 · nondeterministic 0, which is what go run -C tools ./cmd/pilot-exec-diff prints on the merged tree; TestDocumentedCaseCount passes. Only the case total is gate-checked, so the fenced bucket block of the doc, missed at first, was corrected by hand against that run.

Merge with develop: origin/develop at 0286c9845 (after #1538, #1541, #1542, #1544–#1547 landed) is merged in with one merge commit; the two conflicts were the case total and the bucket lists of docs/project/pilot-execution-referee.md and .agents/skills/testing-pilot-execution-referee/SKILL.md, resolved to carry both #1538's rows and these (above). On the merged tree: go build ./..., go vet ./..., gofmt -l . empty; go test of internal/exec/runtime, tests/migrate, internal/translate/..., tests/codegen (TestCompiledCalc*) and tools/referee/exec pass; python3 scripts/changelog.py check and mkdocs build --strict pass; the pilot-exec referee gives the 514-case totals above. Earlier dry merge against #1529 chore/pilot-pin-2026-09 at 8a100b317 (still open): clean; the pilot-exec referee at its 2026-09 pin (0.63.0, evaluator rebuilt from #1529's pilot-pin.sh) gives the same bucket totals and the same verdict for every excludingAt row as the 0.62.0 run above.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/4793fedf215e4fca9ddc5ff9cbb45786
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/4793fedf215e4fca9ddc5ff9cbb45786?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring