Phase 1: Ochránce Core — 10/11 components complete (updated 2026-07-02)
The proof program’s Stages 1–3 are machine-checked and CI-enforced: the
Idris2 workflow builds every core module under --total on each PR, and
the Idris→Zig FFI runtime test proves the production Merkle path computes
real BLAKE3 across the %foreign boundary. The validator enforces policy
(require_sig, max_age freshness) with soundness theorems. Ledger of record:
docs/PROOFS.adoc. Remaining engineering: filling in the placeholder
integration scenarios, canonical signing serialization, and the Stage 4
proofs (Merkle completeness, progressive monotonicity, VerifiedSubsystem
law).
Target: Complete core verification framework with full A2ML support
Completion: 10/11 components
Components:
-
✓ A2ML Lexer (total, tested)
-
✓ A2ML Parser (total, tested)
-
✓ A2ML Validator (structural + policy enforcement proven sound; Ed25519 signature verification via FFI; residual: canonical signing serialization, positive-path signature KAT, trust-root story)
-
✓ A2ML Serializer (roundtrip proven for the reference token codec; production pipeline runtime-checked — the String-primitive wall, see PROOFS.adoc)
-
✓ Framework Interface (VerifiedSubsystem)
-
✓ Proof Witnesses (Lax/Checked/Attested modes)
-
✓ Error Taxonomy (q/p/z classification)
-
✓ Merkle Tree Implementation (size-indexed; real BLAKE3 via libochrance.so, CI-gated end to end; residual assumption: CollisionResistant, isolated)
-
✓ Filesystem Verification (verify soundness proven — Stages 2.2/2.4; residual: proof-token constructor visibility)
-
✓ Linear Type Repair (repair correctness proven — Stages 3.1/3.2; impl models hashes only, no block I/O; full linearity deferred, see PROOFS.adoc)
-
❏ Integration Tests (10 real scenarios green + fail-capable and CI-gated; 45 remaining placeholders to fill)
Critical Next Actions:
-
Canonical signing serialization (delimited, all-fields-bound) + positive-path Ed25519 known-answer test through validateManifestIO
-
Stage 4 proofs: Merkle completeness (4.1), remaining SatisfiesMinimum monotonicity cases (4.3), VerifiedSubsystem law stated + proven for FSState
-
Fill in the 45 placeholder integration scenarios
-
Make real BLAKE3 reachable from a root-verify entry point (IO path via the proven IO↔pure bridge; VerifyRoot currently requires a pure Combiner)
-
Require the Idris2 / Zig FFI checks in the repo ruleset (currently no required status checks — auto-merge lands before CI finishes)
Blockers:
-
None for the components above. Named boundaries: CollisionResistant hypothesis (isolated); ABI-layer blake3Hash placeholder + ECHIDNA FFI stub (issue #39, Phase 2 scope); attestation trust-root / key management (design decision needed)
Target: Bidirectional proof exchange with ECHIDNA neural prover
Components:
-
❏ FFI Implementation (Idris2 → Rust via libechidna.so)
-
❏ Proof Obligation Export (Idris2 → ECHIDNA)
-
❏ Synthesized Proof Import (ECHIDNA → Idris2)
-
❏ Bidirectional Proof Exchange Protocol
-
❏ Integration Tests (100+ proof scenarios)
-
❏ Multi-prover Support (via idris2-echidna bindings)
Prerequisites:
-
Phase 1 complete (all core components 100%)
-
libechidna.so built and accessible
-
idris2-echidna bindings available
Target: Train ECHIDNA on Ochránce proof corpus for automated synthesis
Components:
-
❏ Proof Corpus Collection (200+ Idris2 examples)
-
❏ Corpus Annotation (proof patterns, tactics)
-
❏ Synthesis Pipeline Integration
-
❏ Evaluation Benchmarks (precision/recall)
-
❏ Automated Proof Search
-
❏ Performance Optimization
Deliverables:
-
Annotated proof corpus (200+ examples)
-
Trained synthesis model
-
Benchmark results
Target: Production-ready filesystem verification for OSTree deployments
Components:
-
❏ OSTree Integration (pre/post-transaction hooks)
-
❏ Performance Benchmarks (verification latency)
-
❏ Security Audit (external review)
-
❏ Production Documentation
-
❏ Thesis Document
-
❏ Case Studies (Fedora Kinoite, etc.)
Integration Points:
-
OSTree transaction hooks (
/etc/ostree/hooks/) -
Systemd service units for continuous verification
-
Journal integration for audit logging
-
Complete A2ML parsing, validation, and serialization
-
Verified Merkle trees with BLAKE3 hashing
-
Filesystem verification and linear type repair
-
50+ integration test scenarios
-
Bidirectional FFI with libechidna.so
-
Proof obligation export and import
-
100+ proof test scenarios
-
200+ proof corpus for training
-
Automated proof synthesis pipeline
-
Performance benchmarks
-
Multi-filesystem Support: Extend beyond reference implementation
-
Distributed Verification: Merkle proof sharing across nodes
-
Proof Cache: Store and reuse previously verified proofs
-
Hardware Acceleration: GPU-accelerated hashing (BLAKE3)
-
Cross-language Bindings: FFI for Rust, C, ReScript
-
Real-time Verification: Continuous filesystem monitoring
See CONTRIBUTING.md for guidelines on:
-
Writing total Idris2 functions
-
Property-based testing
-
Proof corpus contribution
-
Integration test scenarios