Skip to content

Commit 280dcb5

Browse files
ci: make CI genuinely green — rust-ci toolchain pin + canonical Julia ABI-FFI gate + fmt/clippy (#40)
* P3: prove TypeCompat (level 3) as a real operand-type-compatibility guarantee Continues the flagship semantic-proof coverage (InjectionFree level 5, SchemaBound level 2) with TypeCompat (level 3: "operand types compatible"). Adds `Typedqliser.ABI.TypeCompat`, to the same quality bar: * a small SQL type universe (`SqlType`) and a typed column environment (`ColEnv`) with a total `lookupType` resolver, reusing the existing `Query`/`Pred`/`Value` AST; * `ValueCompat`/`PredTypeCompat`/`QueryTypeCompat` — the proposition that every WHERE comparison compares a column against a value of a matching type (a bound parameter adopts the column's type; a literal is TInt; a raw splice is TText). There is no constructor for a type clash, so a mismatched comparison is uninhabited; * `decQueryTypeCompat` — a sound + complete `Dec`, so a "Proven" TypeCompat certificate is backed by a constructive witness and a type clash can never be certified; * `certifyTypeCompatSound` (a `Proven` verdict provably entails the property); `typeCompatIsLevelThree : levelNat TypeCompat = 3`; * positive control (a well-typed query, with the certifier computing to `Proven`) and negative control (`name : Text` compared to an integer literal provably cannot be certified). Verified with idris2 0.7.0: `idris2 --build typedqliser-abi.ipkg` exits 0 with zero warnings (all 7 modules). Adversarially checked — three deliberately-false proofs (wrong level ordinal, a TInt literal certified against a TText column, and a type-compatible witness for the clash query) are all rejected by the type checker. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 NullSafe (level 4) theorem with guard discovery Adds Typedqliser.ABI.Invariants, a second, deeper, distinct machine-checked property over the existing Semantics query model (Query/Pred/Value reused verbatim). Where the Layer-2 flagship (Semantics.InjectionFree, level 5) is a purely structural property, NullSafe (level 4) is context-sensitive: a projected nullable column is safe only if the WHERE predicate guards it, with guards discovered by union under And and intersection under Or (disjunctive weakening). Includes a sound + complete decision procedure (decQueryNullSafe : Dec ...), a certifier proven sound (certifyNullSafeSound), the level-ordinal identity plus a proof it differs from InjectionFree, three positive controls and three non-vacuity controls (unguarded projection, And/union, Or/intersection). Builds clean with zero warnings; the deliberately-false adversarial proof is rejected. No believe_me/postulate/assert_total/%hint; %default total throughout. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * Add Layer-4 ABI<->FFI seam proof (Typedqliser.ABI.FfiSeam) Prove the FFI result-code encoding is SOUND: the C integer the Zig FFI returns faithfully round-trips back to the ABI value, and distinct ABI outcomes never collide on the wire. - intToResult / intToStatus: total decoders (if x == n over boolean Bits32 ==, which reduces on concrete literals). - resultRoundTrip / statusRoundTrip: lossless encoding, proved by Refl. - resultToIntInjective / statusToIntInjective: injectivity DERIVED from the round-trip via a local justInj + cong. - Positive controls (decodeOk/decodeNullPointer/decodeUnknown/decodeProven) and machine-checked non-vacuity controls (okNotError, schemaNotNull, provenNotRefuted) refuting collisions of distinct codes. Genuine total proof: no believe_me / postulate / assert_total / sorry. Builds clean with zero warnings; a false seam claim is rejected by --check. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi(capstone): Layer-5 end-to-end ABI soundness certificate Assemble the existing per-layer proofs into one inhabited record `ABISound` and a single value `abiContractDischarged` built from the already-exported witnesses: - Layer-2 flagship: safeQueryInjectionFree (InjectionFree, level 5) - Layer-2 companions: boundQuerySchemaBound (SchemaBound, level 2), goodQueryTypeCompat (TypeCompat, level 3) - Layer-3 invariant: guardedQueryNullSafe (NullSafe, level 4) - Layer-4 FFI seam: resultToIntInjective The capstone proves no new domain theorem; its content is that the whole chain holds simultaneously — if any prior layer were unsound the value would not typecheck. Adversarial control: a false certificate (deriving Ok = Error through the seam) is rejected by the typechecker. %default total, SPDX MPL-2.0, zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * ci: make CI green — bump rust-ci to standards@8dc2bf0 (toolchain: stable fix); port ABI-FFI gate Python->Bash (Python is estate-banned) Resolves the standing baseline CI reds (rust-ci toolchain error, governance Language/anti-pattern, governance workflow-lint) without altering the proven ABI. The Bash gate reproduces the former Python gate's verdict verbatim (validated across all -iser repos) and catches the same drift classes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port * style: cargo fmt + clippy --fix to satisfy rust-ci (fmt --check + clippy -D warnings) * style: cargo fmt + clippy --fix under stable 1.96 (CI toolchain) — fmt --check + clippy -D warnings clean --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 579d759 commit 280dcb5

8 files changed

Lines changed: 151 additions & 128 deletions

File tree

.github/workflows/abi-ffi-gate.yml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,15 @@ jobs:
2121
runs-on: ubuntu-latest
2222
steps:
2323
- uses: actions/checkout@v4
24+
- name: Install Julia 1.11.5
25+
run: |
26+
curl -fsSL https://julialang-s3.julialang.org/bin/linux/x64/1.11/julia-1.11.5-linux-x86_64.tar.gz -o /tmp/julia.tar.gz
27+
tar -xf /tmp/julia.tar.gz -C /tmp
28+
echo "/tmp/julia-1.11.5/bin" >> "$GITHUB_PATH"
2429
- name: Run ABI-FFI gate
25-
run: python3 scripts/abi-ffi-gate.py
30+
run: |
31+
julia --version # confirms the pinned 1.11.5 is on PATH, not the runner default
32+
julia scripts/abi-ffi-gate.jl
2633
2734
zig-build:
2835
name: Zig FFI builds + tests (Zig 0.14.0)

.github/workflows/rust-ci.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,4 @@ permissions:
1414

1515
jobs:
1616
rust-ci:
17-
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
17+
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@8dc2bf039d1ff0372d650895c46bea7fbaec68ff

benches/typedqliser_bench.rs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
//! - `schema_check` and `type_check` overhead per query size.
99
//! - Plugin creation cost.
1010
11-
use criterion::{black_box, criterion_group, criterion_main, BenchmarkId, Criterion, Throughput};
11+
use criterion::{BenchmarkId, Criterion, Throughput, black_box, criterion_group, criterion_main};
1212
use typedqliser::plugins::{ColumnDef, Schema, TableDef, get_plugin};
1313

1414
// ---------------------------------------------------------------------------
@@ -19,17 +19,15 @@ use typedqliser::plugins::{ColumnDef, Schema, TableDef, get_plugin};
1919
const SMALL_QUERY: &str = "SELECT id FROM accounts WHERE id = 1";
2020

2121
/// Medium query (~180 bytes) — a two-table JOIN with a WHERE clause.
22-
const MEDIUM_QUERY: &str =
23-
"SELECT accounts.id, accounts.username, transactions.amount \
22+
const MEDIUM_QUERY: &str = "SELECT accounts.id, accounts.username, transactions.amount \
2423
FROM accounts \
2524
INNER JOIN transactions ON accounts.id = transactions.account_id \
2625
WHERE accounts.id > 10 AND transactions.amount > 0 \
2726
ORDER BY transactions.amount DESC \
2827
LIMIT 50";
2928

3029
/// Large query (~400 bytes) — a CTE + subquery + GROUP BY.
31-
const LARGE_QUERY: &str =
32-
"WITH high_value AS ( \
30+
const LARGE_QUERY: &str = "WITH high_value AS ( \
3331
SELECT account_id, SUM(amount) AS total \
3432
FROM transactions \
3533
WHERE amount > 100 \

scripts/abi-ffi-gate.jl

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
#!/usr/bin/env julia
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
#
5+
# abi-ffi-gate.jl — fail (exit 1) if the Zig FFI does not conform to the Idris2
6+
# ABI. The Idris2 ABI is the source of truth. Checks, with no compile toolchain
7+
# needed (pure base-Julia text analysis):
8+
#
9+
# 1. the Zig FFI carries no unrendered `{{...}}` template tokens;
10+
# 2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
11+
# sources is exported by the Zig FFI (`export fn <name>`);
12+
# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
13+
# names and integer values (the `Error`/`err` spelling is treated as one).
14+
#
15+
# Usage: julia scripts/abi-ffi-gate.jl [repo_root] (defaults to cwd)
16+
#
17+
# Julia port of the former scripts/abi-ffi-gate.py (Python is banned estate-wide,
18+
# RSR-H4); behaviour is identical.
19+
20+
"camelCase / PascalCase → snake_case (insert `_` before each non-initial capital)."
21+
camel_to_snake(s) = lowercase(replace(s, r"(?<!^)(?=[A-Z])" => "_"))
22+
23+
"Canonical result-code key: lowercased, with `err`/`error` unified to `error`."
24+
function canon_rc(name)
25+
n = lowercase(name)
26+
(n == "err" || n == "error") ? "error" : n
27+
end
28+
29+
"Return {variant => value} for the C-ABI `Result` enum (the `enum(c_int)` block whose `ok = 0`), or empty."
30+
function find_result_enum(zig::AbstractString)
31+
best = Dict{String,Int}()
32+
for m in eachmatch(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}"s, zig)
33+
body = m.captures[1]
34+
variants = Dict{String,Int}()
35+
for vm in eachmatch(r"@?\"?([A-Za-z_][A-Za-z0-9_]*)\"?\s*=\s*(\d+)", body)
36+
variants[canon_rc(vm.captures[1])] = parse(Int, vm.captures[2])
37+
end
38+
# The Result enum is the one starting at ok = 0.
39+
if get(variants, "ok", nothing) == 0 && length(variants) > length(best)
40+
best = variants
41+
end
42+
end
43+
return best
44+
end
45+
46+
"Collect every `*.idr` under `abi_dir`, skipping any `build/` output directory."
47+
function idr_sources(abi_dir::AbstractString)
48+
files = String[]
49+
isdir(abi_dir) || return files
50+
for (root, _dirs, fs) in walkdir(abi_dir)
51+
occursin("/build/", root * "/") && continue
52+
for f in fs
53+
endswith(f, ".idr") && push!(files, joinpath(root, f))
54+
end
55+
end
56+
return files
57+
end
58+
59+
function main(root::AbstractString)::Int
60+
name = basename(rstrip(abspath(root), '/'))
61+
abi_dir = joinpath(root, "src/interface/abi")
62+
zig_path = joinpath(root, "src/interface/ffi/src/main.zig")
63+
errs = String[]
64+
65+
idr_files = idr_sources(abi_dir)
66+
if isempty(idr_files)
67+
println("ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir")
68+
return 0
69+
end
70+
if !isfile(zig_path)
71+
println("ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path")
72+
return 1
73+
end
74+
75+
idr = join((read(p, String) for p in idr_files), "\n")
76+
zig = read(zig_path, String)
77+
78+
# 1. unrendered template tokens
79+
toks = sort(unique(String(m.match) for m in eachmatch(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
80+
isempty(toks) || push!(errs, "Zig FFI has unrendered template tokens: $(toks)")
81+
82+
# 2. foreign C symbols must be exported
83+
csyms = sort(unique(String(m.captures[1]) for m in eachmatch(r"C:([A-Za-z0-9_]+)", idr)))
84+
exports = Set(String(m.captures[1]) for m in eachmatch(r"export fn ([A-Za-z0-9_]+)", zig))
85+
missing_syms = [s for s in csyms if !(s in exports)]
86+
isempty(missing_syms) ||
87+
push!(errs, "$(length(missing_syms)) ABI function(s) not exported by the Zig FFI: $(missing_syms)")
88+
89+
# 3. result-code map (names + values) must agree
90+
idr_rc = Dict{String,Int}()
91+
for m in eachmatch(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr)
92+
idr_rc[canon_rc(camel_to_snake(m.captures[1]))] = parse(Int, m.captures[2])
93+
end
94+
zig_rc = find_result_enum(zig)
95+
if !isempty(idr_rc) && isempty(zig_rc)
96+
push!(errs, "no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
97+
elseif !isempty(idr_rc) && !isempty(zig_rc) && idr_rc != zig_rc
98+
push!(errs, "Result-code map differs (name or value):\n" *
99+
" Idris resultToInt: $(sort(collect(idr_rc)))\n" *
100+
" Zig Result enum: $(sort(collect(zig_rc)))")
101+
end
102+
103+
if !isempty(errs)
104+
println("ABI-FFI GATE: FAIL ($name)")
105+
for e in errs
106+
println(" - " * e)
107+
end
108+
return 1
109+
end
110+
println("ABI-FFI GATE: OK ($name) — $(length(csyms)) ABI functions exported, " *
111+
"$(length(idr_rc)) result codes match")
112+
return 0
113+
end
114+
115+
root = length(ARGS) >= 1 ? ARGS[1] : "."
116+
exit(main(root))

scripts/abi-ffi-gate.py

Lines changed: 0 additions & 103 deletions
This file was deleted.

src/plugins/sql.rs

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -205,18 +205,17 @@ impl SqlPlugin {
205205
| BinaryOperator::Lt
206206
| BinaryOperator::LtEq
207207
| BinaryOperator::Gt
208-
| BinaryOperator::GtEq => {
208+
| BinaryOperator::GtEq
209209
if lt_cat != rt_cat
210210
&& lt_cat != TypeCategory::Unknown
211-
&& rt_cat != TypeCategory::Unknown
212-
{
213-
issues.push(TypeIssue {
214-
message: format!(
215-
"Comparing incompatible types: {} ({:?}) vs {} ({:?})",
216-
lt, lt_cat, rt, rt_cat
217-
),
218-
});
219-
}
211+
&& rt_cat != TypeCategory::Unknown =>
212+
{
213+
issues.push(TypeIssue {
214+
message: format!(
215+
"Comparing incompatible types: {} ({:?}) vs {} ({:?})",
216+
lt, lt_cat, rt, rt_cat
217+
),
218+
});
220219
}
221220
_ => {}
222221
}

tests/e2e_test.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -137,10 +137,7 @@ fn e2e_unknown_table_fails_at_l2() {
137137

138138
assert!(plugin.parse_check(query).is_ok(), "L1 must pass");
139139
let l2 = plugin.schema_check(query, &s).unwrap();
140-
assert!(
141-
!l2.is_empty(),
142-
"E2E: unknown table must produce L2 issues"
143-
);
140+
assert!(!l2.is_empty(), "E2E: unknown table must produce L2 issues");
144141
assert!(
145142
l2.iter().any(|i| i.message.contains("ghost_table")),
146143
"L2 issue must mention the missing table name"
@@ -307,7 +304,10 @@ fn e2e_cte_parses_at_l1() {
307304
let plugin = get_plugin("sql").unwrap();
308305
let query = "WITH top_accounts AS (SELECT id FROM accounts WHERE balance > 100) \
309306
SELECT id FROM top_accounts";
310-
assert!(plugin.parse_check(query).is_ok(), "E2E: CTE must parse at L1");
307+
assert!(
308+
plugin.parse_check(query).is_ok(),
309+
"E2E: CTE must parse at L1"
310+
);
311311
}
312312

313313
// ---------------------------------------------------------------------------

tests/property_test.rs

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,10 @@ const CORPUS: &[(&str, &str)] = &[
2222
// 0 — simple valid select
2323
("simple_select", "SELECT 1"),
2424
// 1 — select from known table (requires schema)
25-
("select_known", "SELECT id, username FROM accounts WHERE id = 1"),
25+
(
26+
"select_known",
27+
"SELECT id, username FROM accounts WHERE id = 1",
28+
),
2629
// 2 — invalid syntax
2730
("invalid_syntax", "NOT SQL AT ALL @@@ !!!"),
2831
// 3 — type mismatch: integer vs string
@@ -45,7 +48,10 @@ const CORPUS: &[(&str, &str)] = &[
4548
"SELECT id FROM accounts WHERE id IN (SELECT account_id FROM transactions)",
4649
),
4750
// 9 — aggregate
48-
("aggregate", "SELECT account_id, COUNT(*) FROM transactions GROUP BY account_id"),
51+
(
52+
"aggregate",
53+
"SELECT account_id, COUNT(*) FROM transactions GROUP BY account_id",
54+
),
4955
];
5056

5157
// ---------------------------------------------------------------------------
@@ -333,7 +339,7 @@ fn property_no_panic_on_full_corpus() {
333339
// We cannot move plugin/s into catch_unwind easily, so we just
334340
// verify the calls succeed outside of catch_unwind — if they
335341
// panic, the test fails.
336-
drop(label);
342+
let _ = label;
337343
});
338344
let _ = plugin.schema_check(query, &s);
339345
let _ = plugin.type_check(query, &s);

0 commit comments

Comments
 (0)