Verified jq -> SQL translation, kernel-checked in Lean 4.
10K+
durwasa/querybridge — image contents referenceDetailed catalogue of what is inside the QueryBridge Docker image.
Generated for the local build of querybridge:latest produced by the
project's Dockerfile (multi-stage: frontend → Lean → slim Python
runtime). The same contents apply to the multi-arch images pushed to
Docker Hub at durwasa/querybridge:{latest,v0.1.0}.
| Field | Value |
|---|---|
| Total size on disk | ~1.48 GB (uncompressed) |
| Compressed size on Hub | ~400–500 MB (estimate; depends on layer dedup) |
| Base | python:3.12-slim |
| Linked C runtime | libgcc-s1, libstdc++6 (apt-installed for the Lean exes) |
| Working directory | /app/backend |
| Entrypoint / CMD | uvicorn main:app --host 0.0.0.0 --port 8000 |
| Exposed port | 8000 (HTTP — serves both the API and the static SPA) |
| Architectures | linux/amd64, linux/arm64 |
| Size | Layer |
|---|---|
| 156 MB | COPY .../bin/propRunner |
| 155 MB | COPY .../bin/proofTrace |
| 155 MB | COPY .../bin/sqlGenMain |
| 155 MB | COPY .../bin/sqlGenError |
| 155 MB | COPY .../bin/sqlGenBug2 |
| 155 MB | COPY .../bin/sqlGenBug3 |
| 55 MB | pip install -r requirements.txt (FastAPI + uvicorn + anthropic + …) |
| 45 MB | Python 3.12 build (from python:3.12-slim base) |
| 209 KB | Pre-built Vite bundle (/app/frontend/dist) |
| 168 KB | Lean source (*.lean) |
| 74 KB | Backend Python source |
| 16 KB | proof_trace.json snapshot |
The six 155 MB Lean exes dominate. Each is a statically-linked Lean
binary that includes the elaborated Main.olean (or Error.olean) plus
the Lean stdlib it references. They are independent — no shared library
deduplication possible across them with the current Lake build setup.
/app
├── backend/ Python source (74 KB)
│ ├── main.py FastAPI routes
│ ├── translator.py jq → SQL (mirror of the Lean proof)
│ ├── executor.py run_jq + run_sql on the seed DB
│ ├── lean_client.py spawns sqlGenMain
│ ├── llm_client.py nl_to_jq via Anthropic SDK or mock
│ ├── proof_witness.py builds per-query proof witness
│ ├── counterexample_runner.py spawns propRunner / serves cached proofTrace
│ ├── seed_data.py 7 hardcoded users
│ └── requirements.txt
│
├── ProofPilot/
│ ├── *.lean All Lean source files (~170 KB total)
│ │ — proof_witness.py reads Main.lean
│ ├── proof_trace.json Pre-computed proofTrace output (16 KB)
│ │ — served by /api/proofs (no lake at runtime)
│ └── .lake/build/bin/
│ ├── sqlGenMain (~155 MB) /api/query — verified per-query path
│ ├── sqlGenError (~155 MB) legacy: bug-seeded variant of Main
│ ├── sqlGenBug2 (~155 MB) legacy: bug-seeded variant
│ ├── sqlGenBug3 (~155 MB) legacy: bug-seeded variant
│ ├── propRunner (~156 MB) /api/properties — Plausible.Testable.checkIO
│ └── proofTrace (~155 MB) proof inspector — present but unused at
│ runtime in the slim image (no lake on PATH);
│ its output is pre-cached as proof_trace.json
│
└── frontend/dist/ Pre-built React/Vite SPA bundle (209 KB)
├── index.html
└── assets/index-*.{js,css}
All six binaries are produced in stage 2 of the Dockerfile by:
RUN lake build sqlGenMain sqlGenError sqlGenBug2 sqlGenBug3 propRunner proofTrace
Each binary statically links the Lean stdlib + the Lean module it has as
its root (per ProofPilot/lakefile.toml).
| Binary | Source root | Role |
|---|---|---|
sqlGenMain | SqlGenMain.lean | Per-query verified path — parses jq, applies the proven jquery_to_squery from Main.lean, evaluates both sides on seedDB, returns kernel_match. Drives /api/query's proof witness. |
propRunner | PropRunner.lean | Calls Plausible.Testable.checkIO on each property in Properties.lean. Drives /api/properties. |
proofTrace | ProofTrace.lean | Calls Lean.importModules + Meta.ppExpr + Lean.collectAxioms on theorems in Main.lean. Output is captured at build time and served as proof_trace.json (slim runtime has no lake env). |
sqlGenError | SqlGenError.lean | Variant of sqlGenMain that uses Error.lean's buggy eval_jquery. Legacy demo. |
sqlGenBug2 | SqlGenBug2.lean | Variant using Bug2.lean. Legacy demo. |
sqlGenBug3 | SqlGenBug3.lean | Variant using Bug3.lean. Legacy demo. |
| Path | Method | Driven by | Notes |
|---|---|---|---|
/ | GET | static FastAPI mount | Serves frontend/dist/index.html |
/assets/* | GET | static FastAPI mount | SPA bundle |
/health | GET | main:health | {"ok": true} |
/api/data | GET | main:get_data | Returns the 7-user seed DB |
/api/query | POST | main:run_query → sqlGenMain subprocess | Per-query verified flow + proof_witness block |
/api/properties | GET | main:properties → propRunner subprocess | 4 Plausible runs against Error.lean |
/api/proofs | GET | main:proofs → cached proof_trace.json | 7 kernel-verified theorems from Main.lean |
Per the cached proof_trace.json, every theorem in the runtime image is
kernel-verified (no sorryAx in the transitive dependencies). The
headline query_equiv rests on:
propextQuot.soundClassical.choice— the three Lean foundational axioms, and nothing else. The transitive
axiom set per theorem is exposed verbatim in /api/proofs.
git clone https://github.com/durwasa-chakraborty/QueryBridge
cd QueryBridge
docker build -t querybridge .
For the multi-arch push that produces what's on Docker Hub:
docker buildx create --name querybridge --use --bootstrap # one-time
docker login
docker buildx build \
--platform linux/amd64,linux/arm64 \
--tag durwasa/querybridge:latest \
--tag durwasa/querybridge:v0.1.0 \
--push .
The non-host architecture builds Mathlib from source under QEMU emulation
(the prebuilt lake exe cache get artefacts are amd64-only), so the
multi-arch build can take 30–60 minutes the first time. Subsequent builds
hit the BuildKit layer cache.
Content type
Image
Digest
sha256:72a2bed32…
Size
315 MB
Last updated
5 months ago
docker pull durwasa/querybridge