adacovex 1.6.0

Date: 2026-08-05

Version bumped 1.5.0 -> 1.6.0.

Changes

C1: Full SPARK proof coverage (Platinum, 0 unproved)

The whole SPARK-on codebase is now fully machine-proved. Previously only the bounded IR types (Checked_Add32/64, IR_Bounds.Add32/64) carried complete proofs; every other SPARK unit was analysed but not fully discharged. Now all 491 VCs prove with --prover=z3 --timeout=20, including the run-time range checks, assertions, functional contracts, and loop termination:

  • Renderers: I2S (fixed 10**Pos overflow by replacing exponentiation with a constant Pow10 power table, loop invariants carrying the digit count and value bound, Buf initialized), Pad2 and Escape_JSON (uninitialized-buffer fixes via (others => ' ')), and ISO_From_Epoch (chained & concatenation upper-bound proofs replaced by a bounded Field-copy buffer procedure). Postconditions now document the result lengths (I2S'Result'Length in 1 .. 10, Pad2'Result'Length in 1 .. 11).

  • Parsers: Trim, Trim_Left, Number_After, and Number_Before_Word gained Pre => S'First >= 1 and S'Last < Natural'Last preconditions plus strengthened loop invariants (carried array-index bounds and the digit-run range for all Q in DStart .. K => S (Q) in '0' .. '9').

  • IR synthesiser: Bits, IR_Type_Name (Post => 'Result'Length <= 9), Lower_Type_Name, and Synthesize_Package (buffer bounds, Sub/Result initialization, and J >= I for the outer-loop variant) all proved.

  • Termination: every while loop across the codebase now carries an explicit Loop_Variant (increasing or decreasing bound), so the implicit Always_Terminates aspects discharge – no loop is left as potentially non-terminating.

The self-assessment is now: 26 packages, 59 subprograms, 100% docstrings, Platinum (500/500 VCs, 0 unproved), 295/295 tests, DAL-C Achieved.

C2: Host word-size auto-detection

Fixed-size buffers and the IR host model are now derived from the actual host word size instead of being hard-coded to 64-bit assumptions:

  • Adacovex.Types.Host_Word_Bits : constant := System.Word_Size; the Max_Path / Max_Line path and line buffers scale with it (64 * Host_Word_Bits = 4096, 4096 * Host_Word_Bits = 262144 on a 64-bit host), so builds on narrower hosts use proportionally smaller limits. The semantic limits (Max_Id_Str, Max_Desc_Str, Max_Filename) stay fixed.

  • Adacovex.Target_Profiles.Host_Word_Size auto-detects the host word size (8/16/32/64) from the Ada runtime for Target_Config.Host_Bits, with the dead-branch warning resolved by a case System.Word_Size structure.

  • Test suite extended: 6 new checks (Types conversion + IR host-word-size detection). The suite is now 295 tests.

C3: Conventional test-result file discovery

The test-summary lookup is no longer hard-coded to <target>/test_result.md. A new Parse_Test_Result_From_Project searches a conventional list of test-result file names at the project root (and under docs/) and parses the first file that exists – test_result.md, test_results.md, test-result.md, test_report.md, test_output.md, the equivalent .txt and .log variants, tests.md/tests.txt, and the docs/ mirrors. The assessment, sbom, and --compare-base paths all use the new lookup, so adacovex accepts common report conventions (e.g. CI that emits test_results.md or test-output.txt) without configuration.

The parser itself already understood Markdown tables, plain Passed:/Failed: summary lines, TAP, Automake, Maven Surefire, and Unity formats. The new candidate search adds one SPARK-proved helper (Trim_Right, fully discharged) and 9 new VCs, taking the self-assessment to 500/500 VCs Platinum.

Fixes

H2: Honest SBOM proof levels + badge contrast + install docs

  • SBOM proof levels: Only the root component – the project adacovex actually assessed – now carries adacovex:proof_level (Gold/Platinum) and adacovex:dal_target. Dependency components report adacovex:proof_level = "Not proved": adacovex only proves the target itself, never third-party dependencies, so they no longer claim a Gold/Platinum level they did not earn. Applied to CycloneDX, SPDX, and Markdown outputs; the Write_SBOM summary line now says “root proof level”.

  • Platinum badge contrast: the SPARK badge used white text on the light platinum background (#E5E4E2), which failed contrast. Added a Spark_Text_Color selector (#1a1a1a on Platinum/Gold/Silver, white on Bronze/Stone) and a Value_Text_Color parameter to Badge_SVG.

  • Installation docs: README now documents installing adacovex via alr install covex gnatprove (add Alire’s bin dir to $PATH), downloading the version-matched release bundle with curl from the GitHub Releases page (verifiable with gh attestation verify), or building from source. The prove-mode GNATprove toolchain resolution order (per-project manifest -> $PATH -> cached toolchain -> download) is documented, including the “install Alire first” fallback when a manifest declares gnatprove but alr is missing.

  • SBOM timestamp to git commit: documented how to tie the deterministic SOURCE_DATE_EPOCH timestamp to the exact commit (git -C <target> log -1 --format=%ct); the make targets already do this from HEAD.

H3: Back to zero-dependency – gnatprove moved out of alire.toml

  • alire.toml no longer declares gnatprove. The covex crate is once again fully zero-dependency: no library or tool dependencies. gnatprove lives only in alire-dev.toml (used by the local make targets), and the prove subcommand resolves it at run time via the dev-manifest swap, $PATH, ~/.adacovex/toolchain/, or a download. Installing covex no longer drags in gnatprove or the proof solvers.

  • Install docs prefer the per-project manifest. README/AGENTS now lead with declaring covex (plus gnatprove when proofs are wanted) in the project’s alire-dev.toml, keeping alr install covex gnatprove as the documented global alternative, alongside the GitHub release bundle and from-source installs.

  • Architecture decision: supported platforms. Since Alire is the packaging and delivery mechanism, adacovex supports the platforms Alire itself supports – binary distribution on Linux x86-64, Windows x86-64, and macOS x86-64, and building from source on any host with GNAT FSF 9.2+ that can build Alire. Added to docs/architecture.md.

  • Architecture decision: CI tied to release version. Documented that the GitHub Actions action is version-matched to the binary (the release workflow bundles adacovex-vX. Y. Z.tar.gz for each tag, and the action downloads the binary for the tag it is referenced by, with floating vMAJOR / vMAJOR. MINOR / latest tags force-pushed at release time).

CI runs on ubuntu-latest with the pinned gnat-version.

  • Release/index manifest templates (alire/releases/covex-0.0.0.toml, index/ad/covex/covex-0.1.0-dev.toml, and the 1.6.0 variants) dropped the gnatprove dependency; alire/alire.lock regenerated accordingly.

  • The toolchain-resolution and THIRD_PARTY_NOTICES wording now state plainly that adacovex declares no gnatprove dependency and resolves it at run time.

H4: Compiler/proof warning cleanup + gnatprove standard companion

  • Remaining build warnings fixed.

  • Adacovex. Renderers. SBOM: the compiler inlined Field and constant-folded its Sep /= ASCII. NUL guard, so the check reported “statement has no effect” at the call sites.

Kept the original single-loop form and wrapped it in pragma Warnings (Off/On, "statement has no effect"); the two-loop String alternative was tried and reverted because it cost 35 unproved VCs. Proof remains intact: 500/500 VCs, Platinum, 0 unproved. - Adacovex. Target_Profiles: Host_Word_Size is now a return-expression case (instead of an unreachable multi-branch case statement on the 64-bit archive host), eliminating the “statement is never reached” warnings at lines 10/13/16. - Forced rebuild: 0 warnings. make prove: Platinum, 500/500 VCs, 0 unproved, 0 justified. make test: 295/295.

  • gnatprove is now the standard companion in every covex TOML usage. README (Option 1) and AGENTS (install item 1, dev-manifest usage) declare covex = "*" with gnatprove = "^15.1.0" in the same manifest. The GitHub Actions action.yml no longer passes gnatprove to alr toolchain (gnatprove is not a toolchain component; that failed CI with “The requested crate is not a toolchain component”) – it selects only gnat_native and gprbuild, and the prove subcommand resolves gnatprove via the target project’s alire-dev.toml (README-preferred method), falling back to $PATH, the cached toolchain, or download. The “if you also want proof runs” phrasing was removed.

  • GitHub Actions attestation migrated to actions/attest. The release workflow now uses actions/attest@v4 with subject-path: adacovex-*.tar.gz (kept id: attest + attestation-url output); attest-build-provenance@v2 is gone. All prose references (README, AGENTS, docs/architecture.md, Makefile) updated.

  • Crate tags expanded to 11 across alire.toml, alire-dev.toml, the release templates, and the index templates: ada, spark, formal-verify, cli, gnatprove, sbom, tests, code-coverage, do-178c, compliance, developer-tools. (formal-verify is used because Alire caps tag strings at 15 characters.)

  • Remaining badge contrast fixed. The bright-green (#4c1) and yellow (#dfb317) badge values used white text. Added a Badge_Text_Color selector: dark #1a1a1a text on #4c1/#dfb317, white on the red #e05d44, matching the SPARK badge’s approach. tests.svg, do178c.svg, and docs.svg regenerate with dark value text; SVG tests still pass.

  • install.sh documents curl | bash and checks for Alire. README Option 3 now leads with the one-liner (curl -fsSL .../main/install.sh | bash), and the script warns when alr is missing from $PATH, pointing at curl https://alire.ada.dev -sSf | sh and the remaining gnatprove fallbacks ($PATH, cached toolchain, download).

  • “zero-library-dependency” -> “zero-dependency”. Renamed across README, AGENTS, and the alire.toml long-description (the published 1.0.0-1.5.0 release records keep their historical wording).

Test Suite

Test suite extended: IR synthesis 26 -> 27 checks plus six new word-size checks (Types conversion + IR host-word-size detection); the suite is now 295 tests (passing).

Proof Results

Self-assessment: Platinum (500/500 VCs proved, 0 unproved, AoRTE-free). Every SPARK-on unit is fully discharged – run-time checks 358/358, assertions 60/60, functional contracts 13/13, termination 44/44, flow 69/69. Proof invocation: gnatprove -P adacovex.gpr --prover=z3 --timeout=20.

Traceability

No new HLRs. Existing tags continue to cover the changed packages: -- HLR-SCAN on Adacovex. Parsers. Source, -- HLR-TEST on `Adacovex.

Parsers. Tests, – HLR-PROVE/– HLR-METRICSonAdacovex. Types, – HLR-IRonAdacovex. Target_ProfilesandAdacovex.

IR_Synthesiser, – HLR-SBOMonAdacovex. Renderers. SBOM`. The HLR-SBOM wording was tightened to reflect that only the root component carries proof-aware properties while dependencies are reported as “Not proved”.