Skip to content

feat: tool hardening, Futhark FFI, F* extraction linkage#7

Merged
Jesssullivan merged 3 commits intomainfrom
feat/tool-hardening-ffi-fstar
Feb 26, 2026
Merged

feat: tool hardening, Futhark FFI, F* extraction linkage#7
Jesssullivan merged 3 commits intomainfrom
feat/tool-hardening-ffi-fstar

Conversation

@Jesssullivan
Copy link
Contributor

Summary

  • Tool hardening: Separate stdout/stderr capture via open_process_full, required_binary field on all 42 tools with startup availability check, standardized JSON output envelope (tool_output.ml)
  • Futhark FFI: Ctypes bindings for 3 GPU kernels via Dl.dlopen, lazy init with automatic fallback to pure-OCaml stubs
  • F extraction linkage*: Committed extracted modules, sha256 extern, wired verified backends into sanitize.ml, audit.ml, policy.ml; CI artifact upload for drift detection

Test plan

  • 34 OCaml tests pass (10 new: subprocess stderr, binary check, output envelope, FFI fallback/parity, F* sanitize/audit/policy parity)
  • 28 Go gateway tests pass
  • 3 Futhark kernel tests pass
  • dune build clean with ctypes integration

- Separate stdout/stderr via Unix.open_process_full (subprocess.ml)
- Add required_binary field to tool_def with startup availability check
- Standardized JSON output envelope via tool_output.ml
- Migrate all 42 tools to wrap_result/wrap_json/wrap_lines/wrap_error
- Ctypes bindings for scan_analysis, pattern_match, network_graph kernels
- Lazy dlopen with automatic fallback to pure-OCaml stubs
- Add ctypes/ctypes-foreign to dune and flake.nix
- justfile recipe for compiling Futhark C to shared libraries
- Commit F*-extracted modules (Types, Policy, Sanitize, Audit, Dispatch)
- Implement sha256 extern via Hexstrike_Extern
- Wire verified backends into sanitize.ml, audit.ml, policy.ml
- CI artifact upload for F* extraction output
- Add 10 new tests (subprocess, binary check, output envelope, FFI, F* parity)
@Jesssullivan Jesssullivan merged commit bf7a684 into main Feb 26, 2026
6 of 8 checks passed
@Jesssullivan Jesssullivan deleted the feat/tool-hardening-ffi-fstar branch February 26, 2026 15:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant