Fix GNATprove child-package source resolution using base names

[Jbsco]

Summary

redo prove fails in any component directory whose source set includes autocoded child units (parent-child.ads). GNATprove (as of 15.1.0) rejects those units when they are passed as absolute paths, before analysis begins:

<unit> is not a file or compilation unit of any project

The cause is path resolution, not analysis. GNATprove resolves the same child units when they are passed as base names, and build_prove.py was passing absolute paths.

Fix

Pass the source arguments to GNATprove as base names. The directory of every source is already on -XSOURCE_DIRS, so base names resolve unambiguously. One line in redo/rules/build_prove.py.

Diagnosis and fix from @dinkelk (#194 review).

Validation

In the Adamant container, on a component containing a hand-written SPARK package alongside its autocoded child units. The before/after differ only in this one line; the built source set is identical.

• Before (absolute paths): admt prove in the component directory fails at component-<name>.ads is not a file or compilation unit of any project, before any analysis runs.
• After (base names): admt prove runs to completion and reproduces the package's full proof through the build system — 10 checks, 0 unproved, 0 justified (6 run-time, 1 assertion, 1 functional contract, 1 data dependency, 1 termination; 8 discharged by the provers, 2 by flow), at level: 2, mode: gold, with the summary beside the component under build/prove/gnatprove/gnatprove.out.
• Default-path regression: doc/example_architecture/spark_package (a top-level SPARK unit) builds and proves clean. Base names and absolute paths both resolve for non-child units, so the change is a no-op there.

Closes #192.

---

Prior approach (superseded) — packages: scoping in all.prove.yaml

Summary

redo prove analyzes every source buildable in a directory. In a component directory that includes the autocoded base classes, which GNATprove generally cannot analyze (child-package resolution failures against the framework), so a component that contains a hand-written SPARK package cannot be proven through the build system at all:

<unit> is not a file or compilation unit of any project
error: child package ... cannot be resolved

The current workaround is invoking gnatprove directly with a hand-built project file and -XSOURCE_DIRS, which bypasses the build system and scatters proof output under the GPR directory instead of the component. Agents and developers should not need to call the prover by hand any more than they call the compiler by hand.

Closes #192.

Fix

Model-driven scoping in the existing prove configuration. all.prove.yaml gains an optional packages: list (schema + model + rule):

---
description: GNATprove configuration for the component's step-allocation logic
level: 2
mode: "gold"
packages:
  - My_Component_Logic

When present, redo prove resolves each named package through the source database (case-insensitive) and passes exactly those sources to GNATprove, instead of everything in the directory. A name that resolves to no sources is a hard error naming the package and the yaml file. When absent, behavior is unchanged.

Validation

Run in the Adamant container against a project component containing a proved SPARK logic package alongside its autocoded sources (project details withheld; the shape is exactly the My_Component_Logic example above):

• Before: redo prove in the component directory fails with component-<name>.ads is not a file or compilation unit of any project.
• After, with the logic package listed under packages:: redo prove analyzes exactly the two logic-package files and reproduces the package's full proof (10 checks, 0 unproved, 0 justified: run-time checks, assertion, and functional contracts), with the summary written beside the component under build/prove/gnatprove/gnatprove.out.
• Unknown package name: clear failure (No source files found for package 'No_Such_Package' listed in .../all.prove.yaml), exit 1.
• Default path regression: redo prove on doc/example_architecture/spark_package (no packages: key) behaves exactly as before.

Context: this is the first shortcoming flagged under the "report Adamant SPARK tooling gaps" directive discussed in the skills review; it removes the direct-gnatprove workaround for component-directory proofs.

[dinkelk]

Thanks for the detailed writeup -- I was able to reproduce the reported failure on a project component directory and dug into the root cause. What I found changes the picture: the failure is a file-argument resolution bug in GNATprove itself, not an inability to analyze the autocoded base classes. With the root cause fixed, redo prove works on full component directories with zero configuration, so I'd like to hold off on the packages: mechanism.

Root cause

GNATprove 15.1.0 (the version pinned in alire.toml, GPR2-based) fails to resolve any child-package source file passed as an absolute path. Given the exact same project/externals, varying only the file argument:

File argument	Absolute path	Basename
component-<name>.ads/.adb (autocoded base class)	rejected	resolves
component-<name>-implementation.ads/.adb	rejected	resolves
<name>_events-representation.ads/.adb	rejected	resolves
<name>_events.ads/.adb, <name>_data_dependencies.*	resolves	resolves
Framework child units (sys_time-pretty.ads, ccsds_primary_header-representation.ads)	rejected	resolves
Framework top-level units (component.ads, configuration.ads)	resolves	resolves

The pattern is exact: every rejected file has a dash in its name (a child-package source); every top-level unit resolves either way. The rejection happens before any analysis starts, with the familiar <path> is not a file or compilation unit of any project. I ruled out symlinks, object dir location, and duplicate basenames.

Since build_prove.py passes absolute paths, and every component directory necessarily contains child-unit sources (component-<name>.ads, component-<name>-implementation.ads, *-representation.ads), redo prove always fails in component directories. Two side observations that fall out of this:

• doc/example_architecture/spark_package contains only top-level units, which is why the framework's own prove example never trips the bug.
• The filename named in the error varies run to run (whichever file lands first in the source-database ordering) -- I saw the error blame <name>_events-representation.ads in one run and component-<name>-implementation.adb in another.

Notably, the "autocoded base classes cannot be analyzed" premise doesn't hold up: passing all 10 sources of the component (base class included) as basenames, GNATprove runs the full pipeline and exits 0 -- 66 units loaded, everything without SPARK_Mode => On reported as skipped; SPARK_Mode => Off, nothing errors. The child package ... cannot be resolved errors don't reproduce once file resolution succeeds.

Suggested minimal fix

Basenames resolve through the same project source table (the directory of every closure file is already passed via -XSOURCE_DIRS, and GNAT naming guarantees one filename per unit), so the fix is one line in redo/rules/build_prove.py:

        + " -XSOURCE_DIRS="
        + ",".join(dep_dirs)
        + " "
        # GNATprove (as of 15.1.0) fails to resolve child-package sources, ie.
        # "parent-child.ads", when passed as absolute paths, reporting that
        # they are "not a file or compilation unit of any project". Passing
        # base names avoids this. The directory of every source file is
        # already included in SOURCE_DIRS above, so base names resolve
        # unambiguously.
        + " ".join([os.path.basename(f) for f in source_files])
        + direct

Validated in the Adamant container:

• Component directory (the failing scenario in this PR's summary): redo prove completes, exit 0, all component sources analyzed including the autocoded ones from build/src.
• Regression on doc/example_architecture/spark_package: identical proof results as before (2 run-time checks, 1 functional contract via Z3, flow/data dependencies, 0 unproved).

On the packages: mechanism

I'd prefer not to introduce a new mechanism into the .prove.yaml files right now. Beyond the maintenance surface, it only sidesteps the bug by accident: hand-written SPARK logic packages happen to be top-level units, so their sources have no dash in the filename. Listing a child package under packages: would hit the identical error, because the new code still passes absolute paths. With the basename fix, the motivating scenario (proving a component directory containing a SPARK logic package) works with no configuration at all.

Scoping analysis to specific packages may still be worth having someday as a performance/reporting feature, but it should be proposed on its own merits rather than as a workaround.

The underlying GNATprove behavior looks like a regression in the GPR2-based file-argument matching and is probably worth reporting to AdaCore separately.