From a27d78b591ab8c79354ccfeeee9ab53f4f63abc6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 11:20:21 +0100 Subject: [PATCH] Delete the six duplicated src/abi/*.idr modules and repoint every reference Closes #815. src/abi/hypatia-abi.ipkg sets `sourcedir = ".."`, which resolves to src/, so the modules it compiles are src/Hypatia/ABI/*.idr. A byte-identical copy of all six sat in src/abi/, compiled by nothing. Divergence between the two was undetectable -- DEBT-REGISTER C-4, now marked RESOLVED. Proven lossless before deleting: five of the six blobs were byte-identical across the two directories, and the dead Types.idr blob 40d2ed6c is a strict ancestor revision of the live 788493e6 (the live copy carries #120's authority-direction correction on top). Nothing is lost that is not already in the live module's history. Both .ipkg files and README.adoc stay, so src/abi/ still exists and `idris2 --build src/abi/hypatia-abi.ipkg` is unaffected -- verified: it builds all 6 modules from ../Hypatia/ABI/, which is the direct proof the deleted copies were never compiled. The one functional consumer, and the vacuous gate behind it ----------------------------------------------------------- test/zig_ffi_smoke_test.exs asserted File.exists? on five src/abi/*.idr modules, so deleting them turned `mix test` red. Its sibling test listed the directory, filtered for .idr and asserted SPDX headers -- after deletion that list is empty and Enum.each over nothing passes, so it would have gone VACUOUS rather than red. Both are fixed: @abi_dir now points at src/Hypatia/ABI, the required-module list gains RuleEngine.idr and Gen.idr (it named only 5 of 7 -- a pre-existing coverage gap), and the SPDX test gets a non-empty denominator assertion. Mutant-tested: pointing @abi_dir at an empty directory now yields 2 failures including "no .idr files found", where before it would have yielded 1. This consumer was missed by every earlier sweep because it names the directory ("../src/abi") and the basenames (~w(Types.idr ...)) as separate tokens, so grepping the joined path never matched it. Other corrections ----------------- - .hypatia-exemptions.adoc cited an inline marker `hypatia:ignore ...` that does not exist; the real directive is `hypatia: allow ...`. The prose above it claimed the scanner has no directive recognition, which is false -- scanner_suppression.ex file_allowed?/4 implements it. Repoint only, no new row, so the Exemption ratchet sees no growth (6 insertions, 6 deletions). - docs/proofs/HANDOVER-neural-convergence.adoc asserted that src/abi/*.idr "are the real files" and src/Hypatia/ABI/*.idr "are symlinks into them" -- backwards, and they were never symlinks. - .github/CODEOWNERS owned /src/abi/ but nothing owned /src/Hypatia/ABI/, so the normative ABI was unowned. Added. - stapeln.toml [layers.abi-verify] cache-key was "src/abi/*.idr", which would have matched nothing and cached forever. Deliberately untouched ---------------------- - verification/PROOF-STATUS.adoc -- issue #816 ("stale: wrong path, wrong LOC, wrong proofs") owns the path column; two PRs editing the same six rows would conflict. Commented there instead. - test/unified-api-adapter-contract_test.exs:11 -- a past-tense note explaining why the guard was repointed by #120. Still historically true. - verify-proofs.yml paths:, CODEOWNERS /src/abi/, Justfile compile-abi and abi-gen, pack.toml, src/README.adoc -- all reference the directory or the ipkgs, both of which survive. Verification ------------ - mix test: 1593 tests, 2 failures -- both pre-existing, proven by running test/research_extensions_test.exs at stock 86aa936 content (same 2). - just abi-gen: "connectors emitted: 16 / files written: 3 of 3", zero diff against the tracked generated files. - tests.yml dangerous-pattern denominator: 13 -> 7, still non-zero. - The scanner's `-- hypatia: allow code_safety/believe_me structural_drift/SD008` marker survives at line 19 of the live RuleEngine copy, matching what the exemptions ledger cites. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- .claude/CLAUDE.md | 6 +- .github/CODEOWNERS | 1 + .github/workflows/tests.yml | 2 +- .hypatia-exemptions.adoc | 12 +- Justfile | 2 +- clients/rust/hypatia-client/src/ffi.rs | 2 +- clients/rust/hypatia-client/src/lib.rs | 2 +- clients/rust/hypatia-client/src/types.rs | 2 +- docs/DEBT-REGISTER.adoc | 11 +- docs/governance/CRG-AUDIT-2026-04-18.adoc | 2 +- docs/operations/prover-wars-integration.adoc | 6 +- docs/proofs/HANDOVER-neural-convergence.adoc | 10 +- docs/proofs/needs.adoc | 2 +- ffi/README.adoc | 2 +- ffi/zig/README.adoc | 2 +- ffi/zig/src/main.zig | 2 +- lib/hypatia/scanner_suppression.ex | 2 +- schema/README.adoc | 2 +- src/abi/FFI.idr | 66 -- src/abi/GRPC.idr | 64 -- src/abi/GraphQL.idr | 93 --- src/abi/README.adoc | 46 +- src/abi/REST.idr | 95 --- src/abi/RuleEngine.idr | 569 ------------------ src/abi/Types.idr | 242 -------- stapeln.toml | 2 +- test/merge_orchestration/sensor_test.exs | 2 +- test/zig_ffi_smoke_test.exs | 29 +- .../proofs/idris2/ConfidenceBounds.idr | 2 +- .../proofs/idris2/DispatchStrategy.idr | 2 +- verification/proofs/idris2/SafetyTriangle.idr | 2 +- 31 files changed, 100 insertions(+), 1184 deletions(-) delete mode 100644 src/abi/FFI.idr delete mode 100644 src/abi/GRPC.idr delete mode 100644 src/abi/GraphQL.idr delete mode 100644 src/abi/REST.idr delete mode 100644 src/abi/RuleEngine.idr delete mode 100644 src/abi/Types.idr diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index c99eeace..9832cccc 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -174,9 +174,9 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa | `RuleEngine.idr` | Rule-evaluation types | **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager). -The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles**. A byte-identical -copy of all six modules also sits in `src/abi/*.idr` and is built by nothing — divergence between -them is undetectable. See DEBT-REGISTER C-4. +The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the +normative ABI. `src/abi/` holds only the two `.ipkg` files and a README; the byte-identical +duplicate modules that used to sit there were deleted 2026-09-22 (issue #815, DEBT-REGISTER C-4). ### Zig FFI (ffi/zig/src/) diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 7605321b..1a719583 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -18,6 +18,7 @@ # ABI/FFI layer /src/abi/ @hyperpolymath +/src/Hypatia/ABI/ @hyperpolymath /ffi/zig/ @hyperpolymath # Neural / scanning engine diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 3fb9a47c..68b395db 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -146,7 +146,7 @@ jobs: # strings, not as actual escape hatches). # `grep -v '^\s*--'` strips Idris2 / Haskell line comments, which # legitimately mention these tokens as documentation - # ("Zero believe_me." in src/abi/RuleEngine.idr is the canonical + # ("Zero believe_me." in src/Hypatia/ABI/RuleEngine.idr is the canonical # example). DANGEROUS=$(find lib src \( -name '*.idr' -o -name '*.v' -o -name '*.lean' -o -name '*.hs' \) \ -not -path 'lib/rules/*' \ diff --git a/.hypatia-exemptions.adoc b/.hypatia-exemptions.adoc index ce5f7296..d02a97fa 100644 --- a/.hypatia-exemptions.adoc +++ b/.hypatia-exemptions.adoc @@ -10,19 +10,19 @@ matching its tuple) — the difference: the baseline is a quantitative snapshot (regenerable from any scan), this table is the qualitative justification (curated by humans). -When the scanner gains support for inline `+hypatia:ignore+` directives -(see `+lib/rules/+` — currently regex-pattern-based, no directive -recognition yet), the rows below should map 1:1 to the inline comments -already placed at each file’s site. +The scanner recognises inline `+hypatia: allow /+` directives +(see `+lib/hypatia/scanner_suppression.ex+`, `+file_allowed?/4+`, which scans a +file's first `+:max_header_lines+` lines). The rows below map 1:1 to the +inline comments already placed at each file's site. === Currently accepted findings [width="100%",cols="20%,20%,20%,20%,20%",options="header",] |=== |File |Rule |Inline marker |Rationale |Revisit when -|`+src/abi/RuleEngine.idr+` |`+code_safety/believe_me+`, +|`+src/Hypatia/ABI/RuleEngine.idr+` |`+code_safety/believe_me+`, `+structural_drift/SD008+` -|`+-- hypatia:ignore code_safety/believe_me structural_drift/SD008+` +|`+-- hypatia: allow code_safety/believe_me structural_drift/SD008+` (line 19) |The scanner is counting the literal token `+believe_me+` inside an Idris2 comment that asserts there are _no_ such primitives. There is no actual `+believe_me+` call site in the module. |The scanner diff --git a/Justfile b/Justfile index d7b5545b..63c88dc2 100644 --- a/Justfile +++ b/Justfile @@ -310,7 +310,7 @@ tour: echo " Rust crates for adapters, CLI tools, data processing, fixes." echo "" echo "5. ABI/FFI:" - echo " src/abi/ - Idris2 types (GraphQL, gRPC, REST proofs)" + echo " src/abi/ - Idris2 ABI + codegen packages (.ipkg)" echo " ffi/zig/ - 7 exported C functions" echo "" echo "6. SAFETY SYSTEMS: lib/safety/" diff --git a/clients/rust/hypatia-client/src/ffi.rs b/clients/rust/hypatia-client/src/ffi.rs index 31aab82d..c990fd0e 100644 --- a/clients/rust/hypatia-client/src/ffi.rs +++ b/clients/rust/hypatia-client/src/ffi.rs @@ -22,7 +22,7 @@ // 2. `lib.get(b"hypatia_*\0")` — symbol lookup is unsafe because the // caller asserts the type signature. Each lookup matches the exact // `extern "C"` signature exported by `main.zig` and pinned by the -// Idris2 ABI dependent-type proofs in `src/abi/Types.idr`. Renumbering +// Idris2 ABI dependent-type proofs in `src/Hypatia/ABI/Types.idr`. Renumbering // the Connector enum or changing any exported function's signature // breaks the build at the Idris2 layer first. // diff --git a/clients/rust/hypatia-client/src/lib.rs b/clients/rust/hypatia-client/src/lib.rs index 26e73d0f..6a574872 100644 --- a/clients/rust/hypatia-client/src/lib.rs +++ b/clients/rust/hypatia-client/src/lib.rs @@ -20,7 +20,7 @@ // REST, FlatBuffers, Bebop, JSON-RPC, WebSocket, MQTT, tRPC, // Cap'n Proto, SOAP, VeriSimDB-REST, BSP, SCIP, IPFS, Arrow Flight) // lives on the Zig side at `hypatia/ffi/zig/src/unified-api-adapter.zig` and is -// mirrored by the Idris2 ABI in `src/abi/Types.idr`. The Rust client +// mirrored by the Idris2 ABI in `src/Hypatia/ABI/Types.idr`. The Rust client // knows about all sixteen via `Connector` so that future enumeration // and dispatch endpoints (`hypatia_connector_count`, // `hypatia_connector_name`, `hypatia_unified_api_adapter_start_all`) are diff --git a/clients/rust/hypatia-client/src/types.rs b/clients/rust/hypatia-client/src/types.rs index 63798ae3..4ebd38a4 100644 --- a/clients/rust/hypatia-client/src/types.rs +++ b/clients/rust/hypatia-client/src/types.rs @@ -3,7 +3,7 @@ // // Hypatia client types — the typed surface that replaces the // V-lang client at the deleted `api/v/hypatia.v`. Mirrors the -// Idris2 ABI types in `src/abi/Types.idr` and the Zig ABI types +// Idris2 ABI types in `src/Hypatia/ABI/Types.idr` and the Zig ABI types // in `ffi/zig/src/main.zig`. use serde::{Deserialize, Serialize}; diff --git a/docs/DEBT-REGISTER.adoc b/docs/DEBT-REGISTER.adoc index 877dfa26..4eee2c3d 100644 --- a/docs/DEBT-REGISTER.adoc +++ b/docs/DEBT-REGISTER.adoc @@ -274,12 +274,15 @@ CI-1). So no human or machine has seen a clippy result recently. `+cargo fmt --all --check+` passes and `+Cargo.lock+` is in sync. *To verify:* re-run with a warm `+target/+` (~15-20 min). -==== C-4 · MEDIUM · Idris ABI sources duplicated byte-for-byte · UNTRACKED +==== C-4 · MEDIUM · Idris ABI sources duplicated byte-for-byte · RESOLVED -`+src/Hypatia/ABI/*.idr+` and `+src/abi/*.idr+` — all 6 pairs identical. +`+src/Hypatia/ABI/*.idr+` and `+src/abi/*.idr+` were all 6 pairs identical. `+src/abi/hypatia-abi.ipkg+` sets `+sourcedir = ".."+`, so -*`+src/Hypatia/ABI/+` is what compiles* and `+src/abi/*.idr+` is a dead -copy nothing builds. Divergence between them is undetectable today. +*`+src/Hypatia/ABI/+` is what compiles* and `+src/abi/*.idr+` was a dead +copy nothing built, whose divergence would have been undetectable. +*Resolved 2026-09-22 (issue #815):* the six dead modules are deleted; only +`+hypatia-abi.ipkg+`, `+hypatia-abi-gen.ipkg+` and `+README.adoc+` remain in +`+src/abi/+`. ==== C-5 · LOW · One orphaned module · UNTRACKED diff --git a/docs/governance/CRG-AUDIT-2026-04-18.adoc b/docs/governance/CRG-AUDIT-2026-04-18.adoc index 1e94af98..93ae9271 100644 --- a/docs/governance/CRG-AUDIT-2026-04-18.adoc +++ b/docs/governance/CRG-AUDIT-2026-04-18.adoc @@ -133,7 +133,7 @@ hits, contractile trident complete, full mirror fan-out configured. |=== | Item | Count | Notes -| Idris2 ABI modules (`src/abi/*.idr`) +| Idris2 ABI modules (`src/Hypatia/ABI/*.idr`) | 6 files, 1,128 LOC | `Types.idr` 240, `REST.idr` 95, `GraphQL.idr` 93, `FFI.idr` 66, `GRPC.idr` 64, `RuleEngine.idr` 570. All declare `%default total` at file head. diff --git a/docs/operations/prover-wars-integration.adoc b/docs/operations/prover-wars-integration.adoc index 62b37d0a..82dfc9cd 100644 --- a/docs/operations/prover-wars-integration.adoc +++ b/docs/operations/prover-wars-integration.adoc @@ -91,7 +91,7 @@ Estimated 400–600 LOC including tests. === ABI additions -In `src/abi/Types.idr`: +In `src/Hypatia/ABI/Types.idr`: [source,idris] ---- @@ -113,8 +113,8 @@ record ProofResult where timestamp : String ---- -Add equivalent gRPC + REST endpoint definitions in `src/abi/GRPC.idr` -and `src/abi/REST.idr`. +Add equivalent gRPC + REST endpoint definitions in `src/Hypatia/ABI/GRPC.idr` +and `src/Hypatia/ABI/REST.idr`. === Telemetry diff --git a/docs/proofs/HANDOVER-neural-convergence.adoc b/docs/proofs/HANDOVER-neural-convergence.adoc index c1d2e056..bc4064cc 100644 --- a/docs/proofs/HANDOVER-neural-convergence.adoc +++ b/docs/proofs/HANDOVER-neural-convergence.adoc @@ -57,7 +57,7 @@ assertion; Agda retired) |✅ |parser totality |`+verification/proofs/lean4/ParserTotality.lean+` |✅ -|ABI package + verify package |`+src/abi/*.idr+` +|ABI package + verify package |`+src/Hypatia/ABI/*.idr+` (incl. `+RuleEngine.idr+`), `+verify/src/*.idr+` |✅ |*Neural convergence — PageRank* @@ -185,8 +185,10 @@ cd verification/proofs/tlaplus && java -cp /path/tla2tools.jar tlc2.TLC -config instance to lean on). * Idris reserved words used as identifiers were the bug class: `+data+`, `+record+`, `+partial+`. -* `+src/abi/*.idr+` are the real files; `+src/Hypatia/ABI/*.idr+` are -*symlinks* into them (build namespace `+Hypatia.ABI.*+`). +* `+src/Hypatia/ABI/*.idr+` are the real files (build namespace +`+Hypatia.ABI.*+`, reached via `+sourcedir = ".."+` in the ipkg). They were +never symlinks: `+src/abi/*.idr+` held byte-identical duplicate files that +nothing compiled, deleted 2026-09-22 (issue #815). === Definition of done @@ -203,5 +205,5 @@ instance to lean on). Repo-hygiene PR (173 medium scan findings: `+timeout-minutes+` on `+ci.yml+`/`+clusterfuzzlite.yml+`, the `+setup-java+` SHA-pin false-positive); `+PipelineState+`→real `+proven+` integration; -documenting the `+src/abi+` symlink layout; the `+gitbot-fleet+` / +documenting the `+src/Hypatia/ABI+` layout; the `+gitbot-fleet+` / `+.git-private-farm+` repos. diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index a24a4ca8..7246aaee 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -2,7 +2,7 @@ === Current State (Updated 2026-06-05) -* **src/abi/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`, +* **src/Hypatia/ABI/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`, `+GRPC.idr+`, `+REST.idr+`, `+RuleEngine.idr+` — built as the `+hypatia-abi+` package under `+--total+`. * **verify/src/*.idr**: `+PipelineState.idr+`, `+Verify/Fuel.idr+` — diff --git a/ffi/README.adoc b/ffi/README.adoc index 06de4b1c..f093a5e0 100644 --- a/ffi/README.adoc +++ b/ffi/README.adoc @@ -5,7 +5,7 @@ C-compatible FFI bridge between the Idris2 ABI and consuming runtimes. == zig/ -Zig implementation of the 7 documented C ABI functions declared in `src/abi/FFI.idr`. +Zig implementation of the 7 documented C ABI functions declared in `src/Hypatia/ABI/FFI.idr`. Produces a shared library (`libhypatia_ffi.so`) loadable as an Erlang NIF or via `dlopen`. See link:zig/README.adoc[zig/README.adoc] for build instructions and function reference. diff --git a/ffi/zig/README.adoc b/ffi/zig/README.adoc index 64b21768..6a695ece 100644 --- a/ffi/zig/README.adoc +++ b/ffi/zig/README.adoc @@ -74,7 +74,7 @@ renumbered. Port layout is `base + id + 1` (`UnifiedApiAdapter.portFor`). The connector set is mirrored in three places that *must agree*: * Zig — `ffi/zig/src/unified-api-adapter.zig` (`Connector` enum + `comptime` count assertion) -* Idris2 — `src/abi/Types.idr` (`Connector` + the `connectorCount = Refl` proof) +* Idris2 — `src/Hypatia/ABI/Types.idr` (`Connector` + the `connectorCount = Refl` proof) * Rust — `clients/rust/hypatia-client/src/connector.rs` (`#[repr(u8)]` enum) `ffi/connectors.json` is the *golden source-of-truth*, and diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index 8f8742ea..b0f28473 100644 --- a/ffi/zig/src/main.zig +++ b/ffi/zig/src/main.zig @@ -28,7 +28,7 @@ fn clearError() void { } //============================================================================== -// Core Types (must match src/abi/Types.idr) +// Core Types (must match src/Hypatia/ABI/Types.idr) //============================================================================== /// Result codes (must match Idris2 Result type) diff --git a/lib/hypatia/scanner_suppression.ex b/lib/hypatia/scanner_suppression.ex index 2fc9ec02..ce2b8530 100644 --- a/lib/hypatia/scanner_suppression.ex +++ b/lib/hypatia/scanner_suppression.ex @@ -321,7 +321,7 @@ defmodule Hypatia.ScannerSuppression do File-level allow directive: any of the first `:max_header_lines` (default 20) of the file may include a `hypatia: allow /` directive that suppresses *every* matching finding in the file. Used for files like - `src/abi/RuleEngine.idr` which contain intentional `believe_me` usage and + `src/Hypatia/ABI/RuleEngine.idr` which contain intentional `believe_me` usage and want to declare the allowance once at the top. """ def file_allowed?(content, rule_module, rule_type, opts \\ []) do diff --git a/schema/README.adoc b/schema/README.adoc index 29d327ee..808d0c12 100644 --- a/schema/README.adoc +++ b/schema/README.adoc @@ -9,4 +9,4 @@ Nickel configuration schemas for Hypatia data structures. * `generate-findings.ncl` — Generator helpers for findings in tests and tooling These schemas are used for configuration validation and test fixture generation. -The authoritative type definitions are in `src/abi/Types.idr`. +The authoritative type definitions are in `src/Hypatia/ABI/Types.idr`. diff --git a/src/abi/FFI.idr b/src/abi/FFI.idr deleted file mode 100644 index 4d40bd65..00000000 --- a/src/abi/FFI.idr +++ /dev/null @@ -1,66 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- FFI function type signatures for the Zig C ABI bridge. --- Each constructor in FFIFunction declares a typed foreign function. --- Links to REST endpoint definitions for type-level verification. - -module Hypatia.ABI.FFI - -import Hypatia.ABI.Types -import Hypatia.ABI.REST - -%default total - -||| C ABI return code: 0 = success, non-zero = error -public export -CResult : Type -CResult = Int - -||| Foreign function declaration linking Zig export name to Idris2 types. -||| Each constructor corresponds to an `export fn` in ffi/zig/src/main.zig. -public export -data FFIFunction : Type where - ||| Health check — reads verisim-data dirs, counts files, returns JSON. - ||| Corresponds to: GET /health, GET /status - HealthCheck : FFIFunction - - ||| Scan repo — reads scans/{repo}.json, returns scan result. - ||| Corresponds to: GET /api/v1/scans/:repo - ScanRepo : (repo : String) -> FFIFunction - - ||| Dispatch finding — appends to dispatch/pending.jsonl. - ||| Corresponds to: POST /api/v1/dispatch - Dispatch : (entry : DispatchEntry) -> FFIFunction - - ||| Record outcome — appends to outcomes/YYYY-MM.jsonl. - ||| Corresponds to: POST /api/v1/outcomes - RecordOutcome : (outcome : OutcomeRecord) -> FFIFunction - - ||| Force learning cycle — writes .force-learning signal file. - ||| Corresponds to: POST /api/v1/learning/force - ForceLearningCycle : FFIFunction - - ||| Get confidence — reads recipes/recipe-*.json, extracts confidence. - ||| Corresponds to: GET /api/v1/recipes/:id (confidence field) - GetConfidence : (recipeId : String) -> FFIFunction - -||| Return type of each FFI function -public export -ffiReturnType : FFIFunction -> Type -ffiReturnType HealthCheck = ApiResponse HealthStatus -ffiReturnType (ScanRepo _) = ApiResponse ScanResult -ffiReturnType (Dispatch _) = ApiResponse () -ffiReturnType (RecordOutcome _) = ApiResponse () -ffiReturnType ForceLearningCycle = ApiResponse () -ffiReturnType (GetConfidence _) = ApiResponse Confidence - -||| Proof that every FFI function returns an ApiResponse-wrapped type -public export -ffiReturnsApiResponse : (f : FFIFunction) -> (a : Type ** ffiReturnType f = ApiResponse a) -ffiReturnsApiResponse HealthCheck = (HealthStatus ** Refl) -ffiReturnsApiResponse (ScanRepo _) = (ScanResult ** Refl) -ffiReturnsApiResponse (Dispatch _) = (() ** Refl) -ffiReturnsApiResponse (RecordOutcome _) = (() ** Refl) -ffiReturnsApiResponse ForceLearningCycle = (() ** Refl) -ffiReturnsApiResponse (GetConfidence _) = (Confidence ** Refl) diff --git a/src/abi/GRPC.idr b/src/abi/GRPC.idr deleted file mode 100644 index 0aa47cc2..00000000 --- a/src/abi/GRPC.idr +++ /dev/null @@ -1,64 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Hypatia ABI — gRPC Service Definitions --- Defines the gRPC service contract as dependent types. --- Maps to protobuf service definitions via the FFI layer. - -module Hypatia.ABI.GRPC - -import Hypatia.ABI.Types - -%default total - -||| gRPC method types -public export -data MethodType = Unary | ServerStream | ClientStream | BidiStream - -||| A gRPC method with typed request and response -public export -record GrpcMethod where - constructor MkGrpcMethod - name : String - methodType : MethodType - requestType : Type - responseType : Type - -||| Hypatia Scanner Service — unary RPCs for scanning and querying -public export -scannerService : List GrpcMethod -scannerService = - [ MkGrpcMethod "ScanRepo" Unary String (ApiResponse ScanResult) - , MkGrpcMethod "GetScanResult" Unary String (ApiResponse ScanResult) - , MkGrpcMethod "ListScans" Unary (Nat, Nat) (ApiResponse (List ScanResult)) - , MkGrpcMethod "SearchPatterns" Unary String (ApiResponse (List Pattern)) - ] - -||| Hypatia Dispatch Service — RPCs for fleet coordination -public export -dispatchService : List GrpcMethod -dispatchService = - [ MkGrpcMethod "DispatchFinding" Unary DispatchEntry (ApiResponse String) - , MkGrpcMethod "GetRecipe" Unary String (ApiResponse Recipe) - , MkGrpcMethod "ListRecipes" Unary Double (ApiResponse (List Recipe)) - , MkGrpcMethod "RecordOutcome" Unary OutcomeRecord (ApiResponse String) - , MkGrpcMethod "ForceLearningCycle" Unary () (ApiResponse Nat) - ] - -||| Hypatia Stream Service — server-streaming RPCs for monitoring -public export -streamService : List GrpcMethod -streamService = - [ MkGrpcMethod "StreamScans" ServerStream () ScanResult - , MkGrpcMethod "StreamOutcomes" ServerStream () OutcomeRecord - , MkGrpcMethod "StreamHealthChanges" ServerStream () (String, HealthStatus) - , MkGrpcMethod "StreamConfidenceChanges" ServerStream String (String, Double) - ] - -||| Hypatia Health Service — standard gRPC health check protocol -public export -healthService : List GrpcMethod -healthService = - [ MkGrpcMethod "Check" Unary String (ApiResponse HealthStatus) - , MkGrpcMethod "Watch" ServerStream String (ApiResponse HealthStatus) - ] diff --git a/src/abi/GraphQL.idr b/src/abi/GraphQL.idr deleted file mode 100644 index dc4a1839..00000000 --- a/src/abi/GraphQL.idr +++ /dev/null @@ -1,93 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Hypatia ABI — GraphQL Schema Definitions --- Defines the GraphQL operations as dependent types. --- The Zig FFI layer generates the actual GraphQL schema from these types. - -module Hypatia.ABI.GraphQL - -import Hypatia.ABI.Types - -%default total - -||| GraphQL query operations (read-only) -public export -data Query : Type -> Type where - ||| Get health status of all Hypatia components - HealthQuery : Query (ApiResponse (List (String, HealthStatus))) - - ||| Get scan results for a specific repository - ScanQuery : (repo : String) -> Query (ApiResponse ScanResult) - - ||| List all scanned repositories with pagination - ReposQuery : (offset : Nat) -> (limit : Nat) -> Query (ApiResponse (List ScanResult)) - - ||| Get a specific recipe by ID - RecipeQuery : (recipeId : String) -> Query (ApiResponse Recipe) - - ||| List all recipes with optional confidence filter - RecipesQuery : (minConfidence : Double) -> Query (ApiResponse (List Recipe)) - - ||| Get outcomes for a recipe - OutcomesQuery : (recipeId : String) -> Query (ApiResponse (List OutcomeRecord)) - - ||| Get patterns by severity - PatternsBySeverity : (severity : Severity) -> Query (ApiResponse (List Pattern)) - - ||| Search patterns by keyword - SearchPatterns : (keyword : String) -> Query (ApiResponse (List Pattern)) - -||| GraphQL mutation operations (write) -public export -data Mutation : Type -> Type where - ||| Trigger a scan for a repository - TriggerScan : (repo : String) -> Mutation (ApiResponse ScanResult) - - ||| Dispatch a finding to a fleet bot - DispatchFinding : (entry : DispatchEntry) -> Mutation (ApiResponse String) - - ||| Record a fix outcome (feeds the learning loop) - RecordOutcome : (outcome : OutcomeRecord) -> Mutation (ApiResponse String) - - ||| Force a learning cycle (normally automatic every 5 min) - ForceLearningCycle : Mutation (ApiResponse Nat) - - ||| Update recipe confidence manually - UpdateConfidence : (recipeId : String) -> Mutation (ApiResponse Double) - -||| GraphQL subscription operations (real-time) -public export -data Subscription : Type -> Type where - ||| Stream new scan results as they arrive - OnScanComplete : Subscription ScanResult - - ||| Stream outcome recordings (for monitoring) - OnOutcomeRecorded : Subscription OutcomeRecord - - ||| Stream confidence changes (for drift monitoring) - OnConfidenceChange : (recipeId : String) -> Subscription (String, Double) - - ||| Stream health status changes - OnHealthChange : Subscription (String, HealthStatus) - -||| Proof that all queries return ApiResponse-wrapped types -public export -queryReturnsApiResponse : (q : Query a) -> (b : Type ** a = ApiResponse b) -queryReturnsApiResponse HealthQuery = (_ ** Refl) -queryReturnsApiResponse (ScanQuery _) = (_ ** Refl) -queryReturnsApiResponse (ReposQuery _ _) = (_ ** Refl) -queryReturnsApiResponse (RecipeQuery _) = (_ ** Refl) -queryReturnsApiResponse (RecipesQuery _) = (_ ** Refl) -queryReturnsApiResponse (OutcomesQuery _) = (_ ** Refl) -queryReturnsApiResponse (PatternsBySeverity _) = (_ ** Refl) -queryReturnsApiResponse (SearchPatterns _) = (_ ** Refl) - -||| Proof that all mutations return ApiResponse-wrapped types -public export -mutationReturnsApiResponse : (m : Mutation a) -> (b : Type ** a = ApiResponse b) -mutationReturnsApiResponse (TriggerScan _) = (_ ** Refl) -mutationReturnsApiResponse (DispatchFinding _) = (_ ** Refl) -mutationReturnsApiResponse (RecordOutcome _) = (_ ** Refl) -mutationReturnsApiResponse ForceLearningCycle = (_ ** Refl) -mutationReturnsApiResponse (UpdateConfidence _) = (_ ** Refl) diff --git a/src/abi/README.adoc b/src/abi/README.adoc index 6608dc67..407bacd9 100644 --- a/src/abi/README.adoc +++ b/src/abi/README.adoc @@ -1,8 +1,16 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= src/abi/ — Idris2 ABI Definitions += src/abi/ — Idris2 ABI build packages -Idris2 modules defining the Hypatia API surface with dependent type proofs. -These are the authoritative interface definitions — all other layers derive from them. +This directory holds the Idris2 *package* files for the ABI. It no longer holds +any `.idr` module. + +Both packages set `sourcedir = ".."`, which resolves to `src/`, so the modules +they compile live in **`src/Hypatia/ABI/`** — that is the normative ABI, the +single source the wire contract is generated from. + +Until 2026-09-22 a byte-identical copy of all six ABI modules also sat in this +directory, compiled by nothing. Divergence between the two copies would have +been undetectable, so the dead copy was deleted (issue #815, DEBT-REGISTER C-4). == Files @@ -10,15 +18,33 @@ These are the authoritative interface definitions — all other layers derive fr |=== |File |Purpose -|`Types.idr` |Core types with dependent type proofs (Severity, TriangleTier, DispatchStrategy, etc.) -|`GraphQL.idr` |Query/Mutation/Subscription operations with proofs -|`GRPC.idr` |gRPC service definitions (scanner, dispatch, stream, health) -|`REST.idr` |REST endpoint definitions (18 endpoints, 6 groups) -|`FFI.idr` |GADT constructors for all 7 C ABI functions + `ffiReturnsApiResponse` proof -|`RuleEngine.idr` |Rule engine type definitions and proof obligations -|`hypatia-abi.ipkg` |Idris2 package file for compilation +|`hypatia-abi.ipkg` |Type-checks and builds the ABI modules (`Hypatia.ABI.*`) +|`hypatia-abi-gen.ipkg` |Builds `hypatia-abi-gen`, the generator that emits the Zig enum, the Rust enum and `ffi/connectors.json` from the ABI +|=== + +== The modules themselves + +[cols="2,3"] +|=== +|Module |Purpose + +|`src/Hypatia/ABI/Types.idr` |Core types with dependent type proofs (Severity, TriangleTier, DispatchStrategy, the 16-connector wire contract) +|`src/Hypatia/ABI/GraphQL.idr` |Query/Mutation/Subscription operations with proofs +|`src/Hypatia/ABI/GRPC.idr` |gRPC service definitions (scanner, dispatch, stream, health) +|`src/Hypatia/ABI/REST.idr` |REST endpoint definitions (18 endpoints, 6 groups) +|`src/Hypatia/ABI/FFI.idr` |GADT constructors for all 7 C ABI functions + `ffiReturnsApiResponse` proof +|`src/Hypatia/ABI/RuleEngine.idr` |Rule engine type definitions and proof obligations +|`src/Hypatia/ABI/Gen.idr` |The generator: evaluates the ABI and emits the generated mirrors |=== +== Build + +[source,bash] +---- +just compile-abi # idris2 --build src/abi/hypatia-abi.ipkg +just abi-gen # regenerate the Zig/Rust/JSON mirrors and write them in place +---- + == Key Proof `ffiReturnsApiResponse : (f : FFIFunction) -> (a : Type ** ffiReturnType f = ApiResponse a)` diff --git a/src/abi/REST.idr b/src/abi/REST.idr deleted file mode 100644 index b602b1f6..00000000 --- a/src/abi/REST.idr +++ /dev/null @@ -1,95 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Hypatia ABI — REST API Definitions --- Defines REST endpoints as dependent types. --- All endpoints return ApiResponse-wrapped typed responses. - -module Hypatia.ABI.REST - -import Hypatia.ABI.Types - -%default total - -||| HTTP methods -public export -data HttpMethod = GET | POST | PUT | DELETE | PATCH - -||| A REST endpoint with typed request body and response -public export -record Endpoint where - constructor MkEndpoint - method : HttpMethod - path : String - description : String - requestBody : Type - responseBody : Type - requiresAuth : Bool - -||| Health and status endpoints -public export -healthEndpoints : List Endpoint -healthEndpoints = - [ MkEndpoint GET "/health" "Overall health status" () (ApiResponse (List (String, HealthStatus))) False - , MkEndpoint GET "/status" "Detailed system status" () (ApiResponse (List (String, String))) False - , MkEndpoint GET "/metrics" "Prometheus-compatible metrics" () String False - ] - -||| Scanning endpoints -public export -scanEndpoints : List Endpoint -scanEndpoints = - [ MkEndpoint GET "/api/v1/scans/:repo" "Get scan results for a repo" () (ApiResponse ScanResult) False - , MkEndpoint GET "/api/v1/scans" "List all scan results" () (ApiResponse (List ScanResult)) False - , MkEndpoint POST "/api/v1/scans/:repo" "Trigger a new scan" () (ApiResponse ScanResult) True - ] - -||| Pattern endpoints -public export -patternEndpoints : List Endpoint -patternEndpoints = - [ MkEndpoint GET "/api/v1/patterns" "List all patterns" () (ApiResponse (List Pattern)) False - , MkEndpoint GET "/api/v1/patterns/:id" "Get pattern by ID" () (ApiResponse Pattern) False - , MkEndpoint GET "/api/v1/patterns/severity/:level" "Patterns by severity" () (ApiResponse (List Pattern)) False - , MkEndpoint GET "/api/v1/patterns/search" "Search patterns" () (ApiResponse (List Pattern)) False - ] - -||| Recipe endpoints -public export -recipeEndpoints : List Endpoint -recipeEndpoints = - [ MkEndpoint GET "/api/v1/recipes" "List all recipes" () (ApiResponse (List Recipe)) False - , MkEndpoint GET "/api/v1/recipes/:id" "Get recipe by ID" () (ApiResponse Recipe) False - , MkEndpoint PUT "/api/v1/recipes/:id/confidence" "Update confidence" Double (ApiResponse Double) True - ] - -||| Dispatch endpoints -public export -dispatchEndpoints : List Endpoint -dispatchEndpoints = - [ MkEndpoint POST "/api/v1/dispatch" "Dispatch finding to fleet" DispatchEntry (ApiResponse String) True - , MkEndpoint GET "/api/v1/dispatch/pending" "List pending dispatches" () (ApiResponse (List DispatchEntry)) False - , MkEndpoint GET "/api/v1/dispatch/history" "Dispatch history" () (ApiResponse (List DispatchEntry)) False - ] - -||| Outcome and learning endpoints -public export -outcomeEndpoints : List Endpoint -outcomeEndpoints = - [ MkEndpoint POST "/api/v1/outcomes" "Record fix outcome" OutcomeRecord (ApiResponse String) True - , MkEndpoint GET "/api/v1/outcomes/:recipe" "Outcomes for recipe" () (ApiResponse (List OutcomeRecord)) False - , MkEndpoint POST "/api/v1/learning/cycle" "Force learning cycle" () (ApiResponse Nat) True - , MkEndpoint GET "/api/v1/learning/status" "Learning scheduler status" () (ApiResponse (List (String, String))) False - ] - -||| All endpoints combined -public export -allEndpoints : List Endpoint -allEndpoints = - healthEndpoints ++ scanEndpoints ++ patternEndpoints ++ - recipeEndpoints ++ dispatchEndpoints ++ outcomeEndpoints - -||| Proof: total endpoint count -public export -totalEndpointCount : Nat -totalEndpointCount = length allEndpoints diff --git a/src/abi/RuleEngine.idr b/src/abi/RuleEngine.idr deleted file mode 100644 index 8ae645c8..00000000 --- a/src/abi/RuleEngine.idr +++ /dev/null @@ -1,569 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Hypatia ABI — Rule Engine Proofs --- --- Formal verification of the Hypatia rule engine invariants: --- 1. Rule totality: every finding maps to exactly one action --- 2. Confidence monotonicity: more evidence never decreases confidence --- 3. Safety triangle soundness: eliminate > substitute > control hierarchy --- 4. Dispatch correctness: findings route to the correct bot --- --- These proofs correspond to the Elixir modules: --- - lib/triangle_router.ex (TriangleRouter) --- - lib/fleet_dispatcher.ex (FleetDispatcher) --- - lib/confidence_annealing.ex (ConfidenceAnnealing) --- - lib/outcome_tracker.ex (OutcomeTracker) --- --- No proof-bypass primitives used. %default total throughout. --- hypatia: allow code_safety/believe_me structural_drift/SD008 --- (the existing finding was the scanner counting the literal token --- 'believe_me' (obfuscated here) inside an Idris2 comment that asserts --- there are no such primitives. There is no actual call site.) - -module Hypatia.ABI.RuleEngine - -import Hypatia.ABI.Types -import Data.So -import Data.Nat - -%default total - ------------------------------------------------------------------------- --- Section 1: Safety Triangle — Types and Ordering ------------------------------------------------------------------------- - -||| The safety triangle has a strict total order: -||| Eliminate > Substitute > Control -||| This mirrors the occupational-safety hierarchy of controls. -public export -data TriangleLT : TriangleTier -> TriangleTier -> Type where - ||| Eliminate is strictly preferred over Substitute - ElimGtSubst : TriangleLT Eliminate Substitute - ||| Eliminate is strictly preferred over Control - ElimGtCtrl : TriangleLT Eliminate Control - ||| Substitute is strictly preferred over Control - SubstGtCtrl : TriangleLT Substitute Control - -||| The triangle ordering is irreflexive: no tier is preferred over itself. -public export -triangleIrreflexive : TriangleLT t t -> Void -triangleIrreflexive ElimGtSubst impossible -triangleIrreflexive ElimGtCtrl impossible -triangleIrreflexive SubstGtCtrl impossible - -||| The triangle ordering is transitive. -public export -triangleTransitive : TriangleLT a b -> TriangleLT b c -> TriangleLT a c -triangleTransitive ElimGtSubst SubstGtCtrl = ElimGtCtrl - -||| Decision procedure: for any two distinct tiers, one is preferred. -public export -triangleCompare : (a : TriangleTier) -> (b : TriangleTier) - -> Either (a = b) (Either (TriangleLT a b) (TriangleLT b a)) -triangleCompare Eliminate Eliminate = Left Refl -triangleCompare Eliminate Substitute = Right (Left ElimGtSubst) -triangleCompare Eliminate Control = Right (Left ElimGtCtrl) -triangleCompare Substitute Eliminate = Right (Right ElimGtSubst) -triangleCompare Substitute Substitute = Left Refl -triangleCompare Substitute Control = Right (Left SubstGtCtrl) -triangleCompare Control Eliminate = Right (Right ElimGtCtrl) -triangleCompare Control Substitute = Right (Right SubstGtCtrl) -triangleCompare Control Control = Left Refl - ------------------------------------------------------------------------- --- Section 2: Rule Totality — Every Finding Gets Exactly One Action ------------------------------------------------------------------------- - -||| A routed action is tagged with exactly one triangle tier. -||| This mirrors the Elixir return of {:eliminate, recipe, pattern}, -||| {:substitute, recipe, pattern}, or {:control, pattern}. -public export -data RoutedAction : Type where - ||| Hazard can be removed entirely (recipe found, auto_fixable or proven) - RouteEliminate : (recipe : Recipe) -> (pattern : Pattern) -> RoutedAction - ||| Replace with a proven-safe module - RouteSubstitute : (recipe : Recipe) -> (pattern : Pattern) -> RoutedAction - ||| Add guards/documentation only (no safe fix available) - RouteControl : (pattern : Pattern) -> RoutedAction - -||| Extract the triangle tier from a routed action. -public export -actionTier : RoutedAction -> TriangleTier -actionTier (RouteEliminate _ _) = Eliminate -actionTier (RouteSubstitute _ _) = Substitute -actionTier (RouteControl _) = Control - -||| Whether an eliminate recipe was found for a pattern. -public export -data EliminateResult : Type where - EliminateFound : (recipe : Recipe) -> EliminateResult - EliminateNotFound : EliminateResult - -||| Whether a substitute recipe was found for a pattern. -public export -data SubstituteResult : Type where - SubstituteFound : (recipe : Recipe) -> SubstituteResult - ||| Substitute search found an eliminate-tier recipe (promotion case) - SubstitutePromoted : (recipe : Recipe) -> SubstituteResult - SubstituteNotFound : SubstituteResult - -||| Route a pattern through the safety triangle. -||| This function is total: every combination of eliminate/substitute -||| lookup results produces exactly one RoutedAction. -||| -||| Mirrors TriangleRouter.route/3 in lib/triangle_router.ex: -||| 1. Try eliminate first -||| 2. If not, try substitute (which may promote to eliminate) -||| 3. Fall back to control -public export -route : (pattern : Pattern) -> EliminateResult -> SubstituteResult -> RoutedAction -route pat (EliminateFound recipe) _ = RouteEliminate recipe pat -route pat EliminateNotFound (SubstituteFound recipe) = RouteSubstitute recipe pat -route pat EliminateNotFound (SubstitutePromoted recipe) = RouteEliminate recipe pat -route pat EliminateNotFound SubstituteNotFound = RouteControl pat - -||| Proof: routing always respects the triangle hierarchy. -||| If eliminate is found, the action is Eliminate tier. -||| If only substitute is found, the action is Substitute tier. -||| If neither is found, the action is Control tier. -public export -routeRespectsHierarchy : (pat : Pattern) - -> (elim : EliminateResult) - -> (sub : SubstituteResult) - -> (actionTier (route pat elim sub) = Eliminate) - `Either` - ((actionTier (route pat elim sub) = Substitute) - `Either` - (actionTier (route pat elim sub) = Control)) -routeRespectsHierarchy pat (EliminateFound recipe) _ - = Left Refl -routeRespectsHierarchy pat EliminateNotFound (SubstituteFound recipe) - = Right (Left Refl) -routeRespectsHierarchy pat EliminateNotFound (SubstitutePromoted recipe) - = Left Refl -routeRespectsHierarchy pat EliminateNotFound SubstituteNotFound - = Right (Right Refl) - -||| Proof: routing is total — every input combination produces a result. -||| This is witnessed by the function `route` itself being total (%default total), -||| but we additionally prove that the result is always one of the three tiers. -public export -routeTotality : (pat : Pattern) - -> (elim : EliminateResult) - -> (sub : SubstituteResult) - -> (tier : TriangleTier ** actionTier (route pat elim sub) = tier) -routeTotality pat (EliminateFound recipe) _ - = (Eliminate ** Refl) -routeTotality pat EliminateNotFound (SubstituteFound recipe) - = (Substitute ** Refl) -routeTotality pat EliminateNotFound (SubstitutePromoted recipe) - = (Eliminate ** Refl) -routeTotality pat EliminateNotFound SubstituteNotFound - = (Control ** Refl) - -||| Proof: eliminate is always tried before substitute. -||| When eliminate succeeds, substitute result is irrelevant. -public export -eliminateFirst : (pat : Pattern) -> (recipe : Recipe) - -> (sub : SubstituteResult) - -> actionTier (route pat (EliminateFound recipe) sub) = Eliminate -eliminateFirst pat recipe _ = Refl - -||| Proof: control is only reached when both eliminate and substitute fail. -public export -controlOnlyAsFallback : (pat : Pattern) - -> actionTier (route pat EliminateNotFound SubstituteNotFound) = Control -controlOnlyAsFallback pat = Refl - ------------------------------------------------------------------------- --- Section 3: Confidence and Dispatch Strategy ------------------------------------------------------------------------- - -||| Confidence thresholds matching lib/triangle_router.ex: -||| >= 0.95 -> AutoExecute -||| >= 0.85 -> Review -||| < 0.85 -> ReportOnly -public export -autoExecuteThreshold : Double -autoExecuteThreshold = 0.95 - -public export -reviewThreshold : Double -reviewThreshold = 0.85 - -||| Dispatch strategy determination. -||| Mirrors TriangleRouter.dispatch_strategy/1. -||| Total by construction: the three conditions are exhaustive over Double. -public export -dispatchStrategy : (confidence : Double) -> DispatchStrategy -dispatchStrategy confidence = - if confidence >= 0.95 then AutoExecute - else if confidence >= 0.85 then Review - else ReportOnly - -||| Proof: high confidence (>= 0.95) always yields AutoExecute. -public export -highConfidenceAutoExecutes : (c : Double) - -> So (c >= 0.95) - -> dispatchStrategy c = AutoExecute -highConfidenceAutoExecutes c prf with (c >= 0.95) - highConfidenceAutoExecutes c Oh | True = Refl - -||| Proof: medium confidence (>= 0.85, < 0.95) always yields Review. -public export -mediumConfidenceReviews : (c : Double) - -> So (not (c >= 0.95)) - -> So (c >= 0.85) - -> dispatchStrategy c = Review -mediumConfidenceReviews c notHigh isMed with (c >= 0.95) - mediumConfidenceReviews c notHigh isMed | False with (c >= 0.85) - mediumConfidenceReviews c notHigh Oh | False | True = Refl - -||| Proof: low confidence (< 0.85) always yields ReportOnly. -public export -lowConfidenceReports : (c : Double) - -> So (not (c >= 0.95)) - -> So (not (c >= 0.85)) - -> dispatchStrategy c = ReportOnly -lowConfidenceReports c notHigh notMed with (c >= 0.95) - lowConfidenceReports c notHigh notMed | False with (c >= 0.85) - lowConfidenceReports c notHigh notMed | False | False = Refl - ------------------------------------------------------------------------- --- Section 4: Dispatch Correctness — Findings Route to the Right Bot ------------------------------------------------------------------------- - -||| The bot assigned for each dispatch strategy at the eliminate tier. -||| Mirrors FleetDispatcher.dispatch_eliminate_via_fleet/2. -public export -eliminateBot : DispatchStrategy -> BotId -eliminateBot AutoExecute = RobotRepoAutomaton -eliminateBot Review = Rhodibot -eliminateBot ReportOnly = Sustainabot - -||| The bot(s) assigned for a substitute action. -||| Substitute always goes to Rhodibot (PR) + Echidnabot (proof obligation). -||| Mirrors FleetDispatcher.dispatch_routed_action({:substitute, ...}). -public export -data SubstituteDispatch : Type where - MkSubstituteDispatch : (prBot : BotId) - -> (proofBot : BotId) - -> SubstituteDispatch - -public export -substituteDispatch : SubstituteDispatch -substituteDispatch = MkSubstituteDispatch Rhodibot Echidnabot - -||| The bot assigned for a control action. -||| Control always goes to Sustainabot (advisory). -||| Mirrors FleetDispatcher.dispatch_routed_action({:control, ...}). -public export -controlBot : BotId -controlBot = Sustainabot - -||| Full dispatch: given a routed action, determine which bot(s) handle it. -||| This models the complete FleetDispatcher.dispatch_routed_action/1 function. -public export -data DispatchTarget : Type where - ||| Single bot handles the action (eliminate or control) - SingleBot : BotId -> DispatchTarget - ||| Two bots handle the action in parallel (substitute) - DualBot : BotId -> BotId -> DispatchTarget - -public export -dispatch : RoutedAction -> DispatchTarget -dispatch (RouteEliminate recipe _) = - let confidence = recipe.confidence - strategy = dispatchStrategy confidence - in SingleBot (eliminateBot strategy) -dispatch (RouteSubstitute _ _) = - DualBot Rhodibot Echidnabot -dispatch (RouteControl _) = - SingleBot Sustainabot - -||| Proof: auto-execute eliminate always dispatches to RobotRepoAutomaton. -public export -autoExecuteGoesToAutomaton : (recipe : Recipe) -> (pat : Pattern) - -> So (recipe.confidence >= 0.95) - -> dispatch (RouteEliminate recipe pat) - = SingleBot RobotRepoAutomaton -autoExecuteGoesToAutomaton recipe pat prf with (recipe.confidence >= 0.95) - autoExecuteGoesToAutomaton recipe pat Oh | True = Refl - -||| Proof: control always dispatches to Sustainabot. -public export -controlGoesToSustabot : (pat : Pattern) - -> dispatch (RouteControl pat) = SingleBot Sustainabot -controlGoesToSustabot pat = Refl - -||| Proof: substitute always involves Rhodibot and Echidnabot. -public export -substituteInvolvesBothBots : (recipe : Recipe) -> (pat : Pattern) - -> dispatch (RouteSubstitute recipe pat) - = DualBot Rhodibot Echidnabot -substituteInvolvesBothBots recipe pat = Refl - ------------------------------------------------------------------------- --- Section 5: Confidence Monotonicity (Bayesian Update) ------------------------------------------------------------------------- - -||| Bayesian Beta-distribution confidence model. -||| Mirrors OutcomeTracker.bayesian_update/3. -||| -||| posterior = (alpha_prior + successes) / (alpha_prior + successes + beta_prior + failures) -||| -||| where alpha_prior = prior * strength, beta_prior = (1 - prior) * strength. - -||| Naturals-based model of the Bayesian update to avoid floating-point -||| reasoning. We represent confidence as a rational alpha / (alpha + beta). -||| Prior strength is an implicit parameter (encoded in the initial alpha, beta). -public export -record BayesState where - constructor MkBayes - alpha : Nat -- prior successes (scaled) - beta : Nat -- prior failures (scaled) - -||| Record a success: increment alpha. -public export -recordSuccess : BayesState -> BayesState -recordSuccess st = { alpha $= S } st - -||| Record a failure: increment beta. -public export -recordFailure : BayesState -> BayesState -recordFailure st = { beta $= S } st - -||| The "confidence numerator" is alpha. -||| The "confidence denominator" is alpha + beta. -||| Confidence = alpha / (alpha + beta). - -||| Proof: recording a success never decreases the confidence numerator -||| while the denominator grows by the same amount — so the fraction -||| alpha / (alpha + beta) is non-decreasing. -||| -||| More precisely: a / (a + b) <= (a + 1) / (a + 1 + b) -||| Cross-multiplying: a * (a + 1 + b) <= (a + 1) * (a + b) -||| a^2 + a + ab <= a^2 + ab + a + b -||| 0 <= b -||| which holds for all natural b. -||| -||| We prove the cross-multiplication inequality directly on Nat. -public export -successNonDecreasing : (st : BayesState) - -> LTE (st.alpha * (S st.alpha + st.beta)) - (S st.alpha * (st.alpha + st.beta)) -successNonDecreasing (MkBayes a b) = successLemma a b - where - ||| Core lemma: a * (S a + b) <= S a * (a + b) - ||| Expanding: a * S(a + b) <= S a * (a + b) - ||| i.e. a * (a + b) + a <= (a + b) + a * (a + b) - ||| i.e. a <= (a + b) - ||| which is just LTE a (a + b), i.e. b >= 0. - successLemma : (a : Nat) -> (b : Nat) - -> LTE (a * (S a + b)) (S a * (a + b)) - -- a * (S a + b) = a * S(a+b) = a + a*(a+b) [multRightSuccPlus] - -- S a * (a + b) = (a + b) + a*(a+b) [def of *] - -- so the goal reduces to a + a*(a+b) <= (a+b) + a*(a+b), i.e. a <= a + b. - successLemma a b = - rewrite multRightSuccPlus a (a + b) in - plusLteMonotoneRight (a * (a + b)) a (a + b) (lteAddRight a) - -||| Proof: recording a failure never increases the confidence. -||| After failure, alpha stays the same but beta increases, so -||| alpha / (alpha + beta) >= alpha / (alpha + S beta). -||| Cross-multiplying: alpha * (alpha + S beta) >= alpha * (alpha + beta) -||| which simplifies to: alpha * (alpha + beta) + alpha >= alpha * (alpha + beta) -||| i.e. alpha >= 0, which holds for all Nat. -public export -failureNonIncreasing : (st : BayesState) - -> LTE (st.alpha * (st.alpha + S st.beta)) - (st.alpha * (st.alpha + st.beta) + st.alpha) -failureNonIncreasing (MkBayes a b) = failureLemma a b - where - ||| a * (a + S b) = a * S(a + b) = a * (a + b) + a - ||| So a * (a + S b) <= a * (a + b) + a is actually equality (LTE from reflexivity). - failureLemma : (a : Nat) -> (b : Nat) - -> LTE (a * (a + S b)) (a * (a + b) + a) - -- a * (a + S b) = a * S(a+b) = a + a*(a+b), which equals a*(a+b) + a - -- by commutativity, so the bound holds by reflexivity. - failureLemma a b = - rewrite sym (plusSuccRightSucc a b) in -- a + S b => S (a + b) - rewrite multRightSuccPlus a (a + b) in -- a * S(a+b) => a + a*(a+b) - rewrite plusCommutative a (a * (a + b)) in - reflexive - ------------------------------------------------------------------------- --- Section 6: Safety Triangle Soundness ------------------------------------------------------------------------- - -||| The safety triangle is sound if the routing function always -||| assigns the highest-available tier. That is: -||| -||| - If eliminate is available, the action tier is Eliminate. -||| - If only substitute is available, the action tier is Substitute. -||| - Otherwise, the action tier is Control. -||| -||| We also prove that no lower tier is assigned when a higher one -||| is available (no "downgrading"). - -||| Proof: when eliminate is available, route never produces Substitute or Control. -public export -eliminateNeverDowngraded : (pat : Pattern) -> (recipe : Recipe) - -> (sub : SubstituteResult) - -> Not (actionTier (route pat (EliminateFound recipe) sub) = Substitute) -eliminateNeverDowngraded pat recipe sub Refl impossible - -||| Proof: when eliminate is available, route never produces Control. -public export -eliminateNeverControl : (pat : Pattern) -> (recipe : Recipe) - -> (sub : SubstituteResult) - -> Not (actionTier (route pat (EliminateFound recipe) sub) = Control) -eliminateNeverControl pat recipe sub Refl impossible - -||| Proof: substitute is only chosen when eliminate is unavailable. -public export -substituteOnlyWithoutEliminate : (pat : Pattern) - -> (recipe : Recipe) - -> actionTier (route pat EliminateNotFound (SubstituteFound recipe)) - = Substitute -substituteOnlyWithoutEliminate pat recipe = Refl - -||| Proof: a promoted substitute (eliminate-tier recipe found during -||| substitute search) correctly returns Eliminate tier, not Substitute. -public export -promotedSubstituteIsEliminate : (pat : Pattern) - -> (recipe : Recipe) - -> actionTier (route pat EliminateNotFound (SubstitutePromoted recipe)) - = Eliminate -promotedSubstituteIsEliminate pat recipe = Refl - ------------------------------------------------------------------------- --- Section 7: Dispatch Strategy Ordering ------------------------------------------------------------------------- - -||| Dispatch strategies have a trust ordering: -||| AutoExecute > Review > ReportOnly -||| Higher trust = more autonomous action. -public export -data StrategyLT : DispatchStrategy -> DispatchStrategy -> Type where - AutoGtReview : StrategyLT AutoExecute Review - AutoGtReport : StrategyLT AutoExecute ReportOnly - ReviewGtReport : StrategyLT Review ReportOnly - -||| Strategy ordering is irreflexive. -public export -strategyIrreflexive : StrategyLT s s -> Void -strategyIrreflexive AutoGtReview impossible -strategyIrreflexive AutoGtReport impossible -strategyIrreflexive ReviewGtReport impossible - -||| Strategy ordering is transitive. -public export -strategyTransitive : StrategyLT a b -> StrategyLT b c -> StrategyLT a c -strategyTransitive AutoGtReview ReviewGtReport = AutoGtReport - -||| Annealing stage caps. -||| Mirrors ConfidenceAnnealing.max_dispatch_tier/1: -||| nascent -> ReportOnly -||| adolescent -> Review -||| mature -> AutoExecute -||| veteran -> AutoExecute -public export -data AnnealingStage = Nascent | Adolescent | Mature | Veteran - -public export -maxTier : AnnealingStage -> DispatchStrategy -maxTier Nascent = ReportOnly -maxTier Adolescent = Review -maxTier Mature = AutoExecute -maxTier Veteran = AutoExecute - -||| Strategy rank for comparison (0 = least trust, 2 = most). -public export -strategyRank : DispatchStrategy -> Nat -strategyRank ReportOnly = 0 -strategyRank Review = 1 -strategyRank AutoExecute = 2 - -||| Clamp a strategy to the maximum allowed by the annealing stage. -||| Mirrors ConfidenceAnnealing.clamp_strategy/2. -public export -clampStrategy : DispatchStrategy -> AnnealingStage -> DispatchStrategy -clampStrategy strategy stage = - let maxAllowed = maxTier stage - in if strategyRank strategy > strategyRank maxAllowed - then maxAllowed - else strategy - -||| Proof: clamping never promotes a strategy above the stage maximum. -public export -clampNeverExceedsMax : (strategy : DispatchStrategy) -> (stage : AnnealingStage) - -> LTE (strategyRank (clampStrategy strategy stage)) - (strategyRank (maxTier stage)) -clampNeverExceedsMax ReportOnly Nascent = LTEZero -clampNeverExceedsMax Review Nascent = LTEZero -clampNeverExceedsMax AutoExecute Nascent = LTEZero -clampNeverExceedsMax ReportOnly Adolescent = LTEZero -clampNeverExceedsMax Review Adolescent = LTESucc LTEZero -- 1 <= 1 -clampNeverExceedsMax AutoExecute Adolescent = LTESucc LTEZero -- 1 <= 1 (clamped) -clampNeverExceedsMax ReportOnly Mature = LTEZero -clampNeverExceedsMax Review Mature = LTESucc LTEZero -- 1 <= 2 -clampNeverExceedsMax AutoExecute Mature = LTESucc (LTESucc LTEZero) -- 2 <= 2 -clampNeverExceedsMax ReportOnly Veteran = LTEZero -clampNeverExceedsMax Review Veteran = LTESucc LTEZero -- 1 <= 2 -clampNeverExceedsMax AutoExecute Veteran = LTESucc (LTESucc LTEZero) -- 2 <= 2 - -||| Proof: nascent recipes can never auto-execute. -public export -nascentNeverAutoExecutes : (strategy : DispatchStrategy) - -> Not (clampStrategy strategy Nascent = AutoExecute) -nascentNeverAutoExecutes ReportOnly Refl impossible -nascentNeverAutoExecutes Review Refl impossible -nascentNeverAutoExecutes AutoExecute Refl impossible - -||| Proof: veteran recipes have no dispatch restrictions. -public export -veteranUnrestricted : (strategy : DispatchStrategy) - -> clampStrategy strategy Veteran = strategy -veteranUnrestricted ReportOnly = Refl -veteranUnrestricted Review = Refl -veteranUnrestricted AutoExecute = Refl - ------------------------------------------------------------------------- --- Section 8: End-to-End Composition ------------------------------------------------------------------------- - -||| The full pipeline: route a finding, then dispatch the routed action. -||| This composes Sections 2 and 4, proving the complete path from -||| finding to bot assignment is total and deterministic. -public export -pipeline : (pat : Pattern) - -> (elim : EliminateResult) - -> (sub : SubstituteResult) - -> DispatchTarget -pipeline pat elim sub = dispatch (route pat elim sub) - -||| Proof: the full pipeline always produces a dispatch target. -||| (Witnessed by `pipeline` being total under %default total.) -public export -pipelineTotality : (pat : Pattern) - -> (elim : EliminateResult) - -> (sub : SubstituteResult) - -> (target : DispatchTarget ** pipeline pat elim sub = target) -pipelineTotality pat elim sub = (pipeline pat elim sub ** Refl) - -||| Proof: control findings in the full pipeline always go to Sustainabot. -public export -controlPipelineTarget : (pat : Pattern) - -> pipeline pat EliminateNotFound SubstituteNotFound - = SingleBot Sustainabot -controlPipelineTarget pat = Refl - -||| Proof: substitute findings in the full pipeline always involve both -||| Rhodibot (PR creation) and Echidnabot (proof obligation). -public export -substitutePipelineTarget : (pat : Pattern) -> (recipe : Recipe) - -> pipeline pat EliminateNotFound (SubstituteFound recipe) - = DualBot Rhodibot Echidnabot -substitutePipelineTarget pat recipe = Refl diff --git a/src/abi/Types.idr b/src/abi/Types.idr deleted file mode 100644 index 40d2ed6c..00000000 --- a/src/abi/Types.idr +++ /dev/null @@ -1,242 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Hypatia ABI — Core Types --- Defines the type-safe interface for all Hypatia API operations. --- These types are the single source of truth; all API protocols --- (GraphQL, gRPC, REST) derive from these definitions. - -module Hypatia.ABI.Types - -import Data.So - -%default total - -||| Severity levels for findings, ordered by criticality -public export -data Severity = Critical | High | Medium | Low | Info - -public export -Eq Severity where - Critical == Critical = True - High == High = True - Medium == Medium = True - Low == Low = True - Info == Info = True - _ == _ = False - -public export -Ord Severity where - compare Critical Critical = EQ - compare Critical _ = LT - compare _ Critical = GT - compare High High = EQ - compare High _ = LT - compare _ High = GT - compare Medium Medium = EQ - compare Medium _ = LT - compare _ Medium = GT - compare Low Low = EQ - compare Low _ = LT - compare _ Low = GT - compare Info Info = EQ - -||| Safety triangle tiers (Eliminate > Substitute > Control) -public export -data TriangleTier = Eliminate | Substitute | Control - -||| Dispatch strategy based on confidence level -public export -data DispatchStrategy = AutoExecute | Review | ReportOnly - -||| Fix outcome from bot execution -public export -data Outcome = Success | Failure | FalsePositive - -||| Bot identifiers in the fleet -public export -data BotId - = Rhodibot - | Echidnabot - | Sustainabot - | Glambot - | Seambot - | Cipherbot - | Finishbot - | Accessibilitybot - | RobotRepoAutomaton - -||| Confidence score — bounded between 0.0 and 1.0 -||| The Nat parameter is confidence * 10000 for type-level precision -public export -record Confidence where - constructor MkConfidence - value : Double - {auto prf : So (value >= 0.0 && value <= 1.0)} - -||| A recipe for fixing a specific weakness pattern -public export -record Recipe where - constructor MkRecipe - id : String - description : String - confidence : Double - autoFixable : Bool - provenModule : Maybe String - -||| A canonical weakness pattern -public export -record Pattern where - constructor MkPattern - patternId : String - description : String - severity : Severity - affectedRepos : List String - file : String - line : Nat - cwe : Maybe String - -||| Health check status for a single component -public export -data HealthStatus = Pass | Warn | Fail - -||| API response wrapper with typed content -public export -record ApiResponse (a : Type) where - constructor MkApiResponse - success : Bool - payload : Maybe a -- ^ wire field name is "data"; `data` is an Idris2 keyword - error : Maybe String - timestamp : String - -||| Scan result for a repository -public export -record ScanResult where - constructor MkScanResult - repo : String - weakPoints : Nat - patterns : List Pattern - scannedAt : String - -||| Dispatch manifest entry -public export -record DispatchEntry where - constructor MkDispatchEntry - bot : BotId - repo : String - file : String - recipeId : String - tier : TriangleTier - strategy : DispatchStrategy - -||| Outcome record for the learning loop -public export -record OutcomeRecord where - constructor MkOutcomeRecord - recipeId : String - repo : String - file : String - outcome : Outcome - timestamp : String - bot : String - --- ============================================================ --- UnifiedApiAdapter — sixteen protocol adapters --- ============================================================ --- --- Mirrors the Zig enum at `ffi/zig/src/unified-api-adapter.zig` and the Rust --- enum at `clients/rust/hypatia-client/src/connector.rs`. Wire --- ordering is load-bearing — the integer value of each variant is --- the C ABI id used by `hypatia_connector_name(id)`. Do not --- renumber. The dependent-type proof `connectorWireIdInRange` --- below pins the count at exactly 16. --- --- Replaces the V-lang client at `api/v/hypatia.v` (deleted 2026-04-13). - -||| The sixteen protocol connectors exposed by the Hypatia -||| unified-api-adapter surface. Order is the C ABI wire ordering; -||| see `Hypatia.ABI.Types.connectorWireId` for the mapping. -public export -data Connector - = -- Core 12 - GRPC -- 0 - | GraphQL -- 1 - | REST -- 2 - | FlatBuffers -- 3 - | Bebop -- 4 - | JsonRpc -- 5 - | WebSocket -- 6 - | MQTT -- 7 - | TRPC -- 8 - | CapnProto -- 9 - | SOAP -- 10 - | VeriSimDBRest -- 11 - -- Umoja-substrate 4 - | BSP -- 12 - | SCIP -- 13 - | IPFS -- 14 - | ArrowFlight -- 15 - -||| C ABI wire id of a connector. Must agree with the Zig enum. -public export -connectorWireId : Connector -> Nat -connectorWireId GRPC = 0 -connectorWireId GraphQL = 1 -connectorWireId REST = 2 -connectorWireId FlatBuffers = 3 -connectorWireId Bebop = 4 -connectorWireId JsonRpc = 5 -connectorWireId WebSocket = 6 -connectorWireId MQTT = 7 -connectorWireId TRPC = 8 -connectorWireId CapnProto = 9 -connectorWireId SOAP = 10 -connectorWireId VeriSimDBRest = 11 -connectorWireId BSP = 12 -connectorWireId SCIP = 13 -connectorWireId IPFS = 14 -connectorWireId ArrowFlight = 15 - -||| Canonical wire name of a connector. Must agree with -||| `Connector.name()` in `ffi/zig/src/unified-api-adapter.zig`. -public export -connectorName : Connector -> String -connectorName GRPC = "grpc" -connectorName GraphQL = "graphql" -connectorName REST = "rest" -connectorName FlatBuffers = "flatbuffers" -connectorName Bebop = "bebop" -connectorName JsonRpc = "jsonrpc" -connectorName WebSocket = "websocket" -connectorName MQTT = "mqtt" -connectorName TRPC = "trpc" -connectorName CapnProto = "capnproto" -connectorName SOAP = "soap" -connectorName VeriSimDBRest = "verisimdb-rest" -connectorName BSP = "bsp" -connectorName SCIP = "scip" -connectorName IPFS = "ipfs" -connectorName ArrowFlight = "arrow-flight" - -||| All sixteen connectors in wire order. -public export -allConnectors : List Connector -allConnectors = - [ GRPC, GraphQL, REST, FlatBuffers, Bebop, JsonRpc - , WebSocket, MQTT, TRPC, CapnProto, SOAP, VeriSimDBRest - , BSP, SCIP, IPFS, ArrowFlight - ] - -||| Proof that there are exactly sixteen connectors. Pins the -||| unified-api-adapter invariant at the type level: any code that adds or -||| removes a connector must update this proof, which forces a -||| coordinated update of the Zig enum and the Rust client. -public export -connectorCount : length Hypatia.ABI.Types.allConnectors = 16 -connectorCount = Refl - -||| Bound port for a connector under a given base port. Layout -||| matches the V-lang reference (`base + id + 1`). -public export -connectorPort : (basePort : Nat) -> Connector -> Nat -connectorPort base c = base + connectorWireId c + 1 diff --git a/stapeln.toml b/stapeln.toml index 74a2946e..0e719de8 100644 --- a/stapeln.toml +++ b/stapeln.toml @@ -168,7 +168,7 @@ commands = [ "idris2 --build src/abi/hypatia-abi.ipkg", "idris2 --build verify/hypatia-verify.ipkg || echo 'Proof verification: check results'", ] -cache-key = "src/abi/*.idr" +cache-key = "src/Hypatia/ABI/*.idr" cache = true [layers.ffi-build] diff --git a/test/merge_orchestration/sensor_test.exs b/test/merge_orchestration/sensor_test.exs index 12617f82..b23c48e6 100644 --- a/test/merge_orchestration/sensor_test.exs +++ b/test/merge_orchestration/sensor_test.exs @@ -15,7 +15,7 @@ defmodule Hypatia.MergeOrchestration.SensorTest do test "a proof file is a proof" do assert {:proof, _, _} = Sensor.classify(obs(%{"files" => ["proofs/agda/All.agda"]})) - assert {:proof, _, _} = Sensor.classify(obs(%{"files" => ["src/abi/Types.idr"]})) + assert {:proof, _, _} = Sensor.classify(obs(%{"files" => ["src/Hypatia/ABI/Types.idr"]})) end test "a SECURITY touch (or label) is security" do diff --git a/test/zig_ffi_smoke_test.exs b/test/zig_ffi_smoke_test.exs index 6bc1bd3e..3462f885 100644 --- a/test/zig_ffi_smoke_test.exs +++ b/test/zig_ffi_smoke_test.exs @@ -237,18 +237,24 @@ defmodule Hypatia.ZigFFI.SmokeTest do # --------------------------------------------------------------------------- # Smoke: Idris2 ABI source files are present + # + # Bound to `src/Hypatia/ABI/`, the modules `src/abi/hypatia-abi.ipkg` actually + # compiles (its `sourcedir = ".."` resolves to `src/`). Until 2026-09-22 this + # pointed at `src/abi/`, which held a byte-identical copy compiled by nothing; + # those duplicates are now deleted and only the two .ipkg files remain there. # --------------------------------------------------------------------------- describe "Idris2 ABI source integrity" do - @abi_dir Path.expand("../src/abi", __DIR__) + @abi_dir Path.expand("../src/Hypatia/ABI", __DIR__) - test "src/abi directory exists" do + test "the Idris2 ABI directory exists" do assert File.exists?(@abi_dir), "Idris2 ABI directory not found at #{@abi_dir}" end - test "all 5 required Idris2 ABI modules are present" do - required_modules = ~w(Types.idr GraphQL.idr GRPC.idr REST.idr FFI.idr) + test "all 7 required Idris2 ABI modules are present" do + required_modules = + ~w(Types.idr GraphQL.idr GRPC.idr REST.idr FFI.idr RuleEngine.idr Gen.idr) Enum.each(required_modules, fn mod -> path = Path.join(@abi_dir, mod) @@ -259,10 +265,17 @@ defmodule Hypatia.ZigFFI.SmokeTest do end test "Idris2 ABI modules have SPDX headers" do - @abi_dir - |> File.ls!() - |> Enum.filter(&String.ends_with?(&1, ".idr")) - |> Enum.each(fn file -> + idr_files = + @abi_dir + |> File.ls!() + |> Enum.filter(&String.ends_with?(&1, ".idr")) + + # The denominator. Without it this test passes vacuously the moment the + # directory it points at holds no .idr files -- which is exactly what a + # mis-repointed @abi_dir looks like. + assert idr_files != [], "no .idr files found in #{@abi_dir}" + + Enum.each(idr_files, fn file -> path = Path.join(@abi_dir, file) {:ok, content} = File.read(path) first_2k = String.slice(content, 0, 2000) diff --git a/verification/proofs/idris2/ConfidenceBounds.idr b/verification/proofs/idris2/ConfidenceBounds.idr index 34a29c3c..d7a202d8 100644 --- a/verification/proofs/idris2/ConfidenceBounds.idr +++ b/verification/proofs/idris2/ConfidenceBounds.idr @@ -14,7 +14,7 @@ -- Corresponds to: -- - lib/outcome_tracker.ex (Bayesian confidence updates) -- - lib/confidence_annealing.ex (clamping, floor/cap) --- - src/abi/Types.idr (Confidence record) +-- - src/Hypatia/ABI/Types.idr (Confidence record) module ConfidenceBounds diff --git a/verification/proofs/idris2/DispatchStrategy.idr b/verification/proofs/idris2/DispatchStrategy.idr index b4f99948..b67bda38 100644 --- a/verification/proofs/idris2/DispatchStrategy.idr +++ b/verification/proofs/idris2/DispatchStrategy.idr @@ -17,7 +17,7 @@ -- Corresponds to: -- - lib/triangle_router.ex (dispatch_strategy/1) -- - lib/confidence_annealing.ex (clamp_strategy/2, max_dispatch_tier/1) --- - src/abi/RuleEngine.idr (dispatchStrategy, clampStrategy) +-- - src/Hypatia/ABI/RuleEngine.idr (dispatchStrategy, clampStrategy) module DispatchStrategy diff --git a/verification/proofs/idris2/SafetyTriangle.idr b/verification/proofs/idris2/SafetyTriangle.idr index 08dba3c1..b1dc4f37 100644 --- a/verification/proofs/idris2/SafetyTriangle.idr +++ b/verification/proofs/idris2/SafetyTriangle.idr @@ -9,7 +9,7 @@ -- -- Corresponds to: -- - lib/triangle_router.ex (TriangleRouter.route/3) --- - src/abi/RuleEngine.idr (route, RoutedAction) +-- - src/Hypatia/ABI/RuleEngine.idr (route, RoutedAction) module SafetyTriangle