Skip to content

Commit 92a5ae2

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add ARCHITECTURE.md with reversibility stack + reposystem boundary
Documents P0-P2 from repo tangle assessment. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 31a2f85 commit 92a5ae2

1 file changed

Lines changed: 164 additions & 0 deletions

File tree

‎docs/ARCHITECTURE.md‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
3+
4+
# Architecture: Ochrance and the Reversibility Stack
5+
6+
This document addresses tangles P0-P2 from the repo tangle assessment, clarifying
7+
canonical ownership, the reversibility stack layering, and the reposystem boundary.
8+
9+
---
10+
11+
## P0: Canonical Repository Status
12+
13+
**ochrance** is the canonical repository for verified subsystem integrity work.
14+
15+
The former `ochrance-framework` repository has been archived with a redirect notice.
16+
All valuable content (Progressive.idr, Containerfile, flake.nix) was merged into this
17+
repo before archival. The framework repo originally envisioned a broader four-subsystem
18+
architecture (Filesystem, Memory, Network, Crypto), but the concrete filesystem
19+
verification implementation here in ochrance is the active, thesis-scope work.
20+
21+
Going forward, any new subsystem modules (Memory, Network, Crypto) will be developed
22+
as peer repos implementing the `VerifiedSubsystem` interface defined in
23+
`ochrance-core/Ochrance/Framework/Interface.idr`, not in a separate framework repo.
24+
25+
---
26+
27+
## P1: The Reversibility Stack
28+
29+
Three repositories form a layered reversibility stack. Each layer is self-contained
30+
but designed to compose upward:
31+
32+
```
33+
+------------------------------------------------------------+
34+
| ochrance |
35+
| Filesystem verification with dependent types (Idris2) |
36+
| Merkle trees, A2ML manifests, progressive assurance |
37+
| "Is the filesystem still what we said it was?" |
38+
+------------------------------------------------------------+
39+
| consumes reversibility primitives from
40+
v
41+
+------------------------------------------------------------+
42+
| valence-shell (vsh) |
43+
| Formally verified shell with proven reversibility |
44+
| 250+ theorems across 6 proof systems, MAA framework |
45+
| "Every shell operation can be undone, always" |
46+
+------------------------------------------------------------+
47+
| built on theory from
48+
v
49+
+------------------------------------------------------------+
50+
| januskey |
51+
| Reversible file operations via Maximal Principle Reduction |
52+
| Content-addressed storage, transaction support (Rust) |
53+
| "Data loss is architecturally impossible" |
54+
+------------------------------------------------------------+
55+
```
56+
57+
### Layer Boundaries
58+
59+
**januskey** (bottom layer -- theory and primitives):
60+
- Provides the foundational reversibility guarantee: every file operation carries
61+
sufficient metadata for perfect inversion.
62+
- Implements content-addressed storage with SHA256 deduplication.
63+
- Transaction manager groups operations for atomic commit/rollback.
64+
- Language: Rust. Interface: CLI (`jk` commands).
65+
- Key property: *data loss is architecturally impossible* -- not unlikely, but
66+
structurally prevented by storing inverse metadata with every operation.
67+
68+
**valence-shell** (middle layer -- shell/CLI reversibility):
69+
- Extends reversibility from file operations to full shell semantics.
70+
- Proves reversibility theorems in 6 independent proof systems (Coq, Lean 4, Agda,
71+
Isabelle/HOL, Mizar, Z3) for cross-validation.
72+
- MAA (Mutually Assured Accountability) framework provides provable audit trails.
73+
- Key theorems: `rmdir(mkdir(p, fs)) = fs`, operation sequence composition reversal.
74+
- Language: Rust CLI + formal proofs. Status: advanced research prototype (v0.9.0).
75+
- Trust boundary: formal proofs operate on abstract models; the Lean-to-Rust
76+
extraction gap is not yet formally verified.
77+
78+
**ochrance** (top layer -- filesystem verification):
79+
- Uses dependent types (Idris2) for mathematically proven filesystem integrity.
80+
- Progressive strictness: Lax (structure only) / Checked (hash verification) /
81+
Attested (full dependent type proofs).
82+
- A2ML (Attestation & Audit Markup Language) manifests describe verified state.
83+
- Integrates with ECHIDNA for neural proof synthesis.
84+
- Architecture: L0 Hardware -> L1 C Shims -> L2 Idris2 Proofs -> L3 Repair ->
85+
L4 Policy -> L5 TUI.
86+
87+
### How They Relate
88+
89+
- **januskey** answers: "Can I undo this file operation?" (yes, always)
90+
- **valence-shell** answers: "Can I undo this shell session?" (yes, with proofs)
91+
- **ochrance** answers: "Has anything changed that shouldn't have?" (verified)
92+
93+
januskey provides the *operational* reversibility (undo what you did). valence-shell
94+
extends this to *shell-level* reversibility with formal guarantees. ochrance provides
95+
*verification* that the filesystem matches its declared state, using a different
96+
technique (dependent type proofs over Merkle trees rather than operation-level
97+
inversion).
98+
99+
The stack is loosely coupled: each layer is independently useful, but together they
100+
provide a complete story from "operations are reversible" through "the shell proves it"
101+
to "the filesystem is verified."
102+
103+
---
104+
105+
## P2: Reposystem Boundary
106+
107+
### Inside reposystem (monorepo subdirectories)
108+
109+
The [reposystem](https://github.com/hyperpolymath/reposystem) monorepo contains tools
110+
that form the "railway yard" for multi-repo ecosystem management:
111+
112+
| Subdirectory | Purpose |
113+
|----------------|------------------------------------------------------------|
114+
| **contractiles** | Contract-based CLI system (must/trust/dust/intend/k9) |
115+
| **bitfuckit** | Bitbucket API integration and forge tooling |
116+
| **claim-forge** | Repository claiming and ownership verification |
117+
| **scaffoldia** | Project scaffolding and template validation |
118+
119+
These belong inside reposystem because they are all *repo infrastructure tools* --
120+
they operate on repositories as first-class objects, they share the graph/slot/provider
121+
data model, and they feed into the reposystem TUI and scenario comparison views.
122+
123+
### Standalone (outside reposystem)
124+
125+
**checky-monkey** and **grim-repo** overlap with reposystem's concerns but remain
126+
standalone for the following reasons:
127+
128+
**checky-monkey** (userscript validation platform):
129+
- Operates on a fundamentally different domain: userscripts, userstyles, and browser
130+
extensions -- not git repositories.
131+
- Has its own persistence layer (CUBS content-addressed database), its own API
132+
(GraphQL + REST), and its own distribution mechanism (IPFS).
133+
- The overlap with reposystem is limited to sharing the validation/quality-gate
134+
pattern. checky-monkey validates *scripts*; reposystem validates *repo structure*.
135+
- Technology stack diverges: Haskell core, Lua plugins, PostgreSQL -- versus
136+
reposystem's Rust CLI + ReScript data model.
137+
- Standalone because: **different domain, different data model, different tech stack.**
138+
139+
**grim-repo** (audit-grade repo tooling):
140+
- Provides modular auditing (structure bootstrapping, community standards, golden
141+
registry checks) that could theoretically live inside reposystem.
142+
- Remains standalone because it is designed as a *userscript/browser extension*
143+
that runs on forge web UIs (GitLab, GitHub, Bitbucket pages), not as a CLI or
144+
library consumed by reposystem.
145+
- Its deployment model (browser injection via Tampermonkey/Violentmonkey) is
146+
incompatible with being a reposystem subdirectory.
147+
- It follows a progression model (Raw -> Golden -> Rhodium) that is complementary
148+
to but independent of reposystem's scenario/aspect system.
149+
- Standalone because: **different deployment model (browser extension vs CLI),
150+
different user interaction pattern (forge web UI vs terminal).**
151+
152+
### Decision Criteria
153+
154+
A tool belongs inside reposystem if it:
155+
1. Operates on git repositories as its primary domain object.
156+
2. Shares the slot/provider/scenario data model.
157+
3. Is consumed as a library or CLI component (not a browser extension).
158+
4. Benefits from the shared graph view and scenario comparison.
159+
160+
A tool remains standalone if it:
161+
1. Has a fundamentally different domain (scripts, not repos).
162+
2. Has an incompatible deployment model (browser vs terminal).
163+
3. Has its own persistence and API requirements.
164+
4. Would create unnecessary coupling if embedded.

0 commit comments

Comments
 (0)