Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
78 lines (54 loc) · 7.54 KB

EXPLAINME.adoc

File metadata and controls

78 lines (54 loc) · 7.54 KB
Raw

Ochránce — Show Me The Receipts

Table of Contents

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.

— README

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).

Two Verifiable Claims from How-It-Works

Claim 1: A2ML Lexer and Parser Are Structurally Recursive and Total

Location: ochrance-core/A2ML/Lexer.idr and 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.

Claim 2: Verified Merkle Tree Size Guarantees Are Compile-Time Proofs

Location: ochrance-core/Filesystem/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 size-indexed structure proofs are independent of hash strength. The cryptographic path is live: the Zig FFI implements BLAKE3/SHA-256/SHA3-256 (ffi/zig/src/main.zig, known-answer-vector tested), build.zig emits libochrance.so, and the IO Merkle path calls hashPairBlake3 across %foreign — confirmed end to end by tests/ffi/CryptoFFITest.idr (the production root is the BLAKE3 fold, not the XOR spec root) and CI-gated in the Idris2 and Zig FFI workflows. The pure XOR combiner (xorCombiner) is the totality-friendly spec instance of the combiner-generic theorems, not a fallback. The irreducible crypto assumption is CollisionResistant, isolated in Filesystem.MerkleAssumption.

Dogfooded Across The Account

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.

File Map

Path What’s There

ochrance-core/A2ML/Lexer.idr

Structurally recursive, total lexer for A2ML markup (tokenizes manifest)

ochrance-core/A2ML/Parser.idr

Sized-type parser: parses tokens to AST with compile-time termination proof

ochrance-core/A2ML/Validator.idr

Semantic validation: ensures AST satisfies invariants (hash format, block refs, etc.)

ochrance-core/A2ML/Serializer.idr

Roundtrip serialization: AST → A2ML → AST (identity proof)

ochrance-core/Framework/Interface.idr

Abstract VerifiedSubsystem interface; defines what all subsystems must prove

ochrance-core/Framework/Proof.idr

Proof witness types; generic proof structure for all subsystems

ochrance-core/Framework/Error.idr

Error taxonomy: q/* (query), p/* (proof), z/* (zone/system)

ochrance-core/Framework/FFI/Echidna.idr

FFI to ECHIDNA neural prover (via Zig C ABI)

ochrance-core/Ochrance/Filesystem/Types.idr

Filesystem types: FSState, Block, FSSnapshot with dependent proofs

ochrance-core/Ochrance/Filesystem/Merkle.idr

Verified Merkle tree: height-indexed with compile-time structure proofs and the merkleCorrect inclusion-soundness theorem (placeholder XOR hashes for the pure path)

ochrance-core/Ochrance/Filesystem/Verify.idr

Verification logic: block hashes, tree integrity, attestation signatures

ochrance-core/Ochrance/Filesystem/Repair.idr

Linear type repair: repair operations consume old state (Quantity 1)

ochrance.ipkg

Package definition for the core library (includes the filesystem subsystem)

Testing Critical Paths

  • Lexer/Parser totality: idris2 --build ochrance.ipkg (opts --total) — every core module, including the lexer’s structural recursion and the parser’s sized-type termination, type-checks under the totality checker; CI-gated by the Idris2 workflow

  • Parser/roundtrip: tests/A2ML/ParserTests.idr — lex/parse/serialize roundtrip and error handling (fail-capable, CI-gated)

  • Properties: tests/property/PropertyTests.idr — 47 property checks across hex roundtrip, Merkle, repair idempotence, and validation (incl. policy rejection cases)

  • Integration: tests/integration/IntegrationTests.idr — manifest generation → validation → verification → repair scenarios

  • Crypto FFI runtime: tests/ffi/CryptoFFITest.idr (via tests/ffi/run_ffi_test.sh) — real BLAKE3/SHA-256/SHA3-256 across %foreign into libochrance.so; proves the production Merkle root ≠ XOR spec root

  • ECHIDNA FFI: not yet testable — Ochrance.FFI.Echidna is a design stub (Left "FFI not yet implemented"); see ROADMAP Phase 2

Known Limitations & TODOs

  • Hashes: BLAKE3/SHA-256/SHA3-256 are implemented in the Zig FFI (ffi/zig/src/main.zig, tested via zig build test) and wired into the Idris production path through %foreign. build.zig emits libochrance.so; a C dlopen link test (ffi/zig/test/link_test.c, KAT vectors, CI-gated in zig-ffi.yml) and an Idris→FFI runtime test (tests/ffi/CryptoFFITest.idr) confirm real BLAKE3 end to end — the production Merkle root is the BLAKE3 fold, not the XOR root. The dead zero-hash stubs are removed; the pure XOR combiner is renamed xorCombiner (the spec instance of the combiner-generic proofs). Residual assumption: CollisionResistant (isolated, pigeonhole-false).

  • Attestation: Ed25519 verification is implemented (Zig FFI + validateManifestIO). Remaining: a trust-root / key-management story and end-to-end integration before claiming full attestation.

  • Linear repair: Idris2 linear types framework incomplete for full use-after-repair prevention (ongoing research).

Questions?

Open an issue or reach out directly — happy to explain anything in more detail.