Skip to content

TOPOLOGY.adoc

Latest commit

 

History

History
127 lines (111 loc) · 9.58 KB

TOPOLOGY.adoc

File metadata and controls

127 lines (111 loc) · 9.58 KB
Raw

Ochránce — Project Topology

System Architecture

                        ┌─────────────────────────────────────────┐
                        │              OPERATOR / ADMIN           │
                        │        (Filesystem Audit / Verification)│
                        └───────────────────┬─────────────────────┘
                                            │
                                            ▼
                        ┌─────────────────────────────────────────┐
                        │           OCHRÁNCE CORE (IDRIS2)        │
                        │    (Dependent Types, Formal Proofs)     │
                        └──────────┬───────────────────┬──────────┘
                                   │                   │
                                   ▼                   ▼
                        ┌───────────────────────┐  ┌────────────────────────────────┐
                        │ INTEGRITY LAYER       │  │ MARKUP LAYER (A2ML)            │
                        │ - Verified Merkle     │  │ - Attestation DSL              │
                        │ - Linear Repair Ops   │  │ - Audit Manifests              │
                        │ - Size-indexed Trees  │  │ - Parser / Validator           │
                        └──────────┬────────────┘  └──────────┬─────────────────────┘
                                   │                          │
                                   └────────────┬─────────────┘
                                                ▼
                        ┌─────────────────────────────────────────┐
                        │           INTERFACE LAYER (FFI)         │
                        │  ┌───────────┐  ┌───────────────────┐  │
                        │  │  Zig FFI  │  │  C ABI Bridge     │  │
                        │  │  (System) │  │  (Shared Libs)    │  │
                        │  └─────┬─────┘  └────────┬──────────┘  │
                        └────────│─────────────────│──────────────┘
                                 │                 │
                                 ▼                 ▼
                        ┌─────────────────────────────────────────┐
                        │           ECHIDNA INTEGRATION           │
                        │    (Neural Proof Synthesis, Julia ML)   │
                        └─────────────────────────────────────────┘

                        ┌─────────────────────────────────────────┐
                        │          REPO INFRASTRUCTURE            │
                        │  Justfile Automation  .machine_readable/  │
                        │  Idris2 ipkg          0-AI-MANIFEST.a2ml  │
                        └─────────────────────────────────────────┘

Completion Dashboard

Percentages track proof / verification completeness — the honest axis for a verification framework — not “code exists”. docs/PROOFS.adoc is the authoritative ledger; this dashboard only summarises it. Where an implementation exists but its correctness is unproven (or is a stub), the bar reflects the proof, not the code.

COMPONENT                            STATUS         NOTES (proof / verification axis)
───────────────────────────────────  ──────────────  ────────────────────────────────────────────
CORE VERIFICATION (IDRIS2)
  Merkle soundness + round-trip       ███████░░░ 70%  merkleCorrect(With) + buildGetLeaf proven
  Merkle completeness + binding       █████░░░░░ 50%  binding DONE (merkleBinding; CR isolated in
                                                      MerkleAssumption); completeness converse open (4.1)
  A2ML parser + reference round-trip  ███████░░░ 70%  total; ref-codec proven; prod pipeline runtime-only
  Verify soundness                    ████████░░ 80%  Stages 2.1–2.4 proven (verifyRefsSound,
                                                      merkleRootVerifyHashSound mod CR+DecodeInjective);
                                                      residual: proof-token constructor visibility
  Validator + policy enforcement      ████████░░ 80%  validateManifestSound (4-tuple incl. policy);
                                                      require_sig/max_age proven enforced; residual:
                                                      canonical signing serialization + positive KAT
  Linear-type Repair                  ██████░░░░ 60%  Stages 3.1/3.2 proven (mod GoodRefs+hashRefl);
                                                      impl hash-map-only, no block I/O; linearity deferred
  VerifiedSubsystem law               █████░░░░░ 50%  interface + FSState instance; law not yet STATED
                                                      in Interface.idr (repairThenVerify proven at
                                                      pure-core level, not lifted)
  Progressive assurance               ███████░░░ 70%  attestedSatisfiesLax proven; monotonicity (Stage 4.3)

SYSTEM & EXTERNAL
  Zig crypto (BLAKE3/SHA/Ed25519)     █████████░ 90%  implemented + KAT-tested; Zig 0.15.2; 24 tests
                                                      (unit + linked C-ABI integration) CI-gated
  Crypto linked into verify flow      ███████░░░ 70%  libochrance.so built+linked+CI-gated end to end
                                                      (Idris2 workflow runs run_ffi_test.sh per PR);
                                                      residual: root-verify entry needs pure Combiner
                                                      (IO path open), ABI blake3Hash placeholder (#39)
  ECHIDNA integration                 █░░░░░░░░░ 10%  design types only; FFI entirely stubbed

REPO INFRASTRUCTURE
  Justfile automation                 ██████████ 100% build / verify tasks
  .machine_readable/                  ██████████ 100% STATE tracking active; descriptiles (post-6a2)
  Idris2 .ipkg / totality gate        ██████████ 100% 29 core modules; --total build green
  CI proof gate (Idris2 workflow)     ██████████ 100% every PR: full --total build + 3 fail-capable
                                                      suites + Idris→Zig FFI runtime test

────────────────────────────────────────────────────────────────────────────────────────────────
OVERALL (proof axis):                 ███████░░░ ~70% Stages 1–3 done (mod named hypotheses);
                                                      Stage 4 open: Merkle completeness, monotonicity
                                                      cases, VerifiedSubsystem law. See docs/PROOFS.adoc.

Key Dependencies

A2ML Manifest ───► Idris2 Parser ───► Merkle Root ───► Attestation
     │                 │                 │                │
     ▼                 ▼                 ▼                ▼
Linear Repr ─────► Verified FS ──────► C FFI ───────► ECHIDNA (ML)

Update Protocol

This file is maintained by both humans and AI agents. When updating:

  1. After completing a component: Change its bar and percentage

  2. After adding a component: Add a new row in the appropriate section

  3. After architectural changes: Update the ASCII diagram

  4. Date: Update the Last updated comment at the top of this file

Progress bars use: █ (filled) and ░ (empty), 10 characters wide. Percentages: 0%, 10%, 20%, … 100% (in 10% increments).

The bars track proof / verification completeness against docs/PROOFS.adoc (the authoritative ledger), not whether code merely exists. Do not raise a bar to 100% on the strength of an implementation alone — a component is “done” only when its correctness is proven or honestly bounded per the ledger.