adacovex 1.15.0

Date: 2026-08-18 Version bumped 1.14.0 -> 1.15.0.

Changes

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.