|
| 1 | +<!-- SPDX-License-Identifier: PMPL-1.0-or-later --> |
| 2 | +# JanusKey Architecture — Reversibility Stack Junction Point |
| 3 | + |
| 4 | +## Lineage |
| 5 | + |
| 6 | +``` |
| 7 | +maa-framework (policy vision) |
| 8 | + → absolute-zero (certified null operations — formal theory) |
| 9 | + → januskey (development proof-of-concept — this repo) |
| 10 | + → THREE downstream applications: |
| 11 | + ├── ochrance — neurosymbolic filesystem verification (Idris2) |
| 12 | + ├── valence-shell — formally verified reversible shell (Rust + 6 proof systems) |
| 13 | + └── aletheia — reversible OS operations (early research) |
| 14 | +``` |
| 15 | + |
| 16 | +JanusKey is the **junction point** where absolute-zero's theoretical work on Certified |
| 17 | +Null Operations (CNOs) was first applied to practical file operations. The three |
| 18 | +downstream applications independently implemented reversibility, but shared no code — |
| 19 | +until the `reversible-core` extraction described below. |
| 20 | + |
| 21 | +## Workspace Structure |
| 22 | + |
| 23 | +``` |
| 24 | +januskey/ |
| 25 | +├── crates/ |
| 26 | +│ ├── reversible-core/ ← SHARED LIBRARY (the integration surface) |
| 27 | +│ │ ├── content_store — SHA256 content-addressed storage |
| 28 | +│ │ ├── metadata — OperationMetadata + MetadataStore (append-only log) |
| 29 | +│ │ ├── transaction — Transaction lifecycle (begin/commit/rollback) |
| 30 | +│ │ ├── manifest — A2ML emitter (bridge to ochrance verification) |
| 31 | +│ │ ├── error — ReversibleError types |
| 32 | +│ │ └── lib — ReversibleExecutor trait |
| 33 | +│ │ |
| 34 | +│ └── januskey-cli/ ← CLI TOOL (depends on reversible-core) |
| 35 | +│ ├── operations — FileOperation executor (actual filesystem ops) |
| 36 | +│ ├── keys — Key management (AES-GCM, Argon2) |
| 37 | +│ ├── attestation — Audit trail |
| 38 | +│ ├── obliteration — Secure deletion |
| 39 | +│ ├── delta — Differential operations |
| 40 | +│ ├── main — jk CLI binary |
| 41 | +│ └── keys_cli — jk-keys CLI binary |
| 42 | +│ |
| 43 | +└── src/januskey/ ← LEGACY (pre-extraction, superseded by crates/) |
| 44 | +``` |
| 45 | + |
| 46 | +## reversible-core: The Shared Foundation |
| 47 | + |
| 48 | +`reversible-core` is a lean Rust library crate (no CLI deps) that provides the types |
| 49 | +all three downstream applications share: |
| 50 | + |
| 51 | +### ReversibleExecutor Trait |
| 52 | + |
| 53 | +```rust |
| 54 | +pub trait ReversibleExecutor { |
| 55 | + type Op; |
| 56 | + type Metadata; |
| 57 | + type Error; |
| 58 | + |
| 59 | + fn execute(&mut self, op: Self::Op) -> Result<Self::Metadata, Self::Error>; |
| 60 | + fn undo(&mut self, metadata_id: &str) -> Result<Self::Metadata, Self::Error>; |
| 61 | + fn generate_manifest(&self) -> Result<String, Self::Error>; |
| 62 | +} |
| 63 | +``` |
| 64 | + |
| 65 | +This is the **Rust-side mirror** of ochrance's `VerifiedSubsystem` interface (Idris2). |
| 66 | +The `generate_manifest` method emits A2ML that ochrance can parse and verify. |
| 67 | + |
| 68 | +### CNO Correspondence |
| 69 | + |
| 70 | +Per absolute-zero, every `OperationType` has a known inverse: |
| 71 | + |
| 72 | +| Operation | Inverse | Property | |
| 73 | +|-----------|---------|----------| |
| 74 | +| Delete | Create | `delete ; create ≡ CNO` | |
| 75 | +| Create | Delete | `create ; delete ≡ CNO` | |
| 76 | +| Modify | Modify | Self-inverse (stores old+new content) | |
| 77 | +| Move | Move | Self-inverse (swap src/dst) | |
| 78 | +| Copy | Delete | `copy ; delete_copy ≡ CNO` | |
| 79 | +| Chmod | Chmod | Self-inverse (stores old mode) | |
| 80 | +| Chown | Chown | Self-inverse (stores old uid:gid) | |
| 81 | + |
| 82 | +### A2ML Bridge to Ochrance |
| 83 | + |
| 84 | +`ManifestEmitter::generate()` produces A2ML manifests containing: |
| 85 | +- Manifest header (version, subsystem, timestamp, Merkle root) |
| 86 | +- Refs (one per operation, with content hash) |
| 87 | +- Policy (verification mode) |
| 88 | + |
| 89 | +Ochrance parses these and produces `VerificationProof` witnesses: |
| 90 | +- `LaxProof` — manifest is well-formed |
| 91 | +- `CheckedProof` — all content hashes verified via BLAKE3 |
| 92 | +- `AttestedProof` — manifest is signed (Ed25519) |
| 93 | + |
| 94 | +## Integration Status |
| 95 | + |
| 96 | +### Phase 1: reversible-core extraction ✅ DONE (2026-03-21) |
| 97 | + |
| 98 | +Extracted core types from januskey into `reversible-core`. Workspace builds, |
| 99 | +44 tests pass. januskey-cli re-exports all types for backward compatibility. |
| 100 | + |
| 101 | +### Phase 2: valence-shell integration — NEXT |
| 102 | + |
| 103 | +Wire valence-shell (`impl/rust-cli/`) to depend on `reversible-core`: |
| 104 | +- Add `ContentStore` to `ShellState` for content-addressed undo data |
| 105 | +- Replace inline `undo_data: Option<Vec<u8>>` for large file content |
| 106 | +- Add `a2ml_emitter.rs` for manifest generation |
| 107 | +- Replace `verification.rs` stubs with `ReversibleExecutor` implementation |
| 108 | + |
| 109 | +### Phase 3: ochrance ABI extension — PENDING |
| 110 | + |
| 111 | +Add reversibility types to ochrance's Idris2 ABI: |
| 112 | +- `src/abi/Ochrance/ABI/Reversibility.idr` — `ReversibleOp`, `ReversibilityProof` |
| 113 | +- `ochrance-core/Ochrance/Subsystem/OperationLog.idr` — `VerifiedSubsystem` for op logs |
| 114 | + |
| 115 | +### Phase 4: Cross-repo documentation — PENDING |
| 116 | + |
| 117 | +Update ARCHITECTURE.md and ECOSYSTEM.a2ml in all three repos with cross-references. |
| 118 | + |
| 119 | +### Deferred |
| 120 | + |
| 121 | +- **aletheia**: Too early (Phase 0 research, no operation types yet) |
| 122 | +- **Merkle tree compatibility**: ochrance uses BLAKE3 height-indexed trees; Rust side |
| 123 | + needs compatible implementation |
0 commit comments