Login

u/Gairmonster

r/ada
Ada bindings for Dear ImGui, stb, and ccv (MIT, on Alire)
▲ 19 r/ada

Ada bindings for Dear ImGui, stb, and ccv (MIT, on Alire)

Fellow Ada people,

Three new Ada bindings, MIT-licensed, now on Alire and GitHub:

  • ada_imgui — Dear ImGui immediate-mode GUI, via cimgui
  • ada_stb — Sean Barrett's stb single-header libraries (image load/write, etc.)
  • ada_ccv — Liu Liu's ccv C computer-vision library (image I/O + processing)

alr get ada_imgui (likewise ada_stb, ada_ccv). Source: github.com/the-dark-factory

These are initial releases — the wrapped surface is partial, focused on the common entry points over the raw C ABI. Issues and PRs welcome, especially on platform coverage and thicker idiomatic wrappers.

any more suggestions let me know

Tony

u/Gairmonster — 13 days ago
▲ 14 r/ada

Verifier kit for 15 Fortran→SPARK conversions (Netlib BLAS / LAPACK / FFTPACK + inference kernels)

Posting in case useful — we've been converting Fortran reference implementations to SPARK-Ada and publishing the artefacts at thedarkfactory.co.uk/results/. Each routine ships with the original Fortran, the emitted spec, the emitted body, and the filtered gnatprove output. A new verifier kit packages the .ads/.adb pairs plus build.gpr plus a Makefile so anyone with gnatprove can re-run our discharge calculation.

Routines:

  • BLAS L1/L2/L3: ddot, daxpy, dscal, dnrm2, dgemv, dgemm
  • LAPACK: dpotrf (Cholesky), dgeqrf (QR / Householder), dgetrf (LU / partial pivoting)
  • FFTPACK: cfftf (forward complex FFT)
  • FP64 inference kernels: relu, max_pool, layernorm, conv2d
  • INT8 matmul

All gnatmake-clean under --level=1. Discharge ranges 82.4–96.0% on individual routines; aggregate is 90.1% across the eleven Netlib routines under strong postconditions (quantified Post over outputs — a stub body cannot discharge trivially). dgeqrf, dpotrf, dgetrf also have tier-3 behavioural-equivalence runtime checks against known inputs.

Transparency note. These specs and bodies are emitted from the Fortran reference inputs by an automated pipeline that uses an advanced language model behind a verifier loop. The pipeline isn't published; the output is. The verifier kit is how you confirm what we claim.

The verifier kit: thedarkfactory.co.uk/results/verify/ (28 KB tarball). Two commands:

tar xzf dark-factory-verifier.tar.gz && make all

Output goes to actual-results.txt; diff against expected-results.txt. Should match line for line.

The dgeqrf erratum, for honest context. Our first dgeqrf row was 98.7%. An audit found the emitted body was a sophisticated stub — ghost helpers returned constants, the Post quantified over branches that ignored A and Tau. A fixed body skeleton (LAPACK Householder convention pinned) plus a tier-3 runtime check on Tau ≠ 0 and A modified brought the rerun to 87.5%. Lower number, real body, runtime-verified. The catch is documented at /blog/2026-05-24-old-code-new-code.html. The verifier kit ships the corrected body.

The unproved residue. Most lives in three classes: float-overflow checks at theoretical FP extremes, the unaxiomatised Exp in Ada.Numerics.Generic_Elementary_Functions (closeable by pragma Assume after each call), and recursive ghost induction at --level=1 (closeable at --level=2). None are body-correctness failures. The README documents per-class.

If you find a bug in one of the .ads/.adb files, I'd really like to know. Email tony.gair@thedarkfactory.co.uk or reply here. The publication contract works only if the rerun matches; if yours doesn't, we should hear about it.

If anyone has a better pattern for handling SPARK_Mode => Off on Ada.Numerics, I'd appreciate the pointer. That's where most of the unproved residue sits.

reddit.com
u/Gairmonster — 16 days ago