Low-Level Requirements – adacovex

LLR Mapping

  • LLR-ARCH-01: alire.toml shall declare project metadata [HLR-ARCH]

  • LLR-ARCH-02: justfile (with the Makefile shim) shall provide build, prove, fmt, doc, changelog, and clean tasks [HLR-ARCH]

  • LLR-ARCH-03: adacovex.gpr shall compile all sources with -gnatwa warnings [HLR-ARCH]

  • LLR-ARCH-04: Adacovex.Paths shall answer Is_Separator, Is_Absolute, Join, Strip_Trailing_Separators, Home_Directory, and Expand_User for both path styles, so no other unit spells a platform path assumption inline [HLR-ARCH]

  • LLR-CACHE-01: cache entry paths shall map every : in a key to -, so a namespaced key is a legal file name on Windows [HLR-CACHE]

  • LLR-PROVE-01: the prove runner shall resolve the gnatprove binary under the host executable name (gnatprove.exe on Windows), because Ada.Directories never guesses an extension [HLR-PROVE]

  • LLR-SCAN-01: Scan_Project shall walk directories recursively, skipping .git and obj [HLR-SCAN]

  • LLR-SCAN-02: Scan_Ads_File shall extract procedure, function, and generic declarations [HLR-SCAN]

  • LLR-SCAN-03: Scan_Ads_File shall detect – HLR-XXXX tags in source [HLR-SCAN]

  • LLR-SCAN-04: Scan_Ads_File shall detect @param, @return, @field, @formal docstring tags [HLR-SCAN]

  • LLR-PROOF-01: Parse_Prove_Out shall parse gnatprove.out and extract VC counts per check type [HLR-PROOF]

  • LLR-PROOF-02: Determine_SPARK_Level shall assign level based on proved/unproved ratios [HLR-PROOF]

  • LLR-TEST-01: Parse_Test_Result shall parse Markdown test results for pass/fail counts [HLR-TEST]

  • LLR-TEST-02: Parse_Test_Stdout shall parse raw test runner stdout for pass/fail counts [HLR-TEST]

  • LLR-DAL-01: Assess_DAL_C shall check all HLRs are traced in source [HLR-COMPLIANCE] [HLR-DAL-C]

  • LLR-DAL-02: Assess_DAL_C shall detect orphan tags not matching any HLR [HLR-COMPLIANCE] [HLR-DAL-C]

  • LLR-DAL-03: Assess_DAL_C shall verify test results show zero failures [HLR-COMPLIANCE] [HLR-DAL-C]

  • LLR-DAL-04: Assess_DAL_C shall check SPARK level >= Bronze [HLR-COMPLIANCE] [HLR-DAL-C]

  • LLR-DAL-05: Assess_DAL_A shall require SPARK Gold + tests passing + all HLRs + no orphans [HLR-DAL-A]

  • LLR-DAL-06: Assess_DAL_B shall require SPARK Silver + tests passing + all HLRs + no orphans [HLR-DAL-B]

  • LLR-DAL-07: Assess_DAL_D shall require tests passing + all HLRs [HLR-DAL-D]

  • LLR-DAL-08: Assess_DAL_E shall require all HLRs [HLR-DAL-E]

  • LLR-RENDER-ANSI-01: Render_Summary shall output colour-highlighted terminal report [HLR-RENDER-ANSI]

  • LLR-RENDER-SVG-01: Render_SPARK_Badge shall produce valid SVG with level colour [HLR-RENDER-SVG]

  • LLR-RENDER-SVG-02: Render_Tests_Badge shall show passed/failed in green/red [HLR-RENDER-SVG]

  • LLR-RENDER-SVG-03: Render_DO178C_Badge shall show Achieved/Unmet in green/red [HLR-RENDER-SVG]

  • LLR-RENDER-MD-01: Generate_Verification_Report shall write coverage, proof, test, compliance tables [HLR-RENDER-MD]

  • LLR-RENDER-MD-02: Generate_Trace_Matrix shall map each package to its HLR tags [HLR-RENDER-MD]

  • LLR-RENDER-HTML-01: Render_Dashboard shall produce self-contained HTML with embedded CSS [HLR-RENDER-HTML]

  • LLR-RENDER-HTML-02: Render_Metrics_JSON shall produce JSON with key metrics [HLR-RENDER-HTML]

  • LLR-SERVER-01: Start shall bind to port and serve dashboard at /, API at /api/metrics, badges at /badge/*.svg [HLR-SERVER]

  • LLR-TLDR-01: Detect shall classify the installed tldr client from tldr --show-paths and tldr --version, and shall report no client when the binary is absent [HLR-TLDR]

  • LLR-TLDR-02: Install shall write the bundled page to the tealdeer custom pages directory, or to a base client’s common and platform cache pages, and Installed shall compare the page byte for byte [HLR-TLDR]

  • LLR-CLI-01: Parse_CLI shall parse –target, –dal, –serve, –port, –emit-svg, –emit-markdown [HLR-CLI]

  • LLR-CLI-02: Parse_CLI shall default target to the current working directory and DAL to C [HLR-CLI]