hyperpolymath · hyperpolymath · Apr 2, 2026
@@ -0,0 +1,116 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+name: GitHub Pages
+
+on:
+  push:
+    branches: [main, master]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+
+      - name: Checkout casket-ssg
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+        with:
+          repository: hyperpolymath/casket-ssg
+          path: .casket-ssg
+
+      - name: Setup GHCup
+        uses: haskell-actions/setup@ec49483bfc012387b227434aba94f59a6ecd0900 # v2
+        with:
+          ghc-version: '9.8.2'
+          cabal-version: '3.10'
+
+      - name: Cache Cabal
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            .casket-ssg/dist-newstyle
+          key: ${{ runner.os }}-casket-${{ hashFiles('.casket-ssg/casket-ssg.cabal') }}
+
+      - name: Build casket-ssg
+        working-directory: .casket-ssg
+        run: cabal build
+
+      - name: Prepare site source
+        shell: bash
+        run: |
+          set -euo pipefail
+          rm -rf .site-src _site
+
+          if [ -d site ]; then
+            cp -R site .site-src
+          else
+            mkdir -p .site-src
+            TODAY="$(date +%Y-%m-%d)"
+            REPO_NAME="${{ github.event.repository.name }}"
+            REPO_URL="https://github.com/${{ github.repository }}"
+            README_URL=""
+
+            if [ -f README.md ]; then
+              README_URL="${REPO_URL}/blob/${{ github.ref_name }}/README.md"
+            elif [ -f README.adoc ]; then
+              README_URL="${REPO_URL}/blob/${{ github.ref_name }}/README.adoc"
+            fi
+
+            {
+              echo "---"
+              echo "title: ${REPO_NAME}"
+              echo "date: ${TODAY}"
+              echo "---"
+              echo
+              echo "# ${REPO_NAME}"
+              echo
+              echo "Static documentation site for ${REPO_NAME}."
+              echo
+              echo "- Source repository: [${{ github.repository }}](${REPO_URL})"
+              if [ -n "${README_URL}" ]; then
+                echo "- README: [project README](${README_URL})"
+              fi
+              if [ -d docs ]; then
+                echo "- Docs directory: [docs/](${REPO_URL}/tree/${{ github.ref_name }}/docs)"
+              fi
+              echo
+              echo "Project-specific site content can be added later under site/."
+            } > .site-src/index.md
+          fi
+
+      - name: Build site
+        run: |
+          mkdir -p _site
+          cd .casket-ssg && cabal run casket-ssg -- build ../.site-src ../_site
+          touch ../_site/.nojekyll
+
+      - name: Setup Pages
+        uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b # v5
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3
+        with:
+          path: '_site'
+
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4
@@ -34,7 +34,7 @@ axis-3 = "systems > compliance > effects"
 [scoping]
 sources = "README, roadmap, status docs, maintenance checklist, CI/security docs"
 marker-scan = "TODO/FIXME/XXX/HACK/STUB/PARTIAL"
-idris-unsound-scan = "believe_me/assert_total"
+idris-unsound-scan = "unsound-idris-escape-scan"
 
 [axis-2-maintenance-rules]
 corrective-first = true

@@ -1,64 +1,55 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# STATE.a2ml — Project state checkpoint (META-TEMPLATE)
-#
-# This is the STATE file for rsr-template-repo itself.
-# When consumed by a new project, replace {{PLACEHOLDER}} tokens
-# and customize sections below for the target project.
+# STATE.a2ml — Project state checkpoint
 
 [metadata]
-project = "rsr-template-repo"
-version = "0.2.0"
-last-updated = "2026-02-28"
-status = "active"  # active | paused | archived
+project = "vql-ut"
+version = "0.1.0"
+last-updated = "2026-03-30"
+status = "active"
 
 [project-context]
-name = "rsr-template-repo"
-purpose = "Canonical RSR-compliant repository template providing scaffolding for all hyperpolymath projects — including CI/CD, AI manifests, ABI/FFI standards, container ecosystem, and governance infrastructure."
-completion-percentage = 95
+name = "vql-ut"
+purpose = "Experimental research repo for a proposed type-safe query layer for VeriSimDB, with current Rust formatter/linter surfaces and draft Idris2/Zig/ReScript implementation work."
+completion-percentage = 25
 
 [position]
-phase = "maintenance"      # design | implementation | testing | maintenance | archived
-maturity = "production"    # experimental | alpha | beta | production | lts
+phase = "audit-remediation"
+maturity = "experimental"
 
 [route-to-mvp]
 milestones = [
-  { name = "Phase 0: Core scaffolding (justfile, CI/CD, .machine_readable)", completion = 100 },
-  { name = "Phase 1: ABI/FFI standard (Idris2/Zig templates)", completion = 100 },
-  { name = "Phase 1b: AI Gatekeeper Protocol (0-AI-MANIFEST.a2ml)", completion = 100 },
-  { name = "Phase 1c: TOPOLOGY.md standard and guide", completion = 100 },
-  { name = "Phase 1d: Maintenance gate (axes, checklist, approach)", completion = 100 },
-  { name = "Phase 1e: Trustfile / contractiles", completion = 100 },
-  { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 },
-  { name = "Phase 3: Multi-forge sync hardening", completion = 0 },
-  { name = "Phase 4: Nix/Guix reproducible shells", completion = 50 },
+  { name = "Claim-envelope containment", completion = 70 },
+  { name = "Formatter/linter test surface", completion = 80 },
+  { name = "Draft Idris2 core and ABI encoding", completion = 40 },
+  { name = "End-to-end query pipeline", completion = 10 },
+  { name = "Audited stable release gate", completion = 0 },
 ]
 
 [blockers-and-issues]
-# No active blockers
+issues = [
+  "Public docs and manuscript still outrun implemented and checked evidence in places",
+  "Template residue remains in task runner, container, and support surfaces",
+  "No end-to-end verified query pipeline or proof-certificate output exists yet",
+  "Stable release audit still fails",
+]
 
 [critical-next-actions]
 actions = [
-  "Container templates complete — test with `just container-init`",
-  "Validate container templates across wolfi-base and static Chainguard images",
-  "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases",
-  "Expand Nix/Guix development shell templates",
+  "Keep public claims aligned with the current checked artifact",
+  "Remove remaining template residue from task runner and container surfaces",
+  "Split test surfaces cleanly into point-to-point, e2e, aspect, and benchmark smoke paths",
+  "Advance Idris2 draft modules toward a checked core before making stronger proof claims",
 ]
 
 [maintenance-status]
 last-run-utc = "never"
 last-report = "docs/reports/maintenance/latest.json"
-last-result = "unknown"  # unknown | pass | warn | fail
-open-warnings = 0
-open-failures = 0
+last-result = "fail"
+open-warnings = 3
+open-failures = 1
 
 [ecosystem]
-part-of = ["RSR Framework", "stapeln ecosystem"]
-depends-on = ["stapeln", "selur-compose", "cerro-torre", "svalinn", "vordr", "k9-svc"]
-
-# ---------------------------------------------------------------------------
-# NOTE FOR CONSUMERS: When using this template to create a new repo, reset
-# the fields above to your project's values and replace all {{PLACEHOLDER}}
-# tokens. The milestones above describe the TEMPLATE's evolution, not yours.
-# ---------------------------------------------------------------------------
+part-of = ["TypeLL lineage", "VeriSimDB ecosystem"]
+depends-on = ["typell", "panll", "verisimdb"]
@@ -1,6 +1,6 @@
 {
   "title": "VQL-UT: Progressive Type Safety for Database Query Languages",
-  "description": "Database query bugs form a total order by severity. VQL-UT formalises this as progressive levels of type-level query safety, each strictly subsuming all prior levels. Levels 1-6 (established) cover parse-time to result-type safety. Levels 7-10 (research) cover aliasing, effects, lifetimes, and linearity via QTT. Formalised in Idris 2 with zero runtime overhead through proof erasure.",
+  "description": "Database query bugs can be organised as progressive levels of query safety. VQL-UT is currently a design-stage proposal and research prototype for expressing that safety envelope for VeriSimDB-style queries. The repository contains Rust formatter/linter tooling plus draft Idris2 encodings and architecture notes; it does not yet provide a fully mechanised 10-level implementation or end-to-end zero-overhead proof pipeline.",
   "upload_type": "publication",
   "publication_type": "preprint",
   "creators": [{"name": "Jewell, Jonathan D.A.", "affiliation": "The Open University"}],

@@ -7,9 +7,13 @@
 
 ## WHAT IS THIS?
 
-This is the AI manifest for **vql-ut** (VQL Ultimate Type-Safe) — the 10-level
-type-safe query language for VeriSimDB. It supersedes VQL-DT (dependent types
-only) as THE formally verified query path.
+This is the AI manifest for **vql-ut** (VQL Ultimate Type-Safe), an experimental
+research repo for a proposed type-safe query layer for VeriSimDB.
+
+Do **not** describe this repository as a completed formally verified query path,
+as a production-ready system, or as a replacement for VQL-DT. The current repo
+contains surface tooling and draft proof-oriented components, not a finished
+end-to-end verified compiler.
 
 ## NAMING
 
@@ -40,10 +44,10 @@ TypeLL (type theory core)
 | Path | Purpose | Type Safety |
 |------|---------|-------------|
 | VQL (Slipstream) | Standard routine queries, fast | None (runtime only) |
-| VQL-DT | PROOF clauses (6 proof types) | Dependent types via Lean |
-| VQL-UT | All 10 levels, research → production | Full formal verification via Idris2 |
+| VQL-DT | PROOF clauses (6 proof types) | Existing proof-oriented path |
+| VQL-UT | Proposed 10-level successor path | Experimental repo: formatter/linter tests plus draft Idris2/Zig/ReScript work |
 
-If VQL-UT succeeds, it replaces VQL-DT entirely.
+If VQL-UT matures and earns it, it may eventually supersede VQL-DT. It has not done so yet.
 
 ### Adoption Path
 
@@ -82,11 +86,29 @@ These a2ml files MUST exist in `.machine_readable/` directory ONLY:
 2. **No `assert_total`** — All functions provably total via `%default total`.
 3. **No `assert_smaller`** — Termination proved structurally.
 4. **No SCM duplication** — `.machine_readable/` is authoritative.
-5. **Idris2 over Ephapax** — When proven Idris2 code conflicts with Ephapax
+5. **Evidence boundary honesty** — Do not claim end-to-end verification,
+   proof certificates, or production readiness unless the checked artifact
+   actually supports it.
+6. **Idris2 over Ephapax** — When proven Idris2 code conflicts with Ephapax
    linear types, always choose Idris2. Dependability first.
-6. **License** — PMPL-1.0-or-later throughout.
-7. **Author** — Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-8. **Container images** — Chainguard base, Podman, Containerfile.
+7. **License** — PMPL-1.0-or-later throughout.
+8. **Author** — Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+9. **Container images** — Chainguard base, Podman, Containerfile.
+
+## CURRENT EVIDENCE BOUNDARY
+
+Checked surfaces today:
+
+- Rust formatter/linter crates and integration tests
+- Draft Idris2 modules for the core safety model and ABI/FFI types
+- Early Zig/ReScript scaffolding
+
+Not yet claimable from this repo alone:
+
+- full 10-level enforcement at compile time
+- machine-checkable proof certificates for end-to-end execution
+- production readiness
+- replacement of VQL-DT in live VeriSimDB deployments
 
 ## THE 10 LEVELS OF TYPE SAFETY
 
@@ -146,7 +168,7 @@ defaults to empty and MUST be configured per-workspace.
 ## SESSION STARTUP CHECKLIST
 
 ✅ Read THIS file (0-AI-MANIFEST.a2ml) first
-✅ Understand: VQL-UT supersedes VQL-DT
-✅ Understand: 10 levels from TypeLL → PanLL → VQL-UT
+✅ Understand: VQL-UT is experimental and does not yet supersede VQL-DT
+✅ Understand: 10 levels from TypeLL → PanLL → VQL-UT are the intended design basis
 ✅ NEVER use vql++/vqlpp naming
 ✅ Canonical location: `.machine_readable/`