feat(verify): bind the in parameters of a constraint or requirement at check time

[devin-ai-integration]

What and why

A constraint def or requirement def may declare in parameters its condition reads (requirement def Under { subject s : Thing; in limit : Integer; require constraint { s.v < limit } }). Until now only a verification case could supply them, through RunAnalysis's arguments/named_arguments; asking the requirement directly left the parameter unbound and the condition failed over an empty value with a misleading type error. Workflows that gate a step on a requirement about the run's own values (a stereo pair's acquisition ids, a pod's thread count) had to wrap every such requirement in a case.

VerifyConstraint and VerifyRequirement now take the same bindings RunAnalysis does:

• Runtime — Context.CheckConstraintWith / CheckRequirementWith(sym, scope, self, CheckArgs{Positional, Named}) bind the element's in parameters (inherited and redeclared ones included) positionally in declaration order or by name, and type-check each value against the parameter. The verdict is undecided, naming the fault, on a name no parameter has, more positional values than open parameters, a parameter left with neither an argument, a default nor a same-named value on the checked object (the existing fallback a constraint usage on a part relies on), or a value of the wrong type. A bare in parameter is required; one declared [0..1] may go unbound. The old CheckConstraintOn/CheckRequirementOn remain as the no-argument form.
• Service — VerifyConstraintRequest and VerifyRequirementRequest gain repeated Value arguments = 6 and map<string, Value> named_arguments = 7, advertised by the new verification_arguments capability. A request without bindings never needs the capability. Only the evaluate question takes bindings: holds and satisfiable with any argument are INVALID_ARGUMENT, since the solver decides the parameters' values there.
• CLI / REPL — -requirement 'P::R(limit = 5) P::t', -constraint 'P::C(3.0)', %requirement R(limit = 5) t, %constraint C(3.0, high = 9): the invocation grammar -analysis/%analysis already use. Usage text and manual pages updated.
• Clients — Go (VerifyArguments(...), VerifyArgument(name, v)), Python (arguments=, named_arguments=), Node (VerifyOptions.arguments/namedArguments), Java (VerifyOptions.withArguments/withNamedArguments), Rust (VerifyOptions { arguments, named_arguments, .. }), Julia (arguments=, named_arguments=), MATLAB (arguments, namedArguments). Each requires verification_arguments only when it binds something; the service's INVALID_ARGUMENT on a symbolic question with arguments surfaces through every client's usual status mapping.

The requirement path also fixes a package-level requirement def with an explicit subject not receiving the object a check supplies for it.

Specification basis

KerML 1.0 §7.4.9 / SysML v2 1.0 §7.18 (constraint and requirement definitions are predicates whose in parameters are bound at evaluation); no row of docs/project/spec-compliance.md moves — this widens the API over an already-implemented rule.

How it was verified

• internal/exec/runtime/check_args_test.go: named, positional and mixed bindings, defaults, [0..1] optionality, unknown name, arity, missing required, type mismatch, subject + arguments, requirement usage on a bound subject, and the existing TestUnboundParameterFallsBackToInstanceFeatureValue still passing.
• internal/frontend/grpc/verify_arguments_test.go and robustness_verify_arguments_test.go (TestGRPCRobustnessVerifyArguments): service paths, capability refusal, proof-question refusal.
• REPL (internal/frontend/repl/check_args_test.go) and CLI (cmd/sysml/check_test.go) argument grammar incl. malformed lists.
• Client suites: Go (client/opensysml), Python (tests/test_verification_arguments.py), Node (test/verify.test.ts), Java (ApiIntegrationTest), Julia (extended_client.jl), MATLAB live tests, Rust library tests.
• go build ./..., go vet ./..., gofmt -l . (empty), go test ./... all pass; make man-check, python3 scripts/changelog.py check, python3 scripts/check-doc-ids.py clean.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (CLI, REPL, wire contract, Go/Python/Julia/Rust API, client parity)
• Changelog entry added as changes/unreleased/verify-arguments.added.md
• baselines regenerated and make docs-counts run if a gate count moved — no gate count moved
• No internal work-item labels in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/4b750d3541e349aea211b5a469cfe882
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/4b750d3541e349aea211b5a469cfe882?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

[devin-ai-integration]

Recorded runtime testing of verification arguments on 645df3d (CLI, interactive REPL, Python over gRPC).

CLI, REPL, and Python/gRPC verification

• Named, positional, and mixed bindings return the expected true/false verdicts on all three surfaces.
• Unknown names, excess positionals, missing required inputs, and wrong types return undecided verdicts naming the fault; the error payloads match across CLI/REPL/gRPC.
• CLI statuses are 0/1/2 for true/false/error; a malformed argument list is refused with exit 2 and the REPL stays usable after one.
• Optional [0..1], defaulted, inherited/redeclared, and checked-object fallback inputs (constraint mass : MassLimit; reading the part's own m) behave as before.
• The service advertises verification_arguments and rejects bound holds/satisfiable questions with INVALID_ARGUMENT.
• Through a proxy without the capability, no-argument requests pass and bound calls raise MissingCapabilityError without reaching the service.

Interactive binding results	CLI status and error handling

Compatibility and diagnostic observations

Binaries built from the parent commit 83a7824 matched four no-argument default/fallback cases: CLI output and status were byte-identical, and Python verdict/error fields matched with bindings omitted or explicitly empty.

CLI/REPL decimal literals report Rational whereas a gRPC realValue reports Real in the type-mismatch message; both correctly refuse them for an Integer parameter. This is the pre-existing typing of literals on each surface, not a divergence in the binding path.

Not exercised: Connect over HTTP and the non-Python wrappers beyond their unit and integration suites.