# Adacovex.Prove_Patch

Proof patches for vendored dependencies.

The docstring patch system (Adacovex.Parsers.Source.Apply_Patches)
overlays documentation onto vendored .ads files.  This package extends
the same ``.adacovex/patches/<relative-path>`` layout with SPARK proof
support.  A patch file can carry SPARK aspects.  The aspects are
SPARK_Mode on the package declaration and Pre, Post, or SPARK_Mode on
subprogram declarations.  The ``prove`` subcommand merges them into a copy
of the vendored spec.  When the patch carries one, it also merges the
vendored body.  GNATprove then analyses the vendored unit with the
patched contracts.  It does not modify the original vendored sources.
A .ads patch re-declares the spec with contracts.  A .adb patch opts
the body into the proof.  The body is analysed only when it declares
SPARK_Mode On itself.

The merge is textual and line-based.  The patched source is the original
with each patched subprogram declaration replaced by the patch's
declaration block.  The block carries the aspects.  A declaration
matches on name and normalised parameter profile.  An overload patches
its exact signature, never a same-named sibling.  The default ``in`` mode
is equivalent to a bare mode.  ``in out`` and ``out`` are distinct.  The
package declaration is given the patch's package-level aspect when
present.  Subprogram declarations terminate at the ';' of a spec
declaration or at the ``is`` of a body declaration.  A patched body
declaration is replaced without touching the body proper.

When the vendored body is SPARK-clean and opted in via a body patch,
GNATprove proves the patched contracts.  When it is not, for example
Ada.Text_IO callers, GNATprove skips the I/O bodies by design.  The
unit is then reported as out of proof scope.  A proof patch never drags
the target's proof level down.
HLR-PROVE: GNATprove runner and proof patches

> **Note:** All items in this package are public.

## Functions

### function Count_Proof_Patches (Target_Dir : Standard.String) return Standard.Natural

| Parameter | Description |
|-----------|-------------|
| `Target_Dir` | Target project root. |

**Returns:** Number of proof-carrying patch files.

### function Has_Proof (Text : Standard.String) return Standard.Boolean

| Parameter | Description |
|-----------|-------------|
| `Text` | Patch file contents. |

**Returns:** True when the patch carries proof aspects.

### function Patches_Hash (Target_Dir : Standard.String) return Standard.String

| Parameter | Description |
|-----------|-------------|
| `Target_Dir` | Target project root. |

**Returns:** Hex digest of all patch file contents ("" when none).

## Procedures

### procedure Apply (Original : Standard.String; Patch : Standard.String; Merged : Standard.String; Merged_Len : Standard.Natural; OK : Standard.Boolean)

| Parameter | Description |
|-----------|-------------|
| `Merged` | Buffer receiving the patched source. |
| `Merged_Len` | Length of the patched source (0 on failure). |
| `OK` | True when the merge succeeded. |
| `Original` | Original vendored source text. |
| `Patch` | Patch text (valid Ada .ads with docstrings and/or |

### procedure Build_Patched_Copy (Target_Dir : Standard.String; Root_GPR : Standard.String; Copy_Dir : Standard.String; Copy_Len : Standard.Natural; Copy_GPR : Standard.String; GPR_Len : Standard.Natural; Success : Standard.Boolean)

| Parameter | Description |
|-----------|-------------|
| `Copy_Dir` | Directory of the patched proof tree. |
| `Copy_GPR` | Absolute path of the copy's root project file. |
| `Copy_Len` | Length of Copy_Dir. |
| `GPR_Len` | Length of Copy_GPR. |
| `Root_GPR` | Absolute path of the root project file. |
| `Success` | True when the tree was built (a merge failure |
| `Target_Dir` | Target project root. |