From 6b0859f43ef311d6c3364c4aa13da89c680abaad Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 14:04:30 +0100 Subject: [PATCH] chore(nix->guix): delete Nix estate-wide (#138) --- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 2 +- bindings/nix/default.nix | 102 ----------------- bindings/nix/lib/proven.nix | 62 ----------- bindings/nix/lib/safe-math.nix | 82 -------------- bindings/nix/lib/safe-path.nix | 75 ------------- bindings/nix/lib/safe-string.nix | 76 ------------- bindings/nix/lib/safe-validators.nix | 159 --------------------------- nix/shard.nix | 14 --- 9 files changed, 2 insertions(+), 572 deletions(-) delete mode 100644 bindings/nix/default.nix delete mode 100644 bindings/nix/lib/proven.nix delete mode 100644 bindings/nix/lib/safe-math.nix delete mode 100644 bindings/nix/lib/safe-path.nix delete mode 100644 bindings/nix/lib/safe-string.nix delete mode 100644 bindings/nix/lib/safe-validators.nix delete mode 100644 nix/shard.nix diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index aad0d030..3a0ed491 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -14,4 +14,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 1f8c9405..baf722f8 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -17,4 +17,4 @@ permissions: jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 diff --git a/bindings/nix/default.nix b/bindings/nix/default.nix deleted file mode 100644 index f15e1d4d..00000000 --- a/bindings/nix/default.nix +++ /dev/null @@ -1,102 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# default.nix -- Nix derivation that builds and wraps libproven. -# -# Since Nix is a purely functional configuration language with no direct C FFI, -# this derivation builds the proven CLI from source and provides helper -# functions that shell out to the CLI for validation and safe operations. -# -# All computation is performed by the proven CLI (backed by Idris 2 verified -# code via Zig FFI). No logic is reimplemented in Nix. -# -# Usage: -# nix-build -# nix-build -A proven-cli # Just the CLI binary -# nix-build -A lib # Helper library for use in Nix expressions - -{ pkgs ? import {} }: - -let - # Build the proven CLI from source. - # The CLI wraps libproven (Idris 2 + Zig FFI) behind a command-line interface. - proven-cli = pkgs.stdenv.mkDerivation { - pname = "proven-cli"; - version = "0.9.0"; - - src = ../../.; - - nativeBuildInputs = with pkgs; [ - zig - idris2 - ]; - - buildPhase = '' - # Build the Idris 2 core library - idris2 --build proven.ipkg || true - - # Build the Zig FFI bridge and CLI - cd ffi/zig - zig build -Doptimize=ReleaseSafe || true - cd ../.. - - # Build the CLI application - if [ -d apps/cli ]; then - cd apps/cli - zig build -Doptimize=ReleaseSafe || true - cd ../.. - fi - ''; - - installPhase = '' - mkdir -p $out/bin $out/lib $out/include - - # Install CLI binary (search common output locations) - for candidate in \ - ffi/zig/zig-out/bin/proven \ - apps/cli/zig-out/bin/proven \ - build/proven \ - zig-out/bin/proven; do - if [ -f "$candidate" ]; then - cp "$candidate" $out/bin/proven - break - fi - done - - # Install shared library if available - for lib in ffi/zig/zig-out/lib/libproven.so ffi/zig/zig-out/lib/libproven.a; do - if [ -f "$lib" ]; then - cp "$lib" $out/lib/ - fi - done - - # Install C headers - if [ -d bindings/c/include ]; then - cp bindings/c/include/*.h $out/include/ - fi - ''; - - meta = with pkgs.lib; { - description = "Formally verified safety library -- CLI interface"; - homepage = "https://github.com/hyperpolymath/proven"; - license = { spdxId = "MPL-2.0"; free = true; }; - maintainers = [ "Jonathan D.A. Jewell " ]; - platforms = platforms.unix; - }; - }; - - # Import the helper libraries that wrap the CLI. - lib = import ./lib/proven.nix { inherit pkgs proven-cli; }; - -in { - inherit proven-cli lib; - - # Default output: the CLI binary - default = proven-cli; - - # Expose sub-libraries for targeted imports - safeMath = import ./lib/safe-math.nix { inherit pkgs proven-cli; }; - safeString = import ./lib/safe-string.nix { inherit pkgs proven-cli; }; - safePath = import ./lib/safe-path.nix { inherit pkgs proven-cli; }; - safeValidators = import ./lib/safe-validators.nix { inherit pkgs proven-cli; }; -} diff --git a/bindings/nix/lib/proven.nix b/bindings/nix/lib/proven.nix deleted file mode 100644 index 63c90244..00000000 --- a/bindings/nix/lib/proven.nix +++ /dev/null @@ -1,62 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# proven.nix -- Top-level Nix helper library for the proven safety library. -# -# Aggregates all safe-* sub-modules into a single attribute set. -# Each function shells out to the proven CLI, which delegates to the -# Idris 2 formally verified implementation via the Zig FFI bridge. -# -# NO logic is reimplemented in Nix. All computation is performed by the CLI. -# -# Usage: -# let proven = import ./proven.nix { inherit pkgs proven-cli; }; -# in proven.safeMath.addChecked 100 200 -# proven.safeString.escapeHtml "" -# proven.safeValidators.isValidEmail "user@example.com" - -{ pkgs, proven-cli }: - -let - safeMath = import ./safe-math.nix { inherit pkgs proven-cli; }; - safeString = import ./safe-string.nix { inherit pkgs proven-cli; }; - safePath = import ./safe-path.nix { inherit pkgs proven-cli; }; - safeValidators = import ./safe-validators.nix { inherit pkgs proven-cli; }; - - # Helper to invoke the proven CLI and capture stdout. - # Returns null on non-zero exit code. - runProven = args: - let - result = pkgs.runCommand "proven-invoke" { - nativeBuildInputs = [ proven-cli ]; - } '' - proven ${args} > $out 2>/dev/null || echo "__PROVEN_ERROR__" > $out - ''; - output = builtins.readFile result; - in - if output == "__PROVEN_ERROR__\n" then null - else builtins.replaceStrings ["\n"] [""] output; - - # Library version - version = "0.9.0"; - -in { - inherit safeMath safeString safePath safeValidators; - inherit runProven version; - - # Lifecycle helpers (informational; Nix evaluations are ephemeral) - meta = { - description = "Proven safety library -- Nix bindings via CLI"; - homepage = "https://github.com/hyperpolymath/proven"; - license = "MPL-2.0"; - maintainer = "Jonathan D.A. Jewell "; - moduleCount = 41; - cliRequired = true; - note = '' - Nix cannot perform direct C FFI. All proven operations shell out to - the proven CLI binary. Results are captured as Nix strings and parsed. - This means operations are evaluated at Nix evaluation time via IFD - (import from derivation) or at build time via runCommand. - ''; - }; -} diff --git a/bindings/nix/lib/safe-math.nix b/bindings/nix/lib/safe-math.nix deleted file mode 100644 index 702941f2..00000000 --- a/bindings/nix/lib/safe-math.nix +++ /dev/null @@ -1,82 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# safe-math.nix -- Safe arithmetic operations via the proven CLI. -# -# All computation is performed by the proven CLI binary, which delegates to -# the Idris 2 formally verified implementation through the Zig FFI bridge. -# No arithmetic logic is reimplemented in Nix. -# -# Each function invokes `proven math ` and parses the -# output. On error (overflow, division by zero, etc.), null is returned. -# -# Usage: -# let math = import ./safe-math.nix { inherit pkgs proven-cli; }; -# in math.addChecked 100 200 # "300" -# math.divSafe 10 0 # null (division by zero) -# math.clamp 0 100 150 # "100" - -{ pkgs, proven-cli }: - -let - # Run a proven math subcommand and return the result as a string. - # Returns null if the operation fails (overflow, division by zero, etc.). - runMath = subcommand: args: - let - argStr = builtins.concatStringsSep " " (map toString args); - result = pkgs.runCommand "proven-math-${subcommand}" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven math ${subcommand} ${argStr} > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.replaceStrings ["\n"] [""] (builtins.readFile result); - in - if output == "" then null else output; - -in { - # Checked addition with overflow detection. - # Returns the sum as a string, or null on overflow. - addChecked = a: b: runMath "add-checked" [ a b ]; - - # Checked subtraction with underflow detection. - # Returns the difference as a string, or null on underflow. - subChecked = a: b: runMath "sub-checked" [ a b ]; - - # Checked multiplication with overflow detection. - # Returns the product as a string, or null on overflow. - mulChecked = a: b: runMath "mul-checked" [ a b ]; - - # Safe division with zero-check. - # Returns the quotient as a string, or null on division by zero. - divSafe = numerator: denominator: runMath "div" [ numerator denominator ]; - - # Safe modulo with zero-check. - # Returns the remainder as a string, or null on division by zero. - modSafe = numerator: denominator: runMath "mod" [ numerator denominator ]; - - # Safe absolute value. - # Returns the absolute value as a string, or null for INT64_MIN. - absSafe = n: runMath "abs" [ n ]; - - # Clamp a value to the range [lo, hi]. - # Always succeeds. - clamp = lo: hi: value: runMath "clamp" [ lo hi value ]; - - # Integer exponentiation with overflow checking. - # Returns base^exp as a string, or null on overflow. - powChecked = base: exp: runMath "pow-checked" [ base exp ]; - - # Module metadata - _meta = { - name = "safe-math"; - description = "Safe arithmetic operations via proven CLI"; - functions = [ - "addChecked" "subChecked" "mulChecked" "divSafe" - "modSafe" "absSafe" "clamp" "powChecked" - ]; - }; -} diff --git a/bindings/nix/lib/safe-path.nix b/bindings/nix/lib/safe-path.nix deleted file mode 100644 index 3b48fc5b..00000000 --- a/bindings/nix/lib/safe-path.nix +++ /dev/null @@ -1,75 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# safe-path.nix -- Safe filesystem path operations via the proven CLI. -# -# All computation is performed by the proven CLI binary, which delegates to -# the Idris 2 formally verified implementation through the Zig FFI bridge. -# No path validation or sanitization logic is reimplemented in Nix. -# -# These functions are particularly useful in Nix derivations that accept -# user-supplied filenames, preventing directory traversal attacks. -# -# Usage: -# let path = import ./safe-path.nix { inherit pkgs proven-cli; }; -# in path.hasTraversal "../../../etc/passwd" # true -# path.sanitizeFilename "../../malicious.sh" # "malicious.sh" - -{ pkgs, proven-cli }: - -let - # Run a proven path subcommand with a single path argument. - # Returns the CLI output as a string, or null on error. - runPath = subcommand: input: - let - inputFile = pkgs.writeText "proven-path-input" input; - result = pkgs.runCommand "proven-path-${subcommand}" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven path ${subcommand} --file ${inputFile} > $out 2>/dev/null; then - true - elif proven path ${subcommand} "$(cat ${inputFile})" > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.readFile result; - trimmed = builtins.replaceStrings ["\n"] [""] output; - in - if trimmed == "" then null else trimmed; - - # Run a proven path subcommand that returns a boolean ("true"/"false"). - runPathBool = subcommand: input: - let - raw = runPath subcommand input; - in - if raw == "true" then true - else if raw == "false" then false - else null; - -in { - # Check if a path contains directory traversal sequences (".."). - # Returns true if traversal is detected, false otherwise, null on error. - hasTraversal = path: runPathBool "has-traversal" path; - - # Sanitize a filename by removing dangerous characters. - # Strips path separators, "..", null bytes, and control characters. - # Returns sanitized filename as string, or null on error. - sanitizeFilename = filename: runPath "sanitize-filename" filename; - - # Convenience: check that a path is safe (no traversal detected). - # Returns true if the path is safe, false if traversal is detected. - isSafe = path: - let result = runPathBool "has-traversal" path; - in if result == true then false - else if result == false then true - else null; - - # Module metadata - _meta = { - name = "safe-path"; - description = "Safe filesystem path operations via proven CLI"; - functions = [ "hasTraversal" "sanitizeFilename" "isSafe" ]; - }; -} diff --git a/bindings/nix/lib/safe-string.nix b/bindings/nix/lib/safe-string.nix deleted file mode 100644 index eca3cf70..00000000 --- a/bindings/nix/lib/safe-string.nix +++ /dev/null @@ -1,76 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# safe-string.nix -- Safe string operations via the proven CLI. -# -# All computation is performed by the proven CLI binary, which delegates to -# the Idris 2 formally verified implementation through the Zig FFI bridge. -# No string escaping or validation logic is reimplemented in Nix. -# -# Each function invokes `proven string ` and parses the -# output. On error, null is returned. -# -# Usage: -# let str = import ./safe-string.nix { inherit pkgs proven-cli; }; -# in str.escapeHtml "" -# str.escapeSql "O'Brien" -# str.isValidUtf8 "hello" - -{ pkgs, proven-cli }: - -let - # Run a proven string subcommand with a single string argument. - # Returns the CLI output as a string, or null on error. - runString = subcommand: input: - let - # Write input to a file to avoid shell escaping issues - inputFile = pkgs.writeText "proven-string-input" input; - result = pkgs.runCommand "proven-string-${subcommand}" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven string ${subcommand} --file ${inputFile} > $out 2>/dev/null; then - true - elif proven string ${subcommand} "$(cat ${inputFile})" > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.readFile result; - trimmed = builtins.replaceStrings ["\n"] [""] output; - in - if trimmed == "" then null else trimmed; - - # Run a proven string subcommand that returns a boolean ("true"/"false"). - runStringBool = subcommand: input: - let - raw = runString subcommand input; - in - if raw == "true" then true - else if raw == "false" then false - else null; - -in { - # Check if a byte sequence is valid UTF-8. - # Returns true/false, or null on error. - isValidUtf8 = input: runStringBool "is-valid-utf8" input; - - # Escape a string for safe use in SQL queries. - # Doubles single quotes. Returns escaped string, or null on error. - escapeSql = input: runString "escape-sql" input; - - # Escape a string for safe use in HTML. - # Escapes <, >, &, ", and ' characters. Returns escaped string, or null on error. - escapeHtml = input: runString "escape-html" input; - - # Escape a string for safe use in JavaScript string literals. - # Returns escaped string, or null on error. - escapeJs = input: runString "escape-js" input; - - # Module metadata - _meta = { - name = "safe-string"; - description = "Safe string operations via proven CLI"; - functions = [ "isValidUtf8" "escapeSql" "escapeHtml" "escapeJs" ]; - }; -} diff --git a/bindings/nix/lib/safe-validators.nix b/bindings/nix/lib/safe-validators.nix deleted file mode 100644 index d816c9c7..00000000 --- a/bindings/nix/lib/safe-validators.nix +++ /dev/null @@ -1,159 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -# safe-validators.nix -- Email, URL, IPv4, and JSON validators via the proven CLI. -# -# All computation is performed by the proven CLI binary, which delegates to -# the Idris 2 formally verified implementation through the Zig FFI bridge. -# No validation logic is reimplemented in Nix. -# -# These functions are useful for validating configuration values in Nix -# expressions (e.g., NixOS module options, flake inputs, derivation args). -# -# Usage: -# let v = import ./safe-validators.nix { inherit pkgs proven-cli; }; -# in v.isValidEmail "user@example.com" # true -# v.isValidEmail "not-an-email" # false -# v.isValidIpv4 "192.168.1.1" # true -# v.isValidJson "{\"key\": \"value\"}" # true - -{ pkgs, proven-cli }: - -let - # Run a proven subcommand with a string input and return a boolean. - # Returns true/false as Nix boolean, or null on error. - runValidateBool = module: subcommand: input: - let - inputFile = pkgs.writeText "proven-validate-input" input; - result = pkgs.runCommand "proven-validate-${subcommand}" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven ${module} ${subcommand} --file ${inputFile} > $out 2>/dev/null; then - true - elif proven ${module} ${subcommand} "$(cat ${inputFile})" > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.replaceStrings ["\n"] [""] (builtins.readFile result); - in - if output == "true" then true - else if output == "false" then false - else null; - - # Run a proven subcommand and return the raw string output. - runValidateString = module: subcommand: input: - let - inputFile = pkgs.writeText "proven-validate-input" input; - result = pkgs.runCommand "proven-validate-${subcommand}" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven ${module} ${subcommand} --file ${inputFile} > $out 2>/dev/null; then - true - elif proven ${module} ${subcommand} "$(cat ${inputFile})" > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.replaceStrings ["\n"] [""] (builtins.readFile result); - in - if output == "" then null else output; - -in { - # -------------------------------------------------------------------------- - # Email validation (RFC 5321 simplified) - # -------------------------------------------------------------------------- - - # Validate an email address. - # Returns true if valid, false if invalid, null on error. - isValidEmail = email: runValidateBool "email" "is-valid" email; - - # -------------------------------------------------------------------------- - # URL parsing and validation - # -------------------------------------------------------------------------- - - # Parse a URL and return the scheme, or null if invalid. - parseUrlScheme = url: runValidateString "url" "parse-scheme" url; - - # Parse a URL and return the host, or null if invalid. - parseUrlHost = url: runValidateString "url" "parse-host" url; - - # -------------------------------------------------------------------------- - # IPv4 validation - # -------------------------------------------------------------------------- - - # Validate an IPv4 address string (e.g., "192.168.1.1"). - # Returns true if valid, false if invalid, null on error. - isValidIpv4 = addr: runValidateBool "network" "parse-ipv4" addr; - - # Check if an IPv4 address is private (RFC 1918). - # Returns true/false, or null on error. - isPrivateIpv4 = addr: runValidateBool "network" "is-private" addr; - - # Check if an IPv4 address is loopback (127.0.0.0/8). - # Returns true/false, or null on error. - isLoopbackIpv4 = addr: runValidateBool "network" "is-loopback" addr; - - # -------------------------------------------------------------------------- - # JSON validation - # -------------------------------------------------------------------------- - - # Check if a string is valid JSON. - # Returns true/false, or null on error. - isValidJson = input: runValidateBool "json" "is-valid" input; - - # Get the JSON root value type ("null", "bool", "number", "string", - # "array", "object", or "invalid"). - # Returns the type as a string, or null on error. - jsonType = input: runValidateString "json" "get-type" input; - - # -------------------------------------------------------------------------- - # DateTime validation (ISO 8601) - # -------------------------------------------------------------------------- - - # Parse an ISO 8601 datetime string and return formatted output. - # Returns the formatted datetime, or null on parse failure. - parseDatetime = input: runValidateString "datetime" "parse" input; - - # Check if a year is a leap year. - # Returns true/false, or null on error. - isLeapYear = year: - let - result = pkgs.runCommand "proven-is-leap-year" { - nativeBuildInputs = [ proven-cli ]; - } '' - if proven datetime is-leap-year ${toString year} > $out 2>/dev/null; then - true - else - echo "" > $out - fi - ''; - output = builtins.replaceStrings ["\n"] [""] (builtins.readFile result); - in - if output == "true" then true - else if output == "false" then false - else null; - - # -------------------------------------------------------------------------- - # Version parsing (SemVer) - # -------------------------------------------------------------------------- - - # Parse a semantic version string (e.g., "1.2.3-alpha"). - # Returns the normalized version string, or null on parse failure. - parseVersion = input: runValidateString "version" "parse" input; - - # Module metadata - _meta = { - name = "safe-validators"; - description = "Email, URL, IPv4, JSON, datetime, and version validators via proven CLI"; - functions = [ - "isValidEmail" "parseUrlScheme" "parseUrlHost" - "isValidIpv4" "isPrivateIpv4" "isLoopbackIpv4" - "isValidJson" "jsonType" - "parseDatetime" "isLeapYear" - "parseVersion" - ]; - }; -} diff --git a/nix/shard.nix b/nix/shard.nix deleted file mode 100644 index 5be405be..00000000 --- a/nix/shard.nix +++ /dev/null @@ -1,14 +0,0 @@ -{ pkgs ? import (builtins.fetchGit { - url = "https://github.com/NixOS/nixpkgs.git"; - rev = "be5afa0fcb31f0a96bf9ecba05a516c66fcd8114"; - }) {} }: - -pkgs.mkShell { - packages = with pkgs; [ - idris2 - zig - git - gnumake - pkg-config - ]; -}