From 7e1584b0372a2935fb4afdd0ddbc5117b8904f50 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 12:02:01 +0000 Subject: [PATCH] =?UTF-8?q?chore(docs,ci):=20clear=20genuine=20Hypatia=20f?= =?UTF-8?q?indings=20=E2=80=94=20stale=20src/abi=20paths,=20setup.sh,=20.e?= =?UTF-8?q?nvrc?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the actionable subset of the Hypatia advisory findings surfaced by the scanner upgrade in #26. The remaining ~7 are scanner false-positives (WF017 two-step gate, SC-013 comment stripping, SC-014 codeql substring) for an upstream fix. Docs (structural_drift SD022 x6 — stale path after #20's FFI removal): - correct `src/abi/` -> the real RSR slot `src/interface/abi/` in AI-CONVENTIONS, RSR_OUTLINE, QUICKSTART-DEV, MAINTENANCE-CHECKLIST, INTENT.contractile - replace the unfilled-template docs/developer/ABI-FFI-README.adoc (it still carried a `{{project}}` placeholder and a template-instruction line and described a non-existent FFI surface) with an honest "no FFI surface" stub pointing at the RSR placeholders and PROOF-NEEDS.md setup.sh (code_safety shell_download_then_run / CWE-494): - replace `curl ... just.systems/install.sh | bash` with a download-then-run helper (no pipe-to-shell), with opt-in JUST_VERSION pin and JUST_INSTALL_SHA256 verify; native package managers (incl. nix/guix) are still tried first - update the header usage example to the download-then-run form .envrc (secret_detected "Generic API key" — false-positive, commented placeholder): - remove the residual `# export DATABASE_URL=...` / `# export API_KEY=...` lines (re-lands the fix intended in #25 that never reached main) This does not by itself turn the hypatia check green — that needs the upstream reusable to restore `--exit-zero`/`|| true` on the scan step so it follows its documented advisory ("warn but don't fail") policy. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01UCnxjXkN6uDj9YSANuGEgR --- .envrc | 2 - .machine_readable/INTENT.contractile | 2 +- QUICKSTART-DEV.adoc | 2 +- docs/RSR_OUTLINE.adoc | 4 +- docs/developer/ABI-FFI-README.adoc | 392 +-------------------- docs/governance/MAINTENANCE-CHECKLIST.adoc | 2 +- docs/practice/AI-CONVENTIONS.adoc | 2 +- setup.sh | 47 ++- 8 files changed, 61 insertions(+), 392 deletions(-) diff --git a/.envrc b/.envrc index 190891a..ff03956 100644 --- a/.envrc +++ b/.envrc @@ -20,8 +20,6 @@ fi # Project environment variables export PROJECT_NAME="gv-clade-index" export RSR_TIER="infrastructure" -# export DATABASE_URL="..." -# export API_KEY="..." # Source .env if it exists (gitignored) dotenv_if_exists diff --git a/.machine_readable/INTENT.contractile b/.machine_readable/INTENT.contractile index a112792..dba5524 100644 --- a/.machine_readable/INTENT.contractile +++ b/.machine_readable/INTENT.contractile @@ -58,7 +58,7 @@ ; === Sensitive Areas (if in doubt, ask) === (ask-before-touching ; *REMINDER: List areas where LLMs should check before modifying* - ; "src/abi/ — formal proofs, changes require re-verification" + ; "src/interface/abi/ — formal proofs, changes require re-verification" ; "ffi/zig/ — C ABI boundary, changes affect all language bindings" ; ".machine_readable/ — checkpoint files, format is specified" ) diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc index 5d68517..1fccd73 100644 --- a/QUICKSTART-DEV.adoc +++ b/QUICKSTART-DEV.adoc @@ -54,7 +54,7 @@ cd worker && npm test ---- gv-clade-index/ ├── src/ # Source code -├── src/abi/ # Idris2 ABI definitions (if applicable) +├── src/interface/abi/ # Idris2 ABI definitions (if applicable) ├── ffi/zig/ # Zig FFI bridge (if applicable) ├── tests/ # Test suite ├── docs/ # Documentation diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index e07a65e..c999854 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -101,7 +101,7 @@ just validate-rsr |`AI.a2ml` |Claude-specific instructions -|`src/abi/` +|`src/interface/abi/` |Idris2 ABI definitions (Types, Layout, Foreign) |`ffi/zig/` @@ -177,7 +177,7 @@ project/ │ ├── TOPOLOGY-GUIDE.adoc │ ├── generated/ │ └── man/ -├── src/abi/ # Idris2 ABI definitions +├── src/interface/abi/ # Idris2 ABI definitions │ ├── Types.idr │ ├── Layout.idr │ └── Foreign.idr diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index e63e0d8..835b647 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -1,384 +1,20 @@ -= ABI/FFI Standards -{{~ Aditionally delete this line and fill out the template below ~}} += ABI/FFI — Not Applicable -# gv-clade-index ABI/FFI Documentation +`gv-clade-index` is a JavaScript Cloudflare Worker over a VeriSimDB/KV registry +(a `gv` / `db` project). It has *no native ABI or FFI surface*: there are no +Idris2 ABI definitions and no Zig FFI bindings to document here. -## Overview +== RSR placeholders -This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: +The RSR interface slots are retained for structural validation +(`just validate-rsr`) but carry no implementation: -- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs -- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility -- **Generated C headers** bridge Idris2 ABI to Zig FFI -- **Any language** can call through standard C ABI +* `src/interface/abi/` — ABI slot (README + AI manifest only) +* `src/interface/ffi/` — FFI slot (README + AI manifest only) +* `src/interface/generated/` — generated-bindings slot -## Architecture +== If an ABI/FFI surface is ever introduced -``` -┌─────────────────────────────────────────────┐ -│ ABI Definitions (Idris2) │ -│ src/abi/ │ -│ - Types.idr (Type definitions) │ -│ - Layout.idr (Memory layout proofs) │ -│ - Foreign.idr (FFI declarations) │ -└─────────────────┬───────────────────────────┘ - │ - │ generates (at compile time) - ▼ -┌─────────────────────────────────────────────┐ -│ C Headers (auto-generated) │ -│ generated/abi/{{project}}.h │ -└─────────────────┬───────────────────────────┘ - │ - │ imported by - ▼ -┌─────────────────────────────────────────────┐ -│ FFI Implementation (Zig) │ -│ ffi/zig/src/main.zig │ -│ - Implements C-compatible functions │ -│ - Zero-cost abstractions │ -│ - Memory-safe by default │ -└─────────────────┬───────────────────────────┘ - │ - │ compiled to lib{{project}}.so/.a - ▼ -┌─────────────────────────────────────────────┐ -│ Any Language via C ABI │ -│ - Rust, ReScript, Julia, Python, etc. │ -└─────────────────────────────────────────────┘ -``` - -## Directory Structure - -``` -{{project}}/ -├── src/ -│ ├── abi/ # ABI definitions (Idris2) -│ │ ├── Types.idr # Core type definitions with proofs -│ │ ├── Layout.idr # Memory layout verification -│ │ └── Foreign.idr # FFI function declarations -│ └── lib/ # Core library (any language) -│ -├── ffi/ -│ └── zig/ # FFI implementation (Zig) -│ ├── build.zig # Build configuration -│ ├── build.zig.zon # Dependencies -│ ├── src/ -│ │ └── main.zig # C-compatible FFI implementation -│ ├── test/ -│ │ └── integration_test.zig -│ └── include/ -│ └── {{project}}.h # C header (optional, can be generated) -│ -├── generated/ # Auto-generated files -│ └── abi/ -│ └── {{project}}.h # Generated from Idris2 ABI -│ -└── bindings/ # Language-specific wrappers (optional) - ├── rust/ - ├── rescript/ - └── julia/ -``` - -## Why Idris2 for ABI? - -### 1. **Formal Verification** - -Idris2's dependent types allow proving properties about the ABI at compile-time: - -```idris --- Prove struct size is correct -public export -exampleStructSize : HasSize ExampleStruct 16 - --- Prove field alignment is correct -public export -fieldAligned : Divides 8 (offsetOf ExampleStruct.field) - --- Prove ABI is platform-compatible -public export -abiCompatible : Compatible (ABI 1) (ABI 2) -``` - -### 2. **Type Safety** - -Encode invariants that C/Zig cannot express: - -```idris --- Non-null pointer guaranteed at type level -data Handle : Type where - MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle - --- Array with length proof -data Buffer : (n : Nat) -> Type where - MkBuffer : Vect n Byte -> Buffer n -``` - -### 3. **Platform Abstraction** - -Platform-specific types with compile-time selection: - -```idris -CInt : Platform -> Type -CInt Linux = Bits32 -CInt Windows = Bits32 - -CSize : Platform -> Type -CSize Linux = Bits64 -CSize Windows = Bits64 -``` - -### 4. **Safe Evolution** - -Prove that new ABI versions are backward-compatible: - -```idris --- Compiler enforces compatibility -abiUpgrade : ABI 1 -> ABI 2 -abiUpgrade old = MkABI2 { - -- Must preserve all v1 fields - v1_compat = old, - -- Can add new fields - new_features = defaults -} -``` - -## Why Zig for FFI? - -### 1. **C ABI Compatibility** - -Zig exports C-compatible functions naturally: - -```zig -export fn library_function(param: i32) i32 { - return param * 2; -} -``` - -### 2. **Memory Safety** - -Compile-time safety without runtime overhead: - -```zig -// Null check enforced at compile time -const handle = init() orelse return error.InitFailed; -defer free(handle); -``` - -### 3. **Cross-Compilation** - -Built-in cross-compilation to any platform: - -```bash -zig build -Dtarget=x86_64-linux -zig build -Dtarget=aarch64-macos -zig build -Dtarget=x86_64-windows -``` - -### 4. **Zero Dependencies** - -No runtime, no libc required (unless explicitly needed): - -```zig -// Minimal binary size -pub const lib = @import("std"); -// Only includes what you use -``` - -## Building - -### Build FFI Library - -```bash -cd ffi/zig -zig build # Build debug -zig build -Doptimize=ReleaseFast # Build optimized -zig build test # Run tests -``` - -### Generate C Header from Idris2 ABI - -```bash -cd src/abi -idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h -``` - -### Cross-Compile - -```bash -cd ffi/zig - -# Linux x86_64 -zig build -Dtarget=x86_64-linux - -# macOS ARM64 -zig build -Dtarget=aarch64-macos - -# Windows x86_64 -zig build -Dtarget=x86_64-windows -``` - -## Usage - -### From C - -```c -#include "{{project}}.h" - -int main() { - void* handle = {{project}}_init(); - if (!handle) return 1; - - int result = {{project}}_process(handle, 42); - if (result != 0) { - const char* err = {{project}}_last_error(); - fprintf(stderr, "Error: %s\n", err); - } - - {{project}}_free(handle); - return 0; -} -``` - -Compile with: -```bash -gcc -o example example.c -l{{project}} -L./zig-out/lib -``` - -### From Idris2 - -```idris -import gv-clade-index.ABI.Foreign - -main : IO () -main = do - Just handle <- init - | Nothing => putStrLn "Failed to initialize" - - Right result <- process handle 42 - | Left err => putStrLn $ "Error: " ++ errorDescription err - - free handle - putStrLn "Success" -``` - -### From Rust - -```rust -#[link(name = "{{project}}")] -extern "C" { - fn {{project}}_init() -> *mut std::ffi::c_void; - fn {{project}}_free(handle: *mut std::ffi::c_void); - fn {{project}}_process(handle: *mut std::ffi::c_void, input: u32) -> i32; -} - -fn main() { - unsafe { - let handle = {{project}}_init(); - assert!(!handle.is_null()); - - let result = {{project}}_process(handle, 42); - assert_eq!(result, 0); - - {{project}}_free(handle); - } -} -``` - -### From Julia - -```julia -const lib{{project}} = "lib{{project}}" - -function init() - handle = ccall((:{{project}}_init, lib{{project}}), Ptr{Cvoid}, ()) - handle == C_NULL && error("Failed to initialize") - handle -end - -function process(handle, input) - result = ccall((:{{project}}_process, lib{{project}}), Cint, (Ptr{Cvoid}, UInt32), handle, input) - result -end - -function cleanup(handle) - ccall((:{{project}}_free, lib{{project}}), Cvoid, (Ptr{Cvoid},), handle) -end - -# Usage -handle = init() -try - result = process(handle, 42) - println("Result: $result") -finally - cleanup(handle) -end -``` - -## Testing - -### Unit Tests (Zig) - -```bash -cd ffi/zig -zig build test -``` - -### Integration Tests - -```bash -cd ffi/zig -zig build test-integration -``` - -### ABI Verification (Idris2) - -```idris --- Compile-time verification -%runElab verifyABI - --- Runtime checks -main : IO () -main = do - verifyLayoutsCorrect - verifyAlignmentsCorrect - putStrLn "ABI verification passed" -``` - -## Contributing - -When modifying the ABI/FFI: - -1. **Update ABI first** (`src/abi/*.idr`) - - Modify type definitions - - Update proofs - - Ensure backward compatibility - -2. **Generate C header** - ```bash - idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h - ``` - -3. **Update FFI implementation** (`ffi/zig/src/main.zig`) - - Implement new functions - - Match ABI types exactly - -4. **Add tests** - - Unit tests in Zig - - Integration tests - - ABI verification tests - -5. **Update documentation** - - Function signatures - - Usage examples - - Migration guide (if breaking changes) - -## License - -MPL-2.0 - -## See Also - -- [Idris2 Documentation](https://idris2.readthedocs.io) -- [Zig Documentation](https://ziglang.org/documentation/master/) -- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories) +Formal ABI proofs would be added per the policy in `PROOF-NEEDS.md`, and this +document should then be expanded to describe the Idris2 -> C-header -> Zig +bridge. Until then, treat this project as pure JavaScript at the edge. diff --git a/docs/governance/MAINTENANCE-CHECKLIST.adoc b/docs/governance/MAINTENANCE-CHECKLIST.adoc index 0b40654..f4b082b 100644 --- a/docs/governance/MAINTENANCE-CHECKLIST.adoc +++ b/docs/governance/MAINTENANCE-CHECKLIST.adoc @@ -104,7 +104,7 @@ Run this pass at the end of a corrective/adaptive/perfective cycle: - single navigation entry point in root (`NAVIGATION.adoc` or equivalent) - no duplicate conflicting docs for same purpose (for example both `.md` and `.adoc` in root unless intentionally required) - [ ] Enforce ABI/FFI purity where the policy applies: - - ABI definitions in Idris2 (`src/abi/*.idr`) + - ABI definitions in Idris2 (`src/interface/abi/*.idr`) - FFI implementations in Zig (`ffi/**/*.zig`) - [ ] Ensure quality gate includes: formatting, lint, unit/integration tests, p2p/e2e checks, benchmark smoke, docs checks, security scan. diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index f0ed9ea..7ad8089 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -66,7 +66,7 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit ## ABI/FFI Standard -- ABI definitions: **Idris2** with dependent types (`src/abi/`). +- ABI definitions: **Idris2** with dependent types (`src/interface/abi/`). - FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`). - Generated C headers: `generated/abi/`. diff --git a/setup.sh b/setup.sh index 173e9fe..95410bd 100755 --- a/setup.sh +++ b/setup.sh @@ -6,7 +6,7 @@ # Then hands off to `just setup` for project-specific configuration. # # Usage: -# curl -fsSL https://raw.githubusercontent.com/hyperpolymath/gv-clade-index/main/setup.sh | sh +# curl -fsSL https://raw.githubusercontent.com/hyperpolymath/gv-clade-index/main/setup.sh -o setup.sh && sh setup.sh # # or after cloning: # ./setup.sh # @@ -128,6 +128,43 @@ detect_platform() { esac } +# ── Install just (upstream installer, hardened) ── +# Download the official installer to a temp file and run it, instead of piping a +# remote script straight into a shell (CWE-494). Opt-in reproducibility: +# JUST_VERSION=1.x.y pin the installed just version (installer --tag) +# JUST_INSTALL_SHA256= verify the installer before running it +# For fully reproducible installs prefer a package manager (nix/guix) above. +install_just_upstream() { + _ji_url="https://just.systems/install.sh" + _ji_tmp=$(mktemp 2>/dev/null || printf '/tmp/just-install.%s.sh' "$$") + if ! curl -fsSL "$_ji_url" -o "$_ji_tmp" || [ ! -s "$_ji_tmp" ]; then + fail "Could not download the just installer from $_ji_url" + rm -f "$_ji_tmp" + return 1 + fi + if [ -n "${JUST_INSTALL_SHA256:-}" ]; then + if command -v sha256sum >/dev/null 2>&1; then + printf '%s %s\n' "$JUST_INSTALL_SHA256" "$_ji_tmp" | sha256sum -c - >/dev/null 2>&1 || { + fail "just installer checksum mismatch — aborting" + rm -f "$_ji_tmp" + return 1 + } + else + warn "sha256sum unavailable — cannot verify JUST_INSTALL_SHA256" + fi + fi + _ji_sh=sh + command -v bash >/dev/null 2>&1 && _ji_sh=bash + _ji_rc=0 + if [ -n "${JUST_VERSION:-}" ]; then + "$_ji_sh" "$_ji_tmp" --tag "$JUST_VERSION" --to /usr/local/bin || _ji_rc=$? + else + "$_ji_sh" "$_ji_tmp" --to /usr/local/bin || _ji_rc=$? + fi + rm -f "$_ji_tmp" + return $_ji_rc +} + # ── Install just ── install_just() { if command -v just >/dev/null 2>&1; then @@ -139,10 +176,8 @@ install_just() { case "$PKG_MGR" in dnf) sudo dnf install -y just ;; - apt) sudo apt-get install -y just 2>/dev/null || { - # just not in older apt repos — use installer - curl -fsSL https://just.systems/install.sh | bash -s -- --to /usr/local/bin - } ;; + apt) sudo apt-get install -y just 2>/dev/null \ + || install_just_upstream || true ;; pacman) sudo pacman -S --noconfirm just ;; apk) sudo apk add just ;; brew) brew install just ;; @@ -153,7 +188,7 @@ install_just() { nix) nix-env -iA nixpkgs.just ;; *) info "Using just installer script..." - curl -fsSL https://just.systems/install.sh | bash -s -- --to /usr/local/bin + install_just_upstream || true ;; esac