wrpc-binding false-positives: correctly bus-bound cross-processor connection (applies to <conn>) still warns

[avrabe]

wrpc-binding false-positives: a correctly bus-bound cross-processor connection still warns

Using spar to architect a multi-core wasm-component flight stack (the wRPC direction): a cross-processor port connection that is bound to a bus via Actual_Connection_Binding => (reference (bus)) applies to <conn> still triggers the wrpc-binding warning "crosses processor boundary … but has no Actual_Connection_Binding to a bus."

Repro (spar v0.17.0)

A system impl with two processes bound to different processors and a connection between them, bound to a bus:

  connections
    est_to_falcon : port estimator.state_out -> falcon.state_in;
  properties
    Actual_Processor_Binding => (reference (m4)) applies to estimator;
    Actual_Processor_Binding => (reference (m7)) applies to falcon;
    Actual_Connection_Binding => (reference (shmem)) applies to est_to_falcon;

spar analyze still emits:

[WARNING] wrpc-binding: connection 'est_to_falcon' ... crosses processor boundary ... but has no Actual_Connection_Binding to a bus

Tried both Actual_Connection_Binding => ... and Deployment_Properties::Actual_Connection_Binding => ...; both warn. Full model: pulseengine/jess hardware/pixhawk6x-rt.aadl.

Root cause (from crates/spar-analysis/src/wrpc_binding.rs)

The check reads the owning component's flat property map:

let has_conn_binding = owner_props.get("Deployment_Properties", "Actual_Connection_Binding").is_some()
    || owner_props.get("", "Actual_Connection_Binding").is_some();

A per-connection applies to <conn> binding apparently isn't surfaced under those keys on the owner, so has_conn_binding is always false for the standard idiom. Net: the analysis can't be satisfied by a correct deployment — it warns on every cross-processor connection regardless of binding.

Suggested fix

Resolve the binding on the connection instance (honor applies to <conn>), i.e. check connection.property("Actual_Connection_Binding") (or the owner's applies to-qualified associations keyed by connection) rather than only the owner's flat map. Bonus: verify it points to an actual bus (the doc intent), not just presence.

Impact for jess: this is the analysis we want to lean on to validate the wRPC topology (cross-core connections must name a transport). Right now it's a guaranteed false-positive, so it can't gate. Happy to test a fix against the jess model.

Filed from jess Phase-2 (Pixhawk 6X-RT) wRPC architecture.