# adacovex 1.15.0

Date: _2026-08-18_
Version bumped 1.14.0 -> 1.15.0.

## Changes

### C1: docs cross-linking audit and generator-owned API-doc links

The docs were audited for misplaced and missing cross-links. The README's
compliance bullet now leads with the general standards page instead of the
DO-178C-only DAL page, and its ISO 26262 / IEC 62304 links point at the
dedicated ASIL / Class level pages; the "Compliance levels" section links
all three per-level pages. `docs/target-projects.md`'s HLR-format reference
now points at the docstring spec's HLR-tags section instead of the DAL
criteria page, and the plain-text doc references in CONTRIBUTING.md,
llm-usage.md, installation.md, platforms.md, and standards.md became real
links (dashboard.md and sbom.md gained standards links too, and llm-usage.md
carried a stale 653/653 test count, now corrected to 666/666).

The six hand-written reference pages (docstring spec, test formats, SPARK
levels, DAL/ASIL/Class levels) gained reciprocal "See also" sections. The
generated api-docs cross-links live in `tools/rst2md.py` so they survive
`make doc` regeneration: `GUIDE_PAGES` adds a "Guides" section to the API
index, and `PACKAGE_GUIDES` renders a "See also" line on 13 package pages
(parsers, compliance, types, prove, cache, diff, vcs, cpus, renderers,
server) pointing at their reference pages -- gnatdoc drops markdown link
URLs from `.ads` comments, so the links cannot live in source docstrings.
AGENTS.md's Documentation block (via `tools/doc-links.map`) and the
developer-guide now document the pattern.

### C2: badges sized per-glyph instead of a flat 7px-per-character estimate

Every SVG badge sized its label and value segments as `chars * 7 + 10`
pixels and centered the text, so the visible side padding was whatever the
flat estimate left over. Uppercase-heavy text (SPARK, DO-178C, ISO 26262,
IEC 62304) renders wider than 7px per glyph at the badge font's 11px size
and came out nearly flush against the segment edge, while narrow
lowercase/digit text (docs, 100%, Platinum) came in well under the estimate
and carried visibly extra padding.

`Badge_SVG` now measures each segment as the sum of per-glyph advance
widths -- a DejaVu Sans metric table at 11px, rounded to the pixel, with a
7px fallback for unknown characters -- plus a fixed 20px total padding, so
every badge carries the same 10px side padding regardless of its letters:
the Platinum value segment is 66px (46px text + 20) and the DAL-C PASS
segment 82px (62 + 20), the docs label 46px (26 + 20) and the 100% value
50px (30 + 20). Segments that were flush before (SPARK, ISO 26262,
IEC 62304) now carry the same generous 10px margin as the rest. The
dashboard and server-served badges (`/badge/*.svg`) use the same renderer,
so they pick up the fix automatically; the six `docs/badges/*.svg` files
are regenerated by `make prove` / `make run-self`.

### C3: SPARK_Mode On expansion across pure computation helpers

GNATprove analysed only a handful of explicitly-annotated subprograms; most
pure helpers were plain and so carried no proof obligations. `SPARK_Mode =>
On` (with Pre/Post contracts) was added where the computation is pure and
the types are SPARK-clean, expanding the proved surface from 408 to 433
VCs with zero unproved:

* `renderers-svg`: the per-glyph helpers `Glyph_Width` / `Text_Width`, the
  palette functions `Badge_Text_Color` / `Spark_Color` / `Spark_Text_Color`
  (the latter two were already On), and the integer-to-string `I2S` all
  prove; the string-assembly (`Badge_SVG` and the `Render_*` badges) stays
  plain -- concat-chain bounds blow the solver budget, matching the
  existing `renderers-sbom` convention, and the `Render_Tests_Badge` /
  `Render_Compliance_Badge` / `Render_DO178C_Badge` functions take types
  from the non-SPARK `Types.Implementation` container package, so they
  cannot be analysed.
* `compliance-dal`: `Min_SPARK_For` and `Need_Tests` -- the two pure
  helpers at the heart of the DAL assessment -- are now On with contracts
  pinning their result ranges (`Need_Tests` <= 3, `Min_SPARK_For` maps
  every DAL level into `Stone`..`Platinum`). `Is_DAL_Achieved` takes a
  `DAL_Assessment` from `Types.Implementation` and stays plain.
* `cpus`: `Default_Prove_Jobs` is On with a Post pinning the CI /
  non-CI branch arithmetic (`Natural'Max (1, Cores - 2)`).
* `parsers-gnatprove`: `Determine_SPARK_Level` -- the exact same rules the
  proof-status sync tool implements in Python -- is On with a Post
  pinning its result to `Stone`..`Platinum`.

Units that are I/O- or container-heavy (`main`, `server-http`, `cache`,
`vcs`, `parsers-source`, `parsers-manifest`) keep their default-off bodies,
matching the project's existing SPARK discipline: subprograms that touch
`Types.Implementation` (the non-formal `Ada.Containers` types SPARK forbids
analysing) or do file/process I/O carry no `SPARK_Mode` aspect rather than
an explicit Off pragma.

### C4: SVG renderer tests assert badge pixel geometry

The SVG tests previously asserted only badge content -- SVG markup, labels,
and values -- so a regression in the C2 per-glyph sizing (a wrong advance
width, a lost padding term, a mis-centered label) could ship a visually
broken badge with every test still green. The renderer tests now pin the
actual pixel geometry of every badge.

`adacovex_renderer_svg_tests.adb` gained two helpers: `Nth_Attr` extracts
the numeric value of the Nth `attr="..."` occurrence from the generated
markup (its leading-space needle keeps `x="` from matching inside the
clip-path corner radius `rx="3"`), and `Check_Geometry` asserts the six
numbers that fully determine a badge -- total width, label and value
segment widths, the value segment's x offset (it must start exactly where
the label segment ends), and the two centered text positions. All twelve
badge renderings now lock their geometry, e.g. SPARK Platinum 121px
(55 + 66) with text centers at 27/88, Tests 738 Passed 130px (48 + 82),
docs 100% 96px (46 + 50), DO-178C 149px (67 + 82), ISO 26262 160px
(76 + 84), and IEC 62304 164px (75 + 89) -- the exact values the C2
per-glyph table and 20px padding contract produce, and the same geometry
`make run-self` emits into `docs/badges/*.svg` (the regenerated tests.svg
shows "738 Passed" at the same 130px width, since the tabular digits are
all 7px). The suite grows from 666 to 738 checks (SVG renderer category
36 to 108).

### C5: SPARK_Mode On expansion across the CLI validation and VCS label helpers

Building on C3, `SPARK_Mode => On` was added to five more pure helpers --
the ones with SPARK-clean types whose contracts are full characterizations
of the result:

* `config`: `Has_Prefix`, `Is_Help_Topic`, and `Is_Valid_DAL` -- the CLI
  argument parser's pure validation helpers -- are On with Postconditions
  that exactly characterize their results (a quantified prefix match for
  `Has_Prefix`, a leading-dash-or-alphabetic scan for `Is_Help_Topic`, a
  single A-E/a-e character test for `Is_Valid_DAL`).
* `vcs`: `To_String` and `Tool_Name` -- the VCS display/tool-name label
  helpers used by `adacovex status` and the differential modes -- are On
  with Posts pinning their result to the exact six-value repertoire
  (`"git"`, `"mercurial"`, `"subversion"`, `"fossil"`, `"jj"`, `""`).

The one C5 helper left plain -- `config.Is_All` -- was finished in C6
below. This expansion adds 38 provable checks (433 to 471 VCs) with zero
unproved; the analysed-unit count stays 45 because the new On subprograms
live in units already analysed.

### C6: Is_All proved, and the server badge endpoints pinned

Two additions on top of C5: the `config.Is_All` proof was finished, and
the `/badge/*.svg` server surface gained direct geometry coverage.

**`config.Is_All` is now `SPARK_Mode => On`.** The C5 attempt to
characterize it with a quantified Post over the uppercased buffer blew the
prover's step budget in every formulation tried (per-character
equivalence, a True-implies-length-3 shape). The resolution is structural:
the upper-cased-buffer comparison `Up = "ALL"` is exactly equivalent to
three case-insensitive character tests -- `S'Length = 3`, the first
character in `'a' | 'A'`, and the next two in `'l' | 'L'` -- so the
function body and postcondition now state that characterization directly
(no buffer, no quantifier). The Post fully characterizes the result and
proves cleanly, adding 13 provable checks (471 to 484 VCs) with zero
unproved; the analysed-unit count stays 45 since `config` was already
analysed.

**Server badge endpoints covered by geometry tests.** The five
`/badge/*.svg` routes in `adacovex-server-http.adb` serve
`Render_SPARK_Badge (Proof.Level)`, `Render_Tests_Badge (Tests)`, and
`Render_Compliance_Badge (Assess, DO_178C / ISO_26262 / IEC_62304)` for
`spark`, `tests`, `do178c`, `iso26262`, and `iec62304` respectively. The
C4 geometry tests already pinned the spark / tests / ISO 26262 / IEC
62304 render calls and the `Render_DO178C_Badge` wrapper, but
`/badge/do178c.svg` is served through the standard-parameterized
`Render_Compliance_Badge (Assess, DO_178C)` -- a call the suite did not
exercise. The SVG tests now carry a "Server badge endpoints" section that
names each route and pins its exact server-side render call: every
endpoint asserts content plus the full six-number geometry, including
`/badge/do178c.svg` in both Achieved ("DAL-C PASS", 67/82/149) and Unmet
("DAL-C FAIL", 67/76/143) states through the exact server call, and
`/badge/tests.svg` at the self-assessment count (791 Passed, 48/82/130)
-- the same geometry `make run-self` emits into `docs/badges/tests.svg`.

## Fixes

### H1: release changelog list now newest-first instead of glob order

The `Create GitHub Release` step in `.github/workflows/release.yml` iterated
`docs/changelogs/adacovex-*.md` with a shell glob, so the release body's
**Changelogs** list came out in lexicographic file-name order -- `0.1.0`,
`1.0.0`, `1.1.0`, `1.10.0`..`1.14.0`, then `1.3.0`..`1.9.0` -- instead of
newest-first. The step now collects the in-range versions and pipes them
through `sort -V -r`, so the list reads `1.14.0` down to `1.10.0` (and down
to `0.1.0` when no previous release tag is found). The `make release` target
prints the same list in the same order, and `docs/ci-cd.md` documents the
newest-first contract.

### H2: bump deprecated Node-20 actions to Node-24 runtimes

GitHub deprecated the Node.js 20 runtime on Actions runners: actions that
target Node 20 are now forced to run on Node 24, and every such step emits
a deprecation warning. The composite action's `actions/cache` restore/save
steps (`@v4`, Node 20) and `actions/upload-artifact` steps (`@v4`, Node 20)
are bumped to `@v5` and `@v7` respectively, which run on the Node 24
runtime (minimum Actions Runner 2.327.1). `actions/checkout@v7` and
`actions/attest@v4` already run on Node 24 and are unchanged. All action
inputs and outputs are unchanged, and consumers of the action (e.g.
Ada_CRDT via `bladeacer/adacovex@v1`) pick up the fix with the next
release.

## Test Suite

791 tests (was 738), across 12 categories: the C4 geometry tests add 72
checks to the SVG renderer category (36 to 108), and the C6 server badge
endpoint tests add 53 more (108 to 161) -- the only test changes. The
changelog-listing and action-version fixes (H1/H2) are
release-workflow, Makefile, and composite-action shell/YAML code; the docs
change is documentation plus `tools/rst2md.py` Python tooling (covered by
`make doc` and `make link-check`); and the SPARK expansions (C3/C5/C6) add
aspects and contracts without changing behaviour. The regenerated
`docs/badges/*.svg` geometry is verified by `make run-self`, by the proof
run emitting the six badges, and now also directly by the C4/C6 unit tests.

## Proof Results

Platinum, 484/484 VCs proved across 45 analysed units (up from 408 at
1.14.0): the C3 `SPARK_Mode => On` expansion added 25 provable checks
(408 to 433) across the renderers-svg helpers, the compliance-dal helpers
(`Min_SPARK_For`, `Need_Tests`), `cpus.Default_Prove_Jobs`, and
`parsers-gnatprove.Determine_SPARK_Level`; the C5 expansion added 38 more
(433 to 471) across the config validation helpers (`Has_Prefix`,
`Is_Help_Topic`, `Is_Valid_DAL`) and the VCS label helpers (`To_String`,
`Tool_Name`); and the C6 `Is_All` completion added 13 more (471 to 484)
-- all pure computation with SPARK-clean types. 0 unproved, 0 justified;
the non-SPARK bodies keep gnatprove analysing only the On subprograms,
exactly as before. Proven with `make prove` under gnatprove 16.1.0
(`--steps=10000`).

## Traceability

No new HLRs. The badge geometry tests (C4) and the server badge endpoint tests (C6) extend the coverage of the existing `HLR-RENDER-SVG` tag (`src/renderers/adacovex-renderers-svg.ads`/`.adb` and `src/tests/adacovex_renderer_svg_tests.adb`); the C6 endpoint tests also pin the badge surface of `LLR-SERVER-01` (`HLR-SERVER`), whose routes are served through the same render calls. The SPARK expansions are covered by the existing `HLR-COMPLIANCE` / `HLR-DAL-*` tags (`compliance-dal`), `HLR-CPU` (`cpus`), `HLR-PROOF` (`parsers-gnatprove`), `HLR-CLI` (`config`, including the completed `Is_All` proof), and `HLR-DIFF` (`vcs`) -- the contracts extend the subprograms these tags already trace. The two fixes (H1/H2) live in release-workflow shell code, the `make release` target, the composite action, and docs; the docs change touches documentation and `tools/rst2md.py` / `tools/doc-links.map`.

None of these carry HLR traceability tags.