The README makes claims. This file backs them up.
Ochránce is a neurosymbolic filesystem verification framework built with Idris2 dependent types. It provides mathematically proven guarantees about filesystem integrity through A2ML (Attestation & Audit Markup Language), verified Merkle trees with size-indexed proofs, and linear type repair operations.
Three components orchestrate this: A2ML parser/validator (parses filesystem manifests), verified Merkle trees (compile-time structure proofs), and ECHIDNA integration (neural proof synthesis for verification).
Location: /var/mnt/eclipse/repos/ochrance/ochrance-core/A2ML/Lexer.idr and /var/mnt/eclipse/repos/ochrance/ochrance-core/A2ML/Parser.idr (Idris2 modules)
How verified: Both modules use the %default total directive, requiring all functions to be total (no partial match, no undefined behavior). The lexer is structurally recursive: it tokenizes input by consuming characters and recursing on the remainder (proof: input size strictly decreases). The parser is similarly total: it parses tokens using sized types (List (n : Nat)) to guarantee termination (proof: token list shrinks). README (§Overview) claims "A2ML Parser/Validator" with compile-time structure proofs; this is verified by the Idris2 type checker itself — if either module had a partial function, idris2 --check would reject it with an error, not compile.
Caveat: Idris2 totality checking is a sound approximation but not perfect. Deeply nested mutual recursion can escape detection in rare cases, though practice shows this is extremely rare.
Location: /var/mnt/eclipse/repos/ochrance/ochrance-core/Framework/Merkle.idr (Idris2 Merkle tree with size-indexed types)
How verified: The Merkle tree is defined as a size-indexed binary tree: MerkleTree : (size : Nat) → Type. At compile time, Idris2 verifies that all leaf nodes are at depth log2(size). The tree operations (leaf insertion, hash computation, proof generation) take dependent proofs that structure is maintained. README (§Architecture) claims "Verified Merkle trees — Size-indexed binary trees with compile-time structure proofs." This is proven by the type signature itself: if you try to construct a tree of size 8 with only 7 leaves, the type checker rejects it because the dependent type MerkleTree 8 requires exactly 8 leaves.
Caveat: The placeholder hash functions in Merkle.idr use XOR, not cryptographic hashes (BLAKE3/SHA-256). This is noted in the CLAUDE.md as a critical TODO. The structure proofs are valid but cryptographic strength is absent.
Ochránce uses the hyperpolymath ABI/FFI standard: Idris2 specs → Zig FFI → C bindings. The filesystem module is the reference VerifiedSubsystem implementation for the ochrance-framework (which defines an abstract interface for Filesystem, Memory, Network, Crypto modules). This pattern is reused across proven (formally verified library) and feedback-o-tron (Idris2 ABI for submitter credentials).
Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechidna.so via Zig.
| Path | What’s There |
|---|---|
|
Structurally recursive, total lexer for A2ML markup (tokenizes manifest) |
|
Sized-type parser: parses tokens to AST with compile-time termination proof |
|
Semantic validation: ensures AST satisfies invariants (hash format, block refs, etc.) |
|
Roundtrip serialization: AST → A2ML → AST (identity proof) |
|
Abstract VerifiedSubsystem interface; defines what all subsystems must prove |
|
Proof witness types; generic proof structure for all subsystems |
|
Error taxonomy: q/* (query), p/* (proof), z/* (zone/system) |
|
FFI to ECHIDNA neural prover (via Zig C ABI) |
|
Filesystem types: FSState, Block, FSSnapshot with dependent proofs |
|
Verified Merkle tree: size-indexed with compile-time structure proofs (placeholder XOR hashes) |
|
Verification logic: block hashes, tree integrity, attestation signatures |
|
Linear type repair: repair operations consume old state (Quantity 1) |
|
Package definition for core library |
|
Package definition for filesystem module |
-
Lexer totality:
idris2 --check ochrance-core/A2ML/Lexer.idr— Idris2 type checker verifies structurally recursive, no partial functions -
Parser totality:
idris2 --check ochrance-core/A2ML/Parser.idr— sized types ensure termination proof -
Validator:
tests/validator_test.idr— roundtrip A2ML → AST → A2ML preserves structure -
Merkle tree:
tests/merkle_test.idr— size-indexed tree construction and hash verification -
Repair linearity:
tests/repair_test.idr— linear type system prevents use-after-repair bugs (compile-time error if violated) -
ECHIDNA FFI:
tests/echidna_ffi_test.idr— call libechidna.so via Zig FFI, verify proof synthesis works
-
Hashes: Currently XOR (placeholder). Must replace with BLAKE3/SHA-256 via Zig FFI.
-
Attestation: Cryptographic signature verification not yet integrated (planned).
-
Linear repair: Idris2 linear types framework incomplete for full use-after-repair prevention (ongoing research).