Slice 3: provable CI for the type-checker + render the Zig FFI (provably-real + honest) by hyperpolymath · Pull Request #23 · hyperpolymath/typedqliser

hyperpolymath · 2026-06-18T13:00:29Z

Propagates the chapeliser "provably-real + honest" pattern to typedqliser (the #1 -iser priority). Each layer below was checked, not eyeballed.

Provable — `.github/workflows/provable.yml`

golden-check (the headline, verified locally): the SQL type-checker accepts valid SQL and rejects invalid SQL. Using the blog-api example — a valid query exits 0; a syntax error (L1) and a nonexistent column (L2) each exit non-zero; the full example reports 1 passed, 1 failed. (check --ci's exit code is correct — I confirmed it; an earlier "exit 0" of mine was a | head pipe masking $?.)
zig-ffi: zig build test of the C-ABI FFI (Zig 0.14, SHA-pinned setup-zig@v1.2.2).

Made the Zig FFI real

It shipped as an unrendered RSR template — build.zig/main.zig literally contained {{project}}/{{PROJECT}} (would never build):

Rendered the placeholders → typedqliser across build.zig, src/main.zig, test/integration_test.zig.
build.zig: dropped lib.version (a versioned .so panics in Zig 0.14's InstallArtifact) and added linkLibC() (main.zig uses std.heap.c_allocator) — the same two fixes proven on chapeliser.

Honest docs

The README sold an "Idris2 Type Kernel (src/abi/) … the core of TypedQLiser" with proof terms and dependent types — but there are zero .idr files and src/abi/ is 54 lines of Rust. Reworded:

The 10 levels are proof obligations enforced in Rust today (src/codegen + plugins); the Idris2 kernel is specified but not yet implemented.
Fixed the Zig FFI path (ffi/zig → src/interface/ffi) and the Status paragraph.

Notes

Rust layer unchanged: 116 tests pass; Cargo.lock updated to resolve a pre-existing glob lock gap.
Toolchains: the dev sandbox's network policy blocks every Zig mirror (ziglang.org + 6 community mirrors all 403), so the Zig job is CI-gated; the type-checker golden is locally verified. (idris2 isn't needed here — no .idr.)

Draft until the two Provable jobs are green; I'll drive them.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

Generated by Claude Code

Slice 3 — propagate the chapeliser "provably-real + honest" pattern to typedqliser (the #1 -iser priority). Provable — add .github/workflows/provable.yml: - golden-check: the SQL type-checker ACCEPTS valid queries and REJECTS invalid ones (blog-api example; verified locally — good pass, bad fail at L1/L2/L3). The headline value, machine-checked. - zig-ffi: `zig build test` the C-ABI FFI (Zig 0.14, SHA-pinned action). Make the Zig FFI real — it shipped as an UNRENDERED RSR template: - render {{project}}/{{PROJECT}} -> typedqliser across build.zig, src/main.zig, test/integration_test.zig. - build.zig: drop `lib.version` (versioned .so panics in Zig 0.14's InstallArtifact) and add linkLibC() (main.zig uses std.heap.c_allocator) — the same fixes proven on chapeliser. Honest docs — the README sold an "Idris2 type kernel" as "the core", but there are zero .idr files (src/abi/ is 54 lines of Rust): - reframe the level model as proof OBLIGATIONS enforced in Rust today, with the Idris2 kernel specified-but-unimplemented. - fix the Zig FFI path and the Status paragraph. Rust layer unchanged (116 tests). The golden type-checker is verified locally; the Zig build is CI-gated (no zig mirror reachable in the sandbox). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T13:01:22Z

🔍 Hypatia Security Scan

Findings: 61 issues detected

Severity	Count
🔴 Critical	1
🟠 High	11
🟡 Medium	49

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

- build.zig: drop the addInstallHeader block — the method was removed in Zig 0.14 ("no member 'addInstallHeader' in 'Build'") and the referenced include/typedqliser.h does not exist. `zig build test` only needs main.zig. - main.zig / integration_test.zig: move SPDX-License-Identifier to line 1 (Hypatia SD009) and drop the references to a non-existent src/abi/Foreign.idr / "Idris2 ABI" — there are no .idr files. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T13:04:42Z

🔍 Hypatia Security Scan

Findings: 60 issues detected

Severity	Count
🔴 Critical	1
🟠 High	11
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…ot have fields) The RSR template declared Handle as `opaque` but gave it fields, which Zig rejects ("opaque types cannot have fields"). Make it a struct; C still only sees `*Handle` as an opaque pointer. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T13:07:24Z

🔍 Hypatia Security Scan

Findings: 60 issues detected

Severity	Count
🔴 Critical	1
🟠 High	11
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

`zig build` (now runnable locally) emits these under src/interface/ffi/; they are build outputs, not source. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T13:14:51Z

🔍 Hypatia Security Scan

Findings: 60 issues detected

Severity	Count
🔴 Critical	1
🟠 High	11
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-advanced-security AI found potential problems Jun 18, 2026

View reviewed changes

Comment thread src/interface/ffi/src/main.zig Fixed

hyperpolymath marked this pull request as ready for review June 18, 2026 13:15

hyperpolymath merged commit 340c8fa into main Jun 18, 2026
25 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Slice 3: provable CI for the type-checker + render the Zig FFI (provably-real + honest)#23

Slice 3: provable CI for the type-checker + render the Zig FFI (provably-real + honest)#23
hyperpolymath merged 4 commits into
mainfrom
claude/sharp-cannon-038nwu

hyperpolymath commented Jun 18, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hyperpolymath commented Jun 18, 2026

Provable — .github/workflows/provable.yml

Made the Zig FFI real

Honest docs

Notes

Uh oh!

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Provable — `.github/workflows/provable.yml`