Standardise license setup: MPL-2.0 + PMPL-1.0-or-later (REUSE)

- LICENSE: pure MPL-2.0 text for machine detection (GitHub, registries)
- LICENSES/MPL-2.0.txt: standard MPL-2.0 text
- LICENSES/PMPL-1.0-or-later.txt: Palimpsest License text
- NOTICE: explains the dual-license relationship
- Source SPDX headers remain PMPL-1.0-or-later

This ensures OSI compliance checks pass while preserving PMPL as
the governing license for source code.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.bot_directives/echidnabot.scm

@@ -1,7 +1,26 @@
 ;; SPDX-License-Identifier: PMPL-1.0-or-later
 (bot-directive
   (bot "echidnabot")
-  (scope "formal verification and fuzzing")
-  (allow ("analysis" "fuzzing" "proof checks"))
-  (deny ("write to core modules" "write to bindings"))
-  (notes "May open findings; code changes require explicit approval"))
+  (scope "formal verification, proof totality, and dependent type auditing")
+  (languages ("Idris2" "Zig"))
+  (targets
+    ("ochrance-core/" "Idris2 core library — A2ML, Framework, FFI")
+    ("modules/" "Verified filesystem subsystem")
+    ("src/abi/" "ABI type definitions")
+    ("ffi/zig/" "Zig FFI implementation")
+    ("tests/" "Test suite"))
+  (allow ("analysis" "proof checks" "totality auditing" "FFI safety checks"))
+  (deny ("write to core modules" "write to FFI bindings" "modify proofs without review"))
+  (scanning-rules
+    (idris2
+      (ban ("believe_me" "assert_total" "assert_smaller" "unsafePerformIO") (severity "critical"))
+      (enforce ("total" "%default total") (notes "All modules must be total"))
+      (flag ("partial") (severity "high")))
+    (zig
+      (flag ("@ptrCast" "@alignCast") (severity "medium"))
+      (ban ("@intToPtr") (severity "high") (unless "FFI boundary"))))
+  (echidna-ffi
+    (library "libechidna.so")
+    (bindings "ochrance-core/Ochrance/FFI/Echidna.idr")
+    (status "stub — FFI not yet implemented, wrappers return defaults"))
+  (notes "Ochrance is a neurosymbolic verification framework. Echidna integration is core to its architecture. All functions must be total — structural recursion only."))

.github/workflows/hypatia-scan.yml

@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
         with:
           fetch-depth: 0  # Full history for better pattern analysis
 

.machine_readable/STATE.scm

@@ -1,4 +1,77 @@
 ;; SPDX-License-Identifier: PMPL-1.0-or-later
-(state (metadata (version "0.1.0") (last-updated "2026-02-08") (status active))
-  (project-context (name "language-bridges") (purpose "FFI bridges between languages via Zig") (completion-percentage 20))
-  (components (component "ada-zig-ffi") (component "gleam-zig-ffi") (component "idris2-zig-ffi") (component "julia-zig-ffi") (component "ocaml-zig-ffi") (component "rescript-zig-ffi") (component "rust-zig-ffi") (component "swift-zig-ffi") (component "zig-c-ffi") (component "zig-container-ffi") (component "zig-fuse-ext") (component "zig-libgit2-ffi") (component "zig-nickel-ffi") (component "zig-systemd-ffi") (component "zig-wireguard")))
+;; Ochrance - Neurosymbolic Filesystem Verification Framework
+;; STATE.scm - Current project state
+
+(state
+  (metadata
+    (version "0.2.0")
+    (last-updated "2026-03-10")
+    (status active))
+
+  (project-context
+    (name "ochrance")
+    (purpose "Neurosymbolic filesystem verification framework using Idris2 dependent types")
+    (completion-percentage 77))
+
+  (components
+    (component
+      (name "a2ml")
+      (description "Attestation & Audit Markup Language")
+      (completion-percentage 95)
+      (subcomponents
+        (subcomponent (name "Lexer") (status "complete") (percentage 100))
+        (subcomponent (name "Parser") (status "complete") (percentage 100))
+        (subcomponent (name "Validator") (status "complete") (percentage 95))
+        (subcomponent (name "Serializer") (status "complete") (percentage 85))))
+
+    (component
+      (name "framework")
+      (description "Verification framework core")
+      (completion-percentage 100)
+      (subcomponents
+        (subcomponent (name "Interface") (status "complete") (percentage 100))
+        (subcomponent (name "Proof") (status "complete") (percentage 100))
+        (subcomponent (name "Error") (status "complete") (percentage 100))))
+
+    (component
+      (name "filesystem")
+      (description "Reference VerifiedSubsystem implementation")
+      (completion-percentage 75)
+      (subcomponents
+        (subcomponent (name "Types") (status "complete") (percentage 100))
+        (subcomponent (name "Merkle") (status "active") (percentage 80))
+        (subcomponent (name "Verify") (status "active") (percentage 75))
+        (subcomponent (name "Repair") (status "active") (percentage 65))))
+
+    (component
+      (name "ffi-crypto")
+      (description "Zig FFI cryptographic bindings via libochrance.so")
+      (completion-percentage 30)
+      (notes "FFI declarations present, buffer management needs real implementation"))
+
+    (component
+      (name "abi")
+      (description "Idris2 ABI definitions with formal proofs")
+      (completion-percentage 80)
+      (subcomponents
+        (subcomponent (name "Types") (status "complete") (percentage 95))
+        (subcomponent (name "Layout") (status "complete") (percentage 85))
+        (subcomponent (name "Foreign") (status "active") (percentage 60))))
+
+    (component
+      (name "echidna-ffi")
+      (description "FFI bindings to libechidna.so for neural proof synthesis")
+      (completion-percentage 5)
+      (notes "Stub only, awaiting libechidna.so stabilization")))
+
+  (blockers-and-issues
+    (blocker "FFI buffer management in Crypto.idr uses placeholder cast operations")
+    (blocker "Merkle powerTwoSucc arithmetic lemma is postulated, not proven")
+    (issue "Verify.idr toHex uses assert_total - needs provably total rewrite")
+    (issue "ECHIDNA FFI is stub-only, blocked on libechidna.so API"))
+
+  (critical-next-actions
+    (action "Replace Crypto.idr placeholder stubs with real FFI buffer calls")
+    (action "Prove powerTwoSucc lemma")
+    (action "Rewrite toHex as provably total")
+    (action "Complete ABI Foreign module with full FFI coverage")))