Skip to content

Commit 587ffb3

Browse files
hyperpolymathclaude
andcommitted
fix(chapel-binding): real-Chapel-2.x typecheck + WIRED-subset zig build fix
Wave 1 follow-up to PR #135 (binding-tier-1 Chapel pilot). Three distinct issues surfaced in CI on #135's first run, each of which was hiding behind the binding's never-having-been-compiled state. 1. CHAPEL TYPECHECK: T? syntax is class-only ============================================ The pre-existing binding used Chapel's `T?` postfix on value-type returns: `proc safeAdd(a, b): int(64)?`, `bool?`, `string?`. That syntax is class-only in Chapel 2.x — every Safe*.chpl module fails to typecheck. All 11 modules were affected; this is the deep "binding looked well-written but had never been compiled" finding. Replacement: `Maybe(T)` — a binding-provided generic record with `present: bool` and `value: T`, with constructors `some(v)` and `absent(T)`. Naming note: `none` and `nothing` are both Chapel reserved words, so the absent constructor is `absent`. All 11 Safe*.chpl wrappers + smoke + 3 tests rewritten. `Proven.chpl` adds `public import SafePath / SafeHeader / LibProven` so callers can write `SafePath.hasTraversal(...)` as a qualified reference. `enum ProvenStatus : int(32) { ... }` typed-enum syntax was also removed in Chapel 2.x. Dropped the type spec. `extractString` / `cStringToChapel` switched to `try!` for `string.createCopyingBuffer`, which is a throwing function in Chapel 2.x — the FFI guarantees the buffer shape so the unconditional unwrap is sound. 2. CI BUILD: ffi/zig/build.zig depends on a missing repo ======================================================== `hyperpolymath/idris2-zig-ffi` returns 404 to authenticated `gh`. The same break blocks `zig-ffi.yml` on main; resolving the upstream dep is out of scope for the Chapel pilot. All exports in `ffi/zig/src/main.zig` are pure-Zig (only `@import ("std")` + `@import("builtin")`); none actually consume the `idris2_zig_ffi` module. Switched `chapel-build` to compile `main.zig` directly via `zig build-lib -dynamic -lc`, producing a libproven.so with the WIRED 5 symbols. `build.zig.zon` declares `minimum_zig_version = "0.15.2"`; bumped the CI's pinned Zig from 0.13.0 to 0.15.2 to match. 3. proven.h missing `proven_version` / `proven_build_info` ========================================================== These two accessors are exported by `ffi/zig/src/main.zig` and called by the Chapel `libraryVersion()` / `libraryBuildInfo()` helpers. `chpl` performs extern-decl resolution against included C headers and fails the build when an `extern` references a symbol not declared in any `-I`-supplied header. Added two declarations to `bindings/c/include/proven.h`. These do NOT introduce new Zig exports — they declare functions that `main.zig` has always exported. Verification ============ Locally (chpl 2.8.0 + zig 0.15.2 against a freshly-built libproven.so): $ just check # symbol-audit PASS 5/0 $ just build # smoke target builds $ just test # smoke + 4 tests all GREEN hello_smoke: OK (libproven 0.1.0) TestFfiContract: OK TestLibraryInfo: OK (version=0.1.0) TestSafeHeader: OK TestSafePath: OK All 11 src/*.chpl typecheck clean with `chpl --no-codegen`. Detachability is preserved: every change here is inside the detachable file set (`bindings/chapel/**`, `bindings/c/include/proven.h`, the workflow). No new repo-root reach. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 40b127f commit 587ffb3

18 files changed

Lines changed: 313 additions & 392 deletions

.github/workflows/chapel-ci.yml

Lines changed: 32 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,9 @@ env:
5858
CHAPEL_DEB_URL: 'https://github.com/chapel-lang/chapel/releases/download/2.3.0/chapel-2.3.0-1.ubuntu22.amd64.deb'
5959
CHAPEL_DEB_SHA256: 'b7c1a48cbf26cfc7ad9af22a84ea4becb1a5e2fd485ec4a1f5f8a69e8a7cd58c'
6060
# Pinned Zig version (kept in sync with .github/workflows/zig-ffi.yml).
61-
ZIG_VERSION: '0.13.0'
61+
# Pinned Zig version. Matches ffi/zig/build.zig.zon's
62+
# `minimum_zig_version = "0.15.2"`.
63+
ZIG_VERSION: '0.15.2'
6264

6365
jobs:
6466
# ==========================================================================
@@ -124,20 +126,39 @@ jobs:
124126
with:
125127
path: proven
126128

127-
- name: Checkout idris2-zig-ffi dependency
128-
uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
129-
with:
130-
repository: hyperpolymath/idris2-zig-ffi
131-
path: idris2-zig-ffi
132-
133129
- name: Setup Zig ${{ env.ZIG_VERSION }}
134130
uses: mlugg/setup-zig@e7d1537c378b83b8049f65dda471d87a2f7b2df2 # v1
135131
with:
136132
version: ${{ env.ZIG_VERSION }}
137133

138-
- name: Build libproven.so via Zig
134+
- name: Build libproven.so (WIRED-subset fixture)
139135
working-directory: proven/ffi/zig
140-
run: zig build -Dtarget=x86_64-linux-gnu
136+
# NOTE: ffi/zig/build.zig depends on `idris2_zig_ffi` (relative
137+
# path to a sibling estate repo). That dep is not resolvable
138+
# from a fresh clone in CI (the same issue blocks zig-ffi.yml on
139+
# main), and resolving it is out of scope for the Chapel pilot.
140+
# All exports in src/main.zig are pure-Zig — none consume
141+
# idris2_zig_ffi. We compile main.zig directly with
142+
# `zig build-lib -dynamic -lc`, producing a libproven.so with
143+
# the WIRED 5 symbols (proven_path_has_traversal,
144+
# proven_header_has_crlf, proven_free_string, proven_version,
145+
# proven_build_info). When proven#88 lands the real
146+
# Idris-backed exports, this step swaps to
147+
# `zig build -Dtarget=...`.
148+
run: |
149+
set -euo pipefail
150+
mkdir -p zig-out/lib
151+
zig build-lib -dynamic -O ReleaseSafe \
152+
-fPIC \
153+
--name proven \
154+
-femit-bin=zig-out/lib/libproven.so \
155+
src/main.zig -lc
156+
ls -la zig-out/lib/
157+
nm -D --defined-only zig-out/lib/libproven.so \
158+
| awk '$2 ~ /^[TWV]$/ { print $3 }' \
159+
| grep -E '^(proven_path_has_traversal|proven_header_has_crlf|proven_free_string|proven_version|proven_build_info)$' \
160+
| sort -u | tee /tmp/wired-exports.txt
161+
test "$(wc -l < /tmp/wired-exports.txt)" -eq 5
141162
142163
- name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
143164
run: |
@@ -148,14 +169,13 @@ jobs:
148169
sudo apt-get install -y /tmp/chapel.deb
149170
chpl --version
150171
151-
- name: Chapel module typecheck (--library on every module)
172+
- name: Chapel module typecheck (--no-codegen, every module)
152173
working-directory: proven/bindings/chapel
153174
run: |
154175
set -euo pipefail
155176
for m in src/*.chpl; do
156177
echo "[chapel-build] typecheck $m"
157-
chpl --library --dynamic --print-callstack-on-error \
158-
--no-codegen \
178+
chpl --no-codegen --print-callstack-on-error \
159179
-M src/ \
160180
-I "$GITHUB_WORKSPACE/proven/bindings/c/include" \
161181
"$m"

bindings/c/include/proven.h

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,20 @@ uint32_t proven_version_patch(void);
169169
/** @brief Get total module count. */
170170
uint32_t proven_module_count(void);
171171

172+
/**
173+
* @brief Get the library version string (NUL-terminated, statically allocated).
174+
*
175+
* The returned pointer is owned by the library; do NOT free it.
176+
*/
177+
const char* proven_version(void);
178+
179+
/**
180+
* @brief Get build information (compiler, target, etc.; NUL-terminated, static).
181+
*
182+
* The returned pointer is owned by the library; do NOT free it.
183+
*/
184+
const char* proven_build_info(void);
185+
172186
/* ============================================================================
173187
* SafeMath - Arithmetic that cannot crash (9 functions)
174188
* ============================================================================ */

bindings/chapel/README.adoc

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -74,8 +74,10 @@ just test
7474
use Proven;
7575
7676
// WIRED: links + runs against libproven 0.9.0.
77-
var trav = SafePath.hasTraversal("../../etc/passwd"); // some(true)
78-
var crlf = SafeHeader.hasCrlf("v\r\nX-Inj: 1"); // some(true)
77+
// WIRED: links + runs against libproven 0.9.0.
78+
var trav = SafePath.hasTraversal("../../etc/passwd"); // Maybe(bool): some(true)
79+
var crlf = SafeHeader.hasCrlf("v\r\nX-Inj: 1"); // Maybe(bool): some(true)
80+
if trav.present && trav.value then writeln("blocked");
7981
8082
// Identify the linked libproven (debug-friendly).
8183
writeln("libproven version: ", libraryVersion());
@@ -88,21 +90,35 @@ writeln("libproven version: ", libraryVersion());
8890

8991
== Error Handling
9092

91-
All fallible operations return Chapel optional types (`T?`). Use pattern
92-
matching to handle errors:
93+
All fallible operations return `Maybe(T)` — a binding-provided record
94+
with a `present` flag and a `value`. Chapel 2.x's built-in `T?`
95+
postfix syntax is class-only and does NOT compile for value types
96+
(`bool?`, `int?`, `string?` all error); `Maybe(T)` is the
97+
binding-tier replacement.
9398

9499
[source,chapel]
95100
----
96101
var result = SafePath.hasTraversal(userInput);
97-
if result == none {
102+
if !result.present {
98103
writeln("FFI error reading input");
99-
} else if result! {
104+
} else if result.value {
100105
writeln("Path traversal detected — refusing");
101106
} else {
102107
writeln("Path is safe");
103108
}
104109
----
105110

111+
The constructors are `some(value)` and `absent(T)`:
112+
113+
[source,chapel]
114+
----
115+
return some(true); // Maybe(bool) with present == true
116+
return absent(int(64)); // Maybe(int(64)) with present == false
117+
----
118+
119+
(`absent` rather than `none`/`nothing` because both of those are
120+
reserved words in Chapel.)
121+
106122
== Coverage matrix (WIRED vs GATED)
107123

108124
WIRED — present in `libproven 0.9.0`, verified by `chapel-symbol-audit`,

bindings/chapel/smoke/hello_smoke.chpl

Lines changed: 14 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,8 @@
33
//
44
// hello_smoke.chpl - End-to-end "does the binding link and run" smoke test.
55
//
6-
// Builds:
7-
// chpl -o hello_smoke smoke/hello_smoke.chpl -M src/ -lproven
8-
//
96
// Runs in well under 2s and is kept green by chapel-ci.yml even if larger
10-
// jobs go red. This is the "the binding actually works" gate.
7+
// jobs go red.
118
//
129
// Calls the WIRED subset only. Lifecycle (provenInit/Deinit) is GATED on
1310
// proven#88 because the Zig export ABI does not yet match the proven.h
@@ -16,34 +13,28 @@
1613
use Proven;
1714

1815
proc main(): int {
19-
// SafePath.hasTraversal — happy path (no traversal) and detection path.
20-
const safePath = "/var/www/html/index.html";
21-
const evilPath = "../../etc/passwd";
22-
23-
const okSafe = SafePath.hasTraversal(safePath);
24-
const okEvil = SafePath.hasTraversal(evilPath);
16+
// SafePath.hasTraversal — happy + detection paths.
17+
const okSafe = SafePath.hasTraversal("/var/www/html/index.html");
18+
const okEvil = SafePath.hasTraversal("../../etc/passwd");
2519

26-
if okSafe == none || okSafe! != false {
27-
writeln("FAIL: SafePath.hasTraversal('", safePath, "') did not return some(false)");
20+
if !okSafe.present || okSafe.value != false {
21+
writeln("FAIL: SafePath.hasTraversal('/var/www/html/index.html') did not return some(false)");
2822
return 1;
2923
}
30-
if okEvil == none || okEvil! != true {
31-
writeln("FAIL: SafePath.hasTraversal('", evilPath, "') did not return some(true)");
24+
if !okEvil.present || okEvil.value != true {
25+
writeln("FAIL: SafePath.hasTraversal('../../etc/passwd') did not return some(true)");
3226
return 1;
3327
}
3428

35-
// SafeHeader.hasCrlf — happy path (no CRLF) and detection path.
36-
const safeHeader = "application/json";
37-
const evilHeader = "value\r\nX-Injected: hi";
38-
39-
const headerOkSafe = SafeHeader.hasCrlf(safeHeader);
40-
const headerOkEvil = SafeHeader.hasCrlf(evilHeader);
29+
// SafeHeader.hasCrlf — happy + detection paths.
30+
const headerOkSafe = SafeHeader.hasCrlf("application/json");
31+
const headerOkEvil = SafeHeader.hasCrlf("value\r\nX-Injected: hi");
4132

42-
if headerOkSafe == none || headerOkSafe! != false {
43-
writeln("FAIL: SafeHeader.hasCrlf('", safeHeader, "') did not return some(false)");
33+
if !headerOkSafe.present || headerOkSafe.value != false {
34+
writeln("FAIL: SafeHeader.hasCrlf('application/json') did not return some(false)");
4435
return 1;
4536
}
46-
if headerOkEvil == none || headerOkEvil! != true {
37+
if !headerOkEvil.present || headerOkEvil.value != true {
4738
writeln("FAIL: SafeHeader.hasCrlf(<CRLF>) did not return some(true)");
4839
return 1;
4940
}

bindings/chapel/src/LibProven.chpl

Lines changed: 52 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,14 @@ module LibProven {
3535
// Status codes (used by both WIRED and GATED results)
3636
// ========================================================================
3737

38-
/** Status codes returned by Proven operations. */
39-
enum ProvenStatus : int(32) {
38+
/** Status codes returned by Proven operations.
39+
*
40+
* Chapel 2.x removed the `enum X : int(32) { ... }` type-spec syntax;
41+
* the C ABI's int32 status field is the source of truth, and this
42+
* enum is for human-readable documentation. Use `.toInt(32)` (or
43+
* compare via the `isOk` helper) when interoperating with FFI.
44+
*/
45+
enum ProvenStatus {
4046
OK = 0,
4147
ErrNullPointer = -1,
4248
ErrInvalidArgument = -2,
@@ -266,6 +272,37 @@ module LibProven {
266272
ptr: c_ptrConst(uint(8)), len: c_size_t
267273
): FloatResult;
268274

275+
// ========================================================================
276+
// Maybe(T) — Chapel-2.x-compatible optional-type pattern.
277+
//
278+
// Chapel's `T?` postfix is class-only; value-type wrappers
279+
// (`bool?` / `int(64)?` / `string?`) do NOT compile. Maybe(T) is a
280+
// generic record with a `present` flag and a `value`. `some(v)` and
281+
// `none(T)` are the constructors; call sites pattern-match via
282+
// `if r.present then r.value else fallback`.
283+
// ========================================================================
284+
285+
/** Optional value-type carrier — see module-level note. */
286+
record Maybe {
287+
type T;
288+
var present : bool;
289+
var value : T;
290+
}
291+
292+
/** Wrap a value as a present Maybe(T). */
293+
inline proc some(in v): Maybe(v.type) {
294+
return new Maybe(v.type, true, v);
295+
}
296+
297+
/** Construct an absent Maybe(T). Pass the type explicitly:
298+
* `return absent(bool)` / `absent(int(64))` / `absent(string)`.
299+
*
300+
* (Named `absent` because Chapel reserves `none` and `nothing`.) */
301+
inline proc absent(type T): Maybe(T) {
302+
var dflt : T;
303+
return new Maybe(T, false, dflt);
304+
}
305+
269306
// ========================================================================
270307
// Helper: convert Chapel string to C pointer + length.
271308
// ========================================================================
@@ -280,18 +317,27 @@ module LibProven {
280317
return status == 0;
281318
}
282319

283-
/** Extract a Chapel string from a StringResult and free the C memory. */
320+
/** Extract a Chapel string from a StringResult and free the C memory.
321+
*
322+
* ``string.createCopyingBuffer`` is throwing; we use ``try!`` because
323+
* the C ABI guarantees a valid UTF-8 buffer of declared length when
324+
* status is OK. An empty status / nil pointer short-circuits to "". */
284325
proc extractString(ref r: StringResult): string {
285326
if !isOk(r.status) || r.value == nil then return "";
286-
var s = string.createCopyingBuffer(r.value: c_ptrConst(c_char), r.length: int);
327+
var s = try! string.createCopyingBuffer(r.value: c_ptrConst(c_char),
328+
r.length: int);
287329
provenFreeString(r.value);
288330
return s;
289331
}
290332

291-
/** Read a NUL-terminated C string returned by libproven (no free required). */
333+
/** Read a NUL-terminated C string returned by libproven (no free required).
334+
*
335+
* Uses ``try!`` for the same reason as ``extractString``: libproven
336+
* guarantees NUL-termination on the string accessors that call this
337+
* (proven_version, proven_build_info). */
292338
proc cStringToChapel(p: c_ptrConst(c_char)): string {
293339
if p == nil then return "";
294-
return string.createCopyingBuffer(p);
340+
return try! string.createCopyingBuffer(p);
295341
}
296342

297343
/** Library version string from the loaded libproven. */

bindings/chapel/src/Proven.chpl

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,10 +31,15 @@ module Proven {
3131

3232
// Core FFI declarations + helpers (extern types, WIRED externs,
3333
// GATED extern decls kept under a GATED banner inside LibProven).
34+
// `use` brings procs into scope unqualified; `import` makes the
35+
// module name itself visible as a qualifier.
3436
public use LibProven;
37+
public import LibProven;
3538

36-
// WIRED safety modules (smoke + chapel-tests target these):
39+
// WIRED safety modules (smoke + chapel-tests target these).
3740
public use SafePath;
41+
public import SafePath;
3842
public use SafeHeader;
43+
public import SafeHeader;
3944

4045
}

bindings/chapel/src/SafeCrypto.chpl

Lines changed: 19 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -3,56 +3,43 @@
33
//
44
// SafeCrypto - Cryptographic primitives via libproven FFI.
55
//
6-
// All computation is performed in the Idris 2 core via the Zig FFI bridge.
7-
// This module is a thin wrapper; it does NOT reimplement any logic.
6+
// Status: GATED on proven#88 (proven_crypto_* + proven_hex_encode).
87

98
module SafeCrypto {
109

1110
public use LibProven;
11+
use CTypes;
1212

13-
/**
14-
* Constant-time byte comparison (timing-attack safe).
15-
*
16-
* :arg a: First byte sequence (string).
17-
* :arg b: Second byte sequence (string).
18-
* :returns: ``none`` on error, true if equal, false otherwise.
19-
*/
20-
proc constantTimeEq(a: string, b: string): bool? {
13+
/** Constant-time byte comparison (timing-attack safe). */
14+
proc constantTimeEq(a: string, b: string): Maybe(bool) {
2115
var (ptrA, lenA) = toCBytes(a);
2216
var (ptrB, lenB) = toCBytes(b);
2317
var r = provenCryptoConstantTimeEq(ptrA, lenA, ptrB, lenB);
24-
if isOk(r.status) then return r.value;
25-
return none;
18+
if isOk(r.status) then return some(r.value);
19+
return absent(bool);
2620
}
2721

2822
/**
2923
* Fill a buffer with cryptographically secure random bytes.
3024
*
31-
* :arg n: Number of bytes to generate.
32-
* :returns: ``none`` on error, otherwise an array of random bytes.
25+
* Returns ``some(true)`` on success and ``absent(bool)`` on failure;
26+
* the caller-provided buffer is filled in-place via the FFI.
27+
* Array-typed Maybe return is sidestepped because the result type
28+
* would carry a domain.
3329
*/
34-
proc randomBytes(n: int): [0..#n] uint(8)? {
35-
var buf : [0..#n] uint(8);
36-
var status = provenCryptoRandomBytes(c_ptrTo(buf[0]), n: c_size_t);
37-
if isOk(status) then return buf;
38-
return none;
30+
proc randomBytes(ref buf: [] uint(8)): Maybe(bool) {
31+
var status = provenCryptoRandomBytes(c_ptrTo(buf[buf.domain.low]),
32+
buf.size: c_size_t);
33+
if isOk(status) then return some(true);
34+
return absent(bool);
3935
}
4036

41-
/**
42-
* Encode bytes to hexadecimal string.
43-
*
44-
* :arg data: Input bytes (string).
45-
* :arg uppercase: Use uppercase hex digits (default false).
46-
* :returns: ``none`` on error, otherwise the hex string.
47-
*/
48-
proc hexEncode(data: string, uppercase: bool = false): string? {
37+
/** Encode bytes to hexadecimal string. */
38+
proc hexEncode(data: string, uppercase: bool = false): Maybe(string) {
4939
var (ptr, len) = toCBytes(data);
5040
var r = provenHexEncode(ptr, len, uppercase);
51-
if isOk(r.status) {
52-
var result = extractString(r);
53-
return result;
54-
}
55-
return none;
41+
if isOk(r.status) then return some(extractString(r));
42+
return absent(string);
5643
}
5744

5845
}

0 commit comments

Comments
 (0)