0%

AIMS Interprocedural Evidence Boundary

Routed Finding

Hygiene design route: hr-88ba353fb0897ec5

  • Rule: DESIGN-04 (depend on the narrowest boundary, not another module’s internals).
  • Severity: Major.
  • Evidence: aims::verify::oracle::evidence imports build_subject_independent_alias_to_param_map, find_borrowed_cow_consumed_params, find_iter_consume_call_args, and CowConsumeScope through the interprocedural extraction module. Verification therefore knows extraction algorithms and control vocabulary instead of consuming a stable evidence result owned by interprocedural analysis.
  • Why this is not DESIGN-17: the primary violation is the oracle’s direct knowledge of a sibling module’s implementation surface; shared change pressure is a consequence, not the defining smell.
  • No within-budget cure: narrowing a visibility modifier would only hide the dependency. The producer/consumer contract, evidence identity, extraction ownership, verification inputs, and malformed/stale evidence behavior must be redesigned together.

Goal

Restore one-way AIMS flow: interprocedural analysis produces an immutable, validated evidence product; the verification oracle checks that product without rerunning or reaching into extraction algorithms.

Required Design

  1. Introduce the narrowest evidence type that captures alias-to-parameter facts, borrowed-COW consumption, iterator consumption, provenance, and exact function/artifact identity required by verification.
  2. Keep extraction helpers and scope-control enums private to their producing module.
  3. Make the interprocedural owner construct and validate the evidence once, then pass it explicitly into oracle verification.
  4. Bind evidence to the exact ArcFunction, contract set, interner/registry provenance, and executable-program fingerprint so stale or cross-function replay fails closed.
  5. Delete oracle imports of extraction helpers and reject any verification path that reconstructs producer facts independently.

Verification

  • Compile-time visibility tests keep extraction implementation types private.
  • Positive tests show produced evidence yields the same accepted AIMS results as the current path.
  • Negative tests reject missing facts, extra facts, duplicate sites, stale fingerprints, cross-function replay, and mismatched contracts.
  • Source structure and graph checks prove the dependency direction is producer evidence to verifier only.

Closeout

This section closes only after its owned criterion is satisfied, code-side TPR is clean, and a source-fingerprint-current canonical test-all run is full green.

Work Items

  • Replace oracle access to extraction internals with one narrow interprocedural evidence contract